Skip to main content

Meeting 26 (10/01/2022, Birmingham)

January 10, 2022

Hosted on Zoom by the University of Birmingham
Supported by the London Mathematical Society

Zoom Link: The meeting will be held online via Zoom. You can click here to join.

Schedule (all GMT times):

  • 10:30-10:35 Welcome
  • 10:35-11:20 Eric Finster (University of Birmingham)
  • 11:20-12:05 Matteo Spadetto (University of Leeds)
  • 12:05-13:30 Lunch break
  • 13:30-14:15 Tomáš Jakl (University of Cambridge)
  • 14:15-15:00 Zeinab Galal (University of Leeds)

All talks are 30 minutes followed by 15 minutes of questions and discussion.

Titles and Abstracts:

Speaker: Eric Finster
Title: Infinitely Connected Objects
Abstract: One interesting aspect of ∞-topos theory which separates it from classical homotopy theory is the existence of objects which have trivial homotopy groups in every dimension, but which nonetheless are not contractible. We say such objects are ∞-connected. In this short talk, I will give a quick introduction to this notion and describe the main sources of examples.
Slides: here

Speaker: Matteo Spadetto
Title: Dialectica completion & dialectica logical principles
Abstract: The notion of dialectica construction associated to a finitely complete category, an attempt of providing a categorical version of Gödel's Dialectica interpretation, was introduced by de Paiva in her PhD thesis and then generalised by Hyland and Biering to an arbitrary fibration. In this talk we introduce the notion of Gödel fibration, which categorically embodies both the logical principles of traditional Skolemization and the existence of a prenex normal form presentation for every formula. A Gödel fibration is defined by a list of categorical properties, essentially saying that it has "enough" existential quantifier free and universal quantifier free predicates.

Taking advantage of Hofstra's recent work relating the generalised version of de Paiva's construction to the notions of existential and universal completion of a given fibration, we characterise the instances of the dialectica completion, showing that these are precisely the Gödel fibrations. Secondly we mention some principles and rules that are involved in the Dialectica interpretation and that these fibrations satisfy. Finally, we describe the categorical (logical) structures that behave well with respect to this construction, comparing the proof irrelevant setting to the proof relevant one. The talk is based on joint work with Davide Trotta (University of Pisa) and Valeria de Paiva (Topos Institute).
Slides: here

Speaker: Tomáš Jakl
Title: Game comonads and Courcelle's theorem
Abstract:  In the recent years comonads encoding positions in model comparison games have been successfully applied to study a range of imporatnt notions in finite model theory and combinatorics.

I will give an overivew of the emerging theory of game comonads and an ongoing work with Dan Marsden and Nihil Shah where we prove various Feferman–Vaught-Mostowski-type theorems, which are behind Courcelle's celebrated theorem.
Slides: here

Speaker: Zeinab Galal
Title: Finiteness species of structures
Abstract: Finiteness spaces were introduced by Ehrhard as a refinement of the relational model of linear logic. A finiteness space is a set equipped with a class of finitary subsets which can be thought of being subsets that behave like finite sets. A morphism between finiteness spaces is a relation that preserves the finitary structure. This model allows for a finer analysis of the computational aspects of the relational model and it provided a semantical motivation for differential linear logic and the syntactic notion of Taylor expansion. In this talk, I will present a bicategorical generalization of this construction where the relational model is replaced with the model of generalized species of structures introduced by Fiore, Gambino, Hyland and Winskel and the finiteness property now relies on finite presentability.
Slides: here