Completeness III Metalogic

The previous sections of this chapter have established that the natural deduction calculus is sound and complete for propositional logic as defined by the standard truth table semantics. In this section, we prove completeness yet again. The technique is fundamentally similar to those already seen, in that it consists in building an interpretation incrementally by adding truth value assignments to the atoms one by one, but here we do not appeal to prior results such as the Compactness Theorem or of the Literal Basis Lemma. What we do use is a specialised technique for handling formulae in conjunctive normal form, so naturally we rely on the Diligent Reader to assure us once more that this sacrifices no generality.

Recall that the completeness problem is to show that every valid sequent is provable. As a first step, we simplify by restricting this to the special case in which the conclusion of the sequent is the absurd constant BAD. This restriction is more apparent than real, because any sequent  X TS A  is provable if the corresponding  X, NOTA TS BAD  is provable: SP {} PL {1} {1} {NOT A} {A} PL {X,1} {2} {BAD} {somehow (assumed provable)} PL {X} {3} {NOTNOTA} {2 [1] NOTI} PL {X} {4} {A} {3 NOTNOTE} EP

So we may safely take the completeness theorem to state that whenever a set of formulae is unsatisfiable, there is a derivation of BAD from it. We may also suppose that every formula in the set is in CNF, since that does not change satisfiability, and nor does it change what is derivable. Further, since a formula in CNF is nothing but a conjunction of clauses, and a conjunction implies exactly what is implied by its conjuncts, we may restrict attention to the case in which the premises of our sequent are all clauses and the conclusion is BAD.

A clause, as previously defined, is a disjunction of one or more literals. Since we do not care about the order in which the disjuncts occur, nor about how many times each disjunct is repeated, we may abstract from the syntax of disjunction and think of each clause simply as a set of literals. Of course, we must be careful to remember that we are thinking of the set of literals intuitively as a disjunction, and of a set of clauses intuitively as a conjunction, but no confusion should arise.

The special inference rule of resolution may be stated very simply in these terms. Where C ∪ {p} is a clause (i.e. a set of literals, one of which is the atom p), and D ∪ {NOTp} is a clause containing NOTp, we may resolve the clash by deducing the union C ∪ D. This is one step of resolution, and C ∪ D is called the resolvent.

The corresponding inference can be carried out in natural deduction. Resolution with quantifiers and function symbols thrown in was already noted as one of the examples of first order reasoning, but for the sake of clarity, here it is again in pure propositional logic:

Completeness is thus proved if resolution can be shown to be complete for the derivation of BAD from sets of clauses. Where clauses are seen as sets of literals, it is convenient to represent BAD as the empty clause (i.e. the empty set ∅), so let that convention be followed here.

As usual in completeness proofs, we suppose that the empty clause is not a resolution consequence of X, and show that there exists an assignment of truth values to atoms satisfying X. Again as usual, we define the relevant assignment as the union of a sequence of partial assignments built up incrementally, atom by atom. The structure of the proof is fundamentally the same as previously, but without the need to show the Literal Basis Lemma in generality because only a trivial case of it will be used.

Where X is a set (possibly infinite) of clauses from which there is no resolution derivation of the empty clause, we define an infinte sequence of sets of clauses Y₀, Y₁, Y₂, etc as follows:

Y₀ = ∅

If there is a resolution derivation of BAD from X ∪ Y_i ∪ {{p_i+1}} then Y_i+1 = Y_i ∪ {{NOTp_i+1}}.

Otherwise Y_i+1 = Y_i ∪ {{p_i+1}}.

Now each of the sets Y_i is consistent with X, meaning that there is no derivation of the empty clause from X ∪ Y_i by means of resolution. If there were such a derivation, there would have to be a first set in the series inconsistent with X. This cannot be Y₀, as that is empty. But it cannot be any Y_i+1 either, as we now show.

If there is a derivation of the empty clause from X ∪ Y_i+1, then by the construction Y_i+1 is Y_i ∪ {{NOTp_i+1}}, and there is also such a derivation from X ∪ Y_i ∪ {{p_i+1}}. In the latter derivation, the unit (single-literal) clause {p_i+1} can only be used to remove NOTp_i+1 from other clauses, converting something of the form C ∪ {NOTp_i+1} into C. If all such moves are simply omitted from the derivation, the result is still a resolution derivation, and is essentially the same except that the extra literal NOTp_i+1 persists instead of being resolved away. The effect is that this is now a derivation of the unit clause {NOTp_i+1} rather than of the empty clause, and since {p_i+1} is no longer used, it is a derivation of {NOTp_i+1} from X ∪ Y_i. Similarly, there is a derivation of {p_i+1} from X ∪ Y_i. But resolving these two unit clauses together produces the empty clause from X ∪ Y_i after all, contradicting the assumption that Y_i+1 is the first of the sets inconsistent with X.

Finally, consider the assignment of value 1 (true) to every p_i if {p_i} is in Y_i, and 0 (false) if {NOTp_i} is in Y_i. This assignment of truth values makes every clause in X true, since if it did not, then there would be a clause all of whose literals were false, and clearly resolving them all away with the complementary literals from the appropriate Y_n would lead to the empty clause.

Once again, the incrementally constructed assignment does the job, and the completeness theorem stands proved.