Unpacking Gödel's Deeper Incompleteness — Epoche C2
The sentence, and what is actually proved about it The formula Gödel constructs in his 1931 paper is a single sentence of first-order arithmetic which says, of the number coding itself, that no number codes a proof of it from the axioms; and the two theorems proved about that sentence are narrower in their hypotheses, and sharper in their conclusion, than the familiar slogan that sufficiently complex systems are undecidable. The compressed version of this essay was right to press that distinction and right about its direction. But it stated the first theorem in a form Gödel did not prove, and it attached to the second a phrase — that a system cannot prove "its own completeness" — that has no referent. Both need correcting before the deeper point can be made, and the corrections are the point, because the precision is where the content lies. Fix notation first. $F$ is a first-order theory in a language containing a constant $0$, the successor function $S$, addition and multiplication. $F \vdash A$ means $A$ is derivable from the axioms of $F$, and $F \nvdash A$ that it is not. For a formula or sentence $A$, the expression $\lceil A \rceil$ denotes the numeral naming its code number under a fixed arithmetisation. With that, the two results, stated with the hypotheses their proofs use: First incompleteness theorem (Gödel 1931, in the form due to Rosser 1936). If the set of axioms of $F$ is recursively enumerable, if $F$ interprets Robinson arithmetic, and if $F$ is consistent, then there is a closed formula $\rho$ with $$F \nvdash \rho \qquad \text{and} \qquad F \nvdash \neg \rho .$$ Second incompleteness theorem (Gödel 1931; proof completed in Hilbert and Bernays 1939). If in addition $F$ proves induction for formulas of the shape "there exists $y$ such that $\dots$" with a decidable matrix, and $\mathrm{Con}(F)$ is the sentence, built from the standard proof predicate for $F$, asserting that no number codes a derivation of $0 = 1$, then $F$ consistent implies $$F \nvdash \mathrm{Con}(F) .$$ Everything of interest is in the three hypotheses of the first and the extra hypothesis of the second. Taking them in turn shows why the "too complex, therefore undecidable" reading inverts the situation. Why the axioms must be recursively enumerable, and what that hypothesis is doing An axiom set is recursively enumerable when some algorithm lists its members, possibly without ever halting. This is not a technical convenience; it is the entire content of the theorem, and the compressed version passed over it in a subordinate clause. Consider what would happen without it. Complete, consistent extensions of arithmetic are not scarce. The set of all sentences true in the standard structure of the natural numbers is one: it is consistent, since it has a model, and it is complete, since for any sentence either it or its negation holds there. So the theorem cannot be saying that completeness is unobtainable. It is saying that no complete consistent theory of arithmetic can be presented by a mechanically checkable list. Read that way, the first theorem is at once a positive result: it tells us that arithmetical truth is not recursively enumerable, which is a statement about the complexity of a set of sentences and not about anyone's inability to think of enough axioms. The reason the hypothesis is indispensable inside the proof is that the whole construction turns on expressing, by an arithmetical formula, the condition "$y$ codes a derivation from the axioms of $F$". Checking a candidate derivation means checking that each line is an axiom or follows from earlier lines by a rule. The second half of that test is mechanical for any reasonable proof system. The first half is mechanical only if axiomhood is mechanically testable. When the axiom set is recursively enumerable, the proof relation is a primitive recursive relation of the two code numbers, and provability is the result of prefixing one unbounded existential quantifier to it. Drop the hypothesis and the provability predicate climbs the arithmetical hierarchy out of reach, and with it the diagonal argument. How weak the arithmetic may be: Robinson's seven axioms The second hypothesis fixes the lower threshold, and it is startlingly low. Robinson arithmetic, written $Q$, is the finitely axiomatised theory given by Tarski, Mostowski and Robinson in 1953 with seven axioms and no induction whatever: $Sx \neq 0$ $Sx = Sy \rightarrow x = y$ $x \neq 0 \rightarrow \exists y\, (x = Sy)$ $x + 0 = x$ $x + Sy = S(x + y)$ $x \cdot 0 = 0$ $x \cdot Sy = (x \cdot y) + x$ The count is seven and not eight because the ordering relation, which some presentations axiomatise separately, is here defined rather than postulated. $Q$ is a miserable theory: it does not prove that addition is commutative, nor that every number is comparable with every other. It is nevertheless enough, and the reason is a single property. Every total recursive function is representable in $Q$: for each such $f$ there is a formula $\varphi(x, y)$ such that whenever $f(m) = n$, $Q$ proves $\varphi(\bar{m}, \bar{n})$ and proves that $\bar{n}$ is the unique such value. Representability, not strength, is what the first theorem consumes, and $Q$ already supplies it. This is what makes the threshold precise rather than vague. A theory escapes the first theorem not by being simple in some impressionistic sense but by failing to represent the recursive functions. Presburger showed in 1929 that first-order arithmetic with addition alone is complete and decidable; it escapes because without multiplication one cannot code finite sequences, and without sequence coding one cannot arithmetise derivations, which are sequences. The sequence-coding step deserves its own sentence, because it is where the language's poverty is overcome. Derivations are finite sequences of formulas, so coding them requires a way of packing arbitrarily long sequences into single numbers using only $+$ and $\cdot$ — exponentiation is n