Normal Modal Logics

Axiomatic Derivations

content/normal-modal-logic/axioms-systems/axioms-systems.tex

% Part: normal-modal-logic% Chapter: axioms-systems\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{nml}{prf}{Axiomatic \usetoken{P}{derivation}}\olimport{introduction}\olimport{normal-logics}\olimport{logics-proofs}\olimport{proofs-in-K}\olimport{derived-rules}\olimport{more-proofs-in-K}\olimport{duals}\olimport{proofs-modal-systems}\olimport{soundness}\olimport{systems-distinct}\olimport{provability-from-set}\olimport{provability-properties}\olimport{consistency}\OLEndChapterHook\end{document}

content/normal-modal-logic/axioms-systems/introduction.tex

% Part: normal-modal-logic% Chapter: axioms-systems% Section: introduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{axs}{int}\olsection{Introduction}We have a semantics for the basic modal language in terms of modalmodels, and a notion of !!a{formula} being valid---true at all worldsin all models---or valid with respect to some class of models orframes---true at all worlds in all models in the class, or based onthe frame. Logic usually connects such semantic characterizations ofvalidity with a proof-theoretic notion of !!{derivability}. The aim isto define a notion of !!{derivability} in some system such that!!a{formula} is !!{derivable} iff it is valid.The simplest and historically oldest !!{derivation} systems areso-called Hilbert-type or axiomatic !!{derivation} systems.Hilbert-type !!{derivation} systems for many modal logics arerelatively easy to construct: they are simple as objects ofmetatheoretical study (e.g., to prove soundness andcompleteness). However, they are much harder to use to prove!!{formula}s in than, say, natural deduction systems.In Hilbert-type !!{derivation} systems, !!a{derivation} of !!a{formula}is a sequence of !!{formula}s leading from certain axioms, via ahandful of inference rules, to the !!{formula} in question.  Since wewant the !!{derivation} system to match the semantics, we have toguarantee that the set of !!{derivable} formulas are true in allmodels (or true in all models in which all axioms are true). We'llfirst isolate some properties of modal logics that are necessary forthis to work: the ``normal'' modal logics. For normal modal logics,there are only two inference rules that need to be assumed: modusponens and necessitation.  As axioms we take all (substitutioninstances) of tautologies, and, depending on the modal logic we dealwith, a number of modal axioms. Even if we are just interested in theclass of all models, we must also count all substitution instancesof~$\Ax{K}$\iftag{notprvDiamond}{}{ and~$\Ax{Dual}$} as axioms. Thisalone generates the minimal normal modal logic~$\Log K$.\begin{defn}The rule of \emph{modus ponens} is the inference schema\begin{prooftree}\AxiomC{$!A$}\AxiomC{$!A \lif !B$}\RightLabel{\MP}\BinaryInfC{$!B$}\end{prooftree}We say !!a{formula}~$!B$ \emph{follows from}~!!{formula}s $!A$, $!C$by modus ponens iff $!C \ident !A \lif !B$.\end{defn}\begin{defn}The rule of \emph{necessitation} is the inference schema\begin{prooftree}\AxiomC{$!A$}\RightLabel{\Nec}\UnaryInfC{$\Box !A$}\end{prooftree}We say the !!{formula}~$!B$ follows from the !!{formula}s $!A$ bynecessitation iff $!B \ident \Box !A$.\end{defn}\begin{defn}A \emph{!!{derivation}} from a set of axioms~$\Sigma$ is a sequence of!!{formula}s $!B_1$, $!B_2$, \dots, $!B_n$, where each $!B_i$ iseither\begin{enumerate}\item a substitution instance of a tautology, or\item a substitution instance of !!a{formula} in~$\Sigma$, or\item follows from two !!{formula}s $!B_j$, $!B_k$ with $j$, $k < i$  by modus ponens, or\item follows from !!a{formula}~$!B_j$ with $j < i$ by necessitation.\end{enumerate}If there is such !!a{derivation} with $!B_n \ident !A$, we say that$!A$ is \emph{!!{derivable} from $\Sigma$}, in symbols $\Sigma \Proves !A$.\end{defn}With this definition, it will turn out that the set of !!{derivable}formulas forms a normal modal logic, and that any !!{derivable}!!{formula} is true in every model in which every axiom is true. Thisproperty of !!{derivation}s is called \emph{soundness}. The converse,\emph{completeness}, is harder to prove.\end{document}

content/normal-modal-logic/axioms-systems/normal-logics.tex

% Part: normal-modal-logic% Chapter: axioms-systems% Section: normal-logics\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{prf}{nor}\olsection{Normal Modal Logics}Not every set of modal !!{formula}s can easily be characterized asthose !!{formula}s derivable from a set of axioms. We want modallogics to be well-behaved. First of all, everything we can !!{derive}in classical propositional logic should still be !!{derivable}, ofcourse taking into account that the !!{formula}s may now contain also\iftag{prvBox}{$\Box$\iftag{prvDiamond}{    and~}{}}{}\iftag{prvDiamond}{$\Diamond$}{}. To this end, werequire that a modal logic contain all tautological instances and beclosed under modus ponens.\begin{defn}  A \emph{modal logic} is a set~$\Sigma$ of modal !!{formula}s which  \begin{enumerate}  \item contains all tautologies, and  \item is closed under substitution, i.e., if $!A \in \Sigma$, and    $!D_1$, \dots, $!D_n$ are !!{formula}s, then    \[    \SSubst{!A}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}} \in \Sigma,    \]    \item is closed under \emph{modus ponens}, i.e., if $!A$ and $!A      \lif !B \in \Sigma$, then $!B \in \Sigma$.  \end{enumerate}\end{defn}In order to use the relational semantics for modal logics, we alsohave to require that all !!{formula}s valid in all modal models areincluded. It turns out that this requirement is met as soon as allinstances of \Ax{K}\iftag{prvDiamond}{ and~\Dual{}}{} are!!{derivable}, and whenever !!a{formula}~$!A$ is !!{derivable}, sois~$\Box !A$. A modal logic that satisfies these conditions is called\emph{normal}. (Of course, there are also non-normal modal logics, butthe usual relational models are not adequate for them.)\begin{defn}  A modal logic $\Sigma$ is \emph{normal} if it contains  \begin{align*}    \tag{\Ax{K}} & \Box(p \lif q) \lif (\Box p \lif \Box q),    \iftag{prvDiamond}{\\      \tag{\Dual} & \Diamond p \liff \lnot\Box\lnot p}{}  \end{align*}  and is closed under \emph{necessitation}, i.e., if $!A \in  \Sigma$, then $\Box !A \in \Sigma$.\end{defn}Observe that while tautological implication is ``fine-grained'' enoughto preserve \emph{truth at a world}, the rule \Nec{} only preserves\emph{truth in a model} (and hence also validity in a frame or in aclass of frames).\begin{prop}\ollabel{prop:rk}  Every normal modal logic is closed under rule \RK,  \begin{prooftree}    \AxiomC{$!A_1 \lif (!A_2 \lif \cdots (!A_{n-1} \lif !A_n)\cdots)$}    \RightLabel{\RK}    \UnaryInfC{$\Box!A_1 \lif (\Box!A_2 \lif \cdots (\Box!A_{n-1}      \lif \Box!A_n)\cdots).$}  \end{prooftree}\end{prop}\begin{proof}  By induction on~$n$: If $n = 1$, then the rule is just \Nec, and  every normal modal logic is closed under \Nec.  Now suppose the result holds for $n-1$; we show it holds for~$n$.  Assume  \begin{align*}  & !A_1 \lif (!A_2 \lif \cdots (!A_{n-1} \lif !A_n)\cdots) \in \Sigma  \intertext{By the induction hypothesis, we have}  & \Box!A_1 \lif (\Box!A_2 \lif \cdots \Box(!A_{n-1} \lif !A_n)\cdots)  \in \Sigma  \intertext{Since $\Sigma$ is a normal modal logic, it contains all    instances of~$\Ax{K}$, in particular}  & \Box(!A_{n-1} \lif !A_n) \lif (\Box!A_{n-1} \lif \Box!A_n) \in \Sigma  \intertext{Using modus ponens and suitable tautological instances we get}  & \Box!A_1 \lif (\Box!A_2 \lif \cdots (\Box!A_{n-1}  \lif \Box!A_n)\cdots) \in \Sigma.   \end{align*}\end{proof}\begin{prop}\ollabel{prop:notDiamondBot}  Every normal modal logic $\Sigma$ contains~$\lnot\Diamond\lfalse$.\end{prop}\begin{prob}  Prove \olref[nml][prf][nor]{prop:notDiamondBot}.\end{prob}\begin{prop}  Let $!A_1$, \dots, $!A_n$ be !!{formula}s. Then there is a  smallest modal logic $\Sigma$ containing all instances of  $!A_1$, \dots, $!A_n$.\end{prop}\begin{proof}  Given $!A_1$, \dots, $!A_n$, define $\Sigma$ as the  intersection of all normal modal logics containing all instances of  $!A_1$, \dots, $!A_n$. The intersection is non-empty as  $\Frm[L]$, the set of all !!{formula}s, is such a modal  logic.\end{proof}\begin{defn}The smallest normal modal logic containing $!A_1$, \dots, $!A_n$ iscalled a \emph{modal system} and denoted by $\Log{K} !A_1 \dots!A_n$. The smallest normal modal logic is denoted by~\Log{K}.\end{defn}\end{document}

