For millennia, numbers were perceived as objects to be studied, while logical deductions about those numbers were considered an external commentary belonging to philosophy. In 1931, Kurt Gödel obliterated this distinction. By formalizing Peano Arithmetic ($text{PA}$) and inventing Gödel numbering, he showed that the entire metamathematical architecture of proofs, deductions, axioms, and formulas can be encoded bijectively as integers within arithmetic itself. The commentator became part of the play.
1. The Dedekind-Peano Axiomatization
First-Order Peano Arithmetic is formulated in the signature $mathcal{L}_A = {0, S, +, times}$, where $0$ is a constant, $S$ is the unary successor function ($S(x) = x + 1$), and $+$, $times$ are binary operations. The theory $text{PA}$ consists of seven basic axioms plus the Induction Schema:
- Zero is not a successor: $forall x , (S(x) neq 0)$
- Successor is injective: $forall x forall y , (S(x) = S(y) to x = y)$
- Addition base: $forall x , (x + 0 = x)$
- Addition recursion: $forall x forall y , (x + S(y) = S(x + y))$
- Multiplication base: $forall x , (x times 0 = 0)$
- Multiplication recursion: $forall x forall y , (x times S(y) = (x times y) + x)$
The Axiom Schema of Induction
For every first-order formula $phi(x, y_1, dots, y_k)$ with parameters $vec{y}$:
[
forall vec{y} ; Big( big( phi(0, vec{y}) land forall x (phi(x, vec{y}) to phi(S(x), vec{y})) big) to forall x , phi(x, vec{y}) Big)
]
Because there are countably infinitely many formulas $phi$, $text{PA}$ is an infinite first-order theory. In second-order logic, induction can quantify over all subsets of $mathbb{N}$ ($forall X subseteq mathbb{N}$), which is categorical; but in first-order logic, $text{PA}$ is restricted to definable sets, opening the door to non-standard models.
2. Primitive Recursive Functions
A function $f: mathbb{N}^k to mathbb{N}$ is primitive recursive if it can be built from basic functions (Zero $Z(x)=0$, Successor $S(x)=x+1$, and Projections $P_i^k(vec{x})=x_i$) via finitely many applications of:
- Composition: $h(vec{x}) = f(g_1(vec{x}), dots, g_m(vec{x}))$
- Primitive Recursion:
[
h(0, vec{x}) = f(vec{x})
]
[
h(S(y), vec{x}) = g(y, h(y, vec{x}), vec{x})
]
Addition, multiplication, exponentiation, factorial, prime-testing, and sequence-decoding are all strictly primitive recursive. Every primitive recursive function is provably representable inside $text{PA}$ via Gödel’s $beta$-function lemma.
3. Gödel Numbering: The Arithmetic Translation
Gödel’s masterstroke was assigning a unique integer $ulcorner s urcorner in mathbb{N}$ to every symbol, formula, and sequence of formulas:
Step 1: Symbol Table
Assign odd integers to the basic logical symbols:
[
ulcorner neg urcorner = 1, quad ulcorner lor urcorner = 3, quad ulcorner forall urcorner = 5, quad ulcorner ( urcorner = 7, quad ulcorner ) urcorner = 9, quad ulcorner = urcorner = 11, quad ulcorner 0 urcorner = 13, quad ulcorner S urcorner = 15, quad ulcorner + urcorner = 17, quad ulcorner times urcorner = 19
]
Variables $x_k$ receive even numbers: $ulcorner x_k urcorner = 2k$.
Step 2: Formula Arithmetization via Fundamental Theorem of Arithmetic
A formula is a finite sequence of symbols $s_1 s_2 dots s_k$. Its Gödel number is encoded using prime factorization:
[
ulcorner s_1 s_2 dots s_k urcorner = 2^{ulcorner s_1 urcorner} cdot 3^{ulcorner s_2 urcorner} cdot 5^{ulcorner s_3 urcorner} cdots p_k^{ulcorner s_k urcorner}
]
Because every integer has a unique prime factorization, any formula can be mechanically and uniquely reconstructed from its Gödel number.
Step 3: Proof Arithmetization
A formal proof is a sequence of formulas $langle phi_1, phi_2, dots, phi_m rangle$. Its Gödel number is:
[
ulcorner langle phi_1, dots, phi_m rangle urcorner = 2^{ulcorner phi_1 urcorner} cdot 3^{ulcorner phi_2 urcorner} cdots p_m^{ulcorner phi_m urcorner}
]
4. The Proof Predicate $text{Prf}(x, y)$
Syntactic proof verification is purely mechanical: checking whether a given line is an axiom or follows from previous lines via Modus Ponens requires only inspecting symbols. Therefore, the relation:
[
text{Prf}_{text{PA}}(x, y) equiv text{“} x text{ is the Gödel number of a valid PA-proof of the formula with Gödel number } y text{“}
]
is a primitive recursive relation! Since every primitive recursive relation is representable in $text{PA}$, there exists an explicit arithmetic formula $text{Prf}(x, y)$ such that:
- If $n$ is a proof of $phi$, then $text{PA} vdash text{Prf}(bar{n}, ulcorner phi urcorner)$.
- If $n$ is not a proof of $phi$, then $text{PA} vdash neg text{Prf}(bar{n}, ulcorner phi urcorner)$.
The provability predicate is defined by prefixing an existential quantifier:
[
text{Prov}_{text{PA}}(y) equiv exists x , text{Prf}_{text{PA}}(x, y)
]
$text{Prov}_{text{PA}}(y)$ is a $Sigma_1$-arithmetical formula asserting: “There exists an integer $x$ that encodes a formal proof of formula $y$.” Mathematics had officially acquired the power to interrogate its own proofs.
