Knowledge forgetting in propositional μ-calculus

The μ-calculus is one of the most important logics describing specifications of transition systems. It has been extensively explored for formal verification in model checking due to its exceptional balance between expressiveness and algorithmic properties. From the perspective of systems/knowledge evolving, one may want to discard some atoms (elements) that become irrelevant or unnecessary in a specification; one may also need to know what makes something true, or the minimal condition under which something holds. This paper aims to address these scenarios for μ-calculus in terms of knowledge forgetting. In particular, it proposes a notion of forgetting based on a generalized bisimulation and explores the semantic and logical properties of forgetting, including some reasoning complexity results. It also shows that forgetting can be employed to perform knowledge update.

Not applicable.

Not applicable.

1. Personal communication: Giovanna D’Agostino, 2020.

We thank the reviewers for their insightful comments, with which the presentation of this paper was highly improved. This work was partially supported by the Natural Science Foundation of China under grants 61976065, U1836205 and 61370161. Yisong’s work was also partially supported by Guizhou Science Support Project (2022-259).

This work is funded by the National Natural Science Foundation of P.R. China under Grants 61976065 and U1836205.

Authors and Affiliations

1. Department of Computer Science, Guizhou University, Guizhou, China

   Renyan Feng, Yisong Wang, Ren Qian, Lei Yang & Panfeng Chen

2. Institute for Artificial Intelligence, Guizhou University, Guizhou, China

   Renyan Feng, Yisong Wang, Ren Qian, Lei Yang & Panfeng Chen

Contributions

All authors contributed to the study conception and design. Material preparation and analysis were performed by Renyan Feng and Yisong Wang. The first draft of the manuscript was written by Renyan Feng and all authors commented on previous versions of the manuscript. All authors read and approved the final manuscript.

Corresponding author

Correspondence to Yisong Wang.

Ethics approval

We promise that our work is original, not submitted to more than one journal for simultaneous consideration, and has not been published elsewhere in any form or language (partially or in full).

Consent to participate

Yes.

Consent for Publication

Yes.

Conflict of Interests

The authors have no financial or proprietary interests in any material discussed in this article.

Publisher’s note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Appendix A: Proofs in Section 3

Lemma 1 Let \({\mathcal M}=(S,r,R,L)\), \({\mathcal M}_{s} = (S,s, R, L)\), \(v:{\mathcal V} \rightarrow 2^{S}\), s ∈ S, and φ be a μ-formula. We have

1. (i)

   for each s₁ ∈ S, \(s_{1} \in \left \|\varphi \right \|_{v}^{{\mathcal M}}\) iff \(s_{1} \in \left \|\varphi \right \|_{v}^{{\mathcal M}_{s}}\);

2. (ii)

   \(({\mathcal M},s,v) \models \varphi\) iff \(({\mathcal M}_{s},v)\models \varphi\).

Proof

1. (i)

   Base.:

   1. (a)

      φ = p with \(p \in \mathcal {A}\).

      \(s_{1} \in \left \|\varphi \right \|_{v}^{{\mathcal M}}\)

      ⇔ \(s_{1} \in \{s^{\prime } \mid p \in L(s^{\prime })\}\)

      ⇔ \(s_{1} \in \left \|\varphi \right \|_{v}^{{\mathcal M}_{s}}\).

   2. (b)

      φ = X with \(X\in {\mathcal V}\).

      \(s_{1} \in \left \|\varphi \right \|_{v}^{{\mathcal M}}\)

      ⇔ s₁ ∈ v(X)

      ⇔ \(s_{1} \in \left \|\varphi \right \|_{v}^{{\mathcal M}_{s}}\).

   Step.:

   1. (a)

      φ = ¬φ₁.

      \(s_{1}\in \left \|\varphi \right \|_{v}^{{\mathcal M}}\)

      ⇔ \(s_{1} \not \in \left \|\varphi _{1}\right \|_{v}^{{\mathcal M}}\)

      ⇔ \(s_{1} \not \in \left \|\varphi _{1}\right \|_{v}^{{\mathcal M}_{s}}\) (induction hypothesis)

      ⇔ \(s_{1} \in \left \|\varphi \right \|_{v}^{{\mathcal M}_{s}}\).

   2. (b)

      φ = φ₁ ∨ φ₂.

      \(s_{1} \in \left \|\varphi \right \|_{v}^{{\mathcal M}}\)

      ⇔ \(s_{1} \in \left \|\varphi _{1}\right \|_{v}^{{\mathcal M}}\) or \(s_{1} \in \left \|\varphi _{2}\right \|_{v}^{{\mathcal M}}\)

      ⇔ \(s_{1} \in \left \|\varphi _{1}\right \|_{v}^{{\mathcal M}_{s}}\) or \(s_{1} \in \left \|\varphi _{2}\right \|_{v}^{{\mathcal M}_{s}}\) (induction hypothesis)

      ⇔ \(s_{1} \in \left \|\varphi \right \|_{v}^{{\mathcal M}_{s}}\).

   3. (c)

      φ = axφ₁.

      \(s_{1} \in \left \|\varphi \right \|_{v}^{{\mathcal M}}\)

      ⇔ \(s_{1} \in \{s^{\prime } \mid \forall s^{\prime \prime }.(s^{\prime },s^{\prime \prime }) \in R \Rightarrow s^{\prime \prime }\in \left \|\varphi _{1}\right \|_{v}^{{\mathcal M}}\}\)

      ⇔ \(s_{1} \in \{s^{\prime } \mid \forall s^{\prime \prime }.(s^{\prime },s^{\prime \prime }) \in R \Rightarrow s^{\prime \prime }\in \left \|\varphi _{1}\right \|_{v}^{{\mathcal M}_{s}}\}\) (induction hypothesis)

      ⇔ \(s_{1} \in \left \|\varphi \right \|_{v}^{{\mathcal M}_{s}}\).

   4. (d)

      φ = νX.φ₁.

      \(s_{1} \in \left \|\varphi \right \|_{v}^{{\mathcal M}}\)

      ⇔ \(s_{1}\in \bigcup \{S^{\prime } \subseteq S \mid S^{\prime } \subseteq \left \|\varphi _{1}\right \|_{v[X:=S^{\prime }]}^{{\mathcal M}}\}\)

      ⇔ There is some \(S^{\prime } \subseteq S\) s.t. \(s_{1} \in S^{\prime }\) and \(S^{\prime } \subseteq \left \|\varphi _{1}\right \|_{v[X:=S^{\prime }]}^{{\mathcal M}}\)

      ⇔ There is some \(S^{\prime } \subseteq S\) s.t. \(s_{1} \in S^{\prime }\) and \(S^{\prime } \subseteq \left \|\varphi _{1}\right \|_{v[X:=S^{\prime }]}^{{\mathcal M}_{s}}\) (induction hypothesis)

      ⇔ \(s_{1} \in \bigcup \{S^{\prime } \subseteq S \mid S^{\prime } \subseteq \left \|\varphi _{1}\right \|_{v[X:=S^{\prime }]}^{{\mathcal M}_{s}}\}\)

      ⇔ \(s_{1} \in \left \|\varphi \right \|_{v}^{{\mathcal M}_{s}}\).

   (ii):

   \(({\mathcal M},s,v) \models \varphi\)

   ⇔ \(s \in \left \|\varphi \right \|_{v}^{{\mathcal M}}\)

   ⇔ \(s \in \left \|\varphi \right \|_{v}^{{\mathcal M}_{s}}\) (i)

   ⇔ \(({\mathcal M}_{s}, v) \models \varphi\).

□

Appendix B:: Proofs in Section 4

Proposition 1 Let \({\mathcal V}_{1}, {\mathcal V}_{2}\subseteq {\mathcal V}\), \(V, V_{1} \subseteq \mathcal {A}\), and \({\mathcal M}_{1}\), \({\mathcal M}_{2}\), and \({\mathcal M}_{3}\) be three Kripke structures. If v₁, v₂, and v₃ are valuations of the variables in \({\mathcal V}\) to the states of \({\mathcal M}_{1}\), \({\mathcal M}_{2}\), and \({\mathcal M}_{3}\), respectively, then we have:

1. (i)

   \(\leftrightarrow _{\langle {{\mathcal V}_{1},V}\rangle }\) is an equivalence relation between valuations;

2. (ii)

   If \(({\mathcal M}_{1}, s_{1},v_{1}) \leftrightarrow _{\langle {{\mathcal V}_{1},V}\rangle } ({\mathcal M}_{2},s_{2},v_{2})\), \({\mathcal V}_{1} \subseteq {\mathcal V}_{2}\), and \(V \subseteq V_{1}\), then \(({\mathcal M}_{1}, s_{1}, v_{1}) \leftrightarrow _{\langle {{\mathcal V}_{2},V_{1}}\rangle } ({\mathcal M}_{2}, s_{2}, v_{2})\);

3. (iii)

   if \(({\mathcal M}_{1}, s_{1}, v_{1}) \leftrightarrow _{\langle {{\mathcal V}_{1},V}\rangle } ({\mathcal M}_{2},s_{2}, v_{2})\) and \(({\mathcal M}_{2},s_{2}, v_{2}) \leftrightarrow _{\langle {{\mathcal V}_{2},V_{1}}\rangle } ({\mathcal M}_{3},s_{3}, v_{3})\), then \(({\mathcal M}_{1},s_{1},v_{1}) \leftrightarrow _{\langle {{\mathcal V}_{1} \cup {\mathcal V}_{2}, V \cup V_{1}}\rangle } ({\mathcal M}_{3},s_{3},v_{3})\).

Proof

Let \({\mathcal M}_{i} = (S_{i}, r_{i}, R_{i}, L_{i})\) be Kripke structures, and \(v_{i}: {\mathcal V} \rightarrow 2^{S_{i}}\) be valuations of the variables in \({\mathcal V}\) to the states of \({\mathcal M}_{i}\) (i = 1, 2, 3).

1. (i)
   1. (a)

      Reflexivity: It is easy to check that \(({\mathcal M},s, v)\leftrightarrow _{\langle {{\mathcal V}_{1},V}\rangle } ({\mathcal M},s,v)\) for any valuation \(({\mathcal M},s,v)\).

   2. (b)

      Symmetry: We will show that for each \(({\mathcal M}_{1},s_{1}, v_{1})\) and \(({\mathcal M}_{2},s_{2},v_{2})\), if \(({\mathcal M}_{1},s_{1}, v_{1}) \leftrightarrow _{\langle {{\mathcal V}_{1},V}\rangle } ({\mathcal M}_{2},s_{2},v_{2})\) then \(({\mathcal M}_{2},s_{2}, v_{2}) \leftrightarrow _{\langle {{\mathcal V}_{1},V}\rangle } ({\mathcal M}_{1},s_{1}, v_{1})\). Supposing \(({\mathcal M}_{1}, s_{1},v_{1}) \leftrightarrow _{\langle {{\mathcal V}_{1},V}\rangle } ({\mathcal M}_{2},s_{2},v_{2})\) by the \({\langle {{\mathcal V}_{1},V}\rangle }\)-bisimulation \({\mathscr{B}}\), we construct a relation \({\mathscr{B}}_{1}\) as follows: \({\mathscr{B}}_{1}=\{(s,t) \mid (t, s)\in {\mathscr{B}}\text {with} t\in S_{1} \text {and} s\in S_{2}\}\). We can prove that \({\mathscr{B}}_{1}\) is a V-bisimulation between \({\mathcal M}_{2}\) and \({\mathcal M}_{1}\) from the following several points:

      • \((r_{2},r_{1}) \in {\mathscr{B}}_{1}\) since \((r_{1},r_{2}) \in {\mathscr{B}}\),

      • for each s ∈ S₂ and t ∈ S₁, if \((s,t) \in {\mathscr{B}}_{1}\), then we have \((t,s) \in {\mathscr{B}}\), and hence p ∈ L₁(t) iff p ∈ L₂(s) for each \(p \in \mathcal {A} - V\), and

      • the third and forth points in the definition of V-bisimulation can be checked easily for \({\mathscr{B}}_{1}\).

      Moreover, for any \((t,s) \in {\mathscr{B}}\), we have s ∈ v₁(X) iff t ∈ v₂(X), for every \(X\in {\mathcal V}-{\mathcal V}_{1}\). Therefore, we have for any \((s,t) \in {\mathscr{B}}_{1}\), t ∈ v₂(X) iff s ∈ v₁(X) for every \(X \in {\mathcal V} -{\mathcal V}_{1}\). Hence, \(({\mathcal M}_{2},s_{2}, v_{2}) \leftrightarrow _{\langle {{\mathcal V}_{1},V}\rangle } ({\mathcal M}_{1},s_{1}, v_{1})\) holds.

   3. (c)

      Transitivity: We will show that if \(({\mathcal M}_{1},s_{1},v_{1}) \leftrightarrow _{\langle {{\mathcal V}_{1},V}\rangle } ({\mathcal M}_{2},s_{2},v_{2})\) and \(({\mathcal M}_{2},s_{2},v_{2}) \leftrightarrow _{\langle {{\mathcal V}_{1},V}\rangle } ({\mathcal M}_{3},s_{3},v_{3})\), then \(({\mathcal M}_{1},s_{1},v_{1}) \leftrightarrow _{\langle {{\mathcal V}_{1},V}\rangle } ({\mathcal M}_{3},s_{3},v_{3})\). Supposing \(({\mathcal M}_{1},s_{1},v_{1}) \leftrightarrow _{\langle {{\mathcal V}_{1},V}\rangle } ({\mathcal M}_{2},s_{2},v_{2})\) by the \({\langle {{\mathcal V}_{1},V}\rangle }\)-bisimulation \({\mathscr{B}}_{1}\) and \(({\mathcal M}_{2},s_{2},v_{2}) \leftrightarrow _{\langle {{\mathcal V}_{1},V}\rangle } ({\mathcal M}_{3},s_{3},v_{3})\) by the \({\langle {{\mathcal V}_{1},V}\rangle }\)-bisimulation \({\mathscr{B}}_{2}\), we construct a relation \({\mathscr{B}}\) as follows: \({\mathscr{B}}=\{(s, z) \mid (s,t) \in {\mathscr{B}}_{1}\ \text {and}\ (t, z)\in {\mathscr{B}}_{2} \text {with} s\in S_{1}, t\in S_{2}, \text {and} z \in S_{3}\}\). We can also prove in a similar way to (b) that \({\mathscr{B}}\) is a V-bisimulation between \({\mathcal M}_{1}\) and \({\mathcal M}_{3}\). Therefore, \({\mathcal M}_{1} \leftrightarrow _{V} {\mathcal M}_{3}\).

   Moreover, for any \((s,z) \in {\mathscr{B}}\), there exists t ∈ S₂ s.t. \((s, t) \in {\mathscr{B}}_{1}\) and \((t,z)\in {\mathscr{B}}_{2}\), then we have s ∈ v₁(X) iff t ∈ v₂(X) iff z ∈ v₃(X), for every \(X\in {\mathcal V}-{\mathcal V}_{1}\). Therefore, \(({\mathcal M}_{1},s_{1}, v_{1}) \leftrightarrow _{\langle {{\mathcal V}_{1},V}\rangle } ({\mathcal M}_{3},s_{3}, v_{3})\) holds.

