this is for holding javascript data
Matthew Milano edited subsection_b_bf_Knowledge_generalization__.tex
about 9 years ago
Commit id: fc1520ca62abd74cefd936558d365ede71b4c267
deletions | additions
diff --git a/subsection_b_bf_Knowledge_generalization__.tex b/subsection_b_bf_Knowledge_generalization__.tex
index 30858c9..d4f4b64 100644
--- a/subsection_b_bf_Knowledge_generalization__.tex
+++ b/subsection_b_bf_Knowledge_generalization__.tex
...
\\
(b) $(b)$ I will argue by contradiction. Assume that we have some $M \vDash \varphi \Rightarrow E_S(\psi \wedge \varphi)$, but there is some $(M,s) \vDash
\phi \varphi \wedge \neg C_S \psi$. As $(M,s) \vDash \varphi \wedge \varphi \Rightarrow E_S(\psi \wedge \varphi)$ we conclude $(M,s) \vDash E_S(\psi \wedge \varphi)$. Again by our non-empty assumption, part (a), and knowledge-axiom analog, we get $(M,s) \vDash \varphi \wedge \psi$.
In fact, we can perform this argument at all states $s'$ in which $(M,s') \vDash \varphi \wedge \neg C_S \psi$. Consider the set of S-reachable states from s; in these states, either $\varphi \wedge \neg C_S\psi$, $\varphi \wedge C_S\psi$, or $\neg\varphi$. In the states where $\neg\varphi$ holds, the statement $\varphi \Rightarrow C_S \psi$ holds vacuously. If there are any states where $C_S \psi$ holds, then $C_S \psi$ should have held at $s$, so we safely conclude there are no such states. This leaves us only with states where $\varphi \wedge \neg C_S \psi$. But
by in all these states, we have $\varphi \wedge psi$, which in turn means that we should have $\varphi \Rightarrow C_S \psi$ at these
same states. This contradicts our initial assumption; we conclude $(c)$ holds.