Mathematics · Mathematical Logic · Foundations

Kurt Gödel & the
Incompleteness
of Mathematics

A comprehensive guide to the most profound and unsettling results in the history of formal mathematics — with proofs, interactive demonstrations, and GNU Octave code.

1931 — Theorems published Über formal unentscheidbare Sätze Peano Arithmetic — primary system

§ 01

Biography & Historical Context

Kurt Friedrich Gödel (April 28, 1906 – January 14, 1978) was an Austrian-American logician, mathematician, and analytic philosopher. He is widely regarded as one of the greatest logicians of all time, with his incompleteness theorems producing a seismic shift in the foundations of mathematics.

Life

1906

Born in Brünn, Austria-Hungary (now Brno, Czech Republic)

Showed exceptional mathematical talent from childhood.

1924

University of Vienna

Enrolled studying physics; quickly shifted to mathematics and logic.

1929

Completeness Theorem

Doctoral dissertation proving the Completeness of first-order logic.

1931

Incompleteness Theorems

Published Über formal unentscheidbare Sätze… — the most celebrated paper in 20th-century mathematics.

1940

Institute for Advanced Study, Princeton

Emigrated to the USA; close friendship with Einstein.

1949

Rotating Universe

Discovered a solution to Einstein's equations allowing closed time-like curves.

1978

Death

Died of self-starvation after the death of his wife, Adele, weighing only 65 lb.

The Intellectual Climate

To understand Gödel, you must understand what he destroyed: Hilbert's Programme.

Hilbert's Dream (1900–1930)

David Hilbert believed mathematics could be placed on an absolutely certain foundation — a finite set of axioms from which every true mathematical statement could be proved, and whose own consistency could be proved from within. This was the "formalist" dream.

Mathematicians of the 1920s — Hilbert, Russell, Whitehead (Principia Mathematica), Zermelo, Fraenkel — were racing to complete this programme. The Vienna Circle of logical positivists believed all of mathematics and science could be reduced to formal symbols.

In 1931, the 25-year-old Gödel annihilated this dream with two theorems that showed:

Any sufficiently powerful consistent formal system contains true statements it cannot prove.
Such a system cannot even prove its own consistency.

Famous Contemporaries

David HilbertBertrand RussellAlan TuringJohn von NeumannLudwig WittgensteinAlfred Tarski

§ 02

Formal Systems

Before we can understand Gödel, we need to understand what a formal system is — because that is precisely what his theorems are about.

Definition — Formal System

A formal system $\mathcal{F}$ consists of:

An alphabet $\Sigma$ — a finite set of symbols
A grammar — rules for forming well-formed formulas (wffs)
A set of axioms $\mathcal{A}$ — formulas taken as true without proof
A set of inference rules $\mathcal{R}$ — rules for deriving new formulas from existing ones

Key Properties of Formal Systems

Consistency

$\mathcal{F}$ is consistent if there is no formula $\phi$ such that both $\phi$ and $\lnot\phi$ are provable.

$\nexists\,\phi : \mathcal{F} \vdash \phi \land \mathcal{F} \vdash \lnot\phi$

Completeness

$\mathcal{F}$ is complete if every true formula is provable:

$\phi \text{ true} \Rightarrow \mathcal{F} \vdash \phi$

Equivalently: $\mathcal{F} \vdash \phi$ or $\mathcal{F} \vdash \lnot\phi$ for all $\phi$.

Decidability

$\mathcal{F}$ is decidable if there is an algorithm that, given any formula $\phi$, determines in finite time whether $\mathcal{F} \vdash \phi$.

Soundness

$\mathcal{F}$ is sound if every provable formula is true (in the intended model):

$\mathcal{F} \vdash \phi \Rightarrow \phi \text{ is true}$

Expressiveness

Can the system talk about the natural numbers? Can it express statements about addition, multiplication, primality?

Omega-Consistency

Stronger than consistency: $\mathcal{F}$ does not prove $\exists x \, P(x)$ while also proving $\lnot P(0)$, $\lnot P(1)$, $\lnot P(2)$, … for every numeral.

Peano Arithmetic (PA)

The primary system Gödel studied is Peano Arithmetic — the standard first-order axiomatization of natural number arithmetic, due to Giuseppe Peano (1889).

Definition — Peano Axioms

Let $0$ denote zero and $S(x)$ the successor of $x$ (i.e., $x+1$). The Peano axioms for $\mathbb{N}$ are:

\begin{array}{ll} \text{PA1} & S(x) \neq 0 \quad (\text{zero is not a successor})\\[4pt] \text{PA2} & S(x) = S(y) \Rightarrow x = y \quad (\text{successor is injective})\\[4pt] \text{PA3} & x + 0 = x\\[4pt] \text{PA4} & x + S(y) = S(x + y)\\[4pt] \text{PA5} & x \cdot 0 = 0\\[4pt] \text{PA6} & x \cdot S(y) = (x \cdot y) + x\\[4pt] \text{PA7} & \bigl[\phi(0) \land \forall n\,(\phi(n) \Rightarrow \phi(S(n)))\bigr] \Rightarrow \forall n\,\phi(n) \quad (\text{induction schema}) \end{array}

PA is powerful enough to express (and prove) essentially all of elementary number theory: divisibility, primality, the Euclidean algorithm, the Chinese Remainder Theorem, and much more. This is precisely why Gödel's theorems apply to it.

§ 03

Axioms, Inference Rules & Proofs

Logical Connectives & Quantifiers

