A Constructive Proof of a Theorem in Relevance Logic

In this paper we investigate a propositional systeni L related t o T,-W of relevance logic. It has been conjectured that for any formulas A and B (A) if A .+ B and B --f A are provable in T,-W, t'lien A and B are the same formula (ef. [l]. p. 95). (A) is known as BELXAP'S conjecture and it was proved by E. P. MARTIN and R. I<. J f E m R who used a suitable semantics (cf. [3] and [4]). w e give an indepenclent and purely constructive proof of (A). 1. T + W and the Dwyer's systems. The' only connective in T,-W is -+ and the set of formulas is defined as usual. A ? B, C, . . . range over the set of formulas. Instead of (-4 -+ R) we shall write (AB) and we shall use conventions about oniitting parenthews as in [2]. The axiom-schemes of T,-W are: (ID) .4d, (ASL-) -4B.BC.AC. (XPR) BC.AB.AC. Tlic. onljrule of inferencc is niodus ponens (NP)