Proof theory - Advanced Proof-Theoretic Methods

Proof Theory: Provability, Ordinals, Interpretations, and Reverse Mathematics Proof theory explores the foundations of mathematical reasoning by studying what can be proven within formal systems. This guide covers four major areas that connect how we formalize provability, measure the strength of theories, translate between logical frameworks, and classify theorems by their logical prerequisites. Provability Logic and the Gödel-Löb System What is Provability Logic? Provability logic is a modal logic—a system of reasoning about possibility and necessity—where the box operator $\Box$ is interpreted as "it is provable that." This allows us to reason formally about what can and cannot be proven within mathematical systems. The most important provability logic is GL (Gödel-Löb modal logic), which precisely captures how provability works in Peano arithmetic, the standard formal system for number theory. The Core Axioms GL is built from modal versions of the Hilbert-Bernays derivability conditions, which are technical properties about how provability behaves. The most distinctive axiom is Löb's theorem: if you can prove that "the provability of statement A implies A itself," then you can prove A directly. Written formally: $\Box (\Box A \to A) \to \Box A$ This might seem strange at first, but it captures an important insight: if a statement is self-supporting in the right way through provability, it must actually be true. Connection to Incompleteness Here's a remarkable fact: the statement "a contradiction is not provable implies that we cannot prove that a contradiction is not provable" formalizes Gödel's second incompleteness theorem. This theorem says that no consistent formal system can prove its own consistency—a profound limitation on what mathematics can do for itself. Solovay's Completeness Theorem Robert Solovay proved that GL is complete with respect to Peano arithmetic. This means: Every valid principle of provability in Peano arithmetic is a theorem of GL Every theorem of GL holds true when we interpret the box operator as provability in Peano arithmetic Crucially, this makes propositional reasoning about provability both complete (we can derive exactly the right theorems) and decidable (we can computationally check whether something is a theorem). <extrainfo> First-Order Extensions Researchers have extended provability logic to first-order languages, studying modal predicates about provability. This adds complexity but allows reasoning about provability of statements with quantifiers. </extrainfo> Ordinal Analysis: Measuring Consistency Through Ordinals The Basic Idea Ordinal analysis is a technique for proving that formal systems are consistent using a clever workaround to Gödel's incompleteness theorem. The key insight is this: if a theory T is consistent, then instead of proving "T is consistent" (which T cannot do by incompleteness), we can prove in a weaker system that "T is consistent provided that a certain transfinite ordinal is well-founded." A transfinite ordinal is a generalization of natural numbers that extends beyond infinity in a structured way. A key example is $\varepsilon0$ (epsilon-zero), which is the first ordinal where $\omega^\varepsilon0 = \varepsilon0$ (where $\omega$ is the first infinite ordinal). How It Works For a recursively axiomatized (computer-listable) consistent theory T: Identify a specific transfinite ordinal $\alpha$ associated with T Prove in finitary arithmetic: "If $\alpha$ is well-founded, then T is consistent" The ordinal $\alpha$ is chosen so that T itself cannot prove that $\alpha$ is well-founded (by incompleteness) This gives an "ordinal analysis" of T: the ordinal $\alpha$ measures how strong T is. Major Applications Ordinal analysis yields several important results: Consistency proofs: It provides relative consistency proofs showing that classical theories (like classical analysis) are consistent relative to constructive theories Independence results: It produces combinatorial statements that are independent of various theories Function classification: It classifies which recursive functions can be proven total within a given theory, and which ordinals a theory can prove well-founded Historical Foundation <extrainfo> Gerhard Gentzen proved the consistency of Peano arithmetic by showing that Peano arithmetic is consistent if the ordinal $\varepsilon0$ is well-founded. This was the first major success of ordinal analysis. Since then, the technique has been extended to many fragments of first-order and second-order arithmetic and to set theory. </extrainfo> Functional Interpretations: Translating Between Logical Systems The Two-Stage Process Functional interpretation is a technique that translates theorems from one logical framework to another, allowing us to extract constructive information from classical proofs. The process works in two stages: Stage 1: Classical to Intuitionistic A classical theory C (which uses classical logic) is reduced to an intuitionistic theory I (which uses constructive logic). This is done by providing a constructive translation of every theorem of C into a theorem of I. This is significant because intuitionistic logic is "constructive"—it doesn't allow the law of excluded middle ($A \lor \neg A$), which means proofs must explicitly construct witnesses rather than merely asserting existence. Stage 2: Intuitionistic to Quantifier-Free Functionals The intuitionistic theory I is then reduced to a quantifier-free theory F of functionals (higher-type functions). A functional is essentially a function that can take functions as inputs and return values as outputs. What This Achieves Functional interpretations give us powerful tools: Consistency proofs: They prove that classical theories are consistent relative to constructive theories Extracting information: They enable extraction of explicit constructive information (like algorithms) from proofs in classical systems Representing functions: If a recursive function's totality is provable in I or C, then that function is represented by an explicit term in F The second point is particularly powerful: it means that classical mathematical proofs can be converted into algorithms we can actually run. Historical Origin and Application <extrainfo> Kurt Gödel developed the Dialectica interpretation, which translates intuitionistic arithmetic into a quantifier-free theory of finite-type functionals. When combined with the double-negation translation (which converts classical logic into intuitionistic logic), the Dialectica interpretation reduces classical arithmetic to intuitionistic arithmetic with functional terms. </extrainfo> Reverse Mathematics: Classifying Theorems by Strength The Framework Reverse mathematics investigates the logical strength of mathematical theorems by asking: "What axioms does a theorem really need?" Here's how it works: Start weak: Begin with a weak base theory (call it B) that can formalize the statements you care about but cannot prove them Find a sufficient system: For a theorem T you want to analyze, find a stronger axiom system S that does prove T Prove both directions: Show that S proves T (this is straightforward) Show the "reverse": that T implies S (this is the key step) When both directions hold, we say that T and S are equivalent over the base theory. This reveals that T is exactly as strong as S—they require the same logical power. The Big Five Systems A remarkable discovery in reverse mathematics is that almost every "natural" mathematical theorem is equivalent to one of exactly five axiom systems over the base theory RCA₀ (Recursive Comprehension Axiom): RCA₀ (Recursive Comprehension Axiom) — the base theory itself WKL₀ (Weak König's Lemma) — a system slightly stronger than RCA₀ ACA₀ (Arithmetical Comprehension Axiom) — intermediate strength ATR₀ (Arithmetical Transfinite Recursion) — allowing recursion along well-founded ordinals Π₁₁-CA₀ (Π₁₁-Comprehension Axiom) — the strongest of the five These are ordered by strength: RCA₀ ⊂ WKL₀ ⊂ ACA₀ ⊂ ATR₀ ⊂ Π₁₁-CA₀. The surprising fact is that theorems from across mathematics—from calculus to combinatorics to analysis—cluster around these five systems. This suggests something deep about the logical structure of mathematics itself.