content/normal-modal-logic/axioms-systems/logics-proofs.tex

% Part: normal-modal-logic% Chapter: axioms-systems% Section: logics-proofs\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{prf}{prf}\olsection{\usetoken{P}{derivation} and Modal Systems}We first define what !!a{derivation} is for normal modallogics. Roughly, !!a{derivation} is a sequence of !!{formula}s inwhich every !!{element} is either (a substitution instance of) one ofa number of \emph{axioms}, or follows from previous !!{element}s byone of a few inference rules. For normal modal logics, all instancesof tautologies\iftag{prvDiamond}{, \Ax{K}, and~\Dual{}}{ and~\Ax{K}}count as axioms. This results in the modal system~$\Log{K}$, thesmallest normal modal logic. We may wish to add additional axioms toobtain other systems, however. The rules are always modus ponens~\MP{}and necessitation~\Nec.\begin{defn}  Given a modal system $\Log{K} !A_1 \dots !A_n$ and !!a{formula}~$!B$  we say that $!B$ is \emph{!!{derivable}} in $\Log{K} !A_1 \dots  !A_n$, written $\Log{K} !A_1 \dots !A_n \Proves !B$, if and only if  there are !!{formula}s $!C_1$, \dots, $!C_k$ such that $!C_k = !B$  and each $!C_i$ is either a tautological instance, or an instance of  one of $\Ax{K}$,\iftag{prvDiamond}{ $\Dual$,}{} $!A_1$,  \dots, $!A_n$, or it follows from previous !!{formula}s by means of  the rules \MP{} or~\Nec.\end{defn}The following proposition allows us to show that $!B \in \Sigma$by exhibiting a $\Sigma$-!!{derivation} of~$!B$.\begin{prop}  $\Log{K} !A_1 \dots !A_n = \Setabs{!B}{\Log{K} !A_1 \dots !A_n \Proves !B}$.\end{prop}\begin{proof}  We use induction on the length of !!{derivation}s to show that  $\Setabs{!B}{\Log{K} !A_1 \dots !A_n \Proves !B} \subseteq  \Log{K} !A_1 \dots !A_n$.  If the !!{derivation} of~$!B$ has length~$1$, it contains a single  !!{formula}. That !!{formula} cannot follow from previous formulas  by \MP{} or \Nec, so must be a tautological instance, an instance of  \Ax{K},\iftag{prvDiamond}{ $\Dual$,}{} or an instance  of one of $!A_1$, \dots,~$!A_n$. But $\Log{K}!A_1\dots!A_n$ contains  these as well, so $!B \in \Log{K}!A_1 \dots !A_n$.  If the !!{derivation} of $!B$ has length~$> 1$, then $!B$ may in  addition be obtained by \MP{} or \Nec{} from !!{formula}s not  occurring as the last line in the !!{derivation}. If $!B$ follows  from $!C$ and $!C \lif !B$ (by \MP), then $!C$ and $!C \lif !B \in  \Log{K}!A_1 \dots !A_n$ by induction hypothesis. But every modal  logic is closed under modus ponens, so $!B \in \Log{K}!A_1 \dots  !A_n$. If $!B \equiv \Box !C$ follows from $!C$ by \Nec, then $!C  \in \Log{K}!A_1 \dots !A_n$ by induction hypothesis. But every  normal modal logic is closed under $\Nec$, so $!B \in  \Log{K}!A_1\dots!A_n$.  The converse inclusion follows by showing that  $\Sigma = \Setabs{!B}{\Log{K} !A_1 \dots !A_n \Proves !B }$ is a normal  modal logic containing all the instances of $!A_1$,  \dots, $!A_n$, and the observation that $\Log{K} !A_1 \dots !A_n$  is, by definition, the smallest such logic.  \begin{enumerate}    \item Every tautology~$!B$ is a tautological instance, so      $\Log{K}!A_1\dots!A_n \Proves !B$, so $\Sigma$ contains all      tautologies.    \item If $\Log{K}!A_1\dots!A_n \Proves !C$ and      $\Log{K}!A_1\dots!A_n \Proves !C \lif !B$, then      $\Log{K}!A_1\dots!A_n \Proves !B$: Combine the !!{derivation} of      $!C$ with that of $!C \lif !B$, and add the line~$!B$. The last      line is justified by \MP{}. So $\Sigma$ is closed under modus      ponens.    \item If $!B$ has !!a{derivation}, then every substitution      instance of~$!B$ also has !!a{derivation}: apply the substitution      to every !!{formula} in the !!{derivation}. (Exercise: prove by      induction on the length of !!{derivation}s that the result is      also a correct !!{derivation}). So $\Sigma$ is closed under      uniform substitution. (We have now established that $\Sigma$      satisfies all conditions of a modal logic.)    \item We have $\Log{K}!A_1\dots!A_n \Proves \Ax{K}$, so $K \in \Sigma$.    \tagitem{prvDiamond}{We have      $\Log{K}!A_1\dots!A_n \Proves \Dual$, so $\Dual \in \Sigma$.}{}    \item If $\Log{K}!A_1\dots!A_n \Proves !C$, the additional      line~$\Box !C$ is justified by~\Nec. Consequently, $\Sigma$ is      closed under~\Nec. Thus, $\Sigma$ is normal.  \end{enumerate}\end{proof}\end{document}

content/normal-modal-logic/axioms-systems/proofs-in-K.tex

