# Toward the van Benthem Characterization Theorem for Non-Distributive Modal
Logic

Yiwen Ding${}^{\,a}$ Krishna Manoorkar${}^{\,a}$ Mattia Panettiere${}^{\,a}$
Ruoding Wang${}^{\,a,\,b}$ Vrije Universiteit Amsterdam, The Netherlands
Xiamen University, China

###### Abstract

In this paper, we introduce the simulations and bisimulations on polarity-
based semantics for non-distributive modal logic, which are natural
generalizations of those notions on Kripke semantics for modal logic. We also
generalize other important model-theoretic notions about Kripke semantics such
as image-finite models, modally-saturated models, ultrafilter extension and
ultrapower extension to the non-distributive setting. By using these
generalizations, we prove the Hennessy-Milner theorem and the van Benthem
characterization theorem for non-distributive modal logic based on polarity-
based semantics.

###### keywords:

Polarity-based semantics, Non-distributive modal logics, Simulations,
Bisimulations, Hennessy-Milner theorem, van Benthem characterization theorem.

††thanks: This project has received funding from the European Union’s Horizon
2020 research and innovation programme under the Marie Skłodowska-Curie grant
agreement No 101007627. The research of Krishna Manoorkar is supported by the
NWO grant KIVI.2019.001. Yiwen Ding and Ruoding Wang are supported by the
China Scholarship Council.

##  1 Introduction

This paper focuses on advancing the model theory of polarity-based semantics
for normal non-distributive modal logics [16, 6, 9]. These logics, also known
as LE-logics (lattice expansion logics), are characterized by algebraic
semantics provided by arbitrary lattices expanded with normal operators.
Leveraging the interpretation of polarities as formal contexts in Formal
Concept Analysis [17], non-distributive modal logic is conceptualized as a
logic of formal concepts or categories enriched with modal operators, such as
approximation or knowledge operators [6, 7]. Several model theoretic notions
for polarity-based semantics like disjoint unions, p-morphisms, and
ultrafilter extensions were introduced in prior work [10]. These concepts were
used in [10] to prove Goldblatt-Thomason theorem for LE-logics. Simulations on
polarity-based models were defined and employed to demonstrate the
preservation of lattice-based modal $\mu$-calculus (an extension of basic LE-
logic with the least and the greatest fixed point operators) under simulations
[14, Section 6]. In this paper, we delve more into the problem of generalizing
simulations and bisimulations from Kripke semantics to polarity-based
semantics, and also prove fundamental results like Hennessy-Milner theorem and
van Benthem characterization theorem for polarity-based semantics.

Bisimulations were initially defined by van Benthem [31] as p-relations on
Kripke frames for classical modal logic. They aim to characterize points in
Kripke models with equivalent behavior concerning modal logic formulas. Since
their inception, bisimulations have played an important role in modal logic
theory and its applications in computer science [31, 27, 20, 18]. Hennessy and
Milner [21] showed that on image-finite Kripke models, the semantic
equivalence relation for modal logic forms a bisimulation relation, a result
later extended to modally-saturated Kripke models [22]. Van Benthem [31]
established the characterization theorem for modal logic, showing that
classical modal logic is the bisimulation-invariant fragment of first-order
logic.

Bisimulations have been extensively defined and studied across various
semantic models for different logics. For instance, in topological semantics
for (S4) modal logic, they are referred to as topo-bisimulations [1], where
the Hennessy-Milner property for a class of topological models was established
[11]. Similarly, in Kripke semantics for intuitionistic modal logic, they are
known as asimulations, and results like the Hennessy-Milner theorem and the
van Benthem theorem have been demonstrated [25]. Bezhanishvilli and Henke [3]
proved the van Benthem theorem for models based on general descriptive frames
using Vietoris bisimulations [2]. Similar studies have been carried out for
different semantics of graded modal logics, dynamic modal logics, fuzzy modal
logics, monotone modal logics, etc. [13, 30, 28, 29, 19]. De Groot [12]
established a van Benthem theorem for the meet-semilattice semantics of non-
distributive (positive) logic using the notion of meet simulations. In this
work, we adopt a similar approach to prove the van Benthem theorem for the
polarity-based semantics of normal non-distributive modal logic by defining
appropriate notion of simulations. Along the way, we introduce essential
model-theoretic notions like image-finite models, modally-saturated models,
and $\omega$-saturated models for this semantics, and prove significant
results like the Hennessy-Milner theorem and the Hennessy-Milner property for
the class of modally-saturated models.

Structure of the paper. In Section 2, we collect the required preliminaries.
In Section 3, we define the simulations and bisimulations on the polarity-
based semantics and prove the Hennessy-Milner theorem. In Section 4, we define
the modally-saturated polarity-based models, filter-ideal extensions of
polarity-based models and show that two pointed polarity-based models are
modally equivalent if and only if their filter-ideal extensions are bisimilar.
In Section 5, we define the standard translation and prove the van Benthem
characterization theorem for polarity-based semantics of non-distributive
modal logic. In Section 6, we summarize the main findings of the paper and
suggest some possible future works.

##  2 Preliminary

In this section, we gather useful preliminaries about normal non-distributive
modal logic and its polarity-based semantics based on [9] and [7]. We assume
readers are familiar with the basic concepts from the model theory of
classical modal logic such as simulations, bisimulations, ultrafilter
extensions, standard translations, Hennessy-Milner theorem, and van Benthem
characterization theorem. For a detailed discussion on the model theory of
modal logic, we refer to [4, Section 2].

###  2.1 Non-Distributive Modal Logic

Let $\mathcal{V}$ be a countable set of propositional variables. The language
$\mathcal{L}$ (i.e. set of formulas) is defined as follows:

$\varphi::=p\mid\bot\mid\top\mid\varphi\wedge\varphi\mid\varphi\vee\varphi\mid\Box\varphi\mid\Diamond\varphi$,

where $p\in\mathcal{V}$. Given any $\varphi,\psi\in\mathcal{L}$,
$\varphi\vdash\psi$ is an $\mathcal{L}$-sequent. A normal non-distributive
modal logic is a set of $\mathcal{L}$-sequents containing the following
axioms:

$p\vdash p,\ \ p\vdash\top\ \ \bot\vdash p,\ \ p\vdash p\vee q,\ \ q\vdash
p\vee q,\ \ p\wedge q\vdash p,\ \ p\wedge q\vdash q,\ $
$\top\vdash\Box\top,\ \ \Diamond\bot\vdash\bot,\ \ \Box p\wedge\Box
q\vdash\Box(p\wedge q),\ \ \Diamond(p\vee q)\vdash\Diamond p\vee\Diamond q\ $

and closed under the following inference rules:

$\frac{\varphi\vdash\chi\quad\chi\vdash\psi}{\varphi\vdash\psi}\ \
\frac{\varphi\vdash\psi}{\varphi\left(\chi/p\right)\vdash\psi\left(\chi/p\right)}\
\ \frac{\chi\vdash\varphi\quad\chi\vdash\psi}{\chi\vdash\varphi\wedge\psi}\ \
\frac{\varphi\vdash\chi\quad\psi\vdash\chi}{\varphi\vee\psi\vdash\chi}\ \
\frac{\varphi\vdash\psi}{\Box\varphi\vdash\Box\psi}\ \
\frac{\varphi\vdash\psi}{\Diamond\varphi\vdash\Diamond\psi}$

The smallest such set $\mathbb{L}$ is called the basic normal non-distributive
modal logic. For any sequent $\varphi\vdash\psi$ in $\mathbb{L}$ we denote it
as $\varphi\vdash_{\mathbb{L}}\psi$.

###  2.2 Polarity-Based Semantics

Given any relation $R\subseteq A\times X$ and any $B\subseteq A$, $Y\subseteq
X$, the maps $R^{(1)}:\mathcal{P}(A)\rightarrow\mathcal{P}(X)$ and
$R^{(0)}:\mathcal{P}(X)\rightarrow\mathcal{P}(A)$ are defined as
$R^{(1)}[B]:=\\{x\in X\mid\forall b(b\in B\Rightarrow bRx)\\}$ and
$R^{(0)}[Y]:=\\{a\in A\mid\forall y(y\in Y\Rightarrow aRy)\\}$.

######  Definition 2.1.

A polarity is a tuple $\mathfrak{P}=(A,X,I)$ such that $A$ and $X$ are sets
and $I\subseteq A\times X$ is a binary relation. Given a polarity
$\mathfrak{P}=(A,X,I)$, the maps
$(\cdot)^{\uparrow}:\mathcal{P}(A)\rightarrow\mathcal{P}(X)$ and
$(\cdot)^{\downarrow}:\mathcal{P}(X)\rightarrow\mathcal{P}(A)$ are defined as
follows:

$B^{\uparrow}:=I^{(1)}[B]$ and $Y^{\downarrow}:=I^{(0)}[Y]$, where $B\subseteq
A$ and $Y\subseteq X$.

The maps $(\cdot)^{\uparrow}$ and $(\cdot)^{\downarrow}$ form a Galois
connection between posets $(\mathcal{P}(A),\subseteq)$ and
$(\mathcal{P}(X),\subseteq)$, that is $Y\subseteq B^{\uparrow}$ iff
$B\subseteq Y^{\downarrow}$ for all $B\in\mathcal{P}(A)$ and
$Y\in\mathcal{P}(X)$.

######  Definition 2.2.

A formal concept of the polarity $\mathfrak{P}=(A,X,I)$ is a pair
$([\\![{c}]\\!],(\\![{c}]\\!))$ such that $[\\![{c}]\\!]\subseteq A$,
$(\\![{c}]\\!)\subseteq X$, and $[\\![{c}]\\!]^{\uparrow}=(\\![{c}]\\!)$,
$(\\![{c}]\\!)^{\downarrow}=[\\![{c}]\\!]$. It follows that $[\\![{c}]\\!]$
and $(\\![{c}]\\!)$ are Galois-stable, i.e.
$[\\![{c}]\\!]^{\uparrow\downarrow}=[\\![{c}]\\!]$ and
$(\\![{c}]\\!)^{\downarrow\uparrow}=(\\![{c}]\\!)$. The set
$\mathcal{C}(\mathfrak{P})$ of all the formal concepts of $\mathfrak{P}$ can
be partially ordered as follows: for any $c,d\in\mathcal{C}(\mathfrak{P})$,
$c\leq d$ iff $[\\![{c}]\\!]\subseteq[\\![{d}]\\!]$ iff
$(\\![{d}]\\!)\subseteq(\\![{c}]\\!)$. The poset
$\mathfrak{P}^{+}=(\mathcal{C}(\mathfrak{P}),\leq)$ is a complete lattice –
called the concept lattice of $\mathfrak{P}$ – such that for any
$\mathrm{K}\subseteq\mathcal{C}(\mathfrak{P})$,

$\bigwedge\mathrm{K}=(\bigcap\\{[\\![{c}]\\!]\mid
c\in\mathrm{K}\\},(\bigcap\\{[\\![{c}]\\!]\mid
c\in\mathrm{K}\\})^{\uparrow})$,

$\bigvee\mathrm{K}=((\bigcap\\{(\\![{c}]\\!)\mid
c\in\mathrm{K}\\})^{\downarrow},\bigcap\\{(\\![{c}]\\!)\mid
c\in\mathrm{K}\\})$.

######  Proposition 2.3.

For any polarity $\mathfrak{P}=(A,X,I)$, the concept lattice
$\mathfrak{P}^{+}$ is completely join-generated by the set
$\\{\textbf{a}:=(a^{\uparrow\downarrow},a^{\uparrow})\mid a\in A\\}$, and is
completely meet-generated by the set
$\\{\textbf{y}:=(y^{\downarrow},y^{\downarrow\uparrow})\mid y\in Y\\}$.

######  Theorem 2.4 (Birkhoff’s representation theorem).

Any complete lattice $\mathbf{L}$ is isomorphic to the concept lattice
$\mathfrak{P}^{+}$ of some polarity $\mathfrak{P}$.

######  Definition 2.5.

An $\mathrm{LE}$-frame is a tuple
$\mathfrak{F}=(\mathfrak{P},R_{\Diamond},R_{\Box})$, where
$\mathfrak{P}=(A,X,I)$ is a polarity, and $R_{\Diamond}\subseteq X\times A$
and $R_{\Box}\subseteq A\times X$ are I-compatible relations, i.e., for all
$a\in A$ and $x\in X$, $R^{(0)}_{\Diamond}[a]$ (resp. $R^{(0)}_{\Box}[x]$) and
$R^{(1)}_{\Box}[a]$ (resp. $R^{(1)}_{\Diamond}[x]$) are Galois-stable.

######  Definition 2.6.

For any $\mathrm{LE}$-frame
$\mathfrak{F}=(\mathfrak{P},R_{\Diamond},R_{\Box})$, the complex algebra of
$\mathfrak{F}$ is
$\mathfrak{F}^{+}:=(\mathfrak{P}^{+},\Diamond^{\mathfrak{P}^{+}},\Box^{\mathfrak{P}^{+}})$
where $\mathfrak{P}^{+}$ is the concept lattice of $\mathfrak{P}$,
$\Diamond^{\mathfrak{P}^{+}}$ and $\Box^{\mathfrak{P}^{+}}$ are unary
operators on $\mathfrak{P}^{+}$ defined as follows: for every
$c\in\mathfrak{P}^{+}$,

$\Diamond^{\mathfrak{P}^{+}}(c):=(R^{(0)}_{\Diamond}[[\\![{c}]\\!]]^{\downarrow},R^{(0)}_{\Diamond}[[\\![{c}]\\!]])$
and
$\Box^{\mathfrak{P}^{+}}(c):=(R^{(0)}_{\Box}[(\\![{c}]\\!)],R^{(0)}_{\Box}[(\\![{c}]\\!)]^{\uparrow})$.

Note that $\Diamond^{\mathfrak{P}^{+}}$ (resp. $\Box^{\mathfrak{P}^{+}}$) is
completely join (resp. meet) preserving.

######  Definition 2.7.

