Friday 3 May 2024, 10:00, room 1Z71: Deductive systems and Grothendieck topologies, Olivia Caramello (University of Insubria, Como)

I will show that the classical proof system of geometric logic over a given geometric theory is equivalent to new proof systems based on the notion of Grothendieck topology. These equivalences result from a proof-theoretic interpretation of the duality between the quotients of a geometric theory and the subtoposes of its classifying topos. Interestingly, these new proof systems turn out to be computationally better-behaved than the classical one for many purposes, as I will illustrate by discussing a few selected applications.