I am trying to understand the operators $E_G$ (everybody knows) and $D_G$ (distributed knowledge) when they are stacked on top of each other.
From looking at the semantics of $E_G$ and $D_G$ it looks to me like the statements:
- $E_G D_G \phi$
- $D_G E_G \phi$
- $E_G \phi$
are all equivalent. I.e. If in state $s$ one of them hold, they all hold. This seems intuitively wrong to me, but I cannot find out why.
My reasoning (warning it is messy and very likely wrong :) ) arose while trying to prove that the formula $E_G D_G \phi \rightarrow D_G E_G \phi$ valid.
My Reasoning:
Pick an arbitrary model $M$ and state $s$ such that $(M,s)\models E_G D_G \phi$.
From the semantics of $E_G$ we know that $(M,t)\models D_G \phi$ in all states $t\in\S$ ($\S$ is the set of all states) such that $(s,t)\in K_i$ for any $i$ , and that $(M,u)\models \phi$ in all states $u \in \S$ such that $(t,u)\in \cap_{i\in G} K_i$.
Because $K_i$ is transitive and any relation in set of relations $\{\cap_{i\in G}K_i\}$ must be in the set $\{K_i\}$ for all $i$ for any state. It must therefore be the case that all states in $u$ are in $t$. Because $K_i$ is reflective it must be the case that all the states in $t$ are in $u$, i.e. $u=t$. We therefore have that $(M,u)\models \phi$ is equivalent to $(M,t)\models \phi$ .
We now show that if $(M,t)\models \phi$ then $(M,s)\models D_G E_G \phi$ also holds. For $(M,s)\models D_G E_G \phi$ to be true, by semantics of $D_G$ we know that $(M,v)\models E_G \phi$ in all states $v \in \S$ such that $(s,v)\in \cap_{i\in G} K_i$ , which is to say that $(M,w)\models \phi$ in all states $w \in \S$ such that $(v,w)\in K_i$ for all $i$ must be true.
Again, because $K_i$ is transitive and any relation in set of relations $\{\cap_{i\in G}K_i\}$ must be in the set $\{K_i\}$ for all $i$ for any state, it must be the case that all the states in $w$ are in $t$. Conversely because there are no relations in $\{\cap_{i\in G}K_i\}$ that aren't in $\{K_i\}$ for all $i$ for any state, it must also be the case that all the states in $t$ are in $w$, i.e. $w=t$. We therefore have that $(M,w)\models \phi$ is equivalent to $(M,t)\models \phi$ .
Since both the antecedent and consequent are true if and only if $(M,t)\models \phi$ in all states $t\in\S$ such that $(s,t)\in K_i$ for any $i$, for an arbitrary model $M$ and $s$ we see that the formula is valid.
This is an interesting question. It seems like indeed all three statements are equivalent in $S5$. Here is my reasoning. Please, feel free to comment, I might be mistaken.
(a) $E_G D_G \varphi \rightarrow D_G E_G \varphi$ is valid.
Proof. Let some pointed model $(M,w)$ be given, and $a \in G$. We'll prove two lesser results first.
(i) $K_a D_G \varphi \rightarrow K_a \varphi$ is valid. Suppose towards a contradiction that $(M,w) \models K_a D_G \varphi$ and $(M,w) \not \models K_a \varphi$. The former means, by the semantics, that $\forall v \sim_a w: (M,v) \models D_G \varphi$. Since distributed knowledge is veridical (i.e. $D_G \varphi \rightarrow \varphi$ is valid), we have that $\forall v \sim_a w: (M,v) \models \varphi$. The latter is $(M,w) \models K_a \varphi$ by the semantics. Hence, a contradiction.
(ii) $K_a D_G \varphi \rightarrow D_G K_a \varphi$ is valid. Again, suppose to the contrary that $(M,w) \models K_a D_G \varphi$ and $(M,w) \not \models D_G K_a \varphi$. The former implies $(M,w) \models K_a \varphi$ by (i). Let's consider the latter: $(M,w) \models \neg D_G K_a \varphi$. Since $a \in G$, and we deal with $S5$, this implies that $(M,w) \models \neg K_a \varphi$. Hence, a contradiction.
Finally, suppose that $(M,w) \models E_G D_G \varphi$. By definition of $E_G$ we have that $(M,w) \models \bigwedge_{a \in G} K_a D_G \varphi$. Applying (ii) we yield $(M,w) \models \bigwedge_{a \in G} D_G K_a \varphi$, which is $(M,w) \models D_G E_G \varphi$.
(b) $E_G \varphi \leftrightarrow D_G E_G \varphi$ is valid.
Proof. From right to left it holds due to the fact that distributed knowledge (as all reflexive knowledge) is veridical. From left to right the formula holds due to the reasoning that 'if everyone knows $\varphi$, then if they share this knowledge with each other, agents will know that everyone knows $\varphi'.$
(c) $D_G E_G \varphi \rightarrow E_G D_G \varphi$ is valid.
Proof. Let some pointed model $(M,w)$ be given, and $a \in G$. Again, we prove a lesser result first.
(iii) $K_a \varphi \rightarrow K_a D_G \varphi$ (the other direction of (i)) is valid. Suppose that $(M,w) \models K_a \varphi$. Since we work in $S5$ (and hence have positive introspection), we conclude that $(M,w) \models K_a K_a \varphi$. Moreover, we know that $K_a \varphi \rightarrow D_G \varphi$ is valid for $a \in G$. Hence, we apply necessitation to the validity (to get $K_a (K_a \varphi \rightarrow D_G \varphi)$) and then distributivity of K (to get $K_a K_a \varphi \rightarrow K_a D_G \varphi)$). Finally, by modus ponens we yield that $(M,w) \models K_a D_G \varphi$.
Now, let us assume that $(M,w) \models D_G E_G \varphi$ and $(M,w) \not \models E_G D_G \varphi$. The latter means that for at least one agent $a \in G$ it holds that $(M,w) \models \neg K_a D_G \varphi$. By contraposition of (iii) we have $(M,w) \models \neg K_a \varphi$.
From $(M,w) \models D_G E_G \varphi$ we infer that $(M,w) \models D_G K_a \varphi$, and further that $(M,w) \models K_a \varphi$. Hence, a a contradiction.
(d) $E_G \varphi \leftrightarrow E_G D_G \varphi$ is valid.
Proof. From left to right. (iii) applied to all $a \in G$.
From right to left. Suppose that $(M,w) \models D_G E_G \varphi$. By (c), $(M,w) \models E_G D_G \varphi$, and then by (i) applied to every $a \in G$.