A valuation on an $\mathrm{LE}$-frame
$\mathfrak{F}=(\mathfrak{P},R_{\Diamond},R_{\Box})$ is a map
$V:\mathcal{V}\rightarrow\mathfrak{P}^{+}$. For each $p\in\mathcal{V}$, we let
$[\\![{p}]\\!]:=[\\![{V(p)}]\\!]$ (resp. $(\\![{p}]\\!):=(\\![{V(p)}]\\!)$)
denote the extension (resp. intension) of the interpretation of $p$ under $V$.
A valuation can be homomorphically extended to an unique valuation
$\overline{V}:\mathcal{L}\rightarrow\mathfrak{P}^{+}$ on all the
$\mathcal{L}$-formulas. An $\mathrm{LE}$-model is a pair $(\mathfrak{F},V)$,
where $\mathfrak{F}$ is an $\mathrm{LE}$-frame, and $V$ is a valuation on it.

######  Definition 2.8.

For any $\mathrm{LE}$-model $\mathfrak{M}=(\mathfrak{F},V)$, the modal
satisfaction relations $\Vdash$ and $\succ$ are defined inductively as
follows:

$\mathfrak{M},a\Vdash p$ |  iff $a\in[\\![{p}]\\!]_{\mathfrak{M}}$ | $\mathfrak{M},x\succ p$ |  iff $x\in(\\![{p}]\\!)_{\mathfrak{M}}$
---|---|---|---
$\mathfrak{M},a\Vdash\top$ | always | $\mathfrak{M},x\succ\top$ |  iff $(\forall a\in A)aIx$
$\mathfrak{M},x\succ\bot$ | always | $\mathfrak{M},a\Vdash\bot$ |  iff $(\forall x\in X)aIx$
$\mathfrak{M},a\Vdash\varphi\wedge\psi$ |  iff $\mathfrak{M},a\Vdash\varphi$ and $\mathfrak{M},a\Vdash\psi$ | $\mathfrak{M},x\succ\varphi\wedge\psi$ |  iff $(\forall a\in A)$ $(\mathfrak{M},a\Vdash\varphi\wedge\psi\Rightarrow aIx)$
$\mathfrak{M},x\succ\varphi\vee\psi$ |  iff $\mathfrak{M},x\succ\varphi$ and $\mathfrak{M},x\succ\psi$ | $\mathfrak{M},a\Vdash\varphi\vee\psi$ |  iff $(\forall x\in X)$ $(\mathfrak{M},x\succ\varphi\vee\psi\Rightarrow aIx)$
$\mathfrak{M},a\Vdash\Box\varphi$ |  iff $(\forall x\in X)(\mathfrak{M},x\succ\varphi\Rightarrow aR_{\Box}x)$ | $\mathfrak{M},x\succ\Box\varphi$ |  iff $(\forall a\in A)(\mathfrak{M},a\Vdash\Box\varphi\Rightarrow aIx)$
$\mathfrak{M},x\succ\Diamond\varphi$ |  iff $(\forall a\in A)(\mathfrak{M},a\Vdash\varphi\Rightarrow xR_{\Diamond}a)$ | $\mathfrak{M},a\Vdash\Diamond\varphi$ |  iff $(\forall x\in X)(\mathfrak{M},x\succ\Diamond\varphi\Rightarrow aIx)$

Note that unlike the classical modal logic, the modal operators $\Box$ and
$\Diamond$ are not inter-definable in LE-logic. For any $\mathcal{L}$-sequent
$\varphi\vdash\psi$, and an $\mathrm{LE}$-model
$\mathfrak{M}=(\mathfrak{F},V)$, $\mathfrak{M}\vDash\varphi\vdash\psi$ iff
$[\\![{V(\varphi)}]\\!]\subseteq[\\![{V(\psi)}]\\!]$ iff
$(\\![{V(\psi)}]\\!)\subseteq(\\![{V(\varphi)}]\\!)$.

The following theorem states that the basic normal non-distributive modal
logic defined in Section 2.1 is sound and complete w.r.t. the class of
$\mathrm{LE}$-models.

######  Theorem 2.9 (Proposition 3, [7]).

For any unprovable $\mathcal{L}$-sequent $\varphi\vdash\psi$ in the non-
distributive modal logic, there is an $\mathrm{LE}$-model $\mathfrak{M}$ such
that $\mathfrak{M}\nvDash\varphi\vdash\psi$.

###  2.3 Two Sorted First-Order Logic

Given a countable set of propositional variables $\mathcal{V}$, we let
$\mathcal{L}^{1}$ be the two sorted first-order language with equality built
over two disjoint countable sets of variables $G$ and $M$, three binary
predicates $I$, $R_{\Box}$, $R_{\Diamond}$, and two unary predicates $P_{A}$
and $P_{X}$ for every $p\in\mathcal{V}$. A domain for $\mathcal{L}^{1}$ is a
pair of disjoint sets $A$ and $X$. An interpretation $\mathrm{I}$ of
$\mathcal{L}^{1}$ over domain $(A,X)$ assigns binary predicates $I$,
$R_{\Box}$, and $R_{\Diamond}$ to relations $I^{\mathrm{I}}\subseteq A\times
X$, ${R^{\mathrm{I}}}_{\Box}\subseteq A\times X$, and
${R^{\mathrm{I}}}_{\Diamond}\subseteq X\times A$, such that
${R^{\mathrm{I}}}_{\Box}$ and ${R^{\mathrm{I}}}_{\Diamond}$ are
$I^{\mathrm{I}}$-compatible. For every propositional variable
$p\in\mathcal{V}$, the unary predicates $P_{A}$ and $P_{X}$ are assigned to
sets $P^{\mathrm{I}}_{A}\subseteq A$, $P^{\mathrm{I}}_{X}\subseteq X$, such
that, $(I^{\mathrm{I}})^{(1)}[P^{\mathrm{I}}_{A}]=P^{\mathrm{I}}_{X}$, and
$(I^{\mathrm{I}})^{(0)}[P^{\mathrm{I}}_{X}]=P^{\mathrm{I}}_{A}$, respectively.
An $\mathcal{L}^{1}$-structure is a tuple $\mathfrak{M}=(A,X,\mathrm{I})$,
where $\mathrm{I}$ is an interpretation of $\mathcal{L}^{1}$ over domain $A$
and $X$. A valuation on an $\mathcal{L}^{1}$\- structure $\mathfrak{M}$ is a
map $v$ which assigns every variable $g\in G$ (resp. $m\in M$) to an element
$a\in A$ (resp. $x\in X$). The satisfaction relation for any
$\mathcal{L}^{1}$-term w.r.t. any $\mathcal{L}^{1}$\- structure $\mathfrak{M}$
and valuation $v$ on it is defined as follows:

1\. $\mathfrak{M},v\vDash g_{1}=g_{2}$ iff $v(g_{1})=v(g_{2})$ |  2\. $\mathfrak{M},v\vDash m_{1}=m_{2}$ iff $v(m_{1})=v(m_{2})$
---|---
3\. $\mathfrak{M},v\vDash P_{A}(g_{1})$ iff $v(g_{1})\in P_{A}^{\mathrm{I}}$ |  4\. $\mathfrak{M},v\vDash P_{X}(m_{1})$ iff $v(m_{1})\in P_{X}^{\mathrm{I}}$
5\. $\mathfrak{M},v\vDash g_{1}Im_{1}$ iff $v(g_{1})I^{\mathrm{I}}v(m_{1})$ |  6\. $\mathfrak{M},v\vDash g_{1}R_{\Box}m_{1}$ iff $v(g_{1})R_{\Box}^{\mathrm{I}}v(m_{1})$
7\. $\mathfrak{M},v\vDash m_{1}R_{\Diamond}g_{1}$ iff $v(m_{1})R_{\Diamond}^{\mathrm{I}}v(g_{1})$. |

Any $\mathrm{LE}$-model
$\mathfrak{M}=(A,X,I^{\mathfrak{M}},R^{\mathfrak{M}}_{\Box},R^{\mathfrak{M}}_{\Diamond},V)$
can be seen as an $\mathcal{L}^{1}$-structure (and vice versa), where the
domain of interpretation is formed by sets $A$ and $X$ from the polarity. The
binary predicate symbols $I$, $R_{\Box}$, $R_{\Diamond}$ are interpreted by
the corresponding relations on the polarity, and unary predicate $P_{A}$
(resp. $P_{X}$) is interpreted as the set $[\\![{V(p)}]\\!]$ (resp.
$(\\![{V(p)}]\\!)$), for any $p\in\mathcal{V}$. For any $\mathrm{LE}$-model
$\mathfrak{M}$, we use the same name $\mathfrak{M}$ for the two sorted first-
order structure when they are clearly distinguishable from the context.

##  3 Simulations and Bisimulations on $\mathrm{LE}$-Models

In this section, we generalize simulations and bisimulations from Kripke
models to $\mathrm{LE}$-models and show invariance of $\mathcal{L}$-formulas
under bisimulations. We give an example which shows that the Hennesy-Milner
theorem does not hold with respect to this definition of bisimulation. Hence,
we give a more general definition of bisimilarity which is based on
simulations, and prove Hennesy-Milner theorem for polarity-based semantics of
non-distributive modal logic with respect to this generalized notion of
bisimilarity.

######  Definition 3.1.

Let $\mathfrak{M}_{1}=(\mathfrak{F}_{1},V_{1})$ and
$\mathfrak{M}_{2}=(\mathfrak{F}_{2},V_{2})$ be any $\mathrm{LE}$-models,
$a_{1},x_{1}$ in $\mathfrak{M}_{1}$ and $a_{2},x_{2}$ in $\mathfrak{M}_{1}$,
then

1\. $\mathfrak{M}_{1},a_{1}\rightsquigarrow_{A}\mathfrak{M}_{2},a_{2}$ if for
any $\varphi\in\mathcal{L}$, $\mathfrak{M}_{1},a_{1}\Vdash\varphi$ implies
$\mathfrak{M}_{2},a_{2}\Vdash\varphi$.

2\. $\mathfrak{M}_{1},x_{1}\rightsquigarrow_{X}\mathfrak{M}_{2},x_{2}$ if for
any $\varphi\in\mathcal{L}$, $\mathfrak{M}_{1},x_{1}\succ\varphi$ implies
$\mathfrak{M}_{2},x_{2}\succ\varphi$.

3\.
$\mathfrak{M}_{1},a_{1}\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}_{A}\mathfrak{M}_{2},a_{2}$
if $\mathfrak{M}_{2},a_{2}\rightsquigarrow_{A}\mathfrak{M}_{1},a_{1}$.
$\mathfrak{M}_{1},x_{1}\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}_{X}\mathfrak{M}_{2},x_{2}$
if $\mathfrak{M}_{2},x_{2}\rightsquigarrow_{X}\mathfrak{M}_{1},x_{1}$.

4\. $\mathfrak{M}_{1},a_{1}\leftrightsquigarrow_{A}\mathfrak{M}_{2},a_{2}$ if
$\mathfrak{M}_{1},a_{1}\rightsquigarrow_{A}\mathfrak{M}_{2},a_{2}$ and
$\mathfrak{M}_{1},a_{1}\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}_{A}\mathfrak{M}_{2},a_{2}$.

5\. $\mathfrak{M}_{1},x_{1}\leftrightsquigarrow_{X}\mathfrak{M}_{2},x_{2}$ if
$\mathfrak{M}_{1},x_{1}\rightsquigarrow_{X}\mathfrak{M}_{2},x_{2}$ and
$\mathfrak{M}_{1},x_{1}\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}_{X}\mathfrak{M}_{2},x_{2}$.

For ease of notation, we will use $a_{1}\rightsquigarrow_{A}a_{2}$ instead of
$\mathfrak{M}_{1},a_{1}\rightsquigarrow_{A}\mathfrak{M}_{2},a_{2}$ when
$\mathfrak{M}_{1}$ and $\mathfrak{M}_{2}$ are clear from the context. We use
similar shorthands for the other relations defined in Definition 3.1. The
following definition generalizes simulations and bisimulations on Kripke
models to $\mathrm{LE}$-models.

######  Definition 3.2.

Let $\mathfrak{M}_{1}=(\mathfrak{F}_{1},V_{1})$ and
$\mathfrak{M}_{2}=(\mathfrak{F}_{2},V_{2})$ be any $\mathrm{LE}$-models where
$\mathfrak{F}_{1}=(A_{1},X_{1},I_{1},{R_{\Box}}_{1},{R_{\Diamond}}_{1})$ and
$\mathfrak{F}_{2}=(A_{2},X_{2},I_{2},{R_{\Box}}_{2},{R_{\Diamond}}_{2})$. A
simulation from $\mathfrak{M}_{1}$ to $\mathfrak{M}_{2}$ is a pair of
relations $(S,T)$ such that $S\subseteq A_{1}\times A_{2}$ and $T\subseteq
X_{1}\times X_{2}$ satisfying the following conditions: for any $a_{1}\in
A_{1}$, $x_{1}\in X_{1}$, $a_{2}\in A_{2}$ and $x_{2}\in X_{2}$,

1\. If $a_{1}Sa_{2}$, then $\forall p\in\mathcal{V}$, if
$a_{1}\in[\\![{V_{1}(p)}]\\!]$, then $a_{2}\in[\\![{V_{2}(p)}]\\!]$.

2\. If $x_{1}Tx_{2}$, then $\forall p\in\mathcal{V}$, if
$x_{2}\in(\\![{V_{2}(p)}]\\!)$, then $x_{1}\in(\\![{V_{1}(p)}]\\!)$.

3\. If $a_{1}Sa_{2}$ and $a_{2}I^{c}_{2}x_{2}$, then $\exists x_{1}\in X_{1}$
such that $a_{1}I^{c}_{1}x_{1}$ and $x_{1}Tx_{2}$.

4\. If $x_{1}Tx_{2}$ and $a_{1}I^{c}_{1}x_{1}$, then $\exists a_{2}\in A_{2}$
such that $a_{2}I^{c}_{2}x_{2}$ and $a_{1}Sa_{2}$.

5\. If $a_{1}Sa_{2}$ and $a_{2}R^{c}_{\Box_{2}}x_{2}$, then $\exists x_{1}\in
X_{1}$ such that $a_{1}R^{c}_{\Box_{1}}x_{1}$ and $x_{1}Tx_{2}$.

