Intuitionistic K is a Bisimulation-Invariant Fragment
of Intuitionistic First-Order Logic
January 01, 1970
We define the notion of IK-bisimulation between the relational semantics for the intuitionistic modal logic IK, and prove that IK arises as the IK-bisimulation-invariant fragment of intuitionistic first-order logic. En route, we provide an intrinsic characterisation result of this logic by way of a Hennessy–Milner-style theorem and develop some intuitionistic first-order model theory, including intuitionistic analogues of Łoś’s Theorem, elementary embeddings and countable saturation.
Bisimulations are an important tool in the study of modal logic and computer science. In computer science, they can be used as an equivalence relation between process graphs [@Mil80; @Park81]. In modal logic they provide a structural notion of equivalence: worlds linked through a bisimulation satisfy the same formulas. The converse result, also known as Hennessy–Milner property [@HenMil85], implies that the language is powerful enough to track down structural differences between the linked worlds. Moreover, Van Benthem’s theorem, originally proved in [@VBen76], provides a relative characterisation theorem that states that normal modal logic is precisely the bisimulation-invariant fragment of classical first-order logic.
Similar results have been attained for several other logics, each having an appropriate notion of bisimulation encapsulating the underlying structure of the logic. These include modal logics without negation [@KurRij97], logics with negative and restorative modalities [@GroMarSte25], monotone modal logic [@Han03], neighbourhood logics [@Han09], (bi-)intuitionistic logic [@Bad16; @GrootPatt19; @Olk13; @Pat97], modal \(\mu\)-calculi (within monadic second order logics) [@EnqSeiVen19; @JanWalu95] and fragments of XPath [@AbrioDescFig17; @FigAre15; @TenBalLit10].
In this paper we prove a characterisation theorem for the intuitionistic modal logic \(\mathsf{IK}\). This logic was introduced by Fischer Servi [@Servi84], and was also studied by Plotkin and Stirling [@PltStir86], Ewald [@Ewa86] and Simpson [@Sim94]. It is one of the myriad intuitionistic counterparts of the classical normal modal logic \(\mathsf{K}\) (see [@Sim94] for an overview), and can be viewed as the collection of modal formulas whose standard translations are provable in intuitionistic first-order logic. While existing analogues of the Van Benthem characterisation theorem for non-classical logics, such as bi-intuitionistic logic and modal extensions of positive logic, use a classical first-order logic [@KurRij97; @Bad16; @GroMarSte25], our aim is to establish \(\mathsf{IK}\) as a bisimulation-invariant fragment of intuitionistic first-order logic.
We follow a standard path to obtain the characterisation theorem. This requires an extension of the intuitionistic ultraproduct construction and of Łoś’s Theorem from [@Gab72; @Mar79] to allow for constants. Moreover, we introduce intuitionistic analogues of elementary embeddings and \(\omega\)-saturation, and accompanying theorems. On the modal side, we use the birelational models of \(\mathsf{IK}\) to provide an intuitive notion of IK-bisimulations and prove a Hennessy–Milner-style theorem. The embedding of intuitionistic first-order structures into birelational models then allows us to transfer this to the intuitionistic first-order setting.
Sections 2 and 3 review basic notions and semantics for intuitionistic first-order logic and for IK. Section 4 defines IK-bisimulations and modal saturation, and establishes a Hennessy–Milner-style theorem. In Section 5 we define (ultra)filter products of intuitionistic first-order structures and give an intuitionistic analogue of Łoś’s Theorem, and in Section 6 we provide an intuitionistic analogue of \(\omega\)-saturation. Finally, Section 7 proves that intuitionistic modal logic IK is the IK-bisimulation-invariant fragment of intuitionistic first-order logic.
We recall some first-order logic-related material. We fix throughout the text, unless otherwise stated, an arbitrary first-order signature \((\mathrm{Cnst},\mathrm{Pred})\), without function symbols, where \(\mathrm{Cnst}\) and \(\mathrm{Pred}\) are disjoint sets containing, respectively, constant symbols and predicate symbols, the latter with respective arities. We also fix a denumerable set \(\mathrm{Var}\), disjoint from \(\mathrm{Cnst}\cup\mathrm{Pred}\), of variables.
Definition 1. The language \(\mathcal{L}\)* (for the signature \((\mathrm{Cnst},\mathrm{Pred})\)) is defined by the grammar \[\varphi::= P(t_1, \ldots, t_n) \mid \bot \mid (\varphi\wedge \varphi) \mid (\varphi\vee \varphi) \mid (\varphi\to \varphi) \mid \forall x\, \varphi \mid \exists x\, \varphi\] where \(P\), with arity \(n\), ranges over \(\mathrm{Pred}\), and where \(t_1, \ldots, t_n\) are terms, i.e. elements of \(\mathrm{Var}\cup \mathrm{Cnst}\), and \(x \in \mathrm{Var}\).*
Definition 2. A \(\mathscr{C\!\!L}\)-structure* (for the signature \((\mathrm{Cnst},\mathrm{Pred})\)) is a pair \(\mathfrak{C} = (D, \mathscr{I})\) consisting of a nonempty set \(D\) and an interpretation \(\mathscr{I}\) that assigns to each \(c \in \mathrm{Cnst}\) an individual \(\mathscr{I}(c) \in D\), and to each \(n\)-ary \(P \in \mathrm{Pred}\) a relation \(\mathscr{I}(P) \subseteq D^n\).*
Definition 3. An \(\mathscr{I\!\!L}\)-structure* (for the signature \((\mathrm{Cnst},\mathrm{Pred})\)) is a tuple \(\mathfrak{M} = (W, \leq, \{ \mathfrak{C}_w \}_{w \in W})\) consisting of a poset \((W, \leq)\) of worlds and for each \(w \in W\) a \(\mathscr{C\!\!L}\)-structure \(\mathfrak{C}_w = (D_w, \mathscr{I}_w)\), for some \(\mathrm{Cnst}_w \subseteq \mathrm{Cnst}\), such that*
if \(w \leq w'\), then \(D_w \subseteq D_{w'}\) and \(\mathscr{I}_w(P) \subseteq \mathscr{I}_{w'}(P)\) for any predicate symbol \(P\);
for each constant symbol \(c \in \mathrm{Cnst}\) there is an individual \(c^{\mathfrak{M}} \in \bigcup_{w \in W} D_w\) such that, for each \(w\in W\):
if \(c^{\mathfrak{M}} \in D_w\), then \(c \in \mathrm{Cnst}_w\) and \(\mathscr{I}_w(c) = c^{\mathfrak{M}}\);
if \(c^{\mathfrak{M}} \notin D_w\), then \(c \notin \mathrm{Cnst}_w\) and \(\mathscr{I}_w(c)\) is not defined.
We write \(D_{\mathfrak{M}} \coloneq \bigcup \{ D_w \mid w \in W \}\) for the domain* of \(\mathfrak{M}\).*
An assignment* for an \(\mathscr{I\!\!L}\)-structure \(\mathfrak{M}\) is a mapping \(\rho : \mathrm{Var}\to D_{\mathfrak{M}}\). Given \(d \in D_{\mathfrak{M}}\) and \(x\in\mathrm{Var}\), we write \(\rho[x \coloneq d]\) for the assignment that gives the value \(d\) to \(x\) and agrees with \(\rho\) on all other variables. An assignment \(\rho: \mathrm{Var}\to D_{\mathfrak{M}}\) can naturally be extended to a mapping \(\rho^\mathfrak{M}: \mathrm{Var}\cup \mathrm{Cnst}\to D_{\mathfrak{M}}\) such that \(\rho^\mathfrak{M}(c)=c^\mathfrak{M}\) for every \(c \in \mathrm{Cnst}\).*
We interpret formulas from the set \(\mathcal{L}\) in \(\mathscr{I\!\!L}\)-structures under an assignment \(\rho\) via: \[\begin{align} {3} &\mathfrak{M}, w \Vdash^{\rho} P(t_1, \ldots, t_n) &&\quad\text{iff}\quad(\rho^{\mathfrak{M}}(t_1), \ldots, \rho^{\mathfrak{M}}(t_n)) \in \mathscr{I}_w(P) \\ &\mathfrak{M}, w \Vdash^{\rho} \bot &&\phantom{\quad\text{iff}\quad}\text{never} \\ &\mathfrak{M}, w \Vdash^{\rho} \varphi\land \psi &&\quad\text{iff}\quad\mathfrak{M}, w \Vdash^{\rho} \varphi \text{ and } \mathfrak{M}, w \Vdash^{\rho} \psi \\ &\mathfrak{M}, w \Vdash^{\rho} \varphi\vee \psi &&\quad\text{iff}\quad\mathfrak{M}, w \Vdash^{\rho} \varphi \text{ or } \mathfrak{M}, w \Vdash^{\rho} \psi \\ &\mathfrak{M}, w \Vdash^{\rho} \varphi\to \psi &&\quad\text{iff}\quad\text{for all } w' \in W, \text{ if } w \leq w' \text{ and } \mathfrak{M}, w' \Vdash^{\rho} \varphi, \text{ then } \mathfrak{M}, w' \Vdash^{\rho} \psi \\ &\mathfrak{M}, w \Vdash^{\rho} \forall x\, \varphi &&\quad\text{iff}\quad\text{for all } w' \in W, \text{ if } w \leq w' \text{ and } d \in D_{w'}, \text{ then } \mathfrak{M}, w' \Vdash^{\rho[x \coloneq d]} \varphi \\ &\mathfrak{M}, w \Vdash^{\rho} \exists x\, \varphi &&\quad\text{iff}\quad\text{there exists a } d \in D_w \text{ such that } \mathfrak{M}, w \Vdash^{\rho[x \coloneq d]} \varphi \end{align}\] We say that a world \(w\) satisfies* a formula \(\varphi \in \mathcal{L}\) under the assignment \(\rho\) if \(\mathfrak{M}, w \Vdash^{\rho} \varphi\). In case \(\mathfrak{M}, w \not\Vdash^{\rho} \varphi\), we say that \(w\) refutes the formula \(\varphi\) under the assignment \(\rho\).*
If \(\varphi\) has no free variables then its interpretation does not depend on \(\rho\), and we sometimes omit reference to it. If \(\varphi\) has one free variable \(x\), then satisfaction of \(\varphi\) depends only on the action of \(\rho\) on \(x\), and we write \(\mathfrak{M}, w \Vdash^{[x \coloneq d]} \varphi\) to mean that \(\mathfrak{M}, w \Vdash^{\rho} \varphi\) for some arbitrary assignment \(\rho\) that maps \(x\) to \(d\).
Note that if \(\rho^{\mathfrak{M}}(t_j) \notin D_w\), then \(P(t_1, \ldots, t_n)\) is not satisfied at \(w\). This agrees, as a matter of fact, with the treatment of atomic formulas provided in [@FitMend:2:2023]. As usual, we have persistence:
Lemma 1. If \(w \leq w'\) and \(\mathfrak{M}, w \Vdash^{\rho} \varphi\), then \(\mathfrak{M}, w' \Vdash^{\rho} \varphi\).
Definition 4. A consecution* is a pair \(\langle \Gamma:\Delta \rangle\), where \(\Gamma,\Delta\subseteq \mathcal{L}\). A (finite) subconsecution of \(\langle \Gamma:\Delta \rangle\) is a consecution \(\langle \Gamma':\Delta' \rangle\) such that \(\Gamma'\) and \(\Delta'\) are (finite) subsets of \(\Gamma\) and \(\Delta\), respectively. We write \(\langle \Gamma:\Delta \rangle(x_1,\ldots,x_n)\) to express that the set of free variables occurring in \(\Gamma\cup \Delta\) is a subset of \(x_1,\ldots,x_n\).*
Definition 5. Let \(\mathfrak{M} = (W, \leq, \{ \mathfrak{C}_w \}_{w \in W})\) be an \(\mathscr{I\!\!L}\)-structure. A world \(w\in W\) and an assignment \(\rho\) for \(\mathfrak{M}\) separate* the consecution \(\langle \Gamma:\Delta \rangle\), denoted by \(\mathfrak{M}, w \Vdash^{\rho} \langle \Gamma:\Delta \rangle\), if, under the assignment \(\rho\), \(w\) satisfies all formulas of \(\Gamma\) and refutes all formulas of \(\Delta\). We say that the consecution \(\langle \Gamma:\Delta \rangle\) is separable in a set \(U \subseteq W\) if there exist \(w \in U\) and an assignment \(\rho\) such that \(\mathfrak{M}, w \Vdash^{\rho} \langle \Gamma:\Delta \rangle\). We call \(\langle \Gamma:\Delta \rangle\) finitely separable in a set \(U \subseteq W\) if every finite subconsecution of \(\langle \Gamma:\Delta \rangle\) is separable in \(U\). A set \(\Omega \subseteq \mathcal{L}\) is satisfied at \(w\) under the assignment \(\rho\) (notation: \(\mathfrak{M}, w \Vdash^{\rho} \Omega\)), if \(\mathfrak{M}, w \Vdash^{\rho} \langle \Omega:\emptyset \rangle\), and \(\Omega\) is called (finitely) satisfiable in a set \(U\) if \(\langle \Omega:\emptyset \rangle\) is (finitely) separable in \(U\). Finally, we say that \(\Omega\) is refuted at \(w\) under \(\rho\) if \(\mathfrak{M}, w \Vdash^{\rho} \langle \emptyset:\Omega \rangle\).*
We recall the intuitionistic modal logic \(\mathsf{IK}\) and its connection to intuitionistic first-order logic via the standard translation. Fix a denumerable set \(\mathrm{Prop}\) of propositional letters. Throughout this section, we take \(\mathrm{Cnst}= \emptyset\) and \(\mathrm{Pred}= \mathrm{Prop}\cup \{ R \}\), where each symbol in \(\mathrm{Prop}\) is taken as unary and \(R\) is a binary predicate symbol. The language \(\mathcal{L}\) and the \(\mathscr{I\!\!L}\)-structures in this section have \((\mathrm{Cnst},\mathrm{Pred})\) as their signature.
Definition 6. The modal language* \(\mathcal{L}_{\Box\Diamond}\) is generated by the grammar \[\varphi::= P \mid \bot \mid (\varphi\wedge \varphi) \mid (\varphi\vee \varphi) \mid (\varphi\to \varphi) \mid \Box\varphi \mid \Diamond\varphi \qquad\text{(where P \in \mathrm{Prop})}\]*
Definition 7. The standard translation \(\mathrm{Var}\times \mathcal{L}_{\Box\Diamond}\to \mathcal{L}\) is recursively defined by \[\begin{align} {2} &\mathop{\mathrm{st}}(x, P) = P(x) \qquad \mathop{\mathrm{st}}(x, \bot) = \bot \qquad &\mathop{\mathrm{st}}(x, \varphi\star \psi) &= \mathop{\mathrm{st}}(x, \varphi) \star \mathop{\mathrm{st}}(x, \psi) \qquad (\star \in \{ \wedge, \vee, \to \}) \\ &\mathop{\mathrm{st}}(x, \Box\varphi) = \forall y(R(x,y) \to \mathop{\mathrm{st}}(y, \varphi)) \qquad &\mathop{\mathrm{st}}(x, \Diamond\varphi) &= \exists y(R(x,y) \wedge \mathop{\mathrm{st}}(y, \varphi)) \end{align}\] where \(y\) is a fresh variable. For \(\Phi \subseteq \mathcal{L}_{\Box\Diamond}\) we define \(\mathop{\mathrm{st}}(x, \Phi) \coloneq \{ \mathop{\mathrm{st}}(x, \varphi) \mid \varphi\in \Phi \}\).
The logic \(\mathsf{IK}\) can then be defined as a set of theorems by \[\mathsf{IK}= \{ \varphi\in \mathcal{L}_{\Box\Diamond}\mid \mathfrak{M}, w \Vdash^{\rho} \mathop{\mathrm{st}}(x,\varphi) \text{ for every \mathscr{I\!\!L}-structure \mathfrak{M}, world w and assignment \rho} \}.\] Then we can use \(\mathscr{I\!\!L}\)-structures \(\mathfrak{M} = (W, \leq, \{ \mathfrak{C}_w \}_{w \in W})\) to interpret formulas \(\varphi\in \mathcal{L}_{\Box\Diamond}\) at a world \(w \in W\) and an individual \(d \in D_w\) via \[\mathfrak{M}, w, d \Vdash^{} \varphi \quad\text{iff}\quad\mathfrak{M}, w \Vdash^{[x \coloneq d]} \mathop{\mathrm{st}}(x,\varphi).\] An alternative adequate semantics for \(\mathsf{IK}\) is given by birelational models [@Sim94]:
Definition 8. A birelational model* is a tuple \(\mathfrak{B}= (W, \leq, R, V)\) consisting of a poset \((W, \leq)\), a valuation \(V\) that maps propositional letters to upsets of \((W, \leq)\), and a binary relation \(R\) on \(W\) such that:*
if \(v \geq w R u\), then there exists a \(t \in W\) such that \(vRt \geq u\), for all \(u, v, w \in W\); and
if \(w R u \leq v\), then there exists a \(t \in W\) such that \(w \leq t R v\), for all \(u, v, w \in W\).
The interpretation of formulas in \(\mathcal{L}_{\Box\Diamond}\) is recursively defined by \[\begin{align} {3} &\mathfrak{B}, w \Vdash P &&\quad\text{iff}\quad w \in V(P) \\ &\mathfrak{B}, w \Vdash \bot & &\phantom{\quad\text{iff}\quad}\text{never} \\ &\mathfrak{B}, w \Vdash \varphi\land \psi &&\quad\text{iff}\quad\mathfrak{B}, w \Vdash \varphi\text{ and } \mathfrak{B}, w \Vdash \psi \\ &\mathfrak{B}, w \Vdash \varphi\lor \psi &&\quad\text{iff}\quad\mathfrak{B}, w \Vdash \varphi\text{ or } \mathfrak{B}, w \Vdash \psi \\ &\mathfrak{B},w \Vdash \varphi\to \psi &&\quad\text{iff}\quad\text{for every } v \in W, \text{ if } w \leq v \text{ and } \mathfrak{B}, v \Vdash \varphi, \text{ then } \mathfrak{B}, v \Vdash \psi \\ &\mathfrak{B}, w \Vdash \Box\varphi &&\quad\text{iff}\quad\text{for every } v, u \in W, \text{if } w \leq v \text{ and } vRu, \text{ then } \mathfrak{B}, u \Vdash \varphi\\ & \mathfrak{B}, w \Vdash \Diamond\varphi &&\quad\text{iff}\quad\text{there exists a } v \in W \text{ such that } wRv \text{ and } \mathfrak{B}, v \Vdash \varphi \end{align}\] Worlds \(w_1\) and \(w_2\) are called modally equivalent (notation: \(w_1 \leftrightsquigarrow w_2\)) if they satisfy the same formulas from \(\mathcal{L}_{\Box\Diamond}\). We define separability, satisfaction and refutation as in Definition 5.
Birelational semantics enjoy the expected persistence property [@Sim94]:
Lemma 2. Let \(\mathfrak{B}= (W, \leq, R, V)\) be a birelational model. If \(w, v \in W\) and \(w \leq v\), then \(\mathfrak{B}, w \Vdash \varphi\) implies \(\mathfrak{B}, v \Vdash \varphi\), for all \(\varphi\in \mathcal{L}_{\Box\Diamond}\).
Every \(\mathscr{I\!\!L}\)-structure gives rise to a birelational model in a truth-preserving way as follows (following Section 8.1.1 of [@Sim94]).
Definition 9. Let \(\mathfrak{M} = (W, \leq, \{ \mathfrak{C}_w \}_{w \in W})\) be an \(\mathscr{I\!\!L}\)-structure. The induced birelational model \(\mathfrak{B}_{\mathfrak{M}}\) is given by \((W^{\bullet}, \leq^{\bullet}, R^{\bullet}, V^{\bullet})\), where: \[\begin{align} W^{\bullet} &= \{ (w, d) \mid w \in W \text{ and } d \in D_w \} &(w, d) \leq^{\bullet} (w', d') &\quad\text{iff}\quad w \leq w' \text{ and } d = d' \\ V^{\bullet}(P) &= \{ (w, d) \mid d \in \mathscr{I}_w(P)\} &(w, d) R^{\bullet} (w', d') &\quad\text{iff}\quad w = w' \text{ and } (d, d') \in \mathscr{I}_w(R) \end{align}\]
Lemma 3. For any \(\mathscr{I\!\!L}\)-structure \(\mathfrak{M} = (W, \leq, \{ \mathfrak{C}_w \}_{w \in W})\), \(w \in W\), \(d \in D_w\) and \(\varphi\in \mathcal{L}_{\Box\Diamond}\) we have \[\mathfrak{M}, w, d \Vdash \varphi\quad\text{iff}\quad\mathfrak{B}_{\mathfrak{M}}, (w,d) \Vdash \varphi.\]
We study IK-bisimulations between birelational frames. These are slightly weaker than the usual definition of a (Kripke) bisimulation from modal logic [@BlaRijVen01] because, as we shall see in Example 1, the usual definition is too strong to prove that bisimilarity and modal equivalence coincide even on finite models. Throughout this section we use the same first-order signature as in Section 3. Given binary relations \(S\) and \(R\), we write \(S \mathrel{;} R \coloneq \{ (x, y) \mid xSz \text{ and } zRy \text{ for some } z \}\) for their sequential composition.
Definition 10. Let \(\mathfrak{B}= (W, \leq, R, V)\) and \(\mathfrak{B}' = (W', \leq', R', V')\) be two birelational models. An IK-bisimulation* between \(\mathfrak{B}\) and \(\mathfrak{B}'\) is a relation \(Z\subseteq W \times W'\) such that for all \((w,w')\in Z\):*
\(w \in V(p)\) if and only if \(w' \in V'(p)\), for all \(p\in\mathrm{Prop}\);
if \(w \leq v\), then there exists a \(v'\in W'\) such that \((v,v')\in Z\) and \(w' \leq' v'\);
if \(w' \leq' v'\), then there exists a \(v\in W\) such that \((v,v')\in Z\) and \(w \leq v\);
if \(w Rv\), then there exists a \(v'\in W'\) such that \((v,v')\in Z\) and \(w' ({\leq'} \mathrel{;} {R'}) v'\);
if \(w' R' v'\), then there exists a \(v\in W\) such that \((v,v')\in Z\) and \(w ({\leq} \mathrel{;} {R}) v\);
if \(wRv\), then there exist \(s \in W\) and \(s' \in W'\) such that \(v \leq s\) and \(w' R' s'\) and \((s,s')\in Z\);
if \(w'R'v'\), then there exist \(s' \in W'\) and \(s \in W\) such that \(v' \leq' s'\) and \(w Rs\) and \((s,s')\in Z\).
We write \(w \rightleftharpoons w'\), and call \(w\) and \(w'\) bisimilar, if there exists an IK-bisimulation that links \(w\) and \(w'\).
The last four conditions can be depicted as follows, where solid and dashed arrows indicate universal and existential quantification, respectively: \[\begin{figure}\includegraphics[width=0.8\textwidth]{_pdflatex/rsadmygl.png}\label{gcwarpet}\end{figure}\tag{1}\]
Note that bisimilarity implies model equivalence, that is:
Let \(\mathfrak{B}= (W, \leq, R, V)\) and \(\mathfrak{B}' = (W', \leq', R', V')\) be two birelational models. Then \(w \rightleftharpoons w'\) implies \(w \leftrightsquigarrow w'\), for all \(w \in W\) and \(w' \in W'\).
Proof. We prove something stronger, namely that for every formula \(\varphi\) and for any pair of worlds \(w, w'\) such that \(w\rightleftharpoons w'\) we have \(\mathfrak{B},w\Vdash \varphi\) iff \(\mathfrak{B}',w'\Vdash \varphi\). This may be checked by structural induction on \(\varphi\). We showcase the inductive steps for \(\Diamond\) and \(\Box\). Assume, then, for a certain formula \(\psi\), the following induction hypothesis, P[\(\psi\)]: \(\mathfrak{B},w\Vdash \psi\) iff \(\mathfrak{B}',w'\Vdash \psi\), for any pair of worlds \(w, w'\) such that \(w\rightleftharpoons w'\). Accordingly, in what follows, take arbitrary worlds \(w, w'\) such that \(w \rightleftharpoons w'\).
\(\triangleright\;\) Case for \(\varphi= \Diamond\psi\). Suppose \(\mathfrak{B}, w \Vdash \varphi\). In view of the assumption that \(w \rightleftharpoons w'\), let \(Z \subseteq W \times W'\) be an \(\mathsf{IK}\) bisimulation between \(\mathfrak{B}\) and \(\mathfrak{B}'\) such that \((w, w') \in Z\). From \(\mathfrak{B}, w \Vdash \Diamond\psi\) we may obtain a world \(v \in W\) such that \(w Rv\) and \(\mathfrak{B}, v \Vdash \psi\). Using [it:sim-diamond-1] we obtain \(s \in W\) and \(s' \in W'\) such that \(v \leq s\), \(w'R's'\) and \((s,s') \in Z\). The induction hypothesis and Lemma 2 then imply \(\mathfrak{B}', s' \Vdash \psi\), hence \(\mathfrak{B}', w' \Vdash \Diamond\psi\). The converse (namely, if \(\mathfrak{B}', w' \Vdash \Diamond\psi\) then \(\mathfrak{B}, w \Vdash \Diamond\psi\)) can be proven similarly.
\(\triangleright\;\) Case for \(\varphi= \Box\psi\). Suppose \(\mathfrak{B}, w \Vdash \varphi\). Let \(Z \subseteq W \times W'\) be an \(\mathsf{IK}\) bisimulation between \(\mathfrak{B}\) and \(\mathfrak{B}'\) such that \((w, w') \in Z\). Let \(t', v' \in W'\) be such that \(w' \leq' t' R' v'\). Then we can use [it:sim-imp-2] and [it:sim-box-2] to find \(t, s, v \in W\) such that \(w \leq t \leq s Rv\) and \((v, v') \in Z\). This implies \(w \leq s\), so by Lemma 2 we have \(\mathfrak{B}, s \Vdash \Box\psi\). Hence \(\mathfrak{B}, v \Vdash \psi\), and by the induction hypothesis \(\mathfrak{B}', v' \Vdash \psi\). This entails that \(\mathfrak{B}', w' \Vdash \Box\psi\). The converse is proven similarly.
This concludes the inductive proof of P[\(\varphi\)], for every \(\varphi\).
Take now worlds \(w, w'\) such that \(w \rightleftharpoons w'\). Given an arbitrary formula \(\varphi\), we may use P[\(\varphi\)] to conclude that \(w \leftrightsquigarrow w'\). ◻
Example 1. Consider the two birelational models drawn below, where the circled worlds indicate the valuation of a proposition letter \(P\), and the intuitionistic accessibility relation is the reflexive closure of the depicted \(\leq\)-arrows: \[\begin{figure}\includegraphics[width=0.8\textwidth]{_pdflatex/gbynmtkf.png}\label{lvxpbuwn}\end{figure}\qquad{(1)}\] The following relation is an IK-bisimulation: \[Z= \big\{ (w_1, w_0'), (w_1, w_1'), (w_2, w_2'), (v_1, v_1') \big\} \cup \big\{ (x, y) \mid x \in \{ v_2, u_1, u_2 \} \text{ and } y \in \{ v_2', u_0', u_1', u_2' \} \big\}.\] In particular, \(w_1\) and \(w'_0\) are modally equivalent. However, there is no Kripke bisimulation between \(w_1\) and \(w'_0\), since \(w_1Rv_1\) cannot be mirrored at \(w_0'\).
Definition 11. We define an IK-bisimulation between two \(\mathscr{I\!\!L}\)-structures \(\mathfrak{M}\) and \(\mathfrak{M}'\) as an IK-bisimulation between the induced birelational models \(\mathfrak{B}_{\mathfrak{M}}\) and \(\mathfrak{B}_{\mathfrak{M}'}\).
Next, we give a notion of saturation that encompasses image-finite birelational models, and prove that on the class of saturated birelational models bisimilarity coincides with logical equivalence.
Definition 12. Let \(\mathfrak{B}= (W, \leq, R, V)\) be a birelational model. A subset \(X \subseteq W\) is called
**positively saturated* if every set \(\Phi \subseteq \mathcal{L}_{\Box\Diamond}\) that is finitely satisfiable in \(X\) is also satisfiable in \(X\);*
**saturated* if every consecution \(\langle \Phi:\Psi \rangle\) that is finitely separable in \(X\) is also separable in \(X\).*
We call \(\mathfrak{B}\) modally saturated* if for each \(w \in W\) the set \(R[w] \coloneq \{ v \in W \mid wRv \}\) is positively saturated, and the sets \({\uparrow}w \coloneq \{ v \in W \mid w \leq v \}\) and \(R_{\uparrow}[w] \coloneq \{ v \in W \mid w ({\leq} \mathrel{;} R) v \}\) are both saturated.*
Theorem 1. Let \(\mathfrak{B}= (W, \leq, R, V)\) and \(\mathfrak{B}' = (W', \leq', R', V')\) be two modally saturated birelational models. Then bisimilarity and modal equivalence coincide between these models.
Proof. We prove that the relation \(Z\) of modal equivalence is an IK-bisimulation. It clearly satisfies [it:sim-prop], and [it:sim-imp-1] and [it:sim-imp-2] are similar to [@Pat97]. We show that \(Z\) satisfies [it:sim-box-1] and [it:sim-diamond-1], the remaining conditions being similar. For [it:sim-box-1], let \((w,w')\in Z\) and \(w Rv\) and suppose towards a contradiction that there exists no \(v' \in R'_{\uparrow}[w'] \coloneq \{ x' \in W' \mid w'({\leq'} \mathrel{;} R')x' \}\) such that \((v,v')\in Z\). Then for each such \(v'\) either
there exists a formula \(\varphi_{v'}\) that is true at \(v\) but not at \(v'\); or
there exists a formula \(\psi_{v'}\) that is true at \(v'\) but not at \(v\).
For each \(v' \in R'_{\uparrow}[w']\), pick such \(\varphi_{v'}\) or \(\psi_{v'}\), and collect them in sets \(\Phi\) and \(\Psi\), respectively. Then there is no world in \(R'_{\uparrow}[w']\) that separates \(\langle \Phi:\Psi \rangle\). Since \(R'_{\uparrow}[w']\) is saturated, this implies that there exist finite subsets \(\Phi' \subseteq \Phi\) and \(\Psi' \subseteq \Psi\) such that no world in \(R'_{\uparrow}[w']\) separates \(\langle \Phi':\Psi' \rangle\). Set \(\varphi\coloneq \bigwedge \Phi'\) and \(\psi \coloneq \bigvee \Psi'\). It follows from frame condition (2) on \(\mathfrak{B}'\) that \(w' ({\leq'} \mathrel{;} R' \mathrel{;} {\leq'}) s'\) implies \(w' ({\leq'} \mathrel{;} {R'}) s'\), that is, \(R'_\uparrow[w']\) is upward-closed under \(\leq'\). Therefore, each \(v'\) such that \(w' ({\leq'} \mathrel{;} {R'}) v'\) satisfies \(\varphi\to \psi\). Furthermore, we have \(v \not\Vdash \varphi\to \psi\), so that ultimately \(w \not\Vdash \Box(\varphi\to \psi)\) while \(w' \Vdash \Box(\varphi\to \psi)\), a contradiction.
Next, to see that \(Z\) satisfies [it:sim-diamond-1], let \((w,w')\in Z\) and \(w Rv\) and suppose towards a contradiction that there exist no \(s \in W\) and \(s' \in W'\) such that \(v \leq s\) and \(w' R' s'\) and \((s,s')\in Z\). Note that, by assumption, in particular, \({\uparrow}v\) is saturated. So, similarly to the previous case, for each \(s' \in R'[w']\) we can find formulas \(\varphi_{s'}\) and \(\psi_{s'}\) such that \(s'\) satisfies \(\varphi_{s'}\) and refutes \(\psi_{s'}\), and each \(s \geq v\) either refutes \(\varphi_{s'}\) or satisfies \(\psi_{s'}\). Let \(\xi_{s'} \coloneq \varphi_{s'} \to \psi_{s'}\). Then \(v \Vdash \xi_{s'}\) and \(s' \not\Vdash \xi_{s'}\). Now let \(\Xi \coloneq \{ \xi_{s'} \mid s' \in R'[w'] \}\). Then no world in \(R'[w']\) satisfies \(\Xi\). Since \(R'[w']\) is positively saturated by assumption, it follows that there exists a finite \(\Xi' \subseteq \Xi\) such that each \(s' \in R'[w']\) refutes some formula in \(\Xi'\). Let \(\xi \coloneq \bigwedge \Xi'\). Then \(v \Vdash \xi\), so \(w \Vdash \Diamond\xi\) while \(w' \not\Vdash \Diamond\xi\), a contradiction. ◻
We define an intuitionistic analogue of the ultrafilter product of classical first-order structures, and use this to prove compactness of the logic. We will also use it in Section 6 to prove that every \(\mathscr{I\!\!L}\)-structure can be elementarily embedded in an \(\omega\)-saturated one. The notion of (ultra)filter product of \(\mathscr{I\!\!L}\)-structures —without constant symbols— may be found in [@Gab72] and [@Mar79]. To improve overall legibility, details of some of our constructions and proofs of some of our results were shifted to Appendix 9. The remaining work in this section mirrors the development of classical model theory (see e.g. [@ChaKei73]).
Definition 13. Let \(I\) be a set, and for each \(i \in I\) let \(\mathfrak{M}_i = (W_i, \leq_i, \{ \mathfrak{C}_{i,w} \}_{w \in W_i})\) be an \(\mathscr{I\!\!L}\)-structure, where \(\mathfrak{C}_{i, w} = (D_{i, w}, \mathscr{I}_{i, w})\). Let \(F\) be a filter on \(I\). Then:
Take \(W\) to be the reduced product \(\prod_{i \in I}^F W_i\), namely the elements in \(\prod_{i \in I} W_i\) modulo the equivalence relation given by \(\alpha \sim \beta\) iff \(\{ i \in I \mid \alpha(i) = \beta(i) \} \in F\). The equivalence class of \(\alpha\) is denoted by \(\alpha_F\).
Define the relation \(\leq\) on \(W\) by \(\alpha_F \leq \beta_F\) if and only if \(\{ i \in I \mid \alpha(i) \leq_i \beta(i) \} \in F\)
For each \(i \in I\), let \(D_i \coloneq D_{\mathfrak{M}_i} = \bigcup_{w \in W_i} D_{i,w}\). Let \(D = \prod_{i \in I}^F D_i\) be the reduced product of the \(D_i\), namely the elements in \(\prod_{i \in I} D_i\) modulo the equivalence relation \(\xi \approx \eta\) iff \(\{ i \in I \mid \xi(i) = \eta(i) \} \in F\), and denote the equivalence classes by \(\xi_F\). Define the domain \(D_{\alpha_F}\) at \(\alpha_F \in W\) by \[D_{\alpha_F} \coloneq \{ \xi_F \in D \mid \{ i \in I \mid \xi(i) \in D_{i,\alpha(i)} \} \in F \}.\]
For \(c \in \mathrm{Cnst}\), define \(\tilde{c} : I \to \bigcup_{i \in I} D_i\) by \(\tilde{c}(i) = c^{\mathfrak{M}_i}\), and let \(\mathscr{I}_{\alpha_F}(c) \coloneq \tilde{c}_F\) if \(\tilde{c}_F \in D_{\alpha_F}\) and leave the interpretation of \(c\) undefined otherwise.
Finally, for each \(n\)-ary predicate \(P \in \mathrm{Pred}\), define its interpretation by \[(\xi_F^1, \ldots, \xi_F^n) \in \mathscr{I}_{\alpha_F}(P) \quad\text{iff}\quad\{ i \in I \mid (\xi^1(i), \ldots, \xi^n(i)) \in \mathscr{I}_{i, \alpha(i)}(P) \} \in F.\]
For each \(\alpha_F \in W\) we get a \(\mathscr{C\!\!L}\)-structure \(\mathfrak{C}_{\alpha_F} = (D_{\alpha_F}, \mathscr{I}_{\alpha_F})\). The filter product* of the \(\mathfrak{M}_i\) is given by \[\prod_{i \in I}^F \mathfrak{M}_i = (W, \leq, \{ \mathfrak{C}_{\alpha_F} \}_{\alpha_F \in W}).\]*
Let \(I\) be a set, and for each \(i \in I\) let \(\mathfrak{M}_i\) be an \(\mathscr{I\!\!L}\)-structure. Let \(F\) be a filter on \(I\). Then the filter product \(\prod_{i \in I}^F \mathfrak{M}_i\) is an \(\mathscr{I\!\!L}\)-structure.
Definition 14. Let \(I\) be a set, let \(\mathfrak{M}_i\) be an \(\mathscr{I\!\!L}\)-structure, for each \(i \in I\), and let \(F\) be a filter over \(I\). If \(F\) is an ultrafilter, then the filter product \(\prod_{i \in I}^F \mathfrak{M}_i\) is called an ultraproduct. Finally, if \(\mathfrak{M}_i = \mathfrak{M}\) for all \(i \in I\), then the ultraproduct is called an ultrapower* of \(\mathfrak{M}\).*
The next goal is the following analogue of Łoś’s Theorem. This requires the following notion of a product of assignments.
Definition 15. Suppose \(\rho_i\) is an assignment for \(\mathfrak{M}_i\), for each \(i \in I\). For each \(x \in \mathrm{Var}\), define \(\rho(x) : I \to \bigcup_{i \in I} D_i : i \mapsto \rho_i(x)\). Then the product assignment* \(\rho_F\) maps \(x\) to the equivalence class of \(\rho(x)\), i.e. \(\rho_F(x) \coloneq \rho(x)_F\).*
We obtain the following analogue of Łoś’s Theorem, a proof of which can be found in Appendix 9.
Theorem 2. Let \(I\) be a set, and for each \(i \in I\) let \(\mathfrak{M}_i\) be an \(\mathscr{I\!\!L}\)-structure and \(\rho_i\) an assignment for \(\mathfrak{M}_i\). Let \(F\) be an ultrafilter on \(I\), \(\mathfrak{M} \coloneq \prod_{i \in I}^F \mathfrak{M}_i\) be the filter product, and \(\rho_F\) be the product assignment for \(\mathfrak{M}\). Then for any world \(\alpha_F \in W\) and any formula \(\varphi(x_1, \ldots, x_n)\) such that \(\rho_F(x_1), \ldots, \rho_F(x_n) \in D_{\alpha_F}\), \[\mathfrak{M}, \alpha_F \Vdash^{\rho_F} \varphi \quad\text{iff}\quad\{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i} \varphi \} \in F.\]
As an application of Łoś’s Theorem, we prove that every \(\mathscr{I\!\!L}\)-structure can be elementarily embedded in any of its ultrapowers. We begin by defining an intuitionistic analogue of elementary embeddings.
Definition 16. Let \(\mathfrak{M} = (W, \leq, \{ \mathfrak{C}_{w} \}_{w \in W})\) and \(\mathfrak{M}' = (W', \leq', \{ \mathfrak{C}_{w'} \}_{w' \in W'})\) be two \(\mathscr{I\!\!L}\)-structures. An elementary embedding* of \(\mathfrak{M}\) into \(\mathfrak{M'}\) is a pair \((\epsilon, \eta)\) of injective functions \(\epsilon : W \to W'\) and \(\eta : D_{\mathfrak{M}} \to D_{\mathfrak{M}'}\) such that for every \(\varphi\in \mathcal{L}\), \(w \in W\) and assignment \(\rho\): \[\mathfrak{M}, w \Vdash^{\rho} \varphi \quad\text{iff}\quad\mathfrak{M}', \epsilon(w) \Vdash^{\eta \circ \rho} \varphi.\]*
Definition 17. Let \(\mathfrak{M} = (W, \leq, \{ \mathfrak{C}_w \}_{w \in W})\) be an \(\mathscr{I\!\!L}\)-structure, \(I\) be a set, \(F\) be an ultrafilter over \(I\), and write \(\mathfrak{M}^* = (W^*, \leq^*, \{ \mathfrak{C}_{\alpha_F} \}_{\alpha_F \in W^*})\) for the ultrapower of \(\mathfrak{M}\) modulo \(F\). As in Definition 3, let \(D_{\mathfrak{M}^*} \coloneq \bigcup_{\alpha_F \in W^*} D_{\alpha_F}\). For each \(w \in W\), let \(w^* \in W^* \coloneq \prod_{i \in I}^F W\) be the equivalence class of the constant function \(I \to W : i \mapsto w\) and for each \(d \in D_{\mathfrak{M}}\) let \(d^* \in D_{\mathfrak{M}^*} = \prod_{i \in I}^F D_{\mathfrak{M}}\) be the equivalence class of the constant map \(I \to D_{\mathfrak{M}} : i \mapsto d\). The natural embedding* of \(\mathfrak{M}\) into \(\mathfrak{M}^*\) is given by \[\epsilon : W \to W^* : w \mapsto w^* \quad\text{and}\quad \eta : D_{\mathfrak{M}} \to D_{\mathfrak{M}^*} : d \mapsto d^*.\]*
Let \(\mathfrak{M}\) be an \(\mathscr{I\!\!L}\)-structure, \(I\) be a set and \(F\) be an ultrafilter over \(I\). The natural embedding of \(\mathfrak{M}\) into \(\mathfrak{M}^*\) is an elementary embedding.
Proof. The maps \(w \mapsto w^*\) and \(d \mapsto d^*\) are clearly injective. Let \(\rho\) be any assignment for \(\mathfrak{M}\), and let \(\rho^*\) be the product assignment on \(\mathfrak{M}^*\) induced by \(\rho\) (as in Definition 15). Then \(\rho^* = \eta \circ \rho\). Furthermore, for any \(w \in W\) we have \(w^*(i) = w\), so we get \[\begin{align} \mathfrak{M}^*, w^* \Vdash^{\eta \circ \rho} \varphi &\quad\text{iff}\quad\mathfrak{M}^*, w^* \Vdash^{\rho^*} \varphi &\text{(because \rho^* = \eta \circ \rho)} \\ &\quad\text{iff}\quad\{ i \in I \mid \mathfrak{M}, w^*(i) \Vdash^{\rho} \varphi \} \in F &\text{(Theorem~\ref{thm:Los})} \\ &\quad\text{iff}\quad\{ i \in I \mid \mathfrak{M}, w \Vdash^{\rho} \varphi \} \in F &\text{(because w^*(i) = w)} \\ &\quad\text{iff}\quad\mathfrak{M}, w \Vdash^{\rho} \varphi \end{align}\] The last “iff” follows from the fact that \(\{ i \in I \mid \mathfrak{M}, w \Vdash^{\rho} \varphi \}\) is either empty (if \(\mathfrak{M}, w \not\Vdash^{\rho} \varphi\)) or equal to \(I\) (if \(\mathfrak{M}, w \Vdash^{\rho} \varphi\)), so it is in \(F\) if and only if the latter is the case. ◻
Finally, still mirroring the classical case, we use Łoś’s Theorem 2 to prove compactness of the logic.
Definition 18. Given \(\Gamma,\Delta \subseteq \mathcal{L}\), we say that \(\Delta\) is a consequence of* \(\Gamma\), and write \(\Gamma\models \Delta\), if for every \(\mathscr{I\!\!L}\)-structure \(\mathfrak{M}\), there is no \(w \in W\) and no assignment \(\rho\) that separate \(\langle \Gamma:\Delta \rangle\) in \(\mathfrak{M}\). We say that two formulas \(\varphi\) and \(\psi\) are logically equivalent if \(\{\varphi\}\models \{\psi\}\) and \(\{\psi\}\models \{\varphi\}\).*
Theorem 3. Let \(\langle \Gamma:\Delta \rangle(x_1,\ldots,x_n)\) be a consecution in \(\mathcal{L}\) and let \(I\) be the set of all of its finite subconsecutions, i.e. \(I = \{ \langle \Gamma_\mathrm{fin}:\Delta_\mathrm{fin} \rangle \mid \Gamma_\mathrm{fin}\subseteq \Gamma \text{ and } \Delta_\mathrm{fin}\subseteq \Delta \text{ are finite} \}.\) For each \(i \in I\), let \(\mathfrak{M}_i = (W_i, {\leq_i,} \{ \mathfrak{C}_{i, w} \}_{w \in W_i})\) be an \(\mathscr{I\!\!L}\)-structure, \(w_i \in W_i\) and \(\rho_i\) an assignment such that \(\mathfrak{M}_i, w_i \Vdash^{\rho_i} i\). Then there exists an ultrafilter \(F\) over \(I\) such that \(\prod_{i \in I}^F \mathfrak{M}_i, \{ (i, w_i) \mid i \in I \}_F \Vdash^{\rho_F} \langle \Gamma:\Delta \rangle\), where \(\rho_F\) is the product assignment of the \(\rho_i\).
Proof. For each pair \((\gamma,\delta)\) such that \(\gamma \in \Gamma\) and \(\delta \in \Delta\), define \[\overline{(\gamma,\delta)} = \{ \langle \Gamma_\mathrm{fin}:\Delta_\mathrm{fin} \rangle \in I \mid \gamma \in \Gamma_\mathrm{fin}\text{ and } \delta \in \Delta_\mathrm{fin}\} \quad\text{and}\quad E = \{\overline{(\gamma,\delta)} \mid \gamma \in \Gamma \text{ and } \delta \in \Delta \}.\] Then \(E\) has the finite intersection property because for any given \(\overline{(\gamma_1,\delta_1)},\ldots, \overline{(\gamma_n,\delta_n)} \in E\) we have \[\langle \{\gamma_1,\ldots,\gamma_n\}:\{\delta_1,\ldots,\delta_n\} \rangle \in {\overline{(\gamma_1,\delta_1)}}\cap\cdots\cap {\overline{(\gamma_n,\delta_n)}}.\] By the ultrafilter theorem [@ChaKei73] there exists an ultrafilter \(F\) on \(I\) such that \(E \subseteq F\). Now consider an arbitrary pair \((\gamma, \delta)\) such that \(\gamma \in \Gamma\) and \(\delta \in \Delta\), and \(i= \langle \Gamma_\mathrm{fin}:\Delta_\mathrm{fin} \rangle \in I\). If \(i \in \overline{(\gamma,\delta)}\), then \(\gamma \in \Gamma_\mathrm{fin}, \delta \in \Delta_\mathrm{fin}\) and hence \(\mathfrak{M}_i, w_i \Vdash^{\rho_i} \gamma\) and \(\mathfrak{M}_i, w_i \not\Vdash^{\rho_i} \delta\). Therefore, \(\overline{(\gamma,\delta)} \subseteq \{ i \in I \mid \mathfrak{M}_i, w_i \Vdash^{\rho_i} \gamma\}\) and \(\overline{(\gamma,\delta)} \subseteq \{ i \in I \mid \mathfrak{M}_i, w_i \not\Vdash^{\rho_i} \delta \}\), and since \(\overline{(\gamma, \delta)} \in F\) by construction we get \[\{ i \in I \mid \mathfrak{M}_i, w_i \Vdash^{\rho_i} \gamma\} \in F \quad\text{and}\quad \{ i \in I \mid \mathfrak{M}_i, w_i \not\Vdash^{\rho_i} \delta\} \in F.\] Because \(F\) is an ultrafilter we get \(\{ i \in I \mid \mathfrak{M}_i, w_i \Vdash^{\rho_i} \delta\} \not\in F\), so Theorem 2 entails \[\prod_{i \in I}^F\mathfrak{M}_i, \{(i,w_i) \mid i \in I \}_F \Vdash^{\rho_F} \gamma \quad\text{and}\quad \prod_{i \in I}^F\mathfrak{M}_i, \{(i,w_i) \mid i \in I \}_F \not\Vdash^{\rho_F} \delta,\] where \(\{ (i, w_i) \mid i \in I \}_F\) denotes the equivalence class of the function \(I \to \bigcup_i W_i : i \mapsto w_i\). Note that \(\rho_i\) does not depend on \(\gamma\) or \(\delta\). Therefore \(\{(i,w_i) \mid i \in I \}_F\) and \(\rho_F\) separate the consecution \(\langle \Gamma:\Delta \rangle\) in \(\prod_{i \in I}^F\mathfrak{M}_i\). ◻
Corollary 1. If \(\Gamma \models \Delta\), then there exist finite subsets \(\Gamma_\mathrm{fin}\subseteq \Gamma\) and \(\Delta_\mathrm{fin}\subseteq \Delta\) such that \(\Gamma_\mathrm{fin}\models \Delta_\mathrm{fin}\).
Proof. Let \(\Gamma \models \Delta\) and suppose towards a contradiction that for all finite \(\Gamma_\mathrm{fin}\subseteq \Gamma\) and \(\Delta_\mathrm{fin}\subseteq \Delta\), we have \(\Gamma_\mathrm{fin}\not\models \Delta_\mathrm{fin}\). Let \(I\) be the set of finite subconsecutions of \(\langle \Gamma:\Delta \rangle\). Then for every \(i \in I\) there exists an \(\mathscr{I\!\!L}\)-structure \(\mathfrak{M}_i = (W_i, \leq_i, \{ \mathfrak{C}_{i,w} \}_{w \in W_i})\), a world \(w_i \in W_i\) and an assignment \(\rho_i\) such that \(\mathfrak{M}_i, w_i \Vdash^{\rho_i} i\). Therefore Theorem 3 implies that there exists an ultrafilter \(F\) over \(I\) such that \(\prod_{i \in I}^F \mathfrak{M}_i, \{(i,w_i) \mid i \in I\}_F \Vdash^{\rho_F} \langle \Gamma:\Delta \rangle\), where \(\rho_F\) is the product assignment. As a consequence \(\Gamma \not\models \Delta\), a contradiction. ◻
A final ingredient we need in the proof of the characterisation theorem for \(\mathsf{IK}\) is a way to turn an \(\mathscr{I\!\!L}\)-structure into a modally saturated one. More precisely, we wish to elementarily embed any \(\mathscr{I\!\!L}\)-structure \(\mathfrak{M}\) into an \(\mathscr{I\!\!L}\)-structure \(\mathfrak{M}^*\) whose induced birelational model \(\mathfrak{B}_{\mathfrak{M}^*}\) is modally saturated in the sense of Definition 12. Keeping in sync with the classical case, we do so using an intuitionistic variation of the notion of \(\omega\)-saturation which is tailored towards our needs as an intermediary between \(\mathscr{I\!\!L}\)-structures and modally saturated birelational models.
Definition 19. Given an \(\mathscr{I\!\!L}\)-structure \(\mathfrak{M} = (W, \leq, \{ \mathfrak{C}_w \}_{w \in W})\) and \(A\subseteq\bigcup_{w\in W}D_w\), we write \(\mathcal{L}_A\) for the extension of \(\mathcal{L}\) with constants \(\{ \underline{a} \mid a \in A \}\). We define \((\mathfrak{M})_A\) as the \(\mathscr{I\!\!L}_A\)-structure that extends the \(\mathscr{I\!\!L}\)-structure \(\mathfrak{M}\) by interpreting each of the new constants \(\underline{a}\) as \(a\).
Definition 20. Let \(\mathfrak{M} = (W, \leq, \{ \mathfrak{C}_w \}_{w \in W})\) be an \(\mathscr{I\!\!L}\)-structure.
A set \(U \subseteq W\) is called positively \(\omega\)-saturated* if for all finite \(A \subseteq \bigcap_{w \in U} D_w\) and every set \(\Gamma(x) \subseteq \mathcal{L}_A\) with one free variable \(x\), if \(\Gamma(x)\) is finitely satisfiable in \(U\), then it is satisfiable in \(U\).*
The set \(U \subseteq W\) is called \(\omega\)-saturated* if for all finite \(A \subseteq \bigcap_{w \in U} D_w\) and all sets \(\Gamma(x), \Delta(x) \subseteq \mathcal{L}_A\) with one free variable \(x\), if \(\langle \Gamma(x):\Delta(x) \rangle\) is finitely separable in \(U\), then it is separable in \(U\).*
The \(\mathscr{I\!\!L}\)-structure \(\mathfrak{M}\) is called \(\omega\)-saturated* if, for every \(w \in W\), the set \(\{ w \}\) is positively \(\omega\)-saturated and \({\uparrow}w\) is \(\omega\)-saturated.*
We verify that every \(\omega\)-saturated \(\mathscr{I\!\!L}\)-structure gives rise to a modally saturated birelational model.
Let \(\mathfrak{M} = (W, \leq, \{ \mathfrak{C}_w \}_{w \in W})\) be an \(\omega\)-saturated \(\mathscr{I\!\!L}\)-structure. Then the induced birelational model \(\mathfrak{B}_{\mathfrak{M}} = (W^{\bullet}, \leq^{\bullet}, R^{\bullet}, V^{\bullet})\) is modally saturated.
Proof. Let \((w, d) \in W^{\bullet}\) be an arbitrary world. One may check, similarly to [@BlaRijVen01], that \(R^{\bullet}[(w, d)]\) is positively saturated. We verify the two remaining saturation conditions from Definition 12.
\({\uparrow}(w,d)\) is saturated. Let \(\Phi, \Psi \subseteq \mathcal{L}_{\Box\Diamond}\) be sets of formulas that are finitely separable in \({\uparrow}(w,d)\). Consider the consecution \(\langle \mathop{\mathrm{st}}(x, \Phi):\mathop{\mathrm{st}}(x, \Psi) \rangle\). Then each of its finite subconsecutions is of the form \(\langle \mathop{\mathrm{st}}(x, \Phi'):\mathop{\mathrm{st}}(x, \Psi') \rangle\) for some finite \(\Phi' \subseteq \Phi\) and \(\Psi' \subseteq \Psi\). By assumption, we can find some \((v, d) \in {\uparrow}(w, d)\) that satisfies \(\Phi'\) and refutes \(\Psi'\), which implies \(\mathfrak{M}, v \Vdash^{[x \coloneq d]} \bigwedge\mathop{\mathrm{st}}(x,\Phi')\) and \(\mathfrak{M}, v \not\Vdash^{[x \coloneq d]} \bigvee\mathop{\mathrm{st}}(x,\Psi')\). Therefore \(\langle \mathop{\mathrm{st}}(x, \Phi'):\mathop{\mathrm{st}}(x, \Psi') \rangle\) is finitely separable in \({\uparrow}w\), and since \(\mathfrak{M}\) is assumed to be \(\omega\)-saturated it must also be separable in some world \(u \in {\uparrow}w\). This entails that \((u, d) \in {\uparrow}(w, d)\) separates \(\langle \Phi:\Psi \rangle\), as desired.
\(R^\bullet_{\uparrow}[(w,d)]\) is saturated. Let \(\Phi, \Psi \subseteq \mathcal{L}_{\Box\Diamond}\) and suppose that for any finite \(\Phi' \subseteq \Phi\) and \(\Psi' \subseteq \Psi\) there exists a world \((v, e) \in R^\bullet_{\uparrow}[(w, d)]\) separating \(\langle \Phi':\Psi' \rangle\). Note that \((v, e) \in R^{\bullet}_{\uparrow}[(w, d)]\) iff \((w, d) \leq^{\bullet} (v, d) R^{\bullet} (v, e)\), iff \(w \leq v\) and \((d, e) \in \mathscr{I}_v(R)\). Define \[\Gamma \coloneq \{R\underline{d}x\} \cup \mathop{\mathrm{st}}(x, \Phi) \quad\text{and}\quad \Delta \coloneq \mathop{\mathrm{st}}(x, \Psi).\] We claim that \(\langle \Gamma:\Delta \rangle\) is finitely separable in \({\uparrow}w\) on the \(\mathscr{I\!\!L}\)-structure \(\mathfrak{M}\). To see this, let \(\langle \Gamma':\Delta' \rangle\) be a finite subconsecution of \(\langle \Gamma:\Delta \rangle\), and let \(\Phi' \coloneq \{ \varphi\in \Phi \mid \mathop{\mathrm{st}}(x, \varphi) \in \Gamma' \}\) and \(\Psi' \coloneq \{ \psi \in \Psi \mid \mathop{\mathrm{st}}(x, \psi) \in \Delta' \}\). Then \(\Phi'\) and \(\Psi'\) are finite, so by assumption we can find some \((v, e) \in R^\bullet_{\uparrow}[(w, d)]\) that separates \(\langle \Phi':\Psi' \rangle\). This gives \(\mathfrak{M}, v \Vdash^{[x \coloneq e]} \langle \Gamma':\Delta' \rangle\), since \((v, e) \in R^\bullet_{\uparrow}[(w, d)]\) implies \(\mathfrak{M}, v \Vdash^{[x\coloneq e]} R\underline{d}x\). As we have seen, \((v, e) \in R^\bullet_{\uparrow}[(w, d)]\) implies \(w \leq v\), so \(\langle \Gamma:\Delta \rangle\) is finitely separable in \({\uparrow}w\). Since \(\mathfrak{M}\) is \(\omega\)-saturated, we can find some \(u \in {\uparrow}w\) and \(b \in D_u\) such that \(\mathfrak{M}, u \Vdash^{[x\coloneq b]} \langle \Gamma:\Delta \rangle\). From this it follows that \((u, b) \in W^{\bullet}\) is an element of \(R^\bullet_{\uparrow}[(w,d)]\) that separates \(\langle \Phi:\Psi \rangle\). We conclude that \(R^\bullet_{\uparrow}[(w, d)]\) is saturated, as desired. ◻
Recall that a countably incomplete ultrafilter on a set \(I\) is an ultrafilter that is not closed under countably infinite intersections [@ChaKei73]. Modifying [@ChaKei73] we have:
Let \(\mathcal{L}\) be a language over a countable signature, let \(I\) be a set and \(\mathfrak{M}_i\) an \(\mathscr{I\!\!L}\)-structure for each \(i \in I\). If \(F\) is a countably incomplete ultrafilter on \(I\), then \(\prod_{i \in I}^F\mathfrak{M}_i\) is \(\omega\)-saturated.
Proof. Part 1: for any world \(\alpha_F\) in \(\prod_{i \in I}^F\mathfrak{M}_i\), the set \(\{ \alpha_F \}\) is positively \(\omega\)-saturated. Let \(\alpha_F\) be an element of the ultraproduct \(\prod_{i \in I}^F \mathfrak{M}_i\). Let \(A \subseteq D_{\alpha_F}\) be a finite set of individuals of \(\alpha_F\) and let \(\mathscr{I\!\!L}_A\) be the extension of the language with constants \(\underline{a}\) for each \(a_F \in A\). Let \(A_i = \{ a(i) \mid a_F \in A \}\). Then we have \[\Big(\prod_{i \in I}^F\mathfrak{M}_i\Big)_A = \prod_{i \in I}^F((\mathfrak{M}_i)_{A_i}).\] Let \(\Gamma(x)=\{ \gamma_1(x), \gamma_2(x), \ldots \}\) be a subset of \(\mathcal{L}_A\) that is finitely satisfiable in \(\{ \alpha_F \}\). Since \(\Gamma(x)\) is finitely satisfiable in \(\{ \alpha_F \}\), for each \(n \in \mathbb{N}\) we can find some \(d \in D_{\alpha_F}\) such that \(\prod_{i \in I}^F(\mathfrak{M}_i)_{A_i}, \alpha_F \Vdash^{[x \coloneq d]} \gamma_1(x) \wedge \cdots \wedge \gamma_n(x)\). Hence for each \(n \in \mathbb{N}\), \[\prod_{i \in I}^F((\mathfrak{M}_i)_{A_i}), \alpha_F \Vdash^{} \exists x(\gamma_1(x)\land\cdots\land\gamma_n(x))\]
Using the fact that \(F\) is countably incomplete, we can find a descending chain \(I = I_0 \supseteq I_1 \supseteq I_2 \supseteq \cdots\) of sets in \(F\) such that \(\bigcap_{n \in \mathbb{N}} I_n = \emptyset\). Let \(X_0 = I\), and for each \(n \in \mathbb{N}_{>0}\) define \[X_n = I_n \cap \{i \in I \mid (\mathfrak{M}_i)_{A_i}, \alpha(i) \Vdash^{} \exists x(\gamma_1(x)\land \cdots \wedge \gamma_n(x))\}\] By Łoś’s Theorem, the right part of the intersection belongs to \(F\) and hence \(X_n \in F\). Moreover, we have \(X_n \supseteq X_{n+1}\) for all \(n \in \mathbb{N}\), and \(\bigcap_{n \in\mathbb{N}} X_n = \emptyset\). As a consequence, for each \(i \in I\) there exists an \(n(i) \in \mathbb{N}\) such that \(n(i)\) is the greatest natural number with \(i \in X_{n(i)}\), so there exists an assignment \(\rho_i\) for \(\mathfrak{M}_i\) such that \[(\mathfrak{M}_i)_{A_i}, \alpha(i) \Vdash^{\rho_i} \gamma_1(x)\land\cdots\land\gamma_{n(i)}(x)\]
Now let \(n \in \mathbb{N}_{>0}\) and \(i \in X_n\). Then \(n \leq n(i)\) and hence \((\mathfrak{M}_i)_{A_i}, \alpha(i) \Vdash^{\rho_i} \gamma_n(x)\). Since \(X_n \in F\), we have \[X_n \subseteq \{ i \in I \mid (\mathfrak{M}_i)_{A_i}, \alpha(i) \Vdash^{\rho_i} \gamma_n(x) \} \in F\] so, by Łoś’s Theorem 2, we have \(\prod_{i \in I}^F((\mathfrak{M}_i)_{A_i}), \alpha_F \Vdash^{\rho_F} \gamma_n(x)\), where \(\rho\) is the product assignment. Since this holds for any \(n \in \mathbb{N}_{>0}\), it follows that \(\Gamma(x)\) is satisfiable in \(\{\alpha_F\}\).
Part 2: for any world \(\alpha_F\) in \(\prod_{i \in I}^F\mathfrak{M}_i\), the set \({\uparrow}\alpha_F\) is \(\omega\)-saturated. Let \(\alpha_F\) be an element of the ultraproduct \(\prod_{i \in I}^F \mathfrak{M}_i\). Let \(A \subseteq \bigcap_{\beta_F \in {\uparrow}\alpha_F}D_{\beta_F} = D_{\alpha_F}\) be a finite set of individuals of \(\alpha_F\) and let \(\mathscr{I\!\!L}_A\) be the extension of the language with constants \(\underline{a}\) for each \(a_F \in A\). Let \(A_i = \{ a(i) \mid a_F \in A \}\). As before, we have \((\prod_{i \in I}^F\mathfrak{M}_i)_A = \prod_{i \in I}^F((\mathfrak{M}_i)_{A_i})\).
Let \(\Gamma(x),\Delta(x) \subseteq \mathcal{L}_A\) be countable sets such that \(\prod_{i \in I}^F((\mathfrak{M}_i)_{A_i})\) finitely separates \(\langle \Gamma(x):\Delta(x) \rangle\) in the set \({\uparrow}\alpha_F\). Then we can write \(\Gamma(x) = \{ \gamma_1(x), \gamma_2(x), \ldots \}\) and \(\Delta(x) = \{ \delta_1(x), \delta_2(x), \ldots \}\). By hypothesis, for each \(n \in \mathbb{N}\) there exists an \(\alpha_F \leq \beta^n_F\) and an assignment \(\rho_F^n\) such that \[\prod_{i \in I}^F((\mathfrak{M}_i)_{A_i}), \beta^n_F \Vdash^{\rho_F^n} \langle \{\gamma_1(x),\ldots,\gamma_n(x)\}:\{\delta_1(x),\ldots,\delta_n(x)\} \rangle\] and hence, since \(\alpha_F \leq \beta^n_F\), \[\prod_{i \in I}^F((\mathfrak{M}_i)_{A_i}), \alpha_F \not\Vdash^{} \forall x( (\gamma_1(x) \wedge \cdots \wedge \gamma_n(x)) \to (\delta_1(x) \vee \cdots \vee \delta_n(x)))\]
Again, the fact that \(F\) is countably incomplete yields an infinite descending chain \(I = I_0 \supseteq I_1 \supseteq I_2 \supseteq \cdots\) of elements in \(F\) such that \(\bigcap_{n \in \mathbb{N}} I_n = \emptyset\). Let \(X_0 = I\), and for each \(n \in \mathbb{N}_{>0}\) define \[X_n = I_n \cap \{i \in I \mid (\mathfrak{M}_i)_{A_i}, \alpha(i) \not\Vdash^{} \forall x( (\gamma_1(x) \wedge \cdots \wedge \gamma_n(x)) \to (\delta_1(x) \vee \cdots \vee \delta_n(x)))\}\] By Łoś’s Theorem 2, the right part of the intersection belongs to \(F\) and hence \(X_n \in F\). Moreover, \(X_n \supseteq X_{n+1}\) and \(\bigcap_{n \in\mathbb{N}} X_n = \emptyset\). Hence for each \(i \in I\) there exists an \(n(i) \in \mathbb{N}\) such that \(n(i)\) is the greatest natural number such that \(i \in X_{n(i)}\), so that there exists an assignment \(\rho_i\) for \(\mathfrak{M}_i\) and some \(a_i \geq \alpha(i)\) in \(W_i\) such that \[(\mathfrak{M}_i)_{A_i}, a_i \not\Vdash^{\rho_i} (\gamma_1(x) \wedge \cdots \wedge \gamma_{n(i)}(x)) \to (\delta_1(x) \vee \cdots \vee \delta_{n(i)}(x))\] Therefore, for every \(i \in I\), there exists some \(b_i \geq_i a_i\) such that \[(\mathfrak{M}_i)_{A_i}, b_i \Vdash^{\rho_i} \langle \{\gamma_1(x),\ldots,\gamma_{n(i)}(x)\}:\{\delta_1(x),\ldots,\delta_{n(i)}(x)\} \rangle.\]
For each \(n \in \mathbb{N}_{>0}\) and \(i \in X_n\) we have \(n \leq n(i)\), hence \((\mathfrak{M}_i)_{A_i}, b_i \Vdash^{\rho_i} \langle \{\gamma_n(x)\}:\{\delta_n(x)\} \rangle\). Since \(X_n \in F\), \[X_n \subseteq \{ i \in I \mid (\mathfrak{M}_i)_{A_i}, b_i \Vdash^{\rho_i} \langle \{\gamma_n(x)\}:\{\delta_n(x)\} \rangle\} \in F\] so using Łoś’s Theorem 2 we obtain \(\prod_{i \in I}^F((\mathfrak{M}_i)_{A_i}), \beta_F \Vdash^{\rho_F} \langle \{\gamma_n(x)\}:\{\delta_n(x)\} \rangle\), where \(\rho\) is the product assignment and \(\beta(i)=b_i\) for every \(i \in I\). Since this holds for every \(n \in \mathbb{N}_{>0}\), we may conclude that \(\prod_{i \in I}^F((\mathfrak{M}_i)_{A_i}), \beta_F \Vdash^{\rho_F} \langle \Gamma(x):\Delta(x) \rangle\) so that \(\langle \Gamma(x):\Delta(x) \rangle\) is separable in \({\uparrow}\alpha_F\). ◻
Theorem 4. Every \(\mathscr{I\!\!L}\)-structure for a countable signature can be elementarily embedded in an \(\omega\)-saturated \(\mathscr{I\!\!L}\)-structure.
Proof. Combine the fact that countably incomplete ultrafilters exist (see Proposition 4.3.5 of [@ChaKei73]) with Propositions [prop:ultra-sat] and [prop:ultra-embedding]. ◻
By now we have developed all ingredients needed to prove the characterisation theorem for \(\mathsf{IK}\). Throughout this section we use the same first-order signature as in Section 3.
Definition 21. A formula \(\varphi(x) \in \mathcal{L}\) with one free variable \(x\) is said to be invariant under IK-bisimulations* if for every pair of \(\mathscr{I\!\!L}\)-structures \(\mathfrak{M} = (W, \leq, \{ \mathfrak{C}_w \}_{w \in W})\) and \(\mathfrak{M}' = (W', \leq', \{ \mathfrak{C}_{w'} \}_{w' \in W'})\), worlds \(w \in W\) and \(w'\in W'\), and individuals \(d \in D_w\) and \(d'\in D_{w'}\), if there exists an IK-bisimulation \(B\) between \(\mathfrak{B}_{\mathfrak{M}}\) and \(\mathfrak{B}_{\mathfrak{M}'}\) linking \((w, d)\) and \((w', d')\), then \[\mathfrak{M}, w \Vdash^{[x \coloneq d]} \varphi(x) \quad\text{iff}\quad\mathfrak{M}', w' \Vdash^{[x \coloneq d']} \varphi(x).\]*
Theorem 5. A formula \(\alpha(x) \in \mathcal{L}\) with one free variable \(x\) is equivalent to the translation of a formula in \(\mathcal{L}_{\Box\Diamond}\) if and only if it is invariant under IK-bisimulations.
Proof. Suppose \(\alpha(x)\) is equivalent to \(\mathop{\mathrm{st}}(x,\psi)\) for some \(\psi \in \mathcal{L}_{\Box\Diamond}\). Let \(\mathfrak{M}\) and \(\mathfrak{M}'\) be two \(\mathscr{I\!\!L}\)-structures and \(Z\) be an IK-bisimulation between \(\mathfrak{B}_{\mathfrak{M}}\) and \(\mathfrak{B}_{\mathfrak{M}'}\) linking \((w, d)\) to \((w', d')\). Then \[\begin{align} \mathfrak{M}, w \Vdash^{[x \coloneq d]} \alpha(x) &\quad\text{iff}\quad\mathfrak{M}, w \Vdash^{[x \coloneq d]} \mathop{\mathrm{st}}(x,\psi) \\ &\quad\text{iff}\quad\mathfrak{B}_{\mathfrak{M}}, (w,d) \Vdash \psi &\text{(by definition and Lemma~\ref{lem:induced-birel})} \\ &\quad\text{iff}\quad\mathfrak{B}_{\mathfrak{M'}}, (w',d') \Vdash \psi &\text{(Proposition~\ref{prop:adeq})} \\ &\quad\text{iff}\quad\mathfrak{M}', w' \Vdash^{[x \coloneq d']} \mathop{\mathrm{st}}(x,\psi) &\text{(by definition and Lemma~\ref{lem:induced-birel})} \\ &\quad\text{iff}\quad\mathfrak{M}', w' \Vdash^{[x \coloneq d']} \alpha(x) \end{align}\] So, \(\alpha\) is invariant under IK-bisimulations.
For the converse, assume that \(\alpha(x)\) is invariant under IK-bisimulations. Consider the set \[\mathrm{MOC}(\alpha) = \{ \mathop{\mathrm{st}}(x,\varphi) \mid \varphi\in \mathcal{L}_{\Box\Diamond} \text{ and } \alpha(x) \models \mathop{\mathrm{st}}(x, \varphi) \}.\] It suffices to show \(\mathrm{MOC}(\alpha) \models \alpha(x)\), because then compactness (Corollary 1) yields a finite subset \(\{ \mathop{\mathrm{st}}(x, \psi_1), \ldots, \mathop{\mathrm{st}}(x, \psi_n) \} \subseteq \mathrm{MOC}(\alpha)\) that has \(\alpha(x)\) as a consequence, from which it follows that \(\alpha(x)\) is equivalent to \(\mathop{\mathrm{st}}(x, \psi_1 \wedge \cdots \wedge \psi_n)\).
Assume \(\mathfrak{M}, w \Vdash^{[x \coloneq d]} \mathrm{MOC}(\alpha)\). We need to show that \(\mathfrak{M}, w \Vdash^{[x \coloneq d]} \alpha(x)\). Let \[\Gamma(x) \coloneq \{ \mathop{\mathrm{st}}(x,\varphi) \mid \mathfrak{M}, w \Vdash^{[x \coloneq d]} \mathop{\mathrm{st}}(x,\varphi) \} \quad\text{and}\quad \Delta(x) \coloneq \{ \mathop{\mathrm{st}}(x,\psi) \mid \mathfrak{M}, w \not\Vdash^{[x \coloneq d]} \mathop{\mathrm{st}}(x,\psi) \}.\] Suppose towards a contradiction that \(\Gamma(x) \cup \{ \alpha(x) \} \models \Delta(x)\). Then Corollary 1 yields finite \(\Gamma_\mathrm{fin}(x) \subseteq \Gamma(x)\) and \(\Delta_\mathrm{fin}(x) \subseteq \Delta(x)\) such that \(\Gamma_\mathrm{fin}(x) \cup \{ \alpha(x) \} \models \Delta_\mathrm{fin}(x)\). This implies \(\alpha(x) \models \bigwedge \Gamma_\mathrm{fin}(x) \to \bigvee \Delta_\mathrm{fin}(x)\), hence \(\bigwedge \Gamma_\mathrm{fin}(x) \to \bigvee \Delta_\mathrm{fin}(x) \in \mathrm{MOC}(\alpha)\). By assumption, \(\mathfrak{M}, w \Vdash^{[x \coloneq d]} \mathrm{MOC}(\alpha)\), so \(\mathfrak{M}, w \Vdash^{[x \coloneq d]} \bigwedge \Gamma_\mathrm{fin}(x) \to \bigvee \Delta_\mathrm{fin}(x)\). But then the fact that \(\mathfrak{M}, w \Vdash^{[x\coloneq d]} \mathop{\mathrm{st}}(x,\psi)\) for all \(\mathop{\mathrm{st}}(x, \psi) \in \Gamma_\mathrm{fin}(x)\) contradicts the fact that \(\mathfrak{M}, w \not\Vdash^{[x \coloneq d]} \mathop{\mathrm{st}}(x, \chi)\) for all \(\mathop{\mathrm{st}}(x, \chi) \in \Delta_\mathrm{fin}(x)\).
So we have \(\Gamma(x) \cup \{ \alpha(x) \} \not\models \Delta(x)\), hence there must exist an \(\mathscr{I\!\!L}\)-structure \(\mathfrak{N} = (V, \leq, \{ \mathfrak{C}_v \}_{v \in V})\), a world \(v \in V\) and an individual \(e \in D_v\) such that \(\mathfrak{N}, v\) separates \(\langle \Gamma(x)\cup\{\alpha(x)\}:\Delta(x) \rangle\) under \([x \coloneq e]\). Then by construction we have \(\mathfrak{M}, w \Vdash^{[x \coloneq d]} \mathop{\mathrm{st}}(x,\varphi)\) if and only if \(\mathfrak{N}, v \Vdash^{[x \coloneq e]} \mathop{\mathrm{st}}(x,\varphi)\) for all \(\varphi\in \mathcal{L}_{\Box\Diamond}\). Proposition [prop:ultra-embedding] gives elementary embeddings of \(\mathfrak{M}\) and \(\mathfrak{N}\) into \(\omega\)-saturated \(\mathscr{I\!\!L}\)-structures \(\mathfrak{M}^*\) and \(\mathfrak{N}^*\), respectively. Hence, for every \(\varphi\in \mathcal{L}_{\Box\Diamond}\) \[\begin{align} \mathfrak{M}^*, w^* \Vdash^{[x \coloneq d^*]} \mathop{\mathrm{st}}(x, \varphi) &\quad\text{iff}\quad\mathfrak{M}, w \Vdash^{[x \coloneq d]} \mathop{\mathrm{st}}(x, \varphi) \\ &\quad\text{iff}\quad\mathfrak{N}, v \Vdash^{[x \coloneq e]} \mathop{\mathrm{st}}(x, \varphi) \quad\text{iff}\quad\mathfrak{N}^*, v^* \Vdash^{[x \coloneq e^*]} \mathop{\mathrm{st}}(x,\varphi). \end{align}\] By Proposition [prop:ind95sat], \(\mathfrak{B}_{\mathfrak{M}^*}\) and \(\mathfrak{B}_{\mathfrak{N}^*}\) are modally saturated birelational models, so that Lemma 3 entails \[\mathfrak{B}_{\mathfrak{M}^*}, (w^*, d^*) \Vdash \varphi \quad\text{iff}\quad\mathfrak{B}_{\mathfrak{N}^*}, (v^*, e^*) \Vdash \varphi\] for all \(\varphi\in \mathcal{L}_{\Box\Diamond}\). Hence, by Theorem 1 there exists an IK-bisimulation \(Z\) between \(\mathfrak{B}_{\mathfrak{M}^*}\) and \(\mathfrak{B}_{\mathfrak{N}^*}\) linking \((w^*, d^*)\) and \((v^*, e^*)\). Since \(\alpha\) is invariant under IK-bisimulations, we conclude that \[\mathfrak{M}, w \Vdash^{[x \coloneq d]} \alpha(x) \quad\text{iff}\quad\mathfrak{M}^*, w^* \Vdash^{[x \coloneq d^*]} \alpha(x) \quad\text{iff}\quad\mathfrak{N}^*, v^* \Vdash^{[x \coloneq e^*]} \alpha(x) \quad\text{iff}\quad\mathfrak{N}, v \Vdash^{[x \coloneq e]} \alpha(x).\] By construction the right-hand side holds, so that ultimately \(\mathfrak{M}, w \Vdash^{[x \coloneq d]} \alpha(x)\), as desired. ◻
Motivated by Van Benthem’s celebrated characterisation theorem, we introduced a precise notion of IK-bisimulation between birelational models and proved that the modal logic \(\mathsf{IK}\) corresponds exactly to the IK-bisimulation-invariant fragment of the intuitionistic first-order logic with one binary predicate and a unary predicate for each propositional letter. En route to this result, we developed intuitionistic counterparts of classical model theory machinery, including an intuitionistic version of Łoś’s Theorem, a compactness theorem and notions of elementary embeddings and countable saturation.
Within the model-theoretic framework, a natural next step is to generalise our results and constructions so as to allow for function symbols in the signature, as well as to weaken the restrictions made on the interpretation of terms, and to expand the theory of saturated models beyond the countable case. Regarding the modal logical framework, obtaining a characterisation theorem for IK relative to classical first-order logic may also be of interest, as well as to further explore the relation between Kripke bisimulations and IK-bisimulations to check whether they yield the same invariance notion.
Finally, it would be worth investigating whether the notion of IK-bisimulation developed here is robust to changes in the chosen intuitionistic modal logic (e.g. \(\mathsf{CK}\) [@BelPaiRit01; @Pai03; @MenPai05], \(\mathsf{WK}\) [@Wij90; @WijNer05], \(\mathsf{FS}\) [@WolterZakharyaschev1999], or other constructive variants), or whether each non-classical variant of \(\mathsf{K}\) needs its own tailored bisimulation.
We elaborate on the definition of the filter product. Proposition [prop:filter-product] follows from Lemmas 4 to 6.
The setup Let \(I\) be a set, and for each \(i \in I\) let \(\mathfrak{M}_i = (W_i, \leq_i, \{ \mathfrak{C}_{i,w} \}_{w \in W_i})\) be an \(\mathscr{I\!\!L}\)-structure, where \(\mathfrak{C}_{i, w} = (D_{i, w}, \mathscr{I}_{i, w})\). Let \(F\) be a filter on \(I\). In what follows, we aim to define the filter product \(\prod_{i \in I}^F \mathfrak{M}_i = (W, {\leq,} \{ \mathfrak{C}_w \}_{w \in W})\).
Step 1: defining \(W\). Let \(W\) be the reduced product \(\prod_{i \in I}^F W_i\). In other words, \(W\) consists of elements in \(\prod_{i \in I} W_i\) modulo the equivalence relation \(\sim\) given by \(\alpha \sim \beta \quad\text{iff}\quad\{ i \in I \mid \alpha(i) = \beta(i) \} \in F\). Elements in \(W\) are denoted by \(\alpha_F\).
Step 2: defining \(\leq\). Define the relation \(\leq\) on \(W\) by \(\alpha_F \leq \beta_F\) iff \(\{ i \in I \mid \alpha(i) \leq_i \beta(i) \} \in F\).
Lemma 4.
The definition of \(\leq\) does not depend on the choice of representative of \(\alpha_F\) and \(\beta_F\).
The relation \(\leq\) defines a partial order on \(W\).
Proof. (1) Suppose \(\alpha \sim \alpha'\) and \(\beta \sim \beta'\). Then \(\{ i \in I \mid \alpha(i) = \alpha'(i) \} \in F\) and \(\{ i \in I \mid \beta(i) = \beta'(i) \} \in F\). Note that \[\{ i \in I \mid \alpha(i) = \alpha'(i) \} \cap \{ i \in I \mid \beta(i) = \beta'(i) \} \cap \{ i \in I \mid \alpha(i) \leq_i \beta(i) \} \subseteq \{ i \in I \mid \alpha'(i) \leq_i \beta'(i) \}.\] Therefore, if \(\{ i \in I \mid \alpha(i) \leq_i \beta(i) \} \in F\), then the fact that \(F\) is a filter, hence closed under intersections and upwards closed, entails \(\{ i \in I \mid \alpha'(i) \leq_i \beta'(i) \} \in F\). This proves that \(\leq\) is well defined.
(2) We need to verify that \(\leq\) is reflexive, antisymmetric and transitive. Reflexivity follows from the fact that \(\{ i \in I \mid \alpha(i) \leq_i \alpha(i) \} = I \in F\). For antisymmetry, suppose \(\alpha_F \leq \beta_F\) and \(\beta_F \leq \alpha_F\). Then \[\{ i \in I \mid \alpha(i) \leq_i \beta(i) \} \cap \{ i \in I \mid \beta(i) \leq_i \alpha(i) \} = \{ i \in I \mid \alpha(i) = \beta(i) \} \in F,\] so \(\alpha \sim \beta\), hence \(\alpha_F = \beta_F\). Lastly, suppose \(\alpha_F \leq \beta_F\) and \(\beta_F \leq \gamma_F\). Then \[\{ i \in I \mid \alpha(i) \leq_i \beta(i) \} \cap \{ i \in I \mid \beta(i) \leq_i \gamma(i) \} \subseteq \{ i \in I \mid \alpha(i) \leq_i \gamma(i) \} \in F,\] so \(\alpha_F \leq \gamma_F\). ◻
Step 3: defining the domains \(D_{\alpha_F}\). For each \(i \in I\), let \(D_i \coloneq D_{\mathfrak{M}_i} = \bigcup_{w \in W_i} D_{i,w}\) be the union of the domains \(D_{i,w}\) of the \(\mathscr{C\!\!L}\)-structures \(\mathfrak{C}_{i,w}\). Define \(D \coloneq \prod_{i \in I}^F D_i\) to be the reduced product of the \(D_i\), that is, \(D\) is equal to the product \(\prod_{i \in I} D_i\) modulo the equivalence relation \(\approx\) given by \(\xi \approx \eta\) iff \(\{ i \in I \mid \xi(i) = \eta(i) \} \in F\). Now we define the domain at \(\alpha_F \in W\) by \[D_{\alpha_F} \coloneq \{ \xi_F \in D \mid \{ i \in I \mid \xi(i) \in D_{i,\alpha(i)} \} \in F \}.\]
Lemma 5.
The definition of \(D_{\alpha_F}\) does not depend on the choice of representative of \(\alpha_F\) or \(\xi_F\).
If \(\alpha_F \leq \beta_F\), then \(D_{\alpha_F} \subseteq D_{\beta_F}\).
\(D = \bigcup_{\alpha_F \in W} D_{\alpha_F}\)
Proof. Suppose \(\alpha \sim \alpha'\) and \(\xi \approx \xi'\), so that \(\{ i \in I \mid \alpha(i) = \alpha'(i) \} \in F\) and \(\{ i \in I \mid \xi(i) = \xi'(i) \} \in F\). We need to show that \(\{ i \in I \mid \xi(i) \in D_{i,\alpha(i)} \} \in F\) if and only if \(\{ i \in I \mid \xi'(i) \in D_{i,\alpha'(i)} \} \in F\). Suppose the former is in \(F\). Then for any \(j\) in the intersection \[\label{eq:D-well-def} \{ i \in I \mid \alpha(i) = \alpha'(i) \} \cap \{ i \in I \mid \xi(i) \in D_{i,\alpha(i)} \} \cap \{ i \in I \mid \xi(i) = \xi'(i) \}\tag{2}\] we have \(\alpha(j) = \alpha'(j)\) and \(\xi(j) = \xi'(j)\) and \(\xi(j) \in D_{j, \alpha(j)}\), which clearly entails \(\xi'(j) \in D_{j, \alpha'(j)}\). Therefore the intersection of 2 is contained in \(\{ i \in I \mid \xi'(i) \in D_{i, \alpha'(i)}\}\). Since filters are upwards closed and closed under finite intersections, we find \(\{ i \in I \mid \xi'(i) \in D_{i,\alpha'(i)}\} \in F\), as desired. The other direction of the “iff” is analogous.
For the second item, suppose \(\alpha_F \leq \beta_F\) and \(\xi_F \in D_{\alpha_F}\). Then \(\{ i \in I \mid \alpha(i) \leq_i \beta(i) \} \in F\) and \(\{ i \in I \mid \xi(i) \in D_{i,\alpha(i)} \} \in F\). Now we note that \[\{ i \in I \mid \alpha(i) \leq_i \beta(i) \} \cap \{ i \in I \mid \xi(i) \in D_{i,\alpha(i)} \} \subseteq \{ i \in I \mid \xi(i) \in D_{i,\beta(i)} \},\] because \(\alpha(i) \leq_i \beta(i)\) implies \(D_{i,\alpha(i)} \subseteq D_{i,\beta(i)}\). Since \(F\) is a filter we find \(\{ i \in I \mid \xi(i) \in D_{i,\beta(i)} \} \in F\), hence \(\xi_F \in D_{\beta_F}\), so that \(D_{\alpha_F} \subseteq D_{\beta_F}\).
For the third item, \(\bigcup_{\alpha_F \in W} D_{\alpha_F} \subseteq D\) follows from the corresponding definition. For the converse, take \(\xi_F \in D\). Thus, \(\xi: I \to \bigcup_{i \in I} D_i\) is such that \(\xi(i) \in D_i=\bigcup_{w \in W_i} D_{i,w}\) for each \(i \in I\) and hence, for each \(i \in I\), there exists a \(w_i \in W_i\) such that \(\xi(i) \in D_{i,w_i}\). Define \(\alpha_\xi : I \to \bigcup_{i \in I} W_i\) by \(\alpha_\xi (i) = w_i \in W_i\). Thus, \[\{ i \in I \mid \xi(i) \in D_{i,\alpha_\xi(i)}\} = I\] and hence \(\xi_F \in D_{{\alpha_\xi}_F}\). ◻
Step 4: defining the constants. Let \(c \in \mathrm{Cnst}\) be a constant symbol. For each \(i \in I\), let \(c_i\) be the interpretation of \(c\) in \(D_i\), and define \(\tilde{c} \in \prod_{i \in I} D_i\) by \[\tilde{c} : I \to \bigcup_{i \in I} D_i : i \mapsto c_i.\] Then, if \(\tilde{c}_F \in D_{\alpha_F}\), we let \(c \in \mathrm{Cnst}_{\alpha_F}\) and define \(\mathscr{I}_{\alpha_F}(c) \coloneq \tilde{c}_F\); otherwise, if \(\tilde{c}_F \notin D_{\alpha_F}\), we let \(c \notin \mathrm{Cnst}_{\alpha_F}\) and we leave \(\mathscr{I}_{\alpha_F}(c)\) undefined. The fact that \(D_{\alpha_F}\) does not depend on the representative of \(\alpha_F\) entails that this is well defined, and by definition it satisfies the requirements from Definition 3.
Step 5: defining the predicates. Finally, we define the interpretations of the predicates on the domains \(D_{\alpha_F}\). For an \(n\)-ary predicate \(P \in \mathrm{Pred}\), set \[(\xi_F^1, \ldots, \xi_F^n) \in \mathscr{I}_{\alpha_F}(P) \quad\text{iff}\quad\{ i \in I \mid (\xi^1(i), \ldots, \xi^n(i)) \in \mathscr{I}_{i, \alpha(i)}(P) \} \in F.\] Then for each \(\alpha_F \in W\) we get a \(\mathscr{C\!\!L}\)-structure \(\mathfrak{C}_{\alpha_F} = (D_{\alpha_F}, \mathscr{I}_{\alpha_F})\).
Lemma 6.
\(\mathscr{I}_{\alpha_F}(P) \subseteq D^n_{\alpha_F}\).
The definition of \(\mathscr{I}_{\alpha_F}(P)\) does not depend on the choice of \(\alpha_F\) or any of the \(\xi^j_F\).
If \(\alpha_F \leq \beta_F\), then \(\mathscr{I}_{\alpha_F}(P) \subseteq \mathscr{I}_{\beta_F}(P)\).
Proof. (1) Suppose \((\xi_F^1, \ldots, \xi_F^n) \in \mathscr{I}_{\alpha_F}(P)\). We aim to show \(\xi_F^j \in D_{\alpha_F}\) for each \(j \in \{ 1, \ldots, n \}\). By assumption, \(\{ i \in I \mid (\xi^1(i), \ldots, \xi^n(i)) \in \mathscr{I}_{i, \alpha(i)}(P) \} \in F\). Since \(\mathscr{I}_{i, \alpha(i)}(P) \subseteq D^n_{i,\alpha(i)}\) for each \(i \in I\), this implies \[\{ i \in I \mid (\xi^1(i), \ldots, \xi^n(i)) \in \mathscr{I}_{i, \alpha(i)}(P) \} \subseteq \{ i \in I \mid \xi^j(i) \in D_{i,\alpha(i)}\},\] so that \(\{ i \in I \mid \xi^j(i) \in D_{i, \alpha(i)} \} \in F\) for each \(j \in \{ 1, \ldots, n \}\). By definition, this implies \(\xi^j_F \in D_{\alpha_F}\).
(2) Suppose \(\alpha \sim \beta\) and \(\xi^j \approx \eta^j\) for all \(j \in \{ 1, \ldots, n \}\). Then \(\{ i \in I \mid \alpha(i) = \beta(i) \} \in F\) and \(\{ i \in I \mid \xi^j(i) = \eta^j(i) \} \in F\) for all \(j \in \{ 1, \ldots, n \}\). We need to show that \[\{i \in I \mid (\xi^1(i), \ldots, \xi^n(i)) \in \mathscr{I}_{i,\alpha(i)}(P) \} \in F \quad\text{iff}\quad \{i \in I \mid (\eta^1(i), \ldots, \eta^n(i)) \in \mathscr{I}_{i,\beta(i)}(P) \} \in F.\] The left-to-right direction follows from the fact that \[\begin{align} \{i \in I &\mid (\xi^1(i), \ldots, \xi^n(i)) \in \mathscr{I}_{i,\alpha(i)}(P) \} \cap \{ i \in I \mid \alpha(i) = \beta(i) \} \\ &\cap \{ i \in I \mid \xi^1(i) = \eta^1(i) \} \cap \cdots \cap \{ i \in I \mid \xi^n(i) = \eta^n(i) \} \subseteq \{i \in I \mid (\eta^1(i), \ldots, \eta^n(i)) \in \mathscr{I}_{i,\beta(i)}(P) \}. \end{align}\] The other direction can be proven analogously. (3) is similar to the proof of Lemma 5. ◻
Suppose \(\rho_i\) is an assignment for \(\mathfrak{M}_i\), for each \(i \in I\). For each \(x \in \mathrm{Var}\), define \(\rho(x) : I \to \bigcup_{i \in I} D_i : i \mapsto \rho_i(x)\). Then the product assignment \(\rho_F\) is given by letting \(\rho_F(x)\) be the equivalence class of \(\rho(x)\), i.e. \(\rho_F(x) \coloneq \rho(x)_F\). Conversely, every assignment \(\rho_F\) for \(\prod_{i \in I}^F\mathfrak{M}_i\) can be obtained in this way from assignments \(\rho_i\) given by \(\rho_i(x) = \rho(x)(i)\).
Theorem 6. Let \(I\) be a set, and for each \(i \in I\) let \(\mathfrak{M}_i\) be a first-order structure and \(\rho_i\) an assignment for \(\mathfrak{M}_i\). Let \(F\) be an ultrafilter on \(I\), \(\mathfrak{M} \coloneq \prod_{i \in I}^F \mathfrak{M}_i\) the filter product, and \(\rho_F\) the product assignment for \(\mathfrak{M}\). Then for any world \(\alpha_F \in W\) and any formula \(\varphi(x_1, \ldots, x_n)\) such that \(\rho_F(x_1), \ldots, \rho_F(x_n) \in D_{\alpha_F}\), \[\mathfrak{M}, \alpha_F \Vdash^{\rho_F} \varphi \quad\text{iff}\quad\{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i} \varphi \} \in F.\]
Proof of Theorem 2. We use induction on the structure of \(\varphi\).
\(\triangleright\;\) Case for \(\varphi= P(t_1, \ldots, t_m)\). Compute \[\begin{align} \mathfrak{M}, \alpha_F \Vdash^{\rho_F} P(t_1, \ldots, t_m) &\quad\text{iff}\quad(\rho^{\mathfrak{M}}_F(t_1), \ldots, \rho^{\mathfrak{M}}_F(t_m)) \in \mathscr{I}_{\alpha_F}(P) &\text{(definition of \Vdash^{\rho_F})} \\ &\quad\text{iff}\quad\{ i \in I \mid (\rho^{\mathfrak{M}}(t_1)(i), \ldots, \rho^{\mathfrak{M}}(t_m)(i)) \in \mathscr{I}_{i, \alpha(i)} \} \in F &\text{(definition of \mathscr{I}_{i, \alpha(i)})} \\ &\quad\text{iff}\quad\{ i \in I \mid (\rho^{\mathfrak{M}_i}_i(t_1), \ldots, \rho^{\mathfrak{M}_i}_i(t_m)) \in \mathscr{I}_{i, \alpha(i)} \} \in F &\text{(definition of \rho_F)} \\ &\quad\text{iff}\quad\{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i} P(t_1, \ldots, t_m) \} \in F &\text{(definition of \Vdash^{\rho_i})} \end{align}\]
\(\triangleright\;\) Case for \(\varphi= (\psi \wedge \chi)\). If \(\mathfrak{M}, \alpha_F \Vdash^{\rho_F} \psi \wedge \chi\), then \(\mathfrak{M}, \alpha_F \Vdash^{\rho_F} \psi\) and \(\mathfrak{M}, \alpha_F \Vdash^{\rho_F} \chi\). By induction, \(\{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i} \psi \} \in F\) and \(\{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i} \chi \} \in F\), and using the fact that \(F\) is a filter we find \[\{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i} \psi \} \cap \{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i} \chi \} \subseteq \{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i} \psi \wedge \chi \} \in F.\]
Conversely, if \(\{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i} \psi \wedge \chi \}\in F\), we may use the fact that \(F\) is a filter to conclude that \[\{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i} \psi \wedge \chi \} \subseteq \{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i} \psi \} \in F,\] and, similarly, we conclude that \(\{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i} \chi \} \in F\). The induction hypothesis then entails \(\mathfrak{M}, \alpha_F \Vdash^{\rho_F} \psi\) and \(\mathfrak{M}, \alpha_F \Vdash^{\rho_F} \chi\), from which it follows that \(\mathfrak{M}, \alpha_F \Vdash^{\rho_F} \psi \wedge \chi\).
\(\triangleright\;\) Case for \(\varphi= (\psi \vee \chi)\). This is similar to the previous case, but using the fact that \(F\) is prime.
\(\triangleright\;\) Case for \(\varphi= (\psi \to \chi)\). Suppose \(\{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i} \psi \to \chi \} \in F\). We show that \(\mathfrak{M}, \alpha_F \Vdash^{\rho_F} \psi \to \chi\). To this end, let \(\alpha_F \leq \beta_F\) and suppose \(\mathfrak{M}, \beta_F \Vdash^{\rho_F} \psi\). Then, using the induction hypothesis, we obtain \[\{ i \in I \mid \alpha(i) \leq_i \beta(i) \} \in F \quad\text{and}\quad \{ i \in I \mid \mathfrak{M}_i, \beta(i) \Vdash^{\rho_i} \psi \} \in F.\] Combining this with the assumption gives \[\begin{align} \{ i \in I \mid \alpha(i) \leq_i \beta(i) \} &\cap \{ i \in I \mid \mathfrak{M}_i, \beta(i) \Vdash^{\rho_i} \psi \} \\ &\cap \{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i} \psi \to \chi \} \subseteq \{ i \in I \mid \mathfrak{M}_i, \beta(i) \Vdash^{\rho_i} \chi \} \in F, \end{align}\] so by the induction hypothesis again we obtain \(\mathfrak{M}, \beta_F \Vdash^{\rho_F} \chi\). Therefore \(\mathfrak{M}, \alpha_F \Vdash^{\rho_F} \psi \to \chi\).
For the converse, suppose \[\begin{align} \{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i} \psi\to\chi \} \notin F \end{align}\] Since \(F\) is an ultrafilter, its complement is an element of \(F\): \[\begin{align} S \coloneq \{ i \in I \mid \mathfrak{M}_i, \alpha(i) \not\Vdash^{\rho_i} \psi\to\chi \} \in F \end{align}\] Hence, for every \(i \in S\), there exists a \(b_i \in W_i\) such that \(\alpha(i) \leq_i b_i\) and \(\mathfrak{M}_i, b_i \Vdash^{\rho_i} \psi\) and \(\mathfrak{M}_i, b_i \not\Vdash^{\rho_i} \chi\). Define \(\beta \in \prod_{i \in I} W_i\) by \[\begin{align} \beta(i) = \begin{cases} b_i &\text{if } i \in S \\ \alpha(i) &\text{if } i \notin S \end{cases} \end{align}\] Then \(\beta_F \in W\) and \(\alpha_F \leq_F \beta_F\) because \(S \subseteq \{ i \in I \mid \alpha(i) \leq_i \beta(i) \}\) and \(S \in F\). Furthermore, \(S \subseteq \{ i \in I \mid \mathfrak{M}_i, \beta(i) \Vdash^{\rho_i} \psi \}\) and \(S \subseteq \{ i \in I \mid \mathfrak{M}_i, \beta(i) \not\Vdash^{\rho_i} \chi \}\), so \[\{ i \in I \mid \mathfrak{M}_i, \beta(i) \Vdash^{\rho_i} \psi \} \in F \quad\text{and}\quad \{ i \in I \mid \mathfrak{M}_i, \beta(i) \not\Vdash^{\rho_i} \chi \} \in F,\] hence \(\{ i \in I \mid \mathfrak{M}_i, \beta(i) \Vdash^{\rho_i} \chi \} \notin F\). The induction hypothesis then yields \(\mathfrak{M}, \beta_F \Vdash^{\rho_F} \psi\) and \(\mathfrak{M}, \beta_F \not\Vdash^{\rho_F} \chi\). Since \(\alpha_F \leq_F \beta_F\), this proves \(\mathfrak{M}, \alpha_F \not\Vdash^{\rho_F} \psi\to\chi\).
\(\triangleright\;\) Case for \(\varphi= \forall x\,\psi\). Suppose that \(\{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i} \forall x\,\psi \} \notin F\). Since \(F\) is an ultrafilter, \[S \coloneq \{ i \in I \mid \mathfrak{M}_i, \alpha(i) \not\Vdash^{\rho_i} \forall x\,\psi\} \in F\] and hence for every \(i \in S\) there exist a world \(b_i \in W_i\) and a domain element \(d_i \in D_{i,b_i}\) such that \(\alpha(i) \leq_i b_i\) and \(\mathfrak{M}_i, b_i \not\Vdash^{\rho_i[x \coloneq d_i]} \psi\). Define \(\beta \in \prod_{i \in I} W_i\) by \[\begin{align} \beta(i) = \begin{cases} b_i &\text{if } i \in S \\ \alpha(i) &\text{if } i \notin S \end{cases} \end{align}\] and \(\xi^d \in \prod_{i \in I} D_i\) by \[\begin{align} \xi^d(i) = \begin{cases} d_i &\text{if } i \in S \\ d^*_i &\text{if } i \notin S, \text{where } d^*_i \text{ is any element of } D_{i,\beta(i)} \end{cases} \end{align}\] Then \(\beta_F \in W\) and \(\xi^d_F \in D_{\beta_F}\), because \(S \subseteq \{ i \in I \mid \xi^d(i) \in D_{i, \alpha(i)} \} \in F\). Since \(S \subseteq \{ i \in I \mid \alpha(i) \leq_i \beta(i) \} \in F\) we have \(\alpha_F \leq_F \beta_F\). Furthermore, by construction we have \[S \subseteq \{ i \in I \mid \mathfrak{M}_i, \beta(i) \not\Vdash^{\rho_i[x \coloneq \xi^d(i)]} \psi \} \in F\] so \(\{ i \in I \mid \mathfrak{M}_i, \beta(i) \Vdash^{\rho_i[x \coloneq \xi^d(i)]} \psi \} \not\in F\). Using the fact that \(\rho_F[x \coloneq \xi^d_F]\) is the product of the assignments \(\rho_i[x \coloneq \xi^d(i)]\) and the induction hypothesis we obtain \(\mathfrak{M}, \beta_F \not\Vdash^{\rho_F[x \coloneq \xi^d_F]} \psi\). Therefore \(\mathfrak{M}, \alpha_F \not\Vdash^{\rho_F} \forall x\, \psi\).
For the converse, suppose that \(\mathfrak{M}, \alpha_F \not\Vdash^{\rho_F} \forall x\, \psi\). Then there exist a world \(\beta_F \in W\) and an individual \(\xi_F \in D_{\beta_F}\) such that \(\alpha_F \leq_F \beta_F\) and \(\mathfrak{M}, \beta_F \not\Vdash^{\rho_F[x \coloneq \xi_F]} \psi\). This implies \(\{ i \in I \mid \alpha(i) \leq_i \beta(i) \} \in F\) and \(\{ i \in I \mid \xi(i) \in D_{i,\beta(i)}\} \in F\) and (by the induction hypothesis) \(\{ i \in I \mid \mathfrak{M}_i, \beta(i) \Vdash^{\rho_i[x \coloneq \xi(i)]} \psi \} \notin F\). Since \(F\) is an ultrafilter, we get \(\{ i \in I \mid \mathfrak{M}_i, \beta(i) \not\Vdash^{\rho_i[x \coloneq \xi(i)]} \psi \} \in F\). It follows that \[\begin{align} \{ i \in I \mid \alpha(i) \leq_i \beta(i) \} &\cap \{ i \in I \mid \xi(i) \in D_{i,\beta(i)} \} \\ &\cap \{ i \in I \mid \mathfrak{M}_i, \beta(i) \not\Vdash^{\rho_i[x \coloneq \xi(i)]} \psi \} \subseteq \{ i \in I \mid \mathfrak{M}_i, \alpha(i) \not\Vdash^{\rho_i} \forall x\,\psi\} \in F \end{align}\] and hence \(\{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i} \forall x\,\psi \} \notin F\).
\(\triangleright\;\) Case for \(\varphi= \exists x\,\psi\). Suppose \(\mathfrak{M}, \alpha_F \Vdash^{\rho_F} \exists x\,\psi\). Then there exists some individual \(\xi_F \in D_{\alpha_F}\) such that \(\mathfrak{M}, \alpha_F \Vdash^{\rho_F[x \coloneq \xi_F]} \psi\). By the induction hypothesis, and using the fact that \(\rho_F[x \coloneq \xi_F]\) is the product of the assignments \(\rho_i[x \coloneq \xi(i)]\), we obtain \(\{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i[x \coloneq \xi(i)]} \psi \} \in F\). Clearly \[\begin{align} \{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i[x \coloneq \xi(i)]} \psi\} \subseteq \{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i} \exists x\,\psi \}, \end{align}\] so \(\{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i} \exists x\, \psi \} \in F\).
Now suppose \(S \coloneq \{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i} \exists x\,\psi\} \in F\). Then, for every \(i \in S\) there exists a \(d_i \in D_{i,\alpha(i)}\) such that \(\mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i[x \coloneq d_i]} \psi\). Define \(\xi^d \in \prod_{i \in I} D_i\) by \[\xi^d(i) = \begin{cases} d_i &\text{if } i \in S \\ d^*_i &\text{if } i \not\in S, \text{where } d^*_i \text{ is any element of } D_{i,\alpha(i)} \end{cases}\] Then \(\xi^d_F \in D_{\alpha_F}\) and \[S \subseteq \{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i[x \coloneq \xi^d(i)]} \psi \},\] so \(\{ i \in I \mid \mathfrak{M}_i, \alpha(i) \Vdash^{\rho_i[x \coloneq \xi^d(i)]} \psi \} \in F\) and by the induction hypothesis \(\mathfrak{M}, \alpha_F \Vdash^{\rho_F[x \coloneq \xi^d_F]} \psi\). ◻