Arithmetization and the Incompleteness Theorems

Derivation. Derives Proposition A5.1. Each is settled by a bounded search through the prime factorization of the argument, composed with the syntactic tests of Definition 7.80, which are finite string comparisons. Axiomhood is decidable precisely because \(T\) was assumed effectively axiomatized (Definition 7.81); this is the only hypothesis of the theorem that is not automatic, and it is where the assumption earns its place. Being a derivation is the conjunction of finitely many such tests, one per line of the coded sequence, each of which asks whether a line is an axiom or follows from earlier lines by one of the finitely many rules.

Derives Lemma A5.5. (1) Induction in the metatheory on \(n\). For \(n=0\) the axiom \(x+0=x\) gives \(\overline{m}+\overline{0}=\overline{m}\). If \(Q\vdash\overline{m}+\overline{n}=\overline{m+n}\), then the axiom \(x+Sy=S(x+y)\) gives \(\overline{m}+\overline{n+1}=S(\overline{m}+\overline{n}) =S\overline{m+n}=\overline{m+n+1}\). Multiplication is the same argument using \(x\cdot0=0\) and \(x\cdot Sy=x\cdot y+x\). Note what happened: for each fixed pair \((m,n)\) this is a finite chain of equalities, hence a genuine \(Q\)-derivation; the induction that generated the chain was ours, not \(Q\)'s.

(2) Suppose \(m\neq n\), say \(m<n\). Metatheoretic induction on \(m\). If \(m=0\) then \(\overline{n}\) is \(S\overline{n-1}\) and the axiom \(Sx\neq0\) applies directly. If \(m>0\), both numerals are successors, and the axiom \(Sx=Sy\rightarrow x=y\) contraposed reduces the claim for \((m,n)\) to the claim for \((m-1,n-1)\), which the induction hypothesis supplies.

(3) If \(m\leq n\), take \(z:=\overline{n-m}\); by (1), \(Q\vdash\overline{n-m}+\overline{m}=\overline{n}\), so \(Q\vdash\exists z\,(z+\overline{m}=\overline{n})\), which is \(\overline{m}\leq\overline{n}\) by Equation (A5.2). If \(m>n\), we must refute \(\exists z\,(z+\overline{m}=\overline{n})\). By (4), applied with \(\overline{n}\), any such \(z\) would satisfy \(z=\overline{j}\) for some \(j\leq n\); but then \(z+\overline{m}=\overline{j+m}\) by (1), and \(j+m\geq m>n\), so \(\overline{j+m}\neq\overline{n}\) by (2). As \(j\) ranges over finitely many values, this is a finite case analysis inside \(Q\).

(4) Metatheoretic induction on \(m\). For \(m=0\): suppose \(z\leq\overline{0}\), i.e. \(w+z=\overline{0}\) for some \(w\). If \(z\neq\overline{0}\) then Equation (A5.1) gives \(z=Sv\) for some \(v\), whence \(w+Sv=S(w+v)\) by the addition axiom, so \(\overline{0}\) is a successor, contradicting \(Sx\neq0\). Hence \(z=\overline{0}\). This is the step that fails without Equation (A5.1): nothing else in \(Q\) rules out an element that is neither \(0\) nor a successor.

For the step, assume Equation (A5.6) for \(m\) and suppose \(z\leq\overline{m+1}\), say \(w+z=\overline{m+1}=S\overline{m}\). If \(z=\overline{0}\) we are done. Otherwise \(z=Sv\) by Equation (A5.1), so \(S(w+v)=S\overline{m}\), and injectivity of \(S\) gives \(w+v=\overline{m}\), i.e. \(v\leq\overline{m}\). The induction hypothesis then yields \(v=\overline{j}\) for some \(j\leq m\), so \(z=Sv=\overline{j+1}\) with \(j+1\leq m+1\).

