Sara Negri
Department of Mathematics, University of Genoa
Chair: Hugo Herbelin
Notable parts of algebra and geometry can be formalized as coherent theories over first-order logic. Albeit wide, the class of coherent theories misses certain axioms in algebra such as the axioms of torsion abelian groups, Archimedean ordered fields, or the notion of transitive closure used in the theory of connected graphs and in the modelling of epistemic social notions such as common knowledge. All those examples can however be axiomatized by means of geometric axioms, a generalization of coherent axioms that includes infinitary disjunctions. We give a constructive proof of cut elimination for infinitary classical and intuitionistic sequent calculi for geometric theories. We then exploit their uniformity to obtain, purely by methods of structural proof theory, Glivenko-style conservativity results leading to the infinitary generalization of the first-order Barr theorem as a special case.
(Includes joint work with Giulio Fellin and Eugenio Orlandelli)
Event Timeslots (1)
Thursday
-
by Sara Negri
Leave a Comment