Symbol	Name	Meaning	Example
$\lnot \phi$	Negation	not $\phi$	$\lnot (2=3)$ is true
$\phi \land \psi$	Conjunction	$\phi$ and $\psi$	$(2{>}1) \land (3{>}2)$
$\phi \lor \psi$	Disjunction	$\phi$ or $\psi$	$(x{=}0) \lor (x{>}0)$
$\phi \Rightarrow \psi$	Implication	if $\phi$ then $\psi$	$x{>}2 \Rightarrow x{>}1$
$\phi \Leftrightarrow \psi$	Biconditional	$\phi$ iff $\psi$	$x{=}0 \Leftrightarrow x{+}1{=}1$
$\forall x\,\phi(x)$	Universal	for all $x$, $\phi(x)$	$\forall x\,(x{+}0{=}x)$
$\exists x\,\phi(x)$	Existential	there exists $x$ s.t. $\phi(x)$	$\exists x\,(x{>}5)$
$\mathcal{F} \vdash \phi$	Provability	$\phi$ is provable in $\mathcal{F}$	$\text{PA} \vdash 2{+}2{=}4$
$\phi \models \psi$	Semantic entail.	every model of $\phi$ satisfies $\psi$	$\text{PA} \models \forall x\,x{+}0{=}x$

Core Inference Rules

Modus Ponens

$$\frac{\phi \qquad \phi \Rightarrow \psi}{\psi}$$

From "$\phi$" and "if $\phi$ then $\psi$", conclude $\psi$. The most fundamental rule in logic.

Generalization

$$\frac{\phi(x)}{\forall x\,\phi(x)}$$

If $\phi(x)$ holds for an arbitrary $x$, we may universally quantify. ($x$ must be a free variable not assumed fixed.)

What is a Proof?

Formal Definition of Proof

A proof of $\phi$ in $\mathcal{F}$ is a finite sequence of formulas $\phi_1, \phi_2, \ldots, \phi_n$ where $\phi_n = \phi$, and each $\phi_i$ is either:

An axiom of $\mathcal{F}$, or
Derived from earlier formulas by an inference rule.

This is purely mechanical and syntactic — no meaning required.

The crucial insight: a proof is just a finite string of symbols. This means proofs can be represented as numbers. And this — Gödel's masterstroke — is where everything begins.

§ 04

Gödel's Completeness Theorem (1929)

⚠ Warning — Completeness vs. Incompleteness

Gödel proved two different theorems with nearly opposite names. The Completeness Theorem (1929, his PhD thesis) is a positive result about first-order logic. The Incompleteness Theorems (1931) are about arithmetic and are negative/limiting results. Do not confuse them!

Theorem — Gödel's Completeness Theorem (1929)

Let $\mathcal{L}$ be a first-order language and $T$ a set of sentences in $\mathcal{L}$. Then: $$T \models \phi \quad \Longleftrightarrow \quad T \vdash \phi$$ That is: every first-order statement that is semantically valid (true in all models of $T$) is also syntactically provable from $T$.

This is remarkable: for first-order logic alone, semantic truth and syntactic proof perfectly coincide. The deductive calculus of first-order logic is complete.

Compactness Theorem

An elegant corollary of Completeness:

Theorem — Compactness

A set of first-order sentences $T$ has a model if and only if every finite subset of $T$ has a model. $$T \text{ satisfiable} \;\Longleftrightarrow\; \text{every finite } T_0 \subseteq T \text{ satisfiable}$$

So why does the Incompleteness Theorem still hold? Because it is about systems strong enough to express arithmetic — and the interaction between arithmetic expressiveness and self-reference creates an unavoidable barrier.

§ 05

First Incompleteness Theorem

Theorem — Gödel's First Incompleteness Theorem (1931)

Let $\mathcal{F}$ be any consistent formal system that:

Is recursively axiomatizable (there is an algorithm to list its axioms)
Is powerful enough to express basic arithmetic (can talk about $\mathbb{N}$, $+$, $\times$)

Then there exists a sentence $G_\mathcal{F}$ in the language of $\mathcal{F}$ such that:

$$\mathcal{F} \nvdash G_\mathcal{F} \qquad \text{and} \qquad \mathcal{F} \nvdash \lnot G_\mathcal{F}$$

That is: $G_\mathcal{F}$ is undecidable in $\mathcal{F}$ — it can be neither proved nor disproved. Furthermore, $G_\mathcal{F}$ is true (in the standard model $\mathbb{N}$).

Consequence: $\mathcal{F}$ is incomplete — it cannot prove all arithmetic truths.

Intuitive Explanation

The sentence $G_\mathcal{F}$ essentially says:

The Gödel Sentence

"This statement is not provable in $\mathcal{F}$."

This is a precise mathematical analogue of the ancient Liar Paradox ("This statement is false"), but constructed without paradox — because it talks about provability, not truth.

Why Neither Can Be Proved

Case 1: Suppose $\mathcal{F} \vdash G$

Then $G$ is provable. But $G$ says "I am not provable." So $G$ is false. This means $\mathcal{F}$ proves a false statement, contradicting its soundness (or $\omega$-consistency). Contradiction.

Case 2: Suppose $\mathcal{F} \vdash \lnot G$

Then $\mathcal{F}$ proves "G is provable." But if $G$ is provable, then $G$ is true, i.e., $G$ is not provable. Under $\omega$-consistency, this leads to a contradiction. Contradiction.

