The past century has witnessed the flourishing of many a new logical tradition, each developing along its own lines, yet with analogies identified and formalized through translation.

A classic example is the Gödel–McKinsey–Tarski translation of intuitionistic propositional logic into classical modal logic, which has fostered a rich exchange of ideas, results, and research questions [@ChagrovZ97:ml]; its original intent of demonstrating how intuitionistic logic can be interpreted classically now seems the least of its impact.

The present paper pursues a similar, though more modest, aim for another pair of traditions: relevant logic as conceived in the Anderson–Belnap lineage and modal logic as studied in the theory of normal modal logic.

Our main contributions are full and faithful translations from relevant logics into normal modal logics. We leave aside discussion of philosophical differences and motivations, though we hope that the translations shall as well be conceptually clarifying. We also use the translations to sample a few corollary results and raise some questions, but leave a fuller analysis for future work.

The paper proceeds by developing a series of translations, starting with the relevant vocabulary \(\{\land, \lor, \to\}\) and gradually adding \(\mathsf{t}, \circ,\) and \(\neg\).

1 A basic positive translation↩︎

1.1 Preliminaries↩︎

We begin by presenting relevant logics axiomatically.¹ As we, at first, will be concerned with translating the \(\{\land, \lor, \to\}\)-fragment of the relevant language, sometimes called the positive fragment, we set out only the axioms and rules pertaining to this language.

The weakest logic of concern will be the basic relevant logic \(\mathbf{B}\). It stands to relevant logic much like how \(\mathbf{K}\) stands to modal logic – a point which our first translations will help refine. Its \(\{\land, \lor, \to\}\)-fragment, often denoted \(\mathbf{B}^+\), admits the following Hilbert-style axiomatization. (We follow the convention that \(\land, \lor\) bind tighter than \(\to\).)

Axiom schemes

Rules

The following axiom schemes serve to axiomatize many of the more common stronger relevant logics.

1. \((\varphi\to\psi)\to[(\chi\to\varphi)\to(\chi\to\psi)]\) (prefixing)

2. \((\varphi\to\psi)\to [(\psi\to\chi)\to(\varphi\to\chi)]\) (suffixing)

3. \((\varphi\to\psi)\land (\psi\to\chi)\to (\varphi\to\chi)\) (hypothetical syllogism)

4. \(\varphi\land(\varphi\to\psi)\to\psi\) (pseudo-modus ponens)

5. \([\varphi\to(\varphi\to\psi)]\to(\varphi\to\psi)\) (contraction)

6. \(\varphi\to[(\varphi\to\psi)\to\psi]\) (assertion)

For instance, all of these are theorems of the \(\{\land, \lor, \to\}\)-fragment of \(\mathbf{R}\), denoted \(\mathbf{R}^+\), and already \(\{8., 11., 12.\}\) axiomatize \(\mathbf{R}^+\) relative to \(\mathbf{B}^+\); that is, \[\mathbf{R}^+=\mathbf{B}^+\oplus\{7., \ldots,12.\}=\mathbf{B}^+\oplus\{8.,11.,12.\},\] where we, for a set of formulas \(\Phi\), by the notation \(\mathbf{B}^+\oplus \Phi\) mean the result of adding \(\Phi\) (as axiom schemes) to \(\mathbf{B}^+\) and closing under the above rules. Note that in the presence of the prefixing and suffixing axioms (7. and 8., respectively), the namesake rules become redundant; for example, only the rules of modus ponens and adjunction are needed to axiomatize \(\mathbf{R}^+\). The same holds for each of the following relevant logics: \[\begin{align} \mathbf{TW}^+&\mathrel{:=} \mathbf{B}^+\oplus \{7.,8.\} &\qquad \mathbf{TWJ}^+&\mathrel{:=}\mathbf{B}^+\oplus \{7., 8., 9.\}&\qquad \mathbf{C}^+&\mathrel{:=}\mathbf{B}^+\oplus\{7.,8.,10.\} \\ \mathbf{T}^+&\mathrel{:=} \mathbf{B}^+\oplus \{7.,8., 11.\}&\qquad \mathbf{RW}^+&\mathrel{:=}\mathbf{B}^+\oplus\{7.,8.,12.\} \end{align}\] One major relevant logic not axiomatizable via 7.-12. is Anderson and Belnap’s logic of entailment \(\mathbf{E}\). It is most perspicuously presented when additional vocabulary is available. Here, we make do by setting out \(\mathbf{E}^+\) as \(\mathbf{T}^+\) plus the less than elegant pair: \[\begin{align} ((\varphi\to\varphi)\to \psi)\to \psi, \qquad [((\varphi\to\varphi)\to\varphi)\land ((\psi\to\psi)\to\psi)]\to [(\varphi\land \psi\to\varphi\land \psi)\to\varphi\land \psi].\footnotemark \end{align}\] Both are theorems of \(\mathbf{R}^+\), so \(\mathbf{E}^+\) is a sublogic of \(\mathbf{R}^+\). More generally, the introduced logics are ordered by strength as presented in Figure 5.

