Gödel Numbering & Incompleteness Theorems

Gödel's decisive move was not a paradoxical English sentence. It was a compiler: encode every finite symbol string, formula, and proof as a natural number, then show that elementary arithmetic can express the mechanical relations among those codes. Once a theory can reason about its own proof checker, the diagonal lemma can construct a sentence whose arithmetic content tracks its own provability. Incompleteness is the resulting limit on effective formal theories strong enough for arithmetic, not a claim that every mathematical question is unknowable.

Three notions that must stay separate #

Gödel's completeness theorem for first-order logic says that every semantically valid first-order formula is formally derivable. His incompleteness theorem says that certain particular, effective theories of arithmetic cannot decide every sentence in their language. There is no contradiction: one result relates validity across all models to a proof calculus; the other concerns what follows from one recursively presented set of arithmetic axioms.

Arithmetizing syntax #

Assign every primitive symbol a positive integer. A finite sequence of symbol codes $a_1,\ldots,a_k$ can then be encoded, for example, as

$$\langle a_1,\ldots,a_k\rangle = 2^{a_1+1}3^{a_2+1}\cdots p_k^{a_k+1},$$

where $p_k$ is the $k$th prime. Unique prime factorization makes the sequence recoverable. Real proofs use a convenient effective coding—not necessarily this one—but the chosen code is incidental. What matters is that encoding, decoding, concatenation, substitution, and well-formedness are computable arithmetic operations.

This turns metasyntactic questions into number-theoretic predicates:

• $\mathop{\mathrm{Formula}}(n)$: $n$ codes a well-formed formula;
• $\mathop{\mathrm{Subst}}(f,v,t)$: substitute the term coded by $t$ for the variable coded by $v$ in the formula coded by $f$;
• $\mathop{\mathrm{Proof}}_T(p,n)$: $p$ codes a valid $T$-proof whose last line has code $n$;
• $\mathop{\mathrm{Prov}}_T(n)\equiv\exists p\,\mathop{\mathrm{Proof}}_T(p,n)$: the sentence coded by $n$ is provable in $T$.

The proof relation is decidable when the axiom system is presented in a suitable effective form, and it is representable inside weak arithmetic. The theory is therefore not equipped with a magical truth predicate; it contains an arithmetic model of a proof checker.

flowchart TD
    S["Finite syntax"] -->|"Gödel code"| N["Natural numbers"]
    N --> R["Arithmetic predicates for formula, substitution, proof"]
    R --> P["Prov_T(n)"]
    P --> D["Diagonal fixed point G"]
    D --> I["Limits on what T can prove"]

The diagonal lemma: controlled self-reference #

For any one-variable formula $\psi(x)$, the diagonal lemma constructs a sentence $\theta$ such that

$$T\vdash \theta\leftrightarrow\psi(\ulcorner\theta\urcorner),$$

where $\ulcorner\theta\urcorner$ is the numeral denoting the Gödel code of $\theta$. The construction is the formal analogue of giving a program its own source code: a substitution function first turns a formula's code into the code of that formula applied to its own code, and representability brings that operation inside arithmetic.

Choose $\psi(x)=\neg\mathop{\mathrm{Prov}}_T(x)$. The resulting Gödel sentence $G_T$ satisfies

$$T\vdash G_T\leftrightarrow\neg\mathop{\mathrm{Prov}}_T(\ulcorner G_T\urcorner).$$

It is useful to read this as "the particular sentence with this code has no $T$-proof," but the displayed biconditional—not an informal quotation—is the actual mathematical object.

First incompleteness theorem #

Assume $T$ is consistent. If $T\vdash G_T$, then there is a concrete proof code $p$. Because proof checking is representable, $T$ can verify that code and prove $\mathop{\mathrm{Prov}}_T(\ulcorner G_T\urcorner)$. But $T$ also proves $G_T\rightarrow\neg\mathop{\mathrm{Prov}}_T(\ulcorner G_T\urcorner)$, yielding a contradiction. Therefore $T\nvdash G_T$.

The other direction needs care:

• Gödel's original argument used $\omega$-consistency to obtain $T\nvdash\neg G_T$.
• Rosser's refinement constructs a different sentence comparing the shortest proofs of it and its negation; ordinary consistency then suffices to show that neither side is provable.

Thus a standard modern form is:

"Unprovable" is relative to $T$. Adding $R_T$ as a new axiom may decide that sentence, but the stronger effective theory—if it remains consistent—has a new independent sentence. The theorem blocks a final effective completion, not the extension of any particular theory.

When may the Gödel sentence be called true? #

Provability is syntactic; truth is semantic. If $T$ is sound in the standard natural numbers, then $G_T$ is true in $\mathbb N$: there really is no natural number coding a $T$-proof of it. Consistency alone is enough for the unprovability half of the argument, but it does not justify casually identifying everything $T$ cannot refute with standard truth.

This distinction also explains two important counterpoints:

• True arithmetic, the set of all sentences true in $\mathbb N$, is complete, but it is not computably axiomatizable.
• Presburger arithmetic, which has addition but not multiplication, is complete and decidable. It is not strong enough for the arithmetization required by the theorem.

Incompleteness is a three-way constraint: a theory cannot simultaneously retain the relevant arithmetic strength, effective axiomatization, consistency, and completeness.

Second incompleteness theorem #

Let

$$\mathop{\mathrm{Con}}(T)\equiv\neg\mathop{\mathrm{Prov}}_T(\ulcorner 0=1\urcorner)$$

be the standard arithmetical statement that no $T$-proof of a contradiction exists. Under the usual representability and derivability conditions on the chosen provability predicate, the reasoning about $G_T$ can itself be formalized in $T$ strongly enough to establish

$$T\vdash\mathop{\mathrm{Con}}(T)\rightarrow G_T.$$

If a consistent $T$ proved $\mathop{\mathrm{Con}}(T)$, it would prove $G_T$, contradicting the first theorem's unprovability result. Hence:

This does not say that consistency proofs are impossible. A stronger theory $S$ may prove $\mathop{\mathrm{Con}}(T)$; the theorem says that $S$ then inherits the analogous question about $\mathop{\mathrm{Con}}(S)$. It also does not apply to arbitrary sentences merely called "consistency": the formalized proof predicate and its derivability properties matter.

Incompleteness implies an algorithmic boundary #

Proofs of a computably axiomatized theory can be enumerated. If such a theory were also consistent and complete, an algorithm deciding theoremhood could run two proof searches in parallel: one for $\varphi$, one for $\neg\varphi$. Completeness guarantees that one search finishes, and consistency guarantees that they do not both succeed. For sufficiently strong arithmetic, incompleteness prevents this route; theoremhood is computably enumerable but undecidable.

That connection is not an accident. Gödel coding supplies the data representation, representability supplies an interpreter for effective operations, and diagonalization lets the system confront the behavior of its own proof enumeration. The same pattern reappears in the halting problem.

Misreadings to reject #

A practical reasoning checklist #

When an incompleteness claim appears, ask:

1. Which theory $T$? Its language, axioms, and proof calculus must be fixed.
2. Is $T$ effective? Can its axioms or proofs be mechanically enumerated?
3. How strong is it? Can it represent the required syntax and elementary arithmetic?
4. Which assumption is used? Consistency, $\omega$-consistency, or soundness are not interchangeable.
5. Is the claim syntactic or semantic? "Not provable in $T$" and "false in $\mathbb N$" answer different questions.
6. Is consistency internalized canonically? The second theorem concerns a represented proof predicate satisfying precise derivability conditions.