A metacompleteness theorem for contraction-free relevant logics (Q1064316)

Three of the weaker relevant logics, RW (also sometimes called C or R-W), EW and TW, are shown to have the disjunction (primeness) property that whenever a disjunction is a theorem so is at least one if its disjuncts. Systems previously known to have this property have mostly been close relatives of intuitionist logic, or else have been fragmentary (e.g. positive) logics. The three in this paper, however, have the theorem scheme DN:\(\sim \sim A\to A\), which makes their primeness harder to establish and more interesting. The proof uses a 'metavaluation' in the sense of \textit{R. K. Meyer} [Notre Dame J. Formal Logic 17, 501-516 (1976; Zbl 0232.02015)] but with the difference that the governing algebra is not the two-valued 'truth tables' but for RW and EW the three-valued matrix of \({\L}ukasiewicz\) and for TW a related three-valued matrix. It is essential to the result that the logics concerned do not validate the contraction (or absorption) postulate W:(A\(\to.A\to B)\to.A\to B\) for in the context of logics like RW this suffices to generate the law of the excluded middle LEM:A\(\vee \sim A\) from DN, and LEM is of course fatal to metacompleteness and to the disjunction property. A later paper by the author [Reduced models for relevant logics without WI, Notre Dame J. Formal Logic (to appear)] extends and deepens these results.