A Sentence About Its Own Number

Begin with a small formula such as 0 = 0. The laboratory's numbering scheme gives this formula code 5. This is an agreed encoding, not a calculation saying that zero equals five: the number 5 represents the written expression.

The language has ten kinds of construction. Five build terms, which name numbers: zero, successor, variables, addition and multiplication. Five build formulas: equality, negation, conjunction, a universal quantifier and the symbol Prov. That last symbol has no implemented meaning about provability in this laboratory.

Each kind has a tag from 0 to 9. A construction receives a code by multiplying its argument code by ten and adding its tag. Where it needs two arguments, their codes are first combined by a reversible pairing operation.

Decoding reverses these steps. Dividing 5 by ten leaves remainder 5, the equality tag, and quotient 0, which unpairs into the two zero terms. More complicated codes are decoded recursively; some numbers are rejected because they encode no well-formed expression.

The substitution view then replaces a formula's free variable with a numeral built from a code. This is a concrete ingredient of self-reference, not an implementation of a proof predicate or a proof of the incompleteness theorem.

A formula is a piece of writing about numbers. It cannot be about a formula, because formulas are not numbers, and there is no symbol in the language that means "formula".

Numbering removes that obstacle in the most literal way available. Once every formula has a number, and the numbering can be undone, a statement about a number is a statement about a formula. Nothing mystical happens: what changes is that a language whose only subject matter was arithmetic now has arithmetic that stands for its own syntax.

The second step is smaller than it looks. A formula $F(x)$ with one free variable is a slot waiting for a number. It has a code, and its code is a number. So there is nothing to stop you putting a formula's own code into its own slot, and once you have done it, the resulting sentence is about the formula you started from.

This is why the smallest example matters more than the famous one. The formula $0=0$ is the number 5. Wrap a negation round it and it is 56. The formula $\neg \mathrm{Prov}(x)$ is 296. Substituting 296 into it gives a sentence which, read out, says that the formula numbered 296 is not provable, and 296 is the formula that sentence came from.

The scheme is built from two reversible steps, and reversible is the load-bearing word.

The symbol code. For a node with symbol digit $t$ and payload $p$,

Division with remainder recovers $p$ and $t$ uniquely, which is why one number can be read back as a symbol and its argument.

The pairing. A symbol with two arguments has two codes to store in one payload, and Cantor's pairing does it:

This walks the diagonals of the quarter plane, hitting every natural number exactly once, so it can be undone as well.

Gödel used products of prime powers instead, which is a perfectly good bijection and produces codes of dozens of digits for the shortest formula there is. The pairing is chosen here for one reason: $0=0$ has code 5, and a reader can check the arithmetic without a computer.

Corner quotes. Writing $┌\phi ┐$ for the numeral of $\phi$'s code lets a sentence be printed as $\neg \mathrm{Prov}(┌\neg \mathrm{Prov}(x)┐)$ rather than as 296 successors. It is shorthand for how the page prints, not an extra symbol in the language.

Let $\mathcal{L}$ be the language above and $\#\phi$ the code of $\phi$.

1. $\#$ is injective and effectively invertible: there is an algorithm which, given $n$, returns the unique $\phi$ with $\#\phi =n$ or reports that there is none. Proved below, and checked exhaustively over every formula of depth at most 4 over three variables.
2. Diagonal Lemma. For a theory $T$ interpreting enough arithmetic and any $F(x)$ with one free variable, there is a sentence $G$ with $T⊢G\leftrightarrow F(┌G┐)$. Proved in the literature, and not here. What this laboratory carries out is the construction: $G=F(┌F┐)$, in which $F$'s code appears inside the sentence produced.
3. First incompleteness theorem. If $T$ is consistent, effectively axiomatised and interprets enough arithmetic, then $T$ is incomplete. Cited, and not reproduced anywhere on this page.
4. Presburger. First-order arithmetic with addition and without multiplication is complete and decidable. Proved in the literature, and the reason statement 3 has the conditions it has.

The distance between 2 and what the laboratory does is worth stating exactly. The lemma delivers a sentence equivalent to a statement about its own code; the construction here produces a sentence containing the code of the formula it was made from. Closing that gap requires a substitution function represented inside $T$, and there is no $T$ here.

Claim. The map $\#$ from formulas of $\mathcal{L}$ to natural numbers is injective, and there is an algorithm recovering $\phi$ from $\#\phi$.

Cantor's pairing is a bijection. For $a,b\ge 0$ put $s=a+b$. Then $⟨a,b⟩=s(s+1)/2+b$, and since $0\le b\le s$, the value lies in $[s(s+1)/2,(s+1)(s+2)/2)$. Those intervals for $s=0,1,2,\dots$ are disjoint and cover the natural numbers, so every $z$ determines $s$ uniquely, then $b=z-s(s+1)/2$, then $a=s-b$. ∎

One node is recoverable. A node's code is $10p+t$ with $0\le t\le 9$. Division by ten with remainder gives $t$ and $p$ uniquely, so the symbol and its payload are both determined. ∎

Induction on height. A leaf is $0$ or a variable: its code determines which, and for a variable the payload is the index. For a node of height $h+1$, the code gives its symbol and payload; the symbol says whether the payload is one child's code or a pair, and in the pair case the pairing is undone into two codes. Each child has height at most $h$, so by induction each is determined by its code. Hence the whole tree is determined. ∎

Effectiveness. The recovery is a finite computation: one division per node, one integer square root per pairing. It is what decode performs, and it either returns a formula or reports that the number codes none, since a payload may name a term where a formula is required. ∎

What this proof does not touch. It says nothing about provability, and the words "consistent", "axiom" and "theorem" do not appear in it. It is a statement about a numbering scheme. The incompleteness theorem is not established anywhere on this page, and could not be: this laboratory has no theory, no axioms and no notion of derivation. $\mathrm{Prov}$ is a symbol with a suggestive name and no meaning attached to it at all.

What this laboratory implements. The numbering and the diagonal construction, which are two ingredients of Gödel's proof. It does not implement provability. There is no proof predicate, no axiom set, no derivations and no search: $\mathrm{Prov}$ is an uninterpreted symbol. It does not prove the theorem, and no setting on this page brings it closer to doing so. The theorem is cited in the ledger above and reproduced nowhere.

What is actually checked here. Every formula of depth at most 4 over three variables goes through the encoder and back and returns unchanged, and every integer below a million either decodes to a formula that encodes back to itself or is refused. That is a finite check of a scheme whose general correctness is settled by the proof in layer 5, not by the check.

Where the theorem stops applying. The failure preset drops multiplication. Every part of the machinery on this page carries on working in that fragment: formulas have codes, codes come apart, the diagonal construction produces its sentence. What is gone is the conclusion, because Presburger arithmetic is complete and decidable, so there is no undecidable sentence in it to construct. That is the sharpest thing this page can say about the theorem's conditions: they are not decoration, and removing one symbol removes the theorem.

The gap that stays open on this page. The construction here produces a sentence carrying the code of the formula it was built from. The Diagonal Lemma produces a sentence provably equivalent to a statement about its own code. Getting from the first to the second needs a theory that can represent substitution as an arithmetic relation, which is the technical heart of Gödel's paper and is the part a browser cannot usefully show you.

Read this next to The Sequence That Reads Itself Aloud. There a rule reads its own output and writes down what it saw, and the self-description is at the level of digits. Here it is at the level of statements, and the extra machinery needed to move between the two levels is what took until 1931 to find.