Monotone inductive definitions in a constructive theory of functions and classes
Shuzo Takahashi · Annals of Pure and Applied Logic · 1989
The least fixed point principle has been studied for various types of inductive detititins.As far as mathematical practice is concerned, it seems sufficient to consider this principle for positive elementary inductive definitions, which are described by Grst order positive formulas over a mathematical domain of interest.A domain may, for example, be a set of symbolic expressions, a countable abelian p-group, or a closed subset of real nrrmbcrs.(For a more precise formulation, see 0 1.3; for examples of monotone inductive definitions in mathematics, see Appendix 3.) Beyond mathematical practice, however, the principle has been studied for more general inductive definitions because of their logical interest.One o? the most general formulations of this principle can be given in the language of Zermelo-Fraenkel set theory (ZF) as follows: for any fixed set A, every function which maps from the power set of A to itself and which satisfies the monotonicity condition has a least tied point (for m"sr,: details, see 0 2.2).In fact, this is a theroem in ZF.We refer to this principle as the Least Fixed Point Theorem in ZF.Our interest is in studying the least fixed point principle in a constructive setting, whose formulation is as general as the one of the above theorem in ZF.A constructive theory of functions and sets, To, has been developed by Feferman in his paper [2].This theory deals both with sets and with functions over sets as independent notions.The description of To can be found in the next section.(In a constructive framework, functions are given by algorithmic rules of construction, and sets are given by defining properties.We use operations and classes in To instead of functions and sets in ZF, respectively.)In the language of T,, we are able to formulate the least fixed point principle for monotone inductive definitions as: every operation f on classes to classes which satisfies the monotonicity condition has a least fixed point. is is called t rinciple of 3.50 @ i989, Ekevier Scizne Publishers E.V. (North-