On fixed-point theorems in synthetic computability.

*(English)*Zbl 1403.03076Summary: 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 contrapositive form of the theorem. 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 synthetic computability, which is higher-order intuitionistic logic augmented with the Axiom of Countable Choice, Markov’s principle, and the Enumeration axiom, which states that there are countably many countable subsets of \(\mathbb{N}\). These extra-logical principles are valid in the effective topos, as well as in any realizability topos built over Turing machines with an oracle, and suffice for an abstract axiomatic development of a computability theory.

We show that every countably generated \(\omega\)-chain complete pointed partial order (\(\omega\)cppo) is countable, and that countably generated \(\omega\)cppos are closed under countable products. Therefore, Lawvere’s fixed-point theorem applies and we obtain fixed points of all endomaps on countably generated \(\omega\)cppos. Similarly, the Knaster-Tarski theorem guarantees existence of least fixed points of continuous endomaps. To get the best of both theorems, namely that all endomaps on domains (\(\omega\)cppos generated by a countable set of compact elements) have least fixed points, we prove a synthetic version of the Myhill-Shepherdson theorem: every map from an \(\omega\)cpo to a domain is continuous. The proof relies on a new fixed-point theorem, the synthetic Recursion Theorem, so called because it subsumes the classic Kleene-Rogers Recursion Theorem. The Recursion Theorem takes the form of Lawvere’s fixed point theorem for multi-valued endomaps.

We study Lawvere’s fixed-point theorem in synthetic computability, which is higher-order intuitionistic logic augmented with the Axiom of Countable Choice, Markov’s principle, and the Enumeration axiom, which states that there are countably many countable subsets of \(\mathbb{N}\). These extra-logical principles are valid in the effective topos, as well as in any realizability topos built over Turing machines with an oracle, and suffice for an abstract axiomatic development of a computability theory.

We show that every countably generated \(\omega\)-chain complete pointed partial order (\(\omega\)cppo) is countable, and that countably generated \(\omega\)cppos are closed under countable products. Therefore, Lawvere’s fixed-point theorem applies and we obtain fixed points of all endomaps on countably generated \(\omega\)cppos. Similarly, the Knaster-Tarski theorem guarantees existence of least fixed points of continuous endomaps. To get the best of both theorems, namely that all endomaps on domains (\(\omega\)cppos generated by a countable set of compact elements) have least fixed points, we prove a synthetic version of the Myhill-Shepherdson theorem: every map from an \(\omega\)cpo to a domain is continuous. The proof relies on a new fixed-point theorem, the synthetic Recursion Theorem, so called because it subsumes the classic Kleene-Rogers Recursion Theorem. The Recursion Theorem takes the form of Lawvere’s fixed point theorem for multi-valued endomaps.

##### MSC:

03D75 | Abstract and axiomatic computability and recursion theory |

54H25 | Fixed-point and coincidence theorems (topological aspects) |

03F65 | Other constructive mathematics |

Full Text:
DOI

**OpenURL**

##### References:

[1] | A. Bauer. First steps in synthetic computability theory. Electronic Notes in Theoretical Computer Science, 155:5-31, 2006. · Zbl 1273.03144 |

[2] | A. Bauer and D. Lešnik. Metric spaces in synthetic topology. Annals of pure and applied logic, 163(2):87-100, 2012. |

[3] | E. Bishop. Foundations of Constructive Analysis. McGraw-Hill, 1967. · Zbl 0183.01503 |

[4] | D. Bridges and F. Richman. Varieties of Constructive Mathematics. Number 97 in London Mathematical Society Lecture Note Series. Cambridge University Press, 1987. |

[5] | Y. L. Ershov. The theory of enumerations. Nauka, 1980. |

[6] | M. Escardó. Synthetic topology of data types and classical spaces. Electronic Notes in Theoretical Computer Science, 87:21-156, 2004. |

[7] | J. M. E. Hyland. The effective topos. In A.S. Troelstra and D. Van Dalen, editors, The L.E.J. Brouwer Centenary Symposium, pages 165-216. North Holland Publishing Company, 1982. · Zbl 0522.03055 |

[8] | J. M. E. Hyland. First steps in synthetic domain theory. In Category Theory, number 1488 in Lecture Notes in Mathematics, 1991. · Zbl 0747.18004 |

[9] | S. C. Kleene. On notation for ordinal numbers. Journal of Symbolic Logic, 3(4):150-155, 1938. · Zbl 0020.33803 |

[10] | S. C. Kleene. Introduction to Metamathematics. North-Holland, 1952. · Zbl 0047.00703 |

[11] | B. Knaster. Un théoréme sur les fonctions d’ensembles. Annales Polonici Mathematici, 6:133-134, 1928. · JFM 54.0091.04 |

[12] | J. Lambek and P. J. Scott. Introduction to higher order categorical logic, volume 7 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, Cambridge, 1986. · Zbl 0596.03002 |

[13] | F. W. Lawvere. Diagonal arguments and cartesian closed categories. Lecture Notes in Mathematics, 92:134-145, 1969. Republished in: Reprints in Theory and Applications of Categories, No. 15 (2006), 1-13. |

[14] | D. Lešnik. Synthetic Topology and Constructive Metric Spaces. PhD thesis, University of Ljubljana, 2010. |

[15] | A. A. Markov. On the continuity of constructive functions. Uspekhi Matematicheskikh Nauk, 9(3/61):226-230, 1954. · Zbl 0056.24901 |

[16] | J. Myhill and J. C. Shepherdson. E_ective operations on partial recursive functions. Zeitschrift für mathematische Logik und Grundlagen der Mathematik, 1(4):310-317, 1955. · Zbl 0068.24706 |

[17] | W. Phoa. Domain Theory in Realizability Toposes. PhD thesis, Trinity College, Cambridge, 1991. |

[18] | F. Richman. Church’s thesis without tears. The Journal of Symbolic Logic, 48(3):797-803, September 1983. · Zbl 0527.03036 |

[19] | H. Rogers. Theory of Recursive Functions and E_ective Computability. MIT Press, 1967. |

[20] | G. Rosolini. Continuity and Effectiveness in Topoi. PhD thesis, University of Oxford, 1986. |

[21] | A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5(2):285-309, 1955. · Zbl 0064.26004 |

[22] | P. Taylor. The fixed point property in synthetic domain theory. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS ’91), Amsterdam, The Netherlands, July 15-18, 1991, pages 152-160, 1991. |

[23] | P. Taylor. Foundations for computable topology. In G. Sommaruga, editor, Foundational Theories of Classical and Constructive Mathematics, volume 76 of The Western Ontario Series in Philosophy of Science, pages 265-310. Springer Netherlands, 2011. · Zbl 1317.03041 |

[24] | A. S. Troelstra. Metamathematical investigation of intuitionistic arithmetic and analysis, volume 344 of Lecture notes in mathematics. Springer, 1973. |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.