6\. If $x_{1}Tx_{2}$ and $x_{1}R^{c}_{\Diamond_{1}}a_{1}$, then $\exists
a_{2}\in A_{2}$ such that $x_{2}R^{c}_{\Diamond_{2}}a_{2}$ and $a_{1}Sa_{2}$.

We write $\mathfrak{M}_{1},a_{1}\rightrightarrows\mathfrak{M}_{2},a_{2}$
(resp. $\mathfrak{M}_{1},x_{1}\rightrightarrows\mathfrak{M}_{2},x_{2}$) if
there exists a simulation $(S,T)$ from $\mathfrak{M}_{1}$ to
$\mathfrak{M}_{2}$ such that $a_{1}Sa_{2}$ (resp. $x_{1}Tx_{2}$), and
$\mathfrak{M}_{1},a_{1}\leftleftarrows\mathfrak{M}_{2},a_{2}$ (resp.
$\mathfrak{M}_{1},x_{1}\leftleftarrows\mathfrak{M}_{2},x_{2}$) if
$\mathfrak{M}_{2},a_{2}\rightrightarrows\mathfrak{M}_{1},a_{1}$ (resp.
$\mathfrak{M}_{2},x_{2}\rightrightarrows\mathfrak{M}_{1},x_{1}$). A
bisimulation between $\mathfrak{M}_{1}$ and $\mathfrak{M}_{2}$ is simulation
$(S,T)$ from $\mathfrak{M}_{1}$ to $\mathfrak{M}_{2}$, such that
$(S^{-1},T^{-1})$ is a simulation from $\mathfrak{M}_{2}$ to
$\mathfrak{M}_{1}$.

This definition naturally generalizes sumulations and bisimulations on the
Kripke models in the following sense. In [6, Section 3.3], it was showed that
$\mathrm{LE}$-models can be seen as a generalization of Kripke models by
associating any Kripke model $\mathcal{M}=(W,R,V)$ with an $\mathrm{LE}$-model
$\mathrm{LE}(\mathcal{M})=(W_{A},W_{X},\neq,R_{\Box},R_{\Diamond},V^{\prime})$,
where $W_{A}=W=W_{B}$ and $R_{\Box}=R_{\Diamond}\subseteq W\times W$ such that
$w_{1}R_{\Box}w_{2}$ iff $w_{1}R^{c}w_{2}$ iff $w_{1}R_{\Diamond}w_{2}$, and
for any $p\in\mathcal{V}$, $V^{\prime}(p)=(V(p),V(p)^{c})$. This construction
ensures that for any points in two Kripke models $\mathcal{M}$ and
$\mathcal{M}^{\prime}$ are modally equivalent, their liftings in the
$\mathrm{LE}$-models $\mathrm{LE}(\mathcal{M})$ and
$\mathrm{LE}(\mathcal{M}^{\prime})$ are modally equivalent w.r.t. the language
$\mathcal{L}$. For more details, see [6]. The following lemma shows that any
simulation (resp. bisimulation) on a Kripke model $\mathcal{M}$ naturally
induces a simulation (resp. bisimulation) on $\mathrm{LE}(\mathcal{M})$.

######  Lemma 3.3.

Let $\mathcal{M}_{1}=(W_{1},R_{1},V_{1})$ and
$\mathcal{M}_{2}=(W_{2},R_{2},V_{2})$ be any Kripke models,
$\mathrm{LE}(\mathcal{M}_{1})=(W_{A_{1}},W_{X_{1}},\neq,R_{\Box_{1}},R_{\Diamond_{1}},V_{1}^{\prime})$
and
$\mathrm{LE}(\mathcal{M}_{2})=(W_{A_{2}},W_{X_{2}},\neq,R_{\Box_{2}},R_{\Diamond_{2}},V_{2}^{\prime})$
be their corresponding $\mathrm{LE}$-models. A relation $Z\subseteq
W_{1}\times W_{2}$ between the Kripke models $\mathcal{M}_{1}$ and
$\mathcal{M}_{2}$ is a simulation (resp. bisimulation) iff the tuple
$(Z_{A},Z_{X})$, where $Z_{A}=Z=Z_{X}\subseteq W_{A_{1}}\times
W_{A_{2}}=W_{X_{1}}\times W_{X_{2}}$ is a simulation (resp. bisimulation)
between the $\mathrm{LE}$-models $\mathrm{LE}(\mathcal{M}_{1})$ and
$\mathrm{LE}(\mathcal{M}_{2})$.

######  Proof 3.4.

The proof follows straight-forwardly from the definitions of simulations and
bisimulations on Kripke models and $\mathrm{LE}$-models.

The following theorem shows that the $\mathcal{L}$-formulas are preserved and
reflected by simulations w.r.t. modal satisfaction relations $\Vdash$ and
$\succ$, respectively.

######  Theorem 3.5.

Let $\mathfrak{M}_{1}=(\mathfrak{F}_{1},V_{1})$ and
$\mathfrak{M}_{2}=(\mathfrak{F}_{2},V_{2})$ be any $\mathrm{LE}$-models,
$a_{1},x_{1}$ in $\mathfrak{M}_{1}$ and $a_{2},x_{2}$ in $\mathfrak{M}_{2}$,
then

1\. If $\mathfrak{M}_{1},a_{1}\rightrightarrows\mathfrak{M}_{2},a_{2}$, then
$\mathfrak{M}_{1},a_{1}\rightsquigarrow_{A}\mathfrak{M}_{2},a_{2}$.

2\. If $\mathfrak{M}_{1},x_{1}\rightrightarrows\mathfrak{M}_{2},x_{2}$, then
$\mathfrak{M}_{1},x_{1}\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}_{X}\mathfrak{M}_{2},x_{2}$.

######  Proof 3.6.

See Appendix A.1.

As a corollary, we get that the $\mathcal{L}$-formulas are bisimulation-
invariant.

######  Corollary 3.7.

Let $\mathfrak{M}_{1}=(\mathfrak{F}_{1},V_{1})$ and
$\mathfrak{M}_{2}=(\mathfrak{F}_{2},V_{2})$ be any $\mathrm{LE}$-models, where
$\mathfrak{F}_{1}=(A_{1},X_{1},I_{1},{R_{\Box}}_{1},{R_{\Diamond}}_{1})$ and
$\mathfrak{F}_{2}=(A_{2},X_{2},I_{2},{R_{\Box}}_{2},{R_{\Diamond}}_{2})$, and
$(S,T)$ be a bisimulation between them. Then

1\. For any $a_{1}\in A_{1}$ and $a_{2}\in A_{2}$, $a_{1}Sa_{2}$ implies
$\mathfrak{M}_{1},a_{1}\leftrightsquigarrow_{A}\mathfrak{M}_{2},a_{2}$.

2\. For any $x_{1}\in X_{1}$ and $x_{2}\in X_{2}$, $x_{1}Tx_{2}$ implies
$\mathfrak{M}_{1},x_{1}\leftrightsquigarrow_{X}\mathfrak{M}_{2},x_{2}$.

######  Proof 3.8.

Note that by definition for any bisimulation $(S,T)$, both $(S,T)$ and
$(S^{-1},T^{-1})$ are simulations. The proof follows immediately by Theorem
3.5.

We now try to prove the Hennessy-Milner theorem for the polarity-based
semantics of non-distributive modal logic. We begin by generalizing the notion
of image-finite models from Kripke semantics to polarity-based semantics.

######  Definition 3.9.

An $\mathrm{LE}$-model $\mathfrak{M}=(A,X,I,R_{\Box},R_{\Diamond},V)$ is
image-finite if for any $a\in A$ and $x\in X$, the sets $\\{a^{\prime}\mid
a^{\prime}I^{c}x\\},\\{x^{\prime}\mid aI^{c}x^{\prime}\\},\\{a^{\prime}\mid
a^{\prime}R^{c}_{\Box}x\\}$ and $\\{x^{\prime}\mid
x^{\prime}R^{c}_{\Diamond}a\\}$ are all finite.

Note that a Kripke model $\mathcal{M}$ is image-finite iff
$\mathrm{LE}(\mathcal{M})$ is image-finite. Thus, this definition can be seen
as a generalization of image-finite models to polarity-based setting. However,
as the language of non-distributive modal logic ($\mathcal{L}$) does not
contain negation, the proof strategy for the classical Hennessy-Milner theorem
cannot be adopted in the non-distributive setting. In fact, as the following
example shows, Hennessy-Milner theorem does not hold for the polarity-based
semantics of non-distributive modal logic for the notion of bisimulation given
by Definition 3.2.

######  Example 3.10.

Let
$\mathfrak{M}_{i}=(A_{i},X_{i},I_{i},{R_{\Box}}_{i},{R_{\Diamond}}_{i},V_{i})$
for $i\in\\{1,2\\}$ be two image-finite models such that
$A_{1}=\\{a_{1},b_{1}\\}$, $X_{1}=\\{x_{1},y_{1}\\}$,
$I_{1}=\\{(b_{1},x_{1})\\}$, $A_{2}=\\{a_{2}\\}$, $X_{2}=\\{x_{2}\\}$ and
$I_{2}={R_{\Box}}_{i}={R_{\Diamond}}_{i}=\emptyset$ for $i\in\\{1,2\\}$. Let
$p$, $q$ be any two fixed propositions. Suppose $V_{1}$ and $V_{2}$ are such
that, $V_{1}(q)=(\\{b_{1}\\},\\{x_{1}\\})$, $p\in\mathcal{V}$,
$V_{1}(p)=(\\{a_{1},b_{1}\\},\emptyset)$, $V_{2}(q)=(\emptyset,\\{x_{2}\\})$
and $V_{2}(p)=(\\{a_{2}\\},\emptyset)$. These models are depicted in Figure 1.
It is easy to check that $a_{1}\leftrightsquigarrow_{A}a_{2}$.

Suppose there exists a bisimulation $(S,T)$ between $\mathfrak{M}_{1}$ and
$\mathfrak{M}_{2}$, such that, $a_{1}Sa_{2}$. Then, by item 3 of Definition
3.2 for simulation $(S^{-1},T^{-1})$ and $a_{1}I^{c}_{1}y_{1}$, we must have
$y_{1}Tx_{2}$. However, $\mathfrak{M}_{1},y_{1}\nsucc q$ and
$\mathfrak{M}_{2},x_{2}\succ q$, which contradicts item 2 of Definition 3.2
for simulation $(S,T)$. Hence, there can not be a bisimulation between $a_{1}$
and $a_{2}$.

Figure 1: Models $\mathfrak{M}_{1}$ and $\mathfrak{M}_{2}$ and their complex
algebras

Therefore, to obtain the Hennessy-Milner theorem for polarity-based semantics,
we introduce the notion of bisimilarity, which is founded on the definition of
simulations between $\mathrm{LE}$-models. This notion naturally generalizes
the definition of bisimulation outlined in Definition 3.2.

######  Definition 3.11.

Let $\mathfrak{M}_{1}=(\mathfrak{F}_{1},V_{1})$ and
$\mathfrak{M}_{2}=(\mathfrak{F}_{2},V_{2})$ be any $\mathrm{LE}$-models, where
$\mathfrak{F}_{1}=(A_{1},X_{1},I_{1},{R_{\Box}}_{1},{R_{\Diamond}}_{1})$,
$\mathfrak{F}_{2}=(A_{2},X_{2},I_{2},{R_{\Box}}_{2},{R_{\Diamond}}_{2})$. For
any $a_{1},x_{1}$ in $\mathfrak{M}_{1}$ and $a_{2},x_{2}$ in
$\mathfrak{M}_{2}$, we say that $a_{1}$ and $a_{2}$ (resp. $x_{1}$ and
$x_{2}$) are bisimilar, and denote it by
$\mathfrak{M}_{1},a_{1}\rightleftarrows\mathfrak{M}_{2},a_{2}$ (resp.
$\mathfrak{M}_{1},x_{1}\rightleftarrows\mathfrak{M}_{2},x_{2}$), if both
$\mathfrak{M}_{1},a_{1}\rightrightarrows\mathfrak{M}_{2},a_{2}$ and
$\mathfrak{M}_{1},a_{1}\leftleftarrows\mathfrak{M}_{2},a_{2}$ (resp.
$\mathfrak{M}_{1},x_{1}\rightrightarrows\mathfrak{M}_{2},x_{2}$ and
$\mathfrak{M}_{1},x_{1}\leftleftarrows\mathfrak{M}_{2},x_{2}$).

Henceforth, when we say that two elements are bisimilar, we refer to
Definition 3.11, unless stated otherwise. We now show that even though
Hennessy-Milner theorem for bisimulations does not generalize to the polarity-
based setting, its counterpart for simulations does so.

######  Theorem 3.12 (Hennesy-Milner Theorem).

Let $\mathfrak{M}_{1}=(\mathfrak{F}_{1},V_{1})$ and
$\mathfrak{M}_{2}=(\mathfrak{F}_{2},V_{2})$ be any image-finite
$\mathrm{LE}$-models, $a_{1},x_{1}$ in $\mathfrak{M}_{1}$ and $a_{2},x_{2}$ in
$\mathfrak{M}_{2}$, then

1\. $\mathfrak{M}_{1},a_{1}\rightsquigarrow_{A}\mathfrak{M}_{2},a_{2}$ if and
only if $\mathfrak{M}_{1},a_{1}\rightrightarrows\mathfrak{M}_{2},a_{2}$.

2\. $\mathfrak{M}_{1},x_{1}\rightsquigarrow_{X}\mathfrak{M}_{2},x_{2}$ if and
only if $\mathfrak{M}_{1},x_{1}\leftleftarrows\mathfrak{M}_{2},x_{2}$.

######  Proof 3.13.

The right to left implication for both items follows from Theorem 3.5. We
prove the left to right implication only for the first item, as the proof for
the second is analogous.

