Andrej Bauer: Fixed-point theorems in synthetic computability 2

Datum objave: 17. 10. 2017
Seminar za temelje matematike in teoretično računalništvo
Torek, 17. 10. 2017, od 12h do 14h, Plemljev seminar, Jadranska 19

Nadaljevali in zaključili bomo predavanje iz prejšnjega tedna. Vabljeni!

Abstract: Lawvere's fixed point theorem captures the essence of diagonalization arguments. Cantor's theorem, Gödel's incompleteness theorem, and Tarski's undefinability of truth are all instances of the theorem in the contra-positive form. It is harder to apply the theorem directly because non-trivial examples are not easily found, in fact, none exist if excluded middle holds. 

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.