New consecution calculi for Rt→

Abstract

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→(t), 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. © 2012 by University of Notre Dame.