On Sahlqvist Formulas in Relevant Logic
Abstract
This paper defines a Sahlqvist fragment for relevant logic and establishes that each class of frames in the RoutleyMeyer semantics which is definable by a Sahlqvist formula is also elementary, that is, it coincides with the class of structures satisfying a given first order property calculable by a Sahlqvistvan Benthem algorithm. Furthermore, we show that some classes of RoutleyMeyer frames definable by a relevant formula are not elementary.
Keywords
Relevant logic RoutleyMeyer semantics Correspondence theory Frame definability Sahlqvist’s correspondence1 Introduction
The Sahlqvist Correspondence Theorem is a celebrated result in modal logic (see [3, 6] for slightly different expositions). It tells us that when a modal formula ϕ has certain syntactic form, we can always compute a first order formula ψ in the signature of Kripke frames such that a frame validates ϕ iff it satisfies condition ψ, so the class of frames definable by ϕ is elementary. The proof relies on the so called “Sahlqvistvan Benthem algorithm” for transforming second order frame correspondents of some modal formulas into first order properties.
The present note is a contribution to the correspondence theory of relevant logic in the RoutleyMeyer semantic framework (cf. [4, 8, 16]).^{1} The framework has been considerably generalized and investigated in relation to other semantics in [1].
We will show that, mutatis mutandis, the argument for the Sahlqvist Correspondence Theorem (as presented in [3]) can be adapted to the context of relevant logic to prove an analogous result in the RoutleyMeyer semantics. This result improves our understanding of the first order properties of RoutleyMeyer frames which are definable in relevant logic. It also begins to solve Problem 8.4.18 from [1]. Moreover, we will show that some relevant formulas actually define nonelementary properties of frames, so the problem of elementarity is not trivial.
Correspondence theory for the broader setting of substructural logics with frame semantics was briefly explored by Restall in [14] (pp. 263265) although the subject appears to have been discussed for the first time in the relevant logic literature in [13].^{2} Recently, Suzuki [18] provided a rather general Sahlqvist result for substructural logics with respect to what he calls biapproximation semantics (which unfortunately is much more complicated than the RoutleyMeyer framework). Other settings without boolean negation where Sahlqvist theorems have been obtained are positive modal logic [5] and relevant modal logic [17]. In particular, the work in [17] is rather close to ours, but the concern there is still modal logic.
In Section 2, we will introduce RoutleyMeyer frames and some basic propositions on frame correspondence. In Section 3, we will discuss elementary classes of RoutleyMeyer frames and prove that not all classes of RoutleyMeyer frames definable by a relevant formula are elementary. In Section 4, we will present a Sahlqvist fragment of relevant languages and establish a Sahlqvist correspondence theorem for the RoutleyMeyer semantics. Finally, in Section 5, we will sum up our work.
2 RoutleyMeyer Frames

p1. x ≤ x

p2. If x ≤ y and R y z v then R x z v.

p3. If x ≤ y and R z y v then R z x v.

p4. If x ≤ y and R z v x then R z v y.

p5. If x ≤ y then y ^{∗}≤ x ^{∗} .

p6. O is upward closed under ≤.

A1. t

A2. t → (p → p)

A3. p ∧ q → p

A4. p ∧ q → q

A5. (p → q) ∧ (p → r) → (p → q ∧ r)

A6. p → p ∨ q

A7. q → p ∨ q

A8. p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r)

R1. p,p → q/q

R2. p,q/p ∧ q

R3. p → q/(q → r) → (p → r)

R4. p → q/(r → p) → (r → q)

R5. p →∼ q/q →∼ p

R6. (p ∘ q) → r/p → (q → r)

R7. p → (q → r)/(p ∘ q) → r
 M, w \(\Vdash \) t

iff there is v ∈ O ^{ M } such that v ≤ w
 M, w \(\Vdash \) p

iff w ∈ V (p),
 M, w \(\Vdash \sim \phi \)

iff \(M, w^{*} \nVdash \phi \),
 M, w \(\Vdash \phi \wedge \psi \)

iff \(M, w \Vdash \phi \) and \(M, w \Vdash \psi \),
 M, w \(\Vdash \phi \vee \psi \)

iff \(M, w \Vdash \phi \) or \(M, w \Vdash \psi \),
 M, w \(\Vdash \phi \rightarrow \psi \)

iff for every a, b such that R ^{ M } w a b, if \(M, a \Vdash \phi \) then M, b \(\Vdash \psi \),
 M, w \(\Vdash \phi \circ \psi \)

iff there are a, b such that R ^{ M } a b w, \(M, a \!\Vdash \! \phi \) and \(M, b \Vdash \psi \).
A formula ϕ is said to be true in a model M if \(M, w \Vdash \phi \) for all w ∈ O. ϕ is said to be valid in a frame \(\mathfrak {F}\) (in symbols \(\mathfrak {F} \Vdash \phi \)) if ϕ is true in any model M based on \(\mathfrak {F}\). When w is an arbitrary world of \(\mathfrak {F}\), we also write \(\mathfrak {F}, w \Vdash \phi \) to mean that for every model M based on \(\mathfrak {F}\), \(M, w \Vdash \phi \). Validity and this latter semantic notions will be the focus of the present study. We will be interested in what the languages defined above can say at the level of frames, not so much of models.
Lemma 1
(Hereditary Lemma) For any relevant formula ϕ , model M based on a RoutleyMeyer frame, and worlds x,y of M, x ≤ y implies that \(M, x \Vdash \phi \) only if \(M, y \Vdash \phi \) .
Proof
This is traditionally proven by induction on formula complexity (see [8]). The case ϕ = p follows simply because V (p) is upward closed under ≤, while the case ϕ = t follows because ≤ is a transitive relation.
Next let ϕ =∼ ψ. By p5, we must have that y ^{∗}≤ x ^{∗} given our assumption that x ≤ y. Now, if \(M, x \Vdash \sim \psi \) then \(M, x^{*} \nVdash \psi \), and by inductive hypothesis, it follows that \(M, y^{*} \nVdash \psi \), so \(M, y \Vdash \sim \psi \) as desired.
Let ϕ = ψ → χ. If \(M, x \Vdash \psi \rightarrow \chi \), then for every a,b such that R x a b, if \(M, a \Vdash \psi \) then \(M, b \Vdash \psi \). Now suppose that \(M, y \nVdash \psi \rightarrow \chi \), so there are a ^{′},b ^{′} such that R y a ^{′} b ^{′} while \(M, a^{\prime } \Vdash \psi \) and \(M, b^{\prime } \nVdash \chi \). However, by p2, it must be that R x a ^{′} b ^{′}, which is impossible given the assumption that \(M, x \Vdash \psi \rightarrow \chi \). Hence, actually \(M, y \Vdash \psi \rightarrow \chi \).
Let ϕ = ψ ∘ χ. Similar to the previous case but appealing to p4 instead. The remaining cases are trivial. □
Consider a monadic second order language that comes with one function symbol ∗, a unary predicate O, a distinguished three place relation symbol R, and a unary predicate variable P for each p ∈ PROP. Following the tradition in modal logic, we might call this a correspondence language \(\mathcal {L}^{corr}\) for \(\mathcal {L}\) (cf. [3]). Now we can read a model M as a model for \(\mathcal {L}^{corr}\) in a straightforward way: W is taken as the domain of the structure, V specifies the denotation of each of the predicates P,Q,…, the collection O is the object assigned to the predicate O, while ∗ is the denotation of the function symbol ∗ of \(\mathcal {L}^{corr}\) and R the denotation of the relation R of \(\mathcal {L}^{corr}\).
Next we prove a proposition to the effect that our proposed translation is adequate. While \(\Vdash \) stands for satisfaction as defined for relevant languages, \(\vDash \) will be the usual Tarskian satisfaction relation from classical logic.
Proposition 2
For any w, \(M, w \Vdash \phi \) if and only if \(M \vDash T_{x}(\phi ) [w]\) .

