Venerdì, 25 novembre 2022 ore 11
DILEF - Dipartimento di Lettere e Filosofia
via della Pergola 60, Firenze
Sala Altana
Giulio Fellin (Università di Verona)
Glivenko sequent classes and constructive cut elimination in geometric logics
(joint work with S. Negri, E. Orlandelli)
Abstract: A constructivisation of the cut-elimination proof for sequent calculi for classical, intuitionistic and minimal infinitary logics with geometric rules—given in earlier work by Sara Negri—is presented. This is achieved through a procedure where the non-constructive transfinite induction on the commutative sum of ordinals is replaced by two instances of Brouwer’s Bar Induction. The proof of admissibility of the structural rules is made ordinal-free by introducing a new well-founded parameter called proof embeddability. Additionally, conservativity for classical over intuitionistic/minimal logic for the seven (finitary) Glivenko sequent classes is here shown to hold also for the corresponding infinitary classes.