This post is regarding the proof of "K$_n^D$ is a sound and complete axiomatization with respect to $\mathcal{M}_n$" in Reasoning about Knowledge, by Fagin, Halpern, Moses, & Vardi.
I have proved the soundness part, but I am struggling with the completeness argument. The book has left several gaps in the argument, and asked to fill them as an exercise (Exercise 3.30 in particular), which I need help with.
We start with a canonical structure constructed just as in the proof of Theorem 3.1.3, treating the distributed knowledge operators $D_G$ exactly like the $K_i$ operators. That is, for each maximal K$_n^D$-consistent set $V$ , we define the set $V/D_G$ in the obvious way and define binary relations $R_G$ on $S$ via $(s_V , s_W) ∈ R_G$ iff $V/D_G ⊆ W$. From axiom $\mathbf{D1}$ it follows that $R_{\{i\}}$ (the binary relation derived using $D_G$, where G is the singleton set $\{i\}$) is equal to $R_i$ (the binary relation derived using $K_i$). It can be shown that $R_G ⊆ \bigcap_{i∈G} R_i$; however, in general, equality does not hold. By making multiple copies of states in the canonical structure that are in $\bigcap_{i\in G}R_i$ and not in $R_G$, it is possible to construct a structure at which the same formulas are true in corresponding states, and in which $\bigcap_{i\in G}R_i$ and $R_G$ coincide. This gives us the desired structure. (See Exercise 3.30 for further details.)
For context:
- $V/D_G = \{\phi: D_G\phi\in V\}$
- The canonical structure $M^c$ is constructed so that $(M^c,s_V)\vDash \phi$ iff $\phi\in V$, where $V$ is a maximally consistent set of formulas (and $s_V$ is the state corresponding to this maximally consistent set).
The exercise referred to above (3.30) is as follows:
(a) Show that $R_G\subseteq \bigcap_{i\in G} R_i$.
(b) Construct an example where $R_G \neq \bigcap_{i\in G} R_i$.
(c) Show that the canonical structure (or any other structure for that matter) can be unwound to get a structure whose graph looks like a tree, in such a way that the same formulas are true in corresponding states. (More formally, given a structure $M = (S,\pi, R_1,...,R_n)$ there is another structure $M' = (S',\pi', R_1',...,R_n')$ and function $f:S'\to S$ such that (i) the graph of $M'$ looks like a tree, in that for all states $s',t'\in M'$ there is at most one path from $s'$ to $t'$, and no path from $s'$ back to itself, (ii) if $(s',t')\in R_i'$, then $f(s'),f(t')\in R_i$, (iii) $\pi'(s') = \pi(f(s'))$, and (iv) $f$ is onto, so that for all $s\in S$ there exists $s'\in S'$ such that $f(s') = s$. Moreover, we have $(M',s')\models \phi$ iff $(M,f(s'))\models \phi$ for all states $s'\in S'$ and all formulas $\phi\in\mathcal{L}_n^D$.)
(d) Show that we can unwind the canonical structure in such a way as to get a structure $M'$ where $R_G = \bigcap_{i\in G} R_i$.
I would be really grateful if someone could help me complete the exercise above, and hence fill in the gaps of the proof of the theorem stated before this. Here's what I've tried:
(a) Suppose $(s_V,s_W)\in R_G$. Then, $V/D_G\subseteq W$. I want to show that $(s_V,s_W)\in R_i$ for every $i\in G$. Note that $(s_V,s_W) \in R_i$ iff $V/K_i = \{\phi: K_i\phi \in V\} \subseteq W$. $V/D_G\subseteq W$ tells us that if $\phi \in V/D_G$, i.e. if $D_G\phi \in V$, then $\phi\in W$. I want to show for every $i$, if $\phi\in V/K_i$, i.e. $K_i\phi\in V$, then $\phi\in W$. How do I go ahead?
(c) Is this the same as unraveling a model to generate a tree-like model as described in Blackburn's Modal Logic?
Please help with the remaining parts as well. Thanks a lot!
I provided some hints for parts (a) and (c) in the comments. I'll sketch a solution to part (d).
Let $M=(W, R_1, \ldots, R_n, R_G, V)$ be the canonical model for $K^D$. Let $M'$ be the submodel of $M$ generated by $w$, where $w$ is any point in $W$. Now consider the unraveling $\overrightarrow{M'}$ of $M'$ around $w$. Assume that for arbitrary $\overrightarrow{s_1}, \overrightarrow{s_2} \in \overrightarrow{W}$, $ \overrightarrow{R'_i}\overrightarrow{s_1} \overrightarrow{s_2}$, for every $i \in G$. For any string $t$ from $\overrightarrow{W}$ let $\sigma(t)$ denote the last member of $t$. Then there is some $v \in W'$ with $\overrightarrow{s_1} * \langle v \rangle = \overrightarrow{s_2}$ (where $*$ is string concatenation) such that $R'_i\sigma(\overrightarrow{s_1}) v$, for every $i \in G$. Now suppose $a :=\sigma(\overrightarrow{s_1})$ and that $\phi \in a/D_G$. Then $D_G \phi \in a$. Consequently, $M', a \models D_G \phi$. Thus, $\phi \in u$, for all $u \in W'$ with $a/K_i \subseteq u$, for every $i \in G$. Since $a/K_i \subseteq v$, for every $i \in G$ it follows that $\phi \in v$. So, $a/D_G \subseteq v$ and we can conclude that $\overrightarrow{R_G} \overrightarrow{s_1} \overrightarrow{s_2}$.