Normal Modal Logics

Syntax and Semantics

content/normal-modal-logic/syntax-and-semantics/syntax-and-semantics.tex

% Part: normal-modal-logic% Chapter: syntax-and-semantics\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{nml}{syn}{Syntax and Semantics}\olimport{introduction}\olimport{language-modal-logic}\olimport{substitution}\olimport{relational-models}\olimport{truth-at-w}\olimport{truth-in-model}\olimport{modal-validity}\olimport{tautological-instances}\olimport{schemas}\olimport{entailment}\OLEndChapterHook\end{document}

content/normal-modal-logic/syntax-and-semantics/introduction.tex

% Part: normal-modal-logic% Chapter: syntax-and-semantics% Section: introduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{syn}{int}\olsection{Introduction}Modal logic deals with \emph{modal propositions} and the entailmentrelations among them. Examples of modal propositions are thefollowing:\begin{enumerate}\item It is necessary that $2+2=4$.\item It is necessarily possible that it will rain tomorrow.\item If it is necessarily possible that~$!A$ then it is possible  that~$!A$.\end{enumerate}Possibility and necessity are not the only modalities: other unaryconnectives are also classified as modalities, for instance, ``itought to be the case that~$!A$,'' ``It will be the case that~$!A$,''``Dana knows that~$!A$,'' or ``Dana believes that~$!A$.''Modal logic makes its first appearance in Aristotle's \emph{De  Interpretatione}: he was the first to notice that necessity impliespossibility, but not vice versa; that possibility and necessity areinter-definable; that If $!A \land !B$ is possibly true then$!A$ is possibly true and $!B$ is possibly true, but notconversely; and that if $!A \to !B$ is necessary, then if$!A$ is necessary, so is~$!B$.The first modern approach to modal logic was the work of C.~I. Lewis,culminating with Lewis and Langford, \emph{Symbolic Logic}(1932). Lewis \& Langford were unhappy with the representation ofimplication by means of the material conditional: $!A \lif !B$is a poor substitute for ``$!A$ implies $!B$.'' Instead, theyproposed to characterize implication as ``Necessarily, if $!A$then $!B$,'' symbolized as $!A \strictif !B$. In trying tosort out the different properties, Lewis identified five differentmodal systems, \Log{S1}, \ldots, \Log{S4}, \Log{S5}, the lasttwo of which are still in use.The approach of Lewis and Langford was purely \emph{syntactical}: theyidentified reasonable axioms and rules and investigated what wasprovable with those means. A semantic approach remained elusive for along time, until a first attempt was made by Rudolf Carnap in\emph{Meaning and Necessity} (1947) using the notion of a \emph{state  description}, i.e., a collection of atomic sentences (those that are``true'' in that state description). After lifting the truthdefinition to arbitrary sentences $!A$, Carnap defines $!A$to be \emph{necessarily true} if it is true in all statedescriptions. Carnap's approach could not handle \emph{iterated}modalities, in that sentences of the form ``Possibly necessarily\ldots possibly $!A$'' always reduce to the innermost modality.The major breakthrough in modal semantics came with Saul Kripke'sarticle ``A Completeness Theorem in Modal Logic'' (JSL 1959). Kripkebased his work on Leibniz's idea that a statement is necessarily trueif it is true ``at all possible worlds.'' This idea, though, suffersfrom the same drawbacks as Carnap's, in that the truth of statement ata world $w$ (or a state description $s$) does not depend on $w$ atall. So Kripke assumed that worlds are related by an\emph{accessibility relation} $R$, and that a statement of the form``Necessarily $!A$'' is true at a world $w$ if and only if$!A$ is true at all worlds $w'$ \emph{accessible from}$w$. Semantics that provide some version of this approach are calledKripke semantics and made possible the tumultuous development of modallogics (in the plural).When interpreted by the Kripke semantics, modal logic shows us what\emph{relational structures} look like ``from the inside.'' Arelational structure is just a set equipped with a binary relation(for instance, the set of students in the class ordered by theirsocial security number is a relational structure). But in factrelational structures come in all sorts of domains: besides relativepossibility of states of the world, we can have epistemic states ofsome agent related by epistemic possibility, or states of a dynamicalsystem with their state transitions, etc. Modal logic can be used tomodel all of these: the first gives us ordinary, alethic, modal logic;the others give us epistemic logic, dynamic logic, etc.We focus on one particular angle, known to modal logicians as``correspondence theory.'' One of the most significant earlydiscoveries of Kripke's is that many properties of the accessibilityrelation~$R$ (whether it is transitive, symmetric, etc.)  can becharacterized \emph{in the modal language} itself by means ofappropriate ``modal schemas.'' Modal logicians say, for instance, thatthe reflexivity of $R$ ``corresponds'' to the schema ``Ifnecessarily~$!A$, then~$!A$''. We explore mainly the correspondencetheory of a number of classical systems of modal logic (e.g., \Log{S4}and \Log{S5}) obtained by a combination of the schemas \Ax{D}, \Ax{T},\Ax{B}, \Ax{4}, and~\Ax{5}.\end{document}

content/normal-modal-logic/syntax-and-semantics/language-modal-logic.tex