To situate the relevant family within a bigger logical realm, let us note that the \(\{\land, \lor, \to\}\)-fragment of intuitionistic propositional logic \(\mathbf{IPL}\) results from adding to \(\mathbf{R}^+\) the axiom schema \(\varphi\to (\psi\to\varphi)\).² If one further adds Peirce’s law \(((\varphi\to\psi)\to \varphi)\to \varphi\), one gets the \(\{\land, \lor, \to\}\)-fragment of classical propositional logic \(\mathbf{CPL}\); in fact, over \(\mathbf{R}^+\), from Peirce’s law we already derive \(\varphi\to (\psi\to\varphi)\) [@Meyer90].³

From the above axiomatic presentation, it is not at all clear what affinities relevant logic shares with modal logic (unless we count their equally confusing nomenclature). This is made somewhat clearer by their relational semantics.

Formulas of the positive relevant language are interpreted on Routley–Meyer frames and models:

Validity is defined with respect to normal points: \(\varphi\) is valid on a Routley–Meyer frame \(\mathfrak{F}=(K, R, N)\), written \(\mathfrak{F}\Vdash \varphi\), if for all persistent valuations \(V\) and normal points \(n\in N\), \((\mathfrak{F}, V), n\Vdash \varphi\); and \(\varphi\) is valid on a class of frames \(\mathcal{C}\), written \(\mathcal{C}\Vdash \varphi\), if \(\varphi\) is valid on each frame \(\mathfrak{F}\in \mathcal{C}\). A handy fact, readily proven using persistence (\(\mathfrak{M},x\Vdash \varphi\) and \(x\leq y\) imply \(\mathfrak{M},y\Vdash \varphi\)) and reflexivity of \(\leq\), is that for any frame \(\mathfrak{F}=(K, R, N)\) and implication \(\varphi\to\psi\), \[\begin{align} \mathfrak{F}\Vdash \varphi\to\psi\quad \text{iff}\quad \text{for all x\in K and persistent valuations V: if (\mathfrak{F}, V),x\Vdash \varphi, then (\mathfrak{F}, V),x\Vdash \psi.}\label{eq:handyfact} \end{align}\tag{1}\] The set of validities on all Routley–Meyer frames is the basic relevant logic \(\mathbf{B}^+\). For the axioms 7.-12., we list their frame correspondents below, which facilitate completeness for other relevant logics with respect to the corresponding classes of frames (as the formulas are canonical). There, we use a convenient equivalence between a ternary relation \(R\subseteq K^3\) and a function \(\cdot:K^2\to \mathcal{P}(K)\) defined by \(z\in x\cdot y\) iff \(Rxyz\) and lifted to arbitrary sets \(X, Y\subseteq K\) by \(X\cdot Y\mathrel{:=}\bigcup_{x\in X, y\in Y}x\cdot y.\)

With this, we turn to the target modal logic.⁴ The language is the modal language with a single binary modality \(\Diamond\); that is, the language generated by the grammar \[\varphi\mathrel{::=} \bot| \top |p |\neg\varphi|\varphi\lor\varphi|\Diamond(\varphi,\varphi).\] Conjunction ‘\(\land\)’ and material implication ‘\(\supset\)’ are defined in the usual way.

Semantics for the modal language are provided by Kripke frames – pairs \(\mathbb{F}=(W,R)\) such that \(R\subseteq W^3\) – and Kripke models \(\mathbb{M}=(\mathbb{F},V)\), which are frames \(\mathbb{F}=(W,R)\) with a valuation \(V:\mathsf{Prop}\to \mathcal{P}(W)\). The semantic clauses are the usual ones. As it will make later proofs simpler, we follow the convention that the modality is evaluated at the first point of a triple \((w,v,u)\in R\); i.e., given a model \(\mathbb{M}=(W,R,V)\) and a point \(w\in W\), \[\begin{align} &\mathbb{M},w\vDash \Diamond(\varphi,\psi) && \text{iff} && \text{there exist v,u\in W such that Rwvu, } \mathbb{M},v\vDash \varphi,\text{ and } \mathbb{M},u\vDash \psi. \end{align}\] Having in mind the Routley–Meyer clause for implication, it is particularly suggestive to observe that \[\begin{align} &\mathbb{M},w\vDash \neg \Diamond(\varphi,\neg \psi) && \text{iff} && \text{for all v,u\in W: if Rwvu and } \mathbb{M}, v\Vdash \varphi\text{, then } \mathbb{M}, u\Vdash \psi.\label{eq:defImp} \end{align}\tag{2}\] The set of validities on all frames is the least normal modal logic \(\mathbf{K}_2\), the analog of \(\mathbf{K}\) in the language with a binary, rather than unary, diamond. Given a set of modal formulas \(\Phi\), we write \(\mathbf{K}_2\oplus \Phi\) for the least normal modal logic containing \(\Phi\).

1.1.0.1 Notation.

We maintain a notational distinction between our two semantic frameworks: we reserve the symbol ‘\(\Vdash\)’ and fraktur letters (\(\mathfrak{M}\)) for Routley–Meyer models, and the symbol ‘\(\vDash\)’ and blackboard bold letters (\(\mathbb{M}\)) for Kripke models. Also, given a formula \(\varphi\) in the relevant language and a class of Routley–Meyer frames \(\mathcal{C}\), we write \(\mathcal{C}\Vdash\varphi\) if \(\varphi\) is valid on \(\mathcal{C}\); and for the analogous notion in the modal setting, we write \(\mathcal{C}\vDash\varphi\). However, in both frameworks ‘\(\vdash\)’ denotes derivability (or theoremhood) and subscripts indicate the logic, i.e., for a relevant logic \(\mathbf{L}\), we write \(\vdash_{\mathbf{L}}\varphi\) if \(\varphi\) is a theorem of \(\mathbf{L}\); and for modal logics \(\mathbf{M}\), we likewise write \(\vdash_{\mathbf{M}}\varphi\).