2. (ii)

   Suppose that \({\mathscr{B}}_{V}\) is a \({\langle {{\mathcal V}_{1},V}\rangle }\)-bisimulation between \(({\mathcal M}_{1},s_{1},v_{1})\) and \(({\mathcal M}_{2},s_{2},v_{2})\). We will show that \({\mathscr{B}}_{V}\) is also a \({\langle {{\mathcal V}_{2},V_{1}}\rangle }\)-bisimulation between \(({\mathcal M}_{1},s_{1},v_{1})\) and \(({\mathcal M}_{2},s_{2},v_{2})\). It is obvious that:

   • \((r_{1}, r_{2}) \in {\mathscr{B}}_{V}\),

   • for each w₁ ∈ S₁ and w₂ ∈ S₂, if \((w_{1}, w_{2}) \in {\mathscr{B}}_{V}\) then p ∈ L₁(w₁) iff p ∈ L₂(w₂) for each \(p \in \mathcal {A} - V_{1}\) since p ∈ L₁(w₁) iff p ∈ L₂(w₂) for each \(p \in \mathcal {A} - V\) and \(V \subseteq V_{1}\),

   • if (w₁,r₁) ∈ R₁ and \((w_{1}, w_{2})\in {\mathscr{B}}_{V}\), then ∃r₂ ∈ S₂ s.t. (w₂,r₂) ∈ R₂ and \((r_{1},r_{2}) \in {\mathscr{B}}_{V}\) since \({\mathscr{B}}_{V}\) is a V-bisimulation between \({\mathcal M}_{1}\) and \({\mathcal M}_{2}\), and

   • if (w₂,r₂) ∈ R₂ and \((w_{1}, w_{2})\in {\mathscr{B}}_{V}\), then ∃r₁ ∈ S₁ s.t. (w₁,r₁) ∈ R₁ and \((r_{1},r_{2}) \in {\mathscr{B}}_{V}\) since \({\mathscr{B}}_{V}\) is a V-bisimulation between \({\mathcal M}_{1}\) and \({\mathcal M}_{2}\).

   Therefore, \({\mathscr{B}}_{V}\) is a V₁-bisimulation between \({\mathcal M}_{1}\) and \({\mathcal M}_{2}\).

   Moreover, for any \((s,t) \in {\mathscr{B}}_{V}\), we have s ∈ v₁(X) iff t ∈ v₂(X), for every \(X\in {\mathcal V}-{\mathcal V}_{2}\) since \({\mathcal V}_{1} \subseteq {\mathcal V}_{2}\). Therefore, \(({\mathcal M}_{1}, s_{1}, v_{1}) \leftrightarrow _{\langle {{\mathcal V}_{2},V_{1}}\rangle } ({\mathcal M}_{2},s_{2},v_{2})\) holds.

3. (iii)

   \(({\mathcal M}_{1},s_{1},v_{1}) \leftrightarrow _{\langle {{\mathcal V}_{1},V}\rangle } ({\mathcal M}_{2},s_{2},v_{2})\) implies \(({\mathcal M}_{1},s_{1},v_{1}) \leftrightarrow _{\langle {{\mathcal V}_{1} \cup {\mathcal V}_{2},V \cup V_{1}}\rangle } ({\mathcal M}_{2},s_{2},v_{2})\) by (ii), then we have \(({\mathcal M}_{1},s_{1},v_{1}) \leftrightarrow _{\langle {{\mathcal V}_{1} \cup {\mathcal V}_{2},V \cup V_{1}}\rangle } ({\mathcal M}_{3},s_{3},v_{3})\) by (i).

□

Lemma 3

Let \({\mathcal M} = (S,r,R,L)\), \(v:{\mathcal V} \rightarrow 2^{S}\), φ be a μ-formula, and \(S_{1}\subseteq S_{2} \subseteq S\). If X appears positively in φ, then we have \(\left \|\varphi \right \|_{v[X:=S_{1}]}^{{\mathcal M}} \subseteq \left \|\varphi \right \|_{v[X:=S_{2}]}^{{\mathcal M}}\).

Proof

We show this by inducting on the structures of φ.

Base. :

1. (a)

   φ = p with \(p\in \mathcal {A}\).

   $$\begin{array}{@{}rcl@{}} \left\| \varphi\right\|_{v[X:= S_{1}]}^{\mathcal{M}}& =& \{p\mid p \in L(s)\}\\ & =& \left\| \varphi\right\|_{v[X:= S_{2}]}^{\mathcal{M}}. \end{array}$$
2. (b)

   φ = Y with \(Y \in {\mathcal V}-\{X\}\).

   $$\begin{array}{@{}rcl@{}} \left\| \varphi\right\|_{v[X:= S_{1}]}^{\mathcal{M}}& =& v[X:= S_{1}](Y) \\ & =& v[X:= S_{2}](Y)\\ & =& \left\| \varphi\right\|_{v[X:= S_{2}]}^{\mathcal{M}}. \end{array}$$
3. (c)

   φ = X.

   $$\begin{array}{@{}rcl@{}} \left\| \varphi\right\|_{v[X:= S_{1}]}^{\mathcal{M}}& =& v[X:=S_{1}](X)\\ & =& S_{1}\\ & \subseteq& S_{2} \\ & =& v[X = S_{2}](X)\\ & =& \left\| \varphi\right\|_{v[X:= S_{2}]}^{\mathcal{M}}. \end{array}$$

Step. :

1. (a)

   φ = φ₁ ∗ φ₂ with ∗∈{∨,∧}, where X appears in φ_i (i = 1, 2).

   $$\begin{array}{@{}rcl@{}} \left\| \varphi\right\|_{v[X:= S_{1}]}^{\mathcal{M}}& =& \left\| \varphi_{1}\right\|_{v[X:= S_{1}]}^{\mathcal{M}} * \left\| \varphi_{2}\right\|_{v[X:= S_{1}]}^{\mathcal{M}}\\ & \subseteq& \left\| \varphi_{1}\right\|_{v[X:= S_{2}]}^{\mathcal{M}} * \left\| \varphi_{2}\right\|_{v[X:= S_{2}]}^{\mathcal{M}} \quad \text{(induction hypothesis)}\\ & =& \left\| \varphi\right\|_{v[X:= S_{2}]}^{\mathcal{M}}. \end{array}$$
2. (b)

   φ = axφ₁, and X appears positively in φ₁.

   $$\begin{array}{@{}rcl@{}} \left\| \varphi\right\|_{v[X:= S_{1}]}^{\mathcal{M}}& =& \{s \mid \forall s^{\prime}.(s,s^{\prime}) \in R \Rightarrow s^{\prime} \in \left\| \varphi_{1}\right\|_{v[X:= S_{1}]}^{\mathcal{M}}\}\\ & \subseteq& \{s \mid \forall s^{\prime}.(s,s^{\prime}) \in R \Rightarrow s^{\prime} \in \left\| \varphi_{1}\right\|_{v[X:= S_{2}]}^{\mathcal{M}}\} \quad \text{(induction hypothesis)}\\ & =& \left\| \varphi\right\|_{v[X:= S_{2}]}^{\mathcal{M}}. \end{array}$$
3. (c)

   φ = exφ₁, and X appears positively in φ₁.

   $$\begin{array}{@{}rcl@{}} \left\| \varphi\right\|_{v[X:= S_{1}]}^{\mathcal{M}}& =& \{s \mid \exists s^{\prime}.(s,s^{\prime}) \in R \wedge s^{\prime} \in \left\| \varphi_{1}\right\|_{v[X:= S_{1}]}^{\mathcal{M}}\}\\ & \subseteq& \{s \mid \exists s^{\prime}.(s,s^{\prime}) \in R \wedge s^{\prime} \in \left\| \varphi_{1}\right\|_{v[X:= S_{2}]}^{\mathcal{M}}\} \quad \text{(induction hypothesis)}\\ & =& \left\| \varphi\right\|_{v[X:= S_{2}]}^{\mathcal{M}}. \end{array}$$
4. (d)

   φ = νY.φ₁, and X appears positively in φ₁.

   1. (d.1)

      Y = X.

      $$\begin{array}{@{}rcl@{}} \left\| \varphi\right\|_{v[X:= S_{1}]}^{\mathcal{M}}& =& \bigcup\{S^{\prime} \subseteq S \mid S^{\prime} \subseteq \left\| \varphi_{1}\right\|_{v[X:= S_{1}][X:= S^{\prime}]}^{\mathcal{M}}\}\\ & =& \bigcup\{S^{\prime} \subseteq S \mid S^{\prime} \subseteq \left\| \varphi_{1}\right\|_{v[X:= S^{\prime}]}^{\mathcal{M}}\}\\ & =& \bigcup\{S^{\prime} \subseteq S \mid S^{\prime} \subseteq \left\| \varphi_{1}\right\|_{v[X:= S_{2}][X:= S^{\prime}]}^{\mathcal{M}}\}\\ & = &\left\| \varphi\right\|_{v[X:= S_{2}]}^{\mathcal{M}}. \end{array}$$
   2. (d.2)

      Y ≠X.

      $$\begin{array}{@{}rcl@{}} \left\| \varphi\right\|_{v[X:= S_{1}]}^{\mathcal{M}}& = &\bigcup\{S^{\prime} \subseteq S \mid S^{\prime} \subseteq \left\| \varphi_{1}\right\|_{v[X:= S_{1}][Y:= S^{\prime}]}^{\mathcal{M}}\}\\ & \subseteq& \bigcup\{S^{\prime} \subseteq S \mid S^{\prime} \subseteq \left\| \varphi_{1}\right\|_{v[X:= S_{2}][Y:= S^{\prime}]}^{\mathcal{M}}\} \quad \text{(induction hypothesis)}\\ & = &\left\| \varphi\right\|_{v[X:= S_{2}]}^{\mathcal{M}}. \end{array}$$
5. (e)

   φ = μX.φ₁, and X appears positively in φ₁.

   1. (e.1)

      Y = X.

      $$\begin{array}{@{}rcl@{}} \left\| \varphi\right\|_{v[X:= S_{1}]}^{\mathcal{M}}& =& \bigcap\{S^{\prime} \subseteq S \mid \left\| \varphi_{1}\right\|_{v[X:= S_{1}][X:= S^{\prime}]}^{\mathcal{M}}\subseteq S^{\prime}\}\\ & =& \bigcap\{S^{\prime} \subseteq S \mid \left\| \varphi_{1}\right\|_{v[X:= S^{\prime}]}^{\mathcal{M}} \subseteq S^{\prime}\}\\ & =& \bigcap\{S^{\prime} \subseteq S \mid \left\| \varphi_{1}\right\|_{v[X:= S_{2}][X:= S^{\prime}]}^{\mathcal{M}} \subseteq S^{\prime}\} \\ & = &\left\| \varphi\right\|_{v[X:= S_{2}]}^{\mathcal{M}}. \end{array}$$
   2. (e.2)

      Y ≠X. Please note that \(\left \| \psi \right \|_{v[X:= S]}^{{\mathcal M}} \subseteq S\) for any μ-formula ψ.

      $$\begin{array}{@{}rcl@{}} \left\| \varphi\right\|_{v[X:= S_{1}]}^{\mathcal{M}}& = &\bigcap\{S^{\prime} \subseteq S \mid \left\| \varphi_{1}\right\|_{v[X:= S_{1}][Y:= S^{\prime}]}^{\mathcal{M}}\subseteq S^{\prime}\}\\ & \subseteq& \bigcap\{S^{\prime} \subseteq S \mid \left\| \varphi_{1}\right\|_{v[X:= S_{2}][Y:= S^{\prime}]}^{\mathcal{M}} \subseteq S^{\prime}\} \quad \text{(induction hypothesis)}\\ & = &\left\| \varphi\right\|_{v[X:= S_{2}]}^{\mathcal{M}}. \end{array}$$

