A Clarification on Consistency and Provability — Epoche C2
The claim being corrected The claim to be corrected is this: that Gödel's 1931 results show the consistency of a formal system to be unprovable, and that "true" and "provable" have been shown to be so far apart that consistency proofs are in general impossible. Neither half is what was proved. What was proved is a pair of theorems with four hypotheses that the popular statement drops, and each dropped hypothesis is exactly where the interesting content sits: that the theory be effectively axiomatised; that it be strong enough to represent the computable relations; that the two halves of the first theorem require different assumptions, consistency for one and something strictly stronger for the other; and that "the system proves its own consistency" is not a well-defined predicate of a system until one fixes how the system's axioms are described to it. Restoring these turns the theorems from a barrier into a piece of bookkeeping. They say what a consistency proof must cost and where the cost has to be paid. They do not say the bill cannot be met. What Hilbert asked for, and what would have counted as an answer The second of the problems Hilbert set out in 1900 asks for a proof that the axioms of arithmetic are consistent — that no finite chain of inferences from them ends in a contradiction. In 1900 this was a request without a method; the method came in the 1920s with proof theory, and with it the further demand that the proof be finitary : that it reason only about concrete finite configurations of symbols, using no completed infinite totality and no unrestricted quantification over infinite domains. The demand was not obviously extravagant, and it is worth seeing why. The statement "no proof of a contradiction exists" is, once proofs are coded as numbers, a sentence of the form "for every number, that number does not code a proof of $0 = 1$" — a universally quantified statement whose matrix is decidable by a finite computation. Sentences of that shape are the least infinitary statements there are. If any infinitary-looking claim could be settled by finite means, this was the candidate. The first theorem, with its hypotheses restored Let $\mathcal{F}$ be a theory in a language containing arithmetic. Two hypotheses are needed before anything can be said. The first is that $\mathcal{F}$ is effectively axiomatised : there is an algorithm that decides which sentences are axioms. This is the hypothesis whose omission makes the popular statement false rather than imprecise. The set of all sentences true in the standard model of arithmetic is consistent, is complete, contains all of elementary arithmetic, and proves its own consistency. Everything supposedly forbidden is realised by it. The one thing it is not is effectively axiomatised, and that is the whole of what incompleteness turns on: the theorem is a theorem about theories one could in principle implement. The second is strength. $\mathcal{F}$ must represent every computable relation — that is, for each such relation there must be a formula that $\mathcal{F}$ proves to hold of exactly the tuples of numerals standing in it. Robinson arithmetic $Q$, which is finitely axiomatised and has no induction at all, already suffices. So "sufficiently strong to formalise elementary arithmetic" means, precisely, "interprets $Q$", and the first theorem needs nothing beyond that. With those in place, code formulas and derivations as numbers, and write $\lceil A \rceil$ for the numeral naming the code of $A$. Because axiomhood is decidable and proof-checking is mechanical, the relation "$m$ codes a derivation in $\mathcal{F}$ of the formula coded by $n$" is primitive recursive, hence representable; call its representing formula $\mathrm{Proof}_{\mathcal{F}}(x, y)$, and set $\mathrm{Prov}_{\mathcal{F}}(y) := \exists x\, \mathrm{Proof}_{\mathcal{F}}(x, y)$. The diagonal lemma — for any formula $\varphi(x)$ there is a sentence $D$ with $\mathcal{F} \vdash D \leftrightarrow \varphi(\lceil D \rceil)$ — applied to $\neg\mathrm{Prov}_{\mathcal{F}}$ yields a sentence $G$ with $$\mathcal{F} \vdash G \leftrightarrow \neg\mathrm{Prov}_{\mathcal{F}}(\lceil G \rceil).$$ The first half of the theorem is short. Suppose $\mathcal{F} \vdash G$. Then some number $m$ codes a derivation of $G$, so $\mathrm{Proof}_{\mathcal{F}}(\overline{m}, \lceil G \rceil)$ is a true sentence with only bounded quantifiers, and $Q$ proves every such sentence; hence $\mathcal{F} \vdash \mathrm{Prov}_{\mathcal{F}}(\lceil G \rceil)$, hence $\mathcal{F} \vdash \neg G$ by the fixed point, and $\mathcal{F}$ is inconsistent. Contrapositively: if $\mathcal{F}$ is consistent then $\mathcal{F} \not\vdash G$. The truth of $G$ then follows immediately and without any mysterious appeal to a Platonic realm. $G$ says that no number codes a derivation of $G$. If $\mathcal{F}$ is consistent, no number does. So $G$ is true in the standard model. The only semantic assumption in play is that the arithmetisation is correct — that the numbers coding derivations really are the derivations. Gödel's 1931 paper avoids semantic vocabulary entirely, and the argument above shows why he could afford to. Where consistency is not enough The second half is where the popular statement, and the compressed statement often repeated in commentary, goes wrong. It is frequently written that if $\mathcal{F}$ is consistent then $\mathcal{F} \not\vdash G$ and $\mathcal{F} \not\vdash \neg G$. For Gödel's own $G$ that is not what was proved, and it does not follow from consistency alone. What Gödel used is $\omega$-consistency: $\mathcal{F}$ is $\omega$-consistent if there is no formula $\theta(x)$ such that $\mathcal{F} \vdash \exists x\, \theta(x)$ while $\mathcal{F} \vdash \neg\theta(\overline{n})$ for every natural number $n$. The reason this is exactly the right hypothesis can be read off the argument. Suppose $\mathcal{F} \vdash \neg G$, that is, $\mathcal{F} \vdash \exists x\, \mathrm{Proof}_{\mathcal{F}}(x, \lceil G \rceil)