For the left to right implication of the first item, we claim that
$(\rightsquigarrow_{A},\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}_{X})$
is a simulation from $\mathfrak{M}_{1}$ to $\mathfrak{M}_{2}$, where
$(a,a^{\prime})\in\rightsquigarrow_{A}$ (denoted as
$a\rightsquigarrow_{A}a^{\prime}$) iff
$\mathfrak{M}_{1},a\rightsquigarrow_{A}\mathfrak{M}_{2},a^{\prime}$ and
$(x,x^{\prime})\in\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}_{X}$
(denoted as
$x\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}_{X}x^{\prime}$)
iff
$\mathfrak{M}_{1},x\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}_{X}\mathfrak{M}_{2},x^{\prime}$.
Assume $a_{1}\rightsquigarrow_{A}a_{2}$ and
$x_{1}\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}_{X}x_{2}$,
the items 1 and 2 of Definition 3.2 are satisfied immediately.

For item 3, assume $a_{1}\rightsquigarrow_{A}a_{2}$ and $a_{2}I^{c}_{2}x_{2}$.
Therefore, $\mathfrak{M}_{2},a_{2}\nVdash\bot$. By definition of
$\rightsquigarrow_{A}$, we have $\mathfrak{M}_{1},a_{1}\nVdash\bot$, which
means that there exists $x_{1}$ such that $a_{1}I^{c}_{1}x_{1}$. Therefore,
the set $Y^{\prime}:=\\{x\mid a_{1}I^{c}_{1}x\\}$ is a non-empty finite (by
image-finiteness) set . Let $Y^{\prime}$ be the set
$\\{x_{1}^{\prime},\cdots,x^{\prime}_{n}\\}$. Assume for any $x\in
Y^{\prime}$, it is not the case that
$x\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}_{X}x_{2}$.
So, there exist finitely many formulas $\psi_{1},\cdots,\psi_{n}$ such that
for each $i$, $\mathfrak{M}_{2},x_{2}\succ\psi_{i}$ and
$\mathfrak{M}_{1},x^{\prime}_{i}\nsucc\psi_{i}$. As $a_{2}I^{c}_{2}x_{2}$,
there is $\mathfrak{M}_{2},a_{2}\nVdash\psi_{1}\vee\cdots\vee\psi_{n}$. On the
other hand, let $x^{\prime}$ be any element in $X_{1}$. Thus,
$\mathfrak{M}_{1},x^{\prime}\succ\psi_{1}\vee\cdots\vee\psi_{n}$ implies
$M_{1},x^{\prime}\succ\psi_{i}$ for each $i$, which means that
$x^{\prime}\notin Y^{\prime}$, so $a_{1}I_{1}x^{\prime}$. Hence, there is
$\mathfrak{M}_{1},a_{1}\Vdash\psi_{1}\vee...\vee\psi_{n}$, which contradicts
$a_{1}\rightsquigarrow_{A}a_{2}$. So, there must exist $x_{1}$ such that
$a_{1}I^{c}_{1}x_{1}$ and
$x_{1}\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}_{X}x_{2}$.

Item 4 can be proved similarly to item 3.

For item 5, assume $a_{1}\rightsquigarrow_{A}a_{2}$ and
$a_{2}R^{c}_{\Box_{2}}x_{2}$. Therefore,
$\mathfrak{M}_{2},a_{2}\nVdash\Box\bot$, which implies
$\mathfrak{M}_{1},a_{1}\nVdash\Box\bot$. Therefore, there exists $x_{1}\in
X_{1}$ such that $a_{1}R^{c}_{\Box_{1}}x_{1}$. Thus, the set
$Y^{\prime}:=\\{x\mid a_{1}R^{c}_{\Box_{1}}x\\}$ is a non-empty finite (by
image-finiteness) set. Let $Y^{\prime}$ be the set
$\\{x^{\prime}_{1},\cdots,x^{\prime}_{n}\\}$. Assume for any $x^{\prime}\in
Y^{\prime}$, it is not the case that
$x^{\prime}\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}_{X}x_{2}$.
Therefore, there exist finitely many formulas $\psi_{1},\cdots,\psi_{n}$ such
that for each $i$, $\mathfrak{M}_{2},x_{2}\succ\psi_{i}$ and
$\mathfrak{M}_{1},x^{\prime}_{i}\nsucc\psi_{i}$. Therefore,
$\mathfrak{M}_{2},x_{2}\succ\psi_{1}\vee\cdots\vee\psi_{n}$, which implies
$\mathfrak{M}_{2},a_{2}\nVdash\Box(\psi_{1}\vee\cdots\vee\psi_{n})$. On the
other hand, let $y^{\prime}$ be any element in $X_{1}$.
$\mathfrak{M}_{1},y^{\prime}\succ\psi_{1}\vee\cdots\vee\psi_{n}$ implies
$\mathfrak{M}_{1},y^{\prime}\Vdash\psi_{i}$ for each $i$, which means
$y^{\prime}\notin Y^{\prime}$, so $a_{1}R_{\Box_{1}}y^{\prime}$. Therefore,
$\mathfrak{M}_{1},a_{1}\Vdash\Box(\psi_{1}\vee\cdots\vee\psi_{n})$, which
contradicts $a_{1}\rightsquigarrow_{A}a_{2}$. So, there must exist $x_{1}$
such that $a_{1}R^{c}_{\Box_{1}}x_{1}$ and
$x_{1}\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}_{X}x_{2}$.

Item 6 can be proved similarly to item 5.

The above theorem can be seen as a generalization of Henessey-Milner theorem
to non-distributive setting as it relates invariance under formulas to
simulations. The following corollary is immediate from the above theorem.

######  Corollary 3.14.

Let $\mathfrak{M}_{1}=(\mathfrak{F}_{1},V_{1})$ and
$\mathfrak{M}_{2}=(\mathfrak{F}_{2},V_{2})$ be any image-finite
$\mathrm{LE}$-models, $a_{1},x_{1}$ in $\mathfrak{M}_{1}$ and $a_{2},x_{2}$ in
$\mathfrak{M}_{2}$, then

1\. $\mathfrak{M}_{1},a_{1}\leftrightsquigarrow_{A}\mathfrak{M}_{2},a_{2}$ if
and only if $\mathfrak{M}_{1},a_{1}\rightleftarrows\mathfrak{M}_{2},a_{2}$.

2\. $\mathfrak{M}_{1},x_{1}\leftrightsquigarrow_{X}\mathfrak{M}_{2},x_{2}$ if
and only if $\mathfrak{M}_{1},x_{1}\rightleftarrows\mathfrak{M}_{2},x_{2}$.

As the simulations on $\mathrm{LE}$-models can be seen as a generalizations of
simulations on Kripke models, the converse of Theorem 3.5 does not always
hold. That is, image-finiteness condition in Theorem 3.12 can not be dropped.

Figure 2: Kripke models $\mathcal{M}$ and $\mathcal{N}$

######  Example 3.15.

Consider two Kripke models $\mathcal{M}$ and $\mathcal{N}$ in Fig 2, where any
$p\in\mathcal{V}$ is false at all the points. It is easy to check that $w$ and
$w^{\prime}$ are modally equivalent in $\mathcal{M}$ and $\mathcal{N}$.
Therefore ${w^{\prime}}_{A}\rightsquigarrow_{A}w_{A}$ on their corresponding
$\mathrm{LE}$-models $\mathrm{LE}(\mathcal{N})$ and
$\mathrm{LE}(\mathcal{M})$. Assume that there exists a simulation $(S,T)$ from
$\mathrm{LE}(\mathcal{N})$ to $\mathrm{LE}(\mathcal{M})$ such that
${w^{\prime}}_{A}Sw_{A}$. Then, $S$ must be a simulation from $\mathcal{N}$ to
$\mathcal{M}$. However, it is not possible to have simulations from
$\mathcal{N}$ to $\mathcal{M}$, so there is a contradiction. Therefore, there
is no simulation from $\mathrm{LE}(\mathcal{N})$ to $\mathrm{LE}(\mathcal{M})$
which can link ${w^{\prime}}_{A}$ and $w_{A}$. This shows that converse of
item 1 in Theorem 3.12 is not true in general. We can similarly show that
converse of item 2 in Theorem 3.12 need not hold in general.

##  4 Modal Saturation via Filter-Ideal Extensions

In this section, we continue to investigate the relation between modal
equivalence and bisimilarity. We first introduce the notion of modally-
saturated ($\mathrm{M}$-saturated) $\mathrm{LE}$-models and the Hennessy-
Milner property. Then, we show that the class of $\mathrm{M}$-saturated
$\mathrm{LE}$-models has the Hennessy-Milner property. After that, we
introduce the notion of filter-ideal extension of $\mathrm{LE}$-models and
show that any points in $\mathrm{LE}$-models are modally equivalent if and
only if they are bisimilar on their filter-ideal extensions.

###  4.1 Modally-saturated $\mathrm{LE}$-models and Hennessy-Milner Property

######  Definition 4.1.

Let $\mathrm{K}$ be a class of $\mathrm{LE}$-models. $\mathrm{K}$ is a
Hennessy-Milner class or has the Hennessy-Milner property if for any
$\mathrm{LE}$-models $\mathfrak{M}_{1},\mathfrak{M}_{2}\in\mathrm{K}$, and
$a_{1}$, $x_{1}$ in $\mathfrak{M}_{1}$, and $a_{2}$, $x_{2}$ in
$\mathfrak{M}_{2}$,

1\. $\mathfrak{M}_{1},a_{1}\rightsquigarrow_{X}\mathfrak{M}_{2},a_{2}$ implies
$\mathfrak{M}_{1},a_{1}\rightrightarrows\mathfrak{M}_{2},a_{2}$, and

2\. $\mathfrak{M}_{1},x_{1}\rightsquigarrow_{A}\mathfrak{M}_{2},x_{2}$ implies
$\mathfrak{M}_{1},x_{1}\leftleftarrows\mathfrak{M}_{2},x_{2}$.

Theorem 3.12 shows that image-finite $\mathrm{LE}$-models have the Hennessy-
Milner property; we now introduce a larger class of models which retains the
property.

######  Definition 4.2.

Let $\mathfrak{M}=(A,X,I,{R_{\Box}},{R_{\Diamond}},V)$ be an
$\mathrm{LE}$-model, $A^{\prime}\subseteq A$ and $X^{\prime}\subseteq X$. Let
$\Sigma$ be a set of $\mathcal{L}$-formulas. $\Sigma$ is satisfiable in
$A^{\prime}$ (resp. $X^{\prime}$) if for any $\varphi\in\Sigma$, there exists
a point $a$ (resp. $x$) such that, $\mathfrak{M},a\Vdash\varphi$ (resp.
$\mathfrak{M},x\succ\varphi$). $\Sigma$ is finitely satisfiable in
$A^{\prime}$ (resp. $X^{\prime}$) if any finite subset of $\Sigma$ is
satisfiable in $A^{\prime}$ (resp. $X^{\prime}$). $\mathfrak{M}$ is modally-
saturated ($\mathrm{M}$-saturated for short) if for any set of formulas
$\Sigma$, $a\in A$ and $x\in X$ the following conditions hold:

1. If $\Sigma$ is finitely satisfiable in $\\{x^{\prime}\mid
aI^{c}x^{\prime}\\}$, then $\Sigma$ is satisfiable in $\\{x^{\prime}\mid
aI^{c}x^{\prime}\\}$.

2. If $\Sigma$ is finitely satisfiable in $\\{a^{\prime}\mid
a^{\prime}I^{c}x\\}$, then $\Sigma$ is satisfiable in $\\{a^{\prime}\mid
a^{\prime}I^{c}x\\}$.

3. If $\Sigma$ is finitely satisfiable in $\\{x^{\prime}\mid
aR^{c}_{\Box}x^{\prime}\\}$, then $\Sigma$ is satisfiable in
$\\{x^{\prime}\mid aR^{c}_{\Box}x^{\prime}\\}$.

4. If $\Sigma$ is finitely satisfiable in $\\{a^{\prime}\mid
xR^{c}_{\Diamond}a^{\prime}\\}$, then $\Sigma$ is satisfiable in
$\\{a^{\prime}\mid xR^{c}_{\Diamond}a^{\prime}\\}$.

######  Theorem 4.3.

The class of $\mathrm{M}$-saturated models has Hennessy-Milner property.

######  Proof 4.4.

See Appendix A.2.

###  4.2 Filter-Ideal Extension of $\mathrm{LE}$-Models

Let $\mathbf{A}=(\mathbf{L},\Box,\Diamond)$ be any $\mathrm{LE}$-algebra (cf.
[10, Definition 1]).
$\mathbf{A}_{+}=(\mathsf{Fi}_{\mathbf{A}},\mathsf{Id}_{\mathbf{A}},I,R_{\Box},R_{\Diamond})$
is the filter-ideal frame of $\mathbf{A}$ (c.f. [10, Definition 29]), where
$\mathsf{Fi}_{\mathbf{A}}$ (resp. $\mathsf{Id}_{\mathbf{A}}$) is the set of
all filters (resp. ideals) of $\mathbf{L}$ such that for any
$F\in\mathsf{Fi}_{\mathbf{A}}$ and $J\in\mathsf{Id}_{\mathbf{A}}$,

1\. $FIJ$ if and only if $F\cap J\neq\emptyset$.

2\. $FR_{\Box}J$ if and only if there exists $a\in J$ such that $\Box a\in F$.

3\. $JR_{\Diamond}F$ if and only if there exists $a\in F$ such that $\Diamond
a\in J$.

######  Definition 4.5.

Let $\mathfrak{M}=(\mathfrak{F},V)$ be any $\mathrm{LE}$-model with
$\mathfrak{F}=(A,X,I,R_{\Box},R_{\Diamond})$. The filter-ideal extension of
$\mathfrak{M}$ is the tuple
$\mathfrak{M}^{\mathsf{FI}}=(\mathfrak{F}^{\mathsf{FI}},V^{\mathsf{FI}})$,
where $\mathfrak{F}^{\mathsf{FI}}=(\mathfrak{F}^{+})_{+}$ and for any
$p\in\mathcal{V}$,
$V^{\mathsf{FI}}(p)=([\\![{V^{\mathsf{FI}}(p)}]\\!],(\\![{V^{\mathsf{FI}}(p)}]\\!))=(\\{F\mid([\\![{p}]\\!],(\\![{p}]\\!))\in
F\\},\\{J\mid([\\![{p}]\\!],(\\![{p}]\\!))\in J\\})$.

######  Remark 4.6.

