Completeness I Metalogic
Our goal in this section is to prove that every sequent which is valid according to the defined semantics for classical logic also has a proof in the natural deduction calculus. For the present, we confine attention to propositional logic, leaving the technical care and feeding of quantifiers for later.
The first part of this proof is little more than an observation. Given any finite sequent with premises A1, ..., An and conclusion B, we can appeal to the deduction equivalence n times to find an equivalent single formula
A1 IMP (... IMP (An IMP B))
which is a theorem if and only if the original sequent is provable, and is a tautology iff the original sequent is valid. Now we already know from Chapter 2 that every propositional formula has an equivalent (i.e. with the same truth table) in conjunctive normal form (CNF). Let us call that CNF formula C. We also know that equivalent formulae can replace each other in any context, and we have the Diligent Reader's assurance that the equivalences required for every step of the reduction to CNF can all be proved by natural deduction. Hence we know there is a provable sequent
C TS A1 IMP (... IMP (An IMP B))
If C is a theorem, then
TS A1 IMP (... IMP (An IMP B))
and hence by n applications of IMPE:
A1, ..., An TS B
Hence, to show that the natural deduction system is complete for finite sequents, it suffices to show that every CNF tautology has a proof. But this is (almost) trivial. A CNF formula is a conjunction of clauses (disjunctions of literals). A conjunction is a tautology iff each of its conjuncts is a tautology, and by the rule ANDI, it is provable if each of its conjuncts is provable. A clause is tautologous iff it contains a pair of complementary literals such as p and NOTp, and any such clause is of the form (near enough, by the associativity and commutativity of disjunction) to something of the form (p OR NOTp) OR A, which is easily proved by appending a step of ORI to an proof of the law of the excluded middle.
While the low-level details of the proof that C entails A1 IMP (... IMP (An IMP B)) have not been exhibited explicitly, none of them are implausible and none present much difficulty, so with a small wave of the hands we declare this part of the proof done. However, the restriction to the finite case is a major limitation. Most valid sequents are infinite, so for the completeness theorem to be really interesting it must extend to sequents in which the premise set X contains infinitely many formulae.
What we need, therefore, is a demonstration that proving the finite sequents is enough. This is important enough to be designated a theorem in its own right.
Compactness Theorem: Every valid sequent has a valid finite sub-sequent. That is, if X STS A then there is a finite subset Y of X such that Y STS A.
The argument for compactness proceeds by definition of a semantic tree. The language of propositional logic is built up with connectives out of an infinite supply of atoms p1, p2, p3, etc. By an initial partial interpretation we mean an assignment of truth values 0 and 1 to the first n atoms p1, ..., pn, for some n. For example,
p1: 1, p2: 0, p3: 0, p4: 1,
is an initial partial interpretation for the case n = 4. It consists in assigning 1 (true) to the atoms p1 and p4, while assigning 0 (false) to p2 and p3. Notice that it says nothing about assignments to the rest of the atoms, so it can be extended as we please by making more assignments, and in fact is consistent with absolutely any assignment to the atoms with subscripts above 4,
|
: Nodes in the semantic tree Click for an animated version |
The initial partial interpretations, ordered by the relation of set inclusion, form a tree, starting with the empty assignment as its root, in which each node consisting of an assignment to p1, ..., pn. has exactly two successors reached by asasigning 0 and 1 respectively to pn+1. SemTree shows one node and its two successors. Let us refer to this entire semantic tree as 𝒯.
We say that a node of 𝒯 is "dead" if the assignment of values it represents either makes some formula in X false or makes A true. Otherwise it is "live". By the "fringe" of 𝒯 we mean the set of dead nodes with live parents. That is, a fringe node is a dead node which results from a live one by assigning a truth value to just one more atom.
The set of live nodes of 𝒯 is either finite or infinite. If it is finite, then the fringe is also finite, since no three fringe nodes can have the same parent, and there are only finitely many live parents to go around. Every fringe node either makes A true or else makes at least one formula in X false. Let Y be a set consisting of one such falsified formula for every fringe node which does not verify A. Obviously, Y is a finite subset of X, and it (semantically) entails A because the semantic tree shows that every possible way of assigning values to its atoms either falsifies one of its members or verifies A.
On the other hand, if there are infinitely many live nodes, then there is an infinitely long branch in 𝒯 consisting of live nodes. This must be the case, because the live nodes form a sub-tree of 𝒯 which branches at most two ways at every point, and by König's lemma an infinite tree with finite forks must contain an infinitely long branch. Consider any such infinite branch: a path through 𝒯 consisting of live nodes, starting at the root and going on forever. Each step along its length adds a truth value for the next atom, so the whole branch represents an assignment of truth values to all atoms in the language. This assignment makes every formula in X true and makes A false. Hence A is not a semantic consequence of X, and the result stands proved.
Originally published in 1927 (in German) Koenig, but it is essentially an easy observation which you can make for yourself.So classical propositional entailment is compact. The main theorem that the natural deduction proof system is complete follows easily: if X STS A then by compactness there is a finite subset Y of X such that Y STS A. Since this sequent is finite, it can be turned into a single formula, which is a tautology iff the sequent is valid. All tautologies are theorems, and the steps needed to get back from the tautology to the sequent can be made into a derivation, so there is a proof of Y TS A , which is also a proof of X TS A and natural deduction is complete.