In 1931, Kurt Gödel published the paper that permanently altered human epistemology: “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I”. Armed with the machinery of arithmetization, Gödel proved the Diagonal Lemma (Fixed-Point Lemma), allowing mathematical formulas to refer directly to their own syntactic properties. The consequence was devastating: any consistent formal theory capable of doing elementary arithmetic contains true mathematical assertions that can never be proven within the system.

1. The Diagonal Lemma (The Engine of Self-Reference)

Self-reference in natural language often produces semantic paradoxes like the Liar Paradox (“This statement is false”). Gödel avoided paradox by constructing self-reference purely within syntax, using substitution of numerals:

Let $text{sub}(x, y)$ be the primitive recursive function that takes the Gödel number of a formula $psi(v)$ with one free variable $v$, and returns the Gödel number of the formula $psi(bar{y})$ where the variable $v$ is replaced by the formal numeral for $y$. Since $text{sub}$ is primitive recursive, it is represented by a formula $text{Sub}(x, y, z)$ in $text{PA}$.

The Diagonal Lemma (Carnap-Gödel Fixed Point Theorem)

Let $T$ be any theory containing basic arithmetic, and let $psi(x)$ be any formula with one free variable. Then there exists a sentence $G$ such that:

[
T vdash G leftrightarrow psi(ulcorner G urcorner)
]

Proof:

  1. Define the diagonalizing formula $alpha(y) equiv exists z , (text{Sub}(y, y, z) land psi(z))$. Informally, $alpha(y)$ asserts: “Substitute numeral $y$ into formula $y$, and the result satisfies $psi$.”
  2. Let $m = ulcorner alpha(y) urcorner$ be the Gödel number of $alpha(y)$.
  3. Construct the sentence $G equiv alpha(bar{m})$.
  4. By definition of $alpha$, $G$ is equivalent to $psi(text{sub}(bar{m}, bar{m}))$. But what is $text{sub}(m, m)$? It is the Gödel number of $alpha(bar{m})$, which is none other than $ulcorner G urcorner$!
  5. Therefore, $T vdash G leftrightarrow psi(ulcorner G urcorner)$. $blacksquare$

2. Construction of Gödel’s Sentence $G$

Now, let $psi(x)$ be the formula $neg text{Prov}_T(x)$, which asserts: “Formula $x$ is not provable in $T$.” Applying the Diagonal Lemma to $neg text{Prov}_T(x)$ yields a sentence $G$ such that:

[
T vdash G leftrightarrow neg text{Prov}_T(ulcorner G urcorner)
]

Informally, $G$ asserts: “I am not provable in $T$.”

3. The Incompleteness Proof

Gödel’s First Incompleteness Theorem

Let $T$ be a consistent, effectively axiomatized formal theory capable of formalizing elementary arithmetic (such as Peano Arithmetic). Then:

  1. $T notvdash G$ (The sentence $G$ is not provable in $T$).
  2. If $T$ is $omega$-consistent (or sound), then $T notvdash neg G$ (The negation of $G$ is also not provable in $T$).
  3. Therefore, $G$ is undecidable in $T$.
  4. Furthermore, $G$ is TRUE in the standard model of arithmetic $mathbb{N}$!

Part 1: Proof that $T notvdash G$

Suppose $T vdash G$.

  • Since $G$ is provable, there exists a formal proof sequence $n$, so $text{Prf}_T(n, ulcorner G urcorner)$ is true.
  • Because $text{Prf}_T$ is primitive recursive, $T vdash text{Prf}_T(bar{n}, ulcorner G urcorner)$.
  • By existential generalization, $T vdash exists x , text{Prf}_T(x, ulcorner G urcorner)$, which means $T vdash text{Prov}_T(ulcorner G urcorner)$.
  • However, by definition of $G$, $T vdash G leftrightarrow neg text{Prov}_T(ulcorner G urcorner)$. Therefore, $T vdash neg text{Prov}_T(ulcorner G urcorner)$.
  • $T$ proves both $text{Prov}_T(ulcorner G urcorner)$ and $neg text{Prov}_T(ulcorner G urcorner)$, contradicting the consistency of $T$!
  • Thus, if $T$ is consistent, $T notvdash G$.

Part 2: Proof that $T notvdash neg G$

Suppose $T vdash neg G$.

  • By the equivalence of $G$, $T vdash text{Prov}_T(ulcorner G urcorner)$, which is $T vdash exists x , text{Prf}_T(x, ulcorner G urcorner)$.
  • However, from Part 1, we know $T notvdash G$. This means for every individual integer $k in mathbb{N}$, $k$ is NOT a proof of $G$.
  • Since $text{Prf}_T$ is primitive recursive, for each $k$, $T vdash neg text{Prf}_T(bar{k}, ulcorner G urcorner)$.
  • If $T$ proves $exists x , text{Prf}_T(x, ulcorner G urcorner)$ while simultaneously proving $neg text{Prf}_T(bar{k}, ulcorner G urcorner)$ for every individual $k$, $T$ is $omega$-inconsistent!
  • Thus, if $T$ is $omega$-consistent, $T notvdash neg G$.

4. The Chasm Between Truth and Proof

Why is $G$ true? $G$ asserts that it is unprovable. In Part 1, we mathematically proved that $G$ is indeed unprovable in $T$. Therefore, what $G$ asserts is an undeniable mathematical fact!

$G$ is a true arithmetical statement that $T$ cannot prove. In 1936, J. Barkley Rosser strengthened Gödel’s proof by substituting a modified provability predicate, eliminating the need for $omega$-consistency and requiring only simple consistency.

The philosophical consequence is absolute: Mathematical truth outstrips formal provability. No finite set of axioms, no matter how sophisticated, can ever encompass the totality of mathematical truth.

Shakil Mahmud Shazal

Shakil Mahmud Shazal

Senior Software Engineer based in Dhaka, Bangladesh. Building scalable web architectures and writing at the intersection of computer science, physical systems, history, and ideas.