Counting assumptions Propositional natural deduction


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

: Proof involving a theorem


to represent the claim that A is a theorem. As a special case of the deduction equivalence, an implication A IMP B is a theorem iff AB (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).


Recall that since  ⊢  is a consequence relation, one of its properties is monotonicity: if XA then X,YA for any set Y whatsoever. In particular X,BA where B is any formula, however irrelevant to the derivation of A from X. By the deduction equivalence, therefore, if XA then XB IMP A. The simplest result of this fact is the validity of the sequent pq 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.


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,AB then X,AB, 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:

[p AND (p IMP q)]1 ANDE [p AND (p IMP q)]1 ANDE
p p IMP q IMPE
q IMPI(1)
(p AND (p IMP q)) IMP q

Our 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.