/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
