An Introduction to Proof Theory: Normalization, Cut-Elimination, and Consistency Proofs

by Paolo Mancosu, Richard Zach, Sergio Galvan

Length: 432 pages
Edition: 1
Language: English
Publisher: Oxford University Press
Publication Date: 2021-10-12
ISBN-10: 019289594X
ISBN-13: 9780192895943
Sales Rank: #871694 (See Top 100 Books)

An Introduction to Proof Theory provides an accessible introduction to the theory of proofs, with details of proofs worked out and examples and exercises to aid the reader’s understanding. It also serves as a companion to reading the original pathbreaking articles by Gerhard Gentzen. The first half covers topics in structural proof theory, including the Gödel-Gentzen translation of classical into intuitionistic logic (and arithmetic), natural deduction and the normalization theorems (for both NJ and NK), the sequent calculus, including cut-elimination and mid-sequent theorems, and various applications of these results. The second half examines ordinal proof theory, specifically Gentzen’s consistency proof for first-order Peano Arithmetic. The theory of ordinal notations and other elements of ordinal theory are developed from scratch, and no knowledge of set theory is presumed. The proof methods needed to establish proof-theoretic results, especially proof by induction, are introduced in stages throughout the text. Mancosu, Galvan, and Zach’s introduction will provide a solid foundation for those looking to understand this central area of mathematical logic and the philosophy of mathematics.

An Introduction to Proof Theory: Normalization, Cut-Elimination, and Consistency Proofs
Copyright
Contents
Preface
	About this book
	For further reading
	Acknowledgments
1 Introduction
	1.1 Hilbert's consistency program
	1.2 Gentzen's proof theory
	1.3 Proof theory after Gentzen
2 Axiomatic calculi
	2.1 Propositional logic
	2.2 Reading formulas as trees
	2.3 Sub-formulas and main connectives
	2.4 Logical calculi
	2.5 Inference rules
	2.6 Derivations from assumptions and provability
	2.7 Proofs by induction
	2.8 The deduction theorem
	2.9 Derivations as trees
	2.10 Negation
	2.11 Independence
	2.12 An alternative axiomatization of J0
	2.13 Predicate logic
	2.14 The deduction theorem for the predicate calculus
	2.15 Intuitionistic and classical arithmetic
3 Natural deduction
	3.1 Introduction
	3.2 Rules and deductions
	3.3 Natural deduction for classical logic
	3.4 Alternative systems for classical logic
	3.5 Measuring deductions
	3.6 Manipulating deductions, proofs about deductions
	3.7 Equivalence of natural and axiomatic deduction
4 Normal deductions
	4.1 Introduction
	4.2 Double induction
	4.3 Normalization for ∧, ⊃, ¬, ∀
	4.4 The sub-formula property
	4.5 The size of normal deductions
	4.6 Normalization for NJ
	4.7 An example
	4.8 The sub-formula property for NJ
	4.9 Normalization for NK
5 The sequent calculus
	5.1 The language of the sequent calculus
	5.2 Rules of LK
	5.3 Constructing proofs in LK
	5.4 The significance of cut
	5.5 Examples of proofs
	5.6 Atomic logical axioms
	5.7 Lemma on variable replacement
	5.8 Translating NJ to LJ
	5.9 Translating LJ to NJ
6 The cut-elimination theorem
	6.1 Preliminary definitions
	6.2 Outline of the lemma
	6.3 Removing mixes directly
	6.4 Reducing the degree of mix
	6.5 Reducing the rank
	6.6 Reducing the rank: example
	6.7 Reducing the degree: example
	6.8 Intuitionistic sequent calculus LJ
	6.9 Why mix?
	6.10 Consequences of the Hauptsatz
	6.11 The mid-sequent theorem
7 The consistency of arithmetic
	7.1 Introduction
	7.2 Consistency of simple proofs
	7.3 Preliminary details
	7.4 Overview of the consistency proof
	7.5 Replacing inductions
	7.6 Reducing suitable cuts
	7.7 A first example
	7.8 Elimination of weakenings
	7.9 Existence of suitable cuts
	7.10 A simple example
	7.11 Summary
8 Ordinal notations and induction
	8.1 Orders, well-orders, and induction
	8.2 Lexicographical orderings
	8.3 Ordinal notations up to ε0
	8.4 Operations on ordinal notations
	8.5 Ordinal notations are well-ordered
	8.6 Set-theoretic definitions of the ordinals
	8.7 Constructing ε0 from below
	8.8 Ordinal arithmetic
	8.9 Trees and Goodstein sequences
9 The consistency of arithmetic, continued
	9.1 Assigning ordinal notations <ε0 to proofs
	9.2 Eliminating inductions from the end-part
	9.3 Removing weakenings
	9.4 Reduction of suitable cuts
	9.5 A simple example, revisited
A The Greek alphabet
B Set-theoretic notation
C Axioms, rules, and theorems of axiomatic calculi
	C.1 Axioms and rules of inference
	C.2 Theorems and derived rules
D Exercises on axiomatic derivations
	D.1 Hints for prob:deductions
	D.2 Hints for prob:mo
	D.3 Exercises with quantifiers
E Natural deduction
	E.1 Inference rules
	E.2 Conversions
F Sequent calculus
G Outline of the cut-elimination theorem
Bibliography
Index