Andrej Bauer: Fixed-point theorems in synthetic computability 2

We study Lawvere's fixed-point theorem in the effective topos. Rather than operating directly with the topos, we work in synthetic computability, which is higher-order intuitionistic logic augmented with Countable choice, Markov principle, and the Enumeration axiom, which states that there are countably many countable subsets of natural numbers. These extra-logical principles are valid in the effective topos and suffice for an abstract axiomatic development of a computability theory. 

We show that every countably generated ω-chain complete pointed partial order (ωCPPO) is countable, and that countably generated ωCPPOs are closed under countable products. Therefore, Lawvere's theorem theorem applies and we obtain fixed points of all endomaps on countably generated ωCPPOs, although we cannot say much about them. On the other hand, the Knaster-Tarski theorem guarantees existence of least fixed points, if we restrict to continuous endomaps. To get the best of both theorems, we prove a domain-theoretic version of the Kreisel--Lacombe--Shoenfield--Ceitin theorem: every map from an ωCPO to a domain (an ωCPPO which is generated by a countable set of compact elements) is continuous. The proof relies on a synthetic Recursion theorem, which subsumes the classic Kleene-Rogers Recursion theorem, and takes the form of a modified Lawvere's fixed point theorem that applies to multi-valued endomaps.