Past exam of the mathematics course of the University of Cambridge / 2008 / iii / Paper 27 / 5

Here is the first incompleteness theorem in its modern consistency form: every consistent computably enumerable theory $T$ extending Robinson arithmetic is incomplete. The original Gödel sentence proof assumes omega-consistency to obtain both unprovabilities; we give that proof and the strengthening that removes this assumption. We also give the second incompleteness conclusion for theories extending Peano arithmetic.

First arithmetize syntax. Code strings and finite derivations by natural numbers. If the axioms of $T$ are merely computably enumerable, include the finite enumeration certificate for each nonlogical axiom used in a proof. The resulting proof-checking relation ${\mathrm{Prf}}_T(p,q)$ is primitive recursive. Finite strings and computation histories are coded by finite sequences, with bounded local verification of every step; these give arithmetic formulas representing the coding operations. In Robinson arithmetic every true or false instance with fixed numeral inputs is provable with the appropriate sign. Set

The diagonal lemma gives, for any formula $\theta (x)$, a sentence $D$ with $Q⊢D\leftrightarrow \theta (┌D┐)$. To see the construction, let $d(e)$ be the computable syntactic operation substituting the numeral for $e$ into the formula coded by $e$. Form the formula $\delta (x)=\theta (d(x))$, interpreting the displayed coding function through its arithmetic representation, and let $n=┌\delta ┐$. Then $D=\delta (\bar{n})$, and $d(n)=┌D┐$. The representation proves that fixed computation, giving the asserted equivalence.

Apply the diagonal lemma to $\neg {\mathrm{Prov}}_T(x)$, obtainingIf $T⊢G$, an actual finite proof has code $n$, so $Q$ proves its proof-checking instance and $T$ proves ${\mathrm{Prov}}_T(┌G┐)$. The fixed-point equivalence gives its negation, contradicting consistency. Hence $T⊬G$. For each standard numeral $n$, $Q$ proves $\neg {\mathrm{Prf}}_T(\bar{n},┌G┐)$ because there is no such proof. If $T⊢\neg G$, the equivalence gives $T⊢\exists p{\mathrm{Prf}}_T(p,┌G┐)$, contrary to omega-consistency. Thus the original proof gives two unprovabilities under that hypothesis. It also shows that $G$ is true in the standard natural numbers when $T$ is consistent.

For consistency alone use the Rosser sentenceIf $T⊢R$ with code $n$, consistency excludes every proof of $\neg R$. In particular the finitely many codes $q\le n$ all fail their primitive recursive proof tests. Robinson arithmetic verifies those finitely many failures and the actual proof at $n$, and hence proves $\neg R$, a contradiction. If $T⊢\neg R$ with code $m$, consistency excludes every proof of $R$. For $p<m$, Robinson arithmetic verifies all the finitely many failed proof tests. For $p\ge m$, it verifies that $q=m$ is a proof of $\neg R$ with $q\le p$. The elementary arithmetic dichotomy between $p<m$ and $m\le p$ therefore proves the entire displayed condition, hence $R$, again a contradiction. Thus

For the Gödel second incompleteness theorem, now assume $T\supseteq \mathsf{PA}$ and use its ordinary certified proof predicate. PA formalizes proof concatenation and the verification of a coded proof, giving the derivability conditions: if $T⊢A$ then $T⊢{\mathrm{Prov}}_T(┌A┐)$; and inside $T$,The first internal implication is certified by combining two proofs; the second is certified by producing the arithmetic proof that a given finite proof passes its check, with existential introduction. Apply them to $G\to \neg {\mathrm{Prov}}_T(┌G┐)$. From ${\mathrm{Prov}}_T(┌G┐)$, the two internal implications yield provability of both ${\mathrm{Prov}}_T(┌G┐)$ and its negation, and hence provability of $\perp$. ConsequentlyA proof of this consistency sentence in a consistent $T$ would prove $G$, which the first argument excludes. Therefore $\boxed{T⊬\mathrm{Con}(T)}$. This concerns the standard arithmetic consistency sentence and the stated effective, arithmetic hypotheses; it is not a prohibition on proving consistency in a stronger theory.