% Part: normal-modal-logic% Chapter: axioms-systems% Section: proofs-in-K\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{prf}{prk}\olsection{Proofs in \Log{K}}In order to practice proofs in the smallest modal system, we show thevalid !!{formula}s on the left-hand side of\olref[syn][sch]{tab:valid-invalidSchemas} can all be given\Log{K}-proofs.\begin{prop}  $\Log{K} \Proves \Box!A \lif \Box (!B\lif !A)$\end{prop}\begin{proof}  \begin{derivation}    1. & $!A \lif (!B \lif !A)$ & \Taut \\    2. & $\Box(!A \lif (!B \lif !A))$ & \Nec, 1 \\    3. & $\Box(!A \lif (!B \lif !A)) \lif    (\Box!A \lif \Box(!B \lif !A))$ & \Ax{K}\\    4. & $\Box!A \lif \Box (!B\lif !A)$ & \MP, 2, 3  \end{derivation}\end{proof}\begin{prop}  $\Log{K} \Proves \Box(!A \land !B) \lif (\Box !A \land \Box!B)$\end{prop}\begin{proof}\begin{derivation}  1. & $(!A \land !B) \lif !A$ & \Taut \\  2. & $\Box((!A \land !B) \lif !A)$ & \Nec \\  3. & $\Box((!A \land !B) \lif !A) \lif (\Box(!A \land !B) \lif \Box!A)$  & \Ax{K} \\  4. & $\Box(!A \land !B) \lif \Box!A$ & \MP, 2, 3 \\  5. & $(!A \land !B) \lif !B$ & \Taut \\  6. & $\Box((!A \land !B) \lif !B)$ & \Nec \\  7. & $\Box((!A \land !B) \lif !B) \lif (\Box(!A \land !B) \lif \Box!B)$  & \Ax{K} \\  8. & $\Box(!A \land !B) \lif \Box!B$ & \MP, 6, 7 \\  9. & $(\Box(!A \land !B) \lif \Box!A) \lif{}$ \\  & \qquad $((\Box(!A \land !B) \lif \Box!B) \lif{}$ \\  & \qquad $(\Box(!A \land !B) \lif (\Box !A \land \Box!B)))$ & \Taut\\  10. &  $(\Box(!A \land !B) \lif \Box!B) \lif{}$ \\  & \qquad $(\Box(!A \land !B) \lif (\Box !A \land \Box!B))$ & \MP, 4, 9\\  11. & $\Box(!A \land !B) \lif (\Box !A \land \Box!B)$ & \MP, 8, 10.\end{derivation}Note that the !!{formula} on line~$9$ is an instance of the tautology\[(p \lif q) \lif ((p \lif r) \lif (p \lif (q \land r))).\]\end{proof}\begin{prop}  $\Log{K}\Proves (\Box!A \land \Box!B) \lif \Box (!A \land !B)$\end{prop}\begin{proof}  \begin{derivation}    1. & $!A \lif (!B \lif (!A \land !B))$ & \Taut \\    2. & $\Box(!A \lif (!B \lif (!A \land !B)))$ & \Nec, 1 \\    3. & $\Box(!A \lif (!B \lif (!A \land !B))) \lif (\Box!A \lif \Box(!B \lif (!A \land !B)))$ & \Ax{K}\\    4. & $\Box!A \lif \Box(!B \lif (!A \land !B))$ & \MP, 2, 3\\    5. & $\Box(!B \lif (!A \land !B)) \lif (\Box!B \lif \Box(!A \land !B))$ & \Ax{K} \\    6. & $(\Box!A \lif \Box(!B \lif (!A \land !B))) \lif {}$ \\    & \qquad $(\Box(!B \lif (!A \land !B)) \lif (\Box!B \lif \Box(!A \land !B))) \lif {}$\\    & \qquad $(\Box!A \lif (\Box !B \lif \Box(!A \land !B))))$ & \Taut\\    7. & $(\Box(!B \lif (!A \land !B)) \lif (\Box!B \lif \Box(!A \land !B))) \lif {}$\\    & \qquad $(\Box!A \lif (\Box !B \lif \Box(!A \land !B)))$ & \MP, 4, 6\\    8. & $\Box!A \lif (\Box !B \lif \Box(!A \land !B)))$ & \MP, 5, 7\\    9. & $(\Box!A \lif (\Box !B \lif \Box(!A \land !B)))) \lif {}$\\    & \qquad $((\Box!A \land \Box!B) \lif \Box(!A \land !B))$ & \Taut\\    10. & $(\Box!A \land \Box!B) \lif \Box(!A \land !B)$ & \MP, 8, 9  \end{derivation}  The !!{formula}s on lines $6$ and $9$ are instances of the tautologies  \begin{align*}    (p \lif q) & \lif ((q \lif r) \lif (p \lif r)) \\    (p \lif (q \lif r)) & \lif ((p \land q) \lif r)  \end{align*}\end{proof}\begin{prop}  \iftag{prvBox}{$\Log{K} \Proves \lnot\Box p \lif \Diamond \lnot    p$}{$\Log{K} \Proves \Box\lnot p \lif \lnot\Diamond p$}\end{prop}\begin{proof}  \iftag{prvBox}{\iftag{prvDiamond}{% Box and Diamond are primitive  \begin{derivation}    1. & $\Diamond \lnot p \liff \lnot\Box\lnot\lnot p$ & \Dual\\    2. & $(\Diamond \lnot p \liff \lnot\Box\lnot\lnot p) \lif {}$ \\    & \qquad $(\lnot \Box \lnot\lnot p \lif \Diamond \lnot p)$& \Taut\\    3. & $\lnot \Box \lnot\lnot p \lif \Diamond \lnot p$ & \MP, 1, 2\\    4. & $\lnot\lnot p \lif p$ & \Taut\\    5. & $\Box(\lnot\lnot p \lif p)$ & \Nec, 4\\    6. & $\Box(\lnot\lnot p \lif p) \lif (\Box \lnot\lnot p \lif \Box p)$ & \Ax{K}\\    7. & $(\Box \lnot\lnot p \lif \Box p)$ & \MP, 5, 6\\    8. & $(\Box \lnot\lnot p \lif \Box p) \lif (\lnot \Box p \lif \lnot\Box\lnot\lnot p)$ & \Taut\\    9. & $\lnot \Box p \lif \lnot\Box\lnot\lnot p$ & \MP, 7, 8\\    10. & $(\lnot \Box p \lif \lnot\Box\lnot\lnot p) \lif {}$ \\    & \qquad $((\lnot \Box \lnot\lnot p \lif \Diamond \lnot p) \lif (\lnot \Box p \lif \Diamond\lnot p))$ & \Taut\\    11. & $(\lnot \Box \lnot\lnot p \lif \Diamond \lnot p) \lif (\lnot \Box p \lif \Diamond\lnot p)$ & \MP, 9, 10\\    12. & $\lnot\Box p \lif \Diamond \lnot p$ & \MP, 3, 11\\  \end{derivation}  The !!{formula}s on lines $8$ and $10$ are instances of the tautologies  \begin{align*}    & (p \lif q) \lif (\lnot q \lif \lnot p) \\    & (p \lif q) \lif ((q \lif r) \lif (p \lif r)).  \end{align*}  }{% Diamond is defined  \begin{derivation}    1. & $\lnot\lnot p \lif p$ & \Taut\\    2. & $\Box(\lnot\lnot p \lif p)$ & \Nec, 1\\    3. & $\Box(\lnot\lnot p \lif p) \lif (\Box \lnot\lnot p \lif \Box p)$ & \Ax{K}\\    4. & $(\Box \lnot\lnot p \lif \Box p)$ & \MP, 2, 3\\    5. & $(\Box \lnot\lnot p \lif \Box p) \lif (\lnot \Box p \lif \lnot\Box\lnot\lnot p)$ & \Taut\\    6. & $\lnot \Box p \lif \lnot\Box\lnot\lnot p$ & \MP, 4, 5\\    & $\lnot\Box p \lif \Diamond \lnot p$  \end{derivation}  The last line is $\lnot \Box p \lif \Diamond\lnot p$, since  $\Diamond$ is defined as $\lnot\Box\lnot$.  The !!{formula} on  line~$5$ is an instance of the tautology  \[    (p \lif q) \lif (\lnot q \lif \lnot p).  \]  }}{% Box is defined  \begin{derivation}    1. & $\Diamond  p \liff \lnot\Box\lnot p$ & \Dual\\    2. & $(\Diamond p \liff \lnot\Box\lnot p) \lif    (\Diamond p \lif \lnot \Box \lnot p)$& \Taut\\    3. & $\Diamond p \lif \lnot \Box \lnot p$ & \MP, 1, 2\\    4. & $(\Diamond p \lif \lnot \Box \lnot p) \lif (\Box\lnot p \lif \lnot\Diamond p)$ & \Taut\\    5. & $\Box\lnot p \lif \lnot\Diamond p$ & \MP, 3, 4  \end{derivation}  The !!{formula} on  line~$4$ is an instance of the tautology  \begin{align*}    & (p \lif \lnot q) \lif (q \lif \lnot p).  \end{align*}}\end{proof}\begin{prob}  Find !!{derivation}s in~$\Log{K}$ for the following !!{formula}s:  \begin{enumerate}    \item $\Box \lnot p \lif \Box(p \lif q)$    \item $(\Box p \lor \Box q) \lif \Box(p \lor q)$    \item $\Diamond p \lif \Diamond(p \lor q)$  \end{enumerate}\end{prob}\end{document}