\(\phi ::= Px \  \ \exists v (Ov \wedge v \leq x) \  \ \neg \phi ^{x^{*}/x} \  \ \phi \wedge \psi \  \ \phi \vee \psi \ \ \forall y, z (Rxyz \wedge \phi ^{y/x} \supset \psi ^{z/x}) \  \ \exists y, z (Ryzx \wedge \phi ^{y/x} \wedge \psi ^{z/x})\).
Definition 1
A relevant formula ϕ is said to be positive if T _{ x }(ϕ) is a formula built up from atomic formulas involving only unary predicates and first order formulas where the only nonlogical symbols are R and O, using the connectives ∃,∀,∧ and ∨. On the other hand ϕ is negative if T _{ x }(ϕ) is a formula built up from boolean negations of atomic formulas involving only unary predicates and first order formulas where the only nonlogical symbols are R and T, using the connectives ∃,∀,∧ and ∨.
A remark seems in order here: the translation of a formula of the form ϕ → ψ is in general not positive as it involves ⊃ with its usual definition in terms of ¬ and ∨.
Lemma 3
Let M be a RoutleyMeyer model for a relevant language \(\mathcal {L}\) , \(\phi (\overline {x})\) a positive first order formula of \(\mathcal {L}^{corr}\) where \(\overline {x}\) is a sequence of variables, and M ^{′} a RoutleyMeyer model identical to M except that the interpretation of the unary predicates of the signature of M in the model M ^{′} are supersets of the interpretation of the corresponding predicates in M. Then for any sequence of elements \(\overline {a}\) of M, \(M \vDash \phi [\overline {a}]\) only if \(M^{\prime } \vDash \phi [\overline {a}]\) .
Proof
This follows from Theorem 10.3.3 (a) in [11]. □
We say that a formula ϕ ^{′} of \(\mathcal {L}^{corr}\) corresponds to (or is a correspondent of) a relevant formula ϕ if for any RoutleyMeyer frame \(\mathfrak {F}\), \(\mathfrak {F} \Vdash \phi \) iff \(\mathfrak {F} \vDash \phi ^{\prime }\). A formula ψ of \(\mathcal {L}^{corr}\) locally corresponds to a relevant formula ϕ if for any RoutleyMeyer frame \(\mathfrak {F}\) and world w of \(\mathfrak {F}\), \(\mathfrak {F}, w \Vdash \phi \) iff \(\mathfrak {F} \vDash \psi [w]\).
If we abreviate the formula of \(\mathcal {L}^{corr}\) which expresses that the value of a given predicate P is upward closed under ≤ by U p _{≤}(P), the next proposition is easily established using Proposition 2.
Proposition 4

(i) \(\mathfrak {F} \Vdash \phi \) iff \(\mathfrak {F} \vDash \forall P_{1}, \dots , P_{n} (Up_{\leq }(P_{1}) \wedge {\dots } \wedge Up_{\leq }(P_{n}) \supset \forall w (Ow \supset T_{x}(\phi )^{w/x}))\)