□

Proposition 2 (invariant) Let φ be a μ-formula, \({\mathcal V}_{1}\subseteq {\mathcal V}\) a set of variables, and V a set of atoms. If \(({\mathcal M}, s, v) \leftrightarrow _{\langle {{\mathcal V}_{1}, V}\rangle } ({\mathcal M}^{\prime }, s^{\prime }, v^{\prime })\) and \(\text {IR}(\varphi , V \cup {\mathcal V}_{1})\), then \(({\mathcal M},s, v) \models \varphi\) iff \(({\mathcal M}^{\prime },s^{\prime }, v^{\prime }) \models \varphi\).

Proof

Let \({\mathcal M}=(S,r,R,L)\) and \({\mathcal M}^{\prime }=(S^{\prime },r^{\prime },R^{\prime },L^{\prime })\). Suppose \(\textit {Var}(\varphi ) \cap (V\cup {\mathcal V}_{1}) = \emptyset\) and \(({\mathcal M}, s, v) \leftrightarrow _{\langle {{\mathcal V}_{1}, V}\rangle } ({\mathcal M}^{\prime }, s^{\prime }, v^{\prime })\) by binary relation \({\mathscr{B}}\).

Base. :

1. (a)

   φ = p with p∉V.

   \(({\mathcal M},s,v) \models \varphi\)

   ⇔ p ∈ L(s)

   ⇔ \(p\in L(s^{\prime })\) (\(({\mathcal M}, s, v) \leftrightarrow _{\langle {{\mathcal V}_{1}, V}\rangle } ({\mathcal M}^{\prime }, s^{\prime }, v^{\prime })\), p∉V)

   ⇔ \(({\mathcal M}^{\prime },s^{\prime },v^{\prime }) \models \varphi\).

2. (b)

   φ = X with \(X \not \in {\mathcal V}_{1}\).

   \(({\mathcal M},s, v)\models \varphi\)

   ⇔ s ∈ v(X)

   ⇔ \(s^{\prime } \in v^{\prime }(X)\) (\((s,s^{\prime })\in {\mathscr{B}}\), \(X\not \in {\mathcal V}_{1}\))

   ⇔ \(({\mathcal M}^{\prime },s^{\prime },v^{\prime }) \models \varphi\).

Step. :

1. (a)

   φ = ¬φ₁.

   \(({\mathcal M},s,v) \models \varphi\)

   ⇔ \(({\mathcal M},s,v) \not \models \varphi _{1}\)

   ⇔ \(({\mathcal M}^{\prime },s^{\prime },v^{\prime }) \not \models \varphi _{1}\) (induction hypothesis)

   ⇔ \(({\mathcal M}^{\prime },s^{\prime },v^{\prime }) \models \varphi\).

2. (b)

   φ = φ₁ ∨ φ₂.

   \(({\mathcal M},s,v) \models \varphi\)

   ⇔ \(({\mathcal M},s,v) \models \varphi _{1}\) or \(({\mathcal M},s,v)\models \varphi _{2}\)

   ⇔ \(({\mathcal M}^{\prime },s^{\prime },v^{\prime }) \models \varphi _{1}\) or \(({\mathcal M}^{\prime },s^{\prime },v^{\prime }) \models \varphi _{2}\) (induction hypothesis)

   ⇔ \(({\mathcal M}^{\prime },s^{\prime },v^{\prime })\models \varphi\).

3. (c)

   φ = axφ₁.

   \(({\mathcal M},s,v) \models \varphi\)

   ⇒ For each (s,s₁) ∈ R, we have \(({\mathcal M},s_{1},v) \models \varphi _{1}\)

   ⇒ For each \((s^{\prime },s_{1}^{\prime }) \in R^{\prime }\), there exists (s,s₁) ∈ R s.t. \(({\mathcal M}, s_{1}, v) \leftrightarrow _{\langle {{\mathcal V}_{1}, V}\rangle } ({\mathcal M}^{\prime }, s_{1}^{\prime }, v^{\prime })\) (and vice versa) and \(({\mathcal M},s_{1},v) \models \varphi _{1}\) (\(({\mathcal M}, s, v) \leftrightarrow _{\langle {{\mathcal V}_{1}, V}\rangle } ({\mathcal M}^{\prime }, s^{\prime }, v^{\prime })\))

   ⇒ For each \((s^{\prime },s_{1}^{\prime }) \in R^{\prime }\), we have \(({\mathcal M}^{\prime },s_{1}^{\prime },v^{\prime })\models \varphi _{1}\) (induction hypothesis)

   ⇒ \(({\mathcal M}^{\prime },s^{\prime },v^{\prime })\models \varphi\).

   The other direction can be proved similarly.

4. (d)

   φ = νX.φ₁.

   \(({\mathcal M},s,v) \models \varphi\)

   ⇒ \(s\in \bigcup \{S_{1} \subseteq S \mid S_{1} \subseteq \left \|\varphi _{1}\right \|_{v[X:= S_{1}]}^{{\mathcal M}}\}\)

   ⇒ There is \(S_{1} \subseteq S\) s.t. \(S_{1} \subseteq \left \|\varphi _{1}\right \|_{v[X:= S_{1}]}^{{\mathcal M}}\) and s ∈ S₁

   ⇒ s ∈ S₁ and for each \(w\in S_{2} = S_{1} \cup \{s_{2}\mid (t,s_{i}) \in {\mathscr{B}},~s_{2}\in S \text {and} s_{1}\in S_{1} \text {with} i=1,2\}\), there is \(w^{\prime }\in S_{1}\) s.t. \(({\mathcal M},w,v) \leftrightarrow _{\langle {{\mathcal V}_{1}, V}\rangle } ({\mathcal M},w^{\prime },v)\) (Prop. 1)

   ⇒ s ∈ S₂ and for each w ∈ S₂, there is \(w^{\prime }\in S_{1}\) s.t. \(({\mathcal M},w,v[X:=S_{2}]) \leftrightarrow _{\langle {{\mathcal V}_{1}, V}\rangle } ({\mathcal M},w^{\prime },v[X:=S_{2}])\)

   ⇒ s ∈ S₂ and for each w ∈ S₂, we have \(w \in \left \|\varphi _{1}\right \|_{v[X:= S_{2}]}^{{\mathcal M}}\) (\(S_{1} \subseteq \left \|\varphi _{1}\right \|_{v[X:= S_{1}]}^{{\mathcal M}}\), induction hypothesis, Lemma 3)

   ⇒ s ∈ S₂ and there is \(S_{2} \subseteq S\) s.t. \(S_{2} \subseteq \left \|\varphi _{1}\right \|_{v[X:= S_{2}]}^{{\mathcal M}}\)

   ⇒ s ∈ S₂ and for each \(u^{\prime }\in {\mathscr{B}}(S_{2})\), there is u ∈ S₂ s.t. \(({\mathcal M}^{\prime },u^{\prime },v^{\prime }[X:= {\mathscr{B}}(S_{2})]) \leftrightarrow _{\langle {{\mathcal V}_{1}, V}\rangle } ({\mathcal M},u,v[X:=S_{2}])\) and \(u\in \left \|\varphi _{1}\right \|_{v[X:= S_{2}]}^{{\mathcal M}}\)

   ⇒ s ∈ S₂ and for each \(u^{\prime }\in {\mathscr{B}}(S_{2})\), \(u^{\prime }\in \left \|\varphi _{1}\right \|_{v^{\prime }[X:= {\mathscr{B}}(S_{2})]}^{{\mathcal M}^{\prime }}\) (induction hypothesis)

   ⇒ There is \({\mathscr{B}}(S_{2})\subseteq S^{\prime }\) s.t. \({\mathscr{B}}(S_{2}) \subseteq \left \|\varphi _{1}\right \|_{v^{\prime }[X:= {\mathscr{B}}(S_{2})]}^{{\mathcal M}^{\prime }}\) and \(s^{\prime }\in {\mathscr{B}}(S_{2})\) (\((s,s^{\prime })\in {\mathscr{B}}\))

   ⇒ \(s^{\prime } \in \bigcup \{S_{1}^{\prime }\subseteq S^{\prime } \mid S_{1}^{\prime } \subseteq \left \|\varphi _{1}\right \|_{v^{\prime }[X:= S_{1}^{\prime }]}^{{\mathcal M}^{\prime }}\}\)

   ⇒ \(({\mathcal M}^{\prime },s^{\prime }, v^{\prime }) \models \varphi\).

We can prove the other direction similarly. □

Corollary 3 If \(({\mathcal M},s,v) \leftrightarrow _{\langle {\{X\},V}\rangle } ({\mathcal M}^{\prime },s^{\prime },v^{\prime })\) and φ is μ-formula with IR(φ,V ) and X is bound in φ, then \(({\mathcal M},s,v) \models \varphi\) iff \(({\mathcal M}^{\prime },s^{\prime },v^{\prime }) \models \varphi\).

Proof

Suppose \(({\mathcal M},s,v) \leftrightarrow _{\langle {\{X\},V}\rangle } ({\mathcal M}^{\prime },s^{\prime },v^{\prime })\) by relation \({\mathscr{B}}_{X}\).

Base. :

1. (a)

   φ = p with \(p \in \mathcal {A}-V\).

   \(({\mathcal M},s,v) \models \varphi\)

   ⇔ p ∈ L(s)

   ⇔ \(p \in L^{\prime }(s)\) (\(({\mathcal M},s,v) \leftrightarrow _{\langle {\{X\},V}\rangle } ({\mathcal M}^{\prime },s^{\prime },v^{\prime })\))

   ⇔ \(({\mathcal M}^{\prime },s^{\prime },v^{\prime }) \models \varphi\).

2. (b)

   φ = Y with \(Y \in {\mathcal V}-\{X\}\).

   \(({\mathcal M},s,v) \models \varphi\)

   ⇔ s ∈ v(Y )

   ⇔ \(s^{\prime } \in v^{\prime }(Y)\) (\(({\mathcal M},s,v) \leftrightarrow _{\langle {\{X\},V}\rangle } ({\mathcal M}^{\prime },s^{\prime },v^{\prime })\))

   ⇔ \(({\mathcal M}^{\prime },s^{\prime },v^{\prime }) \models \varphi\).

Step. :

1. (a)

   φ = ¬φ₁.

   \(({\mathcal M},s,v) \models \varphi\)

   ⇔ \(({\mathcal M},s,v) \not \models \varphi _{1}\)

   ⇔ \(({\mathcal M}^{\prime },s^{\prime }, v^{\prime }) \not \models \varphi _{1}\)

   ⇔ \(({\mathcal M}^{\prime },s^{\prime },v^{\prime }) \models \varphi\).

2. (b)

   φ = φ₁ ∨ φ₂ can be proved easily.

3. (c)

   φ = axφ₁.

   \(({\mathcal M},s,v) \models \varphi\)

   ⇒ For each (s,s₁) ∈ R, \(({\mathcal M},s_{1},v) \models \varphi _{1}\)

   ⇒ For each \((s^{\prime },s_{1}^{\prime }) \in R^{\prime }\), there is (s,s₁) ∈ R s.t. \(({\mathcal M}, s_{1},v) \leftrightarrow _{\langle {\{X\},V}\rangle } ({\mathcal M}^{\prime },s_{1}^{\prime },v^{\prime })\) and \(({\mathcal M},s_{1},v) \models \varphi _{1}\)

   ⇒ For each \((s^{\prime },s_{1}^{\prime }) \in R^{\prime }\), \(({\mathcal M}^{\prime },s_{1}^{\prime },v^{\prime }) \models \varphi _{1}\) (induction hypothesis)

   ⇒ \(({\mathcal M}^{\prime },s^{\prime },v^{\prime }) \models \varphi\).

   The other direction can be proved similarly.

4. (d)

   φ = νY.φ₁.

