Monotone inductive definitions in a constructive theory of functions and classes (Q1115865)

A constructive theory of functions and classes, \(T_ 0\), has been developed by \textit{S. Feferman} [Lect. Notes Math. 450, 87-139 (1975; Zbl 0357.02029)]. In a constructive framework, functions are given by algorithmic rules of construction and classes are given by defining properties. In the language of \(T_ 0\) we are able to formulate the least fixed point principle for monotone inductive definitions (MID) as: every monotone operation f on classes to classes has a least fixed point. The question due to \textit{S. Feferman} [The L. E. J. Brouwer Centen. Symp., Proc. Conf., Noordwijkerhout/Holl. 1981, Stud. Logic Found. Math. 110, 77-89 (1982; Zbl 0525.03037)] of the strength of \(T_ 0+M\) and some related questions are prime concern of this paper. Main results are: the consistency of \(T_ 0+MID\) (through constructing the corresponding model in set-theoretic sense) and the proof-theoretical equivalence between a subsystem \(EM_ 0+J+MID\) of \(T_ 0+MID\) and \(\Pi^ 1_ 1-CA\). This equivalence can be obtained by a careful examination of the analogous model construction for \(EM_ 0+J+MID\). The proof-theoretic strength of \(T_ 0+MID\) still remains open. Note that in any model of \(T_ 0\) the cardinality of the collection of classes is the same as the cardinality of the universal class \(V=\{x| x=x\}\) of all entities. So, it does not seem to be possible to use for MID the least fixed point theorem in ZF. There is a similarity with the ordinary Myhill and Shepherdson theorem that every monotone recursive transformation of the indexes of r.e. sets is described by a \(\Sigma^+\)-formula and has a least fixed point. However, in \(T_ 0\) classes are unlike r.e. sets, because they are closed under complementation operation. Hence, some additional ideas are used. The paper is selfcontained and clearly written.