Ordinal diagrams for recursively Mahlo universes (Q1576592)

From MaRDI portal
scientific article
Language Label Description Also known as
English
Ordinal diagrams for recursively Mahlo universes
scientific article

    Statements

    Ordinal diagrams for recursively Mahlo universes (English)
    0 references
    0 references
    9 January 2002
    0 references
    The paper under review is part of a great project of the author which continues the work of G. Gentzen and G. Takeuti, aiming at establishing the proof-theoretic strength of subsystems \(T_N\) of analysis. These systems are characterized by differently strong axiom schemata of \(\Pi_N\)-reflection (\(N\geq 2\)). The strength of a system \(T\) can be described by its proof-theoretic ordinal \[ |T|_{\Pi^{\Omega}_2}:=\inf\{\alpha\leq \omega^{CK}_1\mid\forall \Pi_2\text{-sentences }A(T\vdash A^{\Omega}\Rightarrow A^{\alpha})\}. \] In the considered paper \(N\) is to be 2. Let \(\mu\) be the least recursively Mahlo ordinal. \(\varkappa\) is called recursively Mahlo iff \(\varkappa\) is \(\Pi_2\)-reflecting on admissibles (i.e. on recursively regular ordinals). \(\varkappa\) is called \(\Pi_2\)-reflecting on admissibles if every \(\Pi_2\)-formula with parameters from \(\mathcal{L}_{\varkappa}\), the \(\varkappa\)-th element of the constructible hierarchy which is valid in \(\mathcal{L}_{\varkappa}\) is already valid in \(\mathcal{L}_{\varrho}\) for some admissible \(\varrho< \varkappa\). The author establishes an ordinal system \(O(\mu)\) of so-called ordinal diagrams starting with the symbols \(0\), \(\Omega\), \(\mu\),\(+\), \(\varphi\) and \(d\). \(\Omega\) is to represent the least admissible ordinal, + the usual addition, \(\varphi\) the Veblen functions and \(d\) something like the collapsing functions \(\psi\) introduced by \textit{W. Buchholz} in Ann. Pure Appl. Log. 32, 195-207 (1986; Zbl 0655.03038)]. Collapsing is permitted only with respect to \(\mu\) -- this yields admissible \(d_{\mu}\alpha\), and with respect to these \(\sigma= d_{\mu}\alpha\) -- this gives strongly critical not admissible ordinals \(d_{\sigma}\beta\). Together with \(O(\mu)\) simultaneously a binary relation \(<\) on \(O(\mu)\) is defined. The author proves: 1. The simultaneous definitions of \(O(\mu)\), \(<\), and certain auxiliary concepts, for instance sets of coefficients, are elementary recursive and can be formalized in the system \(S^1_2\) of bounded arithmetic of~~S. Buss. 2. \(<\) is a linear ordering of \(O(\mu)\). 3. \(<\) well-orders \(O(\mu)\). In the original version of the paper the author showed 1. and 2. simultaneously by a very long proof. Following a proposal of the referee, he separated both proofs by a slight modification of the definition. 3. is proved in the system \textbf{KPM} of set theory for recursively Mahlo universes by means of so-called distinguished classes, generalizing a method of \textit{W. Buchholz} [cf. ISILC Proof Theory Symp., dedic. Kurt Schütte, Proc. Int. Summer Inst., Logic Colloq., Kiel 1974, Lect. Notes Math. 500, 4-25 (1975; Zbl 0342.02021)]. Though obviously the system \(O(\mu)\) is closely related to set theory, the author reveals that he has no set-theoretic interpretation of \(O(\mu)\) at hand. The system is rather constructed in such a way that the proof of the Main Lemma in the submitted paper on ``Proof theory for theories of ordinals. I. Recursively Mahlo'' of the author can be executed. In a by now unpublished paper, the author of the paper under review presents a well-ordering proof for \(O(\mu)\) (and other systems) by means of inductive definitions.
    0 references
    proof-theoretic strength of subsystems of analysis
    0 references
    proof-theoretic ordinal
    0 references
    recursively Mahlo ordinal
    0 references
    ordinal diagrams
    0 references

    Identifiers