New Consecution Calculi for R→t
Katalin Bimbó, Jon Michael Dunn · Notre Dame Journal of Formal Logic · 2012
The implicational fragment of the logic of relevant implication, R→ is one of the oldest relevance logics and in 1959 was shown by Kripke to be decidable. The proof is based on LR→, a Gentzen-style calculus. In this paper, we add the truth constant t to LR→, 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 t. This calculus, LT→ⓣ, extends the consecution calculus LT→t formalizing the implicational fragment of ticket entailment. We introduce two other new calculi as alternative formulations of R→t. For each new calculus, we prove the cut theorem as well as the equivalence to the original Hilbert-style axiomatization of R→t. These results serve as a basis for our positive solution to the long open problem of the decidability of T→, which we present in another paper.