1.2 Proof outline↩︎

The first goal is to define a translation \(^\star\) such that for all formulas \(\varphi, \psi\) of the positive relevant language, \[\begin{align} \vdash_{\mathbf{B}^+}\varphi\to \psi\qquad \text{iff}\qquad \vdash_{\mathbf{K}_2}\varphi^\star\supset\psi^\star.\label{basictr} \end{align}\tag{3}\] Afterwards, we extend the translation across further relevant logics and then to arbitrary formulas in the positive language (not only those with main connective \(\to\)). In a later section, we will also translate relevant logics in languages with additional relevant vocabulary. We proceed to outline the proof strategy but defer most proof steps to the appendix. The proof will be carried out semantically by defining a function \(F\) that takes pointed Kripke models (model-world pairs \(\mathbb{M},w\)) and returns pointed Routley–Meyer models (model-point pairs \(\mathfrak{M},x\)), subject to the following adjunction pattern: \[\begin{align} F(\mathbb{M},w)&\Vdash \alpha\qquad \text{iff}\qquad \mathbb{M},w\vDash \alpha^\star.\footnotemark\label{eq:chu} \end{align}\tag{4}\] This ensures left-to-right of 3 (fullness of the translation): if \(\mathbb{M},w\vDash \varphi^\star\), then \(F(\mathbb{M},w)\Vdash \varphi\), whence \(\vdash_{\mathbf{B}^+}\varphi\to \psi\) (and soundness for \(\mathbf{B}^+\)) imply \(F(\mathbb{M},w)\Vdash \psi\) (cf. 1 ), so we have \(\mathbb{M},w\vDash \psi^\star\), which suffices by completeness for \(\mathbf{K}_2\).

For the converse direction (faithfulness, or conservativity, of the translation), it suffices to show that \(F\) is essentially surjective, up to satisfaction equivalence; i.e., that for all pointed Routley–Meyer models \((\mathfrak{M},x)\), there is a pointed Kripke model \((\mathbb{M},w)\) such that for all \(\alpha\), \[\mathfrak{M},x\Vdash \alpha \qquad \text{iff}\qquad F(\mathbb{M},w)\Vdash \alpha.\] It will, however, be more convenient (and equivalent) to directly define a function \(G\) that takes pointed Routley–Meyer models and returns pointed Kripke models, subject to the following: \[\begin{align} \mathfrak{M},x&\Vdash \alpha\qquad \text{iff}\qquad G(\mathfrak{M},x)\vDash \alpha^\star.\label{eq:faithfulness} \end{align}\tag{5}\] Then, whenever \(\mathfrak{M},x\Vdash \varphi\), we also have \(G(\mathfrak{M},x)\vDash \varphi^\star\), so from \(\vdash_{\mathbf{K}_2}\varphi^\star\supset \psi^\star\) (and soundness for \(\mathbf{K}_2\)) we get \(G(\mathfrak{M},x)\vDash \psi^\star\), hence \(\mathfrak{M},x\Vdash \psi\), which, by 1 and completeness for \(\mathbf{B}^+\), is as required.

In sum, we shall define a triple consisting of a translation of formulas \(^\star\) and two model transformations \(F:\{(\mathbb{M},w)\} \rightleftarrows \{(\mathfrak{M},x)\}:G\) fulfilling 4 and 5 .

1.3 Basic translation↩︎

We define \(^\star\) as follows, using an abbreviated operator in the modal language \(\cdot \to\cdot \mathrel{:=}\neg \Diamond(\cdot, \neg\cdot)\) (recall 2 ).\[\begin{align} p^\star &&\mathrel{:=}&& &p && && && (\varphi\lor \psi)^\star&&\mathrel{:=}&& \varphi^\star \lor \psi^\star\\ (\varphi\to \psi)^\star&&\mathrel{:=}&& &\varphi^\star\to\psi^\star && && && (\varphi\land \psi)^\star&&\mathrel{:=}&& \varphi^\star\land \psi^\star. \end{align}\]

Next, we show how the \(^\star\)-translation extends, and fails to extend, to further relevant logics. For this, we use a modal version of Proposition [pr:Relcorrespondence] and the earlier identification of ternary relations \(R\subseteq W^3\) with functions \(\cdot:W^2\to\mathcal{P}(W)\).

Moreover, by again mirroring proofs from relevant logic, one can use the right-hand side conditions to show that the left-hand side translated formulas are canonical. Consequently, each modal logic axiomatized by any subset of the listed translated formulas is complete with respect to the corresponding class of frames. This observation is helpful in extending Theorem 1 to stronger relevant logics. In particular, we have the following, where we, given a set of relevant formulas \(\Phi\), write \(\Phi^\star\mathrel{:=}\{\alpha^\star\supset \beta^\star\mid \alpha\to\beta\in\Phi\}\).

