2.2.4. An example

Now, let us restate an example for which we used tree-form proofs, now using the notation for derivations. The development is shown stage by stage below. At each stage, new material is shown in red. Resources that are exploited or goals that are planned for are shown in blue. At each of the stages 1 and 2, a resource is exploited. The added resources are conclusions drawn from the exploited resource, so the number of the stage is written at the left of the resources that are added and at the right of the one that is exploited.

In stages 3 and 4, we plan for goals. The goals we add in each case are premises from which we plan to conclude the one they replace. The stage number therefore appears at the right of the new goals and to the left of the one we plan for.

In the last three stages we close gaps.

No sentences are added and the stage numbers merely mark the connection between resources that serve as premises and the goals that are concluded from them.

The proof tree from the original example is shown below with corresponding stage numbers added and with colors used to group items added at the same stage.

In stages 1 and 2, the new sentences lie below the horizontal line that is added because they are conclusions we draw as we move down chains of conclusions. In stages 3 and 4, the new sentences are above the line because they are premises from which we plan to reach the conclusion lying below them in a tree-form proof. And in the last three stages only the line is added because we are merely connecting conclusions we have accumulated to premises we have found we need. We use the label QED here, treating it as a pattern of argument whose conclusion is its only premise.

The diagram below shows the derivation and tree-form proof side by side. If your browser has JavaScript enabled, it can be used to display the state of both the derivation and the tree-form proof stage by stage. Simply place the cursor over the number of each stage in turn. (0 is used as the number of the initial stage.) The elements of the tree-form proof are shown in their final location, so the premises appear (with the first one repeated) above the points where they are eventually connected to the branches growing up from the conclusion.

One difference between the two proofs appears at stage 2, when the resources A and B are added to the derivation while only A appears as a conclusion in the tree-form proof. This is because a derivation leads us to accumulate as many conclusions as possible from our premises and B is one that is never needed to reach the final conclusion, something that is shown by the fact that no number appears to its right.