/events/heyting-day-2025-models-intuitionism-and-computability
Symposium in honour of Jaap van Oosten
Can we imagine a world in which computability is built-in into the very fabric of reality? The answer is a resounding yes. However, it took us almost 40 years to get the first detailed picture of such a world.
Our speakers will give you a scenic tour around such worlds of computability. They will introduce the relevant concepts and discuss the many amazing properties of such worlds.
A first step towards unveiling worlds of computability was taken eighty years ago by Stephen Cole Kleene. His idea is presented in his landmark paper "On the interpretation of intuitionistic number theory". In the 1980s, Martin Hyland took the next big step towards a world of computability. He constructed the effective topos. Since Hyland’s work, many new insights have been gathered concerning the effective topos and its kin.
The effective topos is just one example of a class of structures known as realizability toposes. These were the subject of van Oosten's book "Realizability: An Introduction to its Categorical Side" of 2008. Their construction is parameterized by an abstract model of computation known as a partial combinatory algebra.
The significance of realizability toposes lies in the interplay between and unification of several fields including proof theory, computability theory and category theory. They allow the classical mathematician to make sense of intuitionistic logic and yield a semantics for streamlined accounts of mathematics like synthetic computability theory.
Speakers
- Andy Pitts, University of Cambridge
- Andrej Bauer, University of Ljubljana
- Sebastiaan Terwijn, Radboud University
- Jaap van Oosten, Utrecht University
- 9.30 - 10.00 a.m. – Reception with coffee, tea, cookies
- 10.00 - 10.15 a.m. – Opening 10.15-11.15: Andrew Pitts: Heyting Algebras and Higher-Order Logic
- 11.15 - 11.45 a.m. – Break
- 11.45 - 12.45 p.m. – Andrej Bauer: Turing degrees in synthetic computability
- 12.45 - 2.00 p.m. – Lunch
- 2.00 - 3.00 p.m. – Sebastiaan Terwijn: Embeddings and completions in partial combinatory algebra
- 3.00 - 3.30 p.m. – Break
- 3.30 - 3.45 p.m. – Benno introduces Jaap
- 3.45 - 4.45 p.m. – Jaap van Oosten, Heyting Lecture Categories and Computability
- 4.45 - 6.00 p.m. – Drinks
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.
Realizability studies various categorical structures that correspond to logical theories. Ever since Hyland's seminal paper on "the effective topos", computability theory has been instrumental in analysing the logical significance of categorical constructs; recent work by my last PhD student Jetze Zoethout, explores the other direction. My talk will explain one instance of this.
Every logical theory gives rise to a Lindenbaum-Tarski algebra of truth values, whose underlying set is the theory's sentences quotiented by provability in the theory. For theories in classical first-order logic, the algebras that arise are exactly all possible Boolean algebras. For theories in intuitionistic first-order logic, they are all possible Heyting algebras. What happens when we move from first-order to higher-order? Higher-order logic allows quantification not only over individuals, but also over sets of individuals, sets of sets of individuals, and so on, for any finite order of iterating "sets of". In the classical case, the Lindenbaum-Tarski algebras of higher-order theories are still all Boolean algebras. In the intuitionistic case, as far as I am aware, we do not know which Heyting algebras can be the Lindenbaum-Tarski algebra of a higher-order theory.
My attempt to resolve this question more than 30 years ago failed, but produced the consolation prize of a very surprising property of intuitionistic logic that has subsequently been called "uniform interpolation". I will explain the connection between Heyting algebras of higher order theories and uniform interpolation and tell you something of what has followed in the pursuit of this open question.
Partial combinatory algebras (pcas) are abstract models of computation. They are one of the earliest type of model that emerged in the 1930's when mathematicians were trying to define what it means to be computable. Notions such as recursive functions (used by Gödel in the proof of his incompleteness theorems), Turing machines, combinatory algebra and lambda calculus each turned out to be useful in the development of the theory of computation, setting the stage for the advent of computer science. From the beginning, these studies were intertwined with the question about what is provable in mathematics, and what a constructive proof is or should be. Thus pcas play a part, together with the closely related lambda calculus, as the theoretical background for modern day inventions like functional programming, and at the same time are a tool in building models of constructive mathematics.
In this talk we will give a quick introduction to the basics of pcas and discuss some of the key examples, such as Kleene's models K_1 (which describes the classical setting for computation on the natural numbers) and K_2 (which does the same for the real numbers). We then discuss recent results about embeddings and completions of pcas. If time permits we will also discuss the complexity of pcas, and the complexity of the isomorphism problem.
