Computability and non-monotone induction

Non-monotone inductive definitions were studied in the late 1960's and early 1970's with the aim of understanding connections between the complexity of the formulas defining the induction steps and the ordinals measuring the rank of the inductive process. In general, any type 2 functional will generate an inductive process, and in this paper we will view non- monotone induction as a functional of type 3. We investigate the associated computation theory of this functional inherited from the Kleene schemes and we investigate the associated companion of sets with codes computable in the functional of non- monotone induction. The interest in this functional is motivated from observing that constructions via non-monotone induction appear to be natural in classical analysis. There are two groups of results: We establish strong closure properties of the least ordinal without a code computable in the functional of non-monotone induction, and we provide a characterisation of the class of functionals of type 3 computable from this functional, a characterisation in terms of sequential operators working in transfinite time. We will also see that the full computational power of non-monotone induction is required when this principle is used to construct functionals witnessing the compactness of the Cantor space and of closed, bounded intervals.