Proving validity of $D_G\varphi \to D_{G'}\varphi$ if $G\subseteq G'$

Question

This post is regarding the proof of Theorem 3.4.1 in Reasoning about Knowledge, by Fagin, Halpern, Moses, & Vardi.

While proving the soundness of axiom system K$_n^D$, I must show the validity of axiom $\mathbf{(D2)}$ given by $$D_G\varphi \to D_{G'}\varphi \text{ if } G\subseteq G' \quad \mathbf{(D2)}$$ where $D_G$ denotes distributed knowledge. Semantically, we have:

$(M,s)\vDash D_G\varphi$ if and only if $(M,t)\vDash\varphi$ for all $t$ such that $(s,t)\in \bigcap_{i\in G} R_i$.

---

Here's what I'm trying: Suppose $G\subseteq G'$. Also suppose $(M,s)\vDash D_G\varphi$. $(M,s)\vDash D_G\varphi$ if and only if $(M,t)\vDash\varphi$ for all $t$ such that $(s,t)\in \bigcap_{i\in G} R_i$.

Since $G\subseteq G'$, $$\bigcap_{i\in G'} R_i \subseteq \bigcap_{i\in G} R_i$$ (We get smaller sets as we intersect more elements). As a result, $(s,t)\in \bigcap_{i\in G} R_i$ tells me nothing about $(s,t) \stackrel{??}{\in} \bigcap_{i\in G'} R_i$. How do I proceed? Please help, thanks!

---

P.S. Is $\mathbf{(D2)}$ correct as stated? From my reasoning, I should be able to prove $D_G\varphi \to D_{G'}\varphi \text{ if } G'\subseteq G$. Is it possible that this is a typing error? I doubt it though since the author explains in words that (D2) means "larger groups have more distributed knowledge", which also makes sense. Hence, I am confused.

Answer 1

The axiom is stated correctly, and you actually almost have the proof.

So, you know that $\bigcap_{i \in G^\prime} R_i \subseteq \bigcap_{i \in G} R_i$ and that $(M,t) \models \varphi$ for all $t$ such that $(s,t) \in \bigcap_{i \in G} R_i$. Let us call all states reachable from $s$ via the intersection of $G$-relations $S^G$. Similarly, for $G^\prime$ we have $S^{G^\prime}$. Note that $S^{G^\prime} \subseteq S^G$.

Now, the fact that $(M,t) \models \varphi$ for all $t \in S^G$ implies that $(M,u) \models \varphi$ for all $u \in S^{G^\prime}$.