Ordinal Analysis with an Introduction to Proof Theory

Preface
Contents
1 Introduction
	1.1 Languages
	1.2 Sequent Calculi
	1.3 Arithmetic
		1.3.1 Subrecursive Functions and Weak Arithmetic
		1.3.2 Incompleteness
		1.3.3 Jumps and Trees
		1.3.4 Π11-Completeness of W
		1.3.5 Inductive Definitions
	1.4 Proof-Theoretic Ordinals
	1.5 Kripke–Platek Set Theory
		1.5.1 Σ-Reflection and Its Consequences
		1.5.2 Constructible Hierarchy and Admissible Sets
	1.6 Notes
	References
2 Calculi for Classical Logic
	2.1 Completeness of Cut-Free Fragments
		2.1.1 Canonical Proof Search
		2.1.2 Applied Calculi
		2.1.3 Predicative Second Order Logic
		2.1.4 Predicative Extensions
		2.1.5 ω-Logic
	2.2 Consequences of Cut-Elimination
		2.2.1 Midsequent Theorem
		2.2.2 Interpolation Theorem
		2.2.3 Herbrand's Theorems
		2.2.4 Epsilon Theorems
		2.2.5 Parikh's Theorem
		2.2.6 Primitive Recursion
		2.2.7 Primitive Recursion on Sets
	2.3 Notes
		2.3.1 Section2.1
		2.3.2 Section2.2
		2.3.3 Exercises
	References
3 Cut-Elimination with Depths
	3.1 Classical Logic
		3.1.1 Elimination Procedure for Classical Calculus
		3.1.2 Predicative Second Order Logic
		3.1.3 Propositional Logics
	3.2 Fixed Point Logic
	3.3 Intuitionistic Logic
		3.3.1 Elimination Procedure for Intuitionistic Calculus
		3.3.2 Intutionistic Fixed Point Logic
	3.4 Epsilon Calculi
	3.5 Notes
		3.5.1 Section3.1
		3.5.2 Section3.2
		3.5.3 Section3.3
		3.5.4 Section3.4
		3.5.5 Exercises
	References
4 Epsilon Numbers
	4.1 Provability of Transfinite Induction
		4.1.1 A Standard ε0-Order
	4.2 Unprovability of Transfinite Induction
		4.2.1 Bounding Order Types of Provably Well-Founded Orders
		4.2.2 Embeddings
		4.2.3 2-Consistency
	4.3 Consistency Strengths Calibrated with Ordinals
		4.3.1 Consistency Proof
		4.3.2 Π2-Analyses
	4.4 Intuitionistic Fixed Point Theories
		4.4.1 Finitary Analysis of Intuitionistic Fixed Points Theories
	4.5 Notes
		4.5.1 Section 4.1
		4.5.2 Section 4.2
		4.5.3 Section 4.3
		4.5.4 Section 4.4
	References
5 Iterations
	5.1 Binary Veblen Functions and Club Sets
	5.2 Axiom Schemata in Second Order Arithmetic
	5.3 Theories of Jump Hierarchies
		5.3.1 Transfinite Inductions in the Theories of Jump Hierarchies
		5.3.2 Predicative Cut Elimination
	5.4 Classical Fixed Point Theories
		5.4.1 Eliminating Fixed Points
		5.4.2 Proving the Fixed Point Axiom from the Well-Ordering Principle
		5.4.3 Simulating Jump Hierarchies by Fixed Points
	5.5 Proof-Theoretic Strengths of the Well-Ordering Principles
		5.5.1 Derivative and Countable Coded ω-Models
		5.5.2 Elimination of the Inference for Well-Ordering Principle
		5.5.3 Proof-Theoretic Ordinals of the Well-Ordering Principles
	Exercises
	5.6 Notes
		5.6.1 Section5.2
		5.6.2 Section5.3
		5.6.3 Section5.4
		5.6.4 Section5.5
		5.6.5 Exercises5.5.3
	References
6 Collapsings
	6.1 Theories IDν, Π11-CA and KPν
		6.1.1 Kripke–Platek Set Theory for Iterated Admissibility
	6.2 Higher Ordinals with Collapsing Functions
		6.2.1 Recursive Notation System T(Ων) of Ordinals
	6.3 Well-Foundedness Proof
	6.4 Impredicative Cut Elimination
		6.4.1 Operator Controlled Derivations
		6.4.2 Ω-Rule
		6.4.3 Interpretations
	6.5 Ordinal Analysis of Kripke–Platek Set Theory KPν
		6.5.1 Ramified Set Theory
		6.5.2 Embedding
	6.6 Applications of Operator Controlled Derivations
		6.6.1 A Relativized Ordinal Analysis
		6.6.2 Reducing Πn+1-Reflections to Iterated Πn-Reflections
	6.7 Notes
		6.7.1 Section 6.2
		6.7.2 Section 6.3
		6.7.3 Section 6.4
		6.7.4 Section 6.5
		6.7.5 Subsection 6.6.1
		6.7.6 Subsection 6.6.2
		6.7.7 Exercises 6.6.2.2
	References
7 Answers to Exercises
	Reference
Index