On the proof-theoretic strength of monotone induction in explicit mathematics (Q1356976)

In the general setting of explicit mathematics, Feferman introduced a powerful principle MID, which ought to include ``all constructive formulations of iteration of monotone inductive definitions'' [cf. \textit{S. Feferman}, ``Monotone inductive definitions'', in: A. Troelstra and D. van Dalen (eds.), The L. E. J. Brouwer Centenary Symposium, Stud. Logic Found. Math. 110, 77-89 (1982; Zbl 0525.03037)]. MID states: if \(F\) is any operation mapping classes into classes and preserving inclusion among classes, then there exists a class \(Y\) which is a least fixed point of \(F\). The present paper is concerned with the proof-theoretic strength of MID. In order to understand the (difficulty of the) problem, it should be first observed that there is no trivial direct set-theoretic modeling of MID by the (superficially similar) fixed point theorem for monotone operators (the reason resides in the special ontology of explicit mathematics: functions are given by means of type free operations in the sense of partial combinatory logic, while classes are identified with their definitions). The main result of the paper characterizes the strength of MID in terms of existence of stable ordinals and parameter-free \(\Pi^1_2\)-comprehension (respectively). More precisely, the authors consider the following proof-theoretically equivalent systems (modulo a suitable collection of formulas), all of which comprise only induction axioms (no schema) for numbers, sets and classes (respectively): 1. the fragment \(\Sigma^1_2\)-AC\(_0\) of second order arithmetic, based on axiom of choice for \(\Sigma^1_2\)-conditions; 2. Jäger's theory KPi\(^r\) which axiomatizes recursively inaccessible universes [cf. \textit{G. Jäger}, Theories for admissible sets. A unifying approach to proof theory (1986; Zbl 0638.03052)]; 3. Feferman's system, based on elementary comprehension ECA, join J and restricted inductive generation IG. They show that Feferman's system plus MID is equivalent to the second order fragment \(\Sigma^1_2\)-AC\(_0\) extended with parameter-free \(\Pi^1_2\)-CA, as well to KPi\(^r\) extended with the axiom postulating the existence of a stable ordinal (i.e. of an \(\alpha\) such that the constructible hierarchy up to \(\alpha\) is an elementary substructure of the whole hierarchy \(L\) w.r.t. \(\Sigma_1\)-formulas). The most attractive feature of the paper lies in the interplay of generalized recursion theory, set theory and proof theory. We only mention two highlights: 1) the application of Takahashi's technique for modeling systems of explicit mathematics plus MID [\textit{S. Takahashi}, Ann. Pure Appl. Logic 42, 255-297 (1989; Zbl 0665.03037)], as subtly refined by \textit{T. Glaß} [Standardstrukturen für Systeme expliziter Mathematik, Diss., Univ. Münster (1993)]\ and combined with the proof theoretic technique of asymmetric interpretation; 2) \textit{M. Rathjen}'s result [J. Symb. Logic, 61, 125-146 (1996; Zbl 0851.03018)], showing that MID-modulo restricted inductive generation IG and Join- can be used to handle non-monotone inductive definitions. The significance of the equivalences for foundational aims (in the sense of reductive proof theory) is unclear, as the authors themselves acknowledge. As a matter of fact, they achieve a reduction of highly impredicative principles (like the esistence of a stable ordinal or parameter-free \(\Pi^1_2\)-CA) to explicit mathematics plus MID, based on classical logic. But it is left open if the result still works on the basis of intuitionistic logic (as it is the case for the system T\(_0\)); and whether one can yield a justification of MID on the basis of some generalized construction principle. There are little oversights or misprints: 1. In the definition of prewellordering (p.40), well-foundedness is not mentioned, while `linear' ought not to be included. 2. p.7: Definition by cases on the natural numbers is mentioned among the basic operation constants; but the axioms only provide definition by cases on the whole universe (see the applicative axioms of p.8). 3. The symbol N is used as a class constant (p.42), but no class constant is given when defining the basic language. 4. p.45: T\(_0+\mu+D\) should be read as T\(_0+\)MID.