1. (d.1)

   Y = X. \(({\mathcal M},s,v) \models \nu X. \varphi _{1}\)

   ⇒ \(s \in \left \|\varphi \right \|_{v}^{{\mathcal M}}\)

   ⇒ \(s \in \bigcup \{S_{1} \subseteq S\mid S_{1} \subseteq \left \|\varphi _{1}\right \|_{v[X:=S_{1}]}^{{\mathcal M}}\}\)

   ⇒ There is \(S_{1} \subseteq S\) s.t. \(S_{1} \subseteq \left \|\varphi _{1}\right \|_{v[X:=S_{1}]}^{{\mathcal M}}\) and s ∈ S₁

   ⇒ There is \(S_{2}=S_{1} \cup \{s_{2}\mid (s_{i},t) \in {\mathscr{B}}_{X}, ~s_{2}\in S, \text {and} s_{1} \in S_{1} \text {with}i=1,2\}\), s.t. \(S_{2} \subseteq \left \|\varphi _{1}\right \|_{v[X:=S_{2}]}^{{\mathcal M}}\) and s ∈ S₂ (see the proof of Prop. 2)

   ⇒ There is \({\mathscr{B}}_{X}(S_{2}) \subseteq S^{\prime }\) s.t. \({\mathscr{B}}_{X}(S_{2}) \subseteq \left \|\varphi _{1}\right \|_{v^{\prime }[X:={\mathscr{B}}_{X}(S_{2})]}^{{\mathcal M}^{\prime }}\), \(s^{\prime }\in {\mathscr{B}}_{X}(S_{2})\), and \(({\mathcal M},v[X:=S_{2}]) \leftrightarrow _{V} ({\mathcal M}^{\prime },v^{\prime }[X:={\mathscr{B}}_{X}(S_{2})])\) (\((s,s^{\prime }) \in {\mathscr{B}}_{X}\), invariant)

   ⇒ \(s^{\prime }\in \bigcup \{S_{1}^{\prime } \subseteq S^{\prime }\mid S_{1}^{\prime } \subseteq \left \|\varphi _{1}\right \|_{v^{\prime }[X:=S_{1}^{\prime }]}^{{\mathcal M}^{\prime }}\}\)

   ⇒ \(({\mathcal M}^{\prime },s^{\prime },v^{\prime }) \models \nu X. \varphi _{1}\).

   The other direction can be proved similarly.

2. (d.2)

   Y ≠X. \(({\mathcal M},s,v) \models \nu Y. \varphi _{1}\)

   ⇒ \(s \in \left \|\varphi \right \|_{v}^{{\mathcal M}}\)

   ⇒ \(s \in \bigcup \{S_{1} \subseteq S\mid S_{1} \subseteq \left \|\varphi _{1}\right \|_{v[Y:=S_{1}]}^{{\mathcal M}}\}\)

   ⇒ There is \(S_{1} \subseteq S\) s.t. \(S_{1} \subseteq \left \|\varphi _{1}\right \|_{v[Y:=S_{1}]}^{{\mathcal M}}\) and s ∈ S₁

   ⇒ There is \(S_{2}=S_{1} \cup \{s_{2}\mid (s_{i},t) \in {\mathscr{B}}_{X}, ~s_{2}\in S, \text {and} s_{1} \in S_{1} \text {with}i=1,2\}\), s.t. \(S_{2} \subseteq \left \|\varphi _{1}\right \|_{v[Y:=S_{2}]}^{{\mathcal M}}\) and s ∈ S₂ (see the proof of Prop. 2)

   ⇒ There is \({\mathscr{B}}_{X}(S_{2}) \subseteq S^{\prime }\) s.t. \({\mathscr{B}}_{X}(S_{2}) \subseteq \left \|\varphi _{1}\right \|_{v^{\prime }[Y:={\mathscr{B}}_{X}(S_{2})]}^{{\mathcal M}^{\prime }}\), \(s^{\prime }\in {\mathscr{B}}_{X}(S_{2})\), and \(({\mathcal M},v[Y:=S_{2}]) \leftrightarrow _{\langle {\{X\}, V}\rangle } ({\mathcal M}^{\prime },v^{\prime }[Y:={\mathscr{B}}_{X}(S_{2})])\) (\((s,s^{\prime }) \in {\mathscr{B}}_{X}\), induction hypothesis)

   ⇒ \(s^{\prime }\in \bigcup \{S_{1}^{\prime } \subseteq S^{\prime }\mid S_{1}^{\prime } \subseteq \left \|\varphi _{1}\right \|_{v^{\prime }[Y:=S_{1}^{\prime }]}^{{\mathcal M}^{\prime }}\}\)

   ⇒ \(({\mathcal M}^{\prime },s^{\prime },v^{\prime }) \models \nu X. \varphi _{1}\).

The other direction can be proved similarly.

□

Theorem 4 Let \(q \in \mathcal A\) and φ be a μ-sentence. There is a μ-sentence ψ s.t. Var(ψ) ∩{q} = ∅ and ψ ≡F_μ(φ,{q}).

Proof

It has been proved that (Theorem 3.1 in [45]), for each μ-sentence φ and atom q, there is a μ-sentence \(\varphi ^{\prime }\) with \(\textit {Var}(\varphi ^{\prime }) \cap \{q\} = \emptyset\) s.t. :

Then we can check that \(\varphi ^{\prime }\) is a result of forgetting {q} from φ by the definition of forgetting. □

Corollary 6 Let \(V \subseteq \mathcal {A}\) and φ be a μ-sentence. We have \(\widetilde {\exists }V \varphi \equiv \textsc {F}_{\mu }(\varphi , V)\).

Proof

It is obvious that φ⊧F_μ(φ,V ) and F_μ(φ,V ) ∩ V = ∅. In addition, for any ϕ, if φ⊧ϕ and IR(ϕ,V ), there is F_μ(φ,V )⊧ϕ by Theorem 5.

Hence, F_μ(φ,V ) is an uniform interpolation of φ with respect to Var(φ) − V by the definition of uniform interpolation. □

Theorem 7 Let φ be a PL formula and \(V\subseteq \mathcal {A}\), then

Proof

Let \({\mathcal M} = (S, r, R, L)\) and \({\mathcal M}^{\prime } = (S^{\prime }, r^{\prime }, R^{\prime }, L^{\prime })\) be two Kripke structures. It is easy to see that a Kripke structure \({\mathcal M}\) is a model of a PL formula ψ, i.e., \({\mathcal M} \models \psi\), if L(r) satisfies ψ.

(⇒) For each \({\mathcal M} \in \textit {Mod}(\textsc {F}_{\mu }(\varphi , V))\)

⇒ \(\exists {\mathcal M}^{\prime } \in \textit {Mod}(\varphi )\) s.t. \({\mathcal M} \leftrightarrow _{V} {\mathcal M}^{\prime }\) (by a V-bisimulation \({\mathcal B}\)) by Def. 4

⇒ \(r {\mathcal B} r^{\prime }\)

⇒ \({\mathcal M} \models \textit {Forget}(\varphi , V)\) due to IR(Forget(φ,V ),V ) and V-invariant.

(⇐) For each \({\mathcal M} \in \textit {Mod}(\textit {Forget}(\varphi , V))\)

⇒ \(\exists {\mathcal M}^{\prime } \in \textit {Mod}(\varphi )\) s.t. \(\forall p \in \mathcal {A}-V\), p ∈ L(r) iff \(p \in L^{\prime }(r^{\prime })\) by the definition of Forget.

Constructing a Kripke structure \({\mathcal M}_{1} = (S, r, R, L_{1})\) such that L₁(s) = L(s) for each s ∈ S and \(L_{1}(r) = L^{\prime }(r^{\prime })\).

⇒ \({\mathcal M}_{1} \models \varphi\) and \({\mathcal M}_{1} \leftrightarrow _{V} {\mathcal M}\)

⇒ \({\mathcal M} \models \textsc {F}_{\mu }(\varphi , V)\) due to IR(F_μ(φ,V ),V ) and V-invariant. □

Proposition 8 Let φ and φ_i (i = 1, 2) be μ-formulas and \(V\subseteq \mathcal {A}\). We have:

1. (i)

   F_μ(φ,V ) is satisfiable iff φ is,

2. (ii)

   If φ₁ ≡ φ₂, then F_μ(φ₁,V ) ≡F_μ(φ₂,V ),

3. (iii)

   If φ₁⊧φ₂, then F_μ(φ₁,V )⊧F_μ(φ₂,V ),

4. (iv)

   F_μ(φ₁ ∨ φ₂,V ) ≡F_μ(φ₁,V ) ∨F_μ(φ₂,V ),

5. (v)

   F_μ(φ₁ ∧ φ₂,V )⊧F_μ(φ₁,V ) ∧F_μ(φ₂,V ),

6. (vi)

   F_μ(φ₁ ∧ φ₂,V ) ≡F_μ(φ₁,V ) ∧ φ₂ if IR(φ₂,V ).

Proof

(i) \(({\mathcal M},v) \in \textit {Mod}(\textsc {F}_{\mu }(\varphi , V))\)

⇔ \(\exists ({\mathcal M}^{\prime },v^{\prime }) \in \textit {Mod}(\varphi )\) s.t. \(({\mathcal M}, v) \leftrightarrow _{V} ({\mathcal M}^{\prime },v^{\prime })\).

\(({\mathcal M},v) \in \textit {Mod}(\varphi )\) implies \(({\mathcal M},v) \models \textsc {F}_{\mu }(\varphi , V)\) since φ⊧F_μ(φ,V ).

The (ii) and (iii) can be proved similarly.

(iv) \(({\mathcal M},v)\in \textit {Mod}(\textsc {F}_{\mu }(\varphi _{1} \vee \varphi _{2}, V))\)

⇔ \(\exists ({\mathcal M}^{\prime },v^{\prime })\) ∈ Mod(φ₁ ∨ φ₂) s.t. \(({\mathcal M},v) \leftrightarrow _{V} ({\mathcal M}^{\prime },v^{\prime })\) and \(({\mathcal M}^{\prime },v^{\prime }) \models \varphi _{1}\) or \(({\mathcal M}^{\prime },v^{\prime }) \models \varphi _{2}\)

⇔ \(\exists ({\mathcal M},v) \leftrightarrow _{V} ({\mathcal M}^{\prime },v^{\prime })\) s.t. \(({\mathcal M}^{\prime },v^{\prime }) \models \varphi _{1}\) or \(({\mathcal M}^{\prime },v^{\prime }) \models \varphi _{2}\), and then \(\exists ({\mathcal M}_{1},v_{1}) \in \textit {Mod}(\textsc {F}_{\mu }(\varphi _{1}, V))\) s.t. \(({\mathcal M}^{\prime },v^{\prime }) \leftrightarrow _{V} ({\mathcal M}_{1},v_{1})\), or \(\exists ({\mathcal M}_{2},v_{2}) \in \textit {Mod}(\textsc {F}_{\mu }(\varphi _{2}, V))\) s.t. \(({\mathcal M}^{\prime },v^{\prime }) \leftrightarrow _{V} ({\mathcal M}_{2},v_{2})\)

⇔ \(({\mathcal M},v) \models \textsc {F}_{\mu }(\varphi _{1}, V)\) or \(({\mathcal M},v) \models \textsc {F}_{\mu }(\varphi _{2}, V)\)

⇔ \(({\mathcal M},v) \models \textsc {F}_{\mu }(\varphi _{1}, V) \vee \textsc {F}_{\mu }(\varphi _{2}, V)\).

The (v) can be proved as (iv).

(vi) \(({\mathcal M},v) \models \textsc {F}_{\mu }(\varphi _{1} \wedge \varphi _{2},V)\)

⇔ There is \(({\mathcal M}, v) \leftrightarrow _{V} ({\mathcal M}^{\prime },v^{\prime })\) s.t. \(({\mathcal M}^{\prime },v^{\prime }) \models \varphi _{1} \wedge \varphi _{2}\)

⇔ There is \(({\mathcal M}, v) \leftrightarrow _{V} ({\mathcal M}^{\prime },v^{\prime })\) s.t. \(({\mathcal M}^{\prime }, v^{\prime }) \models \varphi _{1}\) and \(({\mathcal M}^{\prime }, v^{\prime }) \models \varphi _{2}\)

⇔ \(({\mathcal M}, v) \models \textsc {F}_{\mu }(\varphi _{1},V)\) and \(({\mathcal M},v) \models \varphi _{2}\) due to IR(φ₂,V )

⇔ \(({\mathcal M},v) \models \textsc {F}_{\mu }(\varphi _{1},V) \wedge \varphi _{2}\). □

Proposition 9 (Decomposition) Given a μ-formula φ, a set of atoms V and an atom p s.t. p∉V, then,

Proof

Let \(({\mathcal M}_{1},v_{1})\) with \({\mathcal M}_{1}=(S_{1}, s_{1}, R_{1}, L_{1})\) be a model of F_μ(φ,{p}∪ V ). By the definition of forgetting, there exists a model \(({\mathcal M},v)\) (\({\mathcal M} = (S, s, R,L)\)) of φ s.t. \(({\mathcal M}_{1},v_{1})\) \(\leftrightarrow _{\{p\} \cup V}\) \(({\mathcal M},v)\). We construct a Kripke structure \({\mathcal M}_{2} = (S_{2}, s_{2}, R_{2}, L_{2})\) as follows:

1. 1.

   for s₂, let s₂ be the state such that:

   • p ∈ L₂(s₂) iff p ∈ L₁(s₁),

   • for all q ∈ V, q ∈ L₂(s₂) iff q ∈ L(s),

   • for all other atoms \(q^{\prime }\), \(q^{\prime } \in L_{2}(s_{2})\) iff \(q^{\prime } \in L_{1}(s_{1})\) iff \(q^{\prime }\in L(s)\).

