add material on applications of modal logic

Author: rzach

content/applied-modal-logic/applied-modal-logic.tex

@@ -0,0 +1,20 @@
+% Part: applied-modal-logic
+
+\documentclass[../../include/open-logic-part]{subfiles}
+
+\begin{document}
+
+\olpart{aml}{Applied Modal Logic}
+
+\begin{editorial}
+This part contains experimental draft material on some applications of
+modal logic, such as temporal and epistemic logics.
+\end{editorial}
+
+\olimport[temporal-logic]{temporal-logic}
+
+\olimport[epistemic-logic]{epistemic-logic}
+
+\OLEndPartHook
+
+\end{document}

content/applied-modal-logic/epistemic-logic/bisimulations.tex

@@ -0,0 +1,103 @@
+% Part: applied-modal-logics
+% Chapter: epistemic-logic
+% Section: bisimulations
+
+\documentclass[../../../include/open-logic-section]{subfiles}
+
+\begin{document}
+
+\olfileid{aml}{el}{bsd}
+
+\olsection{Bisimulations}
+
+One remaining question that we might have about the expressive power
+of our epistemic language has to do with the relationship between
+models and the formulas that hold in them. We have seen from our frame
+correspondence results that when certain formulas are valid in a
+frame, they will also ensure that those frames satisfy certain
+properties. But does our modal language, for example, allow us to
+distinguish between a world at which there is a reflexive arrow, and
+an infinite chain of worlds, each of which leads to the next? That is,
+is there any formula $A$ that might hold at only one of these two
+worlds?
+
+Bisimulation is a relationship that we can define between relational
+models to say that they have effectively the same structure. And as we
+will see, it will capture a sense of equivalence between models that
+can be captured in our epistemic language.
+
+\begin{defn}[Bisimulation]
+Let $M_1 = \tuple{W_1, R_1, V_1}$ and $M_2 = \tuple{W_2, R_2, V_2}$ be
+two relational models. And let $\mathcal{R} \subseteq W_1 \times W_2$
+be a binary relation. We say that $\mathcal{R}$ is a
+\emph{bisimulation} when for every $\tuple{w_1, w_2} \in \mathcal{R}$,
+we have:
+
+\begin{enumerate}
+  \item $w_1 \in V_1(p)$ iff $w_2 \in V_2(p)$ for all
+  !!{propositional variable}s~$p$.
+  \item For all agents $a \in A$ and worlds $v_1 \in W_1$, if
+  $R_{1_a} w_1 v_1$ then there is some $v_2 \in W_2$ such that
+  $R_{2_a} w_2 v_2$, and $\tuple{v_1, v_2} \in
+  \mathcal{R}$.
+  \item For all agents $a \in A$ and worlds $v_2 \in W_2$, if
+   $R_{2_a} w_2 v_2$ then there is some $v_1 \in W_1$ such that
+   $R_{1_a} w_1 v_1$, and $\tuple{v_1, v_2} \in
+   \mathcal{R}$.
+\end{enumerate}
+
+When there is a bisimulation between $M_1$ and $M_2$ that links worlds
+$w_1$ and $w_2$, we can also write $\tuple{M_1, w_1} \leftrightarroweq
+\tuple{M_2, w_2}$, and call $\tuple{M_1, w_1}$ and $\tuple{M_2, w_2}$
+\emph{bisimilar}.
+\end{defn}
+
+The different clauses in the bisimulation relation ensure different
+things. Clause 1 ensures that bisimilar worlds will satisfy the same
+modal-free formulas, since it ensures agreement on all
+!!{propositional variable}s. The other two clauses, sometimes referred
+to as ``forth'' and ``back,'' respectively, ensure that the
+accessibility relations will have the same structure.
+
+\begin{thm}
+If $\tuple{M_1, w_1} \leftrightarroweq \tuple{M_2, w_2}$, then for
+every !!{formula}~$!A$, we have that $\mSat{M_1}{!A}[w_1]$ iff
+$\mSat{M_2}{!A}[w_2]$.
+\end{thm}
+
+\begin{figure}
+  \begin{center}
+    \begin{tikzpicture}[modal]
+      \node[world] (w1) {$w_1$}; 
+      \node[world] (w2) [above left=of w1]{$w_2$}; 
+      \node[world] (w3) [above right=of w1] {$w_3$};
+      \draw[<->] (w1) to node {$a$} (w2);
+      \draw[->,loop below] (w1) to node {$a$} (w1);
+      \draw[<->] (w1) to [swap] node {$a$} (w3);
+      \draw[->,loop above] (w2) to node {$a$} (w2) ;
+      \draw[->,loop above] (w3) to node {$a$} (w3) ;
+      
+      \node[world](v1)[right of=w1, xshift=1.5in]{$v_1$};
+      \node[world](v2)[above of=v1]{$v_2$};
+      \draw[<->] (v1) to node {$a$} (v2);
+      \draw[->,loop below] (v1) to node {$a$} (v1);
+      \draw[->,loop above] (v2) to node {$a$} (v2) ;
+
+      \draw[-,dotted] (w1) to (v1) ;
+      \draw[-,dotted,bend left=45] (w2) to (v2) ;
+      \draw[-,dotted,bend left=30] (w3) to (v2) ;
+    \end{tikzpicture}
+  \end{center}
+  \caption{Two bisimilar models.}
+  \ollabel{fig:bisimilar}
+\end{figure}
+
+Even though the two models pictured in \olref{fig:bisimilar} aren't
+quite the same as each other, there is a bisimulation linking worlds
+$w_1$ and~$v_1$. This bisimulation will also link both $w_2$ and $w_3$
+to~$v_2$, with the idea being that there is nothing expressible in our
+modal language that can really distinguish between them. The situation
+would be different if $w_2$ and~$w_3$ satisfied different
+!!{propositional variable}s, however. 
+
+\end{document}

