Notre Dame Journal of Formal Logic 53 (4):491-509 (2012)

Katalin Bimbo
University of Alberta
Jon Michael Dunn
Indiana University, Bloomington
The implicational fragment of the logic of relevant implication, $R_{\to}$ is one of the oldest relevance logics and in 1959 was shown by Kripke to be decidable. The proof is based on $LR_{\to}$ , a Gentzen-style calculus. In this paper, we add the truth constant $\mathbf{t}$ to $LR_{\to}$ , but more importantly we show how to reshape the sequent calculus as a consecution calculus containing a binary structural connective, in which permutation is replaced by two structural rules that involve $\mathbf{t}$ . This calculus, $LT_\to^{\text{\textcircled{$\mathbf{t}$}}}$ , extends the consecution calculus $LT_{\to}^{\mathbf{t}}$ formalizing the implicational fragment of ticket entailment . We introduce two other new calculi as alternative formulations of $R_{\to}^{\mathbf{t}}$ . For each new calculus, we prove the cut theorem as well as the equivalence to the original Hilbert-style axiomatization of $R_{\to}^{\mathbf{t}}$ . These results serve as a basis for our positive solution to the long open problem of the decidability of $T_{\to}$ , which we present in another paper.
Keywords relevance logics   Ackermann constants   sequent calculi   admissibility of cut   ticket entailment
Categories (categorize this paper)
DOI 10.1215/00294527-1722719
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 55,856
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

No references found.

Add more references

Citations of this work BETA

A Cut-Free Sequent Calculus for Relevant Logic RW.M. Ili & B. Bori I. - 2014 - Logic Journal of the IGPL 22 (4):673-695.
An Alternative Gentzenisation of RW+∘.Mirjana Ilić - 2016 - Mathematical Logic Quarterly 62 (6):465-480.

View all 6 citations / Add more citations

Similar books and articles

Bunched Logics Displayed.James Brotherston - 2012 - Studia Logica 100 (6):1223-1254.
Cut-Free Sequent Calculi for Some Tense Logics.Ryo Kashima - 1994 - Studia Logica 53 (1):119 - 135.
Gentzen's Proof Systems: Byproducts in a Work of Genius.Jan von Plato - 2012 - Bulletin of Symbolic Logic 18 (3):313-367.
Types of I -Free Hereditary Right Maximal Terms.Katalin Bimbó - 2005 - Journal of Philosophical Logic 34 (5/6):607 - 620.
A Note on the Proof Theory the λII-Calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
Implicational F-Structures and Implicational Relevance Logics.A. Avron - 2000 - Journal of Symbolic Logic 65 (2):788-802.


Added to PP index

Total views
22 ( #467,303 of 2,401,722 )

Recent downloads (6 months)
1 ( #551,964 of 2,401,722 )

How can I increase my downloads?


My notes