Geometric Rules in Infinitary Logic

Sara Negri - University of Helsinki
Data e ora
lunedì 15 ottobre 2018 alle ore 16.30 - Sala verde
Peter Michael Schuster
Referente esterno
Data pubblicazione
20 luglio 2018


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  Universit√† degli studi di Verona
Via dell'Artigliere 8, 37129 Verona  |  P. I.V.A. 01541040232  |  C. FISCALE 93009870234