2. 2.

   for another: Suppose that \({\mathcal M}_{1}\) \(\leftrightarrow _{\{p\} \cup V}\) \({\mathcal M}\) by the {p}∪ V-bisimulation \({\mathcal B}\).

   1. (i)

      for all pairs w ∈ S and w₁ ∈ S₁ s.t. \((w,w_{1})\in {\mathcal B}\), let w₂ ∈ S₂ and

      • p ∈ L₂(w₂) iff p ∈ L₁(w₁),

      • for all q ∈ V, q ∈ L₂(w₂) iff q ∈ L(w),

      • for all other atoms \(q^{\prime }\), \(q^{\prime } \in L_{2}(w_{2})\) iff \(q^{\prime } \in L_{1}(w_{1})\) iff \(q^{\prime }\in L(w)\).

   2. (ii)

      if \((w_{1}^{\prime }, w_{1})\in R_{1}\), w₂ is constructed based on w₁ and \(w_{2}^{\prime }\in S_{2}\) is constructed based on \(w_{1}^{\prime }\), then \((w_{2}^{\prime }, w_{2})\in R_{2}\).

3. 3.

   delete duplicated states in S₂ and pairs in R₂.

Then we have \({\mathcal M} \leftrightarrow _{\{p\}} {\mathcal M}_{2}\) and \({\mathcal M}_{2} \leftrightarrow _{V} {\mathcal M}_{1}\) by V-bisimulation \({\mathscr{B}}_{1}\) and \({\mathscr{B}}_{2}\), respectively. Moreover, let \(v_{2}(X) = {\mathscr{B}}_{1}(v(X))\) for all \(X \in {\mathcal V}\). Thus, \(({\mathcal M},v) \leftrightarrow _{\{p\}} ({\mathcal M}_{2},v_{2})\) and \(({\mathcal M}_{2},v_{2}) \leftrightarrow _{V} ({\mathcal M}_{1},v_{1})\), and hence \(({\mathcal M}_{2}, s_{2}) \models \textsc {F}_{\mu }(\varphi , p)\). Therefore \(({\mathcal M}_{1}, v_{1}) \models \textsc {F}_{\mu }(\textsc {F}_{\mu }(\varphi , p), V)\).

On the other hand, suppose that \(({\mathcal M}_{1},v_{1})\) is a model of F_μ(F_μ(φ,p),V )

⇒ \(\exists ({\mathcal M}_{2},v_{2})\) s.t. \(({\mathcal M}_{2},v_{2}) \models \textsc {F}_{\mu }(\varphi , p)\) and \(({\mathcal M}_{2},v_{2}) \leftrightarrow _{V} ({\mathcal M}_{1},v_{1})\) by Def. 4

⇒ \(\exists ({\mathcal M},v)\) s.t. \(({\mathcal M},v) \models \varphi\) and \(({\mathcal M},v) \leftrightarrow _{\{p\}} ({\mathcal M}_{2},v_{2})\) by Def. 4.

Therefore, \(({\mathcal M},v) \leftrightarrow _{\{p\} \cup V} ({\mathcal M}_{1},v_{1})\) by (iii) of Proposition 1, and consequently, \(({\mathcal M}_{1},v_{1}) \models \textsc {F}_{\mu }(\varphi , \{p\} \cup V)\). □

Proposition 11 (Homogeneity) Let \(V\subseteq \mathcal A\) and φ be a μ-formula; then, we have

1. (i)

   F_μ(axφ,V ) ≡axF_μ(φ,V ).

2. (ii)

   F_μ(exφ,V ) ≡exF_μ(φ,V ).

3. (iii)

   F_μ(νX.φ,V ) ≡ νX.F_μ(φ,V ) if νX.φ is a μ-sentence.

4. (iv)

   F_μ(μX.φ,V ) ≡ μX.F_μ(φ,V ) if μX.φ is a μ-sentence.

Proof

Let \(({\mathcal M},v)\) (\({\mathcal M}=(S, r,R, L)\)), \(({\mathcal M}_{i}, v_{i})\) (\({\mathcal M}_{i} = (S_{i}, r_{i}, R_{i}, L_{i})\)) with \(i\in \mathbb {N}\), and \(({\mathcal M}^{\prime },v^{\prime })\) (\({\mathcal M}^{\prime }=(S^{\prime }, r^{\prime }, R^{\prime }, L^{\prime })\)) be valuations. We prove (i), (iii), and (ii), (iv) can be proved similarly.

(i) To prove F_μ(axφ,V ) ≡ax(F_μ(φ,V )), we only need to prove Mod(F_μ(axφ,V )) = Mod(axF_μ(φ,V )):

(⇒) \(({\mathcal M},v) \models \textsc {F}_{\mu }(\textsc {a}\textsc {x} \varphi , V)\)

⇒ There is \(({\mathcal M},v) \leftrightarrow _{V} ({\mathcal M}^{\prime }, v^{\prime })\) and \(({\mathcal M}^{\prime }, v^{\prime }) \models \textsc {a}\textsc {x} \varphi\)

⇒ There is \(({\mathcal M},v) \leftrightarrow _{V} ({\mathcal M}^{\prime }, v^{\prime })\) and \(({\mathcal M}^{\prime },r^{\prime \prime }, v^{\prime }) \models \varphi\) for every \((r^{\prime }, r^{\prime \prime }) \in R^{\prime }\)

⇒ For every (r,r₁) ∈ R, there is \((r^{\prime }, r_{1}^{\prime }) \in R^{\prime }\) s.t. \(({\mathcal M},r_{1}, v) \leftrightarrow _{V} ({\mathcal M}^{\prime },r_{1}^{\prime },v^{\prime })\) and \(({\mathcal M}^{\prime },r^{\prime \prime }, v^{\prime }) \models \varphi\) for every \((r^{\prime }, r^{\prime \prime }) \in R^{\prime }\)

⇒ For every (r,r₁) ∈ R, there is \(({\mathcal M},r_{1}, v) \leftrightarrow _{V} ({\mathcal M}^{\prime },r_{1}^{\prime },v^{\prime })\) and \(({\mathcal M}^{\prime },r_{1}^{\prime },v^{\prime }) \models \varphi\)

⇒ For every (r,r₁) ∈ R, \(({\mathcal M},r_{1}, v) \models \textsc {F}_{\mu }(\varphi ,V)\) (IR(F_μ(φ,V ),V ))

⇒ \(({\mathcal M},v)\models \textsc {a} \textsc {x} (\textsc {F}_{\mu }(\varphi ,V))\).

(⇐) \(({\mathcal M},v) \models \textsc {a} \textsc {x} \textsc {F}_{\mu }(\varphi ,V)\)

⇒ For every (r,r₁) ∈ R, \(({\mathcal M},r_{1},v) \models \textsc {F}_{\mu }(\varphi ,V)\)

⇒ For every (r,r₁) ∈ R, \(({\mathcal M}_{r_{1}},r_{1},v) \models \textsc {F}_{\mu }(\varphi ,V)\) (Lemma 1)

⇒ For every (r,r₁) ∈ R, there is \(({\mathcal M}_{r_{1}},r_{1},v) \leftrightarrow _{V} ({\mathcal M}^{\prime }, r^{\prime }, v^{\prime })\) and \(({\mathcal M}^{\prime }, r^{\prime }, v^{\prime }) \models \varphi\)

⇒ For every i ≥ 0, there is \(({\mathcal M}_{r_{i}},r_{i},v) \leftrightarrow _{V} ({\mathcal M}_{i}^{\prime }, r_{i}^{\prime },v_{i}^{\prime })\) and \(({\mathcal M}_{i}^{\prime }, r_{i}^{\prime }, v_{i}^{\prime }) \models \varphi\), where \(\{r_{0}, r_{1}, \dots \} = \{s\mid (r, s) \in R\}\), \({\mathcal M}_{i}^{\prime } = (S_{i}^{\prime }, r_{i}^{\prime }, R_{i}^{\prime }, L_{i}^{\prime })\) (we assume \(S_{i}^{\prime } \cap S_{j}^{\prime }= \emptyset\) when i≠j) and \({\mathscr{B}}_{i}\) is the Var-V-bisimulation between \(({\mathcal M}_{r_{i}},r_{i},v)\) and \(({\mathcal M}_{i}^{\prime }, r_{i}^{\prime }, v_{i}^{\prime })\)

⇒ \(({\mathcal M}^{*}, v^{*}) \leftrightarrow _{V} ({\mathcal M},v)\) and \(({\mathcal M}^{*}, v^{*}) \models \textsc {a}\textsc {x} \varphi\) where \({\mathcal M}^{*} = (S^{*}, r, R^{*},L^{*})\) and

• \(S^{*} = \{r\} \cup \bigcup _{i\geq 0} S_{i}^{\prime }\),

• \(R^{*} = \{(r, r_{i}^{\prime }) \mid i \geq 0\} \cup \bigcup _{i\geq 0} R_{i}^{\prime }\),

• \(L^{*}(s) = \bigcup _{i\geq 0} L_{i}^{\prime }(s)\) for every s ∈ S^∗ and L^∗(r) = L(r),