% Part: normal-modal-logic% Chapter: syntax-and-semantics% Section: language-modal-logic\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{syn}{lan}\olsection{The Language of Basic Modal Logic}\begin{defn}The basic language of modal 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})}{}.  \tagitem{prvBox}{The modal operator $\Box$.}{}  \tagitem{prvDiamond}{The modal operator $\Diamond$.}{}\end{enumerate}\end{defn}\begin{defn}\emph{!!^{formula}s} of the basic modal 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}.}{}\tagitem{prvBox}{If $!A$ is !!a{formula}, then $\Box !A$ is  !!a{formula}.}{}\tagitem{prvDiamond}{If $!A$ is !!a{formula}, then $\Diamond !A$ is  !!a{formula}.}{}\tagitem{limitClause}{Nothing else is !!a{formula}.}{}\end{enumerate}\end{defn}\begin{tagblock}{defNot,defOr,defAnd,defIf,defIff,defTrue,defFalse,defBox,defDiamond}\begin{defn}Formulas constructed using the defined operators are to be understoodas follows:\begin{tagenumerate}{defTrue,defFalse,defNot,defOr,defAnd,defIf,defIff,defBox,defDiamond}\tagitem{defTrue}{$\ltrue$ abbreviates  \iftag{prvFalse}{$\lnot\lfalse$}{$(!A \lor \lnot !A)$ for some    fixed atomic !!{formula}~$!A$}.}{}\tagitem{defFalse}{$\lfalse$ abbreviates  \iftag{prvTrue}{$\lnot\ltrue$}{$(!A \land \lnot !A)$ for some    fixed atomic !!{formula}~$!A$}.}{}\tagitem{defNot}{$\lnot !A$ abbreviates $!A \lif \lfalse$.}{}\tagitem{defOr}{$!A \lor !B$ abbreviates  \iftag{prvAnd}{$\lnot(\lnot !A \land \lnot !B)$}{$\lnot !A \lif    !B$}.}{}\tagitem{defAnd}{$!A \land !B$ abbreviates  \iftag{prvOr}{$\lnot(\lnot !A \lor \lnot !B)$}{$\lnot (!A \lif    \lnot !B)$}.}{}\tagitem{defIf}{$!A \lif !B$ abbreviates  \iftag{prvOr}{$\lnot !A \lor !B)$}{$\lnot (!A \land \lnot !B)$}.}{}\tagitem{defIff}{$!A \liff !B$ abbreviates $(!A \lif !B) \land (!B  \lif !A)$.}{}\tagitem{defBox}{$\Box !A$ abbreviates $\lnot\Diamond\lnot !A$. }{}\tagitem{defDiamond}{$\Diamond !A$ abbreviates $\lnot\Box\lnot !A$.}{}\end{tagenumerate}\end{defn}\end{tagblock}If !!a{formula}~$!A$ does not contain $\Box$ or $\Diamond$, we say itis \emph{modal-free}.\end{document}

content/normal-modal-logic/syntax-and-semantics/substitution.tex

% Part: normal-modal-logic% Chapter: syntax-and-semantics% Section: substitution\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{syn}{sub}\olsection{Simultaneous Substitution}An \emph{instance} of !!a{formula}~$!A$ is the result of replacing alloccurrences of !!a{propositional variable} in~$!A$ by some other!!{formula}. We will refer to instances of !!{formula}s often, bothwhen discussing validity and when discussing !!{derivability}. Ittherefore is useful to define the notion precisely.\begin{defn}\ollabel{def:subst-inst}  Where $!A$ is a modal !!{formula} all of whose !!{propositional    variable}s are among $p_1$, \dots, $p_n$, and $!D_1$, \dots,  $!D_n$ are also modal !!{formula}s, we define  $\SSubst{!A}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}$ as the  result of simultaneously substituting each $!D_i$ for $p_i$  in~$!A$. Formally, this is a definition by induction on~$!A$:  \begin{enumerate}    \tagitem{prvFalse}{\indcase{!A}{\lfalse}{%        $\SSubst{\indfrm}{\subst{!D_1}{p_1}, \dots,          \subst{!D_n}{p_n}}$ is $\lfalse$.}}{}    \tagitem{prvTrue}{\indcase{!A}{\ltrue}{%        $\SSubst{\indfrm}{\subst{!D_1}{p_1}, \dots,          \subst{!D_n}{p_n}}$ is $\ltrue$.}}{}    \item \indcase{!A}{q}{$\SSubst{\indfrm}{\subst{!D_1}{p_1}, \dots,        \subst{!D_n}{p_n}}$ is $q$, provided $q \not\ident p_i$ for $i      = 1$, \dots,~$n$.}    \item \indcase{!A}{p_i}{$\SSubst{\indfrm}{\subst{!D_1}{p_1},        \dots, \subst{!D_n}{p_n}}$ is $!D_i$.}    \tagitem{prvNot}{\indcase{!A}{\lnot !B}{%        $\SSubst{\indfrm}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}$ is        $\lnot \SSubst{!B}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}$.}}{}    \tagitem{prvAnd}{\indcase{!A}{(!B \land        !C)}{$\SSubst{\indfrm}{\subst{!D_1}{p_1}, \dots,          \subst{!D_n}{p_n}}$ is        \[(\SSubst{!B}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}} \land          \SSubst{!C}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}).\]}}{}    \tagitem{prvOr}{\indcase{!A}{(!B \lor          !C)}{$\SSubst{\indfrm}{\subst{!D_1}{p_1}, \dots,          \subst{!D_n}{p_n}}$ is        \[(\SSubst{!B}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}} \lor          \SSubst{!C}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}).\]}}{}    \tagitem{prvIf}{\indcase{!A}{(!B \lif          !C)}{$\SSubst{\indfrm}{\subst{!D_1}{p_1}, \dots,          \subst{!D_n}{p_n}}$ is        \[(\SSubst{!B}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}} \lif          \SSubst{!C}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}).\]}}{}    \tagitem{prvIf}{\indcase{!A}{(!B \liff          !C)}{$\SSubst{\indfrm}{\subst{!D_1}{p_1}, \dots,          \subst{!D_n}{p_n}}$ is        \[(\SSubst{!B}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}} \liff          \SSubst{!C}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}).\]}}{}    \item \indcase{!A}{\Box !B}{%        $\SSubst{\indfrm}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}$ is        $\Box        \SSubst{!B}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}.$}    \tagitem{prvDiamond}{\indcase{!A}{\Diamond !B}{%        $\SSubst{\indfrm}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}$ is        $\Diamond        \SSubst{!B}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}}.$}}{}  \end{enumerate}  The !!{formula} $\SSubst{!A}{\subst{!D_1}{p_1}, \dots,    \subst{!D_n}{p_n}}$ is called a \emph{substitution instance}  of~$!A$.\end{defn}\begin{ex}  Suppose $!A$ is $p_1 \lif \Box(p_1 \land p_2)$, $!D_1$ is  $\Diamond(p_2 \lif p_3)$ and $!D_2$ is $\lnot\Box p_1$. Then  $\SSubst{!A}{\subst{!D_1}{p_1}, \subst{!D_2}{p_2}}$ is  \begin{align*}    \Diamond(p_2 \lif p_3) &    \lif \Box(\Diamond(p_2 \lif p_3) \land \lnot\Box p_1)    \intertext{while $\SSubst{!A}{\subst{!D_2}{p_1}, \subst{!D_1}{p_2}}$ is}    \lnot\Box p_1 &    \lif \Box(\lnot\Box p_1 \land \Diamond(p_2 \lif p_3))    \intertext{Note that simultaneous substitution is in general not      the same as iterated substitution, e.g., compare      $\SSubst{!A}{\subst{!D_1}{p_1}, \subst{!D_2}{p_2}}$ above with      $\Subst{(\Subst{!A}{!D_1}{p_1})}{!D_2}{p_2}$, which is:}    \Diamond(p_2 \lif p_3) & \Subst{\lif \Box(\Diamond(p_2 \lif p_3) \land p_2)}{\lnot\Box p_1}{p_2}, \text{ i.e.,}\\    \Diamond(\lnot\Box p_1 \lif p_3) &    \lif \Box(\Diamond(\lnot\Box p_1    \lif p_3) \land \lnot\Box p_1)\\    \intertext{and with $\Subst{(\Subst{!A}{!D_2}{p_2})}{!D_1}{p_1}$:}    p_1 & \lif \Subst{\Box(p_1 \land \lnot\Box p_1)}{\Diamond(p_2 \lif p_3)}{p_1}, \text{ i.e.,}\\    \Diamond(p_2 \lif p_3) &    \lif \Box(\Diamond(p_2    \lif p_3) \land \lnot\Box\Diamond(p_2 \lif p_3)).  \end{align*}\end{ex}\end{document}

