2.2.7. More rules

A couple of the principles for ⊤ and ⊥—in particular, with the laws for ⊤ as a conclusion and ⊥ as a premise—have a role to play in derivations. Like the laws for conjunction, these laws have associated patterns of valid argument:

The label for the second, EFQ, abbreviates the Latin ex falso quodlibet (which might be translated as from the false, whatever), a traditional way of stating the law for ⊥ as a premise, and the label for the first, ENV, abbreviates ex nihilo verum (from nothing, the true), which gives a corresponding statement of the law for ⊤ as a conclusion.

The two other laws for ⊤ and ⊥ do not have associated patterns of argument and will not be associated with steps in proofs. The law for ⊤ as a premise does not point to a pattern of argument whose conclusion could replace ⊤, for it tells us that ⊤ may simply be dropped from the premises. In fact, it will be just as easy to retain ⊤ as an active resource but ignore it. And that will make our handling of ⊤ more like our handling of ⊥. For we cannot apply the principle for ⊥ as an alternative unless we begin with multiple alternatives or end with none, so it is not a principle of entailment at all and provides no way of replacing ⊥ as a conclusion. This does not mean that ⊥ as a conclusion is insignificant in the way ⊤ is insignificant as a premise, but the role of ⊥ as conclusion is to mark an entailment as a claim of inconsistency, and such claims will be established by applying principles to their premises rather than to their conclusion. (However, we will eventually have some rules for exploiting resources that we will apply only when the goal is ⊥.)

The principles ENV and EFQ figure in derivations as rules for closing gaps. In the case of the first, it is enough for a gap to be closed 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.

The difference is 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.)

Here are examples of the use of these rules:

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 right-hand side of a derivation mark the use of a line as a premise and ENV is the only form of argument we have seen so far that has no premises, a use of the rule ENV should be the only reason for a stage number to appear on the left of a derivation but not on 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.