Applied Modal Logic

Epistemic Logics

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

% 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

% 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

% 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-agentepistemic 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 oursystem, we can drop the reference to the set~$G$, and individualagents. 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 itis \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 ofinformation is common knowledge among a group of agents, it means thatfor every combination of agents in that group, they all know that eachother knows that each other knows \dots ad infinitum. This issignificantly stronger than group knowledge, and it is easy to come upwith relational models in which !!a{formula} is group knowledge, butnot common knowledge. We will use $\CKnows_G !A$ to symbolize ``it iscommon knowledge among~$G$ that~$!A$.''\end{document}

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

% Part: applied-modal-logics% Chapter: epistemic-logic% Section: relational-models\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{aml}{el}{rel}\olsection{Relational Models}The basic semantic concept for epistemic logics is the same as that ofordinary modal logics. Relational models still consist of a set ofworlds, and an assignment that determines which !!{propositionalvariable}s count as ``true'' at which worlds. And if we are onlydealing with a single agent, we have a single accessibility relationas usual. However, if we have a multi-agent epistemic logic, then oursingle accessibility relation becomes a set of accessibilityrelations, one for each~$a$ in our set of agent symbols~$G$.A \emph{relational model} consists of a set of worlds, which arerelated by binary accessibility relations---one for eachagent---together with an assignment which determines which!!{propositional variable}s are true at which worlds.\begin{defn}  A \emph{model} for the multi-agent epistemic language is a triple  $\mModel{M} = \tuple{W, R, V}$, where  \begin{enumerate}  \item $W$ is a nonempty set of ``worlds,''  \item For each $a \in G$, ${R}_a$ is a binary accessibility relation  on~$W$, and  \item $V$ is a function assigning to each !!{propositional    variable}~$p$ a set $V(p)$ of possible worlds.  \end{enumerate}  When $R_a ww'$ holds, we say that $w'$ is \emph{accessible by a    from}~$w$. When $w \in V(p)$ we say $p$ is \emph{true at}~$w$.\end{defn}The mechanics are just like the mechanics for normal modal logic, justwith more accessibility relations added in. For a given agent, we willgenerally interpret their accessibility relation as representingsomething about their informational states. For example, we oftentreat $R_a ww'$, as expressing that $w'$ is consistent with~$a$'sinformation at~$w$. Or to put it another way, at~$w$, they cannot tellthe difference between world $w$ and world~$w'$.  \end{document}

content/applied-modal-logic/epistemic-logic/truth-at-w.tex

