Gödel's Second Incompleteness Theorem: Unprovability or Relative Provability? — Epoche C2
What the theorem forbids, stated exactly Peano arithmetic does not prove the arithmetical sentence that codes its own consistency, and this note is about what that fact does and does not license one to say. The popular gloss — that the consistency of arithmetic is unprovable — is a misreading, and correcting it is the essay's purpose. But the correction usually offered, that consistency is 'provable only in a stronger system', is itself inaccurate in a way that matters, and the sections below replace it with something exact. Fix notation first, since the argument depends on distinctions the informal statement erases. Let $\mathcal{T}$ be a theory in the language of arithmetic whose axiom set is recursively enumerable, which for present purposes means: there is a formula $\alpha(x)$ of the language such that the sentences satisfying $\alpha$ in the standard model are exactly the axioms. Fix a Gödel numbering and write $\ulcorner \varphi \urcorner$ for the numeral naming the code of $\varphi$. Write $\mathrm{Prf}_\alpha(x,y)$ for a formula expressing that $y$ codes a derivation, from axioms satisfying $\alpha$, of the formula coded by $x$, and put $\mathrm{Prov}_\alpha(x) := \exists y\, \mathrm{Prf}_\alpha(x,y)$, a $\Sigma_1$ formula. Consistency is then the sentence $$\mathrm{Con}_\alpha := \neg\,\mathrm{Prov}_\alpha(\ulcorner 0=1 \urcorner).$$ The theorem says: if $\mathcal{T}$ is consistent and $\mathrm{Prov}_\alpha$ satisfies the three conditions given below, then $\mathcal{T} \nvdash \mathrm{Con}_\alpha$. The subscript is not pedantry; it is the whole of the last third of this note. The three conditions are due to Hilbert and Bernays, who gave the first detailed published proof of the theorem in the second volume of Grundlagen der Mathematik (1939) — Gödel's 1931 paper states the second theorem as a corollary and defers its proof, which he never published. Writing $\mathrm{P}$ for $\mathrm{Prov}_\alpha$ they are: If $\mathcal{T} \vdash \varphi$ then $\mathcal{T} \vdash \mathrm{P}(\ulcorner \varphi \urcorner)$. A theorem's provability is itself provable. $\mathcal{T} \vdash \mathrm{P}(\ulcorner \varphi \to \psi \urcorner) \to (\mathrm{P}(\ulcorner \varphi \urcorner) \to \mathrm{P}(\ulcorner \psi \urcorner))$. Provability is closed under modus ponens, provably so. $\mathcal{T} \vdash \mathrm{P}(\ulcorner \varphi \urcorner) \to \mathrm{P}(\ulcorner \mathrm{P}(\ulcorner \varphi \urcorner) \urcorner)$. If something is provable, that fact is provably provable. The third is the demanding one. It is the internalisation of $\Sigma_1$-completeness — the fact that a true $\Sigma_1$ sentence is provable — and internalising it needs induction. Robinson's arithmetic $\mathrm{Q}$, which suffices for the first incompleteness theorem, does not deliver it; $\mathrm{I}\Delta_0 + \mathrm{EXP}$ does, and Peano arithmetic certainly does. So the theorem's reach downwards is limited by condition (3), not by anything in the diagonal construction. The proof idea, and where each condition is spent The argument is short enough to give, and giving it shows which parts of the machinery the later corrections touch. Everything rests on the diagonal lemma: for any formula $\psi(x)$ with one free variable there is a sentence $G$ with $\mathcal{T} \vdash G \leftrightarrow \psi(\ulcorner G \urcorner)$. Take $\psi(x)$ to be $\neg \mathrm{P}(x)$, giving a sentence that, provably in $\mathcal{T}$, holds if and only if it is unprovable: $$\mathcal{T} \vdash G \leftrightarrow \neg\,\mathrm{P}(\ulcorner G \urcorner).$$ First, half of the first incompleteness theorem. Suppose $\mathcal{T} \vdash G$. By condition (1), $\mathcal{T} \vdash \mathrm{P}(\ulcorner G \urcorner)$. But the fixed point gives $\mathcal{T} \vdash \neg\mathrm{P}(\ulcorner G \urcorner)$. So $\mathcal{T}$ is inconsistent. Contrapositively: if $\mathcal{T}$ is consistent then $\mathcal{T} \nvdash G$. Note that this half needs no assumption beyond consistency; the other half, that $\mathcal{T} \nvdash \neg G$, is what needed Gödel's $\omega$-consistency and was later weakened to plain consistency by Rosser's variant of the sentence. Second, the formalisation. The reasoning just given is elementary, and conditions (2) and (3) are exactly what is needed to run it inside $\mathcal{T}$. From the fixed point, $\mathcal{T} \vdash G \to \neg\mathrm{P}(\ulcorner G \urcorner)$; by (1) and (2), $\mathcal{T} \vdash \mathrm{P}(\ulcorner G\urcorner) \to \mathrm{P}(\ulcorner \neg \mathrm{P}(\ulcorner G \urcorner)\urcorner)$. By (3), $\mathcal{T} \vdash \mathrm{P}(\ulcorner G \urcorner) \to \mathrm{P}(\ulcorner \mathrm{P}(\ulcorner G \urcorner)\urcorner)$. A formula and its negation both provable yield anything provable, so combining these and using (2) again gives $\mathcal{T} \vdash \mathrm{P}(\ulcorner G \urcorner) \to \mathrm{P}(\ulcorner 0=1\urcorner)$. Contraposing, $\mathcal{T} \vdash \mathrm{Con}_\alpha \to \neg\mathrm{P}(\ulcorner G \urcorner)$, and by the fixed point again, $$\mathcal{T} \vdash \mathrm{Con}_\alpha \to G.$$ So if $\mathcal{T}$ proved its own consistency it would prove $G$, which the first step rules out for consistent $\mathcal{T}$. Hence $\mathcal{T} \nvdash \mathrm{Con}_\alpha$. Löb (1955) later showed that the whole phenomenon is an instance of something more general: if $\mathcal{T} \vdash \mathrm{P}(\ulcorner \varphi \urcorner) \to \varphi$ then $\mathcal{T} \vdash \varphi$. In words, a theory can only certify the truth of what it can prove of a sentence it already proves; there are no non-trivial reflection principles available internally. The second theorem is the case $\varphi := 0=1$, because in classical logic $\mathrm{Con}_\alpha$ just is $\mathrm{P}(\ulcorner 0=1\urcorner) \to 0=1$; if $\mathcal{T}$ proved it, Löb's theorem would give $\mathcal{T} \vdash 0=1$. Three relations that the word 'stronger' runs together The published version of this essay defined a system $\mathcal{S}$ to be stronger than $\mathcal{T}$ when $\mathcal{S}$ proves