content/normal-modal-logic/axioms-systems/derived-rules.tex

% Part: normal-modal-logic% Chapter: axioms-systems% Section: derived-rules\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{prf}{der}\olsection{Derived Rules}Finding and writing !!{derivation}s is obviously difficult,cumbersome, and repetitive. For instance, very often we want to passfrom $!A \lif !B$ to $\Box !A \lif \Box !B$, i.e., applyrule~\RK. That requires an application of \Nec, then recording theproper instance of~\Ax{K}, then applying~\MP. Passing from $!A \lif!B$ and $!B \lif !C$ to $!A \lif !C$ requires recording the (long)tautological instance\[(!A \lif !B) \lif ((!B \lif !C) \lif (!A \lif !C))\]and applying \MP{} twice. Often we want to replace a sub-!!{formula}by a formula we know to be equivalent, e.g., \iftag{prvDiamond}{$\Diamond  !A$ by $\lnot\Box\lnot !A$}{$\Box !A$ by $\lnot\Diamond\lnot !A$}, or$\lnot\lnot !A$ by $!A$. So rather than write out the actual!!{derivation}, it is more convenient to simply record why theintermediate steps are !!{derivable}. For this purpose, let us collectsome facts about !!{derivability}.\begin{prop}  If $\Log{K} \Proves !A_1$, \dots, $\Log{K} \Proves !A_n$, and $!B$  follows from $!A_1$, \dots, $!A_n$ by propositional logic, then  $\Log{K} \Proves !B$.\end{prop}\begin{proof}  If $!B$ follows from $!A_1$, \dots,~$!A_n$ by propositional logic, then  \[  !A_1 \lif (!A_2 \lif \cdots (!A_n \lif !B)\dots)  \]  is a tautological instance. Applying \MP{} $n$ times gives a  !!{derivation} of~$!B$.\end{proof}We will indicate use of this proposition by~\PL.\begin{prop}  If $\Log{K} \Proves !A_1 \lif (!A_2 \lif \cdots (!A_{n-1} \lif  !A_n)\dots)$ then $\Log{K} \Proves \Box !A_1 \lif (\Box !A_2 \lif  \cdots (\Box !A_{n-1} \lif \Box !A_n)\dots)$.\end{prop}\begin{proof}  By induction on $n$, just as in the proof of \olref[nor]{prop:rk}.\end{proof}We will indicate use of this proposition by~\RK. Let's illustrate howthese results help establishing !!{derivability} results more easily.\begin{prop}  $\Log{K} \Proves (\Box!A \land \Box!B) \lif \Box (!A \land !B)$\end{prop}\begin{proof}  \begin{derivation}    1. & $\Log{K} \Proves !A \lif (!B \lif (!A \land !B))$ & \Taut \\    2. & $\Log{K} \Proves \Box!A \lif (\Box !B \lif \Box(!A \land !B)))$ & \RK, 1\\    3. & $\Log{K} \Proves (\Box!A \land \Box!B) \lif \Box(!A \land !B)$ & \PL, 2  \end{derivation}\end{proof}\begin{prop}\ollabel{prop:rewriting}  If $\Log{K} \Proves !A \liff !B$ and $\Log{K} \Proves  \Subst{!C}{!A}{q}$ then $\Log{K} \Proves \Subst{!C}{B}{q}$\end{prop}\begin{proof}  Exercise.\end{proof}\begin{prob}  Prove \olref[nml][prf][der]{prop:rewriting} by proving, by induction  on the complexity of~$!C$, that if $\Log{K} \Proves !A \liff !B$  then $\Log{K} \Proves \Subst{!C}{!A}{q} \liff \Subst{!C}{!B}{q}$.\end{prob}This proposition comes in handy especially when we want to convert$\Diamond$ into $\Box$ (or vice versa), or remove double negationsinside !!a{formula}.  In what follows, we will mark applications of\olref{prop:rewriting} by ``$!A$ for $!B$'' whenever we re-write!!a{formula}~$!C(!B)$ for~$!C(!A)$. In other words, ``$!A$ for $!B$''abbreviates:  \begin{derivation}    & $\Proves !C(!A)$ \\    & $\Proves !A \liff !B$\\    & $\Proves !C(!B)$ & by \olref{prop:rewriting}  \end{derivation}For instance:\begin{prop}  $\Log{K} \Proves \lnot\Box p \lif \Diamond \lnot p$\end{prop}\begin{proof}  \iftag{prvDiamond}{% Diamond is primitive  \begin{derivation}    1. & $\Log{K} \Proves \Diamond \lnot p \liff \lnot\Box\lnot\lnot p$ &    \Dual\\    2. & $\Log{K} \Proves \lnot \Box \lnot\lnot p \lif \Diamond \lnot p$ & \PL, 1\\    3. & $\Log{K} \Proves \lnot\Box p \lif \Diamond \lnot p$ & $p$ for $\lnot\lnot p$\\  \end{derivation}  }{% Diamond is defined  \begin{derivation}    1. & $\Log{K} \Proves \lnot \Box \lnot\lnot p \lif \Diamond \lnot p$ & \Taut\\    2. & $\Log{K} \Proves \lnot\Box p \lif \Diamond \lnot p$ & $p$ for $\lnot\lnot p$\\  \end{derivation}  The formula on line~$1$ is an instance of $\lnot q \lif \lnot q$,  substituting $\Box\lnot\lnot p$ for~$q$. $\Diamond\lnot p$ and  $\lnot\Box\lnot\lnot p$ are identical, since $\Diamond$ is defined  as~$\lnot\Box\lnot$.}\end{proof}In the above !!{derivation}, the final step ``$p$ for $\lnot\lnot p$''is short for  \begin{derivation}    & $\Log{K} \Proves \lnot \Box \lnot\lnot p \lif \Diamond \lnot    p$\\    & $\Log{K} \Proves \lnot\lnot p \liff p$ & \Taut\\    & $\Log{K} \Proves \lnot\Box p \lif \Diamond \lnot p$ & by \olref{prop:rewriting}  \end{derivation}The roles of $!C(q)$, $!A$, and $!B$ in \olref{prop:rewriting} areplayed here, respectively, by $\lnot \Box q \lif \Diamond \lnot p$,$\lnot\lnot p$, and~$p$.When !!a{formula} contains a sub-!!{formula} $\lnot\Diamond !A$,we can replace it by $\Box\lnot !A$ using \olref{prop:rewriting}, since$\Log{K} \Proves \lnot\Diamond !A \liff \Box\lnot !A$. We'll indicatethis and similar replacements simply by ``$\Box\lnot$ for$\lnot\Diamond$.''The following proposition justifies that we can establish!!{derivability} results schematically. E.g., the previous propositiondoes not just establish that $\Log{K} \Proves \lnot\Box p \lif\Diamond \lnot p$, but $\Log{K} \Proves \lnot\Box !A \lif \Diamond\lnot !A$ for arbitrary~$!A$.\begin{prop}  If $!A$ is a substitution instance of $!B$ and $\Log{K} \Proves !B$,  then $\Log{K} \Proves !A$.\end{prop}\begin{proof}  It is tedious but routine to verify (by induction on the length of  the !!{derivation} of~$!B$) that applying a substitution to an  entire !!{derivation} also results in a correct  !!{derivation}. Specifically, substitution instances of tautological  instances are themselves tautological instances, substitution  instances of instances of~\iftag{prvDiamond}{\Dual{} and~}{}\Ax{K}  are themselves instances of~\iftag{prvDiamond}{\Dual{}    and~}{}\Ax{K}, and applications of \MP{} and~\Nec{} remain correct  when substituting !!{formula}s for !!{propositional variable}s in  both premise(s) and conclusion.\end{proof}\end{document}

