Derivation tree

A notation for derivations (cf. Derivation, logical) in a calculus, in which the elements of the derivations from which is obtained by one application of a derivation rule are written down above each element . For instance, the derivation in which , and are axioms, is obtained by one application of some rule from and , and is obtained from and , while is obtained from and , may be written down as follows:

This notation, though more cumbersome than the linear notation, often proves to be a convenient tool in the investigation of derivations: It is easy to follow up the interconnections between the elements; the information comprised in the derivation tree represents a more complete description of the situation than does linear ordering (its completeness is almost as satisfactory as that of the information comprised in an analytical derivation). If required, the derivation tree is also given an analysis, i.e. each line is written with the number of the respective rule; axioms are written with their numbers.