2.2.5. More rules

The principles Ex Nihilo Verum and Ex Falso Quodlibet appear in derivations as rules for closing gaps. In the case of the first, for a gap to be closed it is enough that it have ⊤ as its goal. No resource is involved, and the stage number appears only as an annotation to the goal. The rule EFQ takes a form much like QED except that having ⊥ as a resource enables us to close a gap no matter what its goal is. (If the goal also was ⊥, either EFQ or QED could be used.)

│... │ ││... ││ │├─ ││⊤ │...

│... │ ││... ││● │├─ n ENV ││⊤ │...

Fig. 2.2.5-1. Closing a gap that has ⊤ as its goal.

│... │⊥ │... │ ││... ││ │├─ ││φ │...

│... │⊥ (n) │... │ ││... ││● │├─ n EFQ ││φ │...

Fig. 2.2.5-2. Closing a gap that has ⊥ among its resources.

In 2.2.1, ENV and EFQ were illustrated by using tree-form proofs to show that A, B ⇒ (B ∧ ⊤) ∧ A and that A ∧ (⊥ ∧ B) ⇒ C ∧ D. As derivations, these proofs take the following forms:

Notice that, while every stage number of the second derivation appears somewhere among the annotations on its right-hand side, the same is not true of the first derivation because stage 4 is missing. Of course, that’s because stage 4 is when we used ENV, and ENV is a valid argument without premises. Since stage numbers appearing in annotations on the left-hand side of a derivation correspond to horizontal lines lying above conclusions in the tree-form proof and ENV is the only form of argument so far without premises, it should be the only reason for a stage number to appear on the left but not the right.

You can use this idea as a way of checking for errors, and there are some further generalizations like this that you can use as checks. We will have no rules without conclusions, so every stage number should appear somewhere in the left-hand annotations. And, in a completed derivation whose gaps all close, all sentences other than assumptions (which, for now, are just the initial premises) will be conclusions and thus should have annotations on their left-hand side. Resources that are never used may appear with no annotations on their right; but, as you are constructing a derivation, it can be very useful to check for the absence of right-hand annotations because this can lead you to notice resources that you have not yet exploited. And, when we go on (in 2.3) to use derivations to show that claims of entailment fail, a check for the absence of right-hand annotations will be the key test of whether we done everything possible to complete a derivation.