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.

  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.


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 \(C_S \varphi\) and the constraint that \(i \in S\) (and S non-empty) we conclude that \((M,s) \vDash \varphi\). Thus the generalization of the knowledge axiom holds.


This is a huge theorem, you know. I’m somewhat dismayed by the sheer length of this assignment. Right, no time like the present I suppose.

For all formulas \(\varphi\) and \(\psi\), all structures \(M\), and all \(S\) where \(\forall s \in M: S(s) \neq \emptyset \wedge S \subset \{1,...,n\}:\)

\((a) M \vDash E_S \varphi \Leftrightarrow \bigwedge_{i \in S} B^S_i \varphi\)

\((b) M \vDash C_S \varphi \Leftrightarrow E_S (\varphi \wedge C_S \varphi),\)

\((c)\) if \(M \vDash \varphi \Rightarrow E_S(\psi \wedge \varphi)\) then \(M \vDash \varphi \Rightarrow C_G \psi\).

\((a)\) follows immediately from the definition of \(E_S\). For part b, suppose that \((M,s) \vDash C_S \varphi\). Thus \((M,t) \vDash \varphi\) for all states S-reachable from \(s\). In particular, if \(u\) is S-reachable from \(s\) in one step, then \((M,u) \vDash \varphi\) and \((M,t) \vDash \varphi\) for all \(t\) that are S-reachable from \(u\). Thus \((M,u) \vDash \varphi \wedge C_S \varphi\) for all such \(u\), so \((M,s) \vDash E_S(\varphi \wedge C_S \varphi)\). For the converse, suppose that \((M,s) \vDash E_S(\varphi \wedge C_S \varphi)\). From (a), we have then that \((M,s) \vDash B^S_i(\varphi \wedge C_S \varphi)\) for all \(i\). Using our analogue of the knowledge axiom and non-empty assumption, we therefore also have that \((M,s) \vDash \varphi \wedge C_S \varphi\), which in turn implies \((M,s) \vDash C_S \varphi\). We have proven both directions.

\((b)\) I will argue by contradiction. Assume that we have some \(M \vDash \varphi \Rightarrow E_S(\psi \wedge \varphi)\), but there is some