Heyting Day 2025: Exploring Intuitionism & Computability with Andrej Bauer 🧠

Andrej Bauer (University of Ljubljana) – Turing degrees in synthetic computability
The starting point of synthetic computability is the observation that the effective topos is a mathematical world in which computability is built in and inherent in all constructions. One would therefore expect that the topos provides a good environment for developing computability theory. Indeed, classic theorems of computability theory take particularly natural form when expressed in the internal language of the effective topos, which is higher-order intuitionistic logic. For example, the fact that c.e. sets can be computably enumerated manifests itself as the Enumerability Axiom, which states that there are countably many countable subsets of the natural numbers; the recursion theorem is expressed as a fixed-point principle for multi-valued maps; immune sets are those that are neither finite nor infinite, and so on.

In this talk I shall present recent joint work with Andrew Swan, in which we explored how synthetic computability may encompass Turing degrees. Specifically, I will discuss the Kleene-Post and Friedberg-Muchnik constructions of incomparable Turing degrees. In synthetic computability, both constructions are instances of a general domain-theoretic variant of the Baire category theorem. Their non-constructive nature is gauged with judicious use of oracle modalities – logical operators that force non-constructive or non-computable statements, such as the limited principle of omniscience and the decidability of halting.