content/normal-modal-logic/syntax-and-semantics/relational-models.tex

% Part: normal-modal-logic% Chapter: syntax-and-semantics% Section: relational-models\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{syn}{rel}\olsection{Relational Models}The basic concept of semantics for normal modal logics is that of a\emph{relational model}. It consists of a set of worlds, which arerelated by a binary ``accessibility relation,'' together with anassignment which determines which !!{propositional variable}s count as``true'' at which worlds.\begin{defn}  A \emph{model} for the basic modal language is a triple $\mModel{M}  = \tuple{W, R, V}$, where  \begin{enumerate}  \item $W$ is a nonempty set of ``worlds,''  \item $R$ 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 $Rww'$ holds, we say that $w'$ is \emph{accessible    from}~$w$. When $w \in V(p)$ we say $p$ is \emph{true at}~$w$.\end{defn}The great advantage of relational semantics is that models can berepresented by means of simple diagrams, such as the one in\olref{fig:simple}. Worlds are represented by nodes, and world~$w'$ isaccessible from~$w$ precisely when there is an arrow from~$w$to~$w'$. Moreover, we label a node (world) by~$\mTrue{p}$ when $w \in V(p)$,and otherwise by~\mFalse{p}. \olref{fig:simple} represents the modelwith $W = \{w_1, w_2, w_3\}$, $R = \{\tuple{w_1, w_2},\tuple{w_1,  w_3}\}$, $V(p) = \{w_1, w_2\}$, and $V(q) = \{w_2\}$.\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 (w2);      \draw[->] (w1) to (w3);    \end{tikzpicture}  \end{center}  \caption{A simple model.}  \ollabel{fig:simple}\end{figure}\end{document}

content/normal-modal-logic/syntax-and-semantics/truth-at-w.tex

% Part: normal-modal-logic% Chapter: syntax-and-semantics% Section: truth-at-w\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{syn}{trw}\olsection{Truth at a World}Every modal model determines which modal !!{formula}s count as true atwhich worlds in it. The relation ``model $\mModel{M}$ makes!!{formula}~$!A$ true at world~$w$'' is the basic notion of relationalsemantics. The relation is defined inductively and coincides with theusual characterization using truth tables for the 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}{\Box !B}{$\mSat{M}{\indfrm}[w]$ iff    $\mSat{M}{!B}[w']$ for all $w' \in W$ with $Rww'$.}  \item\ollabel{defn:sub:mmodels-diamond}    \indcase{!A}{\Diamond !B}{$\mSat{M}{\indfrm}[w]$ iff    $\mSat{M}{!B}[w']$ for at least one $w' \in W$ with $Rww'$.}  \end{enumerate}\end{defn}Note that by clause~\olref{defn:sub:mmodels-box}, !!a{formula}~$\Box!B$ is true at~$w$ whenever there are no~$w'$ with $Rww'$. Insuch a case $\Box !B$ is \emph{vacuously} true at~$w$. Also,$\Box !B$ may be satisfied at~$w$ even if $!B$ is not. The truthof~$!B$ at~$w$ does not guarantee the truth of~$\Diamond !B$at~$w$. This holds, however, if $Rww$, e.g., if $R$ is reflexive.  Ifthere is no $w'$ such that $Rww'$, then $\mSat/{M}{\Diamond !A}[w]$,for any~$!A$.\begin{prob}  Consider the model of \olref[nml][syn][rel]{fig:simple}. Which of the  following hold?    \begin{enumerate}    \item $\mSat{M}{q}[w_1]$;    \item $\mSat{M}{\lnot q}[w_3]$;    \item $\mSat{M}{p \lor q}[w_1]$;    \item $\mSat{M}{\Box (p \lor q)}[w_1]$;    \item $\mSat{M}{\Box q}[w_3]$;    \item $\mSat{M}{\Box \bot}[w_3]$;    \item $\mSat{M}{\Diamond q}[w_1]$;    \item $\mSat{M}{\Box q}[w_1]$;    \item $\mSat{M}{\lnot \Box\Box \lnot q}[w_1]$.    \end{enumerate}\end{prob}% Prove duality of \Box and \Diamond\begin{tagblock}{prvDiamond}\begin{prop}\ollabel{prop:dual}  \begin{enumerate}  \item $\mSat{M}{\Box !A}[w]$ iff $\mSat{M}{\lnot\Diamond\lnot !A}[w]$.  \item $\mSat{M}{\Diamond !A}[w]$ iff $\mSat{M}{\lnot\Box\lnot !A}[w]$.  \end{enumerate}\end{prop}\begin{proof}  \begin{enumerate}    \item $\mSat{M}{\lnot\Diamond\lnot !A}[w]$ iff $\mSat/{M}{\Diamond\lnot      !A}[w]$ by definition of $\mSat{M}{}[w]$. $\mSat{M}{\Diamond\lnot      !A}[w]$ iff for some $w'$ with $Rww'$, $\mSat{M}{\lnot      !A}[w']$. Hence, $\mSat/{M}{\Diamond\lnot !A}[w]$ iff for all    $w'$ with $Rww'$, $\mSat/{M}{\lnot !A}[w']$. We also have    $\mSat/{M}{\lnot !A}[w']$ iff $\mSat{M}{!A}[w']$. Together we have    $\mSat{M}{\lnot\Diamond\lnot !A}[w]$ iff for all $w'$ with $Rww'$,    $\mSat{M}{!A}[w']$. Again by definition of $\mSat{M}{}[w]$, that      is the case iff $\mSat{M}{\Box !A}[w]$.    \item \iftag{probDiamond}{Exercise.}{$\mSat{M}{\lnot\Box\lnot !A}[w]$ iff      $\mSat/{M}{\Box\lnot !A}$. $\mSat{M}{\Box\lnot !A}[w]$ iff for all      $w'$ with $Rww'$, $\mSat{M}{\lnot !A}[w']$. Hence,      $\mSat/{M}{\Box\lnot !A}[w]$ iff for some $w'$ with $Rww'$,      $\mSat/{M}{\lnot !A}[w']$. We also have $\mSat/{M}{\lnot        !A}[w']$ iff $\mSat{M}{!A}[w']$. Together we have      $\mSat{M}{\lnot\Box\lnot !A}[w]$ iff for some~$w'$ with      $Rww'$, $\mSat{M}{!A}[w']$. Again by definition of      $\mSat{M}{}[w]$, that is the case iff $\mSat{M}{\Diamond        !A}[w]$.}  \end{enumerate}\end{proof}\begin{probtag}{probDiamond}  Complete the proof of \olref[nml][syn][trw]{prop:dual}.\end{probtag}\end{tagblock}\begin{prob}  Let $\mModel{M} = \tuple{W, R, V}$ be a model, and suppose $w_1, w_2 \in  W$ are such that:  \begin{enumerate}  \item $w_1 \in V(p)$ if and only if $w_2 \in V(p)$ (for every !!{propositional variable} $p$); and  \item for all $w \in W$: $Rw_1w$ if and only if $Rw_2w$.  \end{enumerate}  Using induction on !!{formula}s, show that for all !!{formula}s $!A$:  $\mSat{M}{!A}[w_1]$ if and only if $\mSat{M}{!A}[w_2]$.\end{prob}\begin{probtag}{prvDiamond}  Let $\mModel{M} = \tuple{W, R, V}$. Show that  $\mSat{M}{\lnot\Diamond !A}[w]$ if and only if  $\mSat{M}{\Box\lnot!A}[w]$.\end{probtag}\end{document}

