Gentzenization and decidability of some contraction-less relevant logics (Q2277247)

This paper gives cut-free Gentzen systems and decision procedures for the relevant logics TW and DW by significantly extending and modifying the techniques used by the author in an earlier paper [ibid. 19, 35-73 (1990; Zbl 0697.03006)] to Gentzenize RW and show it decidable. TW, DW, and RW are the systems T, D and R without the contraction axiom (A\(\to.A\to B)\to.A\to B\), respectively. See \textit{R. Routley, V. Plumwood, R. K. Meyer} and the author [Relevant logics and their rivals, Vol. I (1983; Zbl 0579.03011)] for axiomatizations thereof. The Gentzenization of RW, mentioned above, utilizes signed formulae, i.e. formulae prefixed with a T or an F. Since the prefix T could easily be dropped, the use of F can be seen as a modification of the use of * of \textit{N. D. Belnap jun.} [J. Philos. Logic 11, 375-417 (1982; Zbl 0509.03008)]. The RW Gentzenization likewise employed the ``structural connectives''; and as given by \textit{J. M. Dunn} [in: Entailment. The logic of relevance and necessity. Vol. I (by \textit{A. R. Anderson} and \textit{N. D. Belnap jun.}), 381-391 (1975; Zbl 0323.02030)]. These structural connectives stand in for the systematic connectives of fusion and conjunction, respectively. With this apparatus in place, the real innovation came in doubling up on the introduction rules, the usual set for introducing unsigned formulae, i.e. those with the prefix T (actually, \(\sim\) introduction rules are the unusual ones of \textit{N. D. Belnap} [loc. cit.]), and a new set for introducing formulae prefixed with F. The new set of rules build in various forms of DeMorgan's Laws in the cases of \& and \(\vee\), and of contraposition and double negation in the cases of \(\to\) and \(\sim\). This allows the systems to be singular on the right. That this could be accomplished was foreshadowed by the proof of primeness of these systems, i.e. that a disjunction is provable iff at least one of the disjuncts is, by \textit{J. K. Slaney} [Stud. Logica 43, 159-168 (1984; Zbl 0576.03014)]. However, the form of the new \(\to\) rules for RW depended on the provable RW equivalence \(A\circ B\leftrightarrow \sim (A\to \sim B)\), which is not provable in TW nor in DW. The problem is solved in this paper by adding another structural connective, ``:'', letting it stand in for the systematic connective \(\oplus\) which is defined by \(A\oplus B=\sim (A\to \sim B)\). It is fitted with the appropriate structural rules \(C\vdash\), \(B\vdash\) and \(B'\vdash\). The general strategy of the paper is an adaptation of that of the reviewer [J. Philos. Logic 14, 235-254 (1985; Zbl 0587.03014)]. The Gentzenizations are first formulated with the logical constant t, allowing for a proof of Cut as given by \textit{J. M. Dunn} [loc. cit.], which has become the standard technique for Cut Theorems for positive and/or contractionless relevant logics. He then uses modified versions of the technique and proof given by the reviewer [loc. cit.] (which conjectured the decidability of TW) to remove the constant t and show decidability. The system TW with the constant t was shown to be undecidable by \textit{A. Urquhart} [J. Symb. Logic 49, 1059- 1073 (1984; Zbl 0581.03011)].