• for all \(X \in {\mathcal V}\),

  $$v^{*}(X) = \left\{ \begin{array}{ll} \bigcup_{i\geq 0} v_{i}(X), \ \ \qquad \qquad \quad \text{if} r \not \in v(X); \\ \bigcup_{i\geq 0} v_{i}(X) \cup \{r\}, \ \ \ \quad \ \ \ \text{otherwise.} \end{array} \right.$$

⇒ \(({\mathcal M},v) \models \textsc {F}_{\mu }(\textsc {a}\textsc {x} \varphi , V)\).

(iii) (⇒) \(({\mathcal M},v) \models \textsc {F}_{\mu }(\nu X. \varphi , V)\)

⇒ There is \(({\mathcal M}^{\prime }, v^{\prime }) \leftrightarrow _{V} ({\mathcal M},v)\) and \(({\mathcal M}^{\prime },v^{\prime }) \models \nu X. \varphi\)

⇒ \(r^{\prime } \in \bigcup \{S_{1} \subseteq S^{\prime } \mid S_{1} \subseteq \left \|\varphi \right \|_{v^{\prime }[X:=S_{1}]}^{{\mathcal M}^{\prime }}\}\)

⇒ There is \(S_{1} \subseteq S^{\prime }\) s.t. \(S_{1} \subseteq \left \|\varphi \right \|_{v^{\prime }[X:=S_{1}]}^{{\mathcal M}^{\prime }}\), \(r^{\prime }\in S_{1}\), and \(r^{\prime }\in \left \|\varphi \right \|_{v^{\prime }[X:=S_{1}]}^{{\mathcal M}^{\prime }}\)

⇒ \(r^{\prime } \in \left \|\textsc {F}_{\mu }(\varphi ,V)\right \|_{v^{\prime }[X:=S_{1}]}^{{\mathcal M}^{\prime }}\) and \(S_{1} \subseteq \left \|\textsc {F}_{\mu }(\varphi ,V)\right \|_{v^{\prime }[X:=S_{1}]}^{{\mathcal M}^{\prime }}\) since φ⊧F_μ(φ,V )

⇒ \(r^{\prime }\in \bigcup \{S_{1} \subseteq S^{\prime } \mid S_{1} \subseteq \left \|\textsc {F}_{\mu }(\varphi ,V)\right \|_{v^{\prime }[X:=S_{1}]}^{{\mathcal M}^{\prime }}\}\)

⇒ \(({\mathcal M}^{\prime },v^{\prime })\models \nu X. \textsc {F}_{\mu }(\varphi ,V)\)

⇒ \(({\mathcal M},v) \models \nu X. \textsc {F}_{\mu }(\varphi ,V)\) since IR(νX.F_μ(φ,V ),V ).

(⇐) \(({\mathcal M},v)\models \nu X. \textsc {F}_{\mu }(\varphi ,V)\)

⇒ \(r\in \bigcup \{S_{1} \subseteq S \mid S_{1} \subseteq \left \|\textsc {F}_{\mu }(\varphi ,V)\right \|_{v[X:=S_{1}]}^{{\mathcal M}}\}\)

⇒ There is \(S_{1} \subseteq S\) s.t. \(S_{1} \subseteq \left \|\textsc {F}_{\mu }(\varphi ,V)\right \|_{v[X:=S_{1}]}^{{\mathcal M}}\) and r ∈ S₁

⇒ r ∈ S₁ and there is \(S_{1}\subseteq S_{2} \subseteq S\) and \(({\mathcal M}^{\prime },v^{\prime }) \leftrightarrow _{V} ({\mathcal M},v[X:= S_{2}])\) by a Var-V-bisimulation \({\mathscr{B}}\) (with \(v^{\prime }(X) = {\mathscr{B}}(S_{2})\)) s.t. \(({\mathcal M}^{\prime },v^{\prime })\models \varphi\) and \(S_{2} \subseteq \left \|\textsc {F}_{\mu }(\varphi ,V)\right \|_{v[X:=S_{2}]}^{{\mathcal M}}\) since X appears in φ positively

⇒ r ∈ S₂ and there is \(({\mathcal M}^{\prime },v^{\prime }) \leftrightarrow _{V} ({\mathcal M},v[X:= S_{2}])\) s.t. \({\mathscr{B}}(S_{2}) \subseteq \left \|\varphi \right \|_{v^{\prime }[X:={\mathscr{B}}(S_{2})]}^{{\mathcal M}^{\prime }}\)

⇒ There is \({\mathscr{B}}(S_{2}) \subseteq S^{\prime }\) s.t. \({\mathscr{B}}(S_{2}) \subseteq \left \|\varphi \right \|_{v^{\prime }[X:={\mathscr{B}}(S_{2})]}^{{\mathcal M}^{\prime }}\) and \(r^{\prime }\in {\mathscr{B}}(S_{2})\) (\((r,r^{\prime })\in {\mathscr{B}}\))

⇒ \(r^{\prime }\in \bigcup \{S_{1}^{\prime } \subseteq S^{\prime } \mid S_{1}^{\prime } \subseteq \left \|\varphi \right \|_{v^{\prime }[X:=S_{1}^{\prime }]}^{{\mathcal M}^{\prime }}\}\)

⇒ \(({\mathcal M}^{\prime },v^{\prime }) \models \nu X. \varphi\)

⇒ \(({\mathcal M}^{\prime },v^{\prime }) \models \textsc {F}_{\mu }(\nu X. \varphi , V)\) and \(({\mathcal M}^{\prime },v^{\prime }) \leftrightarrow _{\langle {\{X\},V}\rangle } ({\mathcal M},v)\)

⇒ \(({\mathcal M}, v) \models \textsc {F}_{\mu }(\nu X. \varphi , V)\) (Corollary 3, Theorem 4) □

Lemma 2 Let \(V\subseteq \mathcal {A}\) be a set of atoms and \(\varphi _{0} \wedge \textsc {a}\textsc {x} \varphi _{1} \wedge \textsc {e}\textsc {x} \varphi _{2} \wedge {\dots } \wedge \textsc {e} \textsc {x} \varphi _{n}\) be a satisfiable formula with the form (1), then

Proof

It is obvious (by Proposition 11 (i) and (ii)) that

(⇒) \(({\mathcal M},v) \models \textsc {F}_{\mu }(\varphi _{0} \wedge \textsc {a}\textsc {x} \varphi _{1} \wedge \textsc {e}\textsc {x} \varphi _{2} \wedge {\dots } \wedge \textsc {e} \textsc {x} \varphi _{n},V)\)

⇒ There is \(({\mathcal M}, v) \leftrightarrow _{V} ({\mathcal M}^{\prime }, v^{\prime })\) s.t. \(({\mathcal M}^{\prime },v^{\prime }) \models \varphi _{0} \wedge \textsc {a}\textsc {x} \varphi _{1} \wedge \textsc {e}\textsc {x} \varphi _{2} \wedge {\dots } \wedge \textsc {e} \textsc {x} \varphi _{n}\)

⇒ \(({\mathcal M}^{\prime },v^{\prime }) \models \varphi _{0}\), \(({\mathcal M}^{\prime }, v^{\prime }) \models \textsc {a}\textsc {x} \varphi _{1}\), and \(({\mathcal M}^{\prime },v^{\prime }) \models \textsc {e}\textsc {x} \varphi _{i}\) with 2 ≤ i ≤ n

⇒ \(({\mathcal M}^{\prime },v^{\prime }) \models \varphi _{0}\), \(({\mathcal M}^{\prime }, v^{\prime }) \models \textsc {a}\textsc {x} \varphi _{1}\), and \(({\mathcal M}^{\prime },v^{\prime }) \models \textsc {e}\textsc {x} (\varphi _{i} \wedge \varphi _{1})\) with 2 ≤ i ≤ n since \(({\mathcal M},v) \models \textsc {a}\textsc {x} \varphi _{1}\)

⇒ \(({\mathcal M},v) \models \textsc {F}_{\mu }(\varphi _{0},V)\), \(({\mathcal M}, v) \models \textsc {F}_{\mu }(\textsc {a}\textsc {x} \varphi _{1}, V)\), and \(({\mathcal M},v) \models \textsc {F}_{\mu }(\textsc {e}\textsc {x} (\varphi _{i} \wedge \varphi _{1}), V)\) with 2 ≤ i ≤ n since \(({\mathcal M}, v) \leftrightarrow _{V} ({\mathcal M}^{\prime }, v^{\prime })\), IR(F_μ(φ₀,V ),V ), IR(F_μ(axφ₁,V ),V ), and IR(F_μ(ex(φ_i ∧ φ₁),V ),V )

⇒ \(({\mathcal M},v) \models \textsc {F}_{\mu }(\varphi _{0}, V) \wedge \textsc {F}_{\mu }(\textsc {a}\textsc {x} \varphi _{1}, V) \wedge \bigwedge _{2\leq i\leq n} \textsc {F}_{\mu }(\textsc {e}\textsc {x}(\varphi _{i} \wedge \varphi _{1}), V)\)

(⇐) \(({\mathcal M},v) \models \textsc {F}_{\mu }(\varphi _{0}, V) \wedge \textsc {F}_{\mu }(\textsc {a}\textsc {x} \varphi _{1}, V) \wedge \bigwedge _{2\leq i\leq n} \textsc {F}_{\mu }(\textsc {e}\textsc {x}(\varphi _{i} \wedge \varphi _{1}), V)\) with \({\mathcal M}=(S,r, R,L)\)

⇒ \(({\mathcal M},v) \models \textsc {F}_{\mu }(\varphi _{0}, V) \wedge \textsc {a}\textsc {x}\textsc {F}_{\mu }(\varphi _{1}, V) \wedge \bigwedge _{2\leq i\leq n} \textsc {e}\textsc {x} \textsc {F}_{\mu }(\varphi _{i} \wedge \varphi _{1}, V)\)

⇒ \(({\mathcal M},r,v) \models \textsc {F}_{\mu }(\varphi _{0}, V)\), for every \((r, r^{\prime })\in R\), \(({\mathcal M}, r^{\prime }, v) \models \textsc {F}_{\mu }(\varphi _{1}, V)\), and there is \((r, r^{\prime \prime })\in R\) s.t. \(({\mathcal M},r^{\prime \prime }, v) \models \textsc {F}_{\mu }(\varphi _{i} \wedge \varphi _{1}, V)\) for each 2 ≤ i ≤ n

⇒ \(({\mathcal M},r,v) \models \textsc {F}_{\mu }(\varphi _{0}, V)\), for every \((r, r^{\prime })\in R\), \(({\mathcal M}_{r^{\prime }}, r^{\prime }, v) \models \textsc {F}_{\mu }(\varphi _{1}, V)\), and there is \((r, r^{\prime \prime })\in R\) s.t. \(({\mathcal M}_{r^{\prime \prime }},r^{\prime \prime }, v) \models \textsc {F}_{\mu }(\varphi _{i} \wedge \varphi _{1}, V)\) for each 2 ≤ i ≤ n (Lemma 1)

⇒ There is \(({\mathcal M}^{\prime },v) \models \varphi _{0}\) and \(({\mathcal M}^{\prime },v) \leftrightarrow _{V} ({\mathcal M},v)\) with \({\mathcal M}^{\prime }=(S,r,R,L^{\prime })\), for every (r,r_j) ∈ R, there is \(({\mathcal M}_{j}^{\prime },r_{j}^{\prime },v_{j}^{\prime })\) s.t. \(({\mathcal M}_{j}^{\prime },r_{j}^{\prime },v_{j}^{\prime }) \leftrightarrow _{V} ({\mathcal M}_{r_{j}},r_{j}, v)\) and \(({\mathcal M}_{j}^{\prime },r_{j}^{\prime },v_{j}^{\prime }) \models \varphi _{1}\), and for each (r,r_j) ∈ R with \(({\mathcal M}_{r_{j}},r_{j}, v) \models \textsc {F}_{\mu }(\varphi _{i} \wedge \varphi _{1}, V)\) and 2 ≤ i ≤ n, there is \(({\mathcal M}_{j}^{\prime }, r_{j}^{\prime }, v_{j}^{\prime }) \leftrightarrow _{V} ({\mathcal M}_{r_{j}},r_{j},v)\) s.t. \(({\mathcal M}_{j}^{\prime }, r_{j}^{\prime }, v_{j}^{\prime })\models \varphi _{i} \wedge \varphi _{1}\) (j ≥ 0, and we assume S_x ∩ S_y = ∅ when x≠y), where \(\{r_{0}, r_{1}, \dots \} = \{r^{\prime }\mid (r,r^{\prime })\in R\}\), \({\mathcal M}_{j}^{\prime }=(S_{j}^{\prime },r_{j}^{\prime }, R_{j}^{\prime }, L_{j}^{\prime })\)

⇒ There is \(({\mathcal M}^{*},v^{*}) \leftrightarrow _{V} ({\mathcal M},v)\) s.t. \(({\mathcal M}^{*}, v^{*}) \models \varphi _{0} \wedge \textsc {a}\textsc {x} \varphi _{1} \wedge \bigwedge _{2\leq i\leq n} \textsc {e}\textsc {x}(\varphi _{i} \wedge \varphi _{1})\), where \({\mathcal M}^{*}=(S^{*},r, R^{*}, L^{*})\) and

• \(S^{*} = \{r\} \cup \bigcup _{j\geq 0} S_{j}^{\prime }\),

• \(R^{*} = \{(r,r_{j}^{\prime }) \mid j \geq 0\}\cup \bigcup _{j\geq 0} R_{j}^{\prime }\),

• \(L^{*}(s) = L_{j}^{\prime }(s)\) for \(s\in S_{j}^{\prime }\) and \(L^{*}(r) = L^{\prime }(r)\), and

• for all \(X \in {\mathcal V}\),

  $$v^{*}(X) = \left\{ \begin{array}{ll} \bigcup_{i\geq 0} v_{j}^{\prime}(X), \ \ \qquad \qquad \quad \text{if} r \not \in v(X); \\ \bigcup_{i\geq 0} v_{j}^{\prime}(X) \cup \{r\}, \ \ \ \quad \ \ \ \text{otherwise.} \end{array} \right.$$

⇒ \(({\mathcal M},v) \models \textsc {F}_{\mu }(\varphi _{0} \wedge \textsc {a}\textsc {x} \varphi _{1} \wedge \textsc {e}\textsc {x} \varphi _{2} \wedge {\dots } \wedge \textsc {e} \textsc {x} \varphi _{n},V)\). □

Proposition 12 Let \(V\subseteq \mathcal {A}\) be a set of atoms and φ a μ-formula in x-class. There is a μ-formula ψ in x-class such that ψ ≡F_μ(φ,V ).

Proof

Suppose the degree of temporal operators in φ is degree(φ) = n; we prove this result by inducting the degree n of φ.

Base case. :

n = 0. φ is a formula that may contain free variables. Then, we have F_μ(φ,V ) = Forget(φ,V ) by Theorem 7 and Proposition 8 (vi).

Step case. :

Suppose F_μ(φ₁,V ) is in x-class for any formula φ₁ with degree(φ₁) ≤ k. We prove F_μ(φ₂,V ) is in x-class for any formula φ₂ with degree(φ₂) = k + 1.

φ₂ can be transformed into the disjunction (denoted as \(\varphi ^{\prime }\)) of formulas with the form (1) and \(degree(\varphi ^{\prime }) \leq k+1\) since there will not introduce new nested modal operators during the transformation.

Without loss of generality, suppose

and φ_i,j (1 ≤ i ≤ x, 1 ≤ j ≤ n_i) are formulas with degree(φ_i,j) ≤ k.

According to Lemma 2 and Proposition 8, we have

Therefore, we have \(\textsc {F}_{\mu }(\varphi ^{\prime }, V)\) in x-class by induction hypothesis. □

Proposition 13 Let φ be a μ-sentence and \(p\in \mathcal {A}\). If φ is a disjunctive μ-formula, then F_μ(φ,{p}) can be computed in linear time in the size of φ.

Proof

F_μ(φ,{p}) can be computed by simultaneously substituting the literals p and ¬p with ⊤ provided the context φ is disjunctive.

In this case, we need only to scan φ once, and this can be done in linear time in the size of φ. □

Proposition 14 (Model Checking) Given a finite Kripke structure \({\mathcal M}\), a μ-sentence φ, and \(V\subseteq \mathcal {A}\). We have:

1. (i)

   deciding \({\mathcal M} \models ^{?} \textsc {F}_{\mu }(\varphi , V)\) is in Exptime,

2. (ii)

   if φ is a disjunctive μ-formula, then deciding \({\mathcal M} \models ^{?} \textsc {F}_{\mu }(\varphi , V)\) is in NP∩co-NP.

Proof

For a given μ-formula, constructing a μ-automaton (also called modal automaton [49]) A_φ can be done in polynomial time if it is a disjunctive μ-formula, else in Exptime^{Footnote 1}. We prove (ii), then (i) can be proved similarly.

Let A_φ be a μ-automaton such that, for any Kripke structure \({\mathcal N}\), A_φ accepts \({\mathcal N}\) iff \({\mathcal N} \models \varphi\), where A_φ = (Q,Σ_p,Σ_r,q₀,δ,Ω) with Σ_p = Var(φ). Without loss of generality, we assume \(V \subseteq \textit {Var}(\varphi )\) and V = {p}. Therefore we can construct a μ-automaton \({\mathcal B}= (Q, {\Sigma }_{p} - V, {\Sigma }_{r}, q_{0}, \delta ^{\prime }, {\Omega })\) such that, for any q ∈ Q and \(L\subseteq {\Sigma }_{p} - V\),

It has been proved in [45] that, for each Kripke structure \({\mathcal N}\), \({\mathcal B}\) accepts \({\mathcal N}\) iff there is a model \({\mathcal N}^{\prime }\) of φ s.t. \({\mathcal N} \leftrightarrow _{\{p\}} {\mathcal N}^{\prime }\), i.e. \({\mathcal B}\) corresponds to a μ-sentence which is equivalent to F_μ(φ,V ) by the definition of forgetting in μ-calculus.

In this case, the problem \({\mathcal M} \models ^{?} \textsc {F}_{\mu }(\varphi , V)\) is reduced to decide whether \({\mathcal B}\) accepts \({\mathcal M}\). The automaton \({\mathcal B}\) accepts a Kripke structure \({\mathcal M}=(S, r, R,L)\) from the root r iff Eve has a winning strategy in the parity game \({\mathcal G}({\mathcal M}, {\mathscr{B}})\) from the position (r,q⁰), which is in NP∩co-NP [49]. □

Theorem 15 (Entailment) Let φ and ψ be two μ-sentences and V be a set of atoms. Then, we have.

1. (i)

   Deciding F_μ(φ,V )⊧^?ψ is Exptime-complete,

2. (ii)

   Deciding \(\psi \models ^{?} \textsc {F}_{\mu }(\varphi , V)\) is in Exptime,

3. (iii)

   Deciding \(\textsc {F}_{\mu }(\varphi , V) \models ^{?} \textsc {F}_{\mu }(\psi , V)\) is in Exptime.

Proof

Membership. Let A_φ and A_ψ be the μ-automaton of φ and ψ respectively, we can construct the μ-automaton \({\mathcal B}\) of F_μ(φ,V ) from A_φ by the proof of Proposition 14. By Proposition 7.3.2 in [53] , we can obtain the complement C of A_ψ in linear time, and then the intersection \(A_{C \cap {\mathcal B}}\) between C and \({\mathcal B}\) in linear time. In this case, the F_μ(φ,V )⊧^?ψ is reduced to decide whether the language accepted by \(A_{C \cap {\mathcal B}}\) is empty, which is Exptime-complete (Theorem 7.5.1 of [53]).

Therefore, deciding F_μ(φ,V )⊧^?ψ is in Exptime.

Hardness. F_μ(φ,V )⊧ψ if and only if ¬F_μ(φ,V ) ∨ ψ is valid. Let ψ ≡⊥, F_μ(φ,V )⊧⊥ if and only if φ⊧⊥, which is Exptime-complete [49].

(ii) This can be similarly proved as that of (i).

(iii) can be similarly proved as that of (ii) since F_μ(φ,V )⊧F_μ(ψ,V ) if and only if φ⊧F_μ(ψ,V ). □

Appendix C:: Proofs in Section 5

Proposition 17 (dual) Let V,q,φ and ψ be defined as in Definition 5. Then, ψ is an SNC (a WSC) of q on V under φ iff ¬ψ is a WSC (an SNC) of ¬q on V under φ.

Proof

1. (i)

   Suppose that ψ is the SNC of q and \(\psi ^{\prime }\) is any SC of ¬q.

   \(\varphi \models q \rightarrow \psi\)

   ⇒ \(\varphi \models \neg \psi \rightarrow \neg q\).

   This shows that ¬ψ is an SC of ¬q on V under φ.

   \(\varphi \models \psi ^{\prime } \rightarrow \neg q\)

   ⇒ \(\varphi \models q \rightarrow \neg \psi ^{\prime }\), i.e., \(\neg \psi ^{\prime }\) is an NC of q on V under φ

   ⇒ \(\varphi \models \psi \rightarrow \neg \psi ^{\prime }\) by assumption

   ⇒ \(\varphi \models \psi ^{\prime } \rightarrow \neg \psi\).

   The proof of the other part of the proposition is similar.

2. (ii)

   The WSC case can be proved in a similar way to the SNC case.

□

Lemma 4

Let φ and α be two μ-formulas, and q be an atom with q∉Var(φ) ∪Var(α). Then, \(\textsc {F}_{\mu }(\varphi \wedge (q\leftrightarrow \alpha ), \{q\})\equiv \varphi\).

Proof

Let \(\varphi^{\prime } =\varphi \wedge (q\leftrightarrow \alpha )\). For each model \(({\mathcal M},v)\) of \(\textsc {F}_{\mu }(\varphi ^{\prime }, \{q\})\), there is an valuation \(({\mathcal M}^{\prime },v^{\prime })\) s.t. HCode \(({\mathcal M},v)\leftrightarrow _{\{q\}}({\mathcal M}^{\prime },v^{\prime })\) and \(({\mathcal M}^{\prime },v^{\prime }) \models \varphi ^{\prime }\). It’s evident that \(({\mathcal M}^{\prime },v^{\prime }) \models \varphi\), and then \(({\mathcal M},v) \models \varphi\) since IR(φ,{q}) and \(({\mathcal M},v)\leftrightarrow _{\{q\}}({\mathcal M}^{\prime },v^{\prime })\).

Let \(({\mathcal M},v) \in \textit {Mod}(\varphi )\) with \({\mathcal M}=(S, s, R, L)\). We construct \(({\mathcal M}^{\prime },v^{\prime })\) with \({\mathcal M}^{\prime } = (S, s, R, L^{\prime })\) as follows:

It is obvious that \({\mathcal M}^{\prime } \leftrightarrow _{\{q\}} {\mathcal M}\), then there is a {q}-bisimulation \({\mathscr{B}}\) between \({\mathcal M}\) and \({\mathcal M}^{\prime }\). Moreover, let \(v^{\prime }(X) = {\mathscr{B}}(v(X))\) for each \(X\in {\mathcal V}\).

Therefore, we have \(({\mathcal M}^{\prime },v^{\prime }) \models \varphi\), \(({\mathcal M}^{\prime },v^{\prime }) \models q\leftrightarrow \alpha\), and \(({\mathcal M},v)\leftrightarrow _{\{q\}}({\mathcal M}^{\prime },v^{\prime })\). Hence, \(({\mathcal M}^{\prime },v^{\prime }) \models \varphi \wedge (q\leftrightarrow \alpha )\), and then \(({\mathcal M},v) \models \textsc {F}_{\mu } (\varphi \wedge (q\leftrightarrow \alpha ), \{q\})\) by \(({\mathcal M},v)\leftrightarrow _{\{q\}}({\mathcal M}^{\prime },v^{\prime })\) and \(\text {IR}(\textsc {F}_{\mu } (\varphi \wedge (q\leftrightarrow \alpha ), q), \{q\})\). □

Proposition 18 Let Γ and α be two μ-formulas, \(V \subseteq \textit {Var}(\alpha ) \cup \textit {Var}({\Gamma })\) and q be a new atom not in Γ and α. Then, a formula φ with\(\textit {Var}(\varphi ) \subseteq V\) is the SNC (WSC) of α on V under Γ iff it is the SNC (WSC) of q on V under\({\Gamma }^{\prime } = {\Gamma } \cup \{q \leftrightarrow \alpha \}\).

Proof

We prove this for SNC. The case for WSC is similar. Let SNC(φ,β,V,Γ) denote that φ is the SNC of β on V under Γ, and NC(φ,β,V,Γ) denote that φ is the NC of β on V under Γ, in which β is a formula.

(⇒) We will show \(\textit {SNC}(\varphi ,\alpha ,V,{\Gamma })\Rightarrow \textit {SNC}(\varphi ,q,V,{\Gamma }^{\prime })\). Suppose \(\varphi ^{\prime }\) is any NC of q on V under \({\Gamma }^{\prime }\).

\({\Gamma } \models \alpha \rightarrow \varphi\) (known)

⇒ \({\Gamma } \wedge (q \leftrightarrow \alpha ) \models \alpha \rightarrow \varphi\)

⇒ \({\Gamma }^{\prime } \models q \rightarrow \varphi\) (q ≡ α)

\({\Gamma }^{\prime } \models q \rightarrow \varphi ^{\prime }\) (assumption)

⇒ \({\Gamma }^{\prime } \models \alpha \rightarrow \varphi ^{\prime }\) (q ≡ α)

⇒ \(\textsc {F}_{\mu }({\Gamma }^{\prime }, \{q\}) \models \alpha \rightarrow \varphi ^{\prime }\) (\(\text {IR}(\alpha \rightarrow \varphi ^{\prime }, \{q\})\), (PP))

⇒ \({\Gamma } \models \alpha \rightarrow \varphi ^{\prime }\) (Lemma 4)

⇒ \({\Gamma } \models \varphi \rightarrow \varphi ^{\prime }\) (known: SNC(φ,α,V,Γ))

⇒ \({\Gamma }^{\prime } \models \varphi \rightarrow \varphi ^{\prime }\).

In total, φ is an NC of q on V under \({\Gamma }^{\prime }\) and for any NC \(\varphi ^{\prime }\) of q on V under \({\Gamma }^{\prime }\), there is \({\Gamma }^{\prime } \models \varphi \rightarrow \varphi ^{\prime }\). Therefore, \(\textit {SNC}(\varphi ,q,V,{\Gamma }^{\prime })\) holds.

(⇐) We will show that \(\textit {SNC}(\varphi ,q,V,{\Gamma }^{\prime })\Rightarrow \textit {SNC}(\varphi ,\alpha ,V,{\Gamma })\). Suppose \(\varphi ^{\prime }\) is any NC of α on V under Γ.

\({\Gamma }^{\prime } \models q \rightarrow \varphi\) (known)

⇒ \({\Gamma }^{\prime } \models \alpha \rightarrow \varphi\) (q ≡ α)

⇒ \(\textsc {F}_{\mu }({\Gamma }^{\prime }, \{q\}) \models \alpha \rightarrow \varphi\) (\(\text {IR}(\alpha \rightarrow \varphi , \{q\})\), (PP))

⇒ \({\Gamma } \models \alpha \rightarrow \varphi\) (Lemma 4)

\({\Gamma } \models \alpha \rightarrow \varphi ^{\prime }\) (assumption)

⇒ \({\Gamma }^{\prime } \models \alpha \rightarrow \varphi ^{\prime }\)

⇒ \({\Gamma }^{\prime } \models q \rightarrow \varphi ^{\prime }\) (q ≡ α)

⇒ \({\Gamma }^{\prime } \models \varphi \rightarrow \varphi ^{\prime }\) (known: \(\textit {SNC}(\varphi ,q,V,{\Gamma }^{\prime })\))

⇒ \(\textsc {F}_{\mu }({\Gamma }^{\prime }, \{q\}) \models \varphi \rightarrow \varphi ^{\prime }\) (\(\text {IR}(\varphi \rightarrow \varphi ^{\prime }, \{q\})\), (PP))

⇒ \({\Gamma } \models \varphi \rightarrow \varphi ^{\prime }\) (Lemma 4)

In total, φ is an NC of α on V under Γ and for any NC \(\varphi ^{\prime }\) of α on V under Γ, there is \({\Gamma } \models \varphi \rightarrow \varphi ^{\prime }\). Therefore, SNC(φ,α,V,Γ) holds. □

Proposition 20 Let Γ be a μ-formula, q be an atom, and \(V\subseteq \textit {Var}({\Gamma })\).

1. (i)

   If φ is an NC of q on V under Γ, and ψ is the WSC of q on V under Γ ∧ φ, then φ ∧ ψ is the WSC of q on V under Γ.

2. (ii)

   If ψ is an SC of q on V under Γ and φ is the SNC of q on V under Γ ∧¬ψ, then φ ∨ ψ is the SNC of q on V under Γ.

Proof

1. (i)

   Suppose \(\varphi ^{\prime }\) is an SC of q on V under Γ, i.e. \({\Gamma } \models \varphi ^{\prime } \rightarrow q\).

   \({\Gamma } \wedge \varphi \models \psi \rightarrow q\) (known)

   ⇒ Γ∧ φ ∧ ψ⊧q

   ⇒ \({\Gamma } \models \varphi \wedge \psi \rightarrow q\).

   \({\Gamma } \models q \rightarrow \varphi\) and \({\Gamma } \models \varphi ^{\prime } \rightarrow q\) (known, assumption)

   ⇒ \({\Gamma } \models \varphi ^{\prime } \rightarrow \varphi\) and \({\Gamma } \wedge \varphi \models \varphi ^{\prime } \rightarrow q\)

   ⇒ \({\Gamma } \wedge \varphi ^{\prime } \models \varphi\) and \({\Gamma } \wedge \varphi \models \varphi ^{\prime } \rightarrow \psi\) since ψ is the WSC of q on V under Γ ∧ φ

   ⇒ \({\Gamma } \wedge \varphi ^{\prime } \models \varphi\) and \({\Gamma } \wedge \varphi ^{\prime } \models \psi\)

   ⇒ \({\Gamma } \models \varphi ^{\prime }\rightarrow \varphi \wedge \psi\).

   Therefore, φ ∧ ψ is an SC of q on V under Γ. In addition, for any SC \(\varphi ^{\prime }\) of q on V under Γ, there is \({\Gamma } \models \varphi ^{\prime }\rightarrow \varphi \wedge \psi\). Hence, φ ∧ ψ is the WSC of q on V under Γ.

2. (ii)

   Let SNC(φ,β,V,Γ) (WSC(φ,β,V,Γ)) denote that φ is the SNC (WSC) of β on V under Γ, and NC(φ,β,V,Γ) (SC(φ,β,V,Γ)) denote that φ is an NC (SC) of β on V under Γ, in which β is a formula.

\({\Gamma } \models \psi \rightarrow q\) (known)

⇒ \({\Gamma } \models \neg q \rightarrow \neg \psi\), i.e., NC(¬ψ,¬q,V,Γ)

SNC(φ,q,V,Γ ∧¬ψ) implies WSC(¬φ,¬q,V,Γ ∧¬ψ) by Proposition 17.

NC(¬ψ,¬q,V,Γ) and WSC(¬φ,¬q,V,Γ ∧¬ψ)

⇒ \(\textit {NC}(\neg \psi , q^{\prime }, V, {\Gamma } \wedge (q^{\prime } \leftrightarrow \neg q))\) and \(\textit {WSC}(\neg \varphi , q^{\prime },V,{\Gamma } \wedge (q^{\prime } \leftrightarrow \neg q) \wedge \neg \psi )\) with \(q^{\prime }\) is a new atom not in Γ ∧¬q ∧¬ψ (Prop. 18)

⇒ \(\textit {WSC}(\neg \varphi \wedge \neg \psi , q^{\prime },V,{\Gamma } \wedge (q^{\prime } \leftrightarrow \neg q))\) (i)

⇔ WSC(¬φ ∧¬ψ,¬q,V,Γ) (Prop. 18)

⇒ SNC(φ ∨ ψ,q,V,Γ) (Prop. 17) □

Theorem 21 Let ψ and φ be two μ-sentences, \(variable(\varphi ) \subseteq V\subseteq \textit {Var}(\varphi )\), q ∈Var(φ) − V and \(\textit {Var}(\psi ) \subseteq V\). Then, we have

1. (i)

   deciding whether ψ is an NC (SC) of q on V under φ is Exptime-complete;

2. (ii)

   deciding whether ψ is an SNC (a WSC) of q on V under φ is in Exptime.

Proof

We prove the NC (SNC) part, the SC (WSC) part can be proved similarly.

1. (i)

   ψ is an NC of q on V under φ iff \(\varphi \models q \rightarrow \psi\), deciding whether \(\varphi \models q \rightarrow \psi\) is Exptime-complete [49].

2. (ii)

   ψ is an SNC of q on V under φ iff ψ ≡F_μ(φ ∧ q, (Var(φ) ∪{q}) − V ). According to Corollary 16, it is in Exptime.

□

Theorem 22 Let \(V \subseteq \mathcal A\) and φ be a μ-sentence. Then there is a μ-sentence ψ such that:

where both \({\mathcal M}\) and \({\mathcal M}^{\prime }\) are initial structures.

Proof

Let ψ = F_μ(φ,V ). For each initial structure \({\mathcal M}\), if \({\mathcal M} \models \psi\) then there is an initial structure \({\mathcal M}^{\prime }\) s.t. \({\mathcal M}^{\prime } \models \varphi\) and \({\mathcal M} \leftrightarrow _{V} {\mathcal M}^{\prime }\).

In addition, for any initial structure \({\mathcal M}\) and \({\mathcal M}^{\prime } \in \textit {Mod}(\varphi )\) with \({\mathcal M} \leftrightarrow _{V} {\mathcal M}^{\prime }\), there is \({\mathcal M} \models \psi\) due to IR(ψ,V ). □

Theorem 24 Let Γ and φ be μ-sentences. Then, we have:

Proof

\({\mathcal M}^{\prime }\in \textit {Mod}({\Gamma } \diamond _{\mu } \varphi )\)

⇔ There is \({\mathcal M} \models {\Gamma }\) and a minimal set \(V_{min} \subseteq \mathcal {A}\) s.t. \({\mathcal M}^{\prime } \in \textit {Mod}(\textsc {F}_{\mu }({\mathcal F}_{\mathcal {A}}({\mathcal M})\), V_min) ∧ φ)

⇔ There is \({\mathcal M} \models {\Gamma }\) and \(V_{min}\subseteq \mathcal {A}\) s.t. \({\mathcal M} \leftrightarrow _{V_{min}} {\mathcal M}^{\prime }\), \({\mathcal M}^{\prime } \models \varphi\), and V_min is a minimal subset of \(\mathcal {A}\) s.t. \(\textsc {F}_{\mu }({\mathcal F}_{\mathcal {A}}({\mathcal M})\), V_min) ∧ φ consistent

⇔ There is \({\mathcal M} \models {\Gamma }\) s.t. for all \({\mathcal M}^{\prime \prime }\models \varphi\), we have \({\mathcal M}^{\prime } \leq _{{\mathcal M}} {\mathcal M}^{\prime \prime }\)

⇔ \({\mathcal M}^{\prime } \in Min(\textit {Mod}(\varphi ), \leq _{{\mathcal M}})\). □

Theorem 25 Knowledge update operator ◇_μ satisfies Katsuno and Mendelzon’s update postulates (U1)-(U8).

Proof

For (U1), we know that \(\textit {Mod}({\Gamma } \diamond _{\mu } \varphi ) \subseteq \textit {Mod}(\varphi )\) by Theorem 24, hence Γ ◇_μφ⊧φ.

(U2). \({\mathcal M}^{\prime }\in \textit {Mod}({\Gamma } \diamond _{\mu } \varphi )\)

⇔ There is \({\mathcal M} \models {\Gamma }\) s.t. for any \({\mathcal M}^{\prime \prime } \models \varphi\) and \(V \subseteq \mathcal {A}\), \({\mathcal M}^{\prime \prime } \leftrightarrow _{V} {\mathcal M}\) implies \({\mathcal M}^{\prime } \leftrightarrow _{V} {\mathcal M}\)

⇔ There is \({\mathcal M} \models {\Gamma }\) and V_min = ∅ s.t. \({\mathcal M}^{\prime } \leftrightarrow _{V_{min}} {\mathcal M}\) due to Γ⊧φ

⇔ \({\mathcal M}^{\prime }\models {\Gamma }\).

It is easy to show that ◇_μ satisfies (U3) and (U4).

(U5). \({\mathcal M}^{\prime }\models ({\Gamma } \diamond _{\mu } \varphi ) \wedge \psi\)

⇒ There is \({\mathcal M} \models {\Gamma }\) s.t. for any \({\mathcal M}^{\prime \prime } \models \varphi \wedge \psi\) and \(V \subseteq \mathcal {A}\), \({\mathcal M}^{\prime \prime } \leftrightarrow _{V} {\mathcal M}\) implies \({\mathcal M}^{\prime } \leftrightarrow _{V} {\mathcal M}\)

⇒ There is \({\mathcal M} \models {\Gamma }\), \(V_{min} \subseteq \mathcal {A}\) s.t. \({\mathcal M}^{\prime } \leftrightarrow _{V_{min}} {\mathcal M}\) with V_min is a minimal subset of \(\mathcal {A}\) satisfy those properties, and \({\mathcal M}^{\prime } \models \varphi \wedge \psi\)

⇒ \({\mathcal M}^{\prime } \models {\Gamma } \diamond _{\mu } (\varphi \wedge \psi )\).

(U6). \({\mathcal M}^{\prime }\models {\Gamma } \diamond _{\mu } \varphi\)

⇔ There is \({\mathcal M} \models {\Gamma }\) s.t. for any \({\mathcal M}^{\prime \prime } \models \varphi\) and \(V \subseteq \mathcal {A}\), \({\mathcal M}^{\prime \prime } \leftrightarrow _{V} {\mathcal M}\) implies \({\mathcal M}^{\prime } \leftrightarrow _{V} {\mathcal M}\)

⇔ There is \({\mathcal M} \models {\Gamma }\) and \(V_{min} \subseteq \mathcal {A}\) s.t. \({\mathcal M}^{\prime } \leftrightarrow _{V_{min}} {\mathcal M}\) with V_min is a minimal subset of \(\mathcal {A}\) s.t. \(\textsc {F}_{\mu }({\mathcal F}_{\mathcal {A}}({\mathcal M}_{1}), V_{min}) \wedge \varphi\) and \(\textsc {F}_{\mu }({\mathcal F}_{\mathcal {A}}({\mathcal M}_{1}), V_{min}) \wedge \psi\) consistent due to Γ ◇_μφ⊧ψ and Γ ◇_μψ⊧φ (Otherwise, suppose that V ⊂ V_min s.t. \(\textsc {F}_{\mu }({\mathcal F}_{\mathcal {A}}({\mathcal M}_{1}), V) \wedge \psi\) is consistent as well. Then, \(\textsc {F}_{\mu }({\mathcal F}_{\mathcal {A}}({\mathcal M}_{1}), V)\) ∧ φ should also be consistent by Γ ◇_μφ⊧ψ, which contradicts to the fact that V_min is the minimal set of atoms s.t. \(\textsc {F}_{\mu }({\mathcal F}_{\mathcal {A}}({\mathcal M}_{1}), V_{min}) \wedge \varphi\) is consistent.)

⇔ There is \({\mathcal M} \models {\Gamma }\) s.t. for any \({\mathcal M}^{\prime \prime } \models \psi\) and \(V \subseteq \mathcal {A}\), \({\mathcal M}^{\prime \prime } \leftrightarrow _{V} {\mathcal M}\) implies \({\mathcal M}^{\prime } \leftrightarrow _{V} {\mathcal M}\)

⇔ \({\mathcal M}^{\prime } \models {\Gamma } \diamond _{\mu } \psi\)

(U7). \({\mathcal M}^{\prime } \models ({\Gamma } \diamond _{\mu } \varphi ) \wedge ({\Gamma } \diamond _{\mu } \psi )\) and \({\mathcal M}\) is the unique model of Γ

⇒ There is two minimal set \(V_{1}, V_{2} \subseteq \mathcal {A}\) s.t. \({\mathcal M} \leftrightarrow _{V_{1}} {\mathcal M}^{\prime }\) and \({\mathcal M} \leftrightarrow _{V_{2}} {\mathcal M}^{\prime }\)

⇒ There is two minimal set \(V_{1}, V_{2} \subseteq \mathcal {A}\) s.t. \({\mathcal M}^{\prime } \models \textsc {F}_{\mu }({\mathcal F}_{\mathcal {A}}({\mathcal M}), V_{1}) \wedge \varphi\) and \({\mathcal M}^{\prime } \models \textsc {F}_{\mu }({\mathcal F}_{\mathcal {A}}({\mathcal M}),\) V₂) ∧ ψ consistent

⇒ \({\mathcal M}^{\prime } \models \textsc {F}_{\mu }({\mathcal F}_{\mathcal {A}}({\mathcal M}), V_{1} \cap V_{2})\), \({\mathcal M}^{\prime } \leftrightarrow _{V_{1} \cap V_{2}} {\mathcal M}\), and V₁ = V₂

⇒ V₁ is a minimal set s.t. \(\textsc {F}_{\mu }({\mathcal F}_{\mathcal {A}}({\mathcal M}), V_{1}) \wedge (\varphi \vee \psi )\) is consistent (Otherwise, suppose that V₃ ⊂ V₁ s.t. \(\textsc {F}_{\mu }({\mathcal F}_{\mathcal {A}}({\mathcal M}), V_{3}) \wedge (\varphi \vee \psi )\) is satisfiable. Then \(\textsc {F}_{\mu }({\mathcal F}_{\mathcal {A}}({\mathcal M}), V_{3}) \wedge \varphi\) or \(\textsc {F}_{\mu }({\mathcal F}_{\mathcal {A}}({\mathcal M}), V_{3}) \wedge \psi\) is satisfiable. Without loss of generality, suppose that \(\textsc {F}_{\mu }({\mathcal F}_{\mathcal {A}}({\mathcal M}), V_{3}) \wedge \varphi\) is satisfiable, V₁ is not the minimal set, a contradiction.)

⇒ \({\mathcal M}^{\prime } \models {\Gamma } \diamond _{\mu } (\varphi \vee \psi )\).

(U8). \({\mathcal M} \models ({\Gamma }_{1} \vee {\Gamma }_{2}) \diamond _{\mu } \varphi\)

⇔ There is an \({\mathcal M}_{1} \models {\Gamma }_{1}\) (or \({\mathcal M}_{1} \models {\Gamma }_{2}\)) and a minimal set V_min s.t. \({\mathcal M} \leftrightarrow _{V_{min}} {\mathcal M}_{1}\)

⇔ \({\mathcal M} \models ({\Gamma }_{1} \diamond _{\mu } \varphi ) \vee ({\Gamma }_{2} \diamond _{\mu } \varphi )\). □

Reprints and permissions