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

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 99,484

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

A Proof Theory for the Logic of Provability in True Arithmetic.Hirohiko Kushida - 2020 - Studia Logica 108 (4):857-875.
A formalization of Sambins's normalization for GL.Edward Hermann Haeusler & Luiz Carlos Pereira - 1993 - Mathematical Logic Quarterly 39 (1):133-142.
A Short and Readable Proof of Cut Elimination for Two First-Order Modal Logics.Feng Gao & George Tourlakis - 2015 - Bulletin of the Section of Logic 44 (3/4):131-147.
Cut-elimination for Weak Grzegorczyk Logic Go.Rajeev Goré & Revantha Ramanayake - 2014 - Studia Logica 102 (1):1-27.
A purely syntactic and cut-free sequent calculus for the modal logic of provability.Francesca Poggiolesi - 2009 - Review of Symbolic Logic 2 (4):593-611.
A Formalization Of Sambins's Normalization For Gl.Edward Hauesler & Luiz Carlos Pereira - 1993 - Mathematical Logic Quarterly 39 (1):133-142.
Cut-elimination Theorems of Some Infinitary Modal Logics.Yoshihito Tanaka - 2001 - Mathematical Logic Quarterly 47 (3):327-340.
Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 43-66.
On the proof-theory of a first-order extension of GL.Yehuda Schwartz & George Tourlakis - 2014 - Logic and Logical Philosophy 23 (3).
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.

Analytics

Added to PP
2015-03-26

Downloads
39 (#468,807)

6 months
5 (#898,127)

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