Thus the \(^\star\)-translation not only ties together the basic relevant logic \(\mathbf{B}^+\) with the basic modal logic \(\mathbf{K}_2\), it also translates a greater family of relevant reasoning systems that includes \(\mathbf{TW}^+, \mathbf{TWJ}^+\), and \(\mathbf{C}^+\). However, as we shall see, it fails to meet the translation criterion of ?? for other sets of relevant axioms \(\Phi\); notably, Theorem 2 states \(\Phi\subseteq \{7., \ldots, 10.\}\), excluding 11. and 12. (contraction and assertion). We will get back to this below, but let us first ameliorate another shortcoming of the translation as so-far proposed: it only translates formulas with main connective \(\to\) (cf. 3 ). This will be particularly instructive in elucidating a subtlety in how relevant implications behave differently when nested.

1.4 Nested implication, nested translation↩︎

To extend Theorem 1 to formulas with main connectives other than \(\to\), we define a second-layer translation \(^\ast\), using the abbreviated modal operator \(\Box_\to\varphi\mathrel{:=}\top \to \varphi\). \[\begin{align} p^\ast &&\mathrel{:=}&& &p && && && (\varphi\lor \psi)^\ast&&\mathrel{:=}&& \varphi^\ast \lor \psi^\ast\\ (\varphi\to \psi)^\ast&&\mathrel{:=}&& &\Box_\to (\varphi^\star\supset\psi^\star) && && && (\varphi\land \psi)^\ast&&\mathrel{:=}&& \varphi^\ast\land \psi^\ast. \end{align}\] As we now prove, the \(^\ast\)-translation is full and faithful for \(\mathbf{B}^+\) and \(\mathbf{K}_2\), thereby tightening the connection between the two: \(\mathbf{B}^+\) is realized as a syntactic fragment of \(\mathbf{K}_2\).

The translation makes precise a sense in which relevant logic draws a qualitative distinction between conditionals within the scope of another conditional (where the \(^\star\)-translation is in force) and those outside it (where \(^\ast\) is in force). Note that the latter resemble intuitionistic conditionals – which perhaps becomes particularly evident upon recalling the Gödel–McKinsey–Tarski translation of \(\mathbf{IPL}\) into the modal logic \(\mathbf{S4}\) – and both traditions invalidate \((p\to q)\lor (q\to p)\) in much the same manner.⁶

As with the \(^\star\)-translation, \(^\ast\) can be extrapolated along the lines of Theorem 2:

Of course, one might here prefer to replace \(\Phi^\star\) with \(\Phi^\ast\mathrel{:=}\{\alpha^\ast\mid \alpha\in \Phi\}\). The issue then is that the correspondences of Proposition [pr:Modcorrespondence] fail for 7.\(^\ast\)-10.\(^\ast\) There are ways to get around this hurdle, most easily by swapping \(\Box_\to\) for the global box of modal logic in the \(^\ast\)-translation. Rather than detailing this here, we will set out and examine yet another translation. This is in part due to the nature of this paper – being exploratory and broad rather than deep – and in part due to some limitations of the translations proposed so far, as we now turn to discuss.

1.5 Lost and found in translation↩︎

1.5.0.1 On translating the relevant family.

Theorem 2 (and Corollary 1) collect a few relevant logics – like \(\mathbf{TW}^+, \mathbf{TWJ}^+\), and \(\mathbf{C}^+\) – for which our translation naturally extends, in the sense of ?? . However, many more relevant logics lie outside the scope of Theorem 2. For good reason: the theorem need not apply to them. For example, over \(\mathbf{B}^+\), contraction (11.) derives pseudo-modus ponens (10.), but the corresponding derivation over \(\mathbf{K}_2\) fails for their translations: \[\begin{align} \vdash_{\mathbf{B}^+\oplus[p \to(p \to q )]\to(p \to q )}[p \land(p \to q )]\to q\qquad \text{but}\qquad \nvdash_{\mathbf{K}_2\oplus [p \to(p \to q )]^\star\supset(p \to q )^\star}[p \land(p \to q )]^\star\supset q^\star, \end{align}\] as witnessed by, e.g., \(x\nvDash[p \land(p \to q )]^\star\supset q^\star\) in the \(\mathbf{K}_2\oplus [p \to(p \to q )]^\star\supset(p \to q )^\star\)-model with \(W=\{0,x,y\}\), \(V(p)=\{x,y\}, V(q)=\varnothing\), and \(R=\{(0,0,0),(0,x,x),(0,y,y),(0,x,y),(y,x,x),(y,x,y),(y,y,y)\}.\)

Model-theoretically, the issue is that the simpler pairs \((W,R)\) of Kripke modeling lack a means to account for relevant inferences relying on the \(\leq\)-conditions of Routley–Meyer frames. Specifically, although the relevant frame correspondent of \([p \to(p \to q )]\to(p \to q )\) and the modal frame correspondent of \([p \to(p \to q )]^\star\supset(p \to q )^\star\) both are \(x\cdot y\subseteq (x\cdot y)\cdot y\), and the relevant frame correspondent of \([p \to(p \to q )]\to(p \to q )\) and the modal frame correspondent of \([p \to(p \to q )]^\star\supset(p \to q )^\star\) likewise both are \(x\in x\cdot x\), only for Routley–Meyer frames does the former correspondent imply the latter, as it crucially relies on the down-down-up condition (recall Definition 1). This is exemplified by the above Kripke model, which, if we follow the suggestive notation and let \(N=\{0\}\), fails to define a Routley–Meyer frame as we then have \(x\leq y\) and \(Ryxx\) yet \(\overline{R}xxx\).⁷

