2.2.5. Two perspectives on derivations

The locations of the stage numbers appearing in a derivation reflect the patterns of argument on which the derivation rules are based. The label for a rule always appears to the left of the conclusion of such an argument, and the number of the stage at which the rule was applied appears not only next to the label but also to the right of the premises of the argument. A tree form proof can be reconstructed from the derivation by beginning with the final conclusion and working backward to the premises from which it was concluded, the premises from which those were concluded, and so on.

If we apply this idea to the example of the last section (which is reproduced below), we get the tree-form proof following it.

The sentence B concluded by Ext at the second stage of the derivation does not appear in the tree-form proof because it is not used as a premise for any later conclusions, something that can directly determined from the derivation by the fact that it has no stage number to its right.

Looked at in this way, a derivation could be thought of as the result of disassembling a tree-form proof and stacking the pieces up vertically. When reassembling the tree, we paid no attention to the horizontal organization provided by scope lines. The order of the stage numbers played no role either: they could just as well have been arbitrary codes used to mark corresponding parts of the tree so they could be fit together again. Indeed, even the vertical order of the lines of the derivation did not matter. Matching numbers on the left with numbers on the right is all that was necessary to reassemble the tree, and pieces could have been given to us in an unorganized heap. However, all these features of derivations, which are not needed to reconstruct a tree-form proof, do matter for another, and more important, way of looking at derivations, one in which a derivation is associated with a sequent proof.

To see this association, first use the stage numbers, scope lines, and the vertical ordering of lines to determine the way the gaps of the derivation develop over time, beginning with the intial gap, eventually dividing, and finally closing. That is shown on the right in the diagram below, where the stages are arrayed left to right and gaps are indicated by circles, with a filled circle used to indicate closure and an empty circle used to indicate a gap that is open. Colors are used to emphasize where and when changes occur.

Now turn the tree pattern counterclockwise so that the tree grows upward. The result is shown on the left below. Then associate with each open gap the argument whose conclusion is the goal of the gap and whose premises are the active resources of the gap, a argument that we will refer to as the proximate argument of the gap. These two steps yield the tree on the right below (where the fact that an argument is valid is again indicated by a filled circle). Colored sentences are new additions as the tree grows (something that is shown by the dashed lines below them); the other sentences at a stage are repeated from earlier stages. Resources that become inactive and goals that are replaced as the derivation develops have dashed lines above them.

The tree on the right amounts to a schematic way of writing a sequent proof. The only differences are the use of the argument slash instead of the entailment sign and the more graphic indication of the branches. We will call this the argument tree associated with a derivation. It serves not only to emphasize the features derivations share with sequent proofs but also to present the sort of information about derivations that will be needed when we go on (in 2.3) to consider the general properties of derivations. Indeed, a derivation can be thought of as an abbreviated way of writing its argument tree.