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 allows us to build proof-trees for and give then two conditions to be satisfied by such a proof-tree in order to be valid. Below we will use the notation to refer to a specific occurrence of an object .

Proof-trees are tree-like structures and in the following we shall use the notation to designate a proof-tree with a variable at some leaf. Now, consider a type and let be the set of primitive parts in the formula-tree of , where is the primitive part in the root of (thus the only primitive part of form (P1) in ). Then, the set of proof-trees for is given by the following:

• If , then is a proof-tree for ;
• if is a proof-tree for and , where , then is a proof-tree for ;
• if is a proof-tree for and , then is a proof-tree for .

Definition 3.4   Given a proof-tree for a type , we call it a valid proof-tree for iff
• all leaves in are of form (P3), i.e. no branch in ends with a variable;
• if , with is a primitive part in the formula-tree , and is a direct descendent/child of at branch , with , then above every occurrence of in there is at least one occurrence of in , such that the occurrence occurs in the subtree of rooted in the 'th branch of .

This last item corresponds to the hierarchy of being imposed on the construction of a valid proof-tree.

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