content/applied-modal-logic/epistemic-logic/epistemic-logic.tex

@@ -0,0 +1,26 @@
+% Part: applied-modal-logics
+% Chapter: epistemic-logic
+
+\documentclass[../../include/open-logic-chapter]{subfiles}
+
+\begin{document}
+
+\olchapter{aml}{el}{Epistemic Logics}
+
+\begin{editorial}
+  This chapter covers the metatheory of epistemic logics. It is structured in a similar way to Aldo Antonelli's notes on classical  basic modal logic, but has been rewritten by Audrey Yap in order to add material on bisimulation and dynamic epistemic logics.
+\end{editorial}
+
+\olimport{introduction}
+\olimport{language-epistemic-logic}
+\olimport{relational-models}
+\olimport{truth-at-w}
+\olimport{properties-accessibility}
+\olimport{bisimulations}
+\olimport{public-announcement-logic-lang}
+\olimport{public-announcement-logic-semantics}
+
+
+\OLEndPartHook
+
+\end{document}

content/applied-modal-logic/epistemic-logic/introduction.tex

@@ -0,0 +1,23 @@
+% Part: applied-modal-logics
+% Chapter: epistemic-logic
+% Section: introduction
+
+\documentclass[../../../include/open-logic-section]{subfiles}
+
+\begin{document}
+
+\olfileid{aml}{el}{int}
+
+\olsection{Introduction}
+
+Just as modal logic deals with \emph{modal propositions} and the entailment relations among them, epistemic logic deals with \emph{epistemic propositions} and the entailment relations among them. Rather than interpreting the modal operators as representing possibility and necessity, the unary connectives are interpreted in epistemic or doxastic ways, to model knowledge and belief. For example, we might want to express claims like the following:
+
+\begin{enumerate}
+\item Richard knows that Calgary is in Alberta.
+\item Audrey thinks it is possible that a dog is on the couch.
+\item Richard knows that Audrey knows that her class is on Tuesdays.
+\item Everyone knows that a year has 12 months.
+\end{enumerate}
+Contemporary epistemic logic is often traced to Jaako Hintikka's \emph{Knowledge and Belief}, from 1962, and it was written at a time when possible worlds semantics were becoming increasingly more used in logic. In fact, epistemic logics use most of the same semantic tools as other modal logics, but will interpret them differently. The main change is in what we take the \emph{accessibility relation} to represent. In epistemic logics, they represent some form of \emph{epistemic possibility}. We'll see that the epistemic notion that we're modelling will affect the constraints that we want to place on the accessibility relation. And we'll also see what happens to correspondence theory when it is given an epistemic interpretation. You'll notice that the examples above mention two agents: Richard and Audrey, and the relationship between the things that each one knows. The epistemic logics we'll consider will be multi-agent logics, in which such things can be expressed. In contrast, a single-agent epistemic logic would only talk about what one individual knows or believes.
+
+\end{document}