content/normal-modal-logic/axioms-systems/more-proofs-in-K.tex

% Part: normal-modal-logic% Chapter: axioms-systems% Section: more-proofs-in-K\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{prf}{mpr}\olsection{More Proofs in \Log{K}}Let's see some more examples of !!{derivability} in~\Log{K}, now usingthe simplified method introduced in \olref[der]{sec}.\begin{prop}  $\Log{K} \Proves \Box (!A \lif !B) \lif (\Diamond !A \lif \Diamond  !B)$\end{prop}\begin{proof}\begin{derivation}1. & $\Log{K} \Proves (!A \lif !B) \lif (\lnot !B \lif \lnot !A)$ & \PL \\2. &  $\Log{K} \Proves \Box(!A \lif !B) \lif (\Box\lnot!B \lif \Box\lnot!A)$ & \RK, 1 \\3. & $\Log{K} \Proves (\Box\lnot!B \lif \Box\lnot!A) \lif (\lnot\Box\lnot!A \lif \lnot\Box\lnot!B)$ & \Taut\\4. & $\Log{K} \Proves \Box(!A \lif !B) \lif (\lnot\Box\lnot!A \lif \lnot\Box\lnot!B)$ & \PL, 2, 3 \\5. &  $\Log{K} \Proves \Box(!A \lif !B) \lif (\Diamond!A \lif \Diamond!B)$ & $\Diamond$ for $\lnot\Box\lnot$.\end{derivation}\end{proof}  \begin{prop}$\Log{K}\Proves \Box!A \lif (\Diamond(!A \lif !B) \lif  \Diamond !B)$\end{prop}\begin{proof}  \begin{derivation}  1. & $\Log{K} \Proves !A \lif (\lnot!B \lif \lnot (!A \lif !B))$ & \Taut \\  2. & $\Log{K} \Proves \Box!A \lif  (\Box\lnot!B \lif \Box\lnot (!A\lif !B))$ &  \RK, 1 \\  3. &  $\Log{K} \Proves \Box!A \lif (\lnot \Box\lnot (!A\lif !B) \lif \lnot  \Box\lnot!B)$ & \PL, 2 \\  4. & $\Log{K} \Proves \Box!A \lif (\Diamond(!A \lif !B) \lif  \Diamond !B)$ & $\Diamond$ for $\lnot\Box\lnot$.  \end{derivation}\end{proof}\begin{prop}  $\Log{K} \Proves (\Diamond!A \lor \Diamond!B) \lif \Diamond(!A \lor !B)$\end{prop}\begin{proof}  \begin{derivation}    1. & $\Log{K} \Proves \lnot(!A \lor !B) \lif \lnot!A$ & \Taut \\    2. & $\Log{K} \Proves \Box\lnot(!A \lor !B) \lif \Box\lnot!A$ & \RK, 1 \\    3. & $\Log{K} \Proves \lnot\Box\lnot !A \lif \lnot\Box\lnot(!A \lor!B)$ &    \PL, 2\\    4. & $\Log{K} \Proves \Diamond!A \lif \Diamond(!A \lor !B)$ &    $\Diamond$ for $\lnot\Box\lnot$\\    5. & $\Log{K} \Proves \Diamond!B \lif \Diamond(!A \lor !B)$ & similarly\\    6. & $\Log{K} \Proves (\Diamond!A \lor\Diamond!B) \lif \Diamond(!A \lor !B)$    & \PL, 4, 5.  \end{derivation}\end{proof}\begin{prop}  $\Log{K} \Proves \Diamond(!A \lor!B) \lif (\Diamond!A \lor \Diamond!B)$\end{prop}\begin{proof}  \begin{derivation}    1. & $\Log{K} \Proves \lnot !A \lif (\lnot !B \lif \lnot (!A \lor !B))$ & \Taut \\    2. & $\Log{K} \Proves \Box\lnot !A \lif    (\Box\lnot!B \lif \Box \lnot (!A \lor !B))$ & \RK\\    3. & $\Log{K} \Proves \Box\lnot !A \lif (\lnot \Box \lnot (!A \lor!B)    \lif \lnot\Box\lnot !B)$ & \PL, 2\\    4. & $\Log{K} \Proves \lnot \Box \lnot(!A \lor !B) \lif (\Box \lnot !A \lif     \lnot\Box\lnot !B)$ & \PL, 3\\    5. & $\Log{K} \Proves \lnot \Box \lnot(!A\lor!B) \lif (\lnot    \lnot\Box\lnot!B \lif \lnot\Box\lnot!A)$ & \PL, 4\\    6. & $\Log{K} \Proves \Diamond(!A \lor !B) \lif (\lnot    \Diamond!B \lif \Diamond!A)$ & $\Diamond$ for $\lnot\Box\lnot$\\    7. & $\Log{K} \Proves \Diamond(!A\lor!B) \lif (\Diamond!B \lor \Diamond!A)$ & \PL, 6. \\  \end{derivation}\end{proof}\begin{prob}  Show that the following !!{derivability} claims hold:  \begin{enumerate}  \item $\Log{K} \Proves \Diamond \lnot \lfalse \lif (\Box !A \lif    \Diamond !A)$;  \item $\Log{K} \Proves \Box(!A \lor !B) \lif (\Diamond !A \lor \Box    !B)$;  \item $\Log{K} \Proves (\Diamond !A \lif \Box !B) \lif \Box(!A \lif    !B)$.  \end{enumerate}\end{prob}\end{document}

content/normal-modal-logic/axioms-systems/duals.tex

% Part: normal-modal-logic% Chapter: axioms-systems% Section: duals\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{prf}{dua}\olsection{Dual \usetoken{P}{formula}}\begin{defn}\ollabel{def:duals}  Each of the !!{formula}s \Ax{T}, \Ax{B}, \Ax{4}, and  \Ax{5} has a \emph{dual}, denoted by a subscripted diamond, as  follows:  \begin{align}    \tag{\Ax{T_\Diamond}} p & \lif \Diamond p\\    \tag{\Ax{B_\Diamond}} \Diamond\Box p & \lif p\\    \tag{\Ax{4_\Diamond}} \Diamond\Diamond p & \lif \Diamond p\\    \tag{\Ax{5_\Diamond}} \Diamond\Box p & \lif \Box p    \end{align}\end{defn}Each of the above dual !!{formula}s is obtained from the corresponding!!{formula} by substituting $\lnot p$ for $p$, contraposing, replacing$\lnot\Box\lnot$ by $\Diamond$, and replacing $\lnot\Diamond\lnot$by~$\Box$. \Ax{D}, i.e., $\Box!A \lif \Diamond!A$ is its own dual inthat sense.\begin{prop}\ollabel{prop:dualsys}  For each !!{formula}~$!A$ in \olref[nml][prf][dua]{def:duals}:  $\Log{K}!A = \Log{K}!A_{\Diamond}$.\end{prop}\begin{proof}  Exercise.\end{proof}\begin{prob}  Prove \olref[nml][prf][dua]{prop:dualsys}.\end{prob}\end{document}

