Gödel numbering

A Gödel numbering is a mechanism that assigns a unique natural number to every symbol, formula, and proof of a formal system. This arithmetization allows a system like MIU-system (or TNT itself) to be talked about within the language of arithmetic, and ultimately within TNT.

The core idea, due to Kurt Gödel, is that if a formal system is recursive (its rules can be executed algorithmically), then all syntactic properties — "this string is a well-formed formula", "this sequence of formulas is a proof" — correspond to arithmetic properties of the associated numbers. This makes the system "visible" from the inside of a sufficiently powerful arithmetic theory.

1. Encoding: symbols as numbers

Fix a bijection between the symbols of a formal system and a set of digits. For the MIU-system one may choose:

Symbol Code
M 3
I 1
U 0

A string like MU becomes the number 30, and MIIU becomes 3110. This is the Gödel number of the string.

2. Arithmetization: rules as operations

A typographical rule — a rule that shuffles symbols on paper — has a precise arithmetic counterpart acting on Gödel numbers. For example, in the MIU-system:

Typographical rule Arithmetic counterpart
I: xI → xIU (if a string ends in I, append U) If a number ends in digit 1, multiply by 10 (appending 0)
II: Mx → Mxx (double everything after M) If a number starts with 3, append the rest after itself
III: III → U (replace III with U) Replace substring 111 with 0
IV: UU → ε (delete UU) Delete substring 00

Thus a derivation in MIU — a sequence of rule applications starting from axiom MI (31) — becomes a chain of arithmetic operations on natural numbers. The statement "s is a theorem of MIU" translates to "the Gödel number of s can be reached from 31 by applying those arithmetic operations finitely many times".

3. From MIU to TNT: MUMON

Since TNT (Typographical Number Theory) is a formal system whose subject matter is natural numbers and their properties, it can express any arithmetic property that is primitive recursive (roughly, computable with predictable termination, just as "23 is not a perfect square"). The property "the number 30 is derivable from 31 via the MIU operations" is primitive recursive, so there exists a formula of TNT — call it MUMON — that asserts exactly that.

The three-level translation works as follows:

  1. MIU-level statement: MU is a theorem of MIU.
  2. Arithmetic level: The number 30 is an MIU-number (reachable from 31 by the arithmetic rules).
  3. TNT level: MUMON — a very long formula built from S, 0, +, ·, =, ∃, etc. — is a theorem of TNT.

Importantly, MUMON contains no letters M or U. It is a purely arithmetic formula whose interpretation under the standard model is "30 is an MIU-number".

Now consider the negation: ~MUMON. This formula of TNT says "30 is not reachable from 31 via the MIU rules" — and indeed it is true (the MU-puzzle has no solution). But notice: from TNT's perspective, ~MUMON is just another arithmetic statement, of exactly the same kind as "23 is not a perfect square" (¬∃a: a·a = SSSSSSSSSSSSSSSSSSSSSSS0, roughly). There is nothing "meta" about it. The fact that it was inspired by a question about a symbol-pushing game is invisible to TNT; internally it is indistinguishable from any other mundane arithmetic falsehood or truth.

4. Self-reference: TNT talks about TNT

Once we assign Gödel numbers to the symbols of TNT itself (a much larger table than the one for MIU), the same mechanism applies. TNT can express properties about TNT-formulas, TNT-proofs, and TNT-theorems.

See also