content/applied-modal-logic/epistemic-logic/language-epistemic-logic.tex

@@ -0,0 +1,87 @@
+% Part: applied-modal-logics
+% Chapter: epistemic-logic
+% Section: language-epistemic-logic
+
+\documentclass[../../../include/open-logic-section]{subfiles}
+
+\begin{document}
+
+\olfileid{aml}{el}{lan}
+
+\olsection{The Language of Epistemic Logic}
+
+\begin{defn}
+Let $G$ be a set of agent-symbols. The basic language of multi-agent
+epistemic logic contains
+\begin{enumerate}
+  \tagitem{prvFalse}{The propositional constant for !!{falsity}~$\lfalse$.}{}
+  \tagitem{prvTrue}{The propositional constant for !!{truth}~$\ltrue$.}{}
+  \item A !!{denumerable}s set of !!{propositional variable}s: $\Obj
+    p_0$, $\Obj p_1$, $\Obj p_2$, \dots
+  \item The propositional connectives: \startycommalist
+  \iftag{prvNot}{\ycomma $\lnot$ (negation)}{}%
+  \iftag{prvAnd}{\ycomma $\land$ (conjunction)}{}%
+  \iftag{prvOr}{\ycomma $\lor$ (disjunction)}{}%
+  \iftag{prvIf}{\ycomma $\lif$ (!!{conditional})}{}%
+  \iftag{prvIff}{\ycomma $\liff$ (!!{biconditional})}{}.
+  \item The knowledge operator $\Knows_a$ where $a \in G$.
+\end{enumerate}
+\end{defn}
+
+If we are only concerned with the knowledge of a single agent in our
+system, we can drop the reference to the set~$G$, and individual
+agents. In that case, we only have the basic operator~$\Knows$.
+
+\begin{defn}
+\emph{!!^{formula}s} of the epistemic language are inductively
+  defined as follows:
+\begin{enumerate}
+\tagitem{prvFalse}{$\lfalse$ is an atomic !!{formula}.}{}
+
+\tagitem{prvTrue}{$\ltrue$ is an atomic !!{formula}.}{}
+
+\item Every propositional variable $\Obj p_i$ is an (atomic) !!{formula}.
+
+\tagitem{prvNot}{If $!A$ is !!a{formula}, then $\lnot !A$ is
+  !!a{formula}.}{}
+
+\tagitem{prvAnd}{If $!A$ and $!B$ are !!{formula}s, then $(!A \land
+  !B)$ is !!a{formula}.}{}
+
+\tagitem{prvOr}{If $!A$ and $!B$ are !!{formula}s, then $(!A \lor !B)$
+  is !!a{formula}.}{}
+
+\tagitem{prvIf}{If $!A$ and $!B$ are !!{formula}s, then $(!A \lif !B)$
+  is !!a{formula}.}{}
+
+\tagitem{prvIff}{If $!A$ and $!B$ are !!{formula}s, then $(!A \liff !B)$
+  is !!a{formula}.}{}
+
+\item If $!A$ is !!a{formula} and $a \in G$, then $\Knows_a !A$ is
+  !!a{formula}.
+
+\tagitem{limitClause}{Nothing else is !!a{formula}.}{}
+\end{enumerate}
+\end{defn}
+
+If !!a{formula}~$!A$ does not contain $\Knows_a$, we say it
+is \emph{modal-free}.
+
+\begin{defn}
+  While the $\Knows$ operator is intended to symbolize individual
+  knowledge, $\EKnows$, often read as ``everybody knows,'' symbolizes
+  group knowledge. Where $G' \subseteq G$, we define $\EKnows_{G'} !A$
+ as an abbreviation for \[\bigwedge_{b \in G'} \Knows_b !A.\]
+\end{defn}
+
+We can also define an even stronger sense of knowledge, namely
+\emph{common knowledge} among a group of agents~$G$. When a piece of
+information is common knowledge among a group of agents, it means that
+for every combination of agents in that group, they all know that each
+other knows that each other knows \dots ad infinitum. This is
+significantly stronger than group knowledge, and it is easy to come up
+with relational models in which !!a{formula} is group knowledge, but
+not common knowledge. We will use $\CKnows_G !A$ to symbolize ``it is
+common knowledge among~$G$ that~$!A$.''
+
+\end{document}

content/applied-modal-logic/epistemic-logic/properties-accessibility.tex

@@ -0,0 +1,78 @@
+% Part: applied-modal-logics
+% Chapter: epistemic-logic
+% Section: properties-accessibility
+
+\documentclass[../../../include/open-logic-section]{subfiles}
+
+\begin{document}
+
+\olfileid{aml}{el}{acc}
+
+\olsection{Accessibility Relations and Epistemic Principles}
+
+Given what we already know about frame correspondence in normal modal
+logics, we might want to see what the characteristic !!{formula}s look
+like given epistemic interpretations. We have already said that
+epistemic logics are typically interpreted in S5. So let's take a look
+at how various epistemic principles are represented, and consider how
+they correspond to various frame conditions.
+
+Recall from normal modal logic, that different modal !!{formula}s
+characterized different properties of accessibility relations. This
+table picks out a few that correspond to particular epistemic
+principles.
+
+\begin{table}[t]
+    \begin{tabular}{| p{.48\textwidth} || p{.48\textwidth} |}
+      \hline
+      {\emph{If $R$ is \dots}} & {\emph{then \dots is true in~$\mModel{M}$:}} \\
+      \hline \hline
+        
+      & $\Knows (p \lif q) \lif (\Knows p \lif \Knows q)$ 
+      \hfill \newline{(Closure)} \\
+      \hline
+      \emph{reflexive}: $\forall w Rww$  
+      & $\Knows p \lif p$ \hfill \newline{(Veridicality)} \\
+      \hline
+      \emph{transitive}: \newline
+      $\forall u \forall v \forall w ((Ruv \land Rvw) \lif Ruw)$ & 
+      $\Knows p \lif \Knows \Knows p$ \hfill 
+           \newline{(Positive Introspection)} \\
+      \hline 
+      \emph{euclidean}: \newline
+      $\forall w \forall u \forall v ((Rwu \land Rwv) \lif Ruv)$ &  
+      $\lnot \Knows p \lif \Knows \neg \Knows p$ \hfill 
+        \newline{(Negative Introspection)} \\
+      \hline
+    \end{tabular}
+    \caption{Four epistemic principles.}
+    \ollabel{tab:four}
+  \end{table} 
+
+Veridicality, corresponding to the $T$ axiom, is often treated as the
+most uncontroversial of these principles, as it represents that claim
+that if !!a{formula} is known, then it must be true. Closure, as well
+as Positive and Negative Introspection are much more contested. 
+
+Closure, corresponding to the $K$ axiom, represents the idea that an
+agent's knowledge is closed under implication. This might seem
+plausible to us in some cases. For instance, I might know that if I am
+in Victoria, then I am on Vancouver Island. Barring odd skeptical
+scenarios, I do know that I am in Victoria, and this should also
+suggest that I know I am on Vancouver Island. So in this case, the
+logical closure of my knowledge might seem relatively intuitive. On
+the other hand, we do not always think through the consequences of our
+knowledge, and so this might lead to less intuitive results in other
+cases.
+
+Positive Introspection, sometimes known as the KK-principle, is
+sometimes articulated as the statement that if I know something, then
+I know that I know. It is the epistemic counterpart of the 4 axiom.
+Correspondingly, negative introspection is articulated as the
+statement that if I \emph{don't} know something, then I know that I
+don't know it, which is the counterpart of the 5 axiom. Both of these
+seem to admit of relatively ordinary counterexamples, in which I am
+unsure whether or not I know something that I do in fact know. 
+
+
+\end{document}