2.2.4. An example

Now, let us look at an example using these rules. 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 goal we are planning for. The stage number therefore appears at the right of the new goals and to the left of the old one.

│(A ∧ B) ∧ C 1
│D
├─
1 Ext │A ∧ B 2
1 Ext │C
2 Ext │A
2 Ext │B
├─
│C 3
├─
│A ∧ D3
├─
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. Although these are separate stages, they are independent of one another and could have been done in any order, so all three are shown together. 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 (both shown in blue).

│(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)

If your browser has JavaScript enabled, the diagram below can be used to display each stage in the development of the derivation we have been considering. Simply place the cursor over the number of the stage. (0 is used as the number of the initial stage.) Moving the cursor along the series of numbers will replay the stages in sequence.

0 1 2 3 4 5 6 7
(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)

When this sort of animation is not available, the stage numbers in a completed derivation can be used to reconstruct its history.

Glen Helman 01 Aug 2011