The implicational fragment of $R$-mingle
Saburo Tamura · Proceedings of the Japan Academy Series A Mathematical Sciences · 1971
The relevant logic R was first defined in Belnap [1] though the implicational ragment o R which we refer to as RI in this note goes back to Church's weak implication [2].Kripke [3] constructed "Sequenzen-kalktil" equivalent to RI. Anderson and Belnap [4] and the author [5] gave systems of the natural deduction equivalent to RI.By adding a mingle axiom a(cra) to R, we get a system R-mingle RM (defined by Meyer and Dunn [6]).Here the mingle axiom has the effect of Gentzen type "mingle" rule introduced by Ohnishi and Matsumoto [7].In this note we shall give a system of the natural deduction equivalent to RMI, that is, the implicational fragment of RM.And then we shall show that the cut elimination theorem holds in Sequenzen- kalktil equivalent to RMI.Finally we shall give the decision procedure