Rencontre, May 28, 2026
Programme
- 10:30 – 11:45
-
Sam van Gool (ENS Paris Saclay)Invited talk: Ultraconvergence spaces
We introduce the concept of ultraconvergence space: a category equipped with additional structure that captures "how objects converge along ultrafilter-indexed families of objects". The main instance of interest is the category of points of any Grothendieck topos, which can be endowed with such an ultraconvergence structure in a canonical way. When viewed through a logical lens, the ultraconvergence space canonically associated to a geometric theory is its category of models, equipped with additional structure that captures "how models map to ultraproducts of models". Our main theorem is a representation result: if a topos has enough points, then it is equivalent to a category of étale spaces over the canonical ultraconvergence space of its points. This theorem simultaneously generalizes both M. Barr's 1970 "Relational algebras" representing topological spaces via the ultrafilter monad, and M. Makkai's 1987 "Stone duality for first-order logic" between coherent toposes and ultracategories.
This is joint work with Jérémie Marquès and Umberto Tarantino, recently appeared in Journal of Pure and Applied Algebra 2026 (https://doi.org/10.1016/j.jpaa.2026.108269), also see https://arxiv.org/abs/2508.09604 .
- 13:45 – 14:45
-
Nuria Brede (IRIF)
In joint work with Hugo Herbelin https://inria.hal.science/hal-03144849, we studied different choice and bar induction principles from a "generic" perspective: We showed how weak Kőnig's lemma, the fan theorem, bar induction, dependent choice, the Boolean prime ideal theorem and general choice have common contrapositive generalisations. In the talk, I will revisit this work and put it into perspective of an ongoing classification and formalisation effort to constructively relate various logical principles which are classically equivalent to choice axioms.
- 15:15 – 16:15
-
Bruno da Rocha Paiva (University of Birmingham)Invited talk: Internalising effectful forcing in System T
Gödel first introduced System T in his dialectica interpretation to prove consistency of arithmetic. As a higher-order analogue of primitive recursive functions, computability in System T has been studied extensively. For example, it is known that all functions F : (ℕ → ℕ) → ℕ are continuous, in the sense that their output must only rely on a finite amount of their input. Moreover, it can even be shown if F is a System T function, then the amount of input that required to compute F(α) can itself be computed via a function m : (ℕ → ℕ) → ℕ in System T. While the former result has a succinct semantic proof using a model based in dialogue trees, the latter result seemed out of reach. In this talk we will see how to rephrase this model as a syntactic translation using Church-encodings of dialogue trees, allowing us to prove that the stronger result about moduli of continuity.
