Proof theory Study Guide

📖 Core Concepts Proof Theory – Treats proofs as formal syntactic objects (lists, trees) that can be mathematically analyzed. Contrasts with model theory (semantic). Structural Proof Theory – Studies the form of proof calculi (Hilbert, natural deduction, sequent) and transformations such as cut‑elimination. Cut‑Free / Analytic Proof – A proof in the sequent calculus that contains no cut rule; enjoys the subformula property (every formula appearing is a sub‑formula of the end‑sequent). Ordinal Analysis – Shows that the well‑foundedness of a specific transfinite ordinal (e.g., ε₀) implies the consistency of a theory \(T\). Provability Logic (GL) – Modal logic with □ meaning “it is provable that”. Captures the Hilbert‑Bernays derivability conditions and Löb’s theorem. Reverse Mathematics – Works inside a weak base theory; isolates the minimal axiom system \(S\) needed to prove a theorem \(T\) and proves the reversal \(T \Rightarrow S\). Functional Interpretation – Two‑stage reduction: classical theory \(C \rightarrow\) intuitionistic theory \(I \rightarrow\) quantifier‑free functional theory \(F\) (e.g., Gödel’s Dialectica). Curry–Howard Correspondence – Identifies natural‑deduction normalisation with β‑reduction in the simply‑typed λ‑calculus; bridges proofs and programs. Formal vs. Informal Proofs – Formal proofs are machine‑checkable; informal proofs are high‑level sketches that need expert reconstruction. --- 📌 Must Remember Cut‑Elimination Theorem → Guarantees existence of cut‑free (analytic) proofs; yields subformula property. Gentzen’s Consistency Proof – Uses transfinite induction up to ε₀ to prove PA’s consistency. GL Axioms – □(□A → A) → □A (Löb’s axiom) + standard modal K axioms + necessitation. Big Five of Reverse Mathematics (in increasing strength): RCA₀ ⊂ WKL₀ ⊂ ACA₀ ⊂ ATR₀ ⊂ Π₁¹‑CA₀. Dialectica Interpretation – Translates classical arithmetic into a quantifier‑free theory of finite‑type functionals. Gödel’s Second Incompleteness – No sufficiently strong ω‑consistent theory can prove its own consistency; reflected in GL as “□¬⊥ → ¬□¬⊥”. Subformula Property – If a sequent is derivable cut‑free, every formula is a subformula of the end‑sequent. --- 🔄 Key Processes Cut‑Elimination (Gentzen) Identify a cut inference. Replace it by a series of reduction steps that push the cut upwards (using permutation of rules). Iterate until no cuts remain → cut‑free proof. Ordinal Analysis for a Theory \(T\) Choose a suitable ordinal notation system (e.g., ε₀ for PA). Formalise transfinite induction up to that ordinal in a weak arithmetic. Prove: Well‑foundedness of the ordinal ⇒ Con(T). Reverse Mathematics Procedure Work in a weak base theory (RCA₀). Show \(S \vdash T\) (forward direction). Inside the base theory, prove \(T \vdash S\) (reversal). Functional Interpretation (Dialectica) Apply double‑negation translation to turn classical proofs into intuitionistic ones. Translate intuitionistic formulas into quantifier‑free statements about functionals. Extract explicit witnessing functions from the resulting proof. Provability Logic Derivation (GL) Encode statements about provability as □A. Use Löb’s axiom □(□A → A) → □A to derive consequences such as Gödel’s second incompleteness. --- 🔍 Key Comparisons Hilbert Calculus vs. Natural Deduction vs. Sequent Calculus Hilbert: Few inference rules, many axioms; good for metatheoretic studies. Natural Deduction: Introduction/Elimination rules mirror logical meaning; normal forms ↔ analytic proofs. Sequent Calculus: Symmetric, explicit cut rule; facilitates cut‑elimination and subformula property. Formal Proof vs. Informal Proof Formal: Machine‑checkable, step‑by‑step, no ambiguity. Informal: Sketches, relies on reader’s expertise, may hide gaps. Ordinal Analysis vs. Functional Interpretation Ordinal Analysis: Uses transfinite induction to prove consistency. Functional Interpretation: Translates proofs to constructive functionals, extracting computational content. Provability Logic (GL) vs. Ordinary Modal Logic (K) GL: Includes Löb’s axiom, captures arithmetic provability. K: Only □(A → B) → (□A → □B); lacks arithmetic-specific principles. --- ⚠️ Common Misunderstandings “Cut‑elimination makes proofs shorter.” – It often lengthens proofs dramatically; the key is the subformula property, not brevity. “Ordinal ε₀ is a number.” – It is a notation system for a transfinite ordinal, not a finite value. “Provability logic proves arithmetic theorems.” – GL is sound and complete for the modal theory of provability; it does not directly prove arithmetic statements. “Reverse mathematics shows every theorem needs the strongest system.” – Most theorems fall into one of the Big Five; many are provable in weak subsystems. “Formal proof = automatically found proof.” – Finding a proof (automated theorem proving) is hard; checking a formal proof is easy. --- 🧠 Mental Models / Intuition Proofs as Trees – Visualise a proof as a branching tree; cut‑elimination “prunes” the tree to remove non‑essential shortcuts. Ordinal Well‑Foundedness – Think of an ordinal as a descending ladder that never loops; if the ladder can’t descend forever, the theory is consistent. □ as “Trusted Certificate” – In provability logic, □A is like a verified certificate that A has a proof inside the theory. Reverse Mathematics as “Reverse Engineering” – Start with a theorem, then work backwards to discover the minimal “engine” (axioms) needed. Functional Interpretation as “Code Extraction” – Translating a proof into a program that computes the witnesses the proof asserts exist. --- 🚩 Exceptions & Edge Cases Cut‑Elimination Fails for Some Non‑Classical Logics – Certain modal or substructural logics lack a full cut‑elimination theorem. Gödel’s Second Incompleteness Requires ω‑Consistency – Rosser’s improvement shows simple consistency suffices for the first theorem but not for the second. Provability Logic Completeness Holds Only for PA – GL is complete w.r.t. Peano Arithmetic; other theories need different modal logics. Ordinal Analysis Not Uniform – Different theories require different ordinals (e.g., ε₀ for PA, larger for stronger systems). --- 📍 When to Use Which Choose a proof calculus Hilbert: When you need a minimal rule set for meta‑proofs. Natural Deduction: For intuitionistic/constructive reasoning and normal‑form analysis. Sequent Calculus: When you plan to apply cut‑elimination or study analytic proofs. Apply Ordinal Analysis When you need a relative consistency proof for an arithmetic or set‑theoretic fragment. Use Provability Logic (GL) To reason about statements about provability in PA (e.g., formalising Gödel’s second theorem). Employ Reverse Mathematics To classify the logical strength of a new theorem or to locate it among the Big Five. Invoke Functional Interpretation When you want to extract explicit constructive witnesses from a classical proof or to obtain an ordinal bound on provably total functions. --- 👀 Patterns to Recognize Subformula Property → Any cut‑free sequent derivation will never introduce new formulas; look for this when checking consistency arguments. Löb’s Formula Pattern – Statements of the form □(□A → A) → □A signal a provability‑logic reasoning step. Transfinite Induction Pattern – Proofs that “prove consistency” by induction up to a specific ordinal (ε₀, Γ₀, …). Big Five Signature – Theorems mentioning weak König’s lemma usually correspond to WKL₀; those involving arithmetical comprehension point to ACA₀. Dialectica Translation Shape – Classical ∀∃ statements become ∀∃ quantifier‑free statements about functionals; look for the “witness‑extraction” cue. --- 🗂️ Exam Traps Distractor: “Cut‑elimination always preserves proof length.” – Wrong; it can dramatically increase length. Distractor: “GL proves every arithmetic theorem.” – GL only captures the modal theory of provability, not the arithmetic content itself. Distractor: “ε₀ is a finite number used in arithmetic.” – ε₀ is a transfinite ordinal, not a finite integer. Distractor: “If a theorem is not provable in RCA₀, it must need Π₁¹‑CA₀.” – Many theorems fall in intermediate systems (WKL₀, ACA₀, ATR₀). Distractor: “Formal proof search is easy because checking is easy.” – Finding a proof (automated theorem proving) remains computationally hard despite easy verification. ---