Abstract

The author gentzenizes the positive fragments T₊ and R₊ of relevant T and R using formulas with prefixes (subscripts). There are three main Gentzen formulations of $S_{+}\in \{T_{+},R_{+}\}$ called W₁ S₊, W₂ S₊ and G₂ S₊. The first two have the rule of modus ponens. All of them have a weak rule DL for disjunction introduction on the left. DL is not admissible in S₊ but it is needed in the proof of a cut elimination theorem for G₂ S₊. W₁ S₊ has a weak rule of weakening W₁ and it is not closed under a general transitivity rule. This allows the proof that $\vdash A$ in S₊ iff $\vdash A$ in W₁ S₊. From the cut elimination theorem for G₂ S₊ it follows that if $\vdash A$ in S₊, then $\vdash A$ in G₂ S₊. In order to prove the converse, W₂ S₊ is needed. It contains modus ponens, transitivity, and a restricted weakening rule. G₂ S₊ is contained in W₂ S₊ and there is a proof that $\vdash A$ in W₂ S₊ iff $\vdash A$ in W₁ S₊.