A formula is encoded as: ∏ pᵢ^aᵢ where pᵢ is the i-th prime and aᵢ is the Gödel number of the i-th symbol.
Enter a formula and click Encode
Enter a Gödel number
The Diagonal Lemma (Fixed Point Theorem)
For any formula φ(x) with one free variable, there exists a sentence ψ such that: PA ⊢ ψ ↔ φ(⌈ψ⌉)
where ⌈ψ⌉ is the Gödel number of ψ itself.
This is self-reference made rigorous. ψ "talks about itself" through its own Gödel number.
Statement ψ
mentions
⟶
Gödel number ⌈ψ⌉
encodes
⟶
ψ itself
= same statement!
How it works:
1. Define sub(n,m): substitute numeral m for free variable in formula #n
2. Define diag(n) = sub(n,n) — "apply formula n to its own code"
3. For any property φ, let ψ say "φ(diag(⌈φ(diag(x))⌉))"
4. Then ψ is equivalent to φ(⌈ψ⌉) — ψ talks about itself!
THE GÖDEL SENTENCE
G = "This statement is not provable in PA"
formally: ¬Provable(⌈G⌉)
If G is provable
⟹
G says it's not provable
⟹
Contradiction! PA inconsistent
∴ If PA is consistent, G is not provable
G is not provable
⟹
G is TRUE
⟹
G is undecidable
First Incompleteness Theorem
Any consistent formal system T which:
• Contains PA (arithmetic)
• Is recursively axiomatizable
...cannot be complete. There exist statements in T's language that are neither provable nor refutable in T.
Proof steps:
1. Encode all syntax as natural numbers
2. "Provable(x)" is expressible in PA
3. Diagonal lemma gives G = ¬Provable(⌈G⌉)
4. G is true but not provable (if T consistent)
5. ¬G is also not provable (if T ω-consistent)
Second Incompleteness Theorem
T cannot prove its own consistency: T ⊬ Con(T)
This follows because: Con(T) → ¬Provable(⌈G⌉)
but G is equivalent to ¬Provable(⌈G⌉), so Con(T)→G, and if T proved Con(T) it would prove G — contradiction.
Famous consequences:
• Hilbert's program fails
• No "theory of everything" in formal math
• True arithmetic ≠ any formal theory
• Chaitin: most truths have no finite proof