content/normal-modal-logic/axioms-systems/proofs-modal-systems.tex

% Part: normal-modal-logic% Chapter: axioms-systems% Section: proofs-modal-systems\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{prf}{prs}\olsection{Proofs in Modal Systems}We now come to proofs in systems of modal logic other than~\Log{K}.\begin{prop}\ollabel{prop:S5facts}The following provability results obtain:  \begin{enumerate}  \item $\Log{KT5} \Proves \Ax{B}$;  \item $\Log{KT5} \Proves \Ax{4}$;  \item $\Log{KDB4} \Proves \Ax{T}$;  \item $\Log{KB4} \Proves \Ax{5}$;  \item $\Log{KB5} \Proves \Ax{4}$;  \item \ollabel{prop:S5facts-KT-D}$\Log{KT} \Proves \Ax{D}$.  \end{enumerate}\end{prop}\begin{proof}  We exhibit proofs for each.  \begin{enumerate}    \item $\Log{KT5} \Proves \Ax{B}$:      \begin{derivation}        1. & $\Log{KT5} \Proves \Diamond!A \lif \Box\Diamond!A$ & \Ax{5}\\        2. & $\Log{KT5} \Proves !A \lif \Diamond!A$ & $\Ax{T_\Diamond}$\\        3. & $\Log{KT5} \Proves !A \lif \Box\Diamond!A$ & \PL, 2, 1.      \end{derivation}    \item $\Log{KT5} \Proves \Ax{4}$:      \begin{derivation}        1. &$\Log{KT5} \Proves \Diamond\Box!A \lif \Box\Diamond\Box!A$ & \Ax{5}        with $\Box!A$ for $p$\\        2. & $\Log{KT5} \Proves \Box!A \lif \Diamond\Box!A$ & $\Ax{T_\Diamond}$        with $\Box!A$ for $p$\\        3. & $\Log{KT5} \Proves \Box!A \lif \Box\Diamond\Box!A$ & \PL, 2, 1\\        4. & $\Log{KT5} \Proves \Diamond\Box!A \lif \Box!A$ & $\Ax{5_\Diamond}$\\        5. & $\Log{KT5} \Proves \Box\Diamond\Box!A \lif \Box\Box!A$ & \RK{}, 4 \\        6. & $\Log{KT5} \Proves \Box!A \lif \Box\Box!A$ & \PL, 3, 5. \\      \end{derivation}    \item $\Log{KDB4} \Proves \Ax{T}$:      \begin{derivation}        1. & $\Log{KDB4} \Proves \Diamond\Box!A \lif !A $ & $\Ax{B_\Diamond}$ \\        2. & $\Log{KDB4} \Proves \Box\Box!A \lif \Diamond\Box!A$ & $\Ax{D}$        with $\Box!A$ for $p$\\        3. & $\Log{KDB4} \Proves \Box\Box!A \lif !A$ & \PL, 1, 2\\        4. & $\Log{KDB4} \Proves \Box!A \lif \Box\Box!A$ & \Ax{4} \\        5. & $\Log{KDB4} \Proves \Box!A \lif !A$ & \PL, 4, 3. \\      \end{derivation}    \item $\Log{KB4} \Proves \Ax{5}$:      \begin{derivation}        1. & $\Log{KB4} \Proves \Diamond!A \lif \Box \Diamond\Diamond!A$ & \Ax{B}        with $\Diamond!A$ for $p$\\        2. & $\Log{KB4} \Proves \Diamond\Diamond !A \lif \Diamond !A$ &        $\Ax{4_\Diamond}$ \\        3. & $\Log{KB4} \Proves \Box\Diamond\Diamond !A \lif \Box \Diamond!A$ &        \RK{}, 2 \\        4. & $\Log{KB4} \Proves \Diamond!A \lif \Box\Diamond!A$ & \PL, 1, 3.      \end{derivation}    \item $\Log{KB5} \Proves \Ax{4}$:      \begin{derivation}        1. & $\Log{KB5} \Proves \Box!A \lif \Box\Diamond\Box !A$ & \Ax{B} with        $\Box!A$ for $p$ \\        2. & $\Log{KB5} \Proves  \Diamond\Box!A \lif \Box !A$ &        $\Ax{5_\Diamond}$\\        3. & $\Log{KB5} \Proves  \Box\Diamond\Box!A \lif \Box\Box !A$ & \RK{}, 2 \\        4. & $\Log{KB5} \Proves  \Box!A \lif \Box\Box!A$ & \PL, 1, 3.      \end{derivation}    \item $\Log{KT} \Proves \Ax{D}$:      \begin{derivation}        1. & $\Log{KT} \Proves \Box !A \lif !A$ & \Ax{T} \\        2. & $\Log{KT} \Proves !A \lif \Diamond!A$ & $\Ax{T_\Diamond}$ \\        3. & $\Log{KT} \Proves \Box !A \lif \Diamond !A$ &  \PL, 1, 2      \end{derivation}  \end{enumerate}\end{proof}\begin{defn}  Following tradition, we define \Log{S4} to be the system  \Log{KT4}, and \Log{S5} the system \Log{KTB4}.\end{defn}The following proposition shows that the classical system \Log{S5} hasseveral equivalent axiomatizations. This should not surprise, as thevarious combinations of axioms all characterize equivalence relations(see \olref[frd][es5]{prop:equivalences}).\begin{prop}\ollabel{prop:S5}  $\Log{KTB4} = \Log{KT5} = \Log{KDB4} = \Log{KDB5}$.\end{prop}\begin{proof}  Exercise.\end{proof}\begin{prob}  Prove \olref[nml][prf][prs]{prop:S5}.\end{prob}\end{document}

content/normal-modal-logic/axioms-systems/soundness.tex

