Give every symbol a small number, then encode a whole formula as one integer: G = 2s₁ · 3s₂ · 5s₃ · … — the k-th prime raised to the k-th symbol code. Because a number factors into primes in exactly one way, that integer can be decoded back to the original formula, symbol for symbol. Arithmetic can now quote arithmetic. Down the center: symbols go in, the machine encodes and decodes, the number and its round-trip come out. The blue team builds it; the red team breaks it.
source E. Nagel & J. R. Newman, Gödel's Proof (1958), rendering Gödel's 1931 Über formal unentscheidbare Sätze — archive.org/details/gdelsproof00nage. Rendered, not quoted.
Number the positions of the formula 1,2,3,… and hand each one its own prime: position i gets pi (the i-th prime). Raise that prime to the symbol's code and multiply everything together.
Decoding just runs it backwards: divide out p₁ as many times as it goes — that count is s₁ — then p₂, then p₃. Unique factorization guarantees the counts are forced, so the formula comes back exactly.
Live, for the formula in the panel:
| i | sym | code si | prime pi | pisi |
|---|
Cantor's diagonal proved a list can never contain everything about itself. Gödel turns that trick into arithmetic: number the formulas, and a claim about formulas becomes a claim about numbers — a sentence the system can state in its own language.
The payload is the fixed point: the number that encodes "the formula with this number has no proof." True, and unprovable. Each sphere is the next one's premise — the diagonal made the mirror, this sphere numbers it.
The blue team's live check: encode then decode a battery of formulas and confirm every one returns identically, plus that two different formulas never collide onto the same number. If red swaps the primes, this badge is where it shows.
A tiny symbol alphabet, each with a fixed code (any injective assignment works; these are just the ones this machine uses). A formula is a sequence of these codes. The bases are the primes 2, 3, 5, 7, 11, …, one per position.
| code | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | 11 | 12 |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| glyph | 0 | s | = | + | × | ( | ) | x | ⇒ | ∀ | ¬ | ∃ |
Build a formula on the keypad below — those codes are what you feed the engine.
tap symbols to build a formula:
Every position multiplies in primecode. Change anything — the number is recomputed with BigInt on the spot, never looked up.
Gödel number G:
What the machine produces, proven: one integer that is the whole formula — — — and the decode that pulls the exact symbols back out of it. Encode and decode are inverse on every formula the witness tries; two different formulas never share a number.
The blue team's witness (left) confirms the round-trip live; the red team (right) tries to make decode lie.
And this machine encodes a flat sequence. Real syntax nests — Gödel encodes a proof as a sequence of formula-numbers, prime-coding a second time. The scheme here is the atom, honestly shown; it is not the whole arithmetization.
"Gödel numbering needs this exact 2·3·5 scheme." Cut. Any injective, computable encoding works — Cantor pairing, digits in a base, a hash with an inverse. Prime powers are just the clearest to decode, which is why they are shown here.
"The Gödel number is the proof of incompleteness." Cut. Numbering is only the arithmetization step. The result needs the diagonal lemma and a provability predicate on top; this sphere builds the floor, not the house.
"Longer formula ⇒ larger number." Kept, corrected. Not monotone in length — a short formula using a high code beats a long one of low codes. Order is by the whole product, not the count.
The red team's move: swap the prime bases 2,3,5,7 for the evens 2,4,6,8. Now the bases share factors, factorization is no longer unique — decode can no longer recover the symbols.
Non-prime bases make the encoding non-injective: the round-trip breaks, the witness (window 7) recomputes, disagrees, and turns red. The value genuinely changes — nothing is faked, and the attack is caught.