Proof. First, item 1 implies item 2 by the soundness of \(\mathsf{H}(\Lambda)\), which can be established straightforwardly. Moreover, item 2 implies item 3 since \(\mathbb{F}_{\Lambda}\) can be regarded as a subclass of \(\mathbb{P}_{\Lambda}\). So it remains to show that item 3 implies item 1, which is a result already established in the literature. A proof sketch for \(\mathsf{H}(\mathbf{K}_{D})\) and \(\mathsf{H}(\mathbf{K45}_{D})\) can be found in [@Fagin_2003_Reasoning] and [@Gerbrandy_1999_bisimulations], respectively. Detailed proofs are provided in [@Agotnes_2021_group] for \(\mathsf{H}(\mathbf{KD45}_{D})\) and in [@Wang_2013_publica] for \(\mathsf{H}(\mathbf{S5}_{D})\). ◻

Proof. By induction on the height of the derivation \(\mathcal{D}\) to obtain \(\Gamma \Rightarrow \Delta\). For base step, our goal is immediate. For inductive step, we divide the argument depending on the last rule applied. We only comment on the case of \((\Rightarrow D^{\mathbf{K45}_{D}})\) for \(\mathsf{G}(\mathbf{K45}_{D})\): \[\infer[(\Rightarrow D^{\mathbf{K45}_{D}})]{D_{G_{1}}\varphi_{1},\dots,D_{G_{m}}\varphi_{m}\Rightarrow D_{H_{1}}\psi_{1},\dots,D_{H_{n}}\psi_{n}, D_{G}\chi}{\varphi_{1},\dots,\varphi_{m},D_{G_{1}}\varphi_{1},\dots,D_{G_{m}}\varphi_{m}\Rightarrow D_{H_{1}}\psi_{1},\dots,D_{H_{n}}\psi_{n},\chi},\] where \(\bigcup^{m}_{i=1}G_{i}\cup\bigcup^{n}_{j=1}H_{j}\subseteq G\). Our goal is to show \(\mathbb{F}_{\mathbf{K45}_{D}}\models\bigwedge_{i=1}^{m}D_{G_{i}}\varphi_{i}\to\bigvee^{n}_{j=1}D_{H_{j}}\psi_{j}\lor D_{G}\chi\). Fix any model \(M\) from \(\mathbb{F}_{\mathbf{K45}_{D}}\) and any \(w\in W\). Suppose \(M,w\models \bigwedge_{i=1}^{m}D_{G_{i}}\varphi_{i}\). We show that \(M,w\models\bigvee^{n}_{j=1}D_{H_{j}}\psi_{j}\lor D_{G}\chi\). Suppose \(M,w\not\models\bigvee^{n}_{j=1}D_{H_{j}}\psi_{j}\) and we show that \(M,w\models D_{G}\chi\). Fix any \(v\in W\) such that \((w,v)\in \bigcap_{a\in G}R_{a}\). It suffices to show that \(M,v\models\chi\). By induction hypothesis, we obtain \(\mathbb{F}_{\mathbf{K45}_{D}}\models\bigwedge_{i=1}^{m}\varphi_{i}\land\bigwedge_{i=1}^{m}D_{G_{i}}\varphi_{i}\to\bigvee^{n}_{j=1}D_{H_{j}}\psi_{j}\lor\chi\). Since \(G_{i}\subseteq G\), \((w,v)\in\bigcap_{a\in G}R_{a}\subseteq \bigcap_{b\in G_{i}}R_{b}\). Hence \(M,v\models\bigwedge_{i=1}^{m}\varphi_{i}\) by our assumption \(M,w\models \bigwedge_{i=1}^{m}D_{G_{i}}\varphi_{i}\). Moreover by transitivity we obtain \(\mathbb{F}_{\mathbf{K45}_{D}}\models\bigwedge_{i=1}^{m}D_{G_{i}}\varphi_{i}\), since for every \(u\in W\) such that \((v,u)\in\bigcap_{b\in G_{i}}R_{b}\), \((w,u)\in\bigcap_{b\in G_{i}}R_{b}\). Therefore \(M,v\models\bigvee^{n}_{j=1}D_{H_{j}}\psi_{j}\lor\chi\). For our goal, it suffices to show \(M,v\not\models\bigvee^{n}_{j=1}D_{H_{j}}\psi_{j}\). By \(M,w\not\models\bigvee^{n}_{j=1}D_{H_{j}}\psi_{j}\), there exists a state \(u_{j}\in W\) for every \(1\le j\le n\) such that \((w,u_{j})\in\bigcap_{c\in H_{j}}R_{c}\) and \(M,u_{j}\not\models\psi_{j}\). Then by Euclideanness, we obtain \((v,u_{j})\in\bigcap_{c\in H_{j}}R_{c}\), which implies our goal \(M,v\not\models\bigvee^{n}_{j=1}D_{H_{j}}\psi_{j}\) together with \(M,u_{j}\not\models\psi_{j}\). ◻

Proof. We note that \((Cut)\) is necessary to simulate \((\mathtt{MP})\). We only check the derivability of \((\mathtt{Incl})\) in each system. Suppose \(G \subseteq H\). For \(\Lambda \in \{\mathbf{K45}_{D}, \mathbf{KD45}_{D}, \mathbf{S5}_{D}\}\), the following derivations (left for \(\mathbf{K45}_{D}, \mathbf{KD45}_{D}\) and right for \(\mathbf{S5}_{D}\)) witness \((\mathtt{Incl})\), where the side conditions are satisfied by the assumption \(G \subseteq H\). \[\infer[(\Rightarrow\to)]{\Rightarrow D_{G}\varphi\to D_{H}\varphi}{\infer[(\Rightarrow D^{\mathbf{K45}_{D}})]{D_{G}\varphi\Rightarrow D_{H}\varphi}{\infer[(w\Rightarrow)]{\varphi, D_{G}\varphi\Rightarrow \varphi}{\varphi\Rightarrow\varphi}}} \quad \infer[(\Rightarrow\to)]{\Rightarrow D_{G}\varphi\to D_{H}\varphi}{\infer[(\Rightarrow D^{\mathbf{S5}_{D}})]{D_{G}\varphi\Rightarrow D_{H}\varphi}{\infer[(D\Rightarrow)]{D_{G}\varphi\Rightarrow \varphi}{\varphi\Rightarrow\varphi}}}. \qedhere\] ◻

Proof. Let \(\varphi^{m}\) denote \(m\) occurrences of \(\varphi\). We comment on the case where \(\Lambda=\mathbf{KD45}_{D}\). We can prove the following statements by simultaneous induction on \(\mathcal{D}\) of \(\mathsf{G}^{-}(\mathbf{KD45}_{D})\).

1. \(\forall m,n,l\in \mathbb{N}\;(\mathtt{root}(\mathcal{D}) \not\equiv\;\Rightarrow (D_{\{a\}}\neg D_{\{a\}}p)^{m}, (D_{\{a,b\}}p)^{n},p^{l})\),

2. \(\forall x_{1},x_{2},y,z\in \mathbb{N}\;(\mathtt{root}(\mathcal{D}) \not\equiv p^{x_{1}},(D_{\{a\}}p)^{x_{2}}\Rightarrow (D_{\{a\}}\neg D_{\{a\}}p)^{y},(\neg D_{\{a\}}p)^{z})\).

