Proof theory

前置知识

30 项必需的前置知识（一直追溯到底）

你将学会

• Present classical and intuitionistic sequent calculi and prove cut elimination for propositional logic.
• Derive the subformula property and consistency from cut elimination.
• Explain the idea of Gentzen's consistency proof for PA using transfinite induction up to ε₀.

定义

• A sequent Γ ⊢ Δ asserts that the conjunction of the formulas in Γ entails the disjunction of those in Δ.
• The cut rule combines proofs of Γ ⊢ A, Δ and Γ′, A ⊢ Δ′ into a proof of Γ, Γ′ ⊢ Δ, Δ′.
• ε₀ is the least ordinal ε with ω^ε = ε.

定理

• Gentzen's Hauptsatz: the cut rule is admissible in the sequent calculus for first-order logic.
• Cut-free proofs have the subformula property.
• Gentzen (1936): the consistency of PA is provable in primitive recursive arithmetic together with quantifier-free transfinite induction up to ε₀.
• PA does not prove transfinite induction up to ε₀ (for a standard notation system), although it proves it for every smaller ordinal in that system.

常见误解

• Thinking Gentzen's proof is circular; it relies on a principle not available in PA but different in kind from PA's consistency.
• Believing cut elimination shortens proofs; it can increase their length enormously (non-elementarily).

可选发现

• Categorical logic Proofs modulo normalisation can be organised into categories: proofs in the conjunction–implication fragment of intuitionistic logic correspond to morphisms of free cartesian closed categories.
• The λ-calculus Curry–Howard: natural-deduction proofs are typed λ-terms, and cut elimination corresponds to β-reduction (normalisation).
• ← Proof: direct, contrapositive, contradiction and induction
• ← Type theory and propositions as types
• ← Computational complexity

延伸阅读

• A. S. Troelstra and H. Schwichtenberg, Basic Proof Theory (1996)
• Jean-Yves Girard, Yves Lafont and Paul Taylor, Proofs and Types (1989)
• Gaisi Takeuti, Proof Theory (1975)