View source for Derivation tree

{{TEX|done}}
A notation for derivations (cf. [[Derivation, logical|Derivation, logical]]) in a [[Calculus|calculus]], in which the elements of the derivations from which $P$ is obtained by one application of a [[Derivation rule|derivation rule]] are written down above each element $P$. For instance, the derivation $P_1,\ldots,P_6$ in which $P_1$, $P_2$ and $P_4$ are axioms, $P_3$ is obtained by one application of some rule from $P_1$ and $P_2$, and $P_5$ is obtained from $P_4$ and $P_3$, while $P_6$ is obtained from $P_3$ and $P_5$, may be written down as follows:

$$\dfrac{P_1,P_2}{P_3}\quad\dfrac{\dfrac{P_4,\dfrac{P_1,P_2}{P_3}}{P_5}}{P_6}$$

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.