Therefore, assuming $\mathcal{F}$ is consistent (and $\omega$-consistent for the $\lnot G$ direction, or just consistent in Rosser's later refinement), neither $G$ nor $\lnot G$ is provable.

The Rosser Improvement (1936)

Theorem — Rosser's Extension

J. Barkley Rosser strengthened Gödel's result: the assumption of $\omega$-consistency can be weakened to mere consistency. Using a modified "Rosser sentence": $$R: \text{"For every proof of }R\text{, there is a shorter proof of }\lnot R\text{"}$$ The same undecidability follows from consistency alone.

Concrete Example: Con(PA)

The most natural Gödel sentence for PA is the statement Con(PA) — "Peano Arithmetic is consistent." By the Second Incompleteness Theorem (§ 06), if PA is consistent then:

\text{PA} \nvdash \text{Con(PA)}

This is a true arithmetic statement (assuming PA is indeed consistent) that PA cannot prove about itself. This is perhaps the most dramatic consequence of the incompleteness theorems.

§ 06

Second Incompleteness Theorem

Theorem — Gödel's Second Incompleteness Theorem (1931)

Under the same hypotheses as the First Incompleteness Theorem:

$$\mathcal{F} \nvdash \text{Con}(\mathcal{F})$$

where $\text{Con}(\mathcal{F})$ is the arithmetical sentence encoding the statement "$\mathcal{F}$ is consistent".

No sufficiently powerful consistent system can prove its own consistency.

Why This Follows from the First

The Second Theorem is essentially a strengthening of the First. The key observation:

\text{Con}(\mathcal{F}) \Rightarrow G_\mathcal{F} \quad \text{is provable in } \mathcal{F}

That is, $\mathcal{F}$ itself can prove: "If I am consistent, then $G$ is unprovable." But since $G$ is unprovable (assuming consistency), and $\mathcal{F}$ cannot prove $G$, if $\mathcal{F}$ could prove its own consistency, it could prove $G$ — contradicting the First Theorem. Therefore:

The Devastating Consequence

$\mathcal{F} \vdash [\text{Con}(\mathcal{F}) \Rightarrow G_\mathcal{F}]$ (provable in $\mathcal{F}$)
$\mathcal{F} \nvdash G_\mathcal{F}$ (by First Incompleteness)
Therefore: $\mathcal{F} \nvdash \text{Con}(\mathcal{F})$ (by contrapositive + modus ponens)

Any proof of consistency would require a stronger system — pushing the problem upward forever. There is no "bedrock" of certainty.

Hilbert's Consistency Programme — Destroyed

Hilbert had demanded a finitary proof that mathematics (specifically, formalized arithmetic) is consistent. Gödel showed this is impossible: you cannot prove PA is consistent using only resources available within PA. You need a stronger system — but then you need to prove that system is consistent, and so on, forever.

Gentzen's Partial Response (1936)

Gerhard Gentzen later proved Con(PA) — but only by using transfinite induction up to the ordinal $\varepsilon_0 = \omega^{\omega^{\omega^{\cdots}}}$. This is a principle not available inside PA, confirming Gödel: you always need a stronger system to prove consistency of the weaker one.

§ 07

Gödel Numbering

The technical heart of the proof is a coding scheme that translates formulas and proofs into natural numbers. This allows the system to "talk about itself" through arithmetic.

The Basic Idea

Assign a unique natural number — the Gödel number (or code) — to every:

Symbol in the language
Formula (sequence of symbols)
Proof (sequence of formulas)

The encoding uses the Fundamental Theorem of Arithmetic: every positive integer has a unique prime factorization.

Definition — Gödel Number of a Sequence

Given a sequence of natural numbers $(a_1, a_2, \ldots, a_n)$, its Gödel number is:

\langle a_1, a_2, \ldots, a_n \rangle = p_1^{a_1} \cdot p_2^{a_2} \cdots p_n^{a_n}

where $p_i$ is the $i$-th prime: $p_1=2, p_2=3, p_3=5, p_4=7, \ldots$

Example: $\langle 3, 1, 2 \rangle = 2^3 \cdot 3^1 \cdot 5^2 = 8 \cdot 3 \cdot 25 = 600$

Symbol Encoding

First assign numbers to the basic symbols of PA:

Symbol	Code	Category
$0$	1	Constant
$S$	2	Function (successor)
$+$	3	Function
$\times$	4	Function
$=$	5	Relation
$\lnot$	6	Connective
$\Rightarrow$	7	Connective
$\forall$	8	Quantifier
$($	9	Punctuation
$)$	10	Punctuation
$v_1, v_2, \ldots$	$10+k$	Variables

Encoding a Formula

The formula $S(0) = S(0)$ (meaning "$1 = 1$") uses symbols: $S$, $(\ )$, $0$, $=$, $S$, $(\ )$, $0$. Their codes are: $2, 9, 1, 10, 5, 2, 9, 1, 10$.

\ulcorner S(0) = S(0) \urcorner = 2^2 \cdot 3^9 \cdot 5^1 \cdot 7^{10} \cdot 11^5 \cdot 13^2 \cdot 17^9 \cdot 19^1 \cdot 23^{10}

This is a specific, astronomically large natural number. But it is a number, and PA can reason about it.

Key Arithmetically-Definable Predicates

The power of Gödel numbering is that all the important metamathematical concepts become arithmetic predicates:

Predicate	Meaning	Note
$\text{Prf}(x, y)$	$x$ is the Gödel number of a proof of the formula with Gödel number $y$	Primitive recursive
$\text{Pvbl}(y)$	$\exists x\, \text{Prf}(x, y)$ — formula $y$ is provable	Existential quantification
$\text{Form}(x)$	$x$ is the Gödel number of a well-formed formula	Decidable
$\text{Axiom}(x)$	$x$ is the Gödel number of an axiom	Decidable (recursive axioms)
$\text{Sub}(x, v, t)$	Result of substituting term $t$ for variable $v$ in formula $x$	Primitive recursive

$\text{Prf}(x, y)$ is primitive recursive — it can be checked mechanically and expressed in PA.

§ 08

The Diagonal Lemma (Self-Reference Lemma)

The Diagonal Lemma is the key machinery that allows us to construct the Gödel sentence. It is the formal version of self-reference, and it is a theorem provable in PA.

Theorem — Diagonal Lemma (Carnap, Gödel)

For any formula $\phi(x)$ with one free variable $x$ in the language of PA, there exists a sentence $\psi$ such that: $$\text{PA} \vdash \psi \Leftrightarrow \phi(\ulcorner \psi \urcorner)$$ where $\ulcorner \psi \urcorner$ is the Gödel number of $\psi$.

In words: "$\psi$ is (provably equivalent to) the statement obtained by plugging $\psi$'s own code into $\phi$."

Proof of the Diagonal Lemma

Proof

Step 1. Define the substitution function. For any formula $\alpha(x)$, let $\text{diag}(\alpha)$ be the sentence obtained by substituting the Gödel number $\ulcorner \alpha(x) \urcorner$ for $x$ in $\alpha$:

$$\text{diag}(\alpha) \equiv \alpha(\ulcorner \alpha(x) \urcorner)$$

Step 2. The function $x \mapsto \ulcorner \text{diag}(\alpha_x) \urcorner$ (where $\alpha_x$ is the formula with Gödel number $x$) is primitive recursive — call it $d(x)$. So $d$ is representable in PA.

Step 3. Let $\theta(x) \equiv \phi(d(x))$. Apply $\theta$ to its own Gödel number: define

$$\psi \equiv \theta(\ulcorner \theta(x) \urcorner) \equiv \phi(d(\ulcorner \theta(x) \urcorner)) \equiv \phi(\ulcorner \text{diag}(\theta) \urcorner) \equiv \phi(\ulcorner \psi \urcorner)$$

Step 4. Since $d$ is representable in PA, this whole chain of equalities holds as a formal proof in PA. Therefore $\text{PA} \vdash \psi \Leftrightarrow \phi(\ulcorner \psi \urcorner)$. $\square$

Applications of the Diagonal Lemma

Choose $\phi(x)$ as…	The resulting $\psi$ says…	Result
$\lnot \text{Pvbl}(x)$	"I am not provable"	Gödel sentence $G$
$\text{Pvbl}(\lnot x)$	"My negation is provable"	Used in Löb's Theorem
$\lnot \text{True}(x)$	"I am false"	Tarski's Undefinability
$\phi = \bot$ (contradiction)	"This is unprovable and refutable"	Rosser sentence

§ 09

Full Proof Sketch — First Incompleteness Theorem

Proof — First Incompleteness Theorem

Assumptions: Let $\mathcal{F}$ be a consistent, recursively axiomatizable system extending PA.

Step 1 — Gödel Numbering. Assign Gödel numbers to all symbols, formulas, and finite sequences of formulas. The Gödel numbering is a computable injection. Prove that all syntactic operations (concatenation, substitution, checking well-formedness, checking axiomhood) correspond to primitive recursive functions on their Gödel numbers.

Step 2 — Representability. For any primitive recursive predicate $P$, there is a formula $\hat{P}(x)$ in PA such that: $$P(n) \text{ holds} \Rightarrow \text{PA} \vdash \hat{P}(\bar{n}) \qquad P(n) \text{ fails} \Rightarrow \text{PA} \vdash \lnot\hat{P}(\bar{n})$$ where $\bar{n}$ is the numeral for $n$. This is the Representation Theorem for primitive recursive predicates.

Step 3 — Proof Predicate. The predicate $\text{Prf}(x, y)$ — "$x$ is a proof of $y$" — is primitive recursive. So it is representable in $\mathcal{F}$. Define:

$$\text{Pvbl}(y) \;\equiv\; \exists x\, \widehat{\text{Prf}}(x, y)$$

Step 4 — Gödel Sentence. Apply the Diagonal Lemma to $\phi(x) = \lnot\text{Pvbl}(x)$. Obtain a sentence $G$ with: $$\mathcal{F} \vdash G \Leftrightarrow \lnot \text{Pvbl}(\ulcorner G \urcorner)$$ Informally: $G$ asserts its own unprovability in $\mathcal{F}$.

Step 5 — $G$ is not provable. Suppose $\mathcal{F} \vdash G$. Then by the Representation Theorem, $\mathcal{F} \vdash \text{Pvbl}(\ulcorner G \urcorner)$. But $G \Leftrightarrow \lnot\text{Pvbl}(\ulcorner G \urcorner)$, so $\mathcal{F} \vdash \lnot G$. This contradicts the consistency of $\mathcal{F}$. Therefore: $$\mathcal{F} \nvdash G$$

Step 6 — $G$ is not refutable (assuming $\omega$-consistency). Suppose $\mathcal{F} \vdash \lnot G$, i.e., $\mathcal{F} \vdash \text{Pvbl}(\ulcorner G \urcorner)$. This says $\mathcal{F}$ asserts $G$ has a proof. But no such proof exists (Step 5). So for each standard number $n$, $\mathcal{F} \vdash \lnot\widehat{\text{Prf}}(\bar{n}, \ulcorner G \urcorner)$. Under $\omega$-consistency, $\mathcal{F}$ cannot also prove $\exists x\, \widehat{\text{Prf}}(x, \ulcorner G \urcorner)$. But that is $\text{Pvbl}(\ulcorner G \urcorner)$. Contradiction. Therefore: $$\mathcal{F} \nvdash \lnot G$$

Step 7 — Conclusion. $G$ is undecidable in $\mathcal{F}$. $\mathcal{F}$ is incomplete. And since $G$ says "I am not provable" and $G$ is indeed not provable, $G$ is true. $\blacksquare$

Tarski's Undefinability Theorem (1933)

Theorem — Tarski's Undefinability of Truth

There is no formula $\text{True}(x)$ in the language of arithmetic such that for every sentence $\phi$: $$\text{PA} \vdash \phi \Leftrightarrow \text{True}(\ulcorner \phi \urcorner)$$ In other words: arithmetic truth is not arithmetically definable.

Proof (via Diagonal Lemma)

If $\text{True}(x)$ existed, apply the Diagonal Lemma to $\lnot \text{True}(x)$ to obtain $\lambda$ with $\lambda \Leftrightarrow \lnot\text{True}(\ulcorner\lambda\urcorner)$. This says "$\lambda$ is true iff $\lambda$ is not true" — a formal contradiction. $\square$

§ 10 — Interactive

Demo: Gödel Number Calculator

Compute the Gödel number of a sequence using prime encoding. Enter comma-separated values $(a_1, a_2, \ldots, a_n)$ and compute $\prod p_i^{a_i}$.

⟨a₁, a₂, …, aₙ⟩ → 2^a₁ · 3^a₂ · 5^a₃ · …

Sequence (comma-separated integers, max 12 terms)

Enter a sequence and press Compute.

Try encoding the formula $S(0)=S(0)$ using codes: $S$→2, $(→9$, $0$→1, $)→10$, $=$→5. Sequence: 2, 9, 1, 10, 5, 2, 9, 1, 10

§ 11 — Interactive

Demo: Proof Stepper

Walk through the proof of the First Incompleteness Theorem step by step.

Step 1 / 8

§ 12 — Interactive

Demo: Formal Deduction Explorer

Simulate a tiny propositional logic system. Enter two premises and a conclusion — the system checks if the conclusion follows by modus ponens or conjunction introduction.

Mini Propositional Proof Checker

Premise 1 (proposition)

Premise 2 (proposition or P→Q)

Desired conclusion

Enter premises and conclusion, then click Check.

Truth Table Generator

Formula (use P, Q, R; operators: &, |, !, →, ↔)

§ 13 — Interactive

Demo: Liar Paradox → Gödel Sentence

Explore the relationship between the Liar Paradox and Gödel's self-referential sentence.

Liar Paradox vs. Gödel Sentence Comparison

Select a sentence type and press Analyze.

§ 14 — GNU Octave

GNU Octave: Prime Factorization Utilities

Gödel numbering relies on the Fundamental Theorem of Arithmetic. Here are Octave functions for working with primes — the backbone of Gödel encoding.

GNU Octave prime_tools.m — Prime number utilities

% ============================================================
%  prime_tools.m  —  Prime utilities for Gödel numbering
%  GNU Octave 8.x
% ============================================================

%% 1. List the first N primes
function P = first_n_primes(n)
  % Returns a row vector of the first n primes
  P = zeros(1, n);
  count = 0;
  k = 2;
  while count < n
    if isprime(k)
      count = count + 1;
      P(count) = k;
    end
    k = k + 1;
  end
end

%% 2. Prime factorization (returns exponents indexed by prime)
function [primes_list, exponents] = factorize(n)
  % Returns prime factors and their exponents
  % Example: factorize(600) → primes=[2,3,5], exps=[3,1,2]
  primes_list = [];
  exponents   = [];
  d = 2;
  while d * d <= n
    if mod(n, d) == 0
      e = 0;
      while mod(n, d) == 0
        e = e + 1;
        n = n / d;
      end
      primes_list(end+1) = d;
      exponents(end+1)   = e;
    end
    d = d + 1;
  end
  if n > 1
    primes_list(end+1) = n;
    exponents(end+1)   = 1;
  end
end

%% 3. Verify the factorization visually
function print_factorization(n)
  [ps, es] = factorize(n);
  fprintf('%d = ', n);
  for i = 1:length(ps)
    if i > 1, fprintf(' × '); end
    if es(i) == 1
      fprintf('%d', ps(i));
    else
      fprintf('%d^%d', ps(i), es(i));
    end
  end
  fprintf('\n');
end

%% ── DEMO ──────────────────────────────────────────────
fprintf('First 12 primes: ');
disp(first_n_primes(12))

print_factorization(600);    % → 600 = 2^3 × 3 × 5^2
print_factorization(2310);   % → 2310 = 2 × 3 × 5 × 7 × 11
print_factorization(30030);  % → product of first 6 primes

% Verify uniqueness: different sequences → different Gödel numbers
assert(2^3 * 3^1 * 5^2 == 600);  % seq [3,1,2]
assert(2^1 * 3^3 * 5^2 ~= 600);  % seq [1,3,2] — different
fprintf('Uniqueness assertion passed.\n');

Expected Output

First 12 primes: 2  3  5  7  11  13  17  19  23  29  31  37
600 = 2^3 × 3 × 5^2
2310 = 2 × 3 × 5 × 7 × 11
30030 = 2 × 3 × 5 × 7 × 11 × 13
Uniqueness assertion passed.

§ 15 — GNU Octave

GNU Octave: Full Gödel Encoding System

GNU Octave godel_encoding.m — Encode and decode sequences

% ============================================================
%  godel_encoding.m — Gödel Number Encoding / Decoding
%  Demonstrates the bijection between sequences and numbers
%  via prime power encoding.
%  GNU Octave 8.x
% ============================================================

%% Compute Gödel number of a sequence a = [a1, a2, ..., an]
function g = godel_number(a)
  % g = 2^a1 * 3^a2 * 5^a3 * ... * p_n^an
  primes = first_n_primes(length(a));
  g = 1;
  for i = 1:length(a)
    g = g * primes(i)^a(i);
  end
end

%% Decode a Gödel number back to its sequence
function seq = godel_decode(g)
  % Extract exponents from prime factorization
  seq = [];
  d   = 2;
  while g > 1
    if isprime(d) && mod(g, d) == 0
      e = 0;
      while mod(g, d) == 0
        e = e + 1;
        g = g / d;
      end
      seq(end+1) = e;
    elseif ~isprime(d)
      d = d + 1;
      continue
    end
    d = d + 1;
  end
end

%% Encode a string formula using our symbol table
function code = encode_symbol(sym)
  % Symbol → code number mapping
  symbols = {'0', 'S', '+', '*', '=', '~', '->', 'A', '(', ')'};
  codes   = [1,  2,   3,   4,   5,   6,   7,          8,   9,   10];
  idx = strcmp(symbols, sym);
  if any(idx)
    code = codes(find(idx, 1));
  else
    % Variables v1, v2, … get codes 11, 12, …
    if length(sym) > 1 && sym(1) == 'v'
      code = 10 + str2num(sym(2:end));
    else
      code = -1;  % Unknown symbol
    end
  end
end

%% Encode a cell array of symbols into one Gödel number
function g = encode_formula(formula_cell)
  codes = cellfun(@encode_symbol, formula_cell);
  g = godel_number(codes);
  fprintf('Formula: ');
  fprintf('%s ', formula_cell{:});
  fprintf('\n');
  fprintf('Codes:   ');
  fprintf('%d ', codes);
  fprintf('\n');
  fprintf('Gödel#:  %g\n\n', g);
end

%% ── DEMO ──────────────────────────────────────────────
fprintf('=== Gödel Encoding Demo ===\n\n');

% Basic sequence encoding
seq1 = [3, 1, 2];
g1   = godel_number(seq1);
fprintf('Sequence [3,1,2] → Gödel# = %d\n', g1);
decoded = godel_decode(g1);
fprintf('Decoded back: ['); fprintf('%d ', decoded); fprintf(']\n\n');

% Encoding the formula: S(0) = S(0)  (i.e., 1 = 1)
% Symbols: S ( 0 ) = S ( 0 )
fprintf('Encoding formula: S(0) = S(0)\n');
g_formula = encode_formula({'S', '(', '0', ')', '=', 'S', '(', '0', ')'});

% Encoding the formula: 0 = 0
fprintf('Encoding formula: 0 = 0\n');
encode_formula({'0', '=', '0'});

% Roundtrip test
for trial = 1:5
  seq = randi(8, 1, randi([2,5]));
  g   = godel_number(seq);
  seq2 = godel_decode(g);
  ok = isequal(seq, seq2);
  fprintf('Roundtrip test %d: seq=[%s] → %g → [%s] %s\n', ...
    trial, num2str(seq), g, num2str(seq2), ...
    ifelse(ok, '✓', '✗'));
end

§ 16 — GNU Octave

GNU Octave: Peano Arithmetic Simulator

Simulate a simplified version of Peano Arithmetic: define successor, addition, and multiplication purely via the Peano axioms — using only recursion, no built-in arithmetic operators.

GNU Octave peano_arithmetic.m — PA from scratch

% ============================================================
%  peano_arithmetic.m — Peano Arithmetic from axioms
%  Addition and multiplication built purely from S and 0.
%  GNU Octave 8.x
% ============================================================

%% Successor function: S(n) = n + 1
function y = S(x)
  y = x + 1;  % In Octave, integers model ℕ
end

%% Zero predicate: PA1 — S(x) ≠ 0, so 0 has no predecessor
function r = is_zero(x)
  r = (x == 0);
end

%% PA3 & PA4: Addition via recursion
%  x + 0 = x
%  x + S(y) = S(x + y)
function result = pa_add(x, y)
  if is_zero(y)
    result = x;                      % PA3: x + 0 = x
  else
    result = S(pa_add(x, y - 1));  % PA4: x + S(y-1) = S(x + (y-1))
  end
end

%% PA5 & PA6: Multiplication via recursion
%  x * 0 = 0
%  x * S(y) = (x * y) + x
function result = pa_mul(x, y)
  if is_zero(y)
    result = 0;                              % PA5: x * 0 = 0
  else
    result = pa_add(pa_mul(x, y-1), x);  % PA6: x*S(y) = (x*y)+x
  end
end

%% PA7 (schema): Induction principle validator
%  Verifies: φ(0) ∧ ∀n(φ(n)→φ(S(n))) ⟹ ∀n≤N φ(n)
function result = pa_induction(phi, N)
  % phi: function handle, phi(n) returns true/false
  % Checks base case and inductive step up to N
  if ~phi(0)
    result = false;
    fprintf('  Base case φ(0) fails!\n');
    return;
  end
  for n = 0:N-1
    if phi(n) && ~phi(S(n))
      result = false;
      fprintf('  Inductive step fails at n=%d!\n', n);
      return;
    end
  end
  result = true;
end

%% ── DEMO ──────────────────────────────────────────────
fprintf('=== Peano Arithmetic Demo ===\n\n');

% Test addition
fprintf('Addition (Peano axioms PA3/PA4):\n');
for a = [0,1,2,3,5]
  for b = [0,1,3,4]
    computed = pa_add(a, b);
    expected = a + b;
    ok = strcmp(mat2str(computed == expected), '1');
    fprintf('  pa_add(%d,%d) = %d  [expected %d]  %s\n', ...
      a, b, computed, expected, ifelse(ok, '✓', '✗'));
  end
end

% Test multiplication
fprintf('\nMultiplication (Peano axioms PA5/PA6):\n');
for a = [0,1,2,3,4]
  for b = [0,1,2,3]
    computed = pa_mul(a, b);
    fprintf('  pa_mul(%d,%d) = %d\n', a, b, computed);
  end
end

% Test induction principle on several predicates
fprintf('\nInduction verification (PA7 schema):\n');
N = 20;

% φ(n): n + 0 = n  (PA3 expressed as predicate)
phi1 = @(n) (pa_add(n, 0) == n);
fprintf('  φ(n): n+0=n    → induction holds to %d: %d\n', N, pa_induction(phi1, N));

% φ(n): 0 + n = n  (commutativity of zero — needs proof)
phi2 = @(n) (pa_add(0, n) == n);
fprintf('  φ(n): 0+n=n    → induction holds to %d: %d\n', N, pa_induction(phi2, N));

% φ(n): n*(n+1) is always even  (a classic induction result)
phi3 = @(n) (mod(pa_mul(n, S(n)), 2) == 0);
fprintf('  φ(n): n(n+1) even → induction holds to %d: %d\n', N, pa_induction(phi3, N));

% φ(n): FAILS — n > 5 (base case fails)
phi4 = @(n) (n > 5);
fprintf('  φ(n): n>5 (should fail):\n');
pa_induction(phi4, N);

§ 17 — GNU Octave

GNU Octave: Fixed-Point & Proof Predicate

Simulate the Diagonal Lemma and Gödel sentence construction computationally.

GNU Octave godel_sentence.m — Fixed-point construction

% ============================================================
%  godel_sentence.m — Computational model of the Diagonal Lemma
%  and the Gödel sentence.
%
%  We work with a FINITE toy formal system (propositional logic)
%  and show how self-reference arises.
%  GNU Octave 8.x
% ============================================================

%% A tiny "formula" is represented as a struct:
%  .type: 'atom', 'not', 'implies', 'provable', 'self_ref'
%  .code: Gödel number (integer)
%  .left, .right: subformulas (for binary connectives)

%% Simulated provability predicate for our toy system
% Our axiom set (stored as Gödel numbers that are "provable")
AXIOMS = [2, 4, 6, 8, 10, 12];  % toy axioms

function result = is_provable(gnum, axioms)
  % Toy: a formula is "provable" iff its Gödel number is even
  %       (just for demonstration of self-reference structure)
  result = any(axioms == gnum) || (mod(gnum, 2) == 0 && gnum > 0);
end

%% Substitution function (toy): sub(φ, x, t)
%  In our model: replace the "argument slot" in φ with t
%  Returns the Gödel number of the resulting formula
function g_new = substitute(g_phi, g_t)
  % Toy substitution: φ(x)[x←t] encoded as g_phi * prime(g_t)
  % (In real PA this is a primitive recursive function)
  primes = [2,3,5,7,11,13,17,19,23,29];
  idx = min(g_t, length(primes));
  g_new = g_phi * primes(idx);  % encoding the substitution
end

%% The diagonal/diagonalization function
%  diag(φ) = φ(⌜φ⌝) — apply φ to its own Gödel number
%  In toy terms: substitute the Gödel number of φ into φ itself
function g_diag = diagonalize(g_phi)
  % sub(φ, x, ⌜φ⌝) — plug φ's own code into φ
  g_diag = substitute(g_phi, g_phi);
  fprintf('  diag(%d) = %d\n', g_phi, g_diag);
end

%% Construct the Gödel sentence for φ(x) = ¬Provable(x)
%  The Gödel sentence G satisfies: G ↔ ¬Provable(⌜G⌝)
function G = construct_godel_sentence(g_phi_not_pvbl, axioms)
  fprintf('Constructing Gödel sentence...\n');
  fprintf('  ¬Pvbl formula code: %d\n', g_phi_not_pvbl);
  
  % The Gödel sentence is: diag(¬Pvbl)
  G = diagonalize(g_phi_not_pvbl);
  
  fprintf('  Gödel sentence G has code: %d\n', G);
  pvbl_G = is_provable(G, axioms);
  fprintf('  G says "I am not provable"\n');
  fprintf('  Is G provable in our toy system? %s\n', ...
    ifelse(pvbl_G, 'YES — inconsistency!', 'NO  — consistent ✓'));
  
  % Verify G is undecidable: not provable AND not refutable
  fprintf('  Is ¬G provable? %s\n', ...
    ifelse(is_provable(G+1, axioms), 'YES', 'NO ✓'));
end

%% ── DEMO ──────────────────────────────────────────────
fprintf('=== Fixed-Point (Diagonal Lemma) Demo ===\n\n');

% In our toy system: "¬Provable(x)" has code 7 (odd = unprovable)
g_not_pvbl = 7;
G = construct_godel_sentence(g_not_pvbl, AXIOMS);

fprintf('\n--- Interpretation of Results ---\n');
fprintf('G (code %d) states: "Formula %d is not provable"\n', G, G);
fprintf('Since G''s code is ODD, our toy system cannot prove G.\n');
fprintf('So G says "I am unprovable" AND is indeed unprovable.\n');
fprintf('G is TRUE but UNPROVABLE — exactly the Gödel sentence!\n\n');

%% Show multiple diagonalizations
fprintf('Diagonalization of various formulas:\n');
for g = [3, 5, 7, 9, 11]
  g_d = diagonalize(g);
  pvbl = is_provable(g_d, AXIOMS);
  fprintf('    Formula %2d → diag = %4d → provable: %s\n', ...
    g, g_d, ifelse(pvbl, 'yes', 'no'));
end

fprintf('\n=== Consistency Check ===\n');
% A consistent system: no formula and its negation are both provable
consistent = true;
for n = 1:50
  if is_provable(n, AXIOMS) && is_provable(n+1, AXIOMS)
    % In toy: treat n and n+1 as "formula" and "¬formula"
    % (very simplified encoding)
    consistent = false;
    fprintf('Inconsistency found at n=%d!\n', n);
    break;
  end
end
if consistent
  fprintf('System appears consistent (no φ and ¬φ both provable)\n');
end

GNU Octave primitive_recursive.m — Show Prf(x,y) is primitive recursive

% ============================================================
%  primitive_recursive.m
%  Demonstrate that the proof-checking predicate is primitive
%  recursive (computable by bounded loops, no unbounded search).
%  GNU Octave 8.x
% ============================================================

%% Primitive recursive functions — building blocks
%  (Following the standard definition)

% Zero function: Z(x) = 0
function y = Z(x),  y = 0;  end

% Successor: Succ(x) = x + 1
function y = Succ(x),  y = x + 1;  end

% Projection: P_i^n(x1,...,xn) = xi
function y = Proj(xs, i),  y = xs(i);  end

%% Bounded minimization (mu-operator with bound)
%  min{y ≤ b : R(y, x)} — primitive recursive when R is
function y = bounded_min(R, b, x)
  for y = 0:b
    if R(y, x), return; end
  end
  y = b + 1;  % Not found
end

%% Bounded quantifiers — both primitive recursive
function r = bounded_exists(R, b, x)
  r = any(arrayfun(@(y) R(y,x), 0:b));
end

function r = bounded_forall(R, b, x)
  r = all(arrayfun(@(y) R(y,x), 0:b));
end

%% Simulation: checking if a "proof sequence" is valid
% In our toy: a "proof" is a vector of formulas where each
% formula is either an axiom (even) or follows from previous
% by modus ponens (simplified rule)

function valid = check_proof(proof_seq, axioms)
  % proof_seq: vector of formula codes
  % Each step is valid if it's an axiom OR follows from two prior steps
  valid = true;
  for i = 1:length(proof_seq)
    step = proof_seq(i);
    is_ax = any(axioms == step);
    % Toy modus ponens: step follows from steps j,k if step = j+k (toy)
    follows = false;
    if i >= 3
      for j = 1:i-1
        for k = 1:i-1
          if j ~= k && proof_seq(j) + proof_seq(k) == step
            follows = true;
          end
        end
      end
    end
    if ~is_ax && ~follows
      fprintf('  Step %d (formula %d): INVALID\n', i, step);
      valid = false;
    else
      fprintf('  Step %d (formula %d): valid (%s)\n', i, step, ...
        ifelse(is_ax, 'axiom', 'inferred'));
    end
  end
end

%% ── DEMO ──────────────────────────────────────────────
AXIOMS = [2, 4, 6, 8];

fprintf('Proof check 1 (valid): [2, 4, 6]\n');
check_proof([2, 4, 6], AXIOMS);

fprintf('\nProof check 2 (uses modus ponens): [2, 4, 6]\n');
% 2+4=6, so 6 follows from 2 and 4 by our toy rule
check_proof([2, 4, 6], AXIOMS);

fprintf('\nProof check 3 (invalid step): [2, 4, 7]\n');
% 7 is neither an axiom nor the sum of any two prior steps
check_proof([2, 4, 7], AXIOMS);

fprintf('\nKey insight: Prf(x,y) involves only BOUNDED loops\n');
fprintf('over steps in the proof — hence PRIMITIVE RECURSIVE.\n');
fprintf('This allows PA to express and reason about its own proofs.\n');

§ 18

Hilbert's Programme & Its Destruction

Hilbert's Goals (1920s)

Formalization: All of mathematics expressed as formal symbols.
Completeness: Every true statement provable from the axioms.
Consistency: A finite proof that no contradiction exists.
Decidability: An algorithm to determine any mathematical truth (the Entscheidungsproblem).

What Gödel (and Turing) Destroyed

Goal	Killed by
Completeness	First Incompleteness Theorem
Finitary Consistency proof	Second Incompleteness Theorem
Decidability	Turing (1936) — Halting Problem
Formalization (universal)	Both theorems combined

Von Neumann's Reaction

John von Neumann — who was present at the 1930 Königsberg conference where Gödel announced his result — immediately recognized the significance and wrote to Gödel that same day. He told colleagues: "It's all over."

Löb's Theorem (1955)

Theorem — Löb's Theorem

For any sentence $\phi$: $$\text{PA} \vdash \text{Pvbl}(\ulcorner\phi\urcorner) \Rightarrow \phi \quad\Longleftrightarrow\quad \text{PA} \vdash \phi$$ In words: PA can prove "if $\phi$ is provable then $\phi$" only when PA can already prove $\phi$ outright.

This is a kind of converse to the Second Incompleteness Theorem, and shows PA is rightly "modest" about its own power.

Turing and Computability

Alan Turing's 1936 paper on computability (and the Halting Problem) is deeply related. Turing proved:

Theorem — Undecidability of the Halting Problem

There is no algorithm $H$ such that, given any program $P$ and input $x$, $H(P,x)$ correctly determines whether $P$ halts on $x$.

The connection: Gödel's Incompleteness Theorems can be re-derived from the unsolvability of the Halting Problem. Both are facets of a single profound limitation: sufficiently expressive systems cannot fully describe themselves.

§ 19

Impact, Misinterpretations & Legacy

What Incompleteness Does NOT Say

Common Misinterpretations

NOT: "Mathematics is broken or inconsistent." Incompleteness says there are truths we cannot prove — not that what we can prove is wrong.
NOT: "Human minds transcend formal systems." (Penrose's argument in The Emperor's New Mind is widely contested.)
NOT: A limitation on science, knowledge, or human achievement generally.
NOT: Every true statement is unprovable. Only some are.

What It Does Say

Correct Interpretations

No formal system can be simultaneously consistent, complete, and capable of expressing basic arithmetic.
Mathematical truth is richer than any single formal system can capture.
There are specific true arithmetic statements (like Con(PA)) that PA cannot prove.
Certainty in mathematics must come from outside any fixed formal system — there is no ultimate foundation.

Legacy Across Disciplines

Mathematics

Spurred the development of proof theory, model theory, reverse mathematics (which axioms are really needed?), and large cardinal axioms.

Computer Science

Directly inspired Turing's computability theory, the Church-Turing thesis, complexity theory, and the theory of undecidable problems.

Philosophy

Challenged logicism (Russell), formalism (Hilbert), and contributed to the philosophy of mind debate about artificial intelligence and consciousness.

Gödel's Other Major Contributions

Result	Year	Significance
Completeness Theorem	1929	First-order logic is complete; semantic ↔ syntactic
Incompleteness Theorems	1931	Fundamental limits of formal arithmetic
Consistency of AC & GCH	1940	Axiom of Choice and Generalized Continuum Hypothesis consistent with ZF
Rotating Universe solution	1949	Exact solution to Einstein's field equations; time travel in GR
Ontological argument	1970s	Formal modal logic proof of God's existence (philosophical curiosity)

§ 20

References & Further Reading

Primary Sources

Gödel, K. (1931). Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik.
Gödel, K. (1929). Über die Vollständigkeit des Logikkalküls. (Doctoral dissertation, University of Vienna.)
Rosser, J.B. (1936). Extensions of some theorems of Gödel and Church. Journal of Symbolic Logic.

Recommended Books

Nagel & Newman — Gödel's Proof (accessible introduction)
Hofstadter — Gödel, Escher, Bach (broad exploration)
Smullyan — Gödel's Incompleteness Theorems (rigorous)
Franzén — Gödel's Theorem: An Incomplete Guide to Its Use and Abuse
Boolos, Burgess & Jeffrey — Computability and Logic
Enderton — A Mathematical Introduction to Logic

This document covers: Peano Arithmetic, formal systems, Gödel numbering, the Diagonal Lemma, First and Second Incompleteness Theorems, Tarski's Undefinability, Rosser's extension, Löb's Theorem, Hilbert's Programme, and connections to computability. GNU Octave code provided for educational simulation of the core concepts. All theorems stated rigorously; proof sketches follow standard presentations in mathematical logic.