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

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