In order to check that $\mathfrak{M}^{\mathsf{FI}}$ is well defined we need to
check that for any $p\in\mathcal{V}$,
$([\\![{V^{\mathsf{FI}}(p)}]\\!],(\\![{V^{\mathsf{FI}}(p)}]\\!))$ indeed forms
a concept of $\mathfrak{F}$. We only prove
$[\\![{V^{\mathsf{FI}}(p)}]\\!]^{\uparrow}=(\\![{V^{\mathsf{FI}}(p)}]\\!)$
here. The proof for
$(\\![{V^{\mathsf{FI}}(p)}]\\!)^{\downarrow}=[\\![{V^{\mathsf{FI}}(p)}]\\!]$
is similar. The right to left inclusion is trivial. As for inclusion in other
direction, suppose there exists
$J\in[\\![{V^{\mathsf{FI}}(p)}]\\!]^{\uparrow}$ and
$J\not\in(\\![{V^{\mathsf{FI}}(p)}]\\!)$. Thus,
$([\\![{p}]\\!],(\\![{p}]\\!))\not\in J$ and for any filter $F$ which contains
$([\\![{p}]\\!],(\\![{p}]\\!))$, $F\cap J\neq\emptyset$. As
$([\\![{p}]\\!],(\\![{p}]\\!))\not\in J$, by the filter-ideal theorem, there
exists a filter $F^{\prime}$ such that $([\\![{p}]\\!],(\\![{p}]\\!))\in
F^{\prime}$ and $F^{\prime}\cap J=\emptyset$. This contradicts our assumption.
So, the left to right inclusion holds.

The following lemma shows that the filter-ideal extensions of
$\mathrm{LE}$-models preserve modal satisfaction.

######  Lemma 4.7.

Let $\mathfrak{M}=(\mathfrak{F},V)$ be any $\mathrm{LE}$-model where
$\mathfrak{F}=(A,X,I,R_{\Box},R_{\Diamond})$, and
$\mathfrak{M}^{\mathsf{FI}}=(\mathfrak{F}^{\mathsf{FI}},V^{\mathsf{FI}})$ is
the filter-ideal extension of $\mathfrak{M}$. Let $F$ be a filter of
$\mathfrak{F}^{+}$ and $J$ be an ideal of $\mathfrak{F}^{+}$. Then

$\mathfrak{M}^{\mathsf{FI}},F\Vdash\varphi$ iff
$([\\![{\varphi}]\\!],(\\![{\varphi}]\\!))\in F$ and
$\mathfrak{M}^{\mathsf{FI}},J\succ\varphi$ iff
$([\\![{\varphi}]\\!],(\\![{\varphi}]\\!))\in J$.

######  Proof 4.8.

It is straight-forward by induction on the complexity of formulas.

For any $\mathrm{LE}$-frame $\mathfrak{F}$ and
$\mathrm{K}\subseteq\mathfrak{F}^{+}$, let $\mathsf{Fi}(\mathrm{K})$ (resp.
$\mathsf{Id}(\mathrm{K})$) denote the filter (resp. the ideal) generated by
$\mathrm{K}$. When $\mathrm{K}=\\{k\\}\subseteq\mathfrak{F}^{+}$, let
$\mathsf{Fi}(k)$ (resp. $\mathsf{Id}(k)$) denote the principal filter (resp.
principal ideal) $\mathsf{Fi}(\\{k\\})$ (resp. $\mathsf{Id}(\\{k\\})$).

######  Corollary 4.9 (truth lemma).

Let $\mathfrak{M}=(\mathfrak{F},V)$ be any $\mathrm{LE}$-model where
$\mathfrak{F}=(A,X,I,R_{\Box},R_{\Diamond})$, and $\mathfrak{M}^{\mathsf{FI}}$
be the filter-ideal extension of $\mathfrak{M}$. For all
$\varphi\in\mathcal{L}$,

1\. For any $a\in A$, $\mathfrak{M},a\Vdash\varphi$ if and only if
$\mathfrak{M}^{\mathsf{FI}},\mathsf{Fi}(\mathbf{a})\Vdash\varphi$.

2\. For any $x\in X$, $\mathfrak{M},x\succ\varphi$ if and only if
$\mathfrak{M}^{\mathsf{FI}},\mathsf{Id}(\mathbf{x})\succ\varphi$.

######  Proof 4.10.

$\mathfrak{M},a\Vdash\varphi$ | $\Leftrightarrow$ | $\mathbf{a}\leq([\\![{\varphi}]\\!],(\\![{\varphi}]\\!))$ |  | $\mathfrak{M},x\succ\varphi$ | $\Leftrightarrow$ | $([\\![{\varphi}]\\!],(\\![{\varphi}]\\!))\leq\mathbf{x}$
---|---|---|---|---|---|---
| $\Leftrightarrow$ | $([\\![{\varphi}]\\!],(\\![{\varphi}]\\!))\in\mathsf{Fi}(\mathbf{a})$ |  |  | $\Leftrightarrow$ | $([\\![{\varphi}]\\!],(\\![{\varphi}]\\!))\in\mathsf{Id}(\mathbf{x})$
| $\Leftrightarrow$ | $\mathfrak{M}^{\mathsf{FI}},\mathsf{Fi}(\mathbf{a})\Vdash\varphi$ |  |  | $\Leftrightarrow$ | $\mathfrak{M}^{\mathsf{FI}},\mathsf{Id}(\mathbf{x})\succ\varphi$

The first equivalences follow from the relationship between $\Vdash$ and
$\succ$ on a polarity-based model and order $\leq$ on its complex algebra. The
second equivalence follows from the definitions of $\mathsf{Fi}(\mathbf{a})$
and $\mathsf{Id}(\mathbf{x})$, and the third equivalence follows from Lemma
4.7.

The above lemma implies that for any $\mathrm{LE}$-model $\mathfrak{M}$ with
filter-ideal extension $\mathfrak{M}^{\mathsf{FI}}$, for any $a\in A$, and
$x\in X$, $a\leftrightsquigarrow_{A}\mathsf{Fi}(\mathbf{a})$ and
$x\leftrightsquigarrow_{X}\mathsf{Id}(\mathbf{x})$.

######  Lemma 4.11.

The filter-ideal extension of an $\mathrm{LE}$-model is
$\mathrm{M}$-saturated.

######  Proof 4.12.

See Appendix A.3.

This lemma gives us the following theorem and corollary immediately, saying
filter-ideal extensions $\mathrm{LE}$-models have the Hennessy-Milner
property.

######  Theorem 4.13.

For all $\mathrm{LE}$-models $\mathfrak{M}_{1}$ and $\mathfrak{M}_{2}$,
$a_{1},x_{1}$ in $\mathfrak{M}_{1}$, and $a_{2},x_{2}$ in $\mathfrak{M}_{2}$,

1\. $\mathfrak{M}_{1},a_{1}\rightsquigarrow_{A}\mathfrak{M}_{2},a_{2}$ if and
only if
$\mathfrak{M}^{\mathsf{Fi}}_{1},\mathsf{Fi}(\mathbf{a_{1}})\rightrightarrows\mathfrak{M}^{\mathsf{Fi}}_{2},\mathsf{Fi}(\mathbf{a_{2}})$.

2\. $\mathfrak{M}_{1},x_{1}\rightsquigarrow_{X}\mathfrak{M}_{2},x_{2}$ if and
only if
$\mathfrak{M}^{\mathsf{Id}}_{1},\mathsf{Id}(\mathbf{x_{1}})\leftleftarrows\mathfrak{M}^{\mathsf{Id}}_{2},\mathsf{Id}(\mathbf{x_{2}})$.

######  Proof 4.14.

Immediate by Corollary 4.9, Lemma 4.11, and Theorem 4.3.

######  Corollary 4.15.

For all $\mathrm{LE}$-models $\mathfrak{M}_{1}$ and $\mathfrak{M}_{2}$, any
$a_{1},x_{1}$ in $\mathfrak{M}_{1}$ and any $a_{2},x_{2}$ in
$\mathfrak{M}_{2}$,

1\. $\mathfrak{M}_{1},a_{1}\leftrightsquigarrow_{A}\mathfrak{M}_{2},a_{2}$ if
and only if
$\mathfrak{M}^{\mathsf{Fi}}_{1},\mathsf{Fi}(\mathbf{a_{1}})\rightleftarrows\mathfrak{M}^{\mathsf{Fi}}_{2},\mathsf{Fi}(\mathbf{a_{2}})$.

2\. $\mathfrak{M}_{1},x_{1}\leftrightsquigarrow_{X}\mathfrak{M}_{2},x_{2}$ if
and only if
$\mathfrak{M}^{\mathsf{Id}}_{1},\mathsf{Id}(\mathbf{x_{1}})\rightleftarrows\mathfrak{M}^{\mathsf{Id}}_{2},\mathsf{Id}(\mathbf{x_{2}})$.

##  5 Toward van Benthem Characterization Theorem

In this section, we firstly introduce the standard translation for non-
distributive modal logic based on polarity-based semantics, and then define
the ultrapower extension for $\mathrm{LE}$-models. Following that, we
introduce $\omega$-saturated $\mathrm{LE}$-models and show that
$\omega$-saturated $\mathrm{LE}$-models are $\mathrm{M}$-saturated. Finally,
we show that for any $\mathrm{LE}$-model, there exists an ultrapower extension
of it which is $\omega$-saturated. We use this result to prove the van Benthem
characterization theorem of non-distributive modal logic.

###  5.1 Standard Translation

The following definition of standard translation for non-distributive modal
logic on polarity-based semantics is inspired from [8, Section 2.1].

######  Definition 5.1.

Let $g\in G$ and $m\in M$ be two $\mathcal{L}_{1}$-variables and
$\varphi\in\mathcal{L}$ (cf. Section 2.3). The standard translations
$ST_{g}:\mathcal{L}\rightarrow\mathcal{L}^{1}$ and
$ST_{m}:\mathcal{L}\rightarrow\mathcal{L}^{1}$ are defined as follows:

$ST_{g}(\bot):=\forall m(gIm)$ |  | $ST_{m}(\bot):=m=m$
---|---|---
$ST_{g}(\top):=g=g$ |  | $ST_{m}(\bot):=\forall g(gIm)$
$ST_{g}(p):=P_{A}(g)$ |  | $ST_{m}(p):=P_{X}(m)$
$ST_{g}(\varphi\vee\psi):=\forall m(ST_{m}(\varphi)\wedge ST_{m}(\psi)\rightarrow gIm)$ |  | $ST_{m}(\varphi\vee\psi):=ST_{m}(\varphi)\wedge ST_{m}(\psi)$
$ST_{g}(\varphi\wedge\psi):=ST_{g}(\varphi)\wedge ST_{g}(\psi)$ |  | $ST_{m}(\varphi\wedge\psi):=\forall g(ST_{g}(\varphi)\wedge ST_{g}(\psi)\rightarrow gIm)$
$ST_{g}(\Diamond\varphi):=\forall m(ST_{m}(\Diamond\varphi)\rightarrow gIm)$ |  | $ST_{m}(\Diamond\varphi):=\forall g(ST_{g}(\varphi)\rightarrow mR_{\Diamond}g)$
$ST_{g}(\Box\varphi):=\forall m(ST_{m}(\varphi)\rightarrow gR_{\Box}m)$ |  | $ST_{m}(\Box\varphi):=\forall g(ST_{g}(\Box\varphi)\rightarrow gIm)$

The following lemma is immediate from the definition above.

######  Lemma 5.2.

Let $\mathfrak{M}=(A,X,I,R_{\Box},R_{\Diamond},V)$ be an $\mathrm{LE}$-model,
then for any $a\in A$ and $x\in X$, and any $\mathcal{L}_{1}$-variables $g\in
G$ and $m\in M$:

1\. $\mathfrak{M},a\Vdash\varphi$ iff $\mathfrak{M}\vDash ST_{g}(\varphi)[a]$
and $\mathfrak{M},x\succ\varphi$ iff $\mathfrak{M}\vDash ST_{m}(\varphi)[x]$.

2\. $\mathfrak{M},a\Vdash\varphi$ iff $\mathfrak{M}\vDash\forall
gST_{g}(\varphi)$ and $\mathfrak{M},x\succ\varphi$ iff
$\mathfrak{M}\vDash\forall mST_{m}(\varphi)$.

######  Proof 5.3.

It is straight-forward by induction on the complexity of formulas.

###  5.2 Ultrapower Extension and $\omega$-Saturated Model

######  Definition 5.4.

Let $\mathrm{K}$ be a non-empty index set, and $\mathfrak{M}=(\mathfrak{F},V)$
be an $\mathrm{LE}$-model, where $\mathfrak{F}=(A,X,I,R_{\Box},R_{\Diamond})$
and for any $p\in\mathcal{V}$, $V(p)=([\\![{p}]\\!],(\\![{p}]\\!))$. The
$\mathrm{K}$-power of $\mathfrak{M}$ is the $\mathrm{LE}$-model
$\mathfrak{M}^{\mathrm{K}}=(A^{\mathrm{K}},X^{\mathrm{K}},I^{\mathrm{K}},R^{\mathrm{K}}_{\Box},R^{\mathrm{K}}_{\Diamond},V^{\mathrm{K}})$,
where

1\. $A^{\mathrm{K}}$ is the set of functions $s:\mathrm{K}\rightarrow A$.

2\. $X^{\mathrm{K}}$ is the set of functions from $t:\mathrm{K}\rightarrow X$.

3\. For any $s\in A^{\mathrm{K}}$ and $t\in X^{\mathrm{K}}$,
$sI^{\mathrm{K}}t$ iff for any $k\in\mathrm{K}$, $s(k)It(k)$.

4\. For any $s\in A^{\mathrm{K}}$ and $t\in X^{\mathrm{K}}$,
$sR^{\mathrm{K}}_{\Box}t$ iff for any $k\in\mathrm{K}$, $s(k)R_{\Box}t(k)$.

5\. For any $s\in A^{\mathrm{K}}$ and $t\in X^{\mathrm{K}}$,
$tR^{\mathrm{K}}_{\Diamond}s$ iff for any $k\in\mathrm{K}$,
$t(k)R_{\Diamond}s(k)$.