Derives Lemma A5.6. First the \(\Delta_{0}\) case, by induction in the metatheory on the structure of the formula. Atomic sentences are equations and inequations between closed terms; evaluating the terms and applying Lemma A5.5(1)–(3) settles them, and a true one is proved while a false one has its negation proved. The connectives are immediate: if the parts are decided, Lemma A4.4-style propositional reasoning decides the compound, using only the tautologies of Proposition 7.22.

For a bounded quantifier, let \(\forall z\leq\overline{m}\,\psi(z)\) be true. Then \(\psi(\overline{j})\) is true for every \(j\leq m\), and each is proved by the induction hypothesis; Equation (A5.6) converts the finitely many instances into the universally quantified statement, since any \(z\) below \(\overline{m}\) is provably one of the \(\overline{j}\). If instead \(\exists z\leq\overline{m}\,\psi(z)\) is true, some witness \(\overline{j}\) with \(j\leq m\) has \(\psi(\overline{j})\) true and provable, and Lemma A5.5(3) supplies \(\overline{j}\leq\overline{m}\).

Now the general case. Let \(\exists x_{1}\cdots\exists x_{k}\,\delta\) be true, and let \(n_{1},\ldots,n_{k}\) be witnesses. Then \(\delta(\overline{n_{1}},\ldots,\overline{n_{k}})\) is a true \(\Delta_{0}\) sentence, hence provable, and existential generalization gives the \(\Sigma_{1}\) sentence.

Derives Lemma A5.7. Put \(P:=m_{0}m_{1}\cdots m_{n}\) and \(P_{i}:=P/m_{i}\). Since the moduli are pairwise coprime, \(P_{i}\) is coprime to \(m_{i}\), so there is \(u_{i}\) with \(P_{i}u_{i}\equiv1\pmod{m_{i}}\). Set \(a:=\sum_{i}r_{i}P_{i}u_{i}\). Modulo \(m_{i}\) every term with \(j\neq i\) vanishes, because \(m_{i}\) divides \(P_{j}\), and the remaining term is \(r_{i}P_{i}u_{i}\equiv r_{i}\).

Derives Lemma A5.9. Let \(c:=\max\set{n,s_{0},\ldots,s_{n}}\) and put \(b:=c!\). Write \(m_{i}:=1+(i+1)b\) for \(i=0,\ldots,n\).

The moduli are pairwise coprime. Suppose a prime \(p\) divides both \(m_{i}\) and \(m_{j}\) with \(i<j\leq n\). Then \(p\) divides their difference,

so \(p\) divides \((j-i)\) or \(p\) divides \(b\). If \(p\) divided \(b\) then, since \(p\) also divides \(m_{i}=1+(i+1)b\), it would divide the difference \(m_{i}-(i+1)b=1\), which is impossible. Hence \(p\) divides \(j-i\). But \(0<j-i\leq n\leq c\), so \(j-i\) is one of the factors of \(c!=b\), giving \(p\mid b\) — the case just excluded. No such prime exists, so \(\gcd(m_{i},m_{j})=1\).

The residues fit. Each \(s_{i}\leq c\leq c!=b<1+(i+1)b=m_{i}\), so \(s_{i}\) is a legitimate remainder modulo \(m_{i}\).

Lemma A5.7 now supplies \(a\) with \(a\equiv s_{i}\pmod{m_{i}}\) for every \(i\leq n\), and since \(0\leq s_{i}<m_{i}\) that congruence says exactly \(\mathrm{rem}(a,m_{i})=s_{i}\), i.e. \(\beta(a,b,i)=s_{i}\).

