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.