Gödel's Theorems: Beyond Unprovability to the Axiomatic Core — Epoche C2
What the second theorem says, and why it carries the weight Gödel's second incompleteness theorem states that a consistent formal system able to formalise elementary arithmetic cannot prove the arithmetical sentence that asserts its own consistency. That result, rather than the more quotable claim that some truths are unprovable, is what makes the 1931 paper a permanent constraint on foundational programmes (Gödel, 1931). The familiar gloss — that not all mathematical truths can be proved, or that mathematical truth is unknowable — is at best a shadow of the first theorem and at worst a misreading of it. The claim defended here is that the theorems locate the limit at a particular place, namely a system's inability to certify itself, and that the consequence is not scepticism about truth but a demand that the choice of axioms be treated as a substantive mathematical decision. Fix notation. Let $\mathcal{T}$ be a formal system: a set of axioms in the language of arithmetic together with the usual rules of first-order logic. Three properties of $\mathcal{T}$ will be assumed throughout, and each will be shown to be doing real work. It is consistent : no sentence and its negation are both derivable. It is recursively axiomatised : there is an algorithm that decides whether a given string is one of its axioms. And it interprets enough arithmetic : it proves the basic facts about addition and multiplication on the natural numbers that are needed to encode finite sequences — Robinson arithmetic, a finitely axiomatised fragment far weaker than Peano arithmetic, already suffices. Write $\mathcal{T} \vdash \varphi$ for "$\varphi$ is derivable in $\mathcal{T}$", and $\mathcal{T} \nvdash \varphi$ for its failure. The machinery: coding, representability, the fixed point Gödel's construction rests on turning statements about proofs into statements about numbers. Assign to each symbol, formula and finite sequence of formulas a distinct natural number by a fixed effective coding; write $\#\varphi$ for the numeral naming the code of $\varphi$. The relation "the number $p$ codes a derivation in $\mathcal{T}$ of the formula coded by $q$" is then a relation between numbers, and it is decidable — one need only check finitely many mechanical conditions on the sequence coded by $p$ — precisely because the axioms of $\mathcal{T}$ can be recognised algorithmically. Call the formula expressing it $\mathrm{Prf}(x, y)$, and abbreviate $\exists x\, \mathrm{Prf}(x, \#\varphi)$ as $\mathrm{Prov}(\#\varphi)$. Two facts about weak arithmetic make the coding usable. First, every computable function is representable: there is a formula that provably defines its graph, so the theory can perform the syntactic bookkeeping internally. Second, the theory is complete for existential arithmetical statements — if such a statement is true of the natural numbers, the theory proves it. Both hold already in Robinson arithmetic, which is why the hypothesis on $\mathcal{T}$ is so weak. From representability comes the fixed-point lemma, which supplies the self-reference without any circularity in the definitions. For any formula $\varphi(x)$ with one free variable there is a sentence $\sigma$ with $\mathcal{T} \vdash \sigma \leftrightarrow \varphi(\#\sigma)$. The construction is three lines. Let $\mathrm{sub}(x, y)$ represent the computable function that takes the code of a formula with one free variable together with a number, and returns the code of the result of substituting the numeral of that number for the variable. Put $\delta(x) := \varphi(\mathrm{sub}(x, x))$ and let $\sigma$ be $\delta(\#\delta)$. Then $\mathrm{sub}(\#\delta, \#\delta)$ is the code of $\delta(\#\delta)$, which is $\sigma$ itself, so $\sigma$ is provably equivalent to $\varphi(\#\sigma)$. Applying this with $\varphi(x) := \neg \mathrm{Prov}(x)$ yields the sentence $G$ satisfying $\mathcal{T} \vdash G \leftrightarrow \neg\mathrm{Prov}(\#G)$, which is the sentence loosely described as saying "I am not provable in $\mathcal{T}$". The two halves of the argument are not symmetric The earlier and shorter version of this essay set out the first theorem as a pair of questions with symmetrical answers. The questions are the right ones, but one of the answers was wrong, and the error is instructive rather than incidental. Question: if $G$ is provable in $\mathcal{T}$, what follows? Answer: suppose $\mathcal{T} \vdash G$. Then some number $p$ codes a derivation of $G$, so the statement $\mathrm{Prf}(p, \#G)$ is a true decidable statement about specific numbers, and $\mathcal{T}$ proves it. Hence $\mathcal{T} \vdash \mathrm{Prov}(\#G)$, and by the fixed-point equivalence $\mathcal{T} \vdash \neg G$. So $\mathcal{T}$ proves both $G$ and $\neg G$ and is inconsistent. Contrapositively, if $\mathcal{T}$ is consistent then $\mathcal{T} \nvdash G$. Question: if $G$ is not provable, does it follow that $\neg G$ is not provable either? Answer: not from consistency alone. This is where the symmetry breaks. The earlier version justified the first half by saying that a provable $G$ would have to be false, and that a consistent system cannot prove a false statement. That last clause is not true. Consistency is a syntactic property — the absence of a derivable contradiction — whereas being unable to prove falsehoods is soundness, a semantic property, and the two come apart. If Peano arithmetic is consistent, then the theory obtained by adding to it the sentence asserting its own inconsistency is also consistent, and that theory proves a sentence false in the standard model. The correct route to the first half is the one given above, which uses only the theory's ability to verify a concrete computation, and never appeals to truth. The second half genuinely needs more. Suppose $\mathcal{T} \vdash \neg G$, that is, $\mathcal{T} \vdash \mathrm{Prov}(\#G)$. From the first half, $\mathcal{T} \nvdash G$, so no number actually codes a derivation of $G$; each statement $\mathrm{Prf}(n, \#G)$ is