# 6.14

## a

Proving Lemma 6.4.1: $$({\mathcal{I}},r,m) \vDash C_S \varphi$$ iff $$({\mathcal{I}},r',m') \vDash \varphi$$ for all points $$(r',m')$$ that are S-reachable from $$(r,m)$$.

### i

First direction: by contradiction. We assume that $$({\mathcal{I}},r',m') \vDash \varphi$$ for all points $$(r',m')$$ that are S-reachable from $$(r,m)$$ while $$({\mathcal{I}},r,m) \vDash \neg C_S \varphi$$. As $$({\mathcal{I}},r,m) \vDash \neg C_S \varphi$$, by definition there exists some $$k$$ such that $$({\mathcal{I}},r,m) \vDash \neg E^k_S \varphi$$. Thus there also $$\exists i \in S(r,m)$$ s.t. $$({\mathcal{I}},r,m) \vDash \neg B^S_i$$, remember this $$i$$, we’ll use it later. As $$({\mathcal{I}},r,m) \vDash \neg B^S_i$$, $$\exists (r',m')$$ s.t. $$r_i(m) = r'_i(m')$$ and $$i \in S(r',m')$$ where $$({\mathcal{I}}, r', m') \vDash \neg \varphi$$. But $$(r',m')$$ is only one $$i$$-hop away from $$(r,m)$$, and is thus clearly $$S$$-reachable from $$(r,m)$$; we have a contradiction.

### ii

I assume that S is non-empty at $$(r,m)$$; when S is empty at $$(r,m)$$, $$C_S \varphi$$ hold vacuously, and (as “S-reachable” is now an empty set) the other half of our iff statement also holds vacuously.

Other direction. I start by proving a related lemma. Lemma: if $$\bigl(\forall (r',m')$$ S-reachable from $$(r,s)$$ in at most $$k$$ hops: $$({\mathcal{I}},r',m') \vDash \varphi \bigr)$$, then $$({\mathcal{I}},r,m) \vDash E^k_S \varphi$$.

Case $$k = 0$$: $$\forall \varphi$$ s.t. $$({\mathcal{I}},r,m) \vDash \varphi$$, all states reachable from some state s in 0 steps are simply that state $$s$$; thus our “if-test” clause holds. We observe that $$E_S^0 \varphi \Leftrightarrow \varphi$$ by definition; thus $$({\mathcal{I}},r,m) \vDash E_S^0 \varphi$$.

Case $$k -1 \Rightarrow k$$: (pay attention to the parens in order to determine scope of the quantifiers)

Assume that, $$\forall (r',m')$$ s-reachable in at most $$k$$ steps from $$(r,m)$$, $$({\mathcal{I}},r',m') \vDash \varphi$$. (Else the statement holds vacuously.) $$\forall i \in S(r,m): \forall (r',m')$$ s.t. $$r_i(m) = r'_i(m'): \bigl($$1 $$(r',m')$$ is 1 step away from $$(r,m)$$; we can immediately derive from our case assumption that $$\forall (r'',m'')$$ s-reachable in at most $$k-1$$ steps from $$(r',m')$$, $$({\mathcal{I}},r'',m'') \vDash \varphi$$. We can therefore use our inductive hypothesis to conclude $$({\mathcal{I}},r',m') \vDash E^{k-1}_S \varphi \bigr )$$. We observe that $$\forall i \in S(r,m): \forall (r',m') \text{s.t. } r_i(m) = r'_i(m'): ({\mathcal{I}},r',m') \vDash E^{k-1}_S \varphi$$ is just the statement $$E^k_S \varphi$$ expanded first by its definition, and second by the definition of $$B^i_S$$; thus $$E^k_S \varphi$$ holds.

We have shown the base and inductive case; by the magic of induction, we conclude the lemma proven.

1. (observe $$i \in S(r,m)$$ from initial quantification)

We now use this lemma to prove this direction by induction: assume $$\forall (r',m')$$ S-reachable from $$(r,m): ({\mathcal{I}},r',m') \vDash \varphi$$ (else holds vacuously). Observe that the set of points S-reachable in $$k$$ steps from $$(r,m)$$ is the subset of all points S-reachable from $$(r,m)$$ for all $$k$$; it thus follows immediately that $$({\mathcal{I}},r,m) \vDash E^k_S \varphi$$ for $$k = 1,2,...$$. This is the definition of common knowledge on nonrigid sets.

## b

Knowledge generalization follows immediately; if $$\varphi$$ holds everywhere, it also holds everywhere s-reachable from a given point.

Negative Introspection by contradiction; There is some $$(M,s)$$ with $$(M,s) \vDash \neg C_S \varphi \wedge \neg C_S \neg C_S \varphi$$. For $$\neg C_S \varphi$$ to hold at $$s$$, there must be some state $$s'$$