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.

│(A ∧ B) ∧ C │D ├─ │ │ │ │ │ │ │ │ │ │ │ │ │ │ │ │ │ │ ├─ │C ∧ (A ∧ D)

│(A ∧ B) ∧ C 1 │D ├─ 1 Ext │A ∧ B 1 Ext │C │ │ │ │ │ │ │ │ │ │ │ │ │ │ │ │ ├─ │C ∧ (A ∧ D)

│(A ∧ B) ∧ C 1 │D ├─ 1 Ext │A ∧ B 2 1 Ext │C 2 Ext │A 2 Ext │B │ │ │ │ │ │ │ │ │ │ │ │ │ │ ├─ │C ∧ (A ∧ D)

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.

│(A ∧ B) ∧ C 1 │D ├─ 1 Ext │A ∧ B 2 1 Ext │C 2 Ext │A 2 Ext │B │ ││ │├─ ││C 3 │ ││ ││ ││ ││ ││ ││ ││ │├─ ││A ∧ D 3 ├─ 3 Cnj │C ∧ (A ∧ D)

│(A ∧ B) ∧ C 1 │D ├─ 1 Ext │A ∧ B 2 1 Ext │C 2 Ext │A 2 Ext │B │ ││ │├─ ││C 3 │ │││ ││├─ │││A 4 ││ │││ ││├─ │││D 4 │├─ 4 Cnj ││A ∧ D 3 ├─ 3 Cnj │C ∧ (A ∧ D)

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.

│(A ∧ B) ∧ C 1 │D ├─ 1 Ext │A ∧ B 2 1 Ext │C (5) 2 Ext │A 2 Ext │B │ ││● │├─ 5 QED ││C 3 │ │││ ││├─ │││A 4 ││ │││ ││├─ │││D 4 │├─ 4 Cnj ││A ∧ D 3 ├─ 3 Cnj │C ∧ (A ∧ D)

│(A ∧ B) ∧ C 1 │D ├─ 1 Ext │A ∧ B 2 1 Ext │C (5) 2 Ext │A (6) 2 Ext │B │ ││● │├─ 5 QED ││C 3 │ │││● ││├─ 6 QED │││A 4 ││ │││ ││├─ │││D 4 │├─ 4 Cnj ││A ∧ D 3 ├─ 3 Cnj │C ∧ (A ∧ D)

│(A ∧ B) ∧ C 1 │D (7) ├─ 1 Ext │A ∧ B 2 1 Ext │C (5) 2 Ext │A (6) 2 Ext │B │ ││● │├─ 5 QED ││C 3 │ │││● ││├─ 6 QED │││A 4 ││ │││● ││├─ 7 QED │││D 4 │├─ 4 Cnj ││A ∧ D 3 ├─ 3 Cnj │C ∧ (A ∧ D)

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 exploitation chains. 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 an analysis tree. And in the last three stages only the line is added because we are merely connecting exploitation chains to an analysis tree.

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 analysis tree.

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 at the end of an exploitation chain. This is because, to save space, only exploitation chains that figure in the final proof are shown. The fact that the resource B is left dangling at the end of an exploitation chain that is never connected to the analysis tree corresponds to the absence of a stage number at its right in the final state of the derivation, for both are consequences of the fact that it never serves as a premise for a further conclusion.