PROBLEMS

unformalized mathematics of a proof of a theorem from a set of axioms. For in later chapters we are going to be establishing results about the scope and limits of formal deducibility whose interest largely depends on their having something to do with proof in a more ordinary sense (just as results about the scope and limits of computability in one or another formal sense discussed in other chapters depend for their interest on their having something to do with computation in a more ordinary sense).

We have already mentioned towards the end of Chapter 10 that theorems and axioms in ordinary mathematics can virtually always be expressed as sentences of a formal first-order language. Suppose they are so expressed. Then if there is a deduction in the logician’s formal sense of the theorem from the axioms, there will be a proof in the mathematician’s ordinary sense, because, as indicated earlier, each formal rule of inference in the definition of deduction corresponds to some ordinary mode of argument as used in mathematics and elsewhere. It is the converse assertion, that if there is a proof in the ordinary sense, then there will be a deduction in our very restrictive format, that may well seem more problematic. This converse assertion is sometimes called Hilbert’s thesis.

As the notion of ‘proof in the ordinary sense’ is an intuitive, not a rigorously defined one, there cannot be a rigorous proof of Hilbert’s thesis. Before the completeness theorem was discovered, a good deal of evidence of two kinds had already been obtained for the thesis. On the one hand, logicians produced vast compendia of formalizations of ordinary proofs. On the other hand, various independently proposed systems of formal deducibility, each intended to capture formally the ordinary notion of provability, had been proved equivalent to each other by directly showing how to convert formal deductions in one format into formal deductions in another format; and such equivalence of proposals originally advanced independently of each other, while it does not amount to a rigorous proof that either has succeeded in capturing the ordinary notion of provability, is surely important evidence in favor of both.

The completeness theorem, however, makes possible a much more decisive argument in favor of Hilbert’s thesis. The argument runs as follows. Suppose there is a proof in the ordinary mathematical sense of some theorem from some axioms. As part-time orthodox mathematicians ourselves, we presume ordinary mathematical methods of proof are sound, and if so, then the existence of an ordinary mathematical proof means that the theorem really is a consequence of the axioms. But if the theorem is a consequence of the axioms, then the completeness theorem tells us that, in agreement with Hilbert’s thesis, there will be a formal deduction of the theorem from the axioms. And when in later chapters we show that there can be no formal deduction in certain circumstances, it will follow that there can be no ordinary proof, either.

Problems

14.1Show that:

(a)secures if and only if is unsatisfiable.

(b)secures if and only if some finite subset of secures some finite subset of .

14.2Explain why the problems following this one become more or less trivial if one is allowed to appeal to the soundness and completeness theorems.

Unless otherwise specified, ‘derivable’ is to mean ‘derivable using (R0)– (R8)’. All proofs should be constructive, not appealing to the soundness and completeness theorems.

14.3Show that if , A, B is derivable, then , A & B is derivable.

14.4Show that if A, and B, are derivable, then A & B, is derivable.

14.5Show that if A(c), is derivable, then x A(x), is derivable, provided c does not appear in , , or A(x).

14.6Show that if , A(t) is derivable, then , x A(x) is derivable.

14.7Show that x F x & xGx is deducible from x(Fx & Gx).

14.8Show that x (Fx & Gx) is deducible from xFx & xGx.

14.9Show that the transitivity of identity, x y z(x = y & y = z → x = z) is demonstrable.

14.10 Show that if , A(s) is derivable, then , s = t, A(t) is derivable.

14.11Prove the following (left) inversion lemma for disjunction: if there is a derivation of {(A B)} using rules (R0)–(R8), then there is such a derivation of { A, B} .

14.12Prove the following (right) inversion lemma for disjunction: if there is a derivation of {(A B)} , then there is a derivation of { A} , and there is a derivation of {B} .

14.13Consider adding one or the other of the following rules to (R0)–(R8):

Show that a sequent is derivable on adding (R11) if and only if it is derivable on adding (R12).