A decidable paraconsistent relevant logic: Gentzen system and Routley-Meyer semantics (Q2813672)

This paper introduces the logic RWP that extends the positive relevance logic RW\(^+\) for relevant implication without contraction to include a strong paraconsistent negation from Nelson's four-valued N4. RWP is defined as a Hilbert-style axiomatic system and, importantly, as an equivalent Gentzen-style sequent calculus, SRWP. The latter is shown to be embeddable in SRW\(^+\), a sequent formulation of RW\(^+\). Since SRW\(^+\) is known to satisfy cut-elimination, to be decidable, and to possess the variable-sharing property, those results extend to SRWP and hence to RWP. In addition, the paper provides two forms of Routley-Meyer ternary semantics for this system, one based on a dual satisfaction relation with \(\models^+\) and \(\models^-\), the other with a variation on the Routley star-operation. For the first form, RWP and SRWP are shown to be (weakly) complete by embedding their models into models for RW\(^+\). For the second form, RWP and SRWP are shown to be (weakly) complete by embedding their models into models of the first form.