This paper presents a sequent calculus for the positive relevant logic with necessity and a proof that it admits the elimination of cut.

This paper is a study of four subscripted Gentzen systems G u R +, G u T +, G u RW + and G u TW +. [16] shows that the first three are equivalent to the semilattice relevant logics u R +, u T + and u RW + and conjectures that G u TW + is, equivalent to u TW +. Here we prove Cut Theorems for these systems, and then show that modus ponens is admissible — which (...) is not so trivial as one normally expects. Finally, we give decision procedures for the contractionless systems, G u TW + and G u RW +. (shrink)

Substructural logics are logics obtained from a sequent formulation of intuitionistic or classical logic by rejecting some structural rules. The substructural logics considered here are linear logic, relevant logic and BCK logic. It is proved that first-order variants of these logics with an intuitionistic negation can be embedded by modal translations into S4-type extensions of these logics with a classical, involutive, negation. Related embeddings via translations like the double-negation translation are also considered. Embeddings into analogues of S4 are obtained with (...) the help of cut elimination for sequent formulations of our substructural logics and their modal extensions. These results are proved for systems with equality too. (shrink)

A method is presented for constructing natural deduction-style systems for propositional relevant logics. The method consists in first translating formulas of relevant logics into ternary relations, and then defining deduction rules for a corresponding logic of ternary relations. Proof systems of that form are given for various relevant logics. A class of algebras of ternary relations is introduced that provides a relation-algebraic semantics for relevant logics.