Part X: Metamathematics — Proof Theory and Model Theory

Metamathematics turns mathematical tools on mathematics itself. Gödel's incompleteness theorems are the central results: they show that any sufficiently expressive formal system has true statements it cannot prove.

10.1 Gödel's Incompleteness Theorems (1931)

Setting: A formal system is consistent if it proves no contradiction; complete if it proves or refutes every sentence in its language.

First Incompleteness Theorem: Any consistent formal system F that is strong enough to express basic arithmetic (Peano arithmetic, or any extension) is incomplete: there exists a sentence G_F — the Gödel sentence — that is true but unprovable in F.

Construction: Gödel encoding assigns a natural number to every formula and proof. The Gödel sentence G_F asserts "G_F is not provable in F." If F proved G_F, F would prove a false statement — contradiction. If F disproved G_F, G_F would be provable — contradiction. So neither.

Second Incompleteness Theorem: F cannot prove its own consistency (assuming it is consistent). The statement "F is consistent" is another unprovable truth.

Significance: Hilbert's program — formalizing all of mathematics and proving the system complete and consistent — is impossible. There is no finite set of axioms from which all mathematical truths follow. Mathematics is inexhaustible.

10.2 Model Theory

Model: A structure M satisfying a set of sentences Γ.

Elementary equivalence: M ≡ N if M and N satisfy the same first-order sentences.

Compactness and Löwenheim-Skolem (restatement): Non-standard models of arithmetic exist — models where all the first-order theorems of ℕ hold, but that contain "infinite" natural numbers. These are not ℕ but are indistinguishable from it by first-order sentences.

Quantifier elimination: A theory T admits quantifier elimination if every formula is equivalent in T to a quantifier-free formula. This often implies decidability. Examples: the theory of dense linear orders (ℚ, ≤), real closed fields, algebraically closed fields.

Morley's Theorem (1965): If a first-order theory is categorical in some uncountable cardinal (has exactly one model of that cardinality up to isomorphism), it is categorical in all uncountable cardinals.

10.3 Proof Theory

Proof theory studies proofs as mathematical objects — their structure, strength, and relationships.

Consistency strength: The hierarchy of formal systems by what they can prove consistent. ZFC can prove the consistency of PA; stronger large cardinal axioms can prove the consistency of ZFC.

Cut elimination (Gentzen, 1934): Any proof in the sequent calculus can be transformed into a "cut-free" proof — one that doesn't use the cut rule (modus ponens equivalent). This makes proofs transparent and is fundamental in proof search.

Proof complexity: Studies the lengths of proofs in various proof systems. Short proofs may not exist for certain tautologies in certain systems — this is related to P vs. NP.

---