Similarly, for assertion (12.) and one of the characteristic axioms of \(\mathbf{E}^+\), we have \[\begin{align} \vdash_{\mathbf{B}^+\oplus p\to [(p\to q)\to q]} [(p\to p)\to q]\to q\qquad \text{but}\qquad \nvdash_{\mathbf{K}_2\oplus p^\star\supset [(p\to q)\to q]^\star}[(p\to p)\to q]^\star\supset q^\star, \end{align}\] where the latter can be readily witnessed by a Kripke frame with \(R=\varnothing\); here, the Kripke modeling is inable to account for relevant inferences validated via reflexivity of \(\leq\) in Routley–Meyer frames.

To make matters more pressing, take \(\mathbf{R}^+\). On the one hand, recall that \(\mathbf{R}^+=\mathbf{B}^+\oplus\{8.,11.,12.\}\) and that \(\vdash_{\mathbf{R}^+} p \land(p \to q )\to q\). On the other, we have \(\nvdash_{\mathbf{K}_2\oplus \{8., 11., 12.\}^\star} [p \land(p \to q )]^\star\supset q^\star\) – so by completeness, not even the frame-class for \(\{8., 11., 12.\}^\star\) validates \([p \land(p \to q )]^\star\supset q^\star\) – which too can be shown by considering a Kripke frame with \(R=\varnothing\). Regrettably, the translation falls short of \(\mathbf{R}^+\), and for a deeper structural relation between relevant logic and modal logic, we should, and will, look elsewhere.

1.5.0.2 Import, export, transport.

It is a staple of logical practice to transfer meta-logical properties along translations. We shall here focus on but two: computability and interpolation.

First, we note that, e.g., \(\mathbf{B}^+\) inherits decidability as well as the finite-model property from \(\mathbf{K}_2\) through translation.⁸ But more interesting, and promising, seem the transfer of undecidability. In seminal work, Urquhart [@urquhart84:jsl] proved that a great many relevant logics are undecidable, not least \(\mathbf{R}^+\). While the \(^\star\)-translation fell short of \(\mathbf{R}^+\), there may be, and still are, results to be had. First off, all we have shown is that \(^\star\) isn’t full for \(\mathbf{R}^+\) and \(\mathbf{K}_2\oplus \{8., 11., 12.\}^\star\). This still leaves considerable room for variation; for example, one may append to \(\{8., 11., 12.\}^\star\) one or more axioms, and thereby have the undecidability of \(\mathbf{R}^+\) transfer. This remains to be explored.⁹ Even if this were to fail, we can, with no further work, collect other undecidability results. The result of [@urquhart84:jsl] applies to \(\mathbf{C}^+\) as well; and in recent work, undecidability is also shown for the weaker \(\mathbf{TWJ}^+\) [@Knudstorp25b]. Since the proof of [@Knudstorp25b] is for formulas whose principal connective is \(\to\), we obtain the following theorem.

The theorem supplements related results from [@Kurucz93; @KuruczNSS95:jolli; @Knudstorp25a] by, in comparison, pertaining to some sort of rotated setting yet without full associativity and using only a fragment of the language.¹⁰ Next, say that a logic \(\mathbf{L}\) has the Craig interpolation property (CIP) for a binary connective \(\rightsquigarrow\) if whenever \(\vdash_{\mathbf{L}}\varphi\rightsquigarrow \psi\), there is a formula \(\theta\) (an interpolant) such that \(\vdash_{\mathbf{L}}\varphi\rightsquigarrow \theta\) and \(\vdash_{\mathbf{L}}\theta\rightsquigarrow \psi\) and \(\mathsf{Var}(\theta)\subseteq \mathsf{Var}(\varphi)\cap \mathsf{Var}(\psi)\), where \(\mathsf{Var}(\alpha)\) denotes the set of propositional variables occurring in \(\alpha\). For normal modal logics, and other classical systems, the connective of concern tends to be the material implication \(\supset\), and for relevant logics, the relevant implication \(\to\).

Intriguingly, although all relevant logics between \(\mathbf{C}^+\) and \(\mathbf{R}^+\) were shown to lack interpolation already in the 1990s [@Urquhart93], it remains open whether \(\mathbf{B}^+\) enjoys it, cf. [@Standefer26]. In contrast, on the one hand, \(\mathbf{K}_2\) is known to have the CIP, while on the other, if the diamond of \(\mathbf{K}_2\) takes only diagonal entries \(\Diamond(\varphi, \varphi)\), one obtains a weakly aggregative modal logic (WAML) which lacks the CIP [@LiuDingWang22]. Since our \(^\star\)-translation sends formulas with main connective \(\to\) to formulas with main connective \(\supset\), this raises a number of questions. Can the proof of the CIP for \(\mathbf{K}_2\) be adapted to work for \(\mathbf{B}^+\)? Or can the argument showing that WAML lacks the CIP inspire a corresponding failure for \(\mathbf{B}^+\)? In case of the latter, since the translation establishes that \(\mathbf{B}^+\)-validities \(\varphi\to\psi\) find interpolants within \(\mathbf{K}_2\), what additional vocabulary would need to be added to \(\mathbf{B}^+\) to obtain the CIP?