(ii) \(\mathfrak {F}, w \Vdash \phi \) iff \(\mathfrak {F} \vDash \forall P_{1}, \dots , P_{n} (Up_{\leq }(P_{1}) \wedge {\dots } \wedge Up_{\leq }(P_{n}) \supset T_{x}(\phi ))[w]\) .
A class (or, informally, a property) K of RoutleyMeyer frames will be said to be definable by a relevant formula ϕ if K is exactly the class of all frames validating ϕ. So, at the level of frames and validity, relevant languages can be seen as fragments of monadic second order logic as opposed to fragments of first order logic at the level of models. To be precise, the “relevant fragment” of monadic second order logic can be taken to be any formula equivalent to a formula in the set
{∀P _{1},…,P _{ n }(U p _{≤}(P _{1}) ∧… ∧ U p _{≤}(P _{ n }) ⊃ T _{ x }(ϕ)) : ϕ is a relevant formula}.
3 Elementary Classes of Frames
A class of structures K is said to be elementary if there is a first order formula ϕ such that K is identical to the class of all models of ϕ. Since frames are clearly structures, then it makes sense to talk about elementary classes of frames.
Note that it is easy to prove that a class of RoutleyMeyer frames which is definable by a formula of relevant logic is elementary iff it is closed under ultraproducts. Goldblatt [10] observed that this was so for modal logic and the same quick little argument applies here. Recall that a class of structures is elementary iff both the class and its complement are closed under ultraproducts ([7], Corollary 6.1.16 (ii)^{3}). Now, the complement of a class of RoutleyMeyer frames definable by a relevant formula ϕ is always closed under ultraproducts. For it is the class of all models of a Σ11 sentence ∃P _{1},…,P _{ n }(U p _{≤}(P _{1}) ∧… ∧ U p _{≤}(P _{ n }) ∧¬T _{ x }(ϕ)^{ T/x }) and Σ11 formulas are preserved under ultraproducts ([7], Corollary 4.1.14). Hence, we have proven the observation. Furthermore, following a similar argument to that in [21] for modal logic, we can actually show that ultrapowers suffice for a characterization of elementarity.
As an example of a relevant formula which defines an elementary class of frames we have \(p_{0} \vee (p_{0} \rightarrow p_{1}) \vee {\dots } \vee \left (\bigwedge _{0 \leq i \leq n1} p_{i} \rightarrow p_{n}\right )\). The intuitionistic counterpart of this formula on intuitionistic Kripke frames corresponds to a cardinality claim ([6], Proposition 2.40). The first order correspondent of the formula on RoutleyMeyer frames is \(\forall x_{1}, y_{1}, \dots , x_{n}, y_{n} \left (\bigwedge _{i=1}^{n} x_{i} \leq y_{i} \supset \bigvee _{1 \leq j \textless i \leq n } x_{i} \leq y_{j}\right )\). This can be seen as follows. Let \(\mathfrak {F}\) be an arbitrary RoutleyMeyer frame. Suppose first that \(\mathfrak {F}\) satisfies our first order condition and that for some model M based on \(\mathfrak {F}\), \(M, T \nVdash p_{0} \vee (p_{0} \rightarrow p_{1}) \vee {\dots } \vee \left (\bigwedge _{0 \leq i \leq n1} p_{i} \rightarrow p_{n}\right )\) for some T ∈ O. The latter means that for each number 1 ≤ i ≤ n, there are x _{ i },y _{ i } such that x _{ i } ≤ y _{ i }, \(M, x_{i} \Vdash \bigwedge _{0 \leq j \leq i1} p_{j}\) but \(M, y_{i} \nVdash p_{i}\). Now take x _{ i },y _{ j }, j<i such that x _{ i } ≤ y _{ j }. We have that \(M, x_{i} \Vdash \bigwedge _{0 \leq j \leq i1} p_{j}\) but \(M, y_{j} \nVdash p_{j}\), which by the Hereditary Lemma implies that \(M, x_{i} \nVdash p_{j} \), a contradiction. On the other hand, suppose \(\forall x_{1}, y_{1}, \dots , x_{n}, y_{n} \left (\bigwedge _{i=1}^{n} x_{i} \leq y_{i} \supset \bigvee _{1 \leq j \textless i \leq n } x_{i} \leq y_{j}\right )\) fails in \(\mathfrak {F}\), that is \(\exists x_{1}, y_{1}, \dots , x_{n}, y_{n} \left (\left (\bigwedge _{i=1}^{n} x_{i} \leq y_{i} \right )\wedge \left (\bigwedge _{1 \leq j \textless i \leq n } x_{i} \nleq y_{j}\right )\right )\) holds in \(\mathfrak {F}\). Without loss of generality, we may assume that for some T ∈ O, we have x _{0} = T,T = y _{0},x _{1},y _{1},…,x _{ n },y _{ n } is an enumeration such that x _{ i } ≤ y _{ j } implies that i ≤ j. Consider a valuation V on \(\mathfrak {F}\) such that \(V(p_{i}) = \{x : x \nleq y_{i}\}\) (this set is upward closed under ≤ by the transitivity of ≤). First thing to note is that \(\langle \mathfrak {F}, V \rangle , T \nVdash p_{0}\) since ≤ is reflexive (which also implies that \(\langle \mathfrak {F}, V \rangle , y_{i} \nVdash p_{i}\)). But for any i>0, \(\langle \mathfrak {F}, V \rangle , x_{i} \Vdash \bigwedge _{0 \leq j \leq i1} p_{j}\), since otherwise for some j<i, x _{ i } ≤ y _{ j }, which is impossible by assumption. Hence, \(\mathfrak {F} \nVdash p_{0} \vee (p_{0} \rightarrow p_{1}) \vee {\dots } \vee \left (\bigwedge _{0 \leq i \leq n1} p_{i} \rightarrow p_{n}\right )\), as desired.
The example in the above paragraph also serves as a point of comparison between the expressive power of relevant formulas on RoutleyMeyer frames and intuitionistic formulas on Kripke frames. More illustrations of relevant formulas defining elementary classes will follow in Section 4, as applications of our Sahlqvist correspondence theorem.
One question that arises immediately is whether all relevant formulas have first order correspondents, i.e., define elementary classes. The next results show that this is not the case (though Section 4 will give a positive result). The formula witnessing this fact in the following theorem is roughly the analogue of the famous McKinsey axiom from modal logic (which was shown not to be elementary simultaneously by van Benthem [20] and Goldblatt [10]). We use a techinique due to van Benthem [20].
Theorem 5

