Premium
A Constructive Proof of a Theorem in Relevance Logic
Author(s) -
Kron Aleksandar
Publication year - 1985
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.19850312505
Subject(s) - relevance (law) , constructive , citation , mathematics , information retrieval , computer science , calculus (dental) , arithmetic , discrete mathematics , mathematical economics , library science , programming language , law , medicine , dentistry , process (computing) , political science
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)