Positive Modal Logic Beyond Distributivity

We know that f^{-1} is a semilattice homomorphism. The map f^{-1} preserves the bottom element because f^{-1}(\{ \top' \}) = \{ \top \}.

For preservation of joins, we need to show that

for a', b' \in \mathcal{F}(X', \top', \wedge'). The inclusion \supseteq follows from the fact that f^{-1}(a' \mathbin{\triangledown} b') is a filter that contains both f^{-1}(a') and f^{-1}(b'). Conversely, if x \in f^{-1}(a' \mathbin{\triangledown} b') then f(x) \in a' \mathbin{\triangledown} b' so there exist y' \in a' and z' \in b' such that y' \wedge z' \leq f(x). Since f is an L-frame morphism, we can find y, z \in X such that y' \leq f(y) and z' \leq f(z) and y \wedge z \leq x. This means that y \in f^{-1}(a') and z \in f^{-1}(b'), and hence x \in f^{-1}(a') \mathbin{\triangledown} f^{-1}(b').

We know that h^{-1} is a semilattice homomorphism, so we only have to show that it satisfies the additional conditions from Definition 2.4.

For the first one, suppose h^{-1}(p') = L (L is the top element of \mathcal{F} L). Then \bot \in h^{-1}(p'), so \bot' = h(\bot) \in p', and therefore p' = L'.

Next, let p' \in \mathcal{F} L' and q, r \in \mathcal{F} L and suppose q \cap r \subseteq h^{-1}(p'). Let q' := {\uparrow}h[q] and r' := {\uparrow} h[r]. Then it is easy to verify that q' and r' are filters (because q and r are), and by construction q \subseteq h^{-1}(q') and r \subseteq h^{-1}(r'). It remains to show that q' \cap r' \subseteq p'.

Let a' \in L' be such that a' \in q' \cap r'. Since a' \in q' there exists a \in q such that h(a) \leq a'. Since a' \in r' there exists b \in r such that h(b) \leq a'. But then a \vee b \in q \cap r, so by assumption h(a \vee b) \in p'. This implies a' \in p', because h(a \vee b) = h(a) \vee h(b) \leq a' and p' is a filter (hence up-closed).

The implication (ii) \Rightarrow (iii) follows from the HMS separation axiom and (iii) \Rightarrow (i) is obvious. For (i) \Rightarrow (ii), suppose c is not principal. Then for each x \in c there exists a y \in c strictly below x. So for each x \in c, using the HMS separation axiom, we can find a clopen filter a_x such that c \not\subseteq a_x. Then \{ a_x \mid x \in c \} is an open cover of c without finite subcover. (Indeed, for every finite collection a_{x_1}, \ldots, a_{x_n} we can find y_1, \ldots, y_n such that y_i \in c but y_i \notin a_i. Then y_1 \wedge \cdots \wedge y_n is in c but not in any of the a_{x_i}.) So c is not compact, hence not closed.

If y \notin {\uparrow}c then for each x \in c we have x \not\leq y, hence a clopen filter a_x containing x but not y. Then c \subseteq \bigcup_{x \in c} a_x, so by compactness we find a finite subcover, say, c \subseteq a_1 \cup \cdots \cup a_n. Since all the a_i are upward closed, we have {\uparrow}c \subseteq a_1 \cup \cdots \cup a_n. By construction, none of the a_i contain y, so X \setminus (a_1 \cup \cdots \cup a_n) is an open neighbourhood of y disjoint from {\uparrow}c.

We only have to verify that the restriction of \mathcal{F}_{clp} to \mathsf{LSpace} lands in \mathsf{Lat}, and the restriction of \mathcal{F}_{top} to \mathsf{Lat} lands in \mathsf{LSpace}.

The former follows from the fact that the clopen filters of an L-space are closed under \mathbin{\triangledown}, together with Proposition 2.5.

For the latter, suppose that L is a lattice and let \theta_L(a) and \theta_L(b) be two arbitrary clopen filters of \mathcal{F}_{top} L.

Writing x, y, z for elements in \mathcal{F}_{top} L, we have

Let us elaborate on the last equality.

If x \in \theta_L(a) and y \in \theta_L(b) then a \in x and b \in y, so a \vee b \in x \cap y. So z \supseteq x \cap y implies a \vee b \in z, and therefore we have “\subseteq”. Conversely, if z \in \theta_L(a \vee b) then we need to find x \in \theta_L(a) and y \in \theta_L(b) such that x \cap y \subseteq z. Let x = {\uparrow}a \in \theta_L(a) and y = {\uparrow}b \in \theta_L(b). Then d \in x \cap y implies a \leq d and b \leq d, hence a \vee b \leq d. Since z \in \theta_L(a \vee b) this implies d \in z, and therefore x \cap y \subseteq z. This proves “\supseteq”. The restriction on morphisms follows from Proposition 2.6.

The first item follows from the lattice of principal filters of L being isomorphic to L^\circ and \mathcal{F} L = (\operatorname{\mathcal{fe}} L)^o. The second item is similar to [MosJip09, Theorem 4.1]. Finally, the third item follows from the mentioned above connection between filter and ideal completions \operatorname{\mathcal{ie}} L = (\operatorname{\mathcal{fe}} L^\circ)^\circ together with \mathcal{F} L = (\operatorname{\mathcal{fe}} L)^o.

The “only if” holds by definition. Conversely, if A \in \mathsf{Lat}(\Gamma) and \mathscr{A} = (A, \sigma_A) is a lattice model, then the assignment [p] \mapsto \sigma_A(p) extends to a lattice homomorphism i : \mathscr{L}_{\Gamma} \to \mathscr{A} such that [\varphi] = \llparenthesis\kern.2ex \varphi \kern.2ex\rrparenthesis_{\mathscr{A}}. (This is well defined because A validates all consequence pairs in \Gamma.) Then \llparenthesis\kern.2ex \varphi \kern.2ex\rrparenthesis_{\mathscr{L}_{\Gamma}} \leq_L \llparenthesis\kern.2ex \psi \kern.2ex\rrparenthesis_{\mathscr{L}_{\Gamma}} implies [\varphi] \leq_L [\psi]. Monotonicity of i yields \llparenthesis\kern.2ex \varphi \kern.2ex\rrparenthesis_{\mathscr{A}} \leq_L \llparenthesis\kern.2ex \psi \kern.2ex\rrparenthesis_{\mathscr{A}}, hence \varphi \mathrel{\kern.1ex\text{ \tikz[baseline=-.81ex, line width=.1ex, line cap=round, scale=1.1] {\draw (0ex,-.75ex) -- (0ex,.75ex); \draw (0ex,0ex) -- (1ex,0ex); \draw (-.4ex,0ex) arc(180:235:.91ex); \draw (-.4ex,0ex) arc(180:125:.91ex);}_}}\kern.1ex \psi.

By Lemma 3.4 it suffices to show that \varphi \vdash_{\Gamma} \psi if and only if \llparenthesis\kern.2ex \varphi \kern.2ex\rrparenthesis_{\mathscr{L}_{\Gamma}} \leq_L \llparenthesis\kern.2ex \psi \kern.2ex\rrparenthesis_{\mathscr{L}_{\Gamma}}.

It follows from the conjunction rules, reflexivity and transitivity that \varphi \vdash_{\Gamma} \psi if and only if \varphi \wedge \psi \dashv\vdash_{\Gamma} \varphi. Therefore we have \varphi \vdash_{\Gamma} \psi if and only if [\varphi \wedge \psi] = [\varphi] in \mathscr{L}_{\Gamma}, and since [\varphi \wedge \psi] = [\varphi] \wedge_L [\psi] this holds if and only if [\varphi] \leq_L [\psi]. Recalling that [\varphi] = \llparenthesis\kern.2ex \varphi \kern.2ex\rrparenthesis_{\mathscr{L}_{\Gamma}} completes the proof.

The fact that \llbracket \varphi \rrbracket^{\mathfrak{M}} is a filter for each \varphi follows from Lemma 3.8. Suppose \mathfrak{M} is principal. Then \llbracket p \rrbracket^{\mathfrak{M}} is principal by definition, as are \llbracket \bot \rrbracket^{\mathfrak{M}} = {\uparrow}\top and \llbracket \top \rrbracket^{\mathfrak{M}} = {\uparrow} 0. If \varphi = \varphi_1 \wedge \varphi_2 or \varphi_1 \vee \varphi_2 then we proceed by induction. We may assume that \llbracket \varphi_1 \rrbracket^{\mathfrak{M}} = {\uparrow}x_1 and \llbracket \varphi_2 \rrbracket^{\mathfrak{M}} = {\uparrow}x_2, so that \llbracket \varphi_1 \wedge \varphi_2 \rrbracket^{\mathfrak{M}} = {\uparrow}(x_1 \curlyvee x_2) and \llbracket \varphi_1 \vee \varphi_2 \rrbracket^{\mathfrak{M}} = {\uparrow}(x_1 \curlywedge x_2).

If \mathfrak{M} is an L-model that validates all consequence pairs in \Gamma, then \mathfrak{M}^* \in \mathsf{Lat}(\Gamma). Since \varphi \vdash_{\Gamma} \psi, Theorem 3.5 yields \varphi \mathrel{\kern.1ex\text{ \tikz[baseline=-.81ex, line width=.1ex, line cap=round, scale=1.1] {\draw (0ex,-.75ex) -- (0ex,.75ex); \draw (0ex,0ex) -- (1ex,0ex); \draw (-.4ex,0ex) arc(180:235:.91ex); \draw (-.4ex,0ex) arc(180:125:.91ex);}_}}\kern.1ex \psi, and hence \llparenthesis\kern.2ex \varphi \kern.2ex\rrparenthesis_{\mathfrak{M}^*} \leq \llparenthesis\kern.2ex \psi \kern.2ex\rrparenthesis_{\mathfrak{M}^*}. Lemma 3.8 now implies \llbracket \varphi \rrbracket^{\mathfrak{M}} \leq \llbracket \psi \rrbracket^{\mathfrak{M}}, so that \mathfrak{M} validates \varphi \trianglelefteqslant \psi.

The first “iff” follows from the fact that clopen valuations of \mathbb{X} correspond bijectively to assignments of the proposition letters for A, together with a routine induction on the structure of \varphi. The second “iff” follows immediately from the first.

Soundness holds by definition, so we prove completeness. Suppose \varphi \not\vdash_{\Gamma} \psi. Then by Theorem 3.5 we can find a lattice A validating all consequence pairs in \Gamma, but not \varphi \trianglelefteqslant \psi. As a consequence of Lemma 3.14 the L-space \mathbb{X} dual to A validates all consequence pairs in \Gamma but does not validate \varphi \trianglelefteqslant \psi, thus we find completeness with respect to \mathsf{D\hyphen LFrm}(\Gamma).

Since \mathbb{X} \not\Vdash \varphi \trianglelefteqslant \psi there must exist a clopen valuation V such that (\mathbb{X}, V) \not\Vdash \varphi \trianglelefteqslant \psi. Therefore (\kappa\mathbb{X}, V) \not\Vdash \varphi \trianglelefteqslant \psi. Besides, Lemma 3.16 implies that \kappa\mathbb{X} validates all consequence pairs in \Gamma. This implies completeness with respect to \mathsf{LFrm}(\Gamma).

Lastly, we note that \mathbb{X} is a principal L-frame and since V is clopen is assigns to each proposition letter a principal filter. Thus \mathbb{X} is a principal L-frame validating \Gamma but not \varphi \trianglelefteqslant \psi, proving completeness with respect to \mathsf{PLFrm}(\Gamma).

The first item follows immediately from the definition of the standard translation, and the other item follows from the first one.

If \mathfrak{X}, w \Vdash \psi \trianglelefteqslant \chi then w \in V(\psi) implies w \in V(\chi) for every valuation V for \mathfrak{X}. If any of the P_i is interpreted as a subset of X that is not a filter, then the implication inside the quantifiers in (3.21) is automatically true, because the antecedent is false. If all P_i are interpreted as filters, then the implication holds because of the assumption.

The converse is similar.

We know that \mathfrak{X}, w \Vdash \psi \trianglelefteqslant \chi if and only if \mathfrak{X}^{\circ} \models \operatorname{so}(\psi \trianglelefteqslant \chi)[w]. Our strategy for obtaining a first-order correspondent is to remove all second-order quantifiers from the second-order translation. We assume that no two quantifiers bind the same variable.

If \psi is equivalent to \top then as a consequence of Lemma 3.24 \psi \trianglelefteqslant \chi is equivalent to \top \trianglelefteqslant \chi', where \chi' is obtained from \chi by replacing all proposition letters with \bot. This, in turn, implies that \operatorname{so}(\top \trianglelefteqslant \chi') is a first-order correspondent of \top \trianglelefteqslant \chi, since the lack of proposition letters in \chi' implies that there are no second-order quantifiers in \operatorname{so}(\top \trianglelefteqslant \chi').

If \psi is equivalent to \bot then \psi \trianglelefteqslant \chi is vacuously valid on all L-frames. So we may assume that the antecedent does not use \top or \bot.

Let p_1, \ldots, p_n be the propositional variables occurring in \psi, and write P_1, \ldots, P_n for their corresponding unary predicates. We assume that every proposition letter that occurs in \chi also occurs is \psi, for otherwise we may replace it by \bot to obtain a formula which is equivalent in terms of validity on frames.

Step 1.

Use equivalences of the form

to pull out all quantifiers that arise in \operatorname{st}_x(\psi). Let Y := \{ y_1, \ldots, y_m \} denote the set of (bound) variables that occur in the antecedent of the implication from the second-order translation. We end up with a formula of the form

Here \operatorname{ISFIL} = \mathsf{isfil}(P_1) \wedge \cdots \wedge \mathsf{isfil}(P_n), \operatorname{AT} is a conjunction of formulae of the form P_iz and \operatorname{REL} is a conjunction of formulae of the form \mathsf{abovemeet}(z; z', z''), where z, z', z'' \in Y \cup \{ x \}.

Step 2. Next we read off minimal instances of the P_i making the antecedent true. Intuitively, these correspond to the smallest valuations for the p_i making the antecedent true.

For each proposition letter P_i, let P_iy_{i_1}, \ldots, P_iy_{i_k} be the occurrences of P_i in \operatorname{AT} in the antecedent of (?). We define the valuation of p_i to be the filter generated by the (interpretations of) y_{i_1}, \ldots, y_{i_k}. Formally,

(If k = 0, i.e. there is no variable y with P_iy, then we let \sigma(P_i) = \lambda u.(u \neq u).)

Then for each L-model \mathfrak{M} and states x', y_1', \ldots, y_m' in \mathfrak{M} we have

If we replace each unary predicate P in (?) with \sigma(P), then all conjoints in \operatorname{ISFIL} and \operatorname{AT} become true. Writing [\sigma(P)/P]\operatorname{st}_x(\chi) for the formula obtained from \operatorname{st}_x(\chi) by replacing each instance of a unary predicate P with \sigma(P), we arrive at the first-order formula

Step 3. Finally, we claim that for every L-frame \mathfrak{X}, \mathfrak{X}^{\circ} validates (?) if and only if it validates (?). The implication from left to right is simply an instantiation of the quantifiers as filters. For the converse, assume that \mathfrak{M} is some model based on \mathfrak{X}, so that \mathfrak{M}^{\circ} is an extension of \mathfrak{X}^{\circ} giving the interpretations of the unary predicates as filters. We may disregard the case where any of them is not a filter as that would make the antecedent in (?) false, hence the whole implication true. Let x', y_1', \ldots, y_m' be states in \mathfrak{M} and assume that

We need to show that \mathfrak{M}^{\circ} \models \operatorname{st}_x(\chi)[x', y_1', \cdots, y_m']. It follows from the assumption that (?) holds that \mathfrak{M}^{\circ} \models [\sigma(P)/P]\operatorname{st}_x(\chi)[x', y_1', \cdots, y_m']. Moreover, as a consequence of (?) we have \mathfrak{M}^{\circ} \models \forall y(\sigma(P)(y) \to Py) for all P \in \{ P_1, \ldots, P_n \}. Using Lemma 3.24 it follows that \mathfrak{M}^{\circ} \models \operatorname{st}_x(\chi)[x', y_1', \cdots, y_m'], as desired.

We assume that \mathfrak{M} is not principal; the case for principal modal L-models is similar. The proof proceeds by induction on the structure of \varphi. The only non-trivial cases are the modal cases. We prove the statement for \varphi = \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\psi; the case \varphi = \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex\psi is similar.

Suppose \varphi = \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\psi, \mathfrak{M}, x \Vdash \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\psi and x \preccurlyeq y. Then there exists an R-successor z of x satisfying \psi, and by (?) we can find an R-successor w of y such that z \preccurlyeq y. By the induction hypothesis we then find \mathfrak{M}, w \Vdash \psi and therefore \mathfrak{M}, y \Vdash \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\psi.

Next, suppose that both x and y satisfy \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\psi. Then there exist v \in R[x] and w \in R[y] satisfying \psi. By (?) we have (x \curlywedge y)R(v \curlywedge w) and by the induction hypothesis \mathfrak{M}, v \curlywedge w \Vdash \psi. Therefore \mathfrak{M}, x \curlywedge y \Vdash \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\psi. Lastly, (?) implies \mathfrak{M}, 1 \Vdash \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\psi. We conclude that \llbracket \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\psi \rrbracket^{\mathfrak{M}} is a filter in (X, 1, \curlywedge).

This follows from a routine induction on the structure of \varphi. We showcase the modal cases of the proof. Suppose \varphi = \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex\psi. It follows immediately from Definition 4.4(?) that \mathfrak{M}', f(x) \Vdash \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex\psi implies \mathfrak{M}, x \Vdash \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex\psi. So suppose \mathfrak{M}, x \Vdash \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex\psi. If y' is an R'-successor of f(x), then there exists some z \in X such that xRz and f(z) \preccurlyeq y'. This implies \mathfrak{M}, z \Vdash \psi and by induction \mathfrak{M}', f(z) \Vdash \psi. Persistence then yields \mathfrak{M}', y' \Vdash \psi. Therefore \mathfrak{M}', f(x) \Vdash \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex\psi.

If \varphi = \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\psi Then the preservation from left to right follows from Definition 4.4(?). Conversely, if \mathfrak{M}', f(x) \Vdash \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\psi, then there exists a y' \in X' such that f(x)Ry' and \mathfrak{M}', y' \Vdash \psi. By (?) we can find some w \in X such that xRw and y' \preccurlyeq f(w). Persistence implies \mathfrak{M}', f(w) \Vdash \psi and induction yields \mathfrak{M}, w \Vdash \psi. Therefore \mathfrak{M}, x \Vdash \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\psi.

All of these follow immediately from the definition of the interpretation of \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex and \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex. In particular, they do not rely on any of the conditions from Definition 4.1.

Suppose y \notin R[x]. Then there exists a clopen filter a such that either x \in [R]a and y \notin a, or y \in a and x \notin \langle R \rangle a. In the first case X \setminus a is a clopen neighbourhood of y disjoint from R[x]. In the second case a is a clopen neighbourhood of y disjoint from R[x].

We know that L-spaces have all non-empty meets, and hence also binary joins, so (?) is satisfied. Furthermore, (?) is satisfied by definition. We verify the other conditions from Definition 4.1, starting with (?).

Condition ?. Suppose x_iRy_i, where i ranges over some index set I. If I = \emptyset then this condition states 1 R 1 which holds by definition, so assume that I \neq \emptyset. By the tightness condition of modal L-spaces, in order to prove (\bigcurlywedge x_i)R(\bigcurlywedge y_i) it suffices to show that for all clopen filters a, \bigcurlywedge x_i \in [R]a implies \bigcurlywedge y_i \in a and \bigcurlywedge y_i \in a implies \bigcurlywedge x_i \in \langle R \rangle a.

First assume \bigcurlywedge x_i \in [R]a. Since [R]a is a clopen filter and \bigcurlywedge x_i \preccurlyeq x_j for each j \in I we have x_j \in [R]a, so R[x_j] \subseteq a. By assumption x_jRy_j, so y_j \in a for all j \in I. Since a is a clopen filter it is principal, hence \bigcurlywedge y_i \in a.

Second, suppose \bigcurlywedge y_i \in a. Then y_j \in a for all j \in I, which implies x_j \in \langle R \rangle a for all j \in I. Since \langle R \rangle a is a clopen filter, hence principal, we find \bigcurlywedge x_i \in \langle R \rangle a.

Condition ?. Let x \preccurlyeq y and yRz. Suppose towards a contradiction that there exists no w \in X such that xRw and w \preccurlyeq z. Let x' = \bigcurlywedge R[x] be the minimal element in R[x] (which is an R-successor of x by (?)). Then x' \not\preccurlyeq z, so we can find a clopen filter a containing x' such that z \notin a. This implies R[x] \subseteq a, so that x \in [R]a, but y \notin [R]a because yRz and z \notin a. As x \preccurlyeq y this violates the fact that [R]a is a filter.

Condition ?. Let x \preccurlyeq y and xRw. Suppose towards a contradiction that there exists no z \in X such that yRz and w \preccurlyeq z. Then R[y] \cap {\uparrow}w = \emptyset. Both R[y] and {\uparrow}z are closed, as a consequence of Lemmas 4.12 and 2.9 and the fact that singletons in a Stone spaces are always closed. Therefore we can find a clopen filter a containing {\uparrow}z which is disjoint from R[y]. This implies that x \in \langle R \rangle a while y \notin \langle R \rangle a. Since x \preccurlyeq y this contradicts the fact that \langle R \rangle a is a filter.

Condition ?. Finally, let \{ x_i \mid i \in I \} be some collection of elements of X and suppose (\bigcurlywedge x_i)Rz. If I is empty then \bigcurlywedge x_i = 1 and Definition 4.11(?) implies z = 1,

and the empty collection witnesses truth of (?).

So assume I \neq \emptyset. Since \bigcurlywedge x_i \preccurlyeq x_j for all j \in I, condition (?) implies that R[x_j] \neq \emptyset for all j \in I. As a consequence of (?) there is a smallest element z_j := \bigcurlywedge R[x_j] in each R[x_j]. We claim that \bigcurlywedge z_j \leq z. Suppose not, then there is a clopen filter a containing \bigcurlywedge z_j such that z \notin a. This implies x_j \in [R]a for all j \in I, but \bigcurlywedge x_i \notin [R]a because (\bigcurlywedge x_i)Rz and z \notin a. But this contradicts the fact that [R]a is principal filter.

The left-to-right inclusion of the first equality follows from the fact that c \subseteq a implies [R]c \subseteq [R]a. For the converse, suppose x \in \mathbb{X} is such that x \notin [R]c. Then R[x] \not\subseteq c, so there is some y \in R[x] such that y \notin c. Since c is a closed filter, it is the intersection of all clopen filters that contain it. A routine compactness argument yields a clopen filter b containing c such that y \notin b. Therefore R[x] \not\subseteq b, so x \notin [R]b and hence x is not in the right hand side of the equality.

For the second equality, it suffices to prove the right-to-left inclusion as well. Suppose x \notin \langle R \rangle c. Then R[x] \cap c = \emptyset. Since R[x] is closed, we can use compactness to find some clopen filter a containing c disjoint from R[x], and the argument proceeds as above.

Next, consider (4.15). We know that c \subseteq d implies [R]c \subseteq [R]d, and since the latter is a filter containing [R]c for all closed filters c \subseteq d, it contains the filter generated by them. This proves \supseteq. Conversely, suppose x \in [R]d. Then R[x] \subseteq d. Since d is up-closed we also have {\uparrow} R[x] \subseteq d. The set {\uparrow} R[x] is closed by Lemmas 4.12 and 2.9, and it is a filter because R[x] is closed under \curlywedge. Thus we have found a closed filter c := {\uparrow} R[x] contained in d such that x \in [R]c. This proves \subseteq.

The right-to-left inclusion of the second equality in (4.15) is easy again. For \subseteq, suppose x \in \langle R \rangle d. Then R[x] \cap d \neq \emptyset, so we can find some y \in R[x] \cap d. Now {\uparrow} y is a closed filter contained in d such that x \in \langle R \rangle({\uparrow} y), witnessing \subseteq.

The maps [R], \langle R \rangle are functions on \mathcal{F}_{clp}\mathbb{X} by definition. It follows from Proposition 4.13 and Lemma 4.6 that they satisfy the conditions from Definition 4.8.

If f is a modal L-space morphism then in particular it is an L-space morphism, so \mathcal{F}_{clp} f is a lattice homomorphism from \mathcal{F}_{clp}\mathbb{X}' to \mathcal{F}_{clp}\mathbb{X}. So we only have to show that f^{-1} preserves the modalities. This can be proven in the same way as in Proposition 4.5.

The set \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex^{-1}(p) is a filter because \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex : A \to A preserves conjunctions and the top element.

To show pR_A\hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex^{-1}(p) we need to prove \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex^{-1}(p) \subseteq \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex^{-1}(p) \subseteq \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex^{-1}(p). The left inclusion is trivial. For the right one, suppose a \in \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex^{-1}(p). Then \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex a \in p. Besides, \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\top = \top \in p. So the duality axiom implies \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex\top \wedge \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex a \leq \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex(\top \wedge a) = \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex a \in p, hence a \in \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex^{-1}(p).

Suppose p \in [R_A]\theta_A(a). By Lemma 4.19 we have pR_A\hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex^{-1}(p) and by assumption a \in \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex^{-1}(p). This implies that \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex a \in p and therefore p \in \theta_A(\hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex a).

For the reverse inclusion, suppose p \in \theta_A(\hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex a). Then a \in \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex^{-1}(p), so pR_Aq implies a \in q, and hence p \in [R_A]\theta_A(a).

Next, suppose p \in \langle R_A \rangle\theta_A(a). Then there exists a filter q such that pR_Aq and a \in q. By definition of R_A this implies a \in \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex^{-1}(p) and hence \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex a \in p, so p \in \theta_A(\hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex a).

Conversely, suppose p \in \theta_A(\hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex a). Let q be the filter generated by \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex^{-1}(p) and a. We claim that c \in q implies \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex c \in p. To see this, note that for each c \in q there exists some d \in \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex^{-1}(p) such that d \wedge a \leq c. We then have \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex d \in p, and \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex a \in p by assumption, so \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex d \wedge \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex a \in p. Since \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex d \wedge \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex a \leq \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex(d \wedge a) \leq \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex c we find \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex c \in p. The filter q is nonempty because it contains \top. Furthermore, we have \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex^{-1}(p) \subseteq q by definition of q and we just showed that c \in q implies \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex c \in p, so that q \subseteq \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex^{-1}(p). This proves pR_Aq. By design a \in q so q witnesses the fact that p \in \langle R_A \rangle \theta_A(a).

We verify the condition from Definition 4.11. Item (?) follows from Theorem 2.13. Item (?) follows from Lemma 4.19. Item (?) follows from Lemma 4.20. Item (?) follows from the definition of R_A and the fact that each clopen filter is of the form \theta_A(a).

It follows from the duality between lattices and L-spaces that h^{-1} is an L-space morphism, so we only have to verify the three conditions from Definition 4.4. We write R' and R for the relations from \mathscr{A}'_* and \mathscr{A}_*.

1. Let p' and q' be filters of \mathscr{A}' (elements of \mathscr{A}'_*) such that p'R'q'. In order to prove that h^{-1}(p')Rh^{-1}(q') we have to show that \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex^{-1}(h^{-1}(p')) \subseteq h^{-1}(q') \subseteq \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex^{-1}(h^{-1}(p')). Let a \in \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex^{-1}(h^{-1}(p')). Then \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex a \in h^{-1}(p') so \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex'(h(a)) = h(\hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex a) \in p'. Therefore h(a) \in (\hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex')^{-1}(p'), and since p'R'q' this implies h(a) \in q', so that a \in h^{-1}(q').

   Next, if a \in h^{-1}(q') then h(a) \in q', so h(\hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex a) = \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex' h(a) \in p'. Therefore \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex a \in h^{-1}(p') so that a \in \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex^{-1}(h^{-1}(p')).

2. Suppose h^{-1}(p')Rq.

   Lemma 4.19 then implies that p'R'(\hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex')^{-1}(p').

   So it suffices to show that h^{-1}((\hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex')^{-1}(p')) \subseteq q. To this end, suppose a \in h^{-1}((\hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex')^{-1}(p')). Then h(\hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex a) = \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex' h(a) \in p', so \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex a \in h^{-1}(p'). Since h^{-1}(p')Rq this implies a \in q, as desired.

3. Suppose h^{-1}(p')Rq. Then {\uparrow}h[q] is a filter (since h is a lattice homomorphism it is non-empty and closed under meets). Let q' be the filter generated by {\uparrow}h[q] and (\hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex')^{-1}(p'). Then q \subseteq h^{-1}(q') by construction, so it suffices to show that p'R'q'. We have (\hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex')^{-1}(p') \subseteq q' by definition, so we only have to show that q' \subseteq (\hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex')^{-1}(p'). Let a' \in q'. Then there are b' \in (\hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex')^{-1}(p') and c \in q such that b' \wedge' h(c) \leq a'. We find

   \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex'b' \wedge h(\hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex c) = \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex'b' \wedge \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex' h(c) \leq \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex a'.

   By construction we have \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex'b' \in p'. Furthermore, c \in q implies \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex c \in h^{-1}(p') and hence h(\hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex c) \in p'. Therefore \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex a' \in p', and consequently p'R'q'.

Let \mathbb{X} = (X, \leq, \tau, R) be a modal L-space. This gives rise to the modal lattice \mathbb{X}^* = (\mathcal{F}_{clp} \mathbb{X}, [R], \langle R \rangle), which in turn yields a modal L-space (\mathbb{X}^*)_* = (\mathcal{F} \mathcal{F}_{clp} \mathbb{X}, \mathcal{F}_{clp}\mathbb{X}, \cap, \tau_{\mathcal{F}_{clp}\mathbb{X}}, R_{\mathcal{F}_{clp}\mathbb{X}}). As a consequence of the duality for lattices (Theorem 2.13) we know that (X, 1, \curlywedge, \tau) is isomorphic to (\mathcal{F}_b\mathcal{F}_{clp}\mathbb{X}, A, \cap, \tau_{\mathcal{F}_{clp}\mathbb{X}}) via x \mapsto \eta_{\mathbb{X}}(x) = \{ a \in \mathcal{F}_{clp}\mathbb{X} \mid x \in a \}. So we only have to show that R and R_{\mathcal{F}_{clp}\mathbb{X}} coincide. This can be seen as follows:

Next, let \mathscr{A} = (A, \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex, \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex) be a modal lattice, \mathscr{A}_* = (\mathcal{F} A, R_A) and (\mathscr{A}_*)^* = (\mathcal{F}_{clp}\mathcal{F} A, [R_A], \langle R_A \rangle). Then the duality for lattices from Theorem 2.13 tells us that A and \mathcal{F}_{clp}\mathcal{F} A are isomorphic via a \mapsto \theta_A(a) = \{ p \in \mathcal{F} A \mid a \in p \}, so we just have to show that \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex coincides with [R_A] and \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex coincides with \langle R_A \rangle. That is, we have to show that \theta_A(\hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex a) = [R_A]\theta_A(a) and \theta_A(\hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex a) = \langle R_A \rangle \theta_A(a). But we have already proven that in Lemma 4.20.

The two paragraphs above establish the duality on objects. The duality for morphisms follows immediately from Theorem 2.13 and the fact that all our categories are concrete.

Let \mathbb{X} = (X, 1, \curlywedge, \tau, R_A) be the modal L-space dual to \mathscr{A}. By Proposition 2.16 we can identify the filter extension of A with the lattice of closed filters of \mathbb{X} with inclusion \theta : A \to \mathcal{F}_k(\mathbb{X}).

In \mathcal{F}_k(\mathbb{X}, the top, bottom and meet are given by X, \{ 1 \} and intersection, and the join of a collection of filters is the smallest filter containing their union.

So we only have to verify that for all c \in \mathcal{F}_k(\mathbb{X}) we have \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex^{\operatorname{\mathcal{fe}}}c = [R_A]c and \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex^{\operatorname{\mathcal{fe}}}c = \langle R_A \rangle c. Thus compute

Similarly we find \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex^{\operatorname{\mathcal{fe}}}c = \langle R_A \rangle c for all c \in \mathcal{F}_k(\mathbb{X}).

For the second item we adopt a similar strategy. Using Proposition 2.16, we identify the \Pi_1-completion of A with \mathcal{F}(\mathbb{X}), the filters of \mathbb{X} with operators as in (?), and inclusion \theta : A \to \mathcal{F}(\mathbb{X}). We view the filter completion of A as sitting inside the \Pi_1-completion, just like \mathcal{F}_k(\mathbb{X}) \subseteq \mathcal{F}(\mathbb{X}). Then we already know that \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex^{\operatorname{\mathcal{fe}}}c = [R_A]c for all closed filters, wherefore

for all filters d. We use Lemma 4.15 for the last equality. Similarly we find \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex^{\operatorname{\Pi_1}}d = \langle R_A \rangle d.

We have \mathscr{A} \mathrel{\kern.1ex\text{ \tikz[baseline=-.81ex, line width=.1ex, line cap=round, scale=1.1] {\draw (0ex,-.75ex) -- (0ex,.75ex); \draw (0ex,0ex) -- (1ex,0ex); \draw (-.4ex,0ex) arc(180:235:.91ex); \draw (-.4ex,0ex) arc(180:125:.91ex);}_}}\kern.1ex \varphi \trianglelefteqslant \psi iff \mathscr{A} \mathrel{\kern.1ex\text{ \tikz[baseline=-.81ex, line width=.1ex, line cap=round, scale=1.1] {\draw (0ex,-.75ex) -- (0ex,.75ex); \draw (0ex,0ex) -- (1ex,0ex); \draw (-.4ex,0ex) arc(180:235:.91ex); \draw (-.4ex,0ex) arc(180:125:.91ex);}_}}\kern.1ex \varphi \wedge \psi = \varphi, so it suffices to focus on equalities. The proposition letters play the role of variables, and every valuation of the proposition letters to elements in \mathscr{A} extends to valuations for \varphi and \psi in the obvious way.

So suppose \mathscr{A} \mathrel{\kern.1ex\text{ \tikz[baseline=-.81ex, line width=.1ex, line cap=round, scale=1.1] {\draw (0ex,-.75ex) -- (0ex,.75ex); \draw (0ex,0ex) -- (1ex,0ex); \draw (-.4ex,0ex) arc(180:235:.91ex); \draw (-.4ex,0ex) arc(180:125:.91ex);}_}}\kern.1ex \varphi = \psi. Let \sigma be any valuation for \operatorname{\mathcal{fe}}(\mathscr{A}) and a \in A. We aim to prove that a \in \sigma(\varphi) if and only if a \in \sigma(\psi). So suppose a \in \sigma(\varphi). Then by Lemma 4.28(?) we can find a valuation \theta for \mathscr{A} such that \theta(\varphi) \leq a. By assumption \mathscr{A} \mathrel{\kern.1ex\text{ \tikz[baseline=-.81ex, line width=.1ex, line cap=round, scale=1.1] {\draw (0ex,-.75ex) -- (0ex,.75ex); \draw (0ex,0ex) -- (1ex,0ex); \draw (-.4ex,0ex) arc(180:235:.91ex); \draw (-.4ex,0ex) arc(180:125:.91ex);}_}}\kern.1ex \varphi = \psi, so \theta(\psi) = \theta(\varphi) \leq a, hence by Lemma 4.28(?) we find a \in \sigma(\psi). Similarly we can prove that a \in \sigma(\psi) implies a \in \sigma(\varphi) so that \sigma(\varphi) = \sigma(\psi). Since \sigma is arbitrary, we conclude \operatorname{\mathcal{fe}}(\mathscr{A}) \mathrel{\kern.1ex\text{ \tikz[baseline=-.81ex, line width=.1ex, line cap=round, scale=1.1] {\draw (0ex,-.75ex) -- (0ex,.75ex); \draw (0ex,0ex) -- (1ex,0ex); \draw (-.4ex,0ex) arc(180:235:.91ex); \draw (-.4ex,0ex) arc(180:125:.91ex);}_}}\kern.1ex \varphi = \psi.

We start with the first statement. We proceed by induction on the structure of \varphi.

If \varphi = p \in \operatorname{Prop} then we set \theta(p) = a and \theta(q) = \top for all other q \in \operatorname{Prop}. If \varphi = \top then \theta(\top) = \top \in \{ \top \} = \sigma(\top), and if \varphi = \bot then \theta(\bot) = \bot \in A = \sigma(\bot).

Suppose \varphi = \varphi_1 \wedge \varphi_2. If a \in \sigma(\varphi_1 \wedge \varphi_2) = \sigma(\varphi_1) \mathbin{\triangledown} \sigma(\varphi_2) then there are a_1 \in \sigma(\varphi_1) and a_2 \in \sigma(\varphi_2) such that a_1 \wedge a_2 \leq a. The induction hypothesis then gives valuations \theta_1, \theta_2 for \mathscr{A} such that \theta_1(\varphi_1) \leq a_1 and \theta_2(\varphi_2) \leq a_2, and such that \theta_1(p) \in \sigma_1(p) and \theta_2(p) \in \sigma_2(p) for all p \in \operatorname{Prop}. Let \theta = \theta_1 \wedge \theta_2. Since \theta_i(p) \in \sigma(p) for all p \in \operatorname{Prop}, and \sigma(p) is a filter, we have \theta(p) \in \sigma(p) for all p \in \operatorname{Prop}. Then \theta(\varphi_i) \leq \theta_i(\varphi_i) for i \in \{ 1, 2 \}, and we find \theta(\varphi_1 \wedge \varphi_2) = \theta(\varphi_1) \wedge \theta(\varphi_2) \leq \theta_1(\varphi_1) \wedge \theta_2(\varphi_2) \leq a_1 \wedge a_2 \leq a.

If \varphi = \varphi_1 \vee \varphi_2, then a \in \sigma(\varphi_1 \vee \varphi_2) = \sigma(\varphi_1) \cap \sigma(\varphi_2) so there are valuations \theta_1, \theta_2 such that \theta_1(\varphi_1) \leq a and \theta_2(\varphi_2) \leq a, and such that \theta_1(p) \in \sigma_1(p) and \theta_2(p) \in \sigma_2(p) for all p \in \operatorname{Prop}. Let again \theta = \theta_1 \wedge \theta_2. Then just as above \theta(p) \in \sigma(p) for all p \in \operatorname{Prop}. Moreover, \theta(\varphi_1 \vee \varphi_2) = \theta(\varphi_1) \vee \theta(\varphi_2) \leq \theta_1(\varphi_1) \vee \theta_2(\varphi_2) \leq a \vee a = a.

Finally, let \scalebox{.75}{\text{\faStarO}} \in \{ \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex, \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex \} and \varphi = \scalebox{.75}{\text{\faStarO}} \varphi_1. Suppose a \in \sigma(\scalebox{.75}{\text{\faStarO}} \varphi_1). Then

The last equality follows from the fact that filters are ordered by reverse inclusion, so that \sigma(\varphi_1) \leq {\uparrow} b iff \sigma(\varphi_1) \supseteq {\uparrow} b iff b \in \sigma(\varphi_1).

Since \bigwedge in \operatorname{\mathcal{fe}}(\mathscr{A}) is defined as \operatorname{\bigtriangledown}, there exist b_1, \ldots, b_n \in A such that b_i \in \sigma(\varphi_1) for all i \in \{ 1, \ldots, n \} and \scalebox{.75}{\text{\faStarO}} b_1 \wedge \cdots \wedge \scalebox{.75}{\text{\faStarO}} b_n \leq a.

The induction hypothesis implies that there exist valuations \theta_1, \ldots, \theta_n for \mathscr{A} such that \theta_i(\varphi_1) \leq b_i and \theta_i(p) \in \sigma(p) for all p \in \operatorname{Prop} and i \in \{ 1, \ldots, n \}. Since \scalebox{.75}{\text{\faStarO}} is monotone we find \theta_i(\scalebox{.75}{\text{\faStarO}}\varphi_1) = \scalebox{.75}{\text{\faStarO}} \theta_i(\varphi_1) \leq \scalebox{.75}{\text{\faStarO}} b_i for all i. Letting \theta = \theta_1 \wedge \cdots \wedge \theta_n gives \theta(\scalebox{.75}{\text{\faStarO}}\varphi_1) \leq \theta_i(\scalebox{.75}{\text{\faStarO}}\varphi_1) \leq \scalebox{.75}{\text{\faStarO}} b_i for all i, so that \theta(\scalebox{.75}{\text{\faStarO}}\varphi_1) \leq \scalebox{.75}{\text{\faStarO}} b_1 \wedge \cdots \wedge \scalebox{.75}{\text{\faStarO}} b_n \leq a, as desired. Since \sigma(p) is a filter and \theta_i(p) \in \sigma(p) for all i \in \{ 1, \ldots, n \} we find \theta(p) \in \sigma(p) for all p \in \operatorname{Prop}.

We prove the second item by induction on the structure of \varphi as well. The base cases \varphi = \top, \bot, p \in \operatorname{Prop} are routine. Suppose \varphi = \varphi_1 \wedge \varphi_2. By induction we have \theta(\varphi_1) \in \sigma(\varphi_1) and \theta(\varphi_2) \in \sigma(\varphi_2). So \theta(\varphi_1 \wedge \varphi_2) = \theta(\varphi_1) \wedge \theta(\varphi_2) \in \sigma(\varphi_1) \mathbin{\triangledown} \sigma(\varphi_2) = \sigma(\varphi_1 \wedge \varphi_2). If \varphi = \varphi_1 \vee \varphi_2, then with the same induction hypothesis we find \theta(\varphi_i) \leq \theta(\varphi_1 \vee \varphi_2) so \theta(\varphi_1 \vee \varphi_2) \in \sigma(\varphi_i) for i \in \{ 1, 2 \}. Therefore \theta(\varphi_1 \vee \varphi_2) \in \sigma(\varphi_1) \cap \sigma(\varphi_2) = \sigma(\varphi_1 \vee \varphi_2).

Lastly suppose \scalebox{.75}{\text{\faStarO}} \in \{ \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, line width=.12ex] {\draw (-.6ex,-.6ex) rectangle (.6ex,.6ex);}}\kern.2ex, \hspace{.2ex}\text{ \tikz[baseline=-.6ex, rounded corners=.01ex, rotate=45, line width=.12ex] {\draw (-.5ex,-.5ex) rectangle (.5ex,.5ex);}}\kern.2ex \} and \varphi = \scalebox{.75}{\text{\faStarO}} \varphi_1. By the induction hypothesis we have \theta(\varphi_1) \in \sigma(\varphi_1), so \sigma(\varphi_1) \supseteq {\uparrow} \theta(\varphi_1) and since \operatorname{\mathcal{fe}}(\mathscr{A}) is ordered by reverse inclusion, it follows from the definition of \scalebox{.75}{\text{\faStarO}}^{\operatorname{\mathcal{fe}}} that \scalebox{.75}{\text{\faStarO}}^{\operatorname{\mathcal{fe}}}\sigma(\varphi_1) \supseteq {\uparrow} \scalebox{.75}{\text{\faStarO}} \theta(\varphi_1), hence

as desired.

Similar to the proof of Theorem 3.17.

By Lemma ... we have \mathfrak{X}, w \Vdash \psi \trianglelefteqslant \chi if and only if \mathfrak{X}^{\circ} \models \operatorname{so}(\psi \trianglelefteqslant \chi)[w]. As in Theorem 3.25, our strategy for obtaining a first-order formula is to remove all second-order quantifiers from \operatorname{so}(\psi \trianglelefteqslant \chi)[w].

We assume that no two quantifiers bind the same variable. The case where \psi = \top or \bot can be handled as in Theorem 3.25.

Let p_1, \ldots, p_n be the propositional variables occurring in \psi, and write P_1, \ldots, P_n for their corresponding unary predicates. We assume that every proposition letter that occurs in \chi also occurs is \psi, for otherwise we may replace it by \bot to obtain a formula which is equivalent in terms of validity on frames.

Step 1. Use equivalences of the form

and

to pull out all existential quantifiers that arise in \operatorname{st}_x(\psi). Let Y := \{ y_1, \ldots, y_m \} denote the set of (bound) variables that arise in the antecedent of the implication from the second-order translation. We end up with a formula of the form

where

• \operatorname{ISFIL} is a conjunction of formulae of the form \mathsf{isfil}(P_i);

• \operatorname{BOX\hyphen AT} is a conjunction of standard translations of boxed proposition letters, i.e. formulae of the form \forall z(z'R^nz \to P_iz) (here P_iz is viewed as \forall z(z'R^0z \to P_iz));

• \operatorname{REL} is a conjunction of formulae of the form zRz' and \mathsf{abovemeet}(z;, z', z'').

Step 2. Next we read off minimal instances of the P_i making the antecedent true.

For each proposition letter P_i, let \forall y_{i_1}(z_{i_1}R^{n_1}y_{i_1} \to P_iy_{i_1}), \ldots, \forall y_{i_k}(z_{i_k}R^{n_k}y_{i_k} \to P_iy_{i_k}) be the occurrences of P_i in \operatorname{BOX\hyphen AT} in the antecedent of (?). Intuitively, we define the valuation of p_i to be the filter generated by the (interpretations of) y_{i_1}, \ldots, y_{i_k}. Formally,

(If k = 0, i.e. there are no boxed atoms involving P_i in the formula, then we take the empty meet to be falsum, i.e. \sigma(P_i) = \lambda u.(u \neq u).)

The remainder of the proof is analogous to the proof of Theorem 3.25.