% Part: normal-modal-logic% Chapter: axioms-systems% Section: soundness\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{prf}{snd}\olsection{Soundness}!!^a{derivation} system is called sound if everything that can be!!{derive}d is valid. When considering modal systems, i.e.,!!{derivation}s where in addition to \Ax{K} we can use instances ofsome !!{formula}s $!A_1$, \dots,~$!A_n$, we want every !!{derivable}formula to be true in any model in which $!A_1$, \dots, $!A_n$ aretrue.  \begin{thm}[Soundness Theorem]\ollabel{thm:soundness}  If every instance of $!A_1$, \dots, $!A_n$ is valid in the  classes of models $\mClass{C}_1$, \dots, $\mClass{C}_n$,  respectively, then $\Log{K}!A_1\dots !A_n  \Proves !B$ implies that $!B$ is valid in the class of  models $\mClass{C}_1 \cap \dots \cap \mClass{C}_n$.\end{thm}\begin{proof}  By induction on length of proofs. For brevity, put $\mClass{C} =  \mClass{C}_1 \cap \dots \cap \mClass{C}_n$.  \begin{enumerate}  \item Induction Basis: If $!B$ has a proof of length~$1$, then it is    either a tautological instance, an instance    of~\Ax{K},\iftag{prvDiamond}{ or of~\Dual{},}{} or an instance of    one of $!A_1$, \dots,~$!A_n$. In the first case, $!B$ is valid in    $\mClass{C}$, since tautological instance are valid in \emph{any}    class of models, by \olref[syn][tau]{prop:valid-taut}. Similarly    in the second case, by    \olref[syn][sch]{prop:Kvalid}\iftag{prvDiamond}{ and      \olref[syn][sch]{prop:Dual-valid}}{}. Finally in the third case,    since $!B$ is valid in $\mClass{C}_i$ and $\mClass{C} \subseteq    \mClass{C}_i$, we have that $!B$ is valid in $\mClass{C}$ as well    by \olref[syn][val]{prop:subset-class}.  \item Inductive step: Suppose $!B$ has a proof of length $k>1$. If    $!B$ is a tautological instance or an instance of one of $!A_1$,    \dots, $!A_n$, we proceed as in the previous step. So suppose $!B$ is    obtained by \MP{} from previous !!{formula}s $!C \lif !B$ and    $!C$. Then $!C \lif !B$ and $!C$ have proofs of length $<k$, and    by inductive hypothesis they are valid in~$\mClass{C}$. By    \olref[syn][sch]{prop:soundMP}, $!B$ is valid in $\mClass{C}$ as    well. Finally suppose $!B$ is obtained by \Nec{} from $!C$ (so    that $!B = \Box!C$). By inductive hypothesis, $!C$ is valid in    $\mClass{C}$, and by \olref[syn][val]{prop:Nec-rule} so is~$!B$.  \end{enumerate}\end{proof}\end{document}

content/normal-modal-logic/axioms-systems/systems-distinct.tex

% Part: normal-modal-logic% Chapter: axioms-systems% Section: systems-distinct\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{prf}{dis}\olsection{Showing Systems are Distinct}In \olref[prs]{sec} we saw how to prove that two systems of modallogic are in fact the same system. \olref[snd]{thm:soundness} allowsus to show that two modal systems $\Sigma$ and $\Sigma'$ are distinct,by finding !!a{formula}~$!A$ such that $\Sigma' \Proves !A$ that fails ina model of~$\Sigma$.\begin{prop}  $\Log{KD} \subsetneq \Log{KT}$\end{prop}\begin{proof} This is the syntactic counterpart to the semantic fact  that all reflexive relations are serial. To show $\Log{KD} \subseteq  \Log{KT}$ we need to see that $\Log{KD} \Proves !B$ implies  $\Log{KT} \Proves !B$, which follows from $\Log{KT} \Proves  \Log{D}$, as shown in  \olref[prs]{prop:S5facts}\olref[prs]{prop:S5facts-KT-D}.  To show  that the inclusion is proper, by Soundness  (\olref[snd]{thm:soundness}), it suffices to exhibit a model of  \Log{KD} where \Ax{T}, i.e., $\Box p \lif p$, fails (an  easy task left as an exercise), for then by Soundness $\Log{KD}  \Proves/ \Box p \lif p$.\end{proof}\begin{prop}  $\Log{KB} \neq \Log{K4}$. \end{prop}\begin{proof}  We construct a symmetric model where some instance of \Ax{4} fails;  since obviously the instance is !!{derivable} for \Log{K4} but not  in \Log{KB}, it will follow $\Log{K4} \nsubseteq \Log{KB}$.  Consider the symmetric model $\mModel{M}$ of \olref{fig:Bnot4}. Since  the model is symmetric, \Ax{K} and~\Ax{B} are true in~$\mModel{M}$  (by \olref[syn][sch]{prop:Kvalid} and  \olref[frd][acc]{thm:soundschemas}, respectively). However,  $\mSat/{M}{\Box p \lif \Box\Box p}[w_1]$.\end{proof}\begin{figure}[htpb]  \centering  \begin{tikzpicture}[modal]    \node[world] (w1) [label=above:\mFalse{p},    label={below:$\mSat{{}}{\Box p}$\\ $\mSat/{{}}{\Box\Box p}$}] {$w_1$};     \node[world] (w2) [label=above:\mTrue{p},      label=below:$\mSat/{{}}{\Box p}$, right=of w1]{$w_2$};     \draw[->, bend left] (w1) to (w2);     \draw[->, bend left] (w2) to (w1);   \end{tikzpicture}  \caption{A symmetric model falsifying an instance of \Ax{4}.}  \ollabel{fig:Bnot4}\end{figure} \begin{thm}\ollabel{thm:KTBnot45}  $\Log{KTB} \Proves/ \Log{4}$ and $\Log{KTB} \Proves/ \Log{5}$.\end{thm}\begin{proof}  By \olref[frd][acc]{thm:soundschemas} we know that all instances of  \Ax{T} and \Ax{B} are true in every reflexive symmetric model  (respectively). So by soundness, it suffices to find a reflexive  symmetric model containing a world at which some instance of~\Ax{4}  fails, and similarly for~\Ax{5}.  We use the same model for both  claims. Consider the symmetric, reflexive model in  \olref{fig:KTBnot45}.  Then $\mSat/{M}{\Box p \to \Box \Box    p}[w_1]$, so \Ax{4} fails at $w_1$. Similarly, $\mSat/{M}{\Diamond    \lnot p \lif \Box \Diamond \lnot p}[w_2]$, so the instance  of~\Ax{5} with $!A = \lnot p$ fails at~$w_2$.\end{proof}\begin{figure}[htpb]  \centering  \begin{tikzpicture}[modal]    \node[world] (w1) [label={right:\mTrue{p}},      label={below: $\mSat{{}}{\Box p}$\\        $\mSat/{{}}{\Box\Box p}$\\        $\mSat/{{}}{\Diamond\lnot p}$}] {$w_1$};    \draw[reflexive above] (w1) to (w1);    \node[world] (w2) [label={right:\mTrue{p}}, label={below:        $\mSat{{}}{\Diamond\lnot p}$\\        $\mSat/{{}}{\Box\Diamond\lnot p}$}, right=of w1] {$w_2$} ;    \draw[reflexive above] (w2) to (w2);    \node[world] (w3) [label={right:\mFalse{p}},right=of w2] {$w_3$};    \draw[reflexive above] (w3) to (w3);    \draw[->, bend left] (w1) to (w2);      \draw[->, bend left] (w2) to (w3);      \draw[->, bend left] (w3) to (w2);      \draw[->, bend left] (w2) to (w1);    \end{tikzpicture}  \caption{The model for \olref{thm:KTBnot45}.}  \ollabel{fig:KTBnot45}\end{figure}\begin{thm}\ollabel{thm:KD5not4}  $\Log{KD5} \neq \Log{KT4} = \Log{S4}$.\end{thm}\begin{proof}  By \olref[frd][acc]{thm:soundschemas} we know that all instances of  \Ax{D} and~\Ax{5} are true in all serial euclidean models.  So  it suffices to find a serial euclidean model containing a world  at which some instance of~\Ax{4} fails.  Consider the model of  \olref{fig:KD5not4}, and notice that $\mSat/{M}{\Box p  \lif \Box\Box p}[w_1]$. \end{proof}\begin{figure}[t]  \centering  \begin{tikzpicture}[modal]    \node[world] (w2) [label=north west:\mTrue{p}]{$w_2$} ;    \draw[reflexive left] (w2) to (w2);    \node[world] (w1) [label=right:\mFalse{p},      label=below:{$\mSat{{}}{\Box p}, \mSat/{{}}{\Box\Box p}$},      below right=of w2]{$w_1$};    \node[world] (w3) [label=north east:\mTrue{p}, above right=of w1]{$w_3$} ;    \draw[reflexive right] (w3) to (w3);    \node[world] (w4) [label=right:\mFalse{p},above right=of w2]{$w_4$};    \draw[reflexive above] (w4) to (w4);    \draw[->] (w1) to (w2);      \draw[->] (w1) to (w3);      \draw[->, bend left=15] (w2) to (w3);    \draw[->, bend left=15] (w3) to (w2);      \draw[->, bend left=15] (w2) to (w4);    \draw[->, bend left=15] (w4) to (w2);      \draw[->, bend left=15] (w3) to (w4);    \draw[->, bend left=15] (w4) to (w3);    \end{tikzpicture}  \caption{The model for \olref{thm:KD5not4}.}  \ollabel{fig:KD5not4}\end{figure}\begin{prob}  Give an alternative proof of \olref[nml][prf][dis]{thm:KD5not4} using a model  with $3$ worlds.\end{prob}\begin{prob}  Provide a single reflexive transitive model showing that both  $\Log{KT4} \Proves/ \Ax{B}$ and $\Log{KT4} \Proves/ \Ax{5}$.\end{prob}\end{document}