6\. For any
$p\in\mathcal{V},V^{\mathrm{K}}(p)=([\\![{p}]\\!]^{\mathrm{K}},(\\![{p}]\\!)^{\mathrm{K}})$
such that $s\in[\\![{p}]\\!]^{\mathrm{K}}$ iff for any $k\in\mathrm{K}$,
$s(k)\in[\\![{p}]\\!]$, and $t\in(\\![{p}]\\!)^{\mathrm{K}}$ iff for any
$k\in\mathrm{K}$, $t(k)\in(\\![{p}]\\!)$.

Let $\mathcal{U}\subseteq\mathcal{P}(\mathrm{K})$ be an ultrafilter over
$\mathrm{K}$. We define equivalence relations $\sim_{A}$ and $\sim_{X}$ on
$A^{\mathrm{K}}$ and $X^{\mathrm{K}}$, respectively, as follows:

1\. $s_{1}\sim_{A}s_{2}$ if and only if $\\{k\in\mathrm{K}\mid
s_{1}(k)=s_{2}(k)\\}\in\mathcal{U}$.

2\. $t_{1}\sim_{X}t_{2}$ if and only if $\\{k\in\mathrm{K}\mid
t_{1}(k)=t_{2}(k)\\}\in\mathcal{U}$.

The ultrapower of $\mathfrak{M}$ modulo $\mathrm{K}$ and $\mathcal{U}$ is a
structure
$\mathfrak{M}^{\mathrm{K}}_{\mathcal{U}}=(A^{\mathrm{K}}_{\mathcal{U}},X^{\mathrm{K}}_{\mathcal{U}},I^{\mathrm{K}}_{\mathcal{U}},{R^{\mathrm{K}}_{\Box}}_{\mathcal{U}},{R^{\mathrm{K}}_{\Diamond}}_{\mathcal{U}},V^{\mathrm{K}}_{\mathcal{U}})$,
where $A^{\mathrm{K}}_{\mathcal{U}}$ (resp. $X^{\mathrm{K}}_{\mathcal{U}}$) is
quotient of $A^{\mathrm{K}}$ (resp. $X^{\mathrm{K}}$) over $\sim_{A}$ (resp.
$\sim_{X}$), and for any $[s]\in A^{\mathrm{K}}_{\mathcal{U}}$, $[t]\in
X^{\mathrm{K}}_{\mathcal{U}}$,

1\. $[s]I^{\mathrm{K}}_{\mathcal{U}}[t]$ if and only if $\\{k\in\mathrm{K}\mid
s(k)It(k)\\}\in\mathcal{U}$.

2\. $[s]{R^{\mathrm{K}}_{\Box}}_{\mathcal{U}}[t]$ if and only if
$\\{k\in\mathrm{K}\mid s(k)R_{\Box}t(k)\\}\in\mathcal{U}$.

3\. $[t]{R^{\mathrm{K}}_{\Diamond}}_{\mathcal{U}}[s]$ if and only if
$\\{k\in\mathrm{K}\mid t(k){R_{\Diamond}}s(k)\\}\in\mathcal{U}$.

4\. For any $p\in\mathcal{V}$,
$V^{\mathrm{K}}_{\mathcal{U}}(p)=([\\![{p}]\\!]^{\mathrm{K}}_{\mathcal{U}},(\\![{p}]\\!)^{\mathrm{K}}_{\mathcal{U}})$,
where $[s]\in[\\![{p}]\\!]^{\mathrm{K}}_{\mathcal{U}}$ if and only if
$\\{k\in\mathrm{K}\mid s(k)\in[\\![{p}]\\!]\\}\in\mathcal{U}$, and
$[t]\in(\\![{p}]\\!)^{\mathrm{K}}_{\mathcal{U}}$ if and only if
$\\{k\in\mathrm{K}\mid t(k)\in(\\![{p}]\\!)\in\mathcal{U}\\}$.

The following theorem is an immediate consequence of Łós’s Theorem for first-
order logic.

######  Theorem 5.5 (Łós’s Theorem).

Let $\mathrm{K}$ be a non-empty index set and $\mathcal{U}$ be an ultrafilter
over $\mathrm{K}$. Let $\mathfrak{M}$ be an $\mathrm{LE}$-model and
$\mathfrak{M}^{\mathrm{K}}_{\mathcal{U}}$ be its ultrapower modulo
$\mathrm{K}$ and $\mathcal{U}$. For any two-sorted first-order formula
$\varphi\in\mathcal{L}^{1}$ (cf. Section 2.3),

$\mathfrak{M}^{\mathrm{K}}_{\mathcal{U}}\vDash\varphi[s,t]$ if and only if
$\\{k\in\mathrm{K}\mid\mathfrak{M}\vDash\varphi[s(k),t(k)]\\}\in\mathcal{U}$.

######  Remark 5.6.

Any ultrapower $\mathfrak{M}^{\mathrm{K}}_{\mathcal{U}}$ of an
$\mathrm{LE}$-model $\mathfrak{M}$ is indeed an $\mathrm{LE}$-model. In order
to see this, we just need to check that relations
${R^{\mathrm{K}}_{\Box}}_{\mathcal{U}}$ and
${R^{\mathrm{K}}_{\Diamond}}_{\mathcal{U}}$ are $I$-compatible, and for any
$p\in\mathcal{V}$, $[\\![{p}]\\!]^{\mathrm{K}}_{\mathcal{U}}$ and
$(\\![{p}]\\!)^{\mathrm{K}}_{\mathcal{U}}$ are Galois stable. This is true
because all these conditions are first-order definable, and so they will be
preserved in the ultrapower extension by Łós’s Theorem.

We now define $\kappa$-saturated first-order models for any infinite cardinal
$\kappa$.

######  Definition 5.7.

Let $\kappa$ be an infinite cardinal, and $\mathfrak{M}$ be an
$\mathrm{LE}$-model. For any set $S$ of elements appearing in $\mathfrak{M}$,
let $\mathcal{L}^{1}_{S}$ be the extension of $\mathcal{L}^{1}$ with constant
symbols for every element of $S$. $\mathfrak{M}$ is $\kappa$-saturated if for
any set of elements $S$ appearing in $\mathfrak{M}$ with $|S|<\kappa$, and any
set $\Sigma$ of $\mathcal{L}^{1}_{S}$ formulas with finite many free
variables, if $\Sigma$ is finitely satisfiable in $\mathfrak{M}$, then
$\Sigma$ is satisfiable in $\mathfrak{M}$.

The following theorem follows from [5, Theorem 6.1.8].

######  Theorem 5.8.

For any $\mathrm{LE}$-model $\mathfrak{M}$, there exist an non-empty index set
$\mathrm{K}$ and an ultrafilter $\mathcal{U}$ over $\mathrm{K}$ such that
$\mathfrak{M}^{\mathrm{K}}_{\mathcal{U}}$ is $\omega$-saturated.

######  Proposition 5.9.

Any $\omega$-saturated $\mathrm{LE}$-model is $\mathrm{M}$-saturated.

######  Proof 5.10.

Let $\mathfrak{M}=(\mathfrak{F},V)$ be an $\omega$-saturated
$\mathrm{LE}$-model, where $\mathfrak{F}=(A,X,I,R_{\Box},R_{\Diamond})$. We
only prove the fist item of Definition 4.2, and other conditions can be proved
similarly. Let $\Sigma$ be a set of $\mathcal{L}$-formulas which are finitely
satisfiable in set $\\{x^{\prime}\mid aI^{c}x^{\prime}\\}$. Define
$\Sigma^{\prime}$ to be the set

$\Sigma^{\prime}=\\{aI^{c}x\\}\cup ST_{x}(\Sigma)$.

Clearly $\Sigma^{\prime}$ contains only finite many free variables (only $x$)
and every finite subset of $\Sigma^{\prime}$ is satisfiable in
$(\mathfrak{M},x)_{x\in X}$. Hence, by $\omega$-saturation $\Sigma^{\prime}$
is satisfiable in $(\mathfrak{M},x)_{x\in X}$ at some $x_{0}$ with
$aI^{c}x_{0}$ . Then, by Lemma 5.2 we have $\mathfrak{M},x_{0}\succ\Sigma$.
Therefore, $\Sigma$ is satisfiable in $\\{x^{\prime}\mid aI^{c}x^{\prime}\\}$.

It follows immediately from the above proposition and Theorem 4.3 that the
class of $\omega$-saturated LE-models satisfy Hennessy-Milner property.

###  5.3 The van Benthem Characterization Theorem

We are now ready to prove the van Benthem characterization theorem for non-
distributive modal logic based on the polarity-based semantics, which follows
from the detour lemma below.

######  Theorem 5.11 (Detour Lemma).

For all $\mathrm{LE}$-models $\mathfrak{M}_{1}$ and $\mathfrak{M}_{2}$, any
$a_{1},x_{1}$ in $\mathfrak{M}_{1}$ and $a_{2},x_{2}$ in $\mathfrak{M}_{2}$,

1\. $\mathfrak{M}_{1},a_{1}\rightsquigarrow_{A}\mathfrak{M}_{2},a_{2}$ if and
only if there exist two $\omega$-saturated $\mathrm{LE}$-models
$\mathfrak{M}^{\omega}_{1}$ and $\mathfrak{M}^{\omega}_{2}$, and two
elementary embeddings
$\omega_{1}:\mathfrak{M}_{1}\rightarrow\mathfrak{M}^{\omega}_{1}$ and
$\omega_{2}:\mathfrak{M}_{2}\rightarrow\mathfrak{M}^{\omega}_{2}$, such that
$\mathfrak{M}^{\omega}_{1},\omega_{1}(a_{1})\rightrightarrows\mathfrak{M}^{\omega}_{2},\omega_{2}(a_{2})$.

2\. $\mathfrak{M}_{1},x_{1}\rightsquigarrow_{X}\mathfrak{M}_{2},x_{2}$ if and
only if there exist two $\omega$-saturated $\mathrm{LE}$-models
$\mathfrak{M}^{\omega}_{1}$ and $\mathfrak{M}^{\omega}_{2}$, and two
elementary embeddings
$\omega_{1}:\mathfrak{M}_{1}\rightarrow\mathfrak{M}^{\omega}_{1}$ and
$\omega_{2}:\mathfrak{M}_{2}\rightarrow\mathfrak{M}^{\omega}_{2}$, such that
$\mathfrak{M}^{\omega}_{1},\omega_{1}(x_{1})\leftleftarrows\mathfrak{M}^{\omega}_{2},\omega_{2}(x_{2})$.

Figure 3: Detour Lemma

######  Proof 5.12.

We only prove the item 1 here, the proof of the item 2 is similar. The
implication from right to left proved by contradiction. Suppose
$\mathfrak{M}^{\omega}_{1},\omega_{1}(a_{1})\rightrightarrows\mathfrak{M}^{\omega}_{2},\omega_{2}(a_{2})$,
and $\omega_{1}:\mathfrak{M}_{1}\rightarrow\mathfrak{M}^{\omega}_{1}$,
$\omega_{2}:\mathfrak{M}_{2}\rightarrow\mathfrak{M}^{\omega}_{2}$ are two
elementary embeddings. Suppose there exists $\varphi\in\mathcal{L}$, such that
$\mathfrak{M},a_{1}\Vdash\varphi$, and $\mathfrak{M},a_{2}\nVdash\varphi$.
Therefore, by Lemma 5.2, $\mathfrak{M}_{1}\vDash ST_{g}(\varphi)[a_{1}]$ and
$\mathfrak{M}_{2}\nVdash ST_{g}(\varphi)[a_{2}]$, which implies that
$\mathfrak{M}^{\omega}_{1}\vDash ST_{g}(\varphi)[\omega_{1}(a_{1})]$ and
$\mathfrak{M}^{\omega}_{2}\nvDash ST_{g}(\varphi)[\omega_{2}(a_{2})]$.
Therefore, by Lemma 5.2 again,
$\mathfrak{M}^{\omega}_{1},\omega_{1}(a_{1})\Vdash\varphi$ and
$\mathfrak{M}^{\omega}_{2},\omega_{2}(a_{2})\nVdash\varphi$. However, this
contradicts
$\mathfrak{M}^{\omega}_{1},\omega_{1}(a_{1})\rightrightarrows\mathfrak{M}^{\omega}_{2},\omega_{2}(a_{2})$
due to Theorem 3.12. Hence proved.

For the implication from left to right, assume that
$\mathfrak{M}_{1},a_{1}\rightsquigarrow_{A}\mathfrak{M}_{2},a_{2}$. We
consider their respective ultrapower extensions
${\mathfrak{M}^{\mathrm{K}}_{1}}_{\mathcal{U}}$,
${\mathfrak{M}^{\mathrm{K}}_{2}}_{\mathcal{U}}$, and natural elementary
embeddings
$\omega_{i}:\mathfrak{M}_{i}\rightarrow{\mathfrak{M}^{\mathrm{K}}_{i}}_{\mathcal{U}}$
where $i\in\\{1,2\\}$ such that for any $a_{i}\in A_{i}$,
$\omega_{i}(a_{i})=[s^{i}_{a_{i}}]$, where
$s^{i}_{a_{i}}:\mathrm{K}\rightarrow A_{i}$ are the constant functions which
send all elements in $\mathrm{K}$ to $a_{i}$. Therefore,
${\mathfrak{M}^{\mathrm{K}}_{1}}_{\mathcal{U}},\omega_{1}(a_{1})\rightsquigarrow_{A}{\mathfrak{M}^{\mathrm{K}}_{2}}_{\mathcal{U}},\omega_{2}(a_{2})$.
By Theorem 5.8, ${\mathfrak{M}^{\mathrm{K}}_{1}}_{\mathcal{U}}$ and
${\mathfrak{M}^{\mathrm{K}}_{2}}_{\mathcal{U}}$ are $\omega$-saturated
$\mathrm{LE}$-models. Therefore, by Proposition 5.9 and Theorem 4.3,
${\mathfrak{M}^{\mathrm{K}}_{1}}_{\mathcal{U}},\omega_{1}(a_{1})\rightrightarrows{\mathfrak{M}^{\mathrm{K}}_{2}}_{\mathcal{U}},\omega_{2}(a_{2})$.

######  Theorem 5.13 (van Benthem Characterization Theorem).

