No label defined (Q4944924)

The author starts with an OS-structure \[ (T_I,\prec_I,\prec'_I,k_{I,I},\text{length}_I) \] as defined in Part I [in: S. B. Cooper et al. (eds.), Sets and proofs. Invited papers from the Logic Colloquium '97 (Cambridge Univ. Press, Cambridge), Lond. Math. Soc. Lect. Note Ser. 258, 301-338 (1999; Zbl 0944.03054)], and associates to each \(\sigma\in T_I\) a \(\sigma\)-structure in the sense of the previous paper. These \(\sigma\)-structures are related to each other by the functions \(k_{ij}:T_i\rightarrow_\omega T_j\), where \(T_i\) resp. \(T_j\) are their domains. An \(I\)-ordinal-system-structure is a ten-tuple \[ \big(T_I,(T_i)_{i\in T_I}, (\prec_i)_{i\in T_I\cup \{I\}},(\prec'_i)_{i\in T_I\cup \{I\}},\text{length},k,L,\prec_L, \text{level},\widetilde{k}\big). \] A system of this kind is called elementary, if the used functions and relations are primitive recursive and if their properties can be proven in \textbf{PRA}. The order types of these elementary \(I\)-OS are less than \(|\text{KPI}|\), the proof-theoretic ordinal of \textbf{KPI}. This results from the well-ordering proof, which is carried through in sections 4 and 5, and can be formalized in the case of elementary systems in \textbf{KPI}. The well-ordering of \(I\)-OS is shown in two ways. In both kinds of the proof a set \(\mathcal{W}\) of ordinals is defined. In section 4 for this purpose ``a new technique of transfinite sequences of ordinal notations'' is used which in section 2 is already applied in a variant of the well-ordering proof of \(\sigma\)-OS. It consists in defining sets \(A_\alpha\) of ordinals which serve to introduce the \(\mu\)-accessible sets \(\text{Acc}_\mu\) and the sets \(M_\mu\) which are received in Part I by the method of distinguished sets developed by \textit{W. Buchholz} [Lect. Notes Math. 500, 4-25 (1975; Zbl 0342.02021)]. This method of Buchholz' is used by the author in section 5 to define the already mentioned set \(\mathcal{W}\). After establishing \(\mathcal{W}\), the well-ordering proof in both sections is the same. In section 6 the author shows that \(|\text{KPI}|\) is the supremum of the order types of all elementary \(I\)-OSs. For this purpose, in analogy to the corresponding consideration in Part I for \(n\)-OS and \(\sigma\)-OS, \(I\)-ordinal function generators are introduced. They are used to define a sequence of \(I\)-OSs whose order types converge to \(|\text{KPI}|\). For the entire collection see [Zbl 0932.00038].