Geometric Rules in Infinitary Logic

Sara Negri - University of Helsinki
Date and time
Monday, October 15, 2018 at 4:30 PM - Sala verde
Programme Director
Peter Michael Schuster
External reference
Publication date
July 20, 2018
Computer Science  


Several mathematical theories - such as the theory of torsion abelian groups, of Archimedean ordered fields, and of connected graphs - are axiomatized by infinitary geometric implications. Proof analysis is extended to all such theories by augmenting an infinitary classical sequent calculus with a rule scheme for infinitary geometric implications. The calculus is designed in such a way as to have all the rules invertible and all the structural rules (weakening, contraction, and cut) admissible. An intuitionistic infinitary multisuccedent sequent calculus is also introduced, and is shown to enjoy the same structural properties. Finally, bringing the classical and intuitionistic calculi close to each other yields the infinitary Barr theorem without any further ado. [This is talk is based on unpublished joint work with the late Roy Dyckhoff.]

Contact person: Peter Schuster

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