Let $\varphi(g)$ (resp. $\varphi(m)$) be any two sorted first-order formula in
$\mathcal{L}^{1}$, then $\varphi(g)$ (resp. $\varphi(m)$) is preserved (resp.
reflected) by simulation if and only if there exist finite many
$\mathcal{L}$-formulas $\psi_{1}$, $\psi_{2}$, $\cdots$, $\psi_{n}$ such that
$\varphi(g)$ (resp. $\varphi(m)$) is equivalent to $\bigvee_{1\leq i\leq
n}ST_{g}(\psi_{i})$ (resp. $\bigvee_{1\leq i\leq n}ST_{m}(\psi_{i})$).

######  Proof 5.14.

We only provide the proof for $\varphi(g)$, the the proof for $\varphi(m)$ is
similar. The implication from right to left follows from Theorem 3.5. For the
implication from left to right, assume that $\varphi(g)$ is preserved by
simulation. We define a set of two sorted first-order formulas
$\mathrm{JMOC}(\varphi):=\\{\bigvee_{1\leq i\leq
n}ST_{g}(\psi_{i})\mid\psi_{i}\in\mathcal{L},n\in\omega,\varphi(g)\vDash\bigvee_{1\leq
i\leq n}ST_{g}(\psi_{i})\\}$. We first check that the following is true: if
$\mathrm{JMOC}(\varphi)\vDash\varphi(g)$, then $\varphi(g)$ is equivalent to
$\bigvee_{j}ST_{g}(\psi_{j})$ for some finite set of $\mathcal{L}$-formulas
$\\{\psi_{j}\mid j\in\mathcal{J}\\}$. Assume that
$\mathrm{JMOC}(\varphi)\vDash\varphi(g)$. By compactness, there exists an
finite set $\\{\bigvee_{1\leq i\leq n}ST_{g}(\psi_{j,i})\mid
j\in\mathcal{J},n\in\omega\\}\subseteq\mathrm{JMOC}(\varphi)$ such that
$\vDash\bigwedge_{j\in\mathcal{J}}\bigvee_{1\leq i\leq
n}ST_{g}(\psi_{j,i})\rightarrow\varphi(g)$. Therefore, we have
$\vDash\varphi(g)\leftrightarrow\bigwedge_{j\in\mathcal{J}}\bigvee_{1\leq
i\leq n}ST_{g}(\psi_{j,i})$. Note that
$\bigwedge_{j\in\mathcal{J}}\bigvee_{1\leq i\leq n}ST_{g}(\psi_{j,i})$ is
equivalent to $\bigvee_{1\leq i\leq
n}\bigwedge_{j\in\mathcal{J}}ST_{g}(\psi_{j,i})$, and the latter is equivalent
to $\bigvee_{1\leq i\leq n}ST_{g}(\bigwedge_{j\in\mathcal{J}}\psi_{j,i})$.

Therefore, it suffices to show that $\mathrm{JMOC}(\varphi)\vDash\varphi(g)$.
Let $\mathfrak{M}$ be an $\mathrm{LE}$-model such that
$\mathfrak{M}\vDash\mathrm{JMOC}(\varphi)[a]$. Let $\mathrm{NT}(g):=\\{\neg
ST_{g}(\psi)\mid\psi\in\mathcal{L},\mathfrak{M}\nvDash ST_{g}(\psi)[a]\\}$. We
want to show that $\mathrm{NT}(g)\cup\\{\varphi(g)\\}$ is consistent. Suppose
not. Then, by compactness there exists a finite subset
$\mathrm{NT}_{0}(g)=\\{\neg ST_{g}(\psi_{k})\mid k\in\mathcal{K}\\}$ of
$\mathrm{NT}(g)$ such that $\mathrm{NT}_{0}(g)\cup\\{\varphi(g)\\}$ is
inconsistent. Therefore,
$\varphi(g)\rightarrow\neg\bigwedge_{k\in\mathcal{K}}\neg ST_{g}(\psi_{i})$ is
valid, which means that
$\varphi(g)\rightarrow\bigvee_{k\in\mathcal{K}}ST_{g}(\psi_{i})$ is valid.
Therefore,
$\bigvee_{k\in\mathcal{K}}ST_{g}(\psi_{i})\in\mathrm{JMOC}(\varphi)$, which
implies $\mathfrak{M}\vDash\bigvee_{k\in\mathcal{K}}ST_{g}(\psi_{i})[a]$.
However, $\mathfrak{M}\nvDash ST_{g}(\psi_{i})[a]$ for any $k\in\mathcal{K}$,
which implies
$\mathfrak{M}\nvDash\bigvee_{k\in\mathcal{K}}ST_{g}(\psi_{i})[a]$, so there is
a contradiction. Hence, $\mathrm{NT}(g)\cup\\{\varphi(g)\\}$ must be
consistent. Therefore, there exists an $\mathcal{L}^{1}$-structure
$\mathfrak{N}$ and $a^{\prime}$ in $\mathfrak{N}$ such that
$\mathfrak{N}\vDash\mathrm{NT}(g)\cup\\{\varphi(g)\\}[a^{\prime}]$.

For any formula $\psi$, $\mathfrak{M},a\nVdash\psi$ iff $\neg ST_{g}(\psi)\in
NT(g)$, which implies $\mathfrak{N},a^{\prime}\nVdash\psi$. Therefore,
$\mathfrak{N},a^{\prime}\rightsquigarrow_{A}\mathfrak{M},a$. By Theorem 5.11
(Detour Lemma), there exist two $\omega$-saturated $\mathrm{LE}$-models
$\mathfrak{N}^{\omega}$ and $\mathfrak{M}^{\omega}$, and two elementary
embeddings $\omega_{n}:\mathfrak{N}\rightarrow\mathfrak{N}^{\omega}$ and
$\omega_{m}:\mathfrak{M}\rightarrow\mathfrak{M}^{\omega}$, such that
$\mathfrak{N}^{\omega},\omega_{n}(a^{\prime})\rightrightarrows\mathfrak{M}^{\omega},\omega_{m}(a)$.
As $\omega_{n}$ is an elementary embedding and
$\mathfrak{N}\vDash\varphi(g)[a^{\prime}]$, we have
$\mathfrak{N}^{\omega}\vDash\varphi(g)[\omega_{n}(a^{\prime})]$. Therefore, as
$\varphi(g)$ is preserved by simulation,
$\mathfrak{M}^{\omega}\vDash\varphi(g)[\omega_{m}(a)]$. As $\omega_{m}$ is an
elementary embedding, we have $\mathfrak{M}\vDash\varphi(g)[a]$. This
concludes the proof.

##  6 Conclusion

In this paper, we introduced bisimulations on polarity-based semantics for
non-distributive modal logic, demonstrating their application in proving the
Hennessy-Milner and van Benthem theorems. These results show that the non-
distributive modal logic is bisimulation invariant fragment (within a specific
signature and axioms) of two-sorted first-order logic. This work suggests the
following directions for future research.

Characterizing theorem for lattice-based modal $\mu$-calculus: Lattice based
modal $\mu$-calculus, i.e. the extension of non-distributive modal logic with
least and greatest fixed point operators, was defined and studied in [14]. In
[14], it was showed that the formulas of modal $\mu$-calculus are
bisimulation-invariant. The classical modal $\mu$-calculus is characterized as
the bisimulation invariant fragment of monadic second-order logic. It would be
interesting to see if a similar characterization holds in its lattice-based
generalization.

Computational properties of bisimulations: In classical modal logic,
computational complexity of different bisimulation related problems like
checking if two models are bisimlar, computing the largest bisimulation on a
model have been studied extensively [26]. It would be interesting to study
similar complexity problems in a non-distributive setting and compare the
results with the classical setting.

Bisimulations and network analysis: In Social Network Analysis (SNA),
different notions of equivalences between nodes are defined to study the
structural nodes in one or two social networks [23, 15]. On of the most
prominent structural equivalences used in SNA is the notion of regular
equivalence, which is analogous to bisimulations on (multi-modal) Kripke
frames [32, 24]. Enriched formal contexts (polarities) can be seen as bi-
partite networks; so, it would be interesting to study if simulations and
bisimulations defined in this paper can be useful in bi-partite network
analysis.

## Appendix

##  Appendix A Proofs

In this appendix, we show the proofs of the results stated throughout the
paper.

###  A.1 Proof of Theorem 3.5

######  Proof A.1.

We give a proof by induction on the complexity of the formula $\varphi$.
Without loss of generality, let $(S,T)$ be a simulation from
$\mathfrak{M}_{1}$ to $\mathfrak{M}_{2}$. The initial step is when
$\varphi\in\mathcal{V}$ is a propositional variable. For the first item,
assume $a_{1}Sa_{2}$, then $a_{1}\rightsquigarrow_{A}a_{2}$ follows directly
from the item 1 of Definition 3.2. For the second item, assume $x_{1}Ta_{2}$,
then $x_{2}\rightsquigarrow_{X}x_{1}$ follows directly from the item 2 of
Definition 3.2. Now, we consider induction step for all the connectives.

(1) Suppose $\varphi$ is $\psi_{1}\wedge\psi_{2}$.

To prove item 1, suppose $a_{1}Sa_{2}$, and
$\mathfrak{M}_{1},a_{1}\Vdash\psi_{1}\wedge\psi_{2}$. Then,
$\mathfrak{M}_{1},a_{1}\Vdash\psi_{1}$ and
$\mathfrak{M}_{1},a_{1}\Vdash\psi_{2}$, which by induction hypothesis implies
$\mathfrak{M}_{2},a_{2}\Vdash\psi_{1}$ and
$\mathfrak{M}_{2},a_{2}\Vdash\psi_{2}$, which implies
$\mathfrak{M},a_{2}\Vdash\psi_{1}\wedge\psi_{2}$.

To prove item 2, suppose $x_{1}Tx_{2}$ and
$\mathfrak{M}_{1},x_{1}\nsucc\psi_{1}\wedge\psi_{2}$. Then, there exists
$a_{1}\in A_{1}$ such that $a_{1}I^{c}_{1}x_{1}$ and
$\mathfrak{M}_{1},a_{1}\Vdash\psi_{1}\wedge\psi_{2}$. Then, by item 4 of
Definition 3.2, there exists $a_{2}\in A_{2}$ such that $a_{2}I^{c}_{2}x_{2}$
and $a_{1}Sa_{2}$. Therefore,
$\mathfrak{M}_{2},a_{2}\Vdash\psi_{1}\wedge\psi_{2}$, which implies
$\mathfrak{M}_{2},x_{2}\nsucc\psi_{1}\wedge\psi_{2}$.

(2) Suppose $\varphi$ is $\psi_{1}\vee\psi_{2}$. The proof is dual to the
previous case.

(3) Suppose $\varphi=\Box\psi$.

To prove item 1, assume $a_{1}Sa_{2}$, and
$\mathfrak{M}_{2},a_{2}\nVdash\Box\psi$. Then, there exists $x_{2}\in X_{2}$
such that $\mathfrak{M}_{2},x_{2}\succ\psi$ and $a_{2}R^{c}_{\Box_{2}}x_{2}$.
By item 5 Definition 3.2, there exists $x_{1}\in X_{1}$ such that
$a_{1}R^{c}_{\Box_{1}}x_{1}$, and $x_{1}Tx_{2}$. Therefore, by induction
hypothesis $\mathfrak{M}_{1},x_{1}\succ\psi$. Hence,
$\mathfrak{M}_{1},a_{1}\nsucc\Box\psi$.

To prove item 2, suppose $x_{1}Tx_{2}$, and
$\mathfrak{M}_{1},x_{1}\nsucc\Box\psi$. Then, there exists $a_{1}\in A_{1}$
such that $a_{1}I^{c}_{1}x_{1}$ and $\mathfrak{M}_{1},a_{1}\Vdash\Box\psi$. By
item 4 of Definition 3.2, there exists $a_{2}\in A_{2}$ such that
$a_{2}I^{c}_{2}x_{2}$, and $a_{1}Sa_{2}$. Therefore,
$\mathfrak{M}_{2},a_{2}\Vdash\Box\psi$, which implies
$\mathfrak{M}_{2},x_{2}\nsucc\Box\psi$.

(4) Suppose $\varphi$ is $\Diamond\psi$. In this case, the proof is dual to
the previous case. This concludes the proof.

###  A.2 Proof of Theorem 4.3

######  Proof A.2.

Let $\mathfrak{M}_{1}$ and $\mathfrak{M}_{2}$ be two $\mathrm{M}$-saturated
models, and let $a_{1},x_{1}\in\mathfrak{M}_{1}$ and
$a_{2},x_{2}\in\mathfrak{M}_{2}$. We only prove the first item of Definition
4.1, and the proof of the second item is similar. Assume that
$a_{1}\rightsquigarrow_{A}a_{2}$, we claim that
$(\rightsquigarrow_{A},\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}_{X})$
is a simulation from $\mathfrak{M}_{1}$ to $\mathfrak{M}_{2}$, where
$(a,a^{\prime})\in\rightsquigarrow_{A}$ (denoted as
$a\rightsquigarrow_{A}a^{\prime}$) iff
$\mathfrak{M}_{1},a\rightsquigarrow_{A}\mathfrak{M}_{2},a^{\prime}$ and
$(x,x^{\prime})\in\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}_{X}$
(denoted as
$x\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}_{X}x^{\prime}$)
iff
$\mathfrak{M}_{1},x\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}_{X}\mathfrak{M}_{2},x^{\prime}$.
Hence, it is sufficient to show that
$(\rightsquigarrow_{A},\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}_{X})$
satisfies item 1-6 of Definition 3.2.