2 Translating beyond the basics↩︎

2.1 Truth \(\mathsf{t}\) and fusion \(\circ\)↩︎

Sometimes relevant languages include the Ackermann truth constant \(\mathsf{t}\) and fusion \(\circ\), residuated by \(\to\). We should like to translate these too.

Adding \(\mathsf{t}\) and \(\circ\), we denote by \(\mathcal{L}^+_{\circ, \mathsf{t}}\) the relevant language with the grammar \[\varphi\mathrel{::=} p | \mathsf{t}|\varphi\lor\varphi|\varphi\land\varphi| \varphi\to \varphi| \varphi\circ\varphi.\] The \(\mathcal{L}^+_{\circ, \mathsf{t}}\)-fragment of the basic relevant logic is axiomatized by adding to the axiomatization of section 1.1, the formula \(\mathsf{t}\) as an axiom and the rules

Formulas of the extended language are still interpreted on the Routley–Meyer frames and models of Definition 1; the clauses for \(\mathsf{t}\) and \(\circ\) are as in the later presented 9 and 10 . The \(\mathcal{L}^+_{\circ, \mathsf{t}}\)-validities on the class of all Routley–Meyer frames are precisely the \(\mathcal{L}^+_{\circ, \mathsf{t}}\)-theorems of the basic relevant logic.

To translate the augmented language, we augment the modal language accordingly: \[\varphi\mathrel{::=} \bot| \top| p| \mathsf{t} |\neg\varphi|\varphi\lor\varphi|\Diamond(\varphi,\varphi)| \varphi\circ\varphi,\] where \(\mathsf{t}\) is a nullary modality and \(\circ\) is a binary modality.¹¹

With two binary modalities and one nullary modality, Kripke frames are now tuples \((W, R, S, N)\) where \(N\subseteq W\) is a set – as \(\mathsf{t}\) is nullary – and \(S\subseteq W^3\) is another ternary relation; however, like in temporal logic, triples \((W, R, N)\) will suffice, as \(\circ\) is residuated by \(\to\), which is ensured by requiring the adjunction \[(\varphi\circ\psi)\supset \chi \text{ is a theorem}\qquad \text{iff} \qquad \varphi\supset (\psi \to\chi)\text{ is a theorem,}\] or, equivalently, by including the following two formulas as axioms: \[\begin{align} [(p\to q)\circ p]\supset q\qquad \text{and}\qquad p\supset [q\to (p\circ q)].\label{eq:residuation} \end{align}\tag{8}\] The clauses for \(\mathsf{t}\) and \(\circ\) on Kripke models \((W, R, N)\) are then just as on Routley–Meyer models: \[\begin{align} &u\vDash \mathsf{t} && \text{iff} && u\in N,\tag{9}\\ &u\vDash \varphi\circ \psi && \text{iff} && \text{there exist w,v such that Rwvu, } w\vDash \varphi,\text{ and } v\vDash \psi.\tag{10} \end{align}\] A pleasant benefit of translating with \(\mathsf{t}\) and \(\circ\) is that now the modal language can define Routley–Meyer frames via correspondence theory. (For a frame \((W, R, N)\), we write \(x\leq y\) iff \(\exists n\in N(Rnxy)\).)

This suggests another translation, into a modal version of \(\mathbf{B}\).

Observe that \(\mathbf{Mod.B^+}\) is complete for the Kripke frames \((W, R, N)\) that are Routley–Meyer frames in the sense of Proposition [pr:ModcorrespondenceII]. This follows from Sahlqvist canonicity for those formulas, and from the canonicity of the residuation axioms 8 , which can be readily verified.¹³

We continue by defining the translation \(^\circ\), a variant of \(^\star\) available in the modal language with \(\circ\) and \(\mathsf{t}\), \[\begin{align} p^\circ &&\mathrel{:=}&& &\mathsf{t}\circ p && && && (\varphi\lor \psi)^\circ&&\mathrel{:=}&& \varphi^\circ \lor \psi^\circ\\ (\varphi\to \psi)^\circ&&\mathrel{:=}&& &\varphi^\circ\to\psi^\circ && && && (\varphi\land \psi)^\circ&&\mathrel{:=}&& \varphi^\circ\land \psi^\circ\\ \mathsf{t}^\circ &&\mathrel{:=}&& &\mathsf{t} && && && (\varphi\circ \psi)^\circ&&\mathrel{:=}&& \varphi^\circ \circ \psi^\circ. \end{align}\] We have the following lemmas, auxiliary to proving full- and faithfulness of the \(^\circ\)-translation.

From these lemmas it follows that the translation is full and faithful; see the appendix (7) for the proof.