∼ (∼ p ∧ (t∨∼t → (p ∘ (t∨∼t)))) ∨ ((t∨∼t) ∘ (t∨∼t → p))
Proof
First, we show that (M) is valid in \(\mathfrak {F_{0}}\). Let V be an arbitrary valuation on \(\mathfrak {F_{0}}\). Suppose that \(\langle \mathfrak {F_{0}}, V \rangle , q \Vdash \sim p \wedge (\textbf {t} \vee \sim \textbf {t} \rightarrow (p \circ (\textbf {t} \vee \sim \textbf {t})))\). This means that \(\langle \mathfrak {F_{0}}, V \rangle , q \Vdash \sim p \) (which implies that \(\langle \mathfrak {F_{0}}, V \rangle , q \nVdash p \) by our definition of ∗) and \(\langle \mathfrak {F_{0}}, V \rangle , q \Vdash \textbf {t} \vee \sim \textbf {t} \rightarrow (p \circ (\textbf {t} \vee \sim \textbf {t}))\) (which implies that for all w ∈ W, \(\langle \mathfrak {F_{0}}, V \rangle , w \Vdash p \circ (\textbf {t} \vee \sim \textbf {t})\), i.e., there are v _{1},v _{2} such that R v _{1} v _{2} w and \(\langle \mathfrak {F_{0}}, V \rangle , v_{1} \Vdash p\)). By the latter, for each q _{ n } there must be some q _{ n,i } such that \(\langle \mathfrak {F_{0}}, V \rangle , q_{n, i} \Vdash p\) (for q,q _{ n } cannot witness p ∘ (t∨∼t) since \(\langle \mathfrak {F_{0}}, V \rangle , q \nVdash p\)). Take r _{ f } to be such that \(\langle \mathfrak {F_{0}}, V \rangle , q_{n, f(n)} \Vdash p\) for any n ∈ ω. Then since R s r _{ f } q and \(\langle \mathfrak {F_{0}}, V \rangle , z_{f} \Vdash \textbf {t} \vee \sim \textbf {t} \rightarrow p\) (since in \(\mathfrak {F_{0}}\), R r _{ f } x y iff for some n ∈ ω, x = q _{ n,f(n)} = y), we have that \(\langle \mathfrak {F_{0}}, V \rangle , q \Vdash (\textbf {t} \vee \sim \textbf {t})\circ (\textbf {t} \vee \sim \textbf {t} \rightarrow p)\), as desired.
Now suppose (M) has a first order correspondent ϕ. By the above paragraph, \(\mathfrak {F_{0}} \vDash \phi \). By the downward LöwenheimSkolem theorem, there is a countable elementary substructure \(\mathfrak {F_{0}}^{\prime }\) of \(\mathfrak {F_{0}}\) including {q,s}∪{q _{ n } : n ∈ ω}∪{q _{ n, i } : n ∈ ω,i ∈{0, 1}} as a subset of its domain. We will show that (M) is not valid in \(\mathfrak {F_{0}}^{\prime }\). This will produce a contradiction since \(\mathfrak {F_{0}}^{\prime } \vDash \phi \), given that \(\mathfrak {F_{0}}^{\prime }\) and \(\mathfrak {F_{0}}\) are elementarily equivalent.
Being countable, \(\mathfrak {F_{0}}^{\prime }\) must leave out an element z _{ g } (g ∈{0, 1}^{ ω }) of W . Consider a valuation V on \(\mathfrak {F_{0}}^{\prime }\) such that V (p) = {q _{ n,g(n)} : n ∈ ω}. We note that \(\langle \mathfrak {F_{0}}^{\prime }, V \rangle , q \nVdash p\), so \(\langle \mathfrak {F_{0}}^{\prime }, V \rangle , q \Vdash \sim p\). Now, for any q _{ n }, since R q _{ n,g(n)} q _{ n,g(n)} q _{ n }, \(\langle \mathfrak {F_{0}}^{\prime }, V \rangle , q_{n} \Vdash p \circ (\textbf {t} \vee \sim \textbf {t})\). Similarly if w≠q _{ n } (n ∈ ω), \(\langle \mathfrak {F_{0}}^{\prime }, V \rangle , w \Vdash p \circ (\textbf {t} \vee \sim \textbf {t})\). Hence, for all w in the domain of \(\mathfrak {F_{0}}^{\prime }\), \(\langle \mathfrak {F_{0}}^{\prime }, V \rangle , w \Vdash p \circ (\textbf {t} \vee \sim \textbf {t})\), which implies that \(\langle \mathfrak {F_{0}}^{\prime }, V \rangle , q \Vdash \textbf {t} \vee \sim \textbf {t} \rightarrow (p \circ (\textbf {t} \vee \sim \textbf {t}))\). Finally, we want to show that \(\langle \mathfrak {F_{0}}^{\prime }, V \rangle , q \nVdash (\textbf {t} \vee \sim \textbf {t})\circ (\textbf {t} \vee \sim \textbf {t} \rightarrow p)\). If R x y q either (1) x = y = q or (2) x = y = q _{ n,i } for some n ∈ ω,i ∈{0,1}, or (3) x = s and y = z _{ f } for some z _{ f } in the domain of \(\mathfrak {F_{0}}^{\prime }\). It suffices to show that in all three cases \(\langle \mathfrak {F_{0}}^{\prime }, V \rangle , y \nVdash \textbf {t} \vee \sim \textbf {t} \rightarrow p\). If (1), since \(\langle \mathfrak {F_{0}}^{\prime }, V \rangle , q \nVdash p\) and given that R q q q, \(\langle \mathfrak {F_{0}}^{\prime }, V \rangle , y \nVdash \textbf {t} \vee \sim \textbf {t} \rightarrow p\). If (2), since R q _{ n,i } q _{ n,h(g(n))} q _{ n,h(g(n))} (where h : {0,1}→{0,1} is the function such that h(0) = 1 and h(1) = 0) and \(\langle \mathfrak {F_{0}}^{\prime }, V \rangle , q_{n, h(g(n))} \nVdash p\), we have that \(\langle \mathfrak {F_{0}}^{\prime }, V \rangle , y \nVdash \textbf {t} \vee \sim \textbf {t} \rightarrow p\). If (3), f≠g, so they differ in their value for some n, hence, q _{ n,f(n)}≠q _{ n,g(n)}, which implies that \(\langle \mathfrak {F_{0}}^{\prime }, V \rangle , q_{n, f(n)} \nVdash p\). Given that R r _{ f } q _{ n,f(n)} q _{ n,f(n)}, we see that \(\langle \mathfrak {F_{0}}^{\prime }, V \rangle , y \nVdash \textbf {t} \vee \sim \textbf {t} \rightarrow p\), as desired. □
Next we provide a much easily graspable nonelementary class of RoutleyMeyer frames which is definable in the language of relevant logic. For the conjunction of conditions (i) and (ii) in Proposition 6 is not expressible in first order logic as will be seen through a compactness argument. This time we build a relevant logic analogue of the wellknown Löb axiom.
Put R ^{ # } x y= _{ d f }∃z(R x y z ∨ R x z y) and ▪p= _{ d f }(p∨∼ p → p) ∧ (∼ p → p∧∼ p). Observe that for any frame \(\mathfrak {F}\), and world x ∈ W, R ^{ # } T x holds, so \(\mathfrak {F} \vDash \forall x (R^{\#}Tx)\). In any frame \(\mathfrak {F}\) where ∀x(x ^{∗}≤ x ∧ x ≤ x ^{∗}), using the Hereditary Lemma, we see that a formula of the form ∼ ϕ ∨ ψ behaves essentially as a material implication in a classical language at the level of models based on \(\mathfrak {F}\). Also, for any valuation V in any such frame \(\mathfrak {F}\), \(\langle \mathfrak {F}, V \rangle , w \Vdash \blacksquare p \) iff for all x,y such that R w x y, \(\langle \mathfrak {F}, V \rangle , x\Vdash p \) and \(\langle \mathfrak {F}, V \rangle , y\Vdash p \) iff for all x such that R ^{ # } w x, \(\langle \mathfrak {F}, V \rangle , x\Vdash p \).
Now, for any frame \(\mathfrak {F}\), \(\mathfrak {F} \Vdash (p \wedge \sim p \rightarrow q) \wedge (q \rightarrow p \vee \sim p)\) iff \(\mathfrak {F} \vDash \forall x (x^{*} \leq x \wedge x \leq x^{*})\).
Proposition 6
\(\mathfrak {F} \Vdash (p \wedge \sim p \rightarrow q) \wedge (q \rightarrow p \vee \sim p) \wedge ((\blacksquare (\blacksquare p \supset p) \wedge p) \supset \blacksquare p)\) iff (i) \(\mathfrak {F} \vDash \forall x (x^{*} \leq x \wedge x \leq x^{*})\) and there is T ∈ O such that (ii) there is no infinite sequence of worlds T = s _{0},s _{1},s _{2}…such that \(s_{0} \nleq s_{i} (0 \textless i \textless \omega )\) and R ^{ # } s _{0} s _{1},R ^{ # } s _{1} s _{2},R ^{ # } s _{2} s _{3},…and (iii) for any x,y , R ^{ # } T x and R ^{ # } x y implies that R ^{ # } T y .
Proof
Let \(\mathfrak {F}\) be an arbitrary RoutleyMeyer frame. We have that if (i) holds, the validity of ▪(▪p ⊃ p) ∧ p ⊃ ▪p implies (ii). For suppose (ii) fails, then there is an infinite sequence of worlds \(T=s_{0} \nleq s_{1}, s_{2} \dots \) such that R ^{ # } s _{0} s _{1}, R ^{ # } s _{1} s _{2}, R ^{ # } s _{2} s _{3},… Now take any valuation V based on \(\mathfrak {F}\) such that \(V(p)=\{w : w \nleq s_{i}, 0 \textless i\textless \omega \}\). By transitivity of ≤, V (p) is upwards closed under ≤. For each s _{ i }, s _{ i } ≤ s _{ i }, so \(\langle \mathfrak {F}, V \rangle , s_{i} \nVdash p\). Hence, \(\langle \mathfrak {F}, V \rangle , T \nVdash \blacksquare p\). Also, by assumption, \(T \nleq s_{i}\) (0<i<ω), which mean that \(\langle \mathfrak {F}, V \rangle , T \Vdash p\). Now let R ^{ # } T v and suppose that \(\langle \mathfrak {F}, V \rangle , v \Vdash \blacksquare p\) but \(\langle \mathfrak {F}, V \rangle , v \nVdash p\). The latter means that v ≤ s _{ i } for some 0<i<ω, however since \(\langle \mathfrak {F}, V \rangle , s_{i+1} \nVdash p\) and R ^{ # } s _{ i } s _{ i+1}, it must be that \(\langle \mathfrak {F}, V \rangle , s_{i} \nVdash \blacksquare p\), and by the Hereditary Lemma, \(\langle \mathfrak {F}, V \rangle , v \nVdash \blacksquare p\). Hence, \(\langle \mathfrak {F}, V \rangle , T \Vdash \blacksquare (\blacksquare p \supset p)\). Similarly, if (iii) fails, we have some x,y such that R ^{ # } T x and R ^{ # } x y but not R ^{ # } T y. Just consider a valuation V such that \(V(p)=\{w : w \nleq x, y \}\). V (p) turns out to be upwards closed under ≤ due to the transitivity of ≤. This concludes the left to right direction of the proposition.
For the converse suppose \(\langle \mathfrak {F}, V \rangle , T \nVdash \blacksquare (\blacksquare p \supset p) \wedge p \supset \blacksquare p\). If (i) holds, one can build the desired sequence to falsify (ii) by taking x such that R ^{ # } T x while \(\langle \mathfrak {F}, V \rangle , x \nVdash p\) and applying \(\langle \mathfrak {F}, V \rangle , T \Vdash \blacksquare (\blacksquare p \supset p)\) in conjunction with (iii). □
To see that the conjunction of conditions (i) and (ii) in Proposition 6 is not a first order property, let us suppose it is to derive a contradiction. Say ϕ is the first order formula expressing (i) and (ii). Expand the correspondence language by adding a constant c _{ i } for each i>0. Let Δ be the collection of first order formulas axiomatizing our class of RoutleyMeyer frames and Θ the set of first order formulas {O(T),R ^{ # } T c _{1},R ^{ # } c _{ i } c _{ i+1} : 0<i<ω}. For each n>0, take the frame \(\mathfrak {F}_{n}\) where W = {k : k ≤ n}, R = {〈0,i, i〉 : i ≤ n}∪{〈j,j + 1,j + 1〉 : j<n}, T is simply the number 0 while O = {0} and ∗ the identity. Each finite subset of {ϕ}∪ Δ ∪ Θ has a model in \(\mathfrak {F}_{n}\) for sufficiently large n. By compactness, the whole thing must have a model, which is impossible since ϕ forbids Θ from being true by assumption.
So we have seen that at the level of frames, the language of relevant logic can go beyond the expressive power of first order logic. More precisely, the fragment of monadic second order logic corresponding to the language of relevant logic over frames can express some nonfirst order concepts. Does it contain first order logic, though? We will give next an easy argument that it does not (though there was never a reason to believe that it did). This shows that the “relevant fragment” of monadic second order logic is indeed incomparable with first order logic in terms of expressive power.
Definition 2

(i) x and f(x) satisfy the same propositional variables.

(ii) R x y z only if R ^{′} f(x)f(y)f(z).

(iii) \(f(x)^{*^{\prime }} = f(x^{*}) \).

(iv) \(R^{\prime }f(x)y^{\prime }z^{\prime }\) only if there are y,z such that R x y z and f(y) = y ^{′} and f(z) = z ^{′}.

(v) f(x) ∈ O ^{′} for x ∈ O

(vi) R ^{′} y ^{′} z ^{′} f(x) only if there are y,z such that R y z x and f(y) = y ^{′} and f(z) = z ^{′}.

(vii) R ^{′} y ^{′} z ^{′} f(x) for y ^{′},z ^{′}∈ O ^{′} only if there are y,z ∈ O such that R y z x and f(y) = y ^{′} and f(z) = z ^{′}.
Lemma 7
Let M,N be two models and f a bounded morphism from M into N. Then, for any world w of M and relevant formula ϕ , \(M, w \Vdash \phi \) iff \(N, f(w) \Vdash \phi \) .
Proof
Routine induction on formula complexity. □
When one omits condition (i) in Definition 2, we might speak of a bounded morphism from a frame \(\mathfrak {F}\) into a frame \(\mathfrak {F}^{\prime }\).
Proposition 8
If there is a bounded morphism f from a frame \(\mathfrak {F} = \langle W, R, *, O \rangle \) into a frame \(\mathfrak {F}^{\prime } = \langle W^{\prime }, R^{\prime }, *^{\prime }, O^{\prime }\rangle \) , then \(\mathfrak {F} \Vdash \phi \) implies \(\mathfrak {F}^{\prime } \Vdash \phi \) for any relevant formula ϕ .
Proof
Suppose \(\mathfrak {F}^{\prime } \nVdash \phi \). So there is a valuation V ^{′} such hat \(\langle \mathfrak {F}, V^{\prime } \rangle , T \nVdash \phi \) for some T ∈ O. Consider now the valuation V such that V (p) = {x ∈ W : f(x) ∈ V ^{′}(p)} for any p. Note that V (p) is closed under ≤ in \(\mathfrak {F}\). For suppose x ∈ V (p) (i.e., f(x) ∈ V ^{′}(p)) and x ≤ y in \(\mathfrak {F}\), which by conditions (ii) and (v) in Definition 2 and our assumption, implies that f(x) ≤ f(y). Hence, f(y) ∈ V ^{′}(p), which means that y ∈ V (p). So f is now a bounded morphism from the model \(\langle \mathfrak {F}, V \rangle \) into the model \(\langle \mathfrak {F}^{\prime }, V^{\prime } \rangle \), which, using Proposition 8, means that \(\mathfrak {F} \nVdash \phi \). □
Finally, let \(\mathfrak {F}_{1}\) be the frame 〈W,R,∗,{s,t}〉 where W = {s,t}, R = W × W × W and ∗ = {〈t,t〉,〈s,t〉}. On the other hand, let \(\mathfrak {F}_{2}\) be the frame 〈W ^{′},R ^{′},∗^{′},{s}〉 where W ^{′} = {s}, R = W ^{′}× W ^{′}× W ^{′} and ∗ is the identity. There is only one function f : W→W ^{′}. The function f is a bounded morphism from \(\mathfrak {F}_{1}\) onto \(\mathfrak {F}_{2}\) as it is easy to check. The first order property ∃x(O x ∧ x≠x ^{∗}) (where the denotation of T is s in both \(\mathfrak {F}_{1}\) and \(\mathfrak {F}_{2}\)) holds at \(\mathfrak {F}_{1}\) but fails at \(\mathfrak {F}_{2}\), so by Proposition 8, ∃x(O x ∧ x≠x ^{∗}) is not definable by a relevant formula.
4 A Sahlqvist Correspondence Theorem
In this section, we prove the result promised in Section 1 using the groundwork layed out in Section 2. In the proof we use lambda terms as in [3], which are to be understood as predicate constants (i.e., the denotation of the lambda term λ u.(ϕ) is fixed by the set of worlds satisfying ϕ).
Lemma 9
Let ϕ, 𝜃, ψ and χ be relevant formulas such that 𝜃 contains no propositional variable and ϕ and χ have no propositional variable in common. Suppose ϕ,ψ and χ have first order frame correspondents. Then 𝜃 → ϕ,ϕ ∧ ψ and ϕ ∨ χ have first order correspondents.
Proof
Suppose ϕ ^{′},ψ ^{′},χ ^{′} are the first order local correspondents of ϕ,ψ and χ respectively.
Definition 3
A formula ϕ → ψ is called a relevant Sahlqvist implication if ψ is positive while ϕ is a formula built up from propositional atoms, double negated atoms (i.e., formulas of the form ∼∼ p), negative formulas, the constant t and implications of the form t → p (for any propositional variable p) using only the connectives ∨,∧ and ∘.
Example 10
p∧∼ p → q,∼∼ p → p,p ∘ q → p ∧ q,((p ∘ q) ∨ (t → p)) → p ∨ q, p → (t∨∼t → p) and (t → p) → p are all relevant Sahlqvist implications according to Definition 3, while (p → (p → q)) → (p → q) is not since, for one thing, T _{ x }(p → q) is not a positive formula.
Lemma 11
Every relevant Sahlqvist implication has a local first order correspondent on RoutleyMeyer frames.
Proof

(T) ∀P _{1},…,P _{ n }∀y,z(U p _{≤}(P _{1}) ∧… ∧ U p _{≤}(P _{ n }) ∧ R x y z ∧ T _{ x }(ϕ)^{ y/x } ⊃ T _{ x }(ψ)^{ z/x }).

(∃x 𝜃(x) ∧ σ) ≡∃x(𝜃(x) ∧ σ),

(∃x 𝜃(x) ⊃ σ) ≡∀x(𝜃(x) ⊃ σ),

(𝜃 ∨ δ ⊃ σ) ≡ ((𝜃 ⊃ σ) ∧ (δ ⊃ σ)),

∀P _{1},…,P _{ n }∀x _{1},…, x _{ k }(𝜃∧σ) ≡ ((∀P _{1},…, P _{ n }∀x _{1},…, x _{ k }…𝜃)∧(∀P _{1},…, P _{ n }∀x _{1},…, x _{ k }…σ)),

(1) ∀P _{1},…,P _{ n }∀x _{1},…,x _{ k }(U p _{≤}(P _{1})∧…∧U p _{≤}(P _{ n })∧REL∧(DN)AT∧IMP∧NEG ⊃POS).

(2) \([\lambda u.(u \nleq u)/P_{i}]\forall P_{1}, {\dots } , P_{i1}, P_{i+1}, {\dots } , P_{n} \forall x_{1}, {\dots } , x_{k} (Up_{\leq }(P_{1}) \\ \quad \wedge {\dots } \wedge Up_{\leq }(P_{n}) \wedge \text {REL} \wedge \text {(DN)AT} \wedge \text {IMP} \wedge \text {NEG} \supset \text {POS}),\)

(3) ∀P _{1},…,P _{ n }∀x _{1},…,x _{ k }(U p _{≤}(P _{1})∧…∧U p _{≤}(P _{ n })∧REL∧(DN)AT∧IMP ⊃¬NEG∨POS).
Suppose π _{1}(x _{ i1}),…,π _{ k }(x _{ i k }) are all the conjuncts of (DN)AT and IMP in the antecedent of (3) in which the unary predicate P _{ i } occurs. Then if π _{ j }(x _{ i j }) appears in one of the conjuncts in IMP, it must be a formula of the form ∀y z(R x _{ i j } y z ∧∃b(O b ∧ b ≤ y) ⊃ P _{ i } z), in which case we define σ(π _{ j }(x _{ i j })) = λ u.(∃y z(R x _{ i j } y z ∧∃b(O b ∧ b ≤ y) ∧ z ≤ u)). On the other hand if π _{ j }(x _{ i j }) appears in one of the conjuncts in (DN)AT we put σ(π _{ j }(x _{ i j })) = λ u.(x _{ i j } ≤ u) in case π _{ j }(x _{ i j }) = P _{ i } x _{ i j } and σ(π _{ j }(x _{ i j })) = λ u.(x i j∗∗≤ u) in case π _{ j }(x _{ i j }) = ¬¬P _{ i } x i j∗∗. Note that σ is a welldefined function and that for any π _{ j }(x _{ i j }), if π _{ j }(x _{ i j })[w] then ∀y(σ(π _{ j }(x _{ i j })(y) ⊃ P _{ i } y)[w]. Next define δ(P _{ i }) = λ u.(σ(π _{1}(x _{ i1}))(u) ∨… ∨ σ(π _{ k }(x _{ i k }))(u)). Now, if (DN)AT[w w _{1}…w _{ k }] and IMP[w w _{1}…w _{ k }] then ∀u(δ(P _{ i })(u) ⊃ P _{ i } u)[w w _{1}…w _{ k }].

(4) [δ(P _{1})/P _{1}…δ(P _{ n })/P _{ n }]∀x _{1},…,x _{ k }(U p _{≤}(P _{1})∧…∧U p _{≤}(P _{ n })∧REL∧(DN)AT∧IMP ⊃¬NEG∨POS),

(5) ∀x _{1},…,x _{ k }(REL ⊃ [δ(P _{1})/P _{1}…δ(P _{ n })/P _{ n }](¬NEG ∨POS)).
The procedure in the above proof is better understood by working out some examples, which we will do next for the benefit of the reader.
Example 12
Example 13
The above condition reduces to ∀x(x ^{∗∗}≤ x ∧ x ≤ x ^{∗∗}) when we consider validity with respect to all the worlds in O of the frame. This is not the same in general as ∀x(x = x ^{∗∗}) which is the condition usually required to validate ∼∼ p → p. However, it is certainly the case that, using the construction from Theorem 5 [12], by restricting our attention to just the frames where ≤ is antisymmetric, we get exactly the same set of validities as in the general case.
Example 14
Example 15
All that is left is to verify that \(\mathfrak {F} \vDash \forall y, z (Rxyz \supset \exists u_{2}u_{3} (Ryu_{2}u_{3} \wedge \exists b(Ob \wedge b\leq u_{2}) \wedge u_{3} \leq z))\) does locally correspond to (t → p) → p. Take a frame \(\mathfrak {F}\) such that \(\mathfrak {F} \vDash \forall y, z (Rxyz \supset \exists u_{2}u_{3} (Ryu_{2}u_{3} \wedge \exists b(Ob \wedge b\leq u_{2}) \wedge u_{3} \leq z))[w]\). Let M be any RoutleyMeyer model based on \(\mathfrak {F}\). Consider arbitrary worlds w _{1},w _{2} such that R w w _{1} w _{2} holds in M and suppose that \(M, w_{1} \Vdash \textbf {t} \rightarrow p\), which means that ∀u,v(R y u v ∧∃b(O b ∧ b ≤ u) ⊃ P v) holds in M. Since R w w _{1} w _{2}, we can conclude that ∃u _{2} u _{3}(R w _{1} u _{2} u _{3} ∧∃b(O b ∧ b ≤ u _{2}) ∧ u _{3} ≤ w _{2}), but then P u _{3}, and, by the Hereditary Lemma, P w _{2} as desired. On the other hand, suppose that \(\mathfrak {F} \nvDash \forall y, z (Rxyz \supset \exists u_{2}u_{3} (Ryu_{2}u_{3} \wedge \exists b(Ob \wedge b\leq u_{2}) \wedge u_{3} \leq z))[w]\), so there are worlds w _{1},w _{2} such that R w w _{1} w _{2} and \(\forall u_{2}u_{3} (Rw_{1}u_{2}u_{3} \wedge \exists b(Ob \wedge b\leq u_{2}) \supset u_{3} \nleq w_{2})\). Take any model M based on \(\mathfrak {F}\) such that \(V(p) = \{x \in W : x \nleq w_{2}\}\). V (p) is upward closed under ≤ thanks to the transitivity of ≤. Also, using the reflexivity of ≤, it is easy to see that \(M, w \nVdash (\textbf {t} \rightarrow p) \rightarrow p\), as desired.
Definition 4
A formula ϕ → ψ is called a dual relevant Sahlqvist implication if ψ is negative while ϕ is a formula built up from negated propositional atoms (i.e. formulas of the form ∼ p), triple negated atoms (i.e., formulas of the form ~ p), positive formulas, the constant ∼t and implications of the form p →t (for any propositional variable p) using only the connectives ∨,∧ and ∘.
Lemma 16
Every dual relevant Sahlqvist implication has a local first order correspondent on RoutleyMeyer frames.
Proof

(1) ∀P _{1},…,P _{ n }∀x _{1},…,x _{ k }(U p _{≤}(P _{1})∧…∧U p _{≤}(P _{ n })∧REL∧(T)NAT∧IMP∧∧POS ⊃NEG),
As before, we may assume that any unary predicate (corresponding to a propositional variable) appearing in NEG, appears also in the antecedent of (1). Otherwise, instantiate the given unary predicate P _{ i } appearing in NEG (and not in the antecedent of (1)) to λ u.(u ≤ u) getting a formula (1) ^{′} −and note that U p _{≤}(λ u.(u ≤ u)). As before, using (the contrapositive of) Lemma 3 and the fact that a negative formula is just the (boolean) negation of a positive formula, we see that (1) ^{′} implies (1), so they are indeed equivalent.

(1) ∀P _{1},…,P _{ n }∀x _{1},…,x _{ k }(U p _{≤}(P _{1})∧…∧U p _{≤}(P _{ n })∧REL∧(T)NAT∧IMP ⊃¬POS∨NEG),
Finally, let π _{1}(x _{ i1}),…,π _{ k }(x _{ i k }) be all the conjuncts of (T)NAT and IMP in the antecedent of (3) in which the unary predicate P _{ i } occurs. Then if π _{ j }(x _{ i j }) appears in one of the conjuncts in IMP, it must be a formula of the form ∀y z(R x _{ i j } y z ∧ P _{ i } y ⊃∃b(O b ∧ b ≤ z)), in which case we define σ(π _{ j }(x _{ i j })) = λ u.(∀z(R x _{ i j } u z ⊃∃b(O b ∧ b ≤ z))). On the other hand if π _{ j }(x _{ i j }) appears is one of the conjuncts in (T)NAT we put \(\sigma (\pi _{j}(x_{ij})) = \lambda u. (u \nleq x_{ij}^{*} )\) in case π _{ j }(x _{ i j }) = ¬P _{ i } x i j∗ and \(\sigma (\pi _{j}(x_{ij})) = \lambda u. (u \nleq x_{ij}^{***} )\) in case π _{ j }(x _{ i j }) = ¬¬¬P _{ i } x i j∗∗∗. Note that σ is a welldefined function and that for any π _{ j }(x _{ i j }), if π _{ j }(x _{ i j })[w] then, then ∀y(P _{ i } y ⊃ σ(π _{ j }(x _{ i j }))(y))[w]. Next define δ(P _{ i }) = λ u.(σ(π _{1}(x _{ i1}))(u) ∧… ∧ σ(π _{ k }(x _{ i k }))(u)). Now, if (T)NAT[w w _{1}…w _{ k }] and IMP[w w _{1}…w _{ k }] then ∀u(P _{ i } u ⊃ δ(P _{ i })(u))[w w _{1}…w _{ k }]. The remainder of the proof is as before but using again the contrapositive formulation of Lemma 3 and noting that the intersection of a collection of upward closed sets under ≤ is also upward closed under ≤. □
Example 17
Definition 5
A relevant Sahlqvist formula is any formula built up from (dual) relevant Sahlqvist implications, propositional variables, and negated propositional variables using ∧, the operations on formulas Θ (for any propositional variable free relevant formula 𝜃) defined by Θ(ϕ) = 𝜃 → ϕ, and applications of ∨ where the disjuncts share no propositional variable in common.
Theorem 18
Every relevant Sahlqvist formula has a local first order correspondent on RoutleyMeyer frames.
Proof
Immediate from Lemma 11, Lemma 16 and Lemma 9. The only thing the reader should note is that \(\mathfrak {F}, w \Vdash p\) iff \(\mathfrak {F} \vDash x \nleq x[w]\) and \(\mathfrak {F}, w \Vdash \sim p\) iff \(\mathfrak {F} \vDash x^{*} \nleq x^{*} [w]\). □
5 Conclusion
In this paper we have defined a fragment of relevant languages analogue to the Sahlqvist fragment of modal logic. We then went to establish that every class of RoutleyMeyer frames definable by a formula in this fragment is actually elementary. This isolates a modest but remarkable collection of relevant formulas. We also showed that there are properties of RoutleyMeyer frames definable by relevant formulas which are not first order axiomatizable.
Footnotes
 1.
The RoutleyMeyer framework remains today the most prominent nonalgebraic approach to the semantics of propositional relevant languages (cf. [4, 8]). Recent applications (e.g., [15, 19]) are easy to find. The RoutleyMeyer semantics has also been given an appropriate philosophical justification in [2] and much more recently in [9]. If anything comes close to being the “standard” relational semantics for propositional relevant logics, it surely is the RoutleyMeyer approach.
 2.
Many thanks to an anonymous referee who pointed this out.
 3.
Note that in [7] elementary classes are called “basic elementary”.
Notes
Acknowledgments
Open access funding provided by Johannes Kepler University Linz. I am grateful to an anonymous reviewer for several useful corrections and references that helped greatly to improve the paper. I am indebted as well to Ed Mares and Katalin Bimbó for their comments. Finally, we also acknowledge the support by the Austrian Science Fund (FWF): project I 1923N25 (New perspectives on residuated posets).
References
 1.Bimbó, K., & Dunn, M., (2008). Generalized Galois Logics: Relational Semantics of Nonclassical Logical Calculi.. CSLI Publications.Google Scholar
 2.Beall, J.C. & et al. (2012). On the ternary relation and conditionality. Journal of Philosophical Logic, 41(3), 595–612.CrossRefGoogle Scholar
 3.Blackburn, P., de Rijke, M., & Venema, Y. (2001). Modal logic. Cambridge.Google Scholar
 4.Brady, R.T. & et al. (2003). Relevant logics and their rivals, 2 Ashgate.Google Scholar
 5.Celani, S., & Jansana, R. (1999). Priestley duality, a Sahlqvist theorem and a GoldblattThomason theorem for positive modal logic. Logic Journal of the IGPL, 7 (6), 683–715.CrossRefGoogle Scholar
 6.Chagrov, A., & Zakharyaschev, M. (1997). Modal logic. Clarendon Press.Google Scholar
 7.Chang, C.C., & Keisler, H.J. (1992). Model theory. NorthHolland.Google Scholar
 8.Dunn, M. (2015). The relevance of relevance to relevance logic. In Logic and its applications: 6th indian conference (ICLA), lecture notes in computer science, no. 8923: 1129.Google Scholar
 9.Dunn, M., & Restall, G. (2002). Relevance logic. In Gabbay, D., & Guenthner, F. (Eds.) Handbook of Philosophical Logic: Kluwer.Google Scholar
 10.Goldblatt, R.I. (1975). First order definability in modal logic. Journal of Symbolic Logic, 40(1), 35–40.CrossRefGoogle Scholar
 11.Hodges, W. (1993). Model theory. Cambridge.Google Scholar
 12.Kremer, P. (1993). Quantifying over propositions in relevance logic: Nonaxiomatizability of primary interpretations of p and p. Journal of Symbolic Logic, 58(1), 334–349.CrossRefGoogle Scholar
 13.Meyer, R.K., & Routley, R. (1972). Algebraic analysis of entailment. Logique et Analyse, 15, 407–428.Google Scholar
 14.Restall, G. (2000). An introduction to substructural logics. Routledge.Google Scholar
 15.Robles, G., & Méndez, J.M. (2010). A RoutleyMeyer type semantics for relevant logics including Br plus the disjunctive syllogism. Journal of Philosophical Logic, 39, 139–158.CrossRefGoogle Scholar
 16.Routley, R. & et al. (1983). Relevant logics and their rivals, 1 Ridgeview.Google Scholar
 17.Seki, T. (2003). A sahlqvist theorem for relevant modal logics. Studia Logica, 73(3), 383–411.CrossRefGoogle Scholar
 18.Suzuki, T. (2013). A Sahlqvist theorem for substructural logic. The Review of Symbolic Logic, 6, 243–276.CrossRefGoogle Scholar
 19.Thomas, M. (2015). A generalization of the RoutleyMeyer semantic framework. Journal of Philosophical Logic, 44(4), 411–427.CrossRefGoogle Scholar
 20.van Benthem, J.F.A.K. (1975). A note on modal formulas and relational properties. Journal of Symbolic Logic, 40(1), 55–58.CrossRefGoogle Scholar
 21.van Benthem, J.F.A.K. (1976). Modal formulas are either elementary or not ΣΔElementary. Journal of Symbolic Logic, 41, 436–438.CrossRefGoogle Scholar
Copyright information
Open AccessThis article is distributed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted use, distribution, and reproduction in any medium, provided you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license, and indicate if changes were made.