In [1], we established Gentzenizations for a good range of relevant logics with distribution, but, in the process, we added inversion rules, which involved extra structural connectives, and also added the sentential constantt. Instead of eliminating them, we used conservative extension results to relate them back to the original logics. In [4], we eliminated the inversion rules andtand established a much simpler Gentzenization for the weak sentential relevant logicDW, and also for its quantificational extensionDWQ, but a restriction to normal formulae (...) (defined below) was required to enable these results to be proved. This method was quite general and hope was expressed about extending it to other relevant logics.In this paper, we develop an innovative method, which makes essential use of this restriction to normality, to establish two simple Gentzenizations for the normal formulae of the slightly weaker logic B, and then extend the method to other sentential contraction-less logics. To obtain the first of these Gentzenizations, for the logicsBandDW, we remove the two branching rules (F&) and (T∨), together with the structural connective ‘,’, to simplify the elimination of the inversion rules andt. We then eliminate the rules (T&) and (F∨), thus reducing the Gentzen system to one containing only ˜ and → and their four associated rules, and reduce the remaining types of structures to four simple finite types. Subsequently, we re-introduce (T&) and (F∨), and also (F&) and (T∨), to obtain the second Gentzenization, which contains ‘,’ but no structural rules. (shrink)

In [1], we established Gentzenizations for a good range of relevant logics with distribution, but, in the process, we added inversion rules, which involved extra structural connectives, and also added the sentential constantt. Instead of eliminating them, we used conservative extension results to relate them back to the original logics. In [4], we eliminated the inversion rules andtand established a much simpler Gentzenization for the weak sentential relevant logicDW, and also for its quantificational extensionDWQ, but a restriction to normal formulae (...) (defined below) was required to enable these results to be proved. This method was quite general and hope was expressed about extending it to other relevant logics.In this paper, we develop an innovative method, which makes essential use of this restriction to normality, to establish two simple Gentzenizations for the normal formulae of the slightly weaker logic B, and then extend the method to other sentential contraction-less logics. To obtain the first of these Gentzenizations, for the logicsBandDW, we remove the two branching rules (F&) and (T∨), together with the structural connective ‘,’, to simplify the elimination of the inversion rules andt. We then eliminate the rules (T&) and (F∨), thus reducing the Gentzen system to one containing only ˜ and → and their four associated rules, and reduce the remaining types of structures to four simple finite types. Subsequently, we re-introduce (T&) and (F∨), and also (F&) and (T∨), to obtain the second Gentzenization, which contains ‘,’ but no structural rules. (shrink)

This paper proves decidability of a range of weak relevant logics using decision procedures based on the Routley-Meyer semantics. Logics are categorized as F-logics, for those proved decidable using a filtration method, and U-logics, for those proved decidable using a direct (unfiltered) method. Both of these methods are set out as reductio methods, in the style of Hughes and Cresswell. We also examine some extensions of the U-logics where the method fails and infinite sequences of worlds can be generated.