Computability and Non-monotone induction

TL;DR

This paper explores the theoretical foundations of non-monotone induction viewed as a type 3 functional, analyzing its computational properties, closure characteristics, and applications in classical analysis and topology.

Contribution

It provides a new characterization of type 3 functionals computable via non-monotone induction and investigates their closure properties and applications in analysis.

Findings

Established strong closure properties of the least ordinal without such codes.

Characterized functionals of type 3 computable from non-monotone induction.

Demonstrated the necessity of full non-monotone induction for certain topological constructions.

Abstract

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 size of the ordinals measuring the duration of the inductions. 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 inherited from the Kleene schemes and we investigate the nature of the associated companion of sets with codes computable in non-monotone induction. The interest in this functional is motivated from observing that constructions via non-monotone induction appear as natural in classical analysis in its original form. There are two groups of results: We establish strong closure properties of the least ordinal without a code computable in non-monotone induction, and we provide a characterisation of the class of functionals of type 3 computable from non-monotone induction, a characterisation in terms of sequential operators working in transfinite time. We will also see that the full 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.