The semantics of \(R4\) (Q1208151)

\(R\) is the Anderson-Belnap system of relevant implication; \(NR\) extends \(R\) with a necessity operator and \(S4\)-like postulates for it. \(R4\) is the result of adding the axiom scheme \(\square(A\vee B)\to(\diamondsuit A\vee\square B)\) to \(NR\) to make a system that includes all of \(S4\). This paper presents a model-theoretic semantics for \(R4\), and proves the system to be sound and complete with respect to this semantics. The semantics is a modification of semantics previously proposed for \(NR\) and follows the pattern of Routley-Meyer model-structures for relevance logics with the addition of a binary relation for alternative accessibility familiar from standard work in modal logic. The trick for \(R4\) is to design just the right postulates for this binary relation. That done, the proofs of soundness and completeness follow the usual procedures for relevance logics. It is also proved that there is a natural embedding of a Kripke model for \(S4\) in each \(R4\) model, and so \(R4\) is a conservative extension of \(S4\) as \(NR\) is not. The naturalness of the embedding suggests that \(R4\) is the appropriate way to combine the modal notions of \(S4\) with the relevance of \(R\).