You are here

Proof Theory: The First Step into Impredicativity

Wolfram Pohlers
Publication Date: 
Number of Pages: 
[Reviewed by
Leon Harkleroad
, on

Consider the natural numbers N and a set of axioms for N, such as those of Peano Arithmetic (PA). Gödel incompleteness tells us that some true statements about N are not provable by means of PA. Of course, a different set of axioms may allow more statements to be proved.

What makes for a stronger axiom system that can prove more? Among other factors, the provisions a system does or does not make for various inductive-type definitions can strengthen or weaken it. For example, contrast these two methods of closing a set A under a binary product:

(1) working from the bottom up by forming products of two elements of A and then multiplying those products by elements of A, etc.

(2) defining the closure from the top down as the intersection of all sets that contain A and are closed under the product.

The latter, more elegant and less constructive, seems a higher-powered approach. One can, in fact, make this intuition precise. A standard measure of the strength of an axiom system is, roughly speaking, the size of the ordinals that the system can handle. Proof Theory takes various axiom systems (such as PA and the axioms for Kripke-Platek set theory) that treat induction in different ways and analyzes them from the ordinal viewpoint to gauge their relative strengths.

The book represents an expansion and rewriting of the author’s previous Springer Lecture Notes volume of the same title but different subtitle. This new version includes several developments in the field that have occurred over the twenty years since the original.

Although the current book, appearing in the Universitext series, claims to be “pitched at undergraduate/graduate level,” an undergraduate course out of Proof Theory would be ambitious indeed. The author pays much attention to presenting the big picture, but a lot of the material is inevitably of a fairly technical nature. The book provides many nontrivial exercises, including one with a “hint” that, even set in quite small type, fills two whole pages!

The notation is sometimes idiosyncratic, as is the English usage by the German author. One encounters such sentences as “The jutting property of well-founded relations is that they admit induction,” and “The following theorem ruminates Theorem 4.4.6.” However, these occasional awkward passages do not seriously affect the text’s comprehensibility.

Although in recent years Leon Harkleroad has mostly concentrated on mathematical aspects of music, he still enjoys revisiting his old stomping grounds of mathematical logic.

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.