Proof theory of reflection (Q1332853)

This is a well-written paper. Its final product is the determination of the proof-theoretic ordinal of \(\text{KP}+ \Pi_ 3\)-Ref, i.e. Kripke- Platek set theory with \(\Pi_ 3\)-reflection. To reach there, the author gives motivations, intuitions, backgrounds, future visions, etc., making the paper accessible and almost self-contained. First, he develops a powerful ordinal notation system, \(T(K)\), composed of \(0\), \(K\), \(+\), \(\varphi\), \(\Omega\), \(\Xi\), \(\Psi\), and the ordering \(<\). According to him, ``nude ordinal notation systems without any set-theoretic interpretation tend to be hard to grasp'', and so he reminds ``the reader some set-theoretical notions'', first. Indeed, \(K\) is a weakly compact cardinal, \(\varphi\) is the Veblen function, etc. Then an infinitary proof system, \(RS(K)\), of ramified set theory is presented. Here, the subject of investigation is the initial segment, given by \(T(K)\), of the constructible set hierarchy. Since each set is named, infinitary rules here are counter-parts of the \(\omega\)-rule in Peano arithmetic. Cut- elimination is achieved by means of \(H\)-controlled derivations, and then KP-set theory is embedded into \(RS(K)\), thus determining its ordinal. Of course, \(\Pi_ 3\)-reflection is just a beginning: ``the idea is that \(\Pi^ 1_ 2\)-comprehension can be fathomed by going through transfinite levels of reflection: and thus an ordinal analysis for it should be attainable via an, admittedly, considerable extension of the machinery laid out in this paper''. \{Being given quite a few inches, one wants an ell: the author could have spent 2, 3 sentences in explaining the Veblen function \(\varphi\), what its connection with \(\varepsilon\)- numbers is, and what \(\alpha= _{\text{NF}} \varphi \beta \gamma\) means. A few more words might not have been wasted on collapsing functions as well as on \(H\)-controlled derivations, perhaps. Apparently, proof-reading was done a bit hastily: among others, p. 190, footnote, read `for' for `für', peut-être; p. 205, Lem. 8.3., `\([\neq]\)' is not defined; p. 210, Def. 9.3.(i), read `\(\alpha_ n \geq \beta_ 1\)' for `\(\alpha_ 1\geq \beta_ 1\)'; p. 211, Def. 9.5.(iii), read `\(\pi\leq\tau \leq\mu\)' for `\(\pi\leq \tau\leq \pi\)'; p. 224, ref. [26], read `Arch.' for `Ann.' and `(1994)' for `(1944)'\}.