Then the statement of the lemma is a special case of (1) where \(m = n = 1\) and \(l\) = \(0\). ◻

Proof. Let \(\varphi_{1},\dots,\varphi_{m}\) be an enumeration of all formulas in \(\mathsf{Sub}(\Gamma,\Delta)\). In what follows we inductively construct a sequence \((\Gamma_{k},\Delta_{k})(1\le k\le m)\) such that \(\mathsf{G}^{\mathtt{a}}(\Lambda)\not\vdash\Gamma_{k}\Rightarrow\Delta_{k}\), \(\Gamma_{k}\subseteq\Gamma_{k+1}\) and \(\Delta_{k}\subseteq\Delta_{k+1}\) for all \(1\le k\le m\). For base step, let \((\Gamma_{0},\Delta_{0}):=(\Gamma,\Delta)\). It is clear that \(\mathsf{G}^{\mathtt{a}}(\Lambda)\not\vdash\Gamma\Rightarrow\Delta\). For inductive step, we define \((\Gamma_{k+1},\Delta_{k+1})\) as follows: \[\begin{cases} \Gamma_{k+1}=\Gamma_{k}\text{ and }\Delta_{k+1}=\Delta_{k}\cup\{\varphi_{k}\} &\text{if }\mathsf{G}^{\mathtt{a}}(\Lambda)\not\vdash\Gamma_{k}\Rightarrow\Delta_{k},\varphi_{k}\\ \Gamma_{k+1}=\Gamma_{k}\cup\{\varphi_{k}\}\text{ and }\Delta_{k+1}=\Delta_{k} &\text{otherwise} \end{cases}\] Moreover, it is not the case that \(\mathsf{G}^{\mathtt{a}}(\Lambda)\vdash\Gamma_{k}\Rightarrow\Delta_{k},\varphi_{k}\) and \(\mathsf{G}^{\mathtt{a}}(\Lambda)\vdash\varphi_{k}, \Gamma_{k}\Rightarrow\Delta_{k}\). Suppose it is the case for contradiction. Then we can derive \(\Gamma_{k}\Rightarrow\Delta_{k}\) by \[\infer=[(w)]{\Gamma_{k}\Rightarrow\Delta_{k}}{\infer[(Cut)^{\mathtt{a}}_{\varphi_{k}}]{\Gamma_{k},\Gamma_{k}\Rightarrow\Delta_{k},\Delta_{k}}{\Gamma_{k}\Rightarrow\Delta_{k},\varphi_{k} & \varphi_{k}, \Gamma_{k}\Rightarrow\Delta_{k}}},\] where \(\varphi_{k}\in\mathsf{Sub}(\Gamma_{k},\Delta_{k})\) holds clearly since \(\varphi_{k}\in\mathsf{Sub}(\Gamma,\Delta)\) and \(\Gamma\subseteq\Gamma_{k}\), \(\Delta\subseteq\Delta_{k}\). Hence we have \(\mathsf{G}^{\mathtt{a}}(\Lambda)\vdash\Gamma_{k}\Rightarrow\Delta_{k}\), which contradicts the induction hypothesis. Therefore, either \(\Gamma_{k}\Rightarrow\Delta_{k},\varphi_{k}\) or \(\varphi_{k}, \Gamma_{k}\Rightarrow\Delta_{k}\) is underivable in \(\mathsf{G}^{\mathtt{a}}(\Lambda)\). Finally, let \((\Gamma^{+},\Delta^{+}):=(\Gamma_{m+1},\Delta_{m+1})\). It holds clearly that \(\mathsf{Sub}(\Gamma,\Delta)=\mathsf{Sub}(\Gamma^{+},\Delta^{+})=\Gamma^{+}\cup\Delta^{+}\). Moreover \(\Gamma\subseteq\Gamma^{+}\), \(\Delta\subseteq\Delta^{+}\) and \(\mathsf{G}^{\mathtt{a}}(\Lambda)\not\vdash\Gamma^{+}\Rightarrow\Delta^{+}\) by our definition. ◻

Proof.

1. Fix any \(G,H\in\mathsf{Grp}\) such that \(G\subseteq H\). Since \(R^{\mathbf{KD45}_{D}}_{G}:=R^{\mathbf{K45}_{D}}_{G}\), we only comment on the cases where \((\Lambda =\mathbf{K45}_{D})\) and \((\Lambda =\mathbf{S5}_{D})\).

   • Let \(\Lambda =\mathbf{K45}_{D}\). Fix any \((\Gamma,\Delta)\), \((\Pi,\Sigma)\in W^{\Lambda}_{\Xi}\) such that \((\Gamma,\Delta)R^{\mathbf{K45}_{D}}_{H}(\Pi,\Sigma)\). We show that \((\Gamma,\Delta)R^{\mathbf{K45}_{D}}_{G}(\Pi,\Sigma)\). Fix any \(I\subseteq G\). It suffices to show (i) \(\left\{\, {\varphi,D_{I}\varphi} \,|\, {D_{I}\varphi\in\Gamma} \,\right\}\subseteq\Pi\) and (ii) \(\left\{\, {D_{I}\varphi} \,|\, {D_{I}\varphi\in\Pi} \,\right\}\subseteq\Gamma\). By assumption, \(I\subseteq G\subseteq H\), hence our goal follows from \[(\Gamma,\Delta)R^{\mathbf{K45}_{D}}_{H}(\Pi,\Sigma).\]

   • Let \(\Lambda =\mathbf{S5}_{D}\). Fix any \((\Gamma,\Delta)\), \((\Pi,\Sigma)\in W^{\Lambda}_{\Xi}\) such that \((\Gamma,\Delta)R^{\mathbf{S5}_{D}}_{H}(\Pi,\Sigma)\). We show that \((\Gamma,\Delta)R^{\mathbf{S5}_{D}}_{G}(\Pi,\Sigma)\). Fix any \(I\subseteq G\). It suffices to show \(\left\{\, {D_{I}\varphi} \,|\, {D_{I}\varphi\in\Gamma} \,\right\}=\left\{\, {D_{I}\varphi} \,|\, {D_{I}\varphi\in\Pi} \,\right\}\). By assumption, \(I\subseteq G\subseteq H\), hence our goal follows from \((\Gamma,\Delta)R^{\mathbf{S5}_{D}}_{H}(\Pi,\Sigma)\).