content/normal-modal-logic/syntax-and-semantics/truth-in-model.tex

% Section: truth-in-model\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{syn}{tru}\olsection{Truth in a Model}Sometimes we are interested in which !!{formula}s are true at every worldin a given model. Let's introduce a notation for this.\begin{defn}  !!^a{formula}~$!A$ is \emph{true in a model} $M = \tuple{W, R,    V}$, written $\mSat{M}{!A}$, if and only if $\mSat{M}{!A}[w]$  for every $w \in W$.\end{defn}\begin{prop}\ollabel{prop:truthfacts}  \begin{enumerate}  \item If $\mSat{M}{!A}$ then $\mSat/{M}{\lnot !A}$, but \emph{not}    vice-versa.  \item If $\mSat{M}{!A \lif !B}$ then $\mSat{M}{!A}$ only if    $\mSat{M}{!B}$, but \emph{not} vice-versa.  \end{enumerate}\end{prop}\begin{proof}  \begin{enumerate}  \item If $\mSat{M}{!A}$ then $!A$ is true at all worlds in $W$, and    since $W \neq \emptyset$, it can't be that $\mSat{M}{\lnot!A}$, or    else $!A$ would have to be both true and false at some    world.    On the other hand, if $\mSat/{M}{\lnot !A}$ then $!A$ is true at    some world $w \in W$. It does not follow that $\mSat{M}{!A}[w]$    for \emph{every}~$w \in W$. For instance, in the model of    \olref[rel]{fig:simple}, $\mSat/{M}{\lnot p}$, and also $\mSat/{M}{p}$.  \item Assume $\mSat{M}{!A \lif !B}$ and $\mSat{M}{!A}$; to show    $\mSat{M}{!B}$ let $w \in W$ be an arbitrary world. Then    $\mSat{M}{!A \lif !B}[w]$ and $\mSat{M}{!A}[w]$, so    $\mSat{M}{!B}[w]$, and since $w$ was arbitrary,    $\mSat{M}{!B}$.    To show that the converse fails, we need to find a model    $\mModel{M}$ such that $\mSat{M}{!A}$ only if $\mSat{M}{!B}$, but    $\mSat/{M}{!A \lif !B}$. Consider again the model of    \olref[rel]{fig:simple}: $\mSat/{M}{p}$ and hence (vacuously)    $\mSat{M}{p}$ only if $\mSat{M}{q}$. However, $\mSat/{M}{p \lif      q}$, as $p$ is true but $q$ false at~$w_1$.  \end{enumerate}\end{proof}\begin{prob}  Consider the following model $\mModel{M}$ for the language  comprising $p_1$, $p_2$, $p_3$ as the only !!{propositional variable}s:  \begin{center}    \begin{tikzpicture}[modal]      \node[world] (w1) [label={[align=right]left:\mTrue{p_1}\\\mFalse{p_2}\\\mFalse{p_3}}]            {$w_1$} ;       \node[world] (w2) [label={[align=right]right:\mTrue{p_1}\\\mTrue{p_2}\\\mFalse{p_3}},        below right=of w1]  {$w_2$};       \node[world] (w3) [label={[align=right]right:\mTrue{p_1}\\\mTrue{p_2}\\\mTrue{p_3}},        above right=of w2] {$w_3$};      \draw[reflexive above] (w3) to (w3);       \draw[->] (w1) to (w2);      \draw[->] (w2) to (w3);      \draw[->] (w1) to (w3);     \end{tikzpicture}  \end{center}  Are the following !!{formula}s and schemas true in the model $\mModel{M}$,  i.e., true at every world in $\mModel{M}$? Explain.  \begin{enumerate}  \item $p\lif \Diamond p$ (for $p$ atomic);  \item $!A\lif \Diamond !A$ (for $!A$ arbitrary);  \item $\Box p \lif p$ (for $p$ atomic);  \item $\lnot p \lif \Diamond \Box p$ (for $p$ atomic);  \item $\Diamond \Box !A$ (for $!A$ arbitrary);  \item $\Box \Diamond p$ (for $p$ atomic).   \end{enumerate}\end{prob}\end{document}

