Completeness II Metalogic

This page gives an alternative proof that propositional natural deduction (that is, the natural deduction calculus without the rules for quantifiers) is complete for the propositional logic defined by the two-valued truth tables for the connectives. It is simpler that the standard proof, and may be easier to grasp on a first reading, and unlike the proof already given, it does not depend on a prior demonstration of compactness.

We begin by defining the notion of a literal basis for a formula A. This is a set of literals (that is, atoms such as p and negated atoms such as NOTq) containing, either negated or unnegated, every atom in A. For instance, the set {NOTp, q, r} is a literal basis for the formula (p AND q) IMP (p AND r) . The set {p, q, NOTr} is another literal basis for the same formula. We stipulate that each literal basis must be consistent: that is, no atom occurs both negated and unnegated in it.

One more piece of useful notation: where β is any literal basis, let I_β be the corresponding assignment of truth values to the atoms occurring (negated or unnegated) in β. That is, I_β(p) = 1 if p ∈ β, and I_β(p) = 0 if NOTp ∈ β (and similarly for every other atom). Note that I_β may be a partial interpretation, as it does not assign values to atoms outside the literal basis, but obviously it can be extended to a full interpretation if required and equally obviously the choice of such an extension cannot affect the value of any formula for which β is a literal basis.

Now, observe two facts, the first of which is important enough to be named for future reference.

Literal Basis Lemma:   If β is a literal basis for A then either β TS A or β TS NOTA.

This is proved by observing first that it is trivially true if A is an atom, and then that it extends up from the atoms to larger and larger subformulae of A and ultimately to A itself. As in the proof of the soundness theorem, we need to consider all the cases corresponding to the connectives.

Case 1: Negation

C B 0 1 1 0

Suppose some subformula B is NOTC, where of course C is a shorter subformula than B and β is a literal basis for it, so we may suppose the lemma holds of C. That is, either there is a natural deduction proof of   β TS C   or else there is one of   β TS NOTC.   In the latter case, there is nothing left to do, as a derivation of NOTC just is a derivation of B. In the former case, we must turn the derivation of C into a derivation of NOTNOTC (i.e. NOTB) which is hardly a challenge!

Case 2: Conjunction

C D B 0 0 0 0 1 0 1 0 0 1 1 1

This time we suppose that B is a subformula of A and is a conjunction C AND D.  C and D are both subformulae of A, so β is a literal basis for them, and they are shorter than B, so we are entitled to assume that the lemma holds of them. That is, there is a natural deduction proof either of   β TS C   or of   β TS NOTC,  and there is also a natural deduction proof of either   β TS D   or   β TS NOTD.  If there are derivations from β of both C and D, then these may be concatenated and extended by one step of ANDI to yield a derivation of B. If not, then there must be a derivation from β either of NOTC or of NOTD. In either case, NOTB may be derived by appending either a proof of   NOTC TS NOT(C AND D)   or a proof of   NOTD TS NOT(C AND D).

Case 3: Disjunction

C D B 0 0 0 0 1 1 1 0 1 1 1 1

Suppose that B is a subformula of A and is a disjunction of the form C OR D,  where as in the case of conjunction we are entitled to the assumption that there is a natural deduction proof either of   β TS C   or of   β TS NOTC,  and also of either   β TS D   or   β TS NOTD.  If there are derivations from β of both NOTC and NOTD, then we are in the top line of the table to the left, which is justified by the provability of the sequent   NOTC, NOTD TS NOT(C OR D).  Recall that this is proved by assuming C OR D and then applying ORE. Each of the assumed disjuncts contradicts one of the premises, so BAD results either way, so ORE and NOTI yield NOTB immediately. On the other hand, any derivation of C or of D may be extended in one step of ORI to yeild a derivation of B.

Case 4: Implication

C D B 0 0 1 0 1 1 1 0 0 1 1 1

Let B be a subformula of A and let it be of the form C IMP D where either there are natural deduction proofs of both   β TS C   and   β TS NOTD,   or else a proof of   β TS NOTC   or of   β TS D.   It is not hard to observe, then, that either     β TS B IMP C   or   β TS NOT(B IMP C)   in virtue of the provable sequents: NOTB   TS   B IMP C C   TS   B IMP C B, NOTC   TS   NOT(B IMP C)

The whole is the sum of the parts, since the property specified in the lemma is preserved by every operation with which A might have been constructed.

Observation:   Where β is any set of literals and A is any formula, if  β TS A , then A is true for I_β, while if  β TS NOTA , than A is false for I_β.

Obviously every literal in β is true for I_β. The observation follows directly from this and the soundness of the deductive system, together with the truth table for negation.

Now we want to show that every valid sequent is provable. In fact, we turn this around and show that every unprovable sequent is invalid. Suppose, then, that X is some set (possibly infinite) of formulae, and A is a formula such that that there is no derivation of A from X. We need to define an assignment of truth values to atoms for which everything in X is true but A is false.

Let the atoms of our propositional language be p₁, p₂, p₃, ..., etc. We build up the required interpretation incrementally by defining a sequence Y₀, Y₁, Y₂, ... of sets of literals, each one extending the previous one by adding the next atom or its negation:

Y₀ = ∅

If   X, Y_i, p_i+1 TS A   then  Y_i+1 = Y_i ∪ {NOTp_i+1}.  Otherwise  Y_i+1 = Y_i ∪ {p_i+1}

Now let Y be the union of all of these sets Y₀, Y₁, Y₂, etc. Clearly, by construction, any literal p_i or NOTp_i is in Y iff it is in Y_i, and iff it is in Y_j for every j ≥ i.

There is no n such that  X,Y_n TS A,  since if there were, there would have to be a first such n. Obviously, this can't be 0, since X ∪ Y₀ is just X, and by hypothesis there is no derivation of A from that. But it can't be any i+1 either, because this would require both X, Y_i, p_i+1 TS A   and  X, Y_i, NOTp_i+1 TS A   and hence X, Y_i TS A  , contradicting the assumption that Y_i+1 is the first set to yield A.

Let B be any formula in X. Although X may be infinite, and may contain every atom in the language, B is a particular (finite) formula, so its atoms are all among the first n for some finite n. That means that Y_n is a literal basis for B, so by the Literal Basis Lemma, either  Y_n TS B  or  Y_n TS NOTB . But we can't have  Y_n TS NOTB because that would make X ∪ Y_n inconsistent, which it isn't because it does not imply A. Therefore Y_n TS B and therefore  Y TS B. In a similar way, there are numbers m be such that the atoms in A are all among {p₁,...,p_m}. Since, as observed, A is not derivable from Y_m, it must be the case that  Y_m TS NOTA and so Y TS NOTA.

By the observation above, then, every formula in X is true for I_Y, while A is false for I_Y.  I_Y is therefore a truth value assaignment invalidating the sequent, finishing the proof of completeness.