A model-theoretic approach to proof theory. Edited by Zofia Adamowicz, Teresa Bigorajska and Konrad Zdanowski (Q2322259)

The unfinished manuscript of the book by Henryk Kotlarski (1949--2008) was prepared for publication by his students and colleagues. The book is devoted to several topics on the border of combinatorics, proof theory, and model theory for Peano arithmetic. It contains an exposition of model-theoretic and combinatorial methods for obtaining results in proof theory, such as incompleteness theorems and a description of the provably total functions of a theory. The book consists of five chapters. Сhapter 1 contains some material about ordinal combinatorics of finite sets in the style of the results by \textit{J. Ketonen} and \textit{R. Solovay} [Ann. Math. (2) 113, 267--314 (1981; Zbl 0494.03027)]. Classical Ramsey-type results are proved. Ordinals up to \(\varepsilon_0\) are introduced and a so-called hierarchy of Hardy functions is studied. This hierarchy allows to define the concept of an \(\alpha\)-large (\(\alpha<\varepsilon_0\)) finite set of natural numbers. Some partition properties for this notion of largeness are proved. This provides a background for an analysis of subsystems of Peano arithmetic and for combinatorial independence results. Chapter 2 presents concepts and ideas from model theory that will be used later in the book: unions of chains, recursive saturation and resplendency, the Chang and Makkai theorem. Chapter 3 provides several proofs of the first and second Gödel incompleteness theorems and Tarski's theorem. Along with the original proof based on the diagonal lemma, the proofs with the application of model-theoretic methods are considered. In the latter case, an important role is played by the completeness theorem (the existence of a model of a consistent theory) formalized in PA, satisfaction predicates, and the concept of a satisfaction class. They are used in many contexts. Scott's proof of the first Gödel theorem, Kreisel's and Jech's proofs of the second Gödel theorem, and the proofs of the incompleteness theorems using nonstandard models are presented, as well as Kikuchi's proofs of the second incompleteness theorem and the Tarski theorem simulating the Berry paradox. The presented proofs are very different in nature. They show various aspects of the phenomena of incompleteness. The so-called \(\Sigma_1\)-closed models are considered. Extensions of PA by adding the \(\omega\)-rule or reflection principles are briefly discussed, and Löb's theorem is proved. Chapter 4 presents a model-theoretic approach to the classical results of Gentzen, developed by \textit{Z. Ratajczyk} [Fundam. Math. 130, No. 4, 191--213 (1988; Zbl 0659.03036)] and \textit{R. Sommer} [Transfinite induction and hierarchies of functions generated by transfinite recursion within Peano arithmetic. Berkeley, CA: University of California (PhD Thesis) (1990)]. The method of indicators for obtaining independence results is defined. It is shown what amount of transfinite induction is proved in fragments of PA. Combinatorics of \(\alpha\)-large sets is used for obtaining independence results. Chapter 5 is devoted to the notion of a nonstandard satisfaction class introduced by \textit{W. Marek} (ed.) et al. [Set theory and hierarchy theory. A memorial tribute to Andrzej Mostowski, Bierutowice, Poland 1975. Berlin-Heidelberg-New York: Springer-Verlag (1976; Zbl 0324.00007)] and playing an important technical role in the study of the models of arithmetic. In particular, it contains the results by \textit{S. Smith} [Nonstandard syntax and semantics and full satisfaction classes for models of arithmetic. New Haven, CT: Yale University (PhD Thesis) (1984)] on definability in the language with a satisfaction class and on models without a satisfaction class.