content/normal-modal-logic/syntax-and-semantics/modal-validity.tex

% Part: normal-modal-logic% Chapter: syntax-and-semantics% Section: modal-validity\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{syn}{val}\olsection{Validity}\begin{explain}  !!^{formula}s that are true in all models, i.e., true at every world  in every model, are particularly interesting. They represent those  modal propositions which are true regardless of how $\Box$ and  $\Diamond$ are interpreted, as long as the interpretation is  ``normal'' in the sense that it is generated by some accessibility  relation on possible worlds. We call such !!{formula}s  \emph{valid}. For instance, $\Box(p \land q) \lif \Box p$ is  valid. Some !!{formula}s one might expect to be valid on the basis  of the alethic interpretation of $\Box$, such as $\Box p \lif p$,  are not valid, however.  Part of the interest of relational models  is that different interpretations of $\Box$ and $\Diamond$ can be  captured by different kinds of accessibility relations. This  suggests that we should define validity not just relative to  \emph{all} models, but relative to all models \emph{of a certain    kind}. It will turn out, e.g., that $\Box p \lif p$ is true in all  models where every world is accessible from itself, i.e., $R$ is  reflexive. Defining validity relative to classes of models enables  us to formulate this succinctly: $\Box p \lif p$ is valid in the  class of reflexive models.\end{explain}\begin{defn}  !!^a{formula}~$!A$ is \emph{valid} in a class $\mClass{C}$ of  models if it is true in every model in~$\mClass{C}$ (i.e., true at  every world in every model in~$\mClass{C}$). If $!A$ is valid  in~$\mClass{C}$, we write $\mClass{C} \Entails !A$, and we  write $\Entails !A$ if $!A$ is valid in the class of  \emph{all} models.\end{defn}\begin{prop}\ollabel{prop:subset-class}  If $!A$ is valid in $\mClass{C}$ it is also valid in each class  $\mClass{C}' \subseteq \mClass{C}$.\end{prop}\begin{prop}\ollabel{prop:Nec-rule}  If $!A$ is valid, then so is $\Box!A$. \end{prop}\begin{proof}  Assume $\Entails !A$. To show $\Entails \Box!A$ let $\mModel{M} =  \tuple{W, R, V}$ be a model and $w \in W$. If $Rww'$ then  $\mSat{M}{!A}[w']$, since $!A$ is valid, and so also  $\mSat{M}{\Box!A}[w]$. Since $\mModel{M}$ and $w$ were  arbitrary, $\Entails \Box!A$.\end{proof}\begin{prob}  Show that the following are valid:  \begin{enumerate}  \item $\Box p \lif \Box (q \lif p)$;  \item $\Box \lnot \lfalse$;  \item $\Box p \lif (\Box q \lif \Box p)$.  \end{enumerate}\end{prob}\begin{prob}  Show that $!A \lif \Box!A$ is valid in the class $\mClass{C}$ of  models $\mModel{M} = \tuple{W, R, V}$ where $W = \{w\}$. Similarly,  show that $!B \lif \Box !A$ and $\Diamond !A \lif !B$ are valid in  the class of models $\mModel{M} = \tuple{W, R, V}$ where  $R = \emptyset$.\end{prob}\end{document}

content/normal-modal-logic/syntax-and-semantics/tautological-instances.tex

% Part: normal-modal-logic% Chapter: syntax-and-semantics% Section: tautological-instances\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{syn}{tau}\olsection{Tautological Instances}\begin{explain}A modal-free formula is a tautology if it is true under everytruth-value assignment. Clearly, every tautology is true at everyworld in every model. But for !!{formula}s involving $\Box$and~$\Diamond$, the notion of tautology is not defined. Is it thecase, e.g., that $\Box p \lor \lnot \Box p$---an instance of theprinciple of excluded middle---is valid? The notion of a\emph{tautological instance} helps: !!a{formula} that is asubstitution instance of a (non-modal) tautology. It is notsurprising, but still requires proof, that every tautological instanceis valid.\end{explain}\begin{defn}  A modal !!{formula}~$!B$ is a \emph{tautological instance} if and  only if there is a modal-free tautology~$!A$ with !!{propositional    variable}s $p_1$, \dots,~$p_n$ and !!{formula}s $!D_1$,  \dots,~$!D_n$ such that $!B \ident \SSubst{!A}{\subst{!D_1}{p_1},    \dots, \subst{!D_n}{p_n}}$.\end{defn}\begin{lem}\ollabel{lem:valid-taut}  Suppose $!A$ is a modal-free !!{formula} whose !!{propositional  variable}s are $p_1$, \dots, $p_n$, and let $!D_1$, \dots,  $!D_n$ be modal !!{formula}s. Then for any assignment $\pAssign{v}$,  any model $\mModel{M} = \tuple{W, R, V}$, and any $w \in W$ such  that $\pAssign{v}(p_i) = \True$ if and only if $\mSat{M}{!D_i}[w]$ we have  that $\pSat{v}{!A}$ if and only if  $\mSat{M}{\SSubst{!A}{\subst{!D_1}{p_1}, \dots,      \subst{!D_n}{p_n}}}[w]$.\end{lem}\begin{proof}  By induction on $!A$.  \begin{enumerate}  \tagitem{prvFalse}{\indcase{!A}{\lfalse}{Both $\pSat/{v}{\lfalse}$      and $\mSat/{M}{\lfalse}[w]$}.}{}  \tagitem{prvTrue}{\indcase{!A}{\ltrue}{Both $\pSat{v}{\ltrue}$      and $\mSat{M}{\ltrue}[w]$}.}{}  \item \indcase{!A}{p_i}{%    \begin{align*}      \pSat{v}{p_i} \Leftrightarrow {} & \pAssign{v}(p_i) = \True \\      & \qquad \text{by definition of $\pSat{v}{p_i}$}\\      \Leftrightarrow {} & \mSat{M}{!D_i}[w] \\      &\qquad \text{by assumption}\\      \Leftrightarrow {} & \mSat{M}{\SSubst{p_i}{\subst{!D_1}{p_1}, \dots,          \subst{!D_n}{p_n}}}[w]\\      &\qquad \text{since $\SSubst{p_i}{\subst{!D_1}{p_1}, \dots,          \subst{!D_n}{p_n}} \ident !D_i$}.      \end{align*}}  \tagitem{prvFalse}{\indcase{!A}{\lnot !B}{%      \begin{align*}        \pSat{v}{\lnot !B} \Leftrightarrow {} & \pSat/{v}{!B}\\        &\qquad \text{by definition of $\pSat{v}{}$};\\        \Leftrightarrow {} & \mSat/{M}{\SSubst{!B}{\subst{!D_1}{p_1}, \dots,          \subst{!D_n}{p_n}}}[w]\\        &\qquad \text{by induction hypothesis}\\        \Leftrightarrow {} &        \mSat{M}{\SSubst{\lnot !B}{\subst{!D_1}{p_1}, \dots,          \subst{!D_n}{p_n}}}[w]\\        &\qquad \text{by definition of $\pSat{v}{}$}.      \end{align*}}}{}  \tagitem{prvAnd}{\indcase{!A}{(!B \land !C)}{%      \begin{align*}        \pSat{v}{!B \land !C} \Leftrightarrow {} &        \pSat{v}{!B} \text{ and } \pSat{v}{!C}\\        &\qquad \text{by definition of $\pSat{v}{}$}\\        \Leftrightarrow {} &        \mSat{M}{\SSubst{!B}{\subst{!D_1}{p_1}, \dots,            \subst{!D_n}{p_n}}}[w] \text{ and } \\        & \mSat{M}{\SSubst{!C}{\subst{!D_1}{p_1}, \dots,          \subst{!D_n}{p_n}}}[w]\\        &\qquad \text{by induction hypothesis}\\        \Leftrightarrow{} &        \mSat{M}{\SSubst{(!B \land !C)}{\subst{!D_1}{p_1}, \dots,          \subst{!D_n}{p_n}}}[w]\\        &\qquad \text{by definition of $\mSat{M}{}[w]$}.      \end{align*}}}{}  \tagitem{prvOr}{\indcase{!A}{(!B \lor !C)}{%      \begin{align*}        \pSat{v}{!B \lor !C} \Leftrightarrow{} &        \pSat{v}{!B} \text{ or } \pSat{v}{!C}\\        &\qquad \text{by definition of $\pSat{v}{}$};\\        \Leftrightarrow{} & \mSat{M}{\SSubst{!B}{\subst{!D_1}{p_1}, \dots,            \subst{!D_n}{p_n}}}[w] \text{ or }\\        & \mSat{M}{\SSubst{!C}{\subst{!D_1}{p_1}, \dots,          \subst{!D_n}{p_n}}}[w]\\        &\qquad \text{by induction hypothesis}\\        \Leftrightarrow{} &        \mSat{M}{\SSubst{(!B \lor !C)}{\subst{!D_1}{p_1}, \dots,          \subst{!D_n}{p_n}}}[w]\\        &\qquad \text{by definition of $\mSat{M}{}[w]$}.      \end{align*}}}{}  \tagitem{prvIf}{\indcase{!A}{(!B \lif !C)}{%      \begin{align*}        \pSat{v}{!B \lif !C} \Leftrightarrow{} &        \pSat/{v}{!B} \text{ or } \pSat{v}{!C}\\        &\qquad \text{by definition of $\pSat{v}{}$}\\        \Leftrightarrow{} &        \mSat/{M}{\SSubst{!B}{\subst{!D_1}{p_1}, \dots,            \subst{!D_n}{p_n}}}[w] \text{ or }\\        & \mSat{M}{\SSubst{!C}{\subst{!D_1}{p_1}, \dots,          \subst{!D_n}{p_n}}}[w]\\        &\qquad \text{by induction hypothesis}\\        \Leftrightarrow{} &        \mSat{M}{\SSubst{(!B \lif !C)}{\subst{!D_1}{p_1}, \dots,          \subst{!D_n}{p_n}}}[w]\\        &\qquad \text{by definition of $\mSat{M}{}[w]$}.      \end{align*}}}{}  \tagitem{prvIff}{\indcase{!A}{(!B \liff !C)}{%      \begin{align*}        \pSat{v}{!B \lif !C} \Leftrightarrow {} &        \text{either } \pSat{v}{!B} \text{ and } \pSat{v}{!C}\\        & \text{or } \pSat/{v}{!B} \text{ and } \pSat/{v}{!C}\\        &\qquad \text{by definition of $\pSat{v}{}$}\\        \Leftrightarrow {} &        \text{either } \mSat{M}{\SSubst{!B}{\subst{!D_1}{p_1}, \dots,            \subst{!D_n}{p_n}}}[w] \text{ and }\\        & \qquad \mSat{M}{\SSubst{!C}{\subst{!D_1}{p_1}, \dots,          \subst{!D_n}{p_n}}}[w]\\         &  \text{ or } \mSat/{M}{\SSubst{!B}{\subst{!D_1}{p_1}, \dots,            \subst{!D_n}{p_n}}}[w] \text{ and }\\        & \qquad \mSat/{M}{\SSubst{!C}{\subst{!D_1}{p_1}, \dots,          \subst{!D_n}{p_n}}}[w]\\        &\qquad\text{by induction hypothesis}\\        \Leftrightarrow {} &        \mSat{M}{\SSubst{(!B \liff !C)}{\subst{!D_1}{p_1}, \dots,          \subst{!D_n}{p_n}}}[w]\\        &\qquad \text{by definition of $\mSat{M}{}[w]$}.      \end{align*}}}{}  \end{enumerate}  \end{proof}\begin{prop}\ollabel{prop:valid-taut}  All tautological instances are valid.\end{prop}\begin{proof}  Contrapositively, suppose $!A$ is such that  $\mSat/{M}{\SSubst{!A}{\subst{!D_1}{p_1}, \dots,  \subst{!D_n}{p_n}}}[w]$, for some model $\mModel{M}$ and world~$w$.  Define an assignment $\pAssign{v}$ such that $\pAssign{v}(p_i) =  \True$ if and only if $\mSat{M}{!D_i}[w]$ (and $\pAssign{v}$ assigns  arbitrary values to $q \notin \{p_1, \dots, p_n \}$).  Then by  \olref{lem:valid-taut}, $\pSat/{v}{!A}$, so $!A$ is not a tautology.\end{proof}\end{document}

content/normal-modal-logic/syntax-and-semantics/schemas.tex

% Part: normal-modal-logic% Chapter: syntax-and-semantics% Section: schemas\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{syn}{sch}\olsection{Schemas and Validity}\begin{defn}  A \emph{schema} is a set of !!{formula}s comprising all  and only the substitution instances of some modal !!{formula}~$!C$, i.e.,  \[  \Setabs{!B}{\lexists[!D_1], \dots, \lexists[!D_n] \left(!B =  \SSubst{!C}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}} \right) }.  \]  The !!{formula}~$!C$ is called the \emph{characteristic} !!{formula} of  the schema, and it is unique up to a renaming of the !!{propositional  variable}s. !!^a{formula}~$!A$ is an \emph{instance} of a schema if  it is a member of the set.\end{defn}It is convenient to denote a schema by the meta-linguistic expressionobtained by substituting `$!A$', `$!B$',~\dots, for the atomiccomponents of~$!C$. So, for instance, the following denote schemas:`$!A$', `$!A \lif \Box!A$', `$!A \lif (!B \lif !A)$'. They correspondto the characteristic !!{formula}s $p$, $p \lif \Box p$, $p \lif (q\lif p)$. The schema `$!A$' denotes the set of \emph{all}!!{formula}s.\begin{defn}  A schema is \emph{true} in a model if and only if all of its instances  are; and a schema is \emph{valid} if and only if it is true in every  model.\end{defn}\begin{prop}\ollabel{prop:Kvalid}  The following schema \Ax{K} is valid  \begin{equation*}  \Box(!A \lif !B) \lif (\Box !A \lif \Box !B). \tag{\Ax{K}}  \end{equation*}\end{prop}\begin{proof}  We need to show that all instances of the schema are true at every  world in every model. So let $\mModel{M} = \tuple{W,R,V}$ and $w \in  W$ be arbitrary. To show that a conditional is true at a world we  assume the antecedent is true to show that the consequent is true as  well. In this case, let $\mSat{M}{\Box(!A \lif !B)}[w]$ and  $\mSat{M}{\Box !A}[w]$. We need to show $\mSat{M}{\Box !B}[w]$. So let  $w'$ be arbitrary such that $Rww'$. Then by the first assumption  $\mSat{M}{!A \lif !B}[w']$ and by the second assumption  $\mSat{M}{!A}[w']$. It follows that $\mSat{M}{!B}[w']$. Since $w'$  was arbitrary, $\mSat{M}{\Box !B}[w]$.\end{proof}\begin{prop}\ollabel{prop:Dual-valid}  The following schema \Dual{} is valid  \begin{equation*}  \Diamond !A \liff \lnot\Box\lnot !A. \tag{\Dual}  \end{equation*}\end{prop}\begin{proof}  Exercise.\end{proof}\begin{prob}  Prove \olref[nml][syn][sch]{prop:Dual-valid}.\end{prob}\begin{prop}\ollabel{prop:soundMP}  If $!A$ and $!A \lif !B$ are true at a world in a model  then so is $!B$. Hence, the valid !!{formula}s are closed under  modus ponens.\end{prop}\begin{prop}\ollabel{prop:valid-instances}  !!^a{formula}~$!A$ is valid iff all its substitution instances  are. In other words, a schema is valid iff its characteristic  !!{formula} is.\end{prop}\begin{proof}  The ``if'' direction is obvious, since $!A$ is a substitution  instance of itself.  To prove the ``only if'' direction, we show the following: Suppose  $\mModel{M} = \tuple{W, R, V}$ is a modal model, and $!B \ident  \SSubst{!A}{\subst{!D_1}{p_1},\dots,\subst{!D_n}{p_n}}$ is a  substitution instance of~$!A$. Define $\mModel{M'} = \tuple{W, R,    V'}$ by $V'(p_i) = \Setabs{w}{\mSat{M}{!D_i}[w]}$.  Then  $\mSat{M}{!B}[w]$ iff $\mSat{M'}{!A}[w]$, for any~$w \in W$. (We  leave the proof as an exercise.) Now suppose that $!A$ was valid,  but some substitution instance $!B$ of~$!A$ was not valid. Then for  some $\mModel{M} = \tuple{W, R, V}$ and some $w \in W$,  $\mSat/{M}{!B}[w]$. But then $\mSat/{M'}{!A}[w]$ by the claim, and  $!A$ is not valid, a contradiction.\end{proof}\begin{prob}  Prove the claim in the ``only if'' part of the proof of  \olref[nml][syn][sch]{prop:valid-instances}. (Hint: use induction  on~$!A$.)\end{prob}Note, however, that it is not true that a schema is true in a modeliff its characteristic formula is. Of course, the ``only if''direction holds: if every instance of $!A$ is true in~$\mModel{M}$,$!A$~itself is true in~$\mModel{M}$. But it may happen that $!A$ istrue in~$\mModel{M}$ but some instance of~$!A$ is false at some worldin~$\mModel{M}$. For a very simple counterexample consider~$p$ in amodel with only one world~$w$ and $V(p) = \{w\}$, so that $p$ is trueat~$w$. But $\lfalse$ is an instance of~$p$, and not true at~$w$.\begin{prob}  Show that none of the following !!{formula}s are valid:  \begin{enumerate}    \item[\Ax{D}:] \quad $\Box p \lif \Diamond p$;    \item[\Ax{T}:] \quad $\Box p \lif p$;    \item[\Ax{B}:] \quad $p \lif \Box\Diamond p$;    \item[\Ax{4}:] \quad $\Box p \lif \Box \Box p$;    \item[\Ax{5}:] \quad $\Diamond p \lif \Box \Diamond      p$.  \end{enumerate}\end{prob}\begin{table}[t]    \centering    \begin{tabular}{| l || l |}      \hline      {\emph{Valid Schemas}} & {\emph{Invalid Schemas}} \\      \hline\hline      $\Box(!A \lif !B) \lif (\Diamond !A \lif \Diamond !B)$      & $\Box (!A \lor !B) \lif (\Box !A \lor \Box !B)$ \\      $\Diamond (!A \lif !B) \lif (\Box !A \lif \Diamond      !B)$      & $(\Diamond !A \land \Diamond !B) \lif \Diamond (!A      \land !B)$\\      $\Box (!A \land !B) \liff (\Box !A \land \Box !B)$      & $!A \lif \Box !A$ \\      $\Box !A \lif \Box (!B \lif !A)$      & $\Box \Diamond !A \lif !B$ \\      $\lnot \Diamond !A \lif \Box (!A \lif !B)$      & $\Box \Box !A \lif \Box !A$ \\      $\Diamond (!A \lor !B) \liff (\Diamond !A \lor      \Diamond !B)$      & $\Box \Diamond !A \lif \Diamond \Box !A$. \\      \hline    \end{tabular}    \caption{Valid and (or?) invalid schemas.}    \ollabel{tab:valid-invalidSchemas}\end{table}\begin{prob}%\ollabel{ex:in/validSchemas}  Prove that the schemas in the first column of  \olref[nml][syn][sch]{tab:valid-invalidSchemas} are valid and those in  the second column are not valid.\end{prob}\begin{prob}  Decide whether the following schemas are valid or invalid:  \begin{enumerate}  \item $(\Diamond !A \lif \Box !B) \lif (\Box !A \lif \Box    !B)$;  \item $\Diamond(!A \lif !B) \lor \Box(!B \lif !A)$.  \end{enumerate}\end{prob}\begin{prob}  For each of the following schemas find a model $\mModel{M}$ such  that every instance of the !!{formula} is true in $\mModel{M}$:  \begin{enumerate}  \item $p \lif \Diamond\Diamond p$;  \item $\Diamond p \lif \Box p$.  \end{enumerate}\end{prob}\end{document}

content/normal-modal-logic/syntax-and-semantics/entailment.tex

% Part: normal-modal-logic% Chapter: syntax-and-semantics% Section: entailment\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{syn}{ent}\olsection{Entailment}\begin{explain}  With the definition of truth at a world, we can define an entailment  relation between !!{formula}s. !!^a{formula}~$!B$ entails~$!A$ iff,  whenever $!B$ is true, $!A$ is true as well. Here, ``whenever''  means both ``whichever model we consider'' as well as ``whichever  world in that model we consider.''\end{explain}\begin{defn}  If $\Gamma$ is a set of !!{formula}s and $!A$ !!a{formula}, then  $\Gamma$ \emph{entails}~$!A$, in symbols: $\Gamma \Entails !A$, if  and only if for every model $\mModel{M} = \tuple{W, R, V}$ and world  $w \in W$, if $\mSat{M}{!B}[w]$ for every $!B \in \Gamma$, then  $\mSat{M}{!A}[w]$. If $\Gamma$ contains a single !!{formula}~$!B$,  then we write $!B \Entails !A$.\end{defn}\begin{ex}  To show that !!a{formula} entails another, we have to reason about  all models, using the definition of $\mSat{M}{}[w]$. For instance,  to show $p \lif \Diamond p \Entails \Box\lnot p \lif \lnot p$, we  might argue as follows: Consider a model $\mModel{M} = \tuple{W, R,    V}$ and $w \in W$, and suppose $\mSat{M}{p \lif \Diamond    p}[w]$. We have to show that $\mSat{M}{\Box\lnot p \lif \lnot    p}[w]$. Suppose not. Then $\mSat{M}{\Box\lnot p}[w]$ and  $\mSat/{M}{\lnot p}[w]$. Since $\mSat/{M}{\lnot p}[w]$, $\mSat{M}{    p}[w]$. By assumption, $\mSat{M}{p \lif \Diamond p}[w]$, hence  $\mSat{M}{\Diamond p}[w]$. By definition of $\mSat{M}{\Diamond    p}[w]$, there is some $w'$ with $Rww'$ such that  $\mSat{M}{p}[w']$. Since also $\mSat{M}{\Box \lnot p}[w]$,  $\mSat{M}{\lnot p}[w']$, a contradiction.  To show that !!a{formula}~$!B$ does not entail another~$!A$, we have  to give a counterexample, i.e., a model $\mModel{M} = \tuple{W, R,    V}$ where we show that at some world~$w \in W$, $\mSat{M}{!B}[w]$  but $\mSat/{M}{!A}[w]$. Let's show that $p \lif \Diamond p \Entails/  \Box p \lif p$. Consider the model in \olref{fig:counterex}.  We  have $\mSat{M}{\Diamond p}[w_1]$ and hence $\mSat{M}{p \lif    \Diamond p}[w_1]$. However, since $\mSat{M}{\Box p}[w_1]$ but  $\mSat/{M}{p}[w_1]$, we have $\mSat/{M}{\Box p \lif p}[w_1]$.  \begin{figure}  \begin{center}    \begin{tikzpicture}[modal]      \node[world] (w1) [label=right:\mFalse{p}]{$w_1$};       \node[world] (w2) [label=right:\mTrue{p}, above left=of w1]{$w_2$};       \node[world] (w3) [label=right:\mTrue{p}, above right=of w1] {$w_3$};      \draw[->] (w1) to (w2);      \draw[->] (w1) to (w3);    \end{tikzpicture}  \end{center}  \caption{Counterexample to $p \lif \Diamond p  \Entails \Box p \lif p$.}  \ollabel{fig:counterex}  \end{figure}    Often very simple counterexamples suffice. The model $\mModel{M'} =  \{W', R', V'\}$ with $W' = \{w\}$, $R' = \emptyset$, and $V'(p) =  \emptyset$ is also a counterexample: Since $\mSat/{M'}{p}[w]$,  $\mSat{M'}{p \lif \Diamond p}[w]$. As no worlds are accessible  from~$w$, we have $\mSat{M'}{\Box p}[w]$, and so $\mSat/{M'}{\Box p    \lif p}[w]$.\end{ex}\begin{prob}  Show that $\Box (!A \land !B) \Entails \Box !A$.\end{prob}\begin{prob}  Show that $\Box (p \lif q) \Entails/ p \lif \Box q$ and $p \lif \Box  q \Entails/\Box (p \lif q)$.\end{prob}\end{document}