2. • Let \(\Lambda =\mathbf{K45}_{D}\). We show that \(R^{\mathbf{K45}_{D}}_{G}\) is transitive and Euclidean.

     Fix any \((\Gamma,\Delta)\), \((\Pi,\Sigma)\), \((\Theta,\Omega)\in W^{\mathbf{K45}_{D}}_{\Xi}\). Suppose \[(\Gamma,\Delta)R^{\mathbf{K45}_{D}}_{G}(\Pi,\Sigma)\text{ and } (\Pi,\Sigma)R^{\mathbf{K45}_{D}}_{G}(\Theta,\Omega).\] We show \((\Gamma,\Delta)R^{\mathbf{K45}_{D}}_{G}(\Theta,\Omega)\). Fix any \(H\subseteq G\). It suffices to show (i) \(\left\{\, {\varphi,D_{H}\varphi} \,|\, {D_{H}\varphi\in\Gamma} \,\right\}\subseteq\Theta\) and (ii) \(\left\{\, {D_{H}\varphi} \,|\, {D_{H}\varphi\in\Theta} \,\right\}\subseteq\Gamma\). First, we show (i). Let us fix any \(D_{H}\psi\in\Gamma\). We show \(\psi,D_{H}\psi\in\Theta\). By assumption, \(\left\{\, {\varphi,D_{H}\varphi} \,|\, {D_{H}\varphi\in\Gamma} \,\right\}\subseteq\Pi\). Then we have \(D_{H}\psi\in\Pi\). Again by assumption, \(\left\{\, {\varphi,D_{H}\varphi} \,|\, {D_{H}\varphi\in\Pi} \,\right\}\subseteq\Theta\). Therefore our goal of \(\psi,D_{H}\psi\in\Theta\) follows from \(D_{H}\psi\in\Pi\).

     Second, we move to (ii). By assumption we have \[\left\{\, {D_{H}\varphi} \,|\, {D_{H}\varphi\in\Theta} \,\right\}\subseteq\Pi\text{ and }\left\{\, {D_{H}\varphi} \,|\, {D_{H}\varphi\in\Pi} \,\right\}\subseteq\Gamma,\] which implies our goal \(\left\{\, {D_{H}\varphi} \,|\, {D_{H}\varphi\in\Theta} \,\right\}\subseteq\Gamma\).

     Fix any \((\Gamma,\Delta)\), \((\Pi,\Sigma)\), \((\Theta,\Omega)\in W^{\mathbf{K45}_{D}}_{\Xi}\). Suppose \((\Gamma,\Delta)R^{\mathbf{K45}_{D}}_{G}(\Pi,\Sigma)\) and \((\Gamma,\Delta)R^{\mathbf{K45}_{D}}_{G}(\Theta,\Omega)\). We show \((\Pi,\Sigma)R^{\mathbf{K45}_{D}}_{G}(\Theta,\Omega)\). Fix any \(H\subseteq G\). It suffices to show (i) \(\left\{\, {\varphi,D_{H}\varphi} \,|\, {D_{H}\varphi\in\Pi} \,\right\}\subseteq\Theta\) and (ii) \(\left\{\, {D_{H}\varphi} \,|\, {D_{H}\varphi\in\Theta} \,\right\}\subseteq\Pi\).

     First, we establish (i). Fix any \(D_{H}\psi\in\Pi\). We show that \(\psi,D_{H}\psi\in\Theta\). By \((\Gamma,\Delta)R^{\mathbf{K45}_{D}}_{G}(\Pi,\Sigma)\) we have \(D_{H}\psi\in\Gamma\). Then our goal holds by \((\Gamma,\Delta)R^{\mathbf{K45}_{D}}_{G}(\Theta,\Omega)\).

     Second, we move to (ii). Fix any \(D_{H}\psi\) with \(D_{H}\psi\in\Theta\). We show that \(D_{H}\psi\in\Pi\). By \((\Gamma,\Delta)R^{\mathbf{K45}_{D}}_{G}(\Theta,\Omega)\), we have \(D_{H}\psi\in\Gamma\). Then our goal holds by \((\Gamma,\Delta)R^{\mathbf{K45}_{D}}_{G}(\Pi,\Sigma)\).

     We prove the seriality of \(R_{\{a\}}^{\mathbf{KD45}_{D}}\). Fix any \((\Gamma,\Delta)\in W^{\mathbf{KD45}_{D}}_{\Xi}\). We show that there exists \((\Pi,\Sigma)\in W^{\mathbf{KD45}_{D}}_{\Xi}\) such that \((\Gamma,\Delta)R^{\mathbf{KD45}_{D}}_{\{a\}}(\Pi,\Sigma)\). We define \(\Pi:=\left\{\, {\varphi} \,|\, {D_{\{a\}}\varphi\in\Gamma} \,\right\}\), \(\Sigma:=\left\{\, {D_{\{a\}}\psi} \,|\, {D_{\{a\}}\psi\in\Delta} \,\right\}\). Then \(\Pi,D_{\{a\}}\Pi\Rightarrow\Sigma\) is underivable in \(\mathsf{G}^{\mathtt{a}}(\mathbf{KD45}_{D})\). Otherwise \(\Gamma\Rightarrow\Delta\) is derivable from \(\Pi,D_{\{a\}}\Pi\Rightarrow\Sigma\) via \((D^{\mathbf{KD45}_D})\) and weakening rules, which contradicts \(\mathsf{G}^{\mathtt{a}}(\Lambda)\not\vdash\Gamma\Rightarrow\Delta\). By Lemma 1, there exists \((\Pi^{+},\Sigma^{+})\in W^{\mathbf{KD45}_{D}}_{\Xi}\) such that \(\Pi\cup D_{\{a\}}\Pi\subseteq\Pi^{+}\), \(\Sigma\subseteq\Sigma^{+}\) and \(\mathsf{Sub}(\Pi,D_{\{a\}}\Pi,\Sigma)=\Pi^{+}\cup\Sigma^{+}\). Then it suffices to show \((\Gamma,\Delta)R^{\mathbf{KD45}_{D}}_{\{a\}}(\Pi^{+},\Sigma^{+})\). Fix any \(D_{\{a\}}\chi\in\Xi\). First, we suppose \(D_{\{a\}}\chi\in\Gamma\). We show that \(\chi, D_{\{a\}}\chi\in\Pi^{+}\). Then \(\chi\in\Pi\subseteq\Pi^{+}\). Moreover \(D_{\{a\}}\chi\in D_{\{a\}}\Pi\subseteq\Pi^{+}\). Therefore, our goal \(\chi\in\Pi^{+}\) and \(D_{\{a\}}\chi\in\Pi^{+}\) holds. Second, we suppose \(D_{\{a\}}\chi\in\Pi\). Our goal is to show \(D_{\{a\}}\chi\in\Gamma\). Suppose \(D_{\{a\}}\chi\notin\Gamma\) for contradiction. By \(D_{\{a\}}\chi\in\Pi\), \(D_{\{a\}}\chi\in\Pi^{+}\cup\Sigma^{+}=\mathsf{Sub}(\Pi,D_{\{a\}}\Pi, \Sigma)\subseteq\mathsf{Sub}(\Gamma,\Delta)=\Gamma\cup\Delta\). Since \(D_{\{a\}}\chi\notin\Gamma\), we have \(D_{\{a\}}\chi\in\Delta\), i.e., \(D_{\{a\}}\chi\in\Sigma\subseteq\Sigma^{+}\). Then \(\Pi^{+}\Rightarrow\Sigma^{+}\) is derivable from \(D_{\{a\}}\chi\Rightarrow D_{\{a\}}\chi\) by weakening rules, which is contradicted to \((\Pi^{+},\Sigma^{+})\) being a \(\Xi\)-partial valuation. Therefore, our goal \(D_{\{a\}}\chi\in\Gamma\) holds.

   • Let \(\Lambda\) = \(\mathbf{S5}_{D}\). We show that \(R^{\mathbf{S5}_{D}}_{G}\) is reflexive, symmetric and transitive. Fix any \((\Gamma,\Delta)\), \((\Pi,\Sigma)\), \((\Theta,\Omega)\in W^{\mathbf{S5}_{D}}_{\Xi}\). First, we show that \((\Gamma,\Delta)R^{\mathbf{S5}_{D}}_{G}(\Gamma,\Delta)\), which holds clearly by \[\left\{\, {D_{H}\varphi} \,|\, {D_{H}\varphi\in\Gamma} \,\right\}=\left\{\, {D_{H}\varphi} \,|\, {D_{H}\varphi\in\Gamma} \,\right\}.\] Second, suppose \((\Gamma,\Delta)R^{\mathbf{S5}_{D}}_{G}(\Pi,\Sigma)\). We show that \((\Pi,\Sigma)R^{\mathbf{S5}_{D}}_{G}(\Gamma,\Delta)\). It suffices to show that \(\left\{\, {D_{H}\varphi} \,|\, {D_{H}\varphi\in\Pi} \,\right\}=\left\{\, {D_{H}\varphi} \,|\, {D_{H}\varphi\in\Gamma} \,\right\}\), which follows from our assumption \[(\Gamma,\Delta)R^{\mathbf{S5}_{D}}_{G}(\Pi,\Sigma),\] i.e., \(\left\{\, {D_{H}\varphi} \,|\, {D_{H}\varphi\in\Gamma} \,\right\}=\left\{\, {D_{H}\varphi} \,|\, {D_{H}\varphi\in\Pi} \,\right\}\). Finally, suppose \[(\Gamma,\Delta)R^{\mathbf{S5}_{D}}_{G}(\Pi,\Sigma)\text{ and }(\Pi,\Sigma)R^{\mathbf{S5}_{D}}_{G}(\Theta,\Omega).\] We show \((\Gamma,\Delta)R^{\mathbf{S5}_{D}}_{G}(\Theta,\Omega)\). Fix any \(H\subseteq G\). It suffices to show \(\left\{\, {D_{H}\varphi} \,|\, {D_{H}\varphi\in\Gamma} \,\right\}=\left\{\, {D_{H}\varphi} \,|\, {D_{H}\varphi\in\Theta} \,\right\}\). By assumption, we have \(\left\{\, {D_{H}\varphi} \,|\, {D_{H}\varphi\in\Gamma} \,\right\}=\left\{\, {D_{H}\varphi} \,|\, {D_{H}\varphi\in\Pi} \,\right\}\) and \(\left\{\, {D_{H}\varphi} \,|\, {D_{H}\varphi\in\Pi} \,\right\}=\left\{\, {D_{H}\varphi} \,|\, {D_{H}\varphi\in\Theta} \,\right\}\). Therefore, our goal holds.

 ◻