What this translation may lack in simplicity or elegance, it may compensate for with greater mathematical naturality. If we let \(\mu^+\) denote the conjunction of the residuation and RM-frame axioms (i.e., the formulas axiomatizing \(\mathbf{Mod.B}^+\)), an appeal to the proof of Theorem 5 shows that for all \(\Gamma\subseteq\mathcal{L}^+_{\circ, \mathsf{t}}\), \[\begin{align} \mathsf{RMFr}^+(\Gamma)\mathrel{:=}&\{\mathfrak{F}\mid \mathfrak{F} \text{ is a Routley--Meyer frame validating each \varphi\in \Gamma} \}\\ =&\{\mathbb{F}\mid\mathbb{F}\text{ is a \mathbf{Mod.B^+} frame validating \mathsf{t\supset \varphi^\circ} for each \varphi\in \Gamma}\}\\ =&\{\mathbb{F}\mid\mathbb{F}\text{ is a Kripke frame validating \mu^+ and \mathsf{t\supset \varphi^\circ} for each \varphi\in \Gamma}\}\mathrel{=:}\mathsf{KFr}^+(\mu^+, \mathsf{t}\supset\Gamma^\circ). \end{align}\] Thus, for any class \(\mathcal{C}\) of Routley–Meyer frames, the translation is full and faithful, in that for all formulas \(\varphi\in\mathcal{L}^+_{\circ, \mathsf{t}}\), \[\mathcal{C}\Vdash\varphi \qquad \text{iff} \qquad \mathcal{C}\vDash \mathsf{t}\supset \varphi^\circ.\] It seems plausible that, and certainly interesting whether, this structural connection can be deepened to include frame-incomplete logics as well. It is also expected to facilitate significant transfer of results. We leave this as open questions and close by extending the translation to the language with negation.

2.2 Negation \(\neg\)↩︎

In this final section, we translate the relevant negation \(\neg\). Proof-theoretically, the basic relevant logic \(\mathbf{B}\) is axiomatized by adding the double-negation elimination scheme together with a rule for contraposition:¹⁴

Model-theoretically, Routley–Meyer frames are expanded with a function \(^\ast:K\to K\) subject to \[x\leq y \; \text{ only if } \; y^\ast\leq x^\ast\qquad \text{and} \qquad x^{\ast\ast}=x,\] so that frames become tuples \((K, R, N, {^\ast})\), with this clause for negation: \(\qquad x\Vdash \neg \varphi \qquad \text{iff} \qquad x^\ast\nVdash \varphi.\)
We translate by expanding the modal grammar with a unary modality \(\ooalign{\Box\cr\hidewidth\raisebox{0.05ex}{\scalebox{0.8}[1]{\neg}}\hidewidth\cr}\).¹⁵ Although we shall only be concerned with \(^\circ\), for each translation \(^\sharp\), we can set \((\neg\varphi)^\sharp\mathrel{:=}{\ooalign{\Box\cr\hidewidth\raisebox{0.05ex}{\scalebox{0.8}[1]{\neg}}\hidewidth\cr}}\neg\varphi^\sharp.\)

With an extra modality present, Kripke frames \((W, R,N, {^\ast})\) now come equipped with an additional binary relation \({^\ast}\subseteq W\times W\). The next proposition is useful for the purpose of translation.

Letting \(\mu\) be the conjunction of \(\mu^+\) and the formulas of Proposition [pr:ModcorrespondenceIII], an appeal to the proof strengthens the theorem to show that for any set of relevant formulas \(\Gamma\), \[\begin{align} \mathsf{RMFr}(\Gamma)\mathrel{:=}&\{\mathfrak{F}\mid \mathfrak{F} \text{ is a Routley--Meyer frame validating each \varphi\in \Gamma} \}\\ =&\{\mathbb{F}\mid\mathbb{F}\text{ is a \mathbf{Mod.B} frame validating \mathsf{t\supset \varphi^\circ} for each \varphi\in \Gamma}\}\\ =&\{\mathbb{F}\mid\mathbb{F}\text{ is a Kripke frame validating \mu and \mathsf{t\supset \varphi^\circ} for each \varphi\in \Gamma}\}\mathrel{=:}\mathsf{KFr}(\mu, \mathsf{t}\supset\Gamma^\circ). \end{align}\] We end by concluding that for any class \(\mathcal{C}\) of Routley–Meyer frames for the language with negation, the translation is full and faithful, in that for all relevant formulas \(\varphi\), \[\mathcal{C}\Vdash\varphi \qquad \text{iff} \qquad \mathcal{C}\vDash \mathsf{t}\supset \varphi^\circ.\]

2.2.0.1 Acknowledgements.

I wish to thank Shawn Standefer for helpful comments on an earlier draft, Josef von-Hoffmann Doyle for discussions of the material, and Maria Aloni and the anonymous referees for constructive suggestions. The research was supported by the Nothing is Logical (NihiL) project (NWO OC 406.21.CTW.023).

3 Technical appendix↩︎

The first lemma gives the model transformation \(F\) and proves 4 , while the subsequent lemma gives the model transformation \(G\) and proves 5 .

The following two lemmas build on the preceding two lemmas, in order to establish 6 and 7 needed for Theorem 3.

Next, we provide proof of representative items from Proposition [pr:ModcorrespondenceII]. Recall that for a frame \((W, R, N)\), we write \(x\leq y\) iff \(\exists n\in N(Rnxy)\).

The proofs of Theorem 5 and Proposition [pr:ModcorrespondenceIII] follow next.

---