Items 1 and 2 are easy to check. To prove item 3, assume that
$a_{1}^{\prime}\rightsquigarrow_{A}a_{2}^{\prime}$ and
$a_{2}^{\prime}I^{c}_{2}x_{2}^{\prime}$. Let $\Sigma$ be the set of all the
formulas satisfied at $x_{2}^{\prime}$. Therefore, for any finite subset
$\Delta$ of $\Sigma$, $\mathfrak{M}_{2},x_{2}^{\prime}\succ\bigvee\Delta$.
Therefore, $\mathfrak{M}_{2},a_{2}^{\prime}\nVdash\bigvee\Delta$, which by
$a_{1}^{\prime}\rightsquigarrow_{A}a_{2}^{\prime}$ implies
$\mathfrak{M}_{1},a_{1}^{\prime}\nVdash\bigvee\Delta$. So, there exists
$x_{1}^{\prime}$, such that
$\mathfrak{M}_{1},x_{1}^{\prime}\succ\bigvee\Delta$ and
$a_{1}^{\prime}I^{c}_{1}x_{1}^{\prime}$. Hence, $\Sigma$ is finitely
satisfiable in $\\{x_{1}^{\prime}\mid
a_{1}^{\prime}I^{c}_{1}x_{1}^{\prime}\\}$. Therefore, by
$\mathrm{M}$-saturation of $\mathfrak{M}_{1}$, $\Sigma$ is satisfiable in
$\\{x_{1}^{\prime}\mid a_{1}^{\prime}I^{c}_{1}x_{1}^{\prime}\\}$. Therefore,
there exists $x_{\Sigma}$ such that $a_{1}^{\prime}I^{c}_{1}x_{\Sigma}$ and
all formulas in $\Sigma$ are satisfied at $x_{\Sigma}$ which means
$x_{\Sigma}\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}_{X}x_{2}^{\prime}$.
The item 4 is proved similarly to item 3.

For item 5, assume that $a_{1}^{\prime}\rightsquigarrow_{A}a_{2}^{\prime}$ and
$a_{2}^{\prime}R^{c}_{\Box_{2}}x_{2}^{\prime}$. Let $\Sigma$ be the set of all
the formulas satisfied at $x_{2}^{\prime}$. Therefore, for any finite subset
$\Delta$ of $\Sigma$, $\mathfrak{M}_{2},x_{2}^{\prime}\succ\bigvee\Delta$.
Therefore $\mathfrak{M}_{2},a_{2}^{\prime}\nVdash\Box(\bigvee\Delta)$, which
by $a_{1}^{\prime}\rightsquigarrow_{A}a_{2}^{\prime}$ implies
$\mathfrak{M}_{1},a_{1}^{\prime}\nVdash\Box(\bigvee\Delta)$. So, there exists
$x_{1}^{\prime}$, such that
$\mathfrak{M}_{1},x_{1}^{\prime}\succ\bigvee\Delta$ and
$a_{1}^{\prime}R^{c}_{\Box_{1}}x_{1}^{\prime}$. Hence, $\Sigma$ is finitely
satisfiable in $\\{x_{1}^{\prime}\mid
a_{1}^{\prime}R^{c}_{\Box_{1}}x_{1}^{\prime}\\}$. Therefore, by
$\mathrm{M}$-saturation of $\mathfrak{M}_{1}$, $\Sigma$ is satisfiable in
$\\{x_{1}^{\prime}\mid a_{1}^{\prime}R^{c}_{\Box_{1}}x_{1}^{\prime}\\}$.
Therefore, there exists $x_{\Sigma}$ such that
$a_{1}^{\prime}R^{c}_{\Box_{1}}x_{\Sigma}$ and all formulas in $\Sigma$ are
satisfied at $x_{\Sigma}$, which means
$x_{\Sigma}\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}_{X}x_{2}^{\prime}$.
The item 6 is proved similarly to item 5. This concludes the proof.

###  A.3 Proof of Lemma 4.11

######  Proof A.3.

Let $\mathfrak{M}$ be an $\mathrm{LE}$-model and $\mathfrak{M}^{\mathsf{FI}}$
be its filter-ideal extension. We only prove items 1 and 3 of Definition 4.2
hold for $\mathfrak{M}^{\mathsf{FI}}$. The proofs for items 2 and 4 can be
obtained dually.

1\. Let $F$ be any filter of $\mathfrak{F}^{+}$. Let $\Sigma$ be a set of
$\mathcal{L}$-formulas which is finitely satisfiable in $\\{J\mid FI^{c}J\\}$.
By definition of filter-ideal extension this set is same as $\\{J\mid F\cap
J=\emptyset\\}$. By Lemma 4.7, for any formula $\varphi$,
$\mathfrak{M}^{\mathsf{FI}},J\succ\varphi$ iff
$([\\![{\varphi}]\\!],(\\![{\varphi}]\\!))\in J$. Thus, $\Sigma$ is finitely
satisfiable in $\\{J\mid FI^{c}J\\}$ iff for any finite
$\Delta\subseteq\Sigma$, the ideal generated by the set
$\\{([\\![{\varphi}]\\!],(\\![{\varphi}]\\!))\mid\varphi\in\Delta\\}$ (denoted
by $Id(\Delta)$) is disjoint with $F$. Let

$Y=\bigcup\\{Id(\Delta)\mid\Delta\subseteq\Sigma,\,\Delta\,\mbox{is
finite}\\}.$

It is clear that $F\cap Y=\emptyset$ and
$([\\![{\varphi}]\\!],(\\![{\varphi}]\\!))\in Y$ for all $\varphi\in\Sigma$.
We claim that $Y$ is an ideal of $\mathfrak{F}^{+}$. Suppose $c\in Y$, and
$d\leq c$. By definition of $Y$, $c$ must be in $Id(\Delta)$ for some finite
$\Delta\subseteq\Sigma$. Then, we must have $d\in Id(\Delta)\subseteq Y$.
Finally, suppose $c_{1},c_{2}\in Y$. Then, we must have finite
$\Delta_{1},\Delta_{2}\subseteq\Sigma$ such that, $c_{1}\in Id(\Delta_{1})$
and $c_{2}\in Id(\Delta_{2})$. Therefore, $c_{1},c_{2}\in
Id(\Delta_{1}\cup\Delta_{2})$ implying $c_{1}\vee c_{2}\in
Id(\Delta_{1}\cup\Delta_{2})$. As $\Delta_{1}\cup\Delta_{2}\subseteq\Sigma$ is
finite, we must have $Id(\Delta_{1}\cup\Delta_{2})\subseteq Y$. Thus, we have
$c_{1}\vee c_{2}\in Y$. So, $Y$ is an ideal such that $FI^{c}Y$ and
$\mathfrak{M}^{\mathsf{FI}},Y\succ\Sigma$. Hence proved.

3\. Let $\mathfrak{M}=(\mathfrak{F},V)$ and $F$ be any filter of
$\mathfrak{F}^{+}$. Let $\Sigma$ be a set of formulas which is finitely
satisfiable in $\\{J\mid FR_{\Box}^{c}J\\}$. By definition of filter-ideal
extension, this set is same as $\\{J\mid F\cap\Box J=\emptyset\\}$, where for
any $C\subseteq\mathfrak{F}^{+}$, $\Box C=\\{\Box c\mid c\in C\\}$. By Lemma
4.7, for any formula $\varphi$, $\mathfrak{M}^{\mathsf{FI}},J\succ\varphi$ iff
$([\\![{\varphi}]\\!],(\\![{\varphi}]\\!))\in J$. Thus, $\Sigma$ is finitely
satisfiable in $\\{J\mid FR_{\Box}^{c}J\\}$ iff for any finite
$\Delta\subseteq\Sigma$, the ideal generated by the set
$\\{([\\![{\varphi}]\\!],(\\![{\varphi}]\\!))\mid\varphi\in\Delta\\}$ (denoted
by $Id(\Delta)$) satisfies the condition $\Box Id(\Delta)\cap F=\emptyset$.
Let

$Y=\bigcup\\{Id(\Delta)\mid\Delta\subseteq\Sigma,\,\Delta\,\mbox{is
finite}\\}.$

It is clear that $F\cap\Box Y=\emptyset$ and
$([\\![{\varphi}]\\!],(\\![{\varphi}]\\!))\in Y$ for all $\varphi\in\Sigma$.
By same proof as in item 1, we have that $Y$ is an ideal. Therefore, $Y$ is an
ideal such that $FR_{\Box}^{c}Y$ and
$\mathfrak{M}^{\mathsf{FI}},Y\succ\Sigma$. Hence proved.

## References

  * [1] Aiello, M., J. Van Benthem and G. Bezhanishvili, _Reasoning about space: the modal way_ , Journal of Logic and Computation 13 (2003), pp. 889–920.
  * [2] Bezhanishvili, N., G. Fontaine and Y. Venema, _Vietoris bisimulations_ , Journal of Logic and Computation 20 (2010), pp. 1017–1040.
  * [3] Bezhanishvili, N. and T. Henke, _A model-theoretic approach to descriptive general frames: the van benthem characterization theorem_ , Journal of Logic and Computation 30 (2020), pp. 1331–1355.
  * [4] Blackburn, P., M. d. Rijke and Y. Venema, “Modal Logic,” Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 2001.
  * [5] Chang, C. C. and H. J. Keisler, “Model theory,” Elsevier, 1990.
  * [6] Conradie, W., S. Frittella, K. Manoorkar, S. Nazari, A. Palmigiano, A. Tzimoulis and N. M. Wijnberg, _Rough concepts_ , Information Sciences 561 (2021), pp. 371–413.
  * [7] Conradie, W., S. Frittella, A. Palmigiano, M. Piazzai, A. Tzimoulis and N. M. Wijnberg, _Toward an epistemic-logical theory of categorization_ , Electronic Proceedings in Theoretical Computer Science, EPTCS 251 (2017).
  * [8] Conradie, W. and A. Palmigiano, _Algorithmic correspondence and canonicity for non-distributive logics_ , Annals of Pure and Applied Logic 170 (2019), pp. 923–974, the 23rd Workshop on Logic, Language, Information and Computation.
  * [9] Conradie, W., A. Palmigiano, C. Robinson and N. Wijnberg, _Non-distributive logics: from semantics to meaning_ , in: A. Rezus, editor, _Contemporary Logic and Computing_ , Landscapes in Logic 1, College Publications, 2020 pp. 38–86.
URL arXivpreprintarXiv:2002.04257

  * [10] Conradie, W., A. Palmigiano and A. Tzimoulis, _Goldblatt-thomason for le-logics_ , arXiv preprint arXiv:1809.08225 (2018).
  * [11] Davoren, J., _On intuitionistic modal and tense logics and their classical companion logics: Topological semantics and bisimulations_ , Annals of Pure and Applied Logic 161 (2009), pp. 349–367, papers presented at the Symposium on Logical Foundations of Computer Science 2007.
URL https://www.sciencedirect.com/science/article/pii/S0168007209001468

  * [12] de Groot, J., _Non-distributive positive logic as a fragment of first-order logic over semilattices_ , Journal of Logic and Computation 34 (2024), pp. 180–196.
  * [13] De Rijke, M., _A note on graded modal logic_ , Studia Logica 64 (2000), pp. 271–283.
  * [14] Ding, Y., K. Manoorkar, M. Panettiere, A. Tzimoulis and R. Wang, _Game semantics for lattice-based modal $\\{$$\backslash$mu$\\}$-calculus_, arXiv preprint arXiv:2310.13944 (2023).
  * [15] Fan, T.-F. and C.-J. Liau, _Logical characterizations of regular equivalence in weighted social networks_ , Artificial Intelligence 214 (2014), pp. 66–88.
URL https://www.sciencedirect.com/science/article/pii/S000437021400068X

  * [16] Frittella, S., K. Manoorkar, A. Palmigiano, A. Tzimoulis and N. Wijnberg, _Toward a dempster-shafer theory of concepts_ , International Journal of Approximate Reasoning 125 (2020), pp. 14–25.
  * [17] Ganter, B. and R. Wille, _Applied lattice theory: Formal concept analysis_ , in: _In General Lattice Theory, G. Grätzer editor, Birkhäuser_ , Citeseer, 1997.
  * [18] Goranko, V. and M. Otto, _5 model theory of modal logic_ (2007).
  * [19] Hansen, H. H., C. Kupke and E. Pacuit, _Neighbourhood structures: Bisimilarity and basic model theory_ , Logical Methods in Computer Science 5 (2009).
  * [20] Hennessy, M. and H. Lin, _Symbolic bisimulations_ , Theoretical Computer Science 138 (1995), pp. 353–389.
  * [21] Hennessy, M. and R. Milner, _Algebraic laws for nondeterminism and concurrency_ , Journal of the ACM (JACM) 32 (1985), pp. 137–161.
  * [22] Hollenberg, M. J., “Hennessy-Milner classes and process algebra,” Citeseer, 1994.
  * [23] Lorrain, F. and H. C. White, _Structural equivalence of individuals in social networks_ , The Journal of mathematical sociology 1 (1971), pp. 49–80.
  * [24] Marx, M. and M. Masuch, _Regular equivalence and dynamic logic_ , Social Networks 25 (2003), pp. 51–65.
URL https://www.sciencedirect.com/science/article/pii/S0378873302000369

  * [25] Olkhovikov, G. K., _Model-theoretic characterization of intuitionistic propositional formulas_ , The Review of Symbolic Logic 6 (2013), pp. 348–365.
  * [26] Paige, R. and R. E. Tarjan, _Three partition refinement algorithms_ , SIAM Journal on computing 16 (1987), pp. 973–989.
  * [27] Ponse, A., M. de Rijke and Y. Venema, “Modal Logic and Process Algebra: A Bisimulation Perspective,” Center for the Study of Language and Information Publication Lecture Notes, Cambridge University Press, 1995.
URL https://books.google.nl/books?id=PXPHQgAACAAJ

  * [28] Rijke, M. D., _A system of dynamic modal logic_ , Journal of Philosophical Logic 27 (1998), pp. 109–142.
URL http://www.jstor.org/stable/30227100

  * [29] Rijke, M. D., _A system of dynamic modal logic_ , Journal of Philosophical Logic 27 (1998), pp. 109–142.
URL http://www.jstor.org/stable/30227100

  * [30] Stanković, M., M. Ćirić and J. Ignjatović, _Simulations and bisimulations for fuzzy multimodal logics over heyting algebras_ , Filomat 37 (2023), pp. 711–743.
  * [31] van Benthem, J., “Modal correspondence theory,” Ph.D. thesis, University of Amsterdam (2014).
  * [32] White, D. R. and K. P. Reitz, _Graph and semigroup homomorphisms on networks of relations_ , Social Networks 5 (1983), pp. 193–234.
URL https://www.sciencedirect.com/science/article/pii/0378873383900254