Monotone inductive definitions in a constructive theory of functions and classes

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.

Recommendations

Cites work

Cited in

(16)

This page was built for publication: Monotone inductive definitions in a constructive theory of functions and classes

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1115865)