Counting assumptions Propositional natural deduction
Before we pass to more complicated topics, it is worthwhile to pause and take note of some features of logic as presented in the last section. In particular, it is important to understand some of the boundary conditions or consequences of exploiting the limits of the specification of what counts as a proof. We begin, for example, by considering the case in which the set of premises of a sequent is empty.
Theorems
An application of IMPI allows one of the assumptions to be discharged. Now what happens if we carry on applying the rule and discharging when there is only one assumption left? Naturally enough, what happens is that the assumption side of the resulting sequent is empty. Consider what it means for the premise set to be empty. The sequent must correspond to an argument form with no premises. On our working definition of validity, a valid sequent without premises is one whose conclusion is necessarily true, so it holds no matter what, without needing the support of any assumption. That is, the conclusion is of a form which can be proved without any special assumptions at all: it holds just in virtue of pure logic. Such a formula is called a theorem. We write
SP {((p AND q) IMP p) IMP r ⊢ r} PL {1} {1} {((p AND q) IMP p) IMP r} {A} PL {2} {2} {p AND q} {A} PL {2} {3} {p} {2 ANDE} PL {} {4} {(p AND q) IMP p} {3 [2] IMPI} PL {1} {4} {r} {1, 4 IMPE} EP⊢ A
as an abbreviation of
∅ ⊢ A
to represent the claim that A is a theorem. Not all theorems are implications, but many important ones are. As a special case of the deduction equivalence, an implication A IMP B is a theorem iff A ⊢ B (that is, iff the sequent A : B is provable). Hence whenever a conclusion is deducible from premises there is a logical theorem attesting to the fact.
Theorems can be used in the proof of sequents with nonempty premise sides. thmProof shows an example. The theorem
⊢ (p AND q) IMP p
is proved at line (4) and then used as input to a further inference at line (5).
Weakening
Recall that since ⊢ is a consequence relation, one of its properties is monotonicity: if X ⊢ A then X,Y ⊢ A for any set Y whatsoever. In particular X,B ⊢ A where B is any formula, however irrelevant to the derivation of A from X. By the deduction equivalence, therefore, if X ⊢ A then X ⊢ B IMP A. The simplest result of this fact is the validity of the sequent p ⊢ q IMP p, but how is this to be proved in our formulations of natural deduction? Presumably by assuming p and then applying IMPI, discharging the assumption of q—but wait: there is no assumption of q! There are several ways around this awkwardness, but in natural deduction systems the easiest is to make discharge optional. That is, in deriving A IMP B from B by IMPI, assumptions of A (if there are any) may be discharged, but they do not have to be. We shall read rules such as IMPI in this way, regardless of whether we are writing proofs sequentially or drawing them as trees.
Where a rule such as IMPI is applied without discharging an assumption, we refer to the discharge as "vacuous". As notation, we write the square brackets with nothing between them. See proof 7 in the Appendix to this section and the exercises at the end of the chapter for examples of vacuous discharge.
It is not easy to find simple examples of the argument from p to q IMP p in natural settings, since in general anyone who is in a position to assert p has no reason to make it conditional on q. We do not usually argue from "He has black hair" to "If it's Saturday, he has black hair". We might make such an argument look more plausibly valid by putting in words like "even" and "anyway":
| Example 6 |
He has black hair [anyway]; Therefore, [even] if it's Saturday, he [still] has black hair. |
Contraction
There is an converse question, which is even more subtle. What if the derivation of B appealed to several assumptions of A, or used one assumption several times? Are we allowed to discharge all assumptions of A in one hit, or must we discharge them one by one? Since assumptions come in sets, and the set {A,A} is the same thing as the set {A}, the answer had better be that multiple occurrences of the same formula can be discharged together: if X,A,A ⊢ B then X,A ⊢ B, because X,A,A just is X,A. This feature, known as contraction or sometimes as absorption is actually a deep logical principle which we shall consider further in a later episode of these notes. For now, note that it is needed in order to prove the validity of such sequents as ⊢ ((p IMP q) AND p) IMP q:
SP {(p AND (p IMP q)) IMP q}{IMPI(1)} SP {q}{IMPE} SP {p}{ANDE} SP {[p AND (p IMP q)]1}{A} EP EP SP {p IMP q}{ANDE} SP {[p AND (p IMP q)]1}{A} EP EP EP EPOur reading of discharge will be maximally permissive: any application of a rule which has discharge of a formula A as a side-effect may discharge any number, zero or more, of assumptions of A, as we wish. In particular, if the number of assumptions discharged is zero, A need not occur as an assumption at all. This liberal reading is needed in order to secure key properties of standard, "classical" logic.
Exchange
SP {p IMP (q IMP r) ⊢ q IMP (p IMP r)} PL {1} {1} {p IMP (q IMP r)} {A} PL {2} {2} {p} {A} PL {3} {3} {q} {A} PL {1,2} {4} {q IMP r} {1, 3 IMPE} PL {1,2,3} {5} {r} {2, 4 IMPE} PL {1,3,2} {6} {r} {5 exchange} PL {1,3} {7} {p IMP r} {6 [2] IMPI} PL {1} {8} {q IMP (p IMP r)} {7 [3] IMPI} EPYet another "hidden" property of derivations is the fact that the order of assumptions makes no difference to what follows from them. This is clear enough on our working definition of what constitutes a sequent: the premises are taken to be a set of formulae, and the set X,Y is the same thing as the set Y,X so of course we may take assumptions in any order we wish. This is the fundamental principle of "exchange". However, we should be aware that this principle, that assumptions may be arbitrarily re-ordered, is a non-trivial feature of logic which we might at some point want to question. If we re-defined a sequent to consist of a list of premises and a conclusion, instead if a set of premises and a conclusion, then the correctness of the exchange principle would not be at all obvious. The list consisting of X followed by Y is not the same thing as Y followed by X, and we should not suppose that they have the same logical consequences without some sort of explicit stipulation to that effect. Exchange is required for such proofs as that in exchProof, where the order of assumptions on the left of the lines has been made explicit and strictly observed. For the purposes of stndard logic, again we read discharge in a permissive way, to allow the step directly from line 5 to line 7.