1. The relevant-logic overview presented here is brief and selective. For more comprehensive expositions, I invite the reader to consult [@AndersonBelnap75; @AndersonBelnapDunn92; @DunnRestall02; @Standefer26].↩︎

2. Relevance, at least over the signature \(\{\land, \lor, \to\}\), has close ties to constructivism; see [@WeissStandefer2026] for points of contact.↩︎

3. Algebraically, the \(\{\land, \lor, \to\}\)-fragment of \(\mathbf{IPL}\) corresponds to the well-studied variety of Brouwerian algebras (only that the latter include a designated element \(\top\) for the term definable \(p\to p\)). The subvariety axiomatized by Peirce’s law is the variety of generalized Boolean algebras, corresponding to the \(\{\land, \lor, \to\}\)- (or \(\{\land, \lor, \to, \top\}\)-fragment) of \(\mathbf{CPL}\). Let us also mention that minimal logic [@Johansson37] is like the \(\{\land, \lor, \to\}\)-fragment of \(\mathbf{IPL}\) but with a constant symbol \(\bot\) for which no axioms or rules are specified.↩︎

4. The paper assumes basic familiarity with normal modal logic. For a more detailed treatment of the subject, the reader is referred to standard textbooks such as [@bluebook; @ChagrovZ97:ml].↩︎

5. We footnote that 6 isn’t a biimplication (hence not a Chu transform/infomorphism), nor is 7 . But neither biimplication is needed.↩︎

6. In addition to the links between constructivism and relevance drawn in [@WeissStandefer2026], we point the reader to [@Meyer73] for a translational embedding of \(\mathbf{IPL}\) into \(\mathbf{R}\), and to [@DunnMeyer1971] for an embedding of the Gödel–Dummett intermediate logic into the relevant logic \(\mathbf{RM}\).↩︎

7. Proof-theoretically, an issue has to do with the translation of the rules. To illustrate, for implications \(\varphi=\alpha\to\beta, \psi=\gamma\to\delta\) the translated rule of modus ponens reads

   which should be admissible in the target logic; however, as the translation highlights, there is a compositional tension with nested versus non-nested conditionals.↩︎

8. One may think that only the \(^\ast\)-translation imparts decidability on \(\mathbf{B}^+\), as \(^\star\) operates on formulas with implication as main connective. However, \(\mathbf{B}^+\), like most other positive relevant logics, enjoys the disjunction property, hence the problem of deciding \(\vdash_{\mathbf{B}^+}\varphi\) reduces to the problem of deciding \(\vdash_{\mathbf{B}^+}\alpha\to\beta\). Proofs of the disjunction property for relevant logics typically go via metacompleteness [@Meyer76; @Slaney84].↩︎

9. One place to look for inspiration is in the work on classical relevant logic and simplified semantics [@MeyerRoutley73; @PriestSylvan92; @Restall93; @RestallRoy09]. Both bear some similarity to the present enterprise, inasmuch as translations also produce semantics – fullness as soundness, faithfulness as completeness.↩︎

10. More generally, the undecidability techniques of [@Knudstorp25a; @Knudstorp25b] have found somewhat broad application [@Knudstorp2024; @GalatosJipsenKnudstorpRevantha:BIund], and comparing these results via translation could serve in mapping the border between the solvable and the unsolvable.↩︎

11. Note that nullary modalities are normal modalities in the technical sense, and are used in e.g. arrow logic.
    Also note that we use infix notation for \(\circ\) and prefix for \(\Diamond\). This is perhaps somewhat odd, but it’s just a matter of convention (aligning partly with relevant conventions, and partly with modal conventions).↩︎

12. One might also consider adding further axioms to capture restrictions sometimes imposed on Routley–Meyer frames to obtain (typically) simpler semantics. An example is \(\mathsf{t}\circ p\supset p\), which is Sahlqvist with correspondent \(N\cdot x \subseteq \{x\}\).↩︎

13. For example, by observing that a normal modal logic contains \([(p\to q)\circ p]\supset q\) iff it contains \([(p\to \neg q)\circ p]\land q\supset \bot\), and it contains \(p\supset [q\to (p\circ q)]\) iff it contains \(\Diamond(q,\neg (p\circ q))\land p\supset \bot\). So canonicity follows because \([(p\to \neg q)\circ p]\land q\supset \bot\) and \(\Diamond(q,\neg (p\circ q))\land p\supset \bot\) are Sahlqvist: \((p\to \neg q)\) and \(\neg (p\circ q)\) are negative formulas; \(\bot\) is vacuously positive; and \(p\) and \(q\) are vacuously boxed atoms.↩︎

14. The weaker logic \(\mathbf{BM}\) is sometimes taken as the fundamental relevant logic with negation (without negation, \(\mathbf{B}\) and \(\mathbf{BM}\) coincide). The results of this section readily extend to \(\mathbf{BM}\) and its extensions. Details are left as an exercise.↩︎

15. This makes literal the idea of negation as a modality (see, e.g., [@BertoRestall2019]). See also [@MeyerRoutley1974] where the relevant language is augmented by a weak-assertion operator that behaves like \(\ooalign{\Box\cr\hidewidth\raisebox{0.05ex}{\scalebox{0.8}[1]{\neg}}\hidewidth\cr}\).↩︎