First order theories for nonmonotone inductive definitions: Recursively inaccessible and Mahlo (Q2758045)

A nonmonotone inductive definition is given by an arbitrary operator \(\Phi\) from subsets of natural numbers to subsets of natural numbers; the inductive set defined by \(\Phi\) is the unique set \(I_{\Phi}\) such that \(I_{\Phi}=I_{\Phi}^{|\Phi|}\), where \(|\Phi|\) is the least ordinal \(\beta\) satisfying \(I_{\Phi}^\beta=I_{\Phi}^{<\beta}\) and, in general, \(\{I_\Phi^\alpha \}\) is the sequence satisfying, for any ordinal \(\alpha\), NEWLINE\[NEWLINE I_\Phi^\alpha=I_\Phi^{<\alpha}\cup\Phi(I_{\Phi}^{<\alpha}) NEWLINE\]NEWLINE Roughly, the theory of inductive definitions deals with the structural properties of classes of inductively defined sets and studies the associated closure ordinals of the form \(|\Phi|\). If \(\Phi\) is monotone, the corresponding theory of monotone inductive definitions is thoroughly investigated both on the model-theoretic side [see, e.g., the book of \textit{Y. N. Moschovakis}, Elementary induction on abstract structures, Amsterdam: North-Holland (1974; Zbl 0307.02003)] and on the proof-theoretic side [see, e.g., the collective volume of \textit{W. Buchholz, S. Feferman, W. Pohlers} and \textit{W. Sieg}, Iterated inductive definitions and subsystems of analysis: Recent proof-theoretical studies, Berlin: Springer-Verlag, Lect. Notes Math. 897 (1981; Zbl 0489.03022)], but no corresponding proof-theoretic investigation was known for nonmonotone inductive definitions (for which much is available in the recursion-theoretic literature since the fundamental papers of \textit{P. Aczel} and \textit{W. Richter} [Lect. Notes Math. 255, 1-9 (1972; Zbl 0272.02065)]and of \textit{Y. N. Moschovakis} [Fundam. Math. 82, 39-83 (1974; Zbl 0306.02039)]. The present paper fills the gap by introducing first-order theories FID(H) of nonmonotone inductive definitions, whose operators are definable by means of arithmetical formulas belongingto suitable classes H. He considers, among others: \([\Pi^0_1, \Pi^0_1]\), \([\Pi^0_1, \Pi^0_0]\), \([POS, \Pi^0_0]\) and \([POS, QF]\); the idea behind these operator classes is that one first applies an operator of the first class until closure is reached, then one proceeds with an operator of the second class. The relevant theories are extensions of Peano arithmetic with ordinal variables and ordinal quantifiers, formally codifying the definitions of the sequence \(\{I_{\Phi}^\alpha\}\) and the existence of \(|\Phi|\), for every operator \(\Phi\) of a given class H. The main results are proof-theoretic in nature and are based upon careful reductions to set theories. Indeed, theories of iterated admissibility are introduced, which describe set-theoretic universes with strong reflection properties (roughly implying recursive inaccessibility or, respectively, Mahloness). Then the theories of nonmonotone inductive definitions under investigation are interpreted in admissible set theories KPi, KPm (and variants thereof, depending on the induction principles adopted). As a by-product, one obtains upper bounds for the given systems of nonmonotone inductive definitions, since the given set theories have known strengths. These upper bounds are sharp, what follows from work by the same author and T. Studer, who have shown that strong systems of Feferman's explicit mathematics [\textit{S. Feferman}, Lect. Notes Math. 450, 87-139 (1975; Zbl 0357.02029)] are naturally modelled within theories of nonmonotone inductive definitions. In particular, the present paper can be profitably read as a companion of \textit{G. Jäger} and \textit{T. Studer}, ``Extending the system \(T_0\) of explicit mathematics: The limit and Mahlo axioms'' [Ann. Pure Appl. Logic 114, 79-101 (2002; Zbl 1002.03052)].