A metacompleteness theorem for contraction-free relevant logics

Abstract

I note that the logics of the "relevant" group most closely tied to the research programme in paraconsistency are those without the contraction postulate (A→.A→B)→.A→B and its close relatives. As a move towards gaining control of the contraction-free systems I show that they are prime (that whenever A ∨B is a theorem so is either A or B). The proof is an extension of the metavaluational techniques standardly used for analogous results about intuitionist logic or the relevant positive logics. Show more