Proof. We comment on item (\(D\)) for \(\mathbf{K45}_{D}\) and \(\mathbf{S5}_{D}\), because the other conditions are established easily (cf.  [@Udatsu_2025_craig]).

• Let \(\Lambda=\mathbf{K45}_{D}\). Suppose \(D_{G}\varphi\in\Delta\). Define \(\Pi:=\left\{\, {\psi,D_{H}\psi} \,|\, {D_{H}\psi\in\Gamma \text{ and }H\subseteq G} \,\right\}\) and
  \(\Sigma:=\left\{\, {D_{I}\gamma} \,|\, {D_{I}\gamma\in\Delta\text{ and }I\subseteq G} \,\right\}\). It follows that \(\Pi\Rightarrow \Sigma,\varphi\) is underivable in \(\mathsf{G}^{\mathtt{a}}(\mathbf{K45}_{D})\). Suppose not. Then we obtain the following: \[\infer[(\Rightarrow D^{\mathbf{K45}_{D}})]{\Pi'\Rightarrow \Sigma,D_{G}\varphi}{\Pi\Rightarrow \Sigma,\varphi},\] where \(\Pi'= \bigcup_{H \subseteq G}\left\{\, {D_{H}\psi} \,|\, {D_{H}\psi\in\Gamma} \,\right\}\), which is contradicted to \((\Gamma,\Delta)\) being a \(\Xi\)-partial valuation by weakening rules. So, \(\mathsf{G}^{\mathtt{a}}(\mathbf{K45}_{D})\not\vdash\Pi\Rightarrow \Sigma,\varphi\). By Lemma 1, there exists a \(\Xi\)-partial valuation \((\Pi^{+},\Sigma^{+})\) such that \(\Pi\subseteq\Pi^{+}\), \(\Sigma\cup\{\varphi\}\subseteq\Sigma^{+}\) and \(\mathsf{Sub}(\Pi, \Sigma,\varphi)=\Pi^{+}\cup\Sigma^{+}\). Then it suffices to show \((\Gamma,\Delta)R_{G}^{\mathbf{K45}_{D}}(\Pi^{+},\Sigma^{+})\), which can be proved similarly to the proof of Proposition [prop:well32definiability32D] (2).

• Let \(\Lambda=\mathbf{S5}_{D}\). Suppose \(D_{G}\varphi\in\Delta\). Let \(\Pi\) and \(\Sigma\) be defined as: \[\Pi:=\left\{\, {D_{H}\psi} \,|\, {D_{H}\psi\in\Gamma \text{ and }H\subseteq G} \,\right\}\quad \Sigma:=\left\{\, {D_{I}\gamma} \,|\, {D_{I}\gamma\in\Delta\text{ and }I\subseteq G} \,\right\}.\] It follows that \(\Pi\Rightarrow\Sigma,\varphi\) is underivable in \(\mathsf{G}^{\mathtt{a}}(\mathbf{S5}_{D})\), otherwise \(\Gamma\Rightarrow\Delta\) is derivable by \((\Rightarrow D^{\mathbf{S5}_{D}})\) and weakening rules. Then by Lemma 1, there exists a \(\Xi\)-partial valuation \((\Pi^{+},\Sigma^{+})\) such that \(\Pi\subseteq\Pi^{+}\), \(\Sigma\cup\{\varphi\}\subseteq\Sigma^{+}\) and \(\mathsf{Sub}(\Pi, \Sigma,\varphi)=\Pi^{+}\cup\Sigma^{+}\). Then it suffices to show \((\Gamma,\Delta)R_{G}^{\mathbf{S5}_{D}}(\Pi^{+},\Sigma^{+})\). Fix any \(C\subseteq G\) and \(\chi\in\Xi\). We show that \(D_{C}\chi\in\Gamma\) iff \(D_{C}\chi\in\Pi^{+}\). (\(\Rightarrow\)) Suppose \(D_{C}\chi\in\Gamma\). By definition of \(\Pi\), \(D_{C}\chi\in\Pi\). Therefore our goal \(D_{C}\chi\in\Pi^{+}\) holds by \(\Pi\subseteq\Pi^{+}\). (\(\Leftarrow\)) Suppose \(D_{C}\chi\in\Pi^{+}\). Then \(D_{C}\chi\in\Pi^{+}\cup\Sigma^{+}=\mathsf{Sub}(\Pi,\Sigma,\varphi)\subseteq\mathsf{Sub}(\Gamma,\Delta)=\Gamma\cup\Delta\). Our goal is to show that \(D_{C}\chi\in\Gamma\). Suppose not. Then \(D_{C}\chi\in\Delta\), i.e., \(D_{C}\chi\in\Sigma\subseteq\Sigma^{+}\). Then \(\Pi^{+}\Rightarrow\Sigma^{+}\) is derivable from \(D_{C}\varphi\Rightarrow D_{C}\varphi\). Therefore our goal \(D_{C}\chi\in\Gamma\) holds.

 ◻

Proof. By induction on \(\varphi\). We comment on the case where \(\varphi\equiv D_{G}\psi\).

1. Suppose \(D_{G}\psi\in\Gamma\). We show that \(M^{\Lambda}_{\Xi},(\Gamma,\Delta)\models D_{G}\psi\). Fix any \((\Pi,\Sigma)\in W^{\Lambda}_{\Xi}\) and suppose \[(\Gamma,\Delta)R_{G}^{\Lambda}(\Pi,\Sigma).\] We show that \(M^{\Lambda}_{\Xi},(\Pi,\Sigma)\models\psi\). We comment on the case for \(\mathbf{K45}_{D}\) and \(\mathbf{S5}_{D}\).

   • \((\mathbf{K45}_{D})\) We show \(M^{\mathbf{K45}_{D}}_{\Xi},(\Pi,\Sigma)\models\psi\). By induction hypothesis, it suffices to show \(\psi\in\Pi\), which follows from Definition 8 and \(D_{G}\psi\in\Gamma\).

   • \((\mathbf{S5}_{D})\) We show \(M^{\mathbf{S5}_{D}}_{\Xi},(\Gamma,\Delta)\models D_{G}\psi\). Fix any \((\Pi,\Sigma)\in W^{\mathbf{S5}_{D}}_{\Xi}\) and suppose \((\Gamma,\Delta)R_{G}^{\mathbf{S5}_{D}}(\Pi,\Sigma)\). Then \(D_{G}\psi\in\Gamma\) implies \(D_{G}\psi\in\Pi\). Then \(\psi\in\mathsf{Sub}(D_{G}\psi)\subseteq\mathsf{Sub}(\Pi,\Sigma)=\Pi\cup\Sigma\). If \(\psi\in\Pi\), our goal \(M^{\mathbf{K45}_{D}}_{\Xi},(\Pi,\Sigma)\models\psi\) follows from induction hypothesis. So suppose \(\psi\notin\Pi\) for contradiction. Then \(\psi\in\Sigma\), hence \(\Pi\Rightarrow\Sigma\) is derivable by \[\infer=[(w)]{\Pi\Rightarrow\Sigma}{\infer[(D\Rightarrow)]{D_{G}\varphi\Rightarrow\varphi}{\varphi\Rightarrow\varphi}},\] which contradicts \((\Pi,\Sigma)\) being a \(\Xi\)-partial valuation. Therefore our goal \(\psi\in\Pi\) holds.

2. Suppose \(D_{G}\psi\in\Delta\). We show \(M^{\Lambda}_{\Xi},(\Gamma,\Delta)\not\models D_{G}\psi\). By Lemma 2, we can find some \((\Pi,\Sigma)\in W^{\Lambda}_{\Xi}\) such that \((\Gamma,\Delta)R_{G}^{\Lambda}(\Pi,\Sigma)\) and \(\psi\in\Sigma\). By induction hypothesis, \(\psi\in\Sigma\) implies \(M^{\Lambda}_{\Xi},(\Pi,\Sigma)\not\models\psi\). Therefore our goal \(M^{\Lambda}_{\Xi},(\Gamma,\Delta)\not\models D_{G}\psi\) holds.

 ◻

Proof. We show the contraposition. Suppose \(\mathsf{G}^{\mathtt{a}}(\Lambda)\not\vdash\Gamma\Rightarrow\Delta\). Let \(\Xi:=\mathsf{Sub}(\Gamma,\Delta)\). By Lemma 1, there exists a \(\Xi\)-partial valuation \((\Gamma^{+},\Delta^{+})\) such that \(\Gamma\subseteq\Gamma^{+}\), \(\Delta\subseteq\Delta^{+}\) and \(\mathsf{Sub}(\Gamma,\Delta)=\Gamma^{+}\cup\Delta^{+}\). By Lemma 3, \(M^{\Lambda}_{\Xi},(\Gamma^{+},\Delta^{+})\not\models\bigwedge\Gamma\to\bigvee\Delta\). Therefore our goal holds. ◻

Proof. Suppose \(\mathsf{G}(\Lambda)\vdash\Gamma \Rightarrow \Delta\). By Proposition [prop:soundness-D], \(\bigwedge\Gamma\to\bigvee\Delta\) is valid in \(\mathbb{F}_{\Lambda}\). Therefore, our goal \(\mathsf{G}^{\mathtt{a}}(\Lambda)\vdash\Gamma\Rightarrow\Delta\) holds by Theorem 2. ◻

Proof. In what follows, we let \(\Lambda\) be \(\mathbf{K45}_{D}\). This is because the cases where \(\Lambda\) is \(\mathbf{KD45}_{D}\) or \(\mathbf{S5}_{D}\) can be handled using an argument similar to that for \(\mathbf{K45}_{D}\). By Corollary 1, we can assume that \(\Gamma\Rightarrow\Delta\) has a derivation \(\mathcal{D}\) in \(\mathsf{G}^{\mathtt{a}}(\Lambda)\). We prove Lemma 5 by induction on \(\mathcal{D}\). Let the height of \(\mathcal{D}\) be \(n\). For the base case, our argument is standard (the reader is referred to [@Ono_1998_prooftheoretic]). For the inductive step, let \(n>0\). First, we suppose \(\Gamma_{1}=\Delta_{1}=\emptyset\) or \(\Gamma_{2}=\Delta_{2}=\emptyset\). Then the interpolant is \(\neg\bot\) or \(\bot\). Hence, in what follows, we suppose it is not the case that \(\Gamma_{1}=\Delta_{1}=\emptyset\) or \(\Gamma_{2}=\Delta_{2}=\emptyset\), i.e., \(\Gamma_{1}\cup\Delta_{1}\ne\emptyset\) and \(\Gamma_{2}\cup\Delta_{2}\ne\emptyset\). We divide our argument depending on the last applied rule to obtain \(\Gamma\Rightarrow\Delta\). We comment on the cases where the last applied rule is an analytic cut or \((\Rightarrow D^{\mathbf{K45}_{D}})\). Although an argument for the case of analytic cut is discussed already in [@Ono_1998_prooftheoretic], we provide the details here in order to make the proof self-contained. For other cases, the reader is referred to [@Ono_1998_prooftheoretic] for propositional connectives.

• Suppose that the last applied rule is an analytic cut: \[\infer[(Cut)_\varphi]{\Gamma_{1},\Gamma_{2}, \Pi_{1},\Pi_{2} \Rightarrow \Delta_{1},\Delta_{2}, \Sigma_{1},\Sigma_{2}}{\Gamma_{1},\Gamma_{2} \Rightarrow \Delta_{1},\Delta_{2}, \varphi & \varphi, \Pi_{1},\Pi_{2} \Rightarrow \Sigma_{1},\Sigma_{2}},\] where \(\varphi\in\mathsf{Sub}(\Gamma_{1},\Gamma_{2}, \Pi_{1},\Pi_{2}, \Delta_{1},\Delta_{2}, \Sigma_{1},\Sigma_{2})\). The partition is of the form \[\langle (\Gamma_{1},\Pi_{1}:\Delta_{1},\Sigma_{1});(\Gamma_{2},\Pi_{2}:\Delta_{2},\Sigma_{2}) \rangle.\] We divide the argument into the following cases: \[\varphi\in\mathsf{Sub}(\Gamma_{1},\Pi_{1},\Delta_{1},\Sigma_{1})\text{ and }\varphi\in\mathsf{Sub}(\Gamma_{2},\Pi_{2},\Delta_{2},\Sigma_{2}).\] We focus only on the former case. Suppose \(\varphi\in\mathsf{Sub}(\Gamma_{1},\Pi_{1},\Delta_{1},\Sigma_{1})\). By induction hypothesis, we can find formulas \(\psi_{1}\) and \(\psi_{2}\) such that

  • both \(\Gamma_{1},\Rightarrow\Delta_{1},\varphi,\psi_{1}\) and \(\psi_{1},\Gamma_{2}\Rightarrow\Delta_{2}\) are derivable in \(\mathsf{G}(\Lambda)\) and \(\mathsf{X}(\psi_{1})\subseteq\mathsf{X}(\Gamma_{1},\Delta_{1},\varphi)\cap\mathsf{X}(\Gamma_{2},\Delta_{2})\) for all \(\mathtt{X}\in \left\{ {\mathsf{Prop}, \mathsf{Agt}} \right\}\);

  • both \(\varphi,\Pi_{1},\Rightarrow\Sigma_{1},\psi_{2}\) and \(\psi_{2},\Pi_{2}\Rightarrow\Sigma_{2}\) are derivable in \(\mathsf{G}(\Lambda)\) and \(\mathsf{X}(\psi_{2})\subseteq\mathsf{X}(\varphi,\Pi_{1},\Sigma_{1})\cap\mathsf{X}(\Pi_{2},\Sigma_{2})\) for all \(\mathtt{X}\in \left\{ {\mathsf{Prop}, \mathsf{Agt}} \right\}\).

  We show that \(\psi_{1}\lor\psi_{2}:=\neg\psi_{1}\to\psi_{2}\) is a desired interpolant. The derivability condition is obtained as follows: \[\infer[(\Rightarrow\to)]{\Gamma_{1},\Pi_{1}\Rightarrow\Delta_{1},\Sigma_{1},\neg\psi_{1}\to\psi_{2}}{\infer[(\neg\Rightarrow)]{\neg\psi_{1},\Gamma_{1},\Pi_{1}\Rightarrow\Delta_{1},\Sigma_{1},\psi_{2}}{\infer[(Cut)^{\mathtt{a}}_{\varphi}]{\Gamma_{1},\Pi_{1}\Rightarrow\Delta_{1},\Sigma_{1},\psi_{1},\psi_{2}}{\Gamma_{1},\Rightarrow\Delta_{1},\varphi,\psi_{1} & \varphi,\Pi_{1},\Rightarrow\Sigma_{1},\psi_{2}}}}, \quad \infer[(\to\Rightarrow)]{\neg\psi_{1}\to\psi_{2},\Gamma_{2},\Pi_{2}\Rightarrow\Delta_{2},\Sigma_{2}}{\infer[(\Rightarrow\neg)]{\Gamma_{2}\Rightarrow\Delta_{2},\neg\psi_{1}}{\psi_{1},\Gamma_{2}\Rightarrow\Delta_{2}} & \psi_{2},\Pi_{2}\Rightarrow\Sigma_{2}},\] where the \((Cut)\) is analytic by our assumption \(\varphi\in\mathsf{Sub}(\Gamma_{1},\Pi_{1},\Delta_{1},\Sigma_{1})\). Moreover the variable and agent conditions are verified as follows. Let \(\mathsf{X} \in \{ \mathsf{Prop}, \mathsf{Agt}\}\). We proceed as follows: \[\begin{align} \mathsf{X}(\neg\psi_{1}\to\psi_{2})&=\mathsf{X}(\psi_{1})\cup\mathsf{X}(\psi_{2}),\\ &\subseteq(\mathsf{X}(\Gamma_{1},\Delta_{1},\varphi)\cap\mathsf{X}(\Gamma_{2},\Delta_{2}))\cup(\mathsf{X}(\varphi,\Pi_{1},\Sigma_{1})\cap\mathsf{X}(\Pi_{2},\Sigma_{2}))\\ &\subseteq\mathsf{X}(\Gamma_{1},\Pi_{1},\Delta_{1},\Sigma_{1},\varphi)\cap\mathsf{X}(\Gamma_{2},\Pi_{2},\Delta_{2},\Sigma_{2}). \end{align}\] By Lemma 4, \(\varphi\in\mathsf{Sub}(\Gamma_{1},\Pi_{1},\Delta_{1},\Sigma_{1})\) implies \(\mathsf{X}(\varphi)\subseteq\mathsf{X}(\Gamma_{1},\Pi_{1},\Delta_{1},\Sigma_{1})\). Therefore, we obtain \(\mathsf{X}(\neg\psi_{1}\to\psi_{2})\subseteq\mathsf{X}(\Gamma_{1},\Pi_{1},\Delta_{1},\Sigma_{1})\cap\mathsf{X}(\Gamma_{2},\Pi_{2},\Delta_{2},\Sigma_{2})\).

• Suppose that the last applied rule is \((\Rightarrow D^{\mathbf{K45}_{D}})\): \[{ \infer[(\Rightarrow D^{\mathbf{K45}_{D}})]{\overrightarrow{D_{G_{1x}}\varphi_{1x}},\overrightarrow{D_{G_{2y}}\varphi_{2y}}\Rightarrow \overrightarrow{D_{H_{1a}}\psi_{1a}},\overrightarrow{D_{H_{2b}}\psi_{2b}}, D_{G}\chi}{\overrightarrow{\varphi_{1x}},\overrightarrow{\varphi_{2y}},\overrightarrow{D_{G_{1x}}\varphi_{1x}},\overrightarrow{D_{G_{2y}}\varphi_{2y}}\Rightarrow \overrightarrow{D_{H_{1a}}\psi_{1a}},\overrightarrow{D_{H_{2b}}\psi_{2b}}, \chi}}{},\] where \(\overrightarrow{\gamma_{iz}}\) denotes a list \(\gamma_{i1},\dots,\gamma_{im_{z}}\) of formulas and \(G_{1x}\), \(H_{1a}\), \(G_{2y}\), \(H_{2b} \subseteq G\) hold for all indices. There are the following two possible forms of the partitions of the conclusion of the rule:

  1. \(\langle (\overrightarrow{D_{G_{1x}}\varphi_{1x}}:\overrightarrow{D_{H_{1a}}\psi_{1a}},D_{G}\chi);(\overrightarrow{D_{G_{2y}}\varphi_{2y}}:\overrightarrow{D_{H_{2b}}\psi_{2b}}) \rangle\),

  2. \(\langle (\overrightarrow{D_{G_{1x}}\varphi_{1x}}:\overrightarrow{D_{H_{1a}}\psi_{1a}});(\overrightarrow{D_{G_{2y}}\varphi_{2y}}:\overrightarrow{D_{H_{2b}}\psi_{2b}},D_{G}\chi) \rangle\).

  Due to space limitations, we focus on case (a) alone. By induction hypothesis, we can find a formula \(\psi\) such that both \(\overrightarrow{\varphi_{1x}},\overrightarrow{D_{G_{1x}}\varphi_{1x}}\Rightarrow \overrightarrow{D_{H_{1a}}\psi_{1a}},\chi,\psi\) and \(\psi, \overrightarrow{\varphi_{2y}},\overrightarrow{D_{G_{2y}}\varphi_{2y}}\Rightarrow \overrightarrow{D_{H_{2b}}\psi_{2b}}\) are derivable in \(\mathsf{G}^{\mathtt{a}}(\mathbf{K45}_{D})\) and \(\psi\) satisfies \(\mathsf{X}(\psi)\subseteq\mathsf{X}(\overrightarrow{\varphi_{1x}},\overrightarrow{D_{G_{1x}}\varphi_{1x}},\overrightarrow{D_{H_{1a}}\psi_{1a}},\chi)\cap\mathsf{X}(\overrightarrow{D_{G_{2y}}\varphi_{2y}},\overrightarrow{D_{H_{2b}}\psi_{2b}})\), where \(\mathtt{X}\in \left\{ {\mathsf{Prop}, \mathsf{Agt}} \right\}\). We show that \(\neg D_{H}\neg\psi\) is a desired interpolant, where \(H=\bigcup \overrightarrow{G_{2y}}\cup \bigcup \overrightarrow{H_{2b}}\). We note that \(H\ne\emptyset\) since we have assumed \(\Gamma_{2}\cup\Delta_{2}\ne\emptyset\). It follows that \(H\subseteq G\).

  \[\infer[(\Rightarrow\neg)]{\overrightarrow{D_{G_{1x}}\varphi_{1x}}\Rightarrow \overrightarrow{D_{H_{1a}}\psi_{1a}},D_{G}\chi,\neg D_{H}\neg\psi}{\infer[(\Rightarrow D^{\mathbf{K45}_{D}})]{D_{H}\neg\psi,\overrightarrow{D_{G_{1x}}\varphi_{1x}}\Rightarrow \overrightarrow{D_{H_{1a}}\psi_{1a}},D_{G}\chi}{\infer[(w\Rightarrow)]{\neg\psi,D_{H}\neg\psi,\overrightarrow{\varphi_{1x}},\overrightarrow{D_{G_{1x}}\varphi_{1x}}\Rightarrow \overrightarrow{D_{H_{1a}}\psi_{1a}},\chi}{\infer[(\neg\Rightarrow)]{\neg\psi,\overrightarrow{\varphi_{1x}},\overrightarrow{D_{G_{1x}}\varphi_{1x}}\Rightarrow \overrightarrow{D_{H_{1a}}\psi_{1a}},\chi}{\overrightarrow{\varphi_{1x}},\overrightarrow{D_{G_{1x}}\varphi_{1x}}\Rightarrow \overrightarrow{D_{H_{1a}}\psi_{1a}},\chi,\psi}}}} \quad \infer[(\neg\Rightarrow)]{\neg D_{H}\neg\psi,\overrightarrow{D_{G_{2y}}\varphi_{2y}}\Rightarrow \overrightarrow{D_{H_{2b}}\psi_{2b}}}{\infer[(\Rightarrow D^{\mathbf{K45}_{D}})]{\overrightarrow{D_{G_{2y}}\varphi_{2y}}\Rightarrow \overrightarrow{D_{H_{2b}}\psi_{2b}},D_{H}\neg\psi}{\infer[(\Rightarrow\neg)]{\overrightarrow{\varphi_{2y}},\overrightarrow{D_{G_{2y}}\varphi_{2y}}\Rightarrow \overrightarrow{D_{H_{2b}}\psi_{2b}},\neg\psi}{\psi,\overrightarrow{\varphi_{2y}},\overrightarrow{D_{G_{2y}}\varphi_{2y}}\Rightarrow \overrightarrow{D_{H_{2b}}\psi_{2b}}}}},\]

  where both applications of \((\Rightarrow D^{\mathbf{K45}_{D}})\) are eligible. Since the condition for propositional variables is easily satisfied, we comment on the condition for agents. Our goal is to show that \(\mathsf{Agt}(\neg D_{H}\neg\psi)\subseteq\mathsf{Agt}(\overrightarrow{D_{G_{1x}}\varphi_{1x}},\overrightarrow{D_{H_{1a}}\psi_{1a}},D_{G}\chi)\cap\mathsf{Agt}(\overrightarrow{D_{G_{2y}}\varphi_{2y}},\overrightarrow{D_{H_{2b}}\psi_{2b}})\). However, note that this argument is not possible when \(\Gamma_{2}=\Delta_{2}=\emptyset\), in which case \(\mathsf{Agt}(\overrightarrow{D_{G_{2y}}\varphi_{2y}},\overrightarrow{D_{H_{2b}}\psi_{2b}})=\emptyset\). The same situation happens when \(\Gamma_{1}=\Delta_{1}=\emptyset\) for case (b). This is precisely why we made the assumption \(\Gamma_{1}=\Delta_{1}=\emptyset\) or \(\Gamma_{2}=\Delta_{2}=\emptyset\) in the first place. Fix any \(a\in \mathsf{Agt}(\neg D_{H}\neg\psi)=H\cup\mathsf{Agt}(\psi)\). We divide the argument into the following two cases: \(a\in \mathsf{Agt}(\psi)\) and \(a\notin \mathsf{Agt}(\psi)\).

  • Suppose \(a\in \mathsf{Agt}(\psi)\). Then our goal \[a\in \mathsf{Agt}(\overrightarrow{D_{G_{1x}}\varphi_{1x}},\overrightarrow{D_{H_{1a}}\psi_{1a}},D_{G}\chi)\cap\mathsf{Agt}(\overrightarrow{D_{G_{2y}}\varphi_{2y}},\overrightarrow{D_{H_{2b}}\psi_{2b}})\] follows from \(\mathsf{Agt}(\psi)\subseteq\mathsf{Agt}(\overrightarrow{\varphi_{1x}},\overrightarrow{D_{G_{1x}}\varphi_{1x}},\overrightarrow{D_{H_{1a}}\psi_{1a}},\chi)\cap\mathsf{Agt}(\overrightarrow{D_{G_{2y}}\varphi_{2y}},\overrightarrow{D_{H_{2b}}\psi_{2b}})\). Note that it is possible that \(\{\overrightarrow{\varphi_{1x}}\}=\{\overrightarrow{D_{G_{1x}}\varphi_{1x}}\}=\emptyset\), in which case the argument remains valid.

  • Suppose \(a\notin \mathsf{Agt}(\psi)\). Then \(a\in H\). Our goal is to show \[a\in \mathsf{Agt}(\overrightarrow{D_{G_{1x}}\varphi_{1x}},\overrightarrow{D_{H_{1a}}\psi_{1a}},D_{G}\chi)\cap\mathsf{Agt}(\overrightarrow{D_{G_{2y}}\varphi_{2y}},\overrightarrow{D_{H_{2b}}\psi_{2b}}),\] i.e., \(a\in \mathsf{Agt}(\overrightarrow{D_{G_{1x}}\varphi_{1x}},\overrightarrow{D_{H_{1a}}\psi_{1a}},D_{G}\chi)\) and \(a\in \mathsf{Agt}(\overrightarrow{D_{G_{2y}}\varphi_{2y}},\overrightarrow{D_{H_{2b}}\psi_{2b}})\). The first condition is satisfied by \(a\in H\subseteq G\subseteq \mathsf{Agt}(D_{G}\chi)\), and the second condition is satisfied by \(H=\bigcup \overrightarrow{G_{2y}}\cup \bigcup \overrightarrow{H_{2b}}\).

 ◻

Proof. Suppose \(\mathsf{G}(\Lambda)\vdash\Rightarrow\varphi\to\psi\). Then we can show \(\mathsf{G}(\Lambda)\vdash\varphi\Rightarrow\psi\) by \[\infer[(Cut)_{\varphi\to\psi}]{\varphi\Rightarrow\psi}{\Rightarrow\varphi\to\psi & \infer[(\to\Rightarrow)]{\varphi,\varphi\to\psi\Rightarrow\psi}{\varphi\Rightarrow\varphi & \psi\Rightarrow\psi}}.\] By Corollary 1, we have \(\mathsf{G}^{\mathtt{a}}({\Lambda})\vdash\varphi\Rightarrow\psi\). Take a partition \(\langle (\varphi:\emptyset);(\emptyset:\psi) \rangle\). Then by Lemma 5, we can find an interpolant \(\chi\) that satisfies the required conditions. ◻

Proof. (Outline) The latter part follows immediately from the former part by Theorem 4. In what follows, we outline the proof of the former part. The following definitions and arguments are adapted from [@Fagin_1992_What; @Agotnes_2021_group; @Murai_2022_intuitionistic]. Suppose that a formula \(\varphi\) is valid in the class \(\mathbb{F}_{\Lambda}\). To show that \(\varphi\) is valid in the pseudo-frame class \(\mathbb{P}_{\Lambda}\), let us fix an arbitrary pseudo-frame \(F = (W,(R_{G})_{G \in \mathsf{Grp}})\) in \(\mathbb{P}_{\Lambda}\). Our goal is to establish the validity of \(\varphi\) on \(F\). Let us fix an arbitrary valuation \(V\) and a state \(w \in W\). We will show that \(M,w\models \varphi\), where \(M := (F,V)\). Without loss of generality, we assume that \(M\) is point-generated by \(w\) with respect to the binary relations \((R_{G})_{G \in \mathsf{Grp}}\). We define the tree unraveling \(\mathtt{Tree}^{\Lambda}(M,w)\) of \(M\) around \(w\) as follows:

• \(\mathtt{Finpath}(M,w)\) is defined as follows: \[\begin{align} \mathtt{Finpath}(M,w) := \{\, &\langle w_{0},G_{1},w_{1},\dots,G_{m},w_{m}\rangle \mid {}\\ & m \ge 0,\;G_i\in\mathsf{Grp},\;w_{0}=w, w_{i-1}R_{G_i}w_i \text{ for all } 1\le i\le m \,\}. \end{align}\] We refer to an element of \(\mathtt{Finpath}(M,w)\) as a “path (from state \(w\))” and denote it by \(\overrightarrow{v},\overrightarrow{u}\), etc.

• We define a binary relation \(\mathcal{R}_{G}\) on \(\mathtt{Finpath}(M,w)\) as follows:\(\overrightarrow{w}\mathcal{R}_{G}\overrightarrow{v}\) iff \(\overrightarrow{v} = \overrightarrow{w} {}^{\frown} (H, \mathtt{tail}(\overrightarrow{w}))\) for some \(H \supseteq G\), where \(\mathtt{tail}(\overrightarrow{w})\) denotes the last element of \(\overrightarrow{w}\), and \({}^{\frown}\) denotes concatenation. We use \(\mathcal{R}_{G}^{+}\) (or \(\mathcal{R}_{G}^{\ast}\)) to mean the transitive closure (or the reflexive and transitive closure) of \(\mathcal{R}_{G}\).

• Depending on our choice of \(\Lambda\), we define \(\mathcal{R}^{\Lambda}_{G}\) as follows:

  • For \(\Lambda \in \left\{ {\mathbf{K45}_{D\mathsf{A}},\mathbf{KD45}_{D\mathsf{A}}} \right\}\), define \(\overrightarrow{w}\mathcal{R}^{\Lambda}_{G}\overrightarrow{v}\) iff there exists \(\overrightarrow{u}\in\mathtt{Finpath}(M,w)\) such that \(\overrightarrow{u} \mathcal{R}_{G}^{\ast} \overrightarrow{w}\) and \(\overrightarrow{u} \mathcal{R}_{G}^{+} \overrightarrow{v}\);

  • For \(\Lambda = \mathbf{S5}_{D\mathsf{A}}\), define \(\overrightarrow{w}\mathcal{R}^{\Lambda}_{G}\overrightarrow{v}\) iff there exists \(\overrightarrow{u}\in\mathtt{Finpath}(M,w)\) such that \(\overrightarrow{u} \mathcal{R}_{G}^{\ast} \overrightarrow{w}\) and \(\overrightarrow{u} \mathcal{R}_{G}^{\ast} \overrightarrow{v}\).

• \(\mathcal{V}(p)=\left\{\, {\overrightarrow{v}\in \mathtt{Finpath}(M,w)} \,|\, {\mathtt{tail}(\overrightarrow{v})\in V(p)} \,\right\}\) for every \(p\in\mathsf{Prop}\).

• Define \(\mathtt{Tree}^{\Lambda}(M,w) := (\mathtt{Finpath}(M,w), (\mathcal{R}^{\Lambda}_{G})_{G \in \mathsf{Grp}}, \mathcal{V})\).

It is straightforward to verify that the frame part \((\mathtt{Finpath}(M,w), (\mathcal{R}^{\Lambda}_{G})_{G \in \mathsf{Grp}})\) of \(\mathtt{Tree}^{\Lambda}(M,w)\) still belongs to \(\mathbb{P}_{\Lambda}\). Moreover, we note that \(\mathcal{R}^{\Lambda}_{G}\) \(=\) \(\bigcap_{a \in G} \mathcal{R}^{\Lambda}_{\left\{ {a} \right\}}\) holds. We can also establish that the mapping \(\mathtt{tail}: \mathtt{Finpath}(M,w) \to W\), which sends each \(\overrightarrow{v}\) to its last element \(\mathtt{tail}(\overrightarrow{v})\), is a surjective bounded morphism between pseudo-models. Here, surjectivity is necessary for preserving the truth of formulas of the form \(\mathsf{A}\psi\) (along the bounded morphism). Then we obtain \(\mathtt{Tree}^{\Lambda}(M,w),\langle w \rangle \models \varphi\) iff \(M, \mathtt{tail}(\langle w\rangle) \models \varphi\), where \(\mathtt{tail}(\langle w\rangle) = w\). Since \(\mathcal{R}^{\Lambda}_{G}\) \(=\) \(\bigcap_{a \in G} \mathcal{R}^{\Lambda}_{\left\{ {a} \right\}}\) holds, \((\mathtt{Finpath}(M,w), (\mathcal{R}^{\Lambda}_{\left\{ {a} \right\}})_{a \in \mathsf{Ag}}) \in \mathbb{F}_{\Lambda}\). Since \(\varphi\) is valid in \(\mathbb{F}_{\Lambda}\), we obtain \((\mathtt{Finpath}(M,w), (\mathcal{R}^{\Lambda}_{\left\{ {a} \right\}})_{a \in \mathsf{Ag}}, \mathcal{V}), \langle w \rangle \models \varphi\), hence \(\mathtt{Tree}^{\Lambda}(M,w),\langle w \rangle \models \varphi\) in terms of pseudo models. Therefore, it follows from the above equivalence that \(M,w\models \varphi\), as desired. ◻