Proof Theory: The First Step into Impredicativity

1. Historical Background 2. Primitive Recursive Functions and Relations 2.1 Primitive Recursive Functions 2.2 Primitive Recursive Relations 3 Ordinals 3.1 Heuristic 3.2 Some Basic Facts on Ordinals 3.3 Fundamentals of Ordinal Arithmetic 3.3.1 A Notation System for the Ordinals below epsilon nought 3.4 The Veblen Hierarchy 3.4.1 Preliminaries 3.4.2 The Veblen Hierarchy 3.4.3 A Notation System for the Ordinals below Gamma nought 4. Pure Logic 4.1 Heiristics 4.2 First and Second Order Logic 4.3 The Tait Calculus 4.4 Trees and the Completeness Theorem 4.5 Gentzens Hauptsatz for Pure First Order Logic 4.6 Second Order Logic 5. Truth Complexities for Pi 1-1-Sentences 5.1 The language of Arithmetic 5.2 The Tait language for Second Order Arithmetic 5.3 Truth Complexities for Arithmetical Sentences 5.4 Truth Complexities for Pi 1-1-Sentences 6. Inductive Definitions 6.1 Motivation 6.2 Inductive Definitions as Monotone Operators 6.3 The Stages of an Inductive Definition 6.4 Arithmetically Definable Inductive Definitions 6.5 Inductive Definitions, Well-Orderings and Well-Founded Trees 6.6 Inductive Definitions and Truth Complexities 6.7 The Pi-1-1- Ordinal of a Theory 7. The Ordinal Analysis for Pean Arithmetic 7.1 The Theory PA 7.2 The Theory NT 7.3 The Upper Bound 7.4 The Lower Bound 7.5 The Use of Gentzen's Consistency Proof for Hilbert's Programme 7.5.1 On the Consistency of Formal and Semi-Formal Systems 7.5.2 The Consistency of NT 7.5.3 Kreisel's Counterexample 7.5.4 Gentzen's Consistency Proof in the Light of Hilbert's Programme 8. Autonomous Ordinals and the Limits of Predicativity 8.1 The Language L-kappa 8.2 Semantics for L-kappa 8.3 Autonomous Ordinals 8.4 The Upper Bound for Autonomous Ordinals 8.5 The Lower Bound for Autonomous Ordinals 9. Ordinal Analysis of the Theory for Inductive Definitions 9.1 The Theory ID1 9.2 The Language L infinity (NT) 9.3 The Semi-Formal System for L infinity (NT) 9.3.1 Semantical Cut-Elimination 9.3.2 Operator Controlled Derivations 9.4 The Collapsing Theorem for ID1 9.5 The Upper Bound 9.6 The Lower Bound 9.6.1 Coding Ordinals in L(NT) 9.6.2 The Well-Ordering Proof 9.7 Alternative Interpretations for Omega 10 Provably Recursive Functions of NT 10.1 Provably Recursive Functions of a Theory 10.2 Operator Controlled Derivations 10.3 Iterating Operators 10.4 Cut Elimination for Operator Controlled Derivations 10.5 The Embedding of NT 10.6 Discussion 11. Ordinal Analysis for Kripke Platek Set Theory with infinity 11.1 Naive Set Theory 11.2 The Language of Set Theory 11.3 Constructible Sets 11.4 Kripke Platek Set Theory 11.5 ID1 as a Subtheory of Kp-omega 11.6 Variations of KP-omega and Axiom beta 11.7 The Sigma Ordinal of KP-omega 11.8 The Theory of Pi-2 Reflection 11.9 An Infinite Verification Calculus for the Constructible Hierarchy 11.10 A Semi-Formal System for Ramified Set Theory 11.11 The Collapsing Theorem for Ramified Set Theory 11.12 Ordinal Analysis for Kripke Platek Set Theory 12 Predicativity Revisited 12.1 Admissible Extensions 12.2 M-Logic 12.3 Extending Semi-Formal Systems 12.4 Asymmetric Interpretations 12.5 Reduction of T+ to T 12.6 The Theories KP n and KP 0-n 12.7 The Theories KPl 0 and KP i 0 13 Non-Monotone Inductive Definitions 13.1 Non-Monotone Inductive Definitions 13.2 Prewellorderings 13.3 The Theory for Pi 0-1 definable Fixed-Points 13.4 ID1 as a Sub-Theory of the Theory for Pi 0-1 definable Fixed-Points 13.5 The Upper Bound for the Proof theoretical Ordinal of Pi 0-1-FXP 14. Epilogue