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.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.