next up previous
Next: The relationship between proof-trees Up: Short description of the Previous: Formula-trees

Proof-trees

We now describe the set of rules that given a formula-tree of some type $\varphi$ allows us to build proof-trees for $\varphi$ and give then two conditions to be satisfied by such a proof-tree in order to be valid. Below we will use the notation $\overline{o}$ to refer to a specific occurrence of an object $o$.

Proof-trees are tree-like structures and in the following we shall use the notation $\begin{array}{c} \vdots A \end{array}$ to designate a proof-tree with a variable $A$ at some leaf. Now, consider a type $\varphi$ and let ${\tt pp}(\varphi) = \{p_0,\ldots,p_n\}$ be the set of primitive parts in the formula-tree of $\varphi$, where $p_0 =
\begin{array}{c}\vert A\end{array}$ is the primitive part in the root of ${\tt tree}(\varphi)$ (thus the only primitive part of form (P1) in ${\tt pp}(\varphi)$). Then, the set of proof-trees for $\varphi$ is given by the following:


Definition 3.4   Given a proof-tree $\tt PT$ for a type $\varphi$, we call it a valid proof-tree for $\varphi$ iff


This last item corresponds to the hierarchy of ${\tt tree}(\varphi)$ being imposed on the construction of a valid proof-tree.


next up previous
Next: The relationship between proof-trees Up: Short description of the Previous: Formula-trees
Sabine Broda