Geometric Rules in Infinitary Logic

Relatore:  Sara Negri - University of Helsinki
  lunedì 15 ottobre 2018 alle ore 16.30 Sala verde

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

Peter Michael Schuster

Data pubblicazione
20 luglio 2018

Offerta formativa