% Part: applied-modal-logics% Chapter: epistemic-logic% Section: truth-at-w\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{aml}{el}{trw}\olsection{Truth at a World}Just as with normal modal logic, every epistemic model determines which !!{formula}s count as true atwhich worlds in it. We use the same notation ``model $\mModel{M}$ makes!!{formula}~$!A$ true at world~$w$'' for the basic notion of relationalsemantics. The relation is defined inductively and is identical to the normal modal case for all non-modal operators.\begin{defn}\ollabel{defn:mmodels}  \emph{Truth of !!a{formula}~$!A$ at~$w$} in a~$\mModel M$, in symbols:  $\mSat{M}{!A}[w]$, is defined inductively as follows:  \begin{enumerate}  \tagitem{prvFalse}{\indcase{!A}{\lfalse}{Never $\mSat{M}{\lfalse}[w]$}.}{}  \tagitem{prvTrue}{\indcase{!A}{\ltrue}{Always $\mSat{M}{\ltrue}[w]$}.}{}  \item $\mSat{M}{p}[w]$ iff $w \in V(p)$  \tagitem{prvNot}{\indcase{!A}{\lnot !B}{$\mSat{M}{\indfrm}[w]$ iff    $\mSat/{M}{!B}[w]$}.}{}  \tagitem{prvAnd}{\indcase{!A}{(!B \land !C)}{$\mSat{M}{\indfrm}[w]$ iff    $\mSat{M}{!B}[w]$ and $\mSat{M}{!C}[w]$}.}{}  \tagitem{prvOr}{\indcase{!A}{(!B \lor !C)}{$\mSat{M}{\indfrm}[w]$ iff    $\mSat{M}{!B}[w]$ or $\mSat{M}{!C}[w]$} (or both).}{}  \tagitem{prvIf}{\indcase{!A}{(!B \lif !C)}{$\mSat{M}{\indfrm}[w]$ iff    $\mSat/{M}{!B}[w]$ or $\mSat{M}{!C}[w]$}.}{}  \tagitem{prvIff}{\indcase{!A}{(!B \liff !C)}{$\mSat{M}{\indfrm}[w]$ iff    either both $\mSat{M}{!B}[w]$ and $\mSat{M}{!C}[w]$ or    neither $\mSat{M}{!B}[w]$ nor $\mSat{M}{!C}[w]$}.}{}  \item\ollabel{defn:sub:mmodels-box}    \indcase{!A}{\Knows_a !B}{$\mSat{M}{\indfrm}[w]$ iff    $\mSat{M}{!B}[w']$ for all $w' \in W$ with $R_a ww'$}  \end{enumerate} \end{defn}Here's where we need to think about restrictions on our accessibilityrelations, though. After all, by clause~\olref{defn:sub:mmodels-box},!!a{formula}~$\Knows_a !B$ is true at~$w$ whenever there are no~$w'$with $R_a ww'$. This is the same clause as in normal modal logic; whena world has no successors, all $\Box$-formulas are vacuously truethere. This seems extremely counterintuitive if we think about$\Knows$ as representing \emph{knowledge}. After all, we tend to thinkthat there are \emph{no} circumstances under which an agent might knowboth $!A$ and $\lnot !A$ at the same time.One solution is to ensure that our accessibility relation in epistemiclogic will always be \emph{reflexive}. This roughly corresponds to theidea that the actual world is consistent with an agent's information.In fact, epistemic logics typically use S5, but others might useweaker systems depending on what exactly they want the $\Knows_a$relation to represent.\begin{figure}  \begin{center}    \begin{tikzpicture}[modal]      \node[world] (w1) [label={[align=right]right:\mTrue{p}\\ \mFalse{q}}]{$w_1$};       \node[world] (w2) [label={[align=right]right:\mTrue{p}\\ \mTrue{q}},        above right=of w1]{$w_2$};       \node[world] (w3) [label={[align=right]right:\mFalse{p}\\ \mFalse{q}},        below right=of w1] {$w_3$};      \draw[<->] (w1) to node {$a$} (w2);      \draw[->,loop left] (w1) to node {$a,b$} (w1);      \draw[<->] (w1) to [swap] node {$b$} (w3);      \draw[->,loop above] (w2) to node {$a,b$} (w2) ;      \draw[->,loop below] (w3) to node {$a,b$} (w3) ;    \end{tikzpicture}  \end{center}  \caption{A simple epistemic model.}  \ollabel{fig:simple}\end{figure}\begin{prob}  Consider which of the following hold in  \olref[aml][el][trw]{fig:simple}:  \begin{enumerate}    \item $\mSat{M}{\lnot q}[w_1]$;    \item $\mSat{M}{\Knows_a \lnot q}[w_1]$;    \item $\mSat{M}{\Knows_b \lnot q}[w_1]$;    \item $\mSat{M}{\Knows_b q \lor \Knows_b \lnot q}[w_2]$;    \item $\mSat{M}{\Knows_a( \Knows_b q \lor \Knows_b \lnot q)}[w_2]$;    \item $\mSat{M}{\EKnows_{\{a,b\}} \lnot q}[w_3]$;    \end{enumerate}\end{prob}Now that we have given our basic definition of truth at a world, theother semantic concepts from normal modal logic, such as modalvalidity and entailment, simply carry over, applied to this new way ofthinking about the interpretation for the modal operators.We are now also in a position to give truth conditions for the commonknowledge operator~$\CKnows_G$. Recall from \olref[sfr][rel][ops]{sec}that the \emph{transitive closure}~$R^+$ of a relation~$R$ is definedas\begin{align*}  R^+ &= \bigcup_{ n \in \mathbb{N}} R^n, \intertext{where}  R^0 & = R \text{ and}\\   R^{n+1} & = \Setabs{\tuple{x, z}}{\exists y (R^n xy \land Ryz)}.\end{align*}Then, where $G$ is a group of agents, we define $R_G = ( \bigcup_{b\in G} R_b )^+$ to be the transitive closure of the union of allagents' accessibility relations.\begin{defn}If $G' \subseteq G$, we let $\mSat{M}{\CKnows_{G'} !A}[ w]$ iff forevery $w'$ such that $R_{G'} w w'$, $\mSat{M}{!A}[w']$.\end{defn}\end{document}

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

