authorea.com/23780

Reasoning About Knowledge: HW8

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)\).

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.

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.

(observe \(i \in S(r,m)\) from initial quantification)↩

## Share on Social Media