\(TW_+\) and \(RW_+\) are decidable (Q1072541)

This paper provides consecution calculi (Gentzen systems) and decision procedures for the contractionless relevant logics \(TW_+\) and \(RW_+\), which are, respectively, the positive fragments of the systems T of ticket entailment and R of relevant implication without the contraction axiom \((A\to.A\to B)\to.A\to B\). The decision procedures are proof- theoretic in character and based upon the Gentzen systems provided. Aside from the inherent interest of contractionless relevant logics, these results are significant for at least two other reasons. In the first place, consecution calculi for full positive relevant logics are of a higher order of complexity than the usual ones, e.g., those for classical and intuitionistic logic. This is the first time such complex systems have been successfully used to obtain major results. Further, \(TW_+\) and \(RW_+\) will be nearly the strongest decidable relevant logics, as is indicated by \textit{A. Urquhart}'s ''The undecidability of entailment and relevant implication'' [J. Symb. Logic 49, 1059-1073 (1984; Zbl 0581.03011)] in which it is shown that even the deducibility problem for \(TW_+\) is undecidable.