The proof-theoretic relevance of Grothendieck topologies

Olivia Caramello - UniversitĂ  dell'Insubria
Date and time
Thursday, October 5, 2017 at 4:00 PM - Rinfresco 16.00 in Sala caffé (primo piano) - inizio seminario 16.15
Programme Director
Peter Michael Schuster
External reference
Publication date
September 5, 2017
Computer Science  


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 given geometric theory and the subtoposes of its classifying topos. Interestingly, these alternative 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.

© 2002 - 2021  Verona University
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234