A decidable paraconsistent relevant logic: Gentzen system and Routley‐Meyer semantics

In this paper, the positive fragment of the logic of contraction‐less relevant implication is extended with the addition of a paraconsistent negation connective similar to the strong negation connective in Nelson's paraconsistent four‐valued logic . This extended relevant logic is called , and it has the property of constructible falsity which is known to be a characteristic property of . A Gentzen‐type sequent calculus for is introduced, and the cut‐elimination and decidability theorems for are proved. Two extended Routley‐Meyer semantics are introduced for , and the completeness theorems with respect to these semantics are proved.