Gödel's Theorems and the Formal Limits of Provability — Epoche C2
The theorem, with the hypotheses it actually has Gödel's first incompleteness theorem is a statement about a class of formal systems, and the class is defined by three conditions, not two. A system $F$ falls under the theorem if it is consistent, if it is effectively axiomatised — that is, if there is an algorithm that decides which strings are axioms, or at least one that enumerates them — and if it is strong enough to represent every computable function, for which it suffices that $F$ interprets Robinson arithmetic $Q$, the finitely axiomatised fragment of Peano arithmetic $PA$ with no induction. An earlier version of this essay stated only the first and third conditions. The omission is not a technicality: the second condition is what the theorem is about, and dropping it makes the theorem false. The counterexample is immediate. Let $\mathrm{Th}(\mathbb{N})$ be the set of all sentences of the language of arithmetic true in the standard model. It is consistent, it contains $Q$, and it is complete by construction: for every sentence $\varphi$ it contains $\varphi$ or $\neg\varphi$. If the theorem needed only consistency and arithmetical strength, it would apply to $\mathrm{Th}(\mathbb{N})$ and produce a sentence undecided by it, which is absurd. What excludes $\mathrm{Th}(\mathbb{N})$ is that no algorithm enumerates it. Incompleteness is thus not a limit on what is true, nor even a limit on what a set of axioms can capture; it is a limit on what a set of axioms that one can recognise can capture. The whole misconception the earlier version of this essay set out to dispel — that Gödel showed some mathematical truths to be unknowable in an absolute sense — dissolves once this hypothesis is put back in. There are two theorems and both are needed below, so both should be on the table before the argument starts. The first, just characterised, produces for each such $F$ a sentence that $F$ does not settle. The second says that no such $F$ certifies itself: writing $\mathrm{Con}(F)$ for the arithmetical sentence saying that no number codes an $F$-derivation of a contradiction, a consistent $F$ of the relevant kind does not prove $\mathrm{Con}(F)$. The second is obtained by formalising the proof of the first inside $F$, which is why it carries extra hypotheses, and the sections below take them in that order. How the sentence is built The construction has three components, and each corresponds to one of the hypotheses. The first is arithmetisation. Every symbol, formula and finite sequence of formulas of $F$ is assigned a distinct natural number, its code; the code of $\varphi$ is written $\lceil \varphi \rceil$. Under this assignment, syntactic relations become arithmetical relations. In particular, let $\mathrm{Prf}_F(x,y)$ hold when $x$ codes a derivation in $F$ of the formula coded by $y$. Checking whether a given finite sequence is a derivation requires checking, at each line, whether it is an axiom or follows from earlier lines by a rule — and that check is decidable precisely because the axiom set is decidable. This is where effectiveness enters, and it is the only place it needs to. The second is representability. Since $\mathrm{Prf}_F$ is a decidable relation, and $Q$ represents all such relations, there is a formula of the language of arithmetic — write it $\mathrm{Prf}_F(x,y)$ as well — such that for each pair of numbers, $F$ proves the formula of the corresponding numerals if the relation holds of them and proves its negation if it does not. Write $\bar{n}$ for the numeral naming $n$. Define the provability predicate $\mathrm{Prov}_F(y) := \exists x\, \mathrm{Prf}_F(x,y)$. This is a $\Sigma_1$ formula: one unbounded existential quantifier over a decidable matrix. The third is the diagonal lemma, due to Gödel and stated in its general form by Carnap: for any formula $\psi(x)$ with one free variable, there is a sentence $\sigma$ with $$F \vdash \sigma \leftrightarrow \psi(\lceil \sigma \rceil)$$ The lemma requires only that $F$ represent the substitution function, which $Q$ does. Applying it to $\psi(x) := \neg\mathrm{Prov}_F(x)$ yields a sentence $G$ with $F \vdash G \leftrightarrow \neg\mathrm{Prov}_F(\lceil G \rceil)$. There is no self-reference in any objectionable sense here: $G$ is an ordinary arithmetical sentence, in fact a $\Pi_1$ sentence, asserting that no natural number stands in a certain decidable relation to a certain fixed numeral. The resemblance to the liar sentence is a resemblance in the proof's shape, not a shared defect. The two halves of the first theorem are not symmetric An earlier version of this essay wrote the theorem as: if $F$ is consistent, then neither $G$ nor $\neg G$ is provable in $F$. The first conjunct is right and the second is not, and the point is worth spelling out, because it is the single most frequent error in informal statements of the result. Unprovability of $G$. Suppose $F \vdash G$. Then some finite derivation exists; let $n$ be its code. Since $\mathrm{Prf}_F$ is represented, $F \vdash \mathrm{Prf}_F(\bar{n}, \lceil G \rceil)$, hence $F \vdash \mathrm{Prov}_F(\lceil G\rceil)$, hence by the fixed point $F \vdash \neg G$. So $F$ proves both $G$ and $\neg G$ and is inconsistent. Consistency alone therefore gives $F \not\vdash G$. Unprovability of $\neg G$. Here consistency is not enough, and Gödel knew it. Suppose $F \vdash \neg G$, that is, $F \vdash \exists x\, \mathrm{Prf}_F(x, \lceil G \rceil)$. From the first half we already know that if $F$ is consistent then $F \not\vdash G$, so no number actually codes a proof of $G$, and therefore $F \vdash \neg\mathrm{Prf}_F(\bar{n}, \lceil G\rceil)$ for every numeral $\bar{n}$. A system that proves an existential claim while refuting every one of its instances is not thereby inconsistent — no contradiction is derivable — but it is what Gödel called $\omega$-inconsistent. His theorem accordingly reads: if $F$ is consistent, $F \not\vdash G$; if $F$ is $\omega$-consistent, $F \not\vdash \neg G$. T