The constructible hierarchy is $L_0=\varnothing$, $L_{\alpha +1}=\mathrm{Def}(L_{\alpha })$ and $L_{\lambda }={\bigcup }_{\alpha <\lambda }{L}_{\alpha }$ at limits; $L={\bigcup }_{\alpha \in \mathrm{Ord}}{L}_{\alpha }$. Definability allows parameters from the current level. Satisfaction for a set-sized level is recursively definable, so this is a definable class construction in ZF. Induction shows its levels are sets, increasing and transitive, and contain every ordinal below their height.

We give the necessary reflection argument to check its full axiom schemes. For any finite collection $\Sigma$ of formulas, close it under subformulas and negation. Starting at any level containing the desired parameters, for every existential subformula and parameter tuple in that level for which a witness in $L$ exists, take the least constructibility stage containing such a witness. These least stages are uniquely definable ordinals; ambient replacement bounds all of them. Enlarge to a level beyond the bound, repeat countably many times, and take the union stage $\beta$. Every existential witness required by a tuple in $L_{\beta }$ is then already in $L_{\beta }$, because the tuple appeared at a previous stage. Induction on the finitely many formulas givesThis uses a truth definition for each fixed finite list, not a truth predicate for the entire ambient universe.

Extensionality and foundation hold in $L$ by transitivity. Pairs and unions of elements of a level are definable subsets of a sufficiently large transitive level. The hereditarily finite sets appear in $L_{\omega }$, and the set of its finite ordinals is definable there, so $\omega \in L$ and infinity holds. For separation on $a\in L$ with parameters in $L$, reflect the relevant formula into a level $L_{\beta }$ containing them and $a$. The desired subset of $a$ is then definable over $L_{\beta }$, so belongs to $L_{\beta +1}$.

For replacement, suppose $L$ says $\phi$ defines a unique value in $L$ for each $x\in a$. The relativization ${\phi }^L$ is an ambient formula. Ambient replacement collects its values, and replacement applied to their least constructibility stages bounds them all in some $L_{\gamma }$. Reflect the formula in a still larger level containing $a$, the parameters and those values. The range is now a definable subset of that level, so lies in $L$. For power set, the ambient set $\mathcal{P}(a)\cap L$ exists by separation. Its members' constructibility stages are bounded, say all members lie in $L_{\gamma }$ with $a\in L_{\gamma }$. Thenis definable over $L_{\gamma }$; transitivity makes the displayed bounded subset condition absolute. Thus this internal power set also belongs to $L$. We have proved $L\models \mathsf{ZF}$.

Finally define its canonical well-order recursively. At a successor stage, code a definition by its formula number and its finite tuple of parameters, ordered by the already constructed well-order of the previous level. Order new elements by their least definition codes, preserving earlier elements first. At a limit take the coherent union, with first-appearance stages providing the primary comparison. Induction makes every level well-ordered and gives a definable class well-order of $L$. Its restriction to any set in $L$ belongs to $L$ by separation, so every such set is internally well-orderable. HenceThe implication is a relative consistency argument, not a proof by ZF of its own consistency.

Now Shepherdson's wall explains the limitation of this method. If $W$ is a transitive inner model containing all ordinals, its constructible levels agree with the ambient ones. At successors both compute definable subsets of the same set-sized structure, with the same finite formulas and parameters; at limits both take the same union. Thus $L^W=L\subseteq W$. In an ambient universe satisfying $V=L$, this forces $W=V$. Therefore a uniform inner-model construction valid in every model of ZF cannot always yield an inner model with $V\ne L$, nor one failing choice or CH: apply the proposed construction in a model of ZF with $V=L$. The construction of $L$ removes nonconstructible sets and proves positive choice consistency; it cannot manufacture the nonconstructible sets needed for those negative results.