Source-linked AI summary
Proof Theory
Jeremy Avigad
TL;DR
Proof theory asks how mathematical reasoning can be formalized and studied through concrete proof systems, a question originating in Hilbert’s program. The paper develops natural deduction and sequent-calculus methods, including cut elimination and witness extraction, while noting limits imposed by incompleteness and proof-size growth.
Problem
Proof theory addresses how mathematical reasoning can be represented in formal systems and analyzed syntactically, a foundational question raised by Hilbert’s program.
Method
The paper studies natural deduction and sequent calculi, using cut elimination, normalization, translations, and related proof-theoretic methods.
Results
Cut elimination yields cut-free proofs, while Herbrand’s theorem and the intuitionistic explicit definability property extract term-level information under stated conditions.
Takeaways & Limitations
Proof-theoretic analysis can expose explicit information, constructive content, and syntactic structure in formal reasoning.
Takeaways & Limitations
Gödel’s second incompleteness theorem prevents sufficiently strong mathematics from establishing its own consistency, and cut elimination can cause unavoidable iterated exponential proof growth.
Abstract
from arXiv · showhide
Proof theory began in the 1920's as a part of Hilbert's program, which aimed to secure the foundations of mathematics by modeling infinitary mathematics with formal axiomatic systems and proving those systems consistent using restricted, finitary means. The program thus viewed mathematics as a system of reasoning with precise linguistic norms, governed by rules that can be described and studied in concrete terms. Today such a viewpoint has applications in mathematics, computer science, and the philosophy of mathematics.
1 Introduction
Proof theory emerged from Hilbert’s program to formalize infinitary mathematics and establish consistency through finitary reasoning. Although Gödel’s second incompleteness theorem defeated the program’s original formulation, syntactic study of mathematical reasoning remains broadly fruitful.
- Hilbert’s program sought to represent abstract mathematical reasoning in formal axiomatic systems with fixed languages and precise inference rules.
- Proofs were treated as finite combinatorial objects whose consistency could be established using concrete arguments.Consistency means that no contradiction can be derived.
- Gödel’s second incompleteness theorem shows that sufficiently strong mathematics cannot establish its own consistency.The theorem also blocks establishing the consistency of any theory properly extending that mathematics.
- Modern proof theory studies formal deductive systems and applies syntactic analysis to mathematical reasoning and other forms of inference.The field includes modal, temporal, probabilistic, inductive, defeasible, and deontic reasoning.
- The paper introduces natural deduction and a sequent calculus, states cut elimination and its consequences, surveys proof-theoretic analysis, and discusses applications.
2 Natural deduction and sequent calculi
The section presents natural deduction and sequent calculi as formal representations of logical reasoning, then develops cut elimination and extraction results. These results show how proof transformations can expose explicit information and constructive content.
- Natural deduction models connectives through introduction and elimination rules and represents arguments within a context of hypotheses.For conjunction, introduction requires both conjuncts, while elimination permits either conjunct to be concluded.
- A sequent Γ ⇒ϕ expresses that ϕ follows from Γ, while implication introduction discharges a temporary hypothesis.
- Sequent calculi represent derivations as Γ ⇒∆, where the hypotheses imply the disjunction of the assertions; intuitionistic logic restricts ∆ to at most one formula.The cut rule is the only rule containing a hypothesis formula unrelated to the conclusion formulas.
- If Γ ⇒∆ is derivable with cut, it is derivable without cut.Gentzen’s proof supplies an explicit cut-removal algorithm.
- Cut-free proofs make the formulas in each sequent directly dependent on preceding sequents, facilitating extraction of useful information.
- Herbrand’s theorem extracts explicit term witnesses from proofs of existential statements derived from universal hypotheses.Theorem 2.2 specifies a finite disjunction of quantifier-free instances with a quantifier-free proof.
- In intuitionistic logic, under the stated restriction on positive occurrences of ∨ and ∃, a derivable existential statement has a term substitution whose quantifier-free conclusion is also derivable.
3 Methods and goals
Proof theory formalizes mathematical reasoning in hierarchies of logical, arithmetic, and set-theoretic systems, then compares their strength through reductions, conservation results, and interpretations.
- Hilbert’s program represents mathematical reasoning in formal systems and studies those systems as mathematical objects.
- Proof theory examines systems ranging from pure first-order logic and primitive recursive arithmetic to Peano arithmetic, second-order arithmetic, and ZF.Primitive recursive arithmetic is designed as a patently finitary system and can express much mathematics involving finite objects and structures.
- 3.1 Classical foundations: Classical foundations distinguish axiomatic higher-order systems from their semantic characterizations, and second-order arithmetic extends Peano arithmetic with second-order logic and induction principles.
- 3.2 Constructive foundations: Constructive foundations restrict logic to intuitionistic reasoning, yielding systems such as Heyting arithmetic, Martin-Löf type theory, and the calculus of inductive constructions.The excluded middle is not generally accepted intuitionistically because one may lack knowledge or an algorithm identifying which disjunct holds.
- 3.4 Comparative analysis and reduction: Comparative analysis uses translations, cut elimination, normalization, double-negation interpretations, realizability, functional interpretations, model theory, and forcing.Conservation results can provide foundational reductions between theories, including reductions from infinitary to finitary or nonconstructive to constructive theories.
4 Applications
Proof-theoretic methods extract information from ordinary proofs, study combinatorial independence, connect logic with programming and verification, and analyze proof complexity.
- 4.1 Proof interpretation: Proof-theoretic methods can extract useful information from ordinary mathematical proofs by interpreting classical arguments constructively.This process, called “unwinding proofs,” requires formal modeling choices and domain-specific adaptation of metamathematical tools.
- 4.2 Combinatorial independences: Natural combinatorial independences are finitary principles independent of conventional mathematical methods, exemplified by the Paris-Harrington statement.Such work investigates combinatorial behavior beyond ordinary patterns of mathematical reasoning and yields mathematics in its own right.
- 4.3 Constructive mathematics and type theory: Constructive mathematics and type theory connect logical constructions with programming principles in both directions and combine proving with programming.
- 4.4 Automated reasoning and formal verification: Automated reasoning and formal verification use formal methods to check hardware, software, and complex mathematical proofs against specifications or correctness requirements.These efforts have led to interactive approaches involving users.
- 4.5 Proof complexity: Proof complexity combines proof theory with computational complexity, relating proof lengths in calculi to complexity-theoretic questions such as whether NP equals co-NP.