Proof theory. An introduction (Q1801306)

This is the fourth view to the massif of proof theory after Schütte's, Takeuti's and Girard's. As in the moutains, different points of view present different impressions. The subheading promises a more elementary access, but already in the preface the author indicates a stereo view, one eye looking basically and the other one more advanced. The general attitude of the author against proof theory is similar to that of S. Feferman described at the beginning of his appendix to the second edition of Takeuti's monograph on proof theory. Pohlers comes from the Munich school of Proof Theory, and therefore it is quite natural that he concentrates upon ordinal analysis of some subsystems of analysis. The philosophical aspects of proof theory in general and of his own procedure are referred to very briefly at the beginning and at the end. Other possible philosophical views of proof theory are neither mentioned nor dealt with. This gives space for a comprehensive motivation of the ideas and methods used. Thus the author covers more and more advanced theories than Girard in his splendid book, avoiding deviations respectively hiding his digressions (especially in the direction of recursion theory) in the exercises. In Chapter I he acquits himself of the duty to deal with pure number theory, but from the beginning he works in a general setting in view of the later use. He introduces infinitary languages and formal systems. In Chapter II the ordinal analysis of predicative analysis is treated. Chapter III is devoted to a formal system \(ID_ 1\) of noniterated inductive definitions and its proof theoretic ordinal. First an introduction to monotone inductive definitions is given. Since this is a tool used throughout in mathematics, but its logical treatment can only be found in advanced literature, it may be interesting for mathematicians not especially engaged in logic to get informed of the role and development of this general device in logic. For the ordinal analysis of \(ID_ 1\) the notation system of W. Buchholz is used, which is especially elegant for this purpose. This monograph may well be the basis for an introductory lecture on proof theory. Also mathematicians may read it to get informed of central ideas and main methods of a very important branch of proof theory. But they must realize that this book presents only the top of an iceberg, and the other parts and cross connections to other disciplines are deserving of being studied as well.