Constructing Gödel Sentences

Mathematical Logic · Axiom Academy

EXAMPLE Constructing Gödel Sentences Step-by-step walkthrough of Gödel numbering, encoding, and self-reference Excellent work! You've walked through the construction of Gödel sentences. Here's what we learned: Gödel Numbering: Every symbol, formula, and proof can be encoded as a unique natural number using prime factorization. This allows us to talk about syntax within arithmetic. Encoding Formulas: A formula like ∀x(x = x) gets encoded as a product of primes raised to powers corresponding to symbol codes: 2^7 · 3^4 · 5^11 · 7^4 · 11^5 · 13^4 · 17^12. Provability Predicate: We can express "y is a proof of x" as an arithmetic relation Prf(x,y), making provability itself a mathematical object we can reason about. Diagonalization: The key trick is self-reference: we construct a formula that talks about its own Gödel number. The substitution function sub(φ,n) replaces the free variable in φ with the numeral for n. The Fixed-Point Lemma: For any formula φ(x), there exists a sentence G such that T ⊢ G ↔ φ(⌜G⌝). This is the technical heart of the proof. The Gödel Sentence: Let G be the fixed point of ¬Prov(x), so G ↔ ¬Prov(⌜G⌝). Then G literally says "I am not provable in T". The Paradox Resolution: If T is consistent, G cannot be proved (else G would be false but provable). If T is ω-consistent, ¬G also cannot be proved. So G is true but unprovable!

This is the written version of the interactive lesson above. See the full Mathematical Logic course.