Abstract
A comprehensive introduction to proof theory covering natural deduction, sequent calculus, normalization, and cut-elimination for both classical and intuitionistic logic. The book provides detailed treatments of the proof-theoretic foundations of logic and type theory, including the Curry-Howard correspondence, strong normalization theorems, and realizability interpretations. It serves as a standard reference for structural proof theory with rigorous proofs of fundamental metatheorems. The second edition expands coverage of linear logic, modal logic, and computational interpretations.
Outline
Chapter 1: Introduction
- Basic notions of proof theory
- Historical development
- Natural deduction versus sequent calculus
Chapter 2: Natural Deduction
- Natural deduction for propositional logic
- Natural deduction for first-order logic
- Introduction and elimination rules
- Normalization of derivations
- Subformula property for normal proofs
Chapter 3: The Curry-Howard Isomorphism
- Curry-Howard correspondence for intuitionistic logic
- Propositions as types
- Proofs as programs
- Simply-typed lambda calculus
- Strong normalization and logical consistency
Chapter 4: Sequent Calculus
- Sequent calculus (LK and LJ)
- Structural rules
- Cut-elimination theorem (Gentzen’s Hauptsatz)
- Midsequent theorem
- Applications to consistency
Chapter 5: Completeness
- Soundness and completeness
- Kripke semantics for intuitionistic logic
- Completeness via canonical models
- Beth trees and tableaux methods
Chapter 6: Strong Normalization
- Strong normalization for simply-typed lambda calculus
- Tait’s computability method
- Girard’s reducibility candidates
- Applications to consistency and decidability
Chapter 7: Intuitionistic Logic and Arithmetic
- Heyting arithmetic
- Realizability interpretations
- Kleene’s number realizability
- Modified realizability
- Relations to constructive mathematics
Chapter 8: Classical Logic and Arithmetic
- Peano arithmetic
- Gödel’s incompleteness theorems
- Provable recursion
- Ordinal analysis
Chapter 9: Extensions
- Modal logic proof theory
- Linear logic
- Substructural logics
- Proof nets