Cut Elimination for GLS Using the Terminability of its Regress Process

Journal of Philosophical Logic 45 (2):147-153 (2016)
  Copy   BIBTEX

Abstract

The system GLS, which is a modal sequent calculus system for the provability logic GL, was introduced by G. Sambin and S. Valentini in Journal of Philosophical Logic, 11, 311–342,, and in 12, 471–476,, the second author presented a syntactic cut-elimination proof for GLS. In this paper, we will use regress trees in order to present a simpler and more intuitive syntactic cut derivability proof for GLS1, which is a variant of GLS without the cut rule

Categories

Keywords

Reprint years

DOI

10.1007/s10992-015-9368-4

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,322

External links

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

Through your library

My notes

Similar books and articles

Cut-elimination Theorems of Some Infinitary Modal Logics.Yoshihito Tanaka - 2001 - Mathematical Logic Quarterly 47 (3):327-340.
A Cut-free Gentzen Formulation Of The Modal Logic S5.T. Braüner - 2000 - Logic Journal of the IGPL 8 (5):629-643.
Syntactic cut-elimination for a fragment of the modal mu-calculus.Kai Brünnler & Thomas Studer - 2012 - Annals of Pure and Applied Logic 163 (12):1838-1853.
A note on the proof theory the λII-calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
Modal Tree‐Sequents.Claudio Cerrato - 1996 - Mathematical Logic Quarterly 42 (1):197-210.
A cut-elimination proof in intuitionistic predicate logic.Mirjana Borisavljević - 1999 - Annals of Pure and Applied Logic 99 (1-3):105-136.
Cut-elimination for Weak Grzegorczyk Logic Go.Rajeev Goré & Revantha Ramanayake - 2014 - Studia Logica 102 (1):1-27.
Cut Might Cautiously.Jaap van der Does - 1995 - Logic Journal of the IGPL 3 (2-3):191-202.
Deep sequent systems for modal logic.Kai Brünnler - 2009 - Archive for Mathematical Logic 48 (6):551-577.
A cut-free Gentzen formulation of basic propositional calculus.Kentaro Kikuchi & Katsumi Sasaki - 2003 - Journal of Logic, Language and Information 12 (2):213-225.
Syntactic cut-elimination for common knowledge.Kai Brünnler & Thomas Studer - 2009 - Annals of Pure and Applied Logic 160 (1):82-95.
Sufficient conditions for cut elimination with complexity analysis.João Rasga - 2007 - Annals of Pure and Applied Logic 149 (1-3):81-99.
Cut‐Elimination Theorem for the Logic of Constant Domains.Ryo Kashima & Tatsuya Shimura - 1994 - Mathematical Logic Quarterly 40 (2):153-172.
An approach to infinitary temporal proof theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.
A proof-theoretic treatment of λ-reduction with cut-elimination: λ-calculus as a logic programming language.Michael Gabbay - 2011 - Journal of Symbolic Logic 76 (2):673 - 699.

Analytics

Added to PP
2015-03-26

Downloads
33 (#470,805)

6 months
11 (#226,803)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Cut elimination by unthreading.Gabriele Pulcini - 2023 - Archive for Mathematical Logic 63 (1):211-223.
Tautology Elimination, Cut Elimination, and S5.Andrezj Indrzejczak - 2017 - Logic and Logical Philosophy 26 (4):461-471.

Add more citations

References found in this work

Basic proof theory.A. S. Troelstra - 1996 - New York: Cambridge University Press. Edited by Helmut Schwichtenberg.
Mathematical logic.Stephen Cole Kleene - 1967 - Mineola, N.Y.: Dover Publications.
Solution of a problem of Leon Henkin.M. H. Löb - 1955 - Journal of Symbolic Logic 20 (2):115-118.
Provability Interpretations of Modal Logic.Robert M. Solovay - 1981 - Journal of Symbolic Logic 46 (3):661-662.
The modal logic of provability. The sequential approach.Giovanni Sambin & Silvio Valentini - 1982 - Journal of Philosophical Logic 11 (3):311 - 342.

View all 9 references / Add more references