% 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 modallogics, we might want to see what the characteristic !!{formula}s looklike given epistemic interpretations. We have already said thatepistemic logics are typically interpreted in S5. So let's take a lookat how various epistemic principles are represented, and consider howthey correspond to various frame conditions.Recall from normal modal logic, that different modal !!{formula}scharacterized different properties of accessibility relations. Thistable picks out a few that correspond to particular epistemicprinciples.\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 themost uncontroversial of these principles, as it represents that claimthat if !!a{formula} is known, then it must be true. Closure, as wellas Positive and Negative Introspection are much more contested. Closure, corresponding to the $K$ axiom, represents the idea that anagent's knowledge is closed under implication. This might seemplausible to us in some cases. For instance, I might know that if I amin Victoria, then I am on Vancouver Island. Barring odd skepticalscenarios, I do know that I am in Victoria, and this should alsosuggest that I know I am on Vancouver Island. So in this case, thelogical closure of my knowledge might seem relatively intuitive. Onthe other hand, we do not always think through the consequences of ourknowledge, and so this might lead to less intuitive results in othercases.Positive Introspection, sometimes known as the KK-principle, issometimes articulated as the statement that if I know something, thenI know that I know. It is the epistemic counterpart of the 4 axiom.Correspondingly, negative introspection is articulated as thestatement that if I \emph{don't} know something, then I know that Idon't know it, which is the counterpart of the 5 axiom. Both of theseseem to admit of relatively ordinary counterexamples, in which I amunsure whether or not I know something that I do in fact know. \end{document}

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

% 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 powerof our epistemic language has to do with the relationship betweenmodels and the formulas that hold in them. We have seen from our framecorrespondence results that when certain formulas are valid in aframe, they will also ensure that those frames satisfy certainproperties. But does our modal language, for example, allow us todistinguish between a world at which there is a reflexive arrow, andan 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 twoworlds?Bisimulation is a relationship that we can define between relationalmodels to say that they have effectively the same structure. And as wewill see, it will capture a sense of equivalence between models thatcan 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}$ betwo 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 differentthings. Clause 1 ensures that bisimilar worlds will satisfy the samemodal-free formulas, since it ensures agreement on all!!{propositional variable}s. The other two clauses, sometimes referredto as ``forth'' and ``back,'' respectively, ensure that theaccessibility relations will have the same structure.\begin{thm}If $\tuple{M_1, w_1} \leftrightarroweq \tuple{M_2, w_2}$, then forevery !!{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'tquite 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 ourmodal language that can really distinguish between them. The situationwould be different if $w_2$ and~$w_3$ satisfied different!!{propositional variable}s, however. \end{document}

content/applied-modal-logic/epistemic-logic/public-announcement-logic-lang.tex

% Part: applied-modal-logics% Chapter: epistemic-logic% Section: language-epistemic-logic\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{aml}{el}{pal}\olsection{Public Announcement Logic}Dynamic epistemic logics allow us to represent the ways in whichagents' knowledge changes over time, or as they gain new information.Many of these represent changes in knowlege using informational\emph{events} or \emph{updates}. The most basic kind of update is apublic announcement in which some formula is truthfully announced andall of the agents witness this taking place together. To do this, weexpand the language as follows\begin{defn}Let $G$ be a set of agent-symbols. The basic language of multi-agentepistemic logic with public announcements 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})}{}%  \item The knowledge operator $\Knows_a$ where $a \in G$.  \item The public announcement operator $[!B]$ where $!B$ is !!a{formula}.\end{enumerate}\end{defn}The public announcement operator functions as a box operator, and ourinductive definition of the language is given accordingly:\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}.    \item If $!A$ and $!B$ are !!{formula}s, then $[!A] !B$ is !!a{formula}.  \tagitem{limitClause}{Nothing else is !!a{formula}.}{}\end{enumerate}\end{defn}The intended reading of the !!{formula} $[!A] !B$ is ``After $!A$ istruthfully announced, $!B$~holds. It will sometimes also be useful totalk about common knowledge in the context of public announcements, sothe language may also include the common knowledge operator~$\CKnows_G!A$.\end{document}

content/applied-modal-logic/epistemic-logic/public-announcement-logic-semantics.tex

% Part: applied-modal-logics% Chapter: epistemic-logic% Section: public-announcement-logic-semantics\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{aml}{el}{psm}\olsection{Semantics of Public Announcement Logic}Relational models for public announcement logics are the same as theywere in epistemic logics. However, the semantics for the publicannouncement operator are something new.\begin{defn}\ollabel{defn:mmodels} \emph{Truth of !!a{formula}~$!A$  at~$w$} in a~$\mModel M = \tuple{W, R, V}$, in symbols:  $\mSat{M}{!A}[w]$, is defined inductively as follows:  \begin{enumerate}  \tagitem{prvFalse}{\indcase{!A}{\lfalse}{Never $\mSat{M}{\lfalse}[w]$}.}{}  \tagitem{prvTrue}{\indcase{!A}{\ltrue}{Always $\mSat{M}{\ltrue}[w]$}.}{}  \item $\mSat{M}{p}[w]$ iff $w \in V(p)$  \tagitem{prvNot}{\indcase{!A}{\lnot !B}{$\mSat{M}{\indfrm}[w]$ iff    $\mSat/{M}{!B}[w]$}.}{}  \tagitem{prvAnd}{\indcase{!A}{(!B \land !C)}{$\mSat{M}{\indfrm}[w]$ iff    $\mSat{M}{!B}[w]$ and $\mSat{M}{!C}[w]$}.}{}  \tagitem{prvOr}{\indcase{!A}{(!B \lor !C)}{$\mSat{M}{\indfrm}[w]$ iff    $\mSat{M}{!B}[w]$ or $\mSat{M}{!C}[w]$} (or both).}{}  \tagitem{prvIf}{\indcase{!A}{(!B \lif !C)}{$\mSat{M}{\indfrm}[w]$ iff    $\mSat/{M}{!B}[w]$ or $\mSat{M}{!C}[w]$}.}{}  \tagitem{prvIff}{\indcase{!A}{(!B \liff !C)}{$\mSat{M}{\indfrm}[w]$ iff    either both $\mSat{M}{!B}[w]$ and $\mSat{M}{!C}[w]$ or    neither $\mSat{M}{!B}[w]$ nor $\mSat{M}{!C}[w]$}.}{}  \item\ollabel{defn:sub:mmodels-box}    \indcase{!A}{\Knows_a !B}{$\mSat{M}{\indfrm}[w]$ iff    $\mSat{M}{!B}[w']$ for all $w' \in W$ with $R_a ww'$}  \item\ollabel{defn:sub:mmodels-pal}    \indcase{!A}{[!B] !C}{$\mSat{M}{\indfrm}[w]$ iff    $\mSat{M}{!B}[w]$ implies $\mSat{M \mid !B}{!C}[w]$}    Where $\mModel M \mid !B = \tuple{W', R', V'}$ is defined as  follows:  \begin{enumerate}    \item $W' = \Setabs{ u \in W}{\mSat{M}{!B}[u]}$. So the worlds of      $\mModel M \mid !B$ are the worlds in~$\mModel M$ at which $!B$      holds.    \item $R'_a = R_a \cap (W' \times W')$. Each agent's accessibility      relation is simply restricted to the worlds that remain in~$W'$.    \item $V'(p) = \Setabs{ u \in W'}{u \in V(p) }$. Similarly, the      propositional valuations at worlds remain the same, representing      the idea that informational events will not change the truth      value of propositional variables.  \end{enumerate}    \end{enumerate} \end{defn}What is distinctive, then, about public announcement logics, is thatthe truth of !!a{formula} at~$\mModel M$ can sometimes only be decidedby referring to a model other than~$\mModel M$ itself.Notice also that our semantics treats the announcement operator as a$\Box$~operator, and so if !!a{formula}~$!A$ cannot be truthfullyannounced at a world, then $[!A]B$ will hold there trivially, just asall $\Box$ !!{formula}s hold at endpoints. \begin{figure}  \begin{center}    \begin{tikzpicture}[modal]      \node[world] (w1) [label={below left:$p, \lnot q$}]{$w_1$};       \node[world] (w2) [left=of w1, label={left:$\lnot p, \lnot q$}]{$w_2$};       \node[world] (w3) [above=of w1, label={right:$p, q$}] {$w_3$};      \draw[<->] (w1) to [swap] node {$b$} (w2);      \draw[->,loop below] (w1) to node {$a, b$} (w1);      \draw[<->] (w1) to [swap] node {$a$} (w3);      \draw[->,loop above] (w2) to node {$a, b$} (w2) ;      \draw[->,loop above] (w3) to node {$a, b$} (w3) ;            \node[world](v1)[right of=w1, xshift=1.25in, label={right:$p, \lnot q$}]{$w'_1$};      \node[world](v3)[above of=v1,label={right:$p,q$}]{$w'_3$};      \draw[<->] (v1) to node {$a$} (v3);      \draw[->,loop below] (v1) to node {$a,b$} (v1);      \draw[->,loop above] (v3) to node {$a,b$} (v3) ;            \node(m)[below=of w1]{$\mModel M$};      \node(m')[below=of v1]{$\mModel M \mid p$};       \draw[-,dotted] (w1) to node {\footnotesize announcement of $p$}(v1) ;         \end{tikzpicture}  \end{center}  \caption{Before and after the public announcement of $p$.}  \ollabel{fig:announcement-example}\end{figure}We can see the public announcement of !!a{formula} as shrinking amodel, or restricting it to the worlds at which the !!{formula} wastrue. \olref{fig:announcement-example} gives an example of the effectsof publicly announcing~$p$. One notable thing about that model is thatagent~$b$ learns that~$p$ as a result of the announcement, whileagent~$a$ does not (since $a$ already knew that~$p$ was true).More formally, we have $\mSat{M}{\lnot \Knows_b p}[w_1]$ but $\mSat{M\mid p}{\Knows_b p}[w'_1]$. This implies that $\mSat{M}{[p] \Knows_bp}[w_1]$. But we have some even stronger claims that we can make aboutthe result of the announcement. In fact, it is the case that$\mSat{M}{[p]\CKnows_{\{a,b\}} p}[w_1]$. In other words, after $p$ isannounced, it becomes \emph{common knowledge}.We might wonder, though, whether this holds in the general case, andwhether a truthful announcement of~$!A$ will \emph{always} result in$!A$ becoming common knowledge. It may be surprising that the answeris no. And in fact, it is possible to truthfully announce !!{formula}sthat will no longer be true once they are announced. For example,consider the effects of announcing $p \land \lnot \Knows_b p$ at~$w_1$in \olref{fig:announcement-example}. In fact, $\mModel M \mid p$ and$\mModel M \mid (p \land \lnot \Knows_b p)$ are the same model.However, as we have already noted, $\mSat{M \mid p}{\Knows_bp}[w'_1]$. Therefore, $\mSat{M \mid (p \land \lnot \Knows_b p)}{\lnot(p \land \lnot \Knows_b p)}[w'_1]$, so this is !!a{formula} thatbecomes false once it has been announced. \end{document}