content/normal-modal-logic/axioms-systems/provability-from-set.tex

% Part: normal-modal-logic% Chapter: axioms-systems% Section: provability-from-set\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{prf}{prg}\olsection{\usetoken{S}{derivability} from a Set of \usetoken{P}{formula}}In \olref[prf][prs]{sec} we defined a notion of provabilityof !!a{formula} in a system~$\Sigma$. We now extend this notion toprovability in $\Sigma$ from !!{formula}s in a set~$\Gamma$.\begin{defn}\ollabel{defn:Gammaproves}  !!^a{formula}~$!A$ is !!{derivable} in a system~$\Sigma$ from a set of  !!{formula}s $\Gamma$, written $\Gamma \Proves[\Sigma] !A$ if and  only if there are $!B_1$, \dots, $!B_n \in \Gamma$ such that  $\Sigma \Proves !B_1 \lif (!B_2 \lif \cdots (!B_n \lif !A)  \cdots)$. \end{defn}\end{document}

content/normal-modal-logic/axioms-systems/provability-properties.tex

% Part: normal-modal-logic% Chapter: axioms-systems% Section: provability-properties\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{prf}{prp}\olsection{Properties of \usetoken{S}{derivability}}\begin{prop}\ollabel{prop:derivabilityfacts}  Let $\Sigma$ be a modal system and $\Gamma$ a set of modal  !!{formula}s. The following properties hold:  \begin{enumerate}  \item\ollabel{prop:derivabilityfacts-monotonicity} \emph{Monotonicity}: If    $\Gamma \Proves[\Sigma] !A$ and $\Gamma \subseteq \Delta$ then    $\Delta \Proves[\Sigma] !A$;  \item\ollabel{prop:derivabilityfacts-reflexivity}    \emph{Reflexivity}: If $!A \in \Gamma$ then $\Gamma    \Proves[\Sigma] !A$;  \item\ollabel{prop:derivabilityfacts-cut} \emph{Cut}: If $\Gamma    \Proves[\Sigma] !A$ and $\Delta \cup \{!A\} \Proves[\Sigma] !B$    then $\Gamma \cup \Delta \Proves[\Sigma] !B$;  \item\ollabel{prop:derivabilityfacts-deduction} \emph{Deduction theorem}: $\Gamma \cup \{!B\}    \Proves[\Sigma] !A$ if and only if $\Gamma \Proves[\Sigma] !B \lif      !A$;  \item \ollabel{prop:derivabilityfacts-ruleT}% \emph{Rule T}: If    $\Gamma \Proves[\Sigma] !A_1$ and \dots and $\Gamma    \Proves[\Sigma] !A_n$ and $!A_1 \to (!A_2 \lif \cdots (!A_n \lif    !B)\cdots)$ is a tautological instance, then $\Gamma    \Proves[\Sigma] !B$.  \end{enumerate}\end{prop}The proof is an easy exercise. Part\olref{prop:derivabilityfacts-ruleT} of \olref{prop:derivabilityfacts}gives us that, for instance, if $\Gamma \Proves[\Sigma] !A \lor !B$and $\Gamma \Proves[\Sigma] \lnot !A$, then $\Gamma \Proves[\Sigma]!B$. Also, in what follows, we write $\Gamma, !A \Proves[\Sigma] !B$instead of $\Gamma \cup \{ !A\} \Proves[\Sigma] !B$.\begin{defn}  A set $\Gamma$ is \emph{deductively closed} relatively to a system  $\Sigma$ if and only if $\Gamma \Proves[\Sigma] !A$ implies  $!A \in \Gamma$.\end{defn}\end{document}

content/normal-modal-logic/axioms-systems/consistency.tex

% Part: normal-modal-logic% Chapter: axioms-systems% Section: consistency\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{prf}{con}\olsection{Consistency}Consistency is an important property of sets of !!{formula}s. A set of!!{formula}s is inconsistent if a contradiction, such as~$\lfalse$, is!!{derivable} from it; and otherwise consistent. If a set isinconsistent, its !!{formula}s cannot all be true in a model at aworld. For the completeness theorem we prove the converse: everyconsistent set is true at a world in a model, namely in the ``canonicalmodel.''\begin{defn}  A set $\Gamma$ is \emph{consistent} relatively to a system~$\Sigma$  or, as we will say, $\Sigma$-consistent, if and only if $\Gamma  \Proves/[\Sigma] \lfalse$.\end{defn}So for instance, the set $\{ \Box(p \lif q), \Box p, \lnot\Box q \}$ isconsistent relatively to propositional logic, but not\Log{K}-consistent. Similarly, the set $\{ \Diamond p, \Box\Diamondp \lif q, \lnot q \}$ is not \Log{K5}-consistent.\begin{prop}\ollabel{prop:consistencyfacts}  Let $\Gamma$ be a set of !!{formula}s. Then:  \begin{enumerate}  \item $\Gamma$ is $\Sigma$-consistent if and only if there is    some !!{formula}~$!A$ such that $\Gamma \Proves/[\Sigma]    !A$.  \item \ollabel{prop:consistencyfacts-b}%    $\Gamma \Proves[\Sigma] !A$ if and only if $\Gamma \cup \{    \lnot!A \}$ is not $\Sigma$-consistent.  \item \ollabel{prop:consistencyfacts-c}%    If $\Gamma$ is $\Sigma$-consistent, then for any !!{formula}    $!A$, either $\Gamma \cup \{ !A \}$ is    $\Sigma$-consistent or $\Gamma \cup \{ \lnot!A \}$ is    $\Sigma$-consistent.  \end{enumerate}\end{prop}\begin{proof}  These facts follow easily using classical propositional logic. We  give the argument for \olref{prop:consistencyfacts-c}. Proceed  contrapositively and suppose neither $\Gamma \cup \{ !A \}$ nor  $\Gamma \cup \{ \lnot!A \}$ is $\Sigma$-consistent. Then by  \olref{prop:consistencyfacts-b}, both $\Gamma, !A \Proves[\Sigma]  \lfalse$ and $\Gamma, \lnot !A \Proves[\Sigma] \lfalse$. By the  deduction theorem $\Gamma \Proves[\Sigma] !A \to \lfalse$ and  $\Gamma \Proves[\Sigma] \lnot!A \lif \lfalse$. But $(!A \lif  \lfalse) \lif ((\lnot!A \lif \lfalse) \lif \lfalse)$ is a  tautological instance, hence by  \olref[prp]{prop:derivabilityfacts}\olref[prp]{prop:derivabilityfacts-ruleT},  $\Gamma \Proves[\Sigma] \lfalse$.\end{proof}\end{document}