Overview
Proof Theory is the study of proofs themselves. Instead of just proving things about numbers or geometry, proof theory treats the proof as the object of study. It asks: What is a proof? How complex is it? Can it be transformed or simplified?
Core Idea
The core idea is syntax over semantics. Proof theory focuses on the formal rules of manipulating symbols to derive conclusions, regardless of what those symbols “mean.”
Formal Definition
Proof theory analyzes formal deduction systems, such as:
- Hilbert Systems: Many axioms, few rules.
- Natural Deduction: Few axioms, many rules (closer to how humans reason).
- Sequent Calculus: Focuses on the logical connectives and symmetries (Left rules vs. Right rules).
Intuition
If Model Theory is about “Truth” (semantics), Proof Theory is about “Provability” (syntax). It’s like studying the rules of chess (how pieces move) rather than the strategy of winning.
Examples
- Cut-Elimination: A famous theorem (Gentzen’s Hauptsatz) showing that any proof in Sequent Calculus can be transformed into a proof without “detours” (lemmas). This implies consistency.
- Consistency Proofs: Proving that a system will never derive “False” ($\bot$).
Common Misconceptions
- Misconception: A proof is just an argument that convinces someone.
- Correction: In proof theory, a proof is a finite, syntactically correct tree or sequence of formulas following strict rules.
- Misconception: If it’s true, it’s provable.
- Correction: Gödel’s Incompleteness Theorems showed that in any sufficiently complex system, there are true statements that cannot be proved within that system.
Related Concepts
- Model Theory: The other main pillar of logic, focusing on semantics and truth.
- Curry-Howard Correspondence: A deep connection between proofs in logic and programs in computer science (Proofs as Programs).
- Automated Theorem Proving: Using computers to find proofs.
Applications
- Computer Science: Type theory (used in programming languages like Haskell and Rust) is essentially proof theory.
- Verification: Ensuring software is bug-free by proving it meets a specification.
- Philosophy: Understanding the nature of mathematical justification.
Criticism and Limitations
- Hilbert’s Program: The original goal of proof theory—to prove the consistency of all mathematics using finitary means—was shown to be impossible by Gödel.
Further Reading
- Proofs and Types by Jean-Yves Girard
- Basic Proof Theory by A.S. Troelstra and H. Schwichtenberg