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)↩

**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'\) S-reachable from \(s\) with \((M,s') \vDash \neg \varphi\). Consider the case where there is another state \(s''\) S-reachable from \(s\) with \((M,s'') \vDash \varphi\). As S-reachability is a symmetric relation, it is clear that \(\neg C_S \varphi\) holds at all S-reachable states; but then \(C_S \neg C_S \varphi\) should hold by definition. This contradicts our assumption; we must have negative introspection.

**Positive Introspection** by contradiction: There is some \((M,s)\) with \((M,s) \vDash C_S \varphi \wedge \neg C_S C_S \varphi\). Common knowledge is simultaneous among S-reachable states. Thus we have that \(\forall s'\) S-reachable from \(s\), \((M,s') \vDash C_S \varphi\). But by the definition of common knowledge, this means that we should also have \((M,s) \vDash C_S C_S \varphi\). Again we reach contradiction.

**Distribution Axiom** again by contradiction: There is some \((M,s)\) with \((M,s) \vDash (C_S \varphi \wedge C_S (\varphi \Rightarrow \psi)) \wedge \neg C_S \psi\). Once again by my favourite lemma, the first part of this conjuct means that in all S-reachable states \(s\) from \(s\) we have \((M,s') \vDash \varphi \wedge (\varphi \Rightarrow \psi)\), which by classical logic means we also have \((M,s') \vDash \psi\), which in turn means that \((M,s) \vDash C_S \psi\), which is yet again a contradiction.

I’m going to assume here that the axiom you want is \(i \in S \Rightarrow (C_S \varphi \Rightarrow \varphi)\). If so, this follows immediately, but for fun I’m doing it by contradiction anyway. We have some Model, state, and agent \((M,s) \vDash i \in S \wedge C_S \varphi \wedge \neg\varphi\). By definition of