Derives Lemma A5.10. Equation (A5.8) is the division algorithm written out: \(v\) is the remainder exactly when \(a=q\cdot m+v\) with \(v<m\). The quotient \(q\) is at most \(a\), so bounding its quantifier by \(a\) loses nothing, and every quantifier in Equation (A5.8) is therefore bounded. For uniqueness at numeral arguments: if \(v,v'\) both satisfied it with \(v<v'\), subtracting gives \((q-q')m=v'-v\) with \(0<v'-v<m\), impossible for a multiple of \(m\); and by Lemma A5.5 this finite arithmetic is carried out inside \(Q\) for each numeral instance.

Derives Theorem A5.11. Induction in the metatheory on the construction of the function.

Initial functions. The zero function is represented by \(y=\overline{0}\); the successor by \(y=Sx\); the projection \(\pi^{n}_{i}\) by \(y=x_{i}\). In each case Equation (A5.4) holds because the defining equation is provable for numerals by Lemma A5.5(1), and Equation (A5.5) because a wrong value is refuted by Lemma A5.5(2).

Composition. Let \(f(\vect{x})=h(g_{1}(\vect{x}),\ldots, g_{k}(\vect{x}))\) with \(h,g_{1},\ldots,g_{k}\) represented by \(\eta,\gamma_{1},\ldots,\gamma_{k}\). Take

At numeral arguments the \(z_{i}\) are provably the values of the \(g_{i}\), by the uniqueness clause of Definition A5.2, and \(\eta\) then pins \(y\); the negative clause follows likewise.

Primitive recursion. Let

with \(g,h\) represented by \(\gamma,\eta\). The obstruction is that \(f\)'s value at \(n\) depends on the whole computation \(f(\vect{x},0),\ldots, f(\vect{x},n)\), which is a sequence. Encode it with \(\beta\): say that \(y\) is the value if there is a pair \((a,b)\) coding a sequence whose \(0\)th entry is \(g(\vect{x})\), whose entries step according to \(h\), and whose \(n\)th entry is \(y\). Formally,

For numeral arguments \(\vect{m},n\) with true value \(p\), Lemma A5.9 supplies \(a,b\) coding the actual computation sequence, every conjunct of Equation (A5.10) is then a true \(\Delta_{0}\) or \(\Sigma_{1}\) statement about numerals, and Lemma A5.6 makes it provable — giving Equation (A5.4). For Equation (A5.5), if \(y=\overline{p'}\) with \(p'\neq p\), then \(B(a,b,\overline{n},y)\) together with the uniqueness of Lemma A5.10 and the induction hypothesis on \(\eta\) forces \(\overline{p'}=\overline{p}\), refuted by Lemma A5.5(2).

Proof of Theorem A5.3. Derives Theorem A5.3. A decidable relation has a computable indicator function (Definition 7.93), so it suffices to treat total computable functions.

By Kleene's normal form, every total computable \(f\) can be written \(f(\vect{x})=V\bigl(\mu z\,[\,C(\vect{x},z)=0\,]\bigr)\) with \(V\) and \(C\) primitive recursive, where \(\mu z\) denotes the least \(z\) making the bracket true — \(C\) tests whether \(z\) codes a halting computation of the machine for \(f\) on \(\vect{x}\), which by Proposition A5.1 is a primitive recursive test, and \(V\) reads the output off it. Since \(f\) is total, such a \(z\) exists for every \(\vect{x}\). Let \(\chi\) and \(\nu\) represent \(C\) and \(V\), which Theorem A5.11 provides, and set

At numeral arguments, let \(z_{0}\) be the true least witness. Then \(\chi(\vect{\overline{m}},\overline{z_{0}},\overline{0})\) is provable, each of the finitely many \(\neg\chi(\vect{\overline{m}},\overline{w}, \overline{0})\) with \(w<z_{0}\) is provable, and Equation (A5.6) assembles them into the bounded universal clause. So Equation (A5.4) holds. If \(y\) is given a wrong numeral value, the uniqueness clauses for \(\chi\) and \(\nu\) refute it, giving Equation (A5.5).

The \(\Sigma_{1}\)-completeness half of the theorem is Lemma A5.6. Every step used only the seven axioms of \(Q\); no induction inside the theory was required, because each claim was proved separately for each numeral by an induction carried out here rather than there.

Axiom 7.94 entered nowhere as a step. It is needed only to identify the informal notion of “computable procedure” with the formal one in the statement of the theorem; the proof itself concerns Turing machines and primitive recursion throughout.

Derives Theorem A5.12. By Proposition A5.1 the substitution function \(\mathrm{sub}\) is computable, so by Theorem A5.3 it is representable: there is a formula \(\mathrm{Sub}(x,y,z)\) such that for all \(m,n\),

Given \(\psi\), define the auxiliary formula in the single free variable \(x\)

let \(k:=\ulcorner\theta\urcorner\) be its own Gödel number, and put

The point of the construction is the arithmetical identity

which holds because substituting the numeral \(\overline{k}\) into the formula coded by \(k\) — namely \(\theta\) — produces exactly \(\sigma\).

Now instantiate Equation (A5.14) at \(m=n=k\) and use Equation (A5.17):

Substituting this equivalence into Equation (A5.16) gives

and the right-hand side is provably equivalent to \(\psi(\ulcorner\sigma\urcorner)\), since a universally quantified variable constrained to a single value may be replaced by that value. This is Equation (A5.13).

Derives Theorem A5.13. Let \(\mathrm{neg}(x)\) be the computable function taking the code of a formula to the code of its negation, represented as in Theorem A5.3. Apply Theorem A5.12 to

obtaining \(R\) with \(T\vdash R\leftrightarrow\psi(\ulcorner R\urcorner)\). In words, \(R\) says: for every proof of me there is a no-longer proof of my negation.

\(T\nvdash R\). Suppose \(T\vdash R\), with a derivation coded by \(m\). Then \(\mathrm{Proof}_{T}(\overline{m},\ulcorner R\urcorner)\) is true, hence provable by Equation (A5.4). Combining with \(R\) itself, \(T\) proves \(\exists z\leq\overline{m}\ \mathrm{Proof}_{T}(z,\ulcorner\neg R\urcorner)\). But \(T\) is consistent, so \(T\nvdash\neg R\), so for each \(j\leq m\) the statement \(\neg\mathrm{Proof}_{T}(\overline{j},\ulcorner\neg R\urcorner)\) is true and hence provable by Equation (A5.5). Since \(Q\) proves the bounded expansion \(\forall z\,(z\leq\overline{m}\rightarrow z=\overline{0}\vee\cdots\vee z=\overline{m})\), the theory proves the negation of the displayed existential. So \(T\) is inconsistent — contradiction.

\(T\nvdash\neg R\). Suppose \(T\vdash\neg R\), with derivation coded by \(m\); then \(T\vdash\mathrm{Proof}_{T}(\overline{m},\ulcorner\neg R\urcorner)\), and therefore

taking \(z=\overline{m}\) as the witness. On the other hand \(\neg R\) is provably equivalent to \(\exists y\,\bigl(\mathrm{Proof}_{T}(y,\ulcorner R\urcorner)\wedge \neg\exists z\leq y\,\mathrm{Proof}_{T}(z,\ulcorner\neg R\urcorner)\bigr)\), so with Equation (A5.19) and the provable trichotomy of \(\leq\), the theory proves \(\exists y<\overline{m}\ \mathrm{Proof}_{T}(y,\ulcorner R\urcorner)\). But consistency gives \(T\nvdash R\), so each \(\neg\mathrm{Proof}_{T}(\overline{j},\ulcorner R\urcorner)\) with \(j<m\) is true and provable, and the bounded expansion again refutes the existential. So \(T\) is inconsistent — contradiction.

Derivation. Derives Proposition A5.14. Equation (7.93) is \(\Sigma_{1}\)-completeness (Theorem A5.3): a derivation of \(\varphi\) is a concrete finite object, so \(\mathrm{Prov}_{T}(\ulcorner\varphi\urcorner)\) is a true \(\Sigma_{1}\) sentence and is therefore provable. Equation (7.94) formalizes the observation that two derivations, one of \(\varphi\rightarrow\chi\) and one of \(\varphi\), can be concatenated and extended by one application of modus ponens to give a derivation of \(\chi\); the concatenation is a computable operation on codes and PA proves that it does what it does, by induction on the length of the derivations. Equation (7.95) is Equation (7.93) formalized inside PA, and is the laborious one: it requires proving in PA the general \(\Sigma_{1}\)-completeness statement rather than using it instance by instance, which is done by induction on the structure of \(\Sigma_{1}\) formulas.

Derives Theorem A5.15. Let \(G\) be the Gödel sentence of Equation (7.89),

We derive Equation (7.92) from the conditions.

From Equation (A5.20), \(T\vdash G\rightarrow\neg\mathrm{Prov}_{T} (\ulcorner G\urcorner)\), equivalently \(T\vdash\mathrm{Prov}_{T}(\ulcorner G\urcorner)\rightarrow\neg G\). Applying Equation (7.93) to this theorem and then Equation (7.94),

By Equation (7.95),

and chaining Equation (A5.22) with Equation (A5.21),

A theory proving both a sentence and its negation proves everything, and this fact is itself formalizable, giving \(T\vdash\bigl(\mathrm{Prov}_{T}(\ulcorner G\urcorner)\wedge \mathrm{Prov}_{T}(\ulcorner\neg G\urcorner)\bigr)\rightarrow \mathrm{Prov}_{T}(\ulcorner 0=1\urcorner)\). With Equation (A5.23),

whose contrapositive, recalling \(\mathrm{Con}_{T}=\neg\mathrm{Prov}_{T}(\ulcorner 0=1\urcorner)\) from Equation (7.90), reads

Combining Equation (A5.25) with Equation (A5.20) gives \(T\vdash\mathrm{Con}_{T}\rightarrow G\), which is Equation (7.92).

Finally, suppose \(T\vdash\mathrm{Con}_{T}\). Modus ponens would yield \(T\vdash G\), contradicting the first half of Theorem 7.87, which requires only consistency. Hence \(T\nvdash\mathrm{Con}_{T}\).

Derives Theorem A5.16. The proof has two moves: reduce validity to provability in a finitely axiomatized theory, then reduce halting to that.

Validity to provability in \(Q\). Robinson arithmetic \(Q\) has finitely many axioms; let \(\chi\) be their conjunction, a single sentence. By the deduction theorem, for every sentence \(\varphi\),

the last step by Theorem 7.84. A decision procedure for validity would therefore decide provability in \(Q\). This is where finite axiomatizability is essential; the argument does not run for PA, whose induction schema is infinite.

Halting to provability in \(Q\). The halting set

is semi-decidable: simulate \(M\) on \(w\) with Theorem 7.95 and halt when it halts. Every semi-decidable set is definable by a \(\Sigma_{1}\) formula — the existential quantifier ranging over codes of terminating computations, whose verification is decidable by Proposition A5.1 — so fix \(\eta(x,y)\) of that form with

Then:

• If \((m,w)\in H\), the sentence \(\eta(\overline{m},\overline{w})\) is a true \(\Sigma_{1}\) sentence, so \(Q\vdash\eta(\overline{m},\overline{w})\) by \(\Sigma_{1}\)-completeness (Theorem A5.3).

• If \((m,w)\notin H\), the sentence is false in \(\N\). Since \(\N\) is a model of \(Q\), soundness (Theorem 7.84) gives \(Q\nvdash\eta(\overline{m},\overline{w})\).

Hence \(Q\vdash\eta(\overline{m},\overline{w})\) if and only if \(M\) halts on \(w\). A decision procedure for \(Q\)-provability would decide the halting problem, contradicting Theorem 7.96; by Equation (A5.26) a decision procedure for validity would supply one. Therefore no decision procedure for validity exists.