A Model-Theoretic Approach to Ordinal Analysis (Q4338039)

Ordinal analysis, a main tool of proof theory, is of a very syntactical nature. Indeed, the first result of this area, by Gentzen, gives a proof of transfinite induction up to \(\alpha\) in PA for any \(\alpha<\varepsilon_0\), and also a finitary method that transforms a purported proof of induction up to \(\varepsilon_0\) into a simpler one. Thus, \(\varepsilon_0\) is the precise limit, i.e. proof-theoretic ordinal, of PA. [Cf. \textit{G. Gentzen}, ``Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der transfiniten Induktion in der reinen Zahlentheorie'', Math. Ann. 119, 140-161 (1943; Zbl 0028.10201).] The authors obtain this and other proof-theoretic ordinals by model-theoretic and combinatorial means, like indicators and \(\alpha\)-largeness, that have been developed by Paris, Solovay et al. since the mid 1970's. Starting from a non-standard model \(\mathfrak M\) of true arithmetic and the assumption that \({\mathfrak M}\models[a,b]\) is \(\alpha\)-large, the authors construct an initial segment \(I\), between \(a\) and \(b\), that is a model of the theory, \(T\), in question. Thinking of the case when \(b\) is the least so that \([a,b]\) is \(\alpha\)-large, we know that \(\forall x \exists y\) (\([x,y]\) is \(\alpha\)-large) is false in \(I\). But this statement is provable in a very weak base theory, \(I\Delta_0+(\exp)\), by induction up to \(\alpha\). That means: this induction cannot be proved in \(T\). Thus, the authors replace transformations of formal proofs by constructions of models! Tools used are more or less familiar (as they state), but their combinations are interesting. Of course, the construction of the model, \(I\), needs work, particularly when \(T\) is second order. Among other devices, they use the jump operator with respect to the truth predicate to approximate \(\{x/\varphi(x)\}\) in the model and to give the range of set-variables. In this paper, after a leisurely introduction about ideas, approaches, literature, etc. (as is appropriate for this Bulletin), the authors determine ordinals of \(I\Sigma_n\), PA, \(\text{WKL}_0\) (weak König's lemma), \(\text{ACA}_0\) (arithmetic comprehension axioms), and \(\Sigma^1_1\)-\(\text{AC}_0\) (axiom of choice), among others, to be \(\omega_{n+1}\), \(\varepsilon_0\), \(\omega^\omega\), \(\varepsilon_0\), and \(\varepsilon_0\), respectively. (Of course, these are known in the literature.) They state that more powerful, and yet predicative theories will be considered in a sequel to appear in the Journal of Symb. Logic.