A constructivisation of the cut-elimination proof for sequent calculi for classical, intu- itionistic and minimal infinitary logics with geometric rules—given in earlier work by the second author—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 struc- tural rules is made ordinal-free by introducing a new well-founded relation based on a notion of embeddability of derivations. 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.

Glivenko sequent classes and constructive cut elimination in geometric logics / Fellin, Giulio; Negri, Sara; Orlandelli, Eugenio. - In: ARCHIVE FOR MATHEMATICAL LOGIC. - ISSN 0933-5846. - ELETTRONICO. - online first:(2022), pp. 1-32. [10.1007/s00153-022-00857-z]

Glivenko sequent classes and constructive cut elimination in geometric logics

Orlandelli, Eugenio
Co-primo
Writing – Original Draft Preparation
2022

Abstract

A constructivisation of the cut-elimination proof for sequent calculi for classical, intu- itionistic and minimal infinitary logics with geometric rules—given in earlier work by the second author—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 struc- tural rules is made ordinal-free by introducing a new well-founded relation based on a notion of embeddability of derivations. 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.
2022
Glivenko sequent classes and constructive cut elimination in geometric logics / Fellin, Giulio; Negri, Sara; Orlandelli, Eugenio. - In: ARCHIVE FOR MATHEMATICAL LOGIC. - ISSN 0933-5846. - ELETTRONICO. - online first:(2022), pp. 1-32. [10.1007/s00153-022-00857-z]
Fellin, Giulio; Negri, Sara; Orlandelli, Eugenio
File in questo prodotto:
File Dimensione Formato  
AML_InfGlivenko-2.pdf

Open Access dal 09/12/2023

Descrizione: Articolo
Tipo: Postprint
Licenza: Licenza per Accesso Aperto. Creative Commons Attribuzione - Non commerciale - Condividi allo stesso modo (CCBYNCSA)
Dimensione 1.43 MB
Formato Adobe PDF
1.43 MB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/909326
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 3
social impact