Glivenko sequent classes and constructive cut elimination in geometric logics

Archive for Mathematical Logic 62 (5):657-688 (2023)
  Copy   BIBTEX

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

Other Versions

No versions found

Links

PhilArchive

    This entry is not archived by us. If you are the author and have permission from the publisher, we recommend that you archive it. Many publishers automatically grant permission to authors to archive pre-prints. By uploading a copy of your work, you will enable us to better index it, making it easier to find.

    Upload a copy of this work     Papers currently archived: 104,706

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Glivenko sequent classes in the light of structural proof theory.Sara Negri - 2016 - Archive for Mathematical Logic 55 (3-4):461-473.
Proof analysis in intermediate logics.Roy Dyckhoff & Sara Negri - 2012 - Archive for Mathematical Logic 51 (1):71-92.
Simple cut elimination proof for hybrid logic.Andrezj Indrzejczak - 2016 - Logic and Logical Philosophy 25 (2):129-141.

Analytics

Added to PP
2022-12-21

Downloads
38 (#658,353)

6 months
8 (#528,679)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

Eugenio Orlandelli
University of Bologna

References found in this work

Proof Theory.Gaisi Takeuti - 1990 - Studia Logica 49 (1):160-161.
Cut Elimination in the Presence of Axioms.Sara Negri & Jan Von Plato - 1998 - Bulletin of Symbolic Logic 4 (4):418-435.
Glivenko sequent classes in the light of structural proof theory.Sara Negri - 2016 - Archive for Mathematical Logic 55 (3-4):461-473.

View all 9 references / Add more references