Normal Modal Logics

Completeness and Canonical Models

content/normal-modal-logic/completeness/completeness.tex

% Part: normal-modal-logic% Chapter: completeness\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{nml}{com}{Completeness and Canonical Models}\olimport{introduction}\olimport{complete-consistent-sets}\olimport{lindenbaums-lemma}\olimport{modalities-ccs}\olimport{canonical-models}\olimport{truth-lemma}\olimport{completeness-K}\olimport{frame-completeness}\OLEndChapterHook\end{document}

content/normal-modal-logic/completeness/introduction.tex

% Part: normal-modal-logic% Chapter: completeness% Section: introduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{com}{int}\olsection{Introduction}If $\Sigma$ is a modal system, then the soundness theorem establishesthat if $\Sigma \Proves !A$, then $!A$ is valid in any class$\mClass{C}$ of models in which all instances of all !!{formula}sin~$\Sigma$ are valid. In particular that means that if $\Log{K}\Proves !A$ then $!A$ is true in all models; if $\Log{KT} \Proves !A$then $!A$ is true in all reflexive models; if $\Log{KD} \Proves !A$then $!A$ is true in all serial models, etc.Completeness is the converse of soundness: that \Log{K} is completemeans that if !!a{formula}~$!A$ is valid, $\Proves !A$, for instance.Proving completeness is a lot harder to do than proving soundness.  Itis useful, first, to consider the contrapositive: \Log{K} is completeiff whenever $\Proves/ !A$, there is a countermodel, i.e., amodel~$\mModel{M}$ such that $\mSat/{M}{!A}$. Equivalently (negating$!A$), we could prove that whenever $\Proves/ \lnot !A$, there is amodel of~$!A$.  In the construction of such a model, we can useinformation contained in $!A$.  When we find models for specific!!{formula}s we often do the same: e.g., if we want to find acountermodel to $p \lif \Box q$, we know that it has to contain aworld where $p$ is true and $\Box q$ is false. And a world where $\Boxq$ is false means there has to be a world accessible from it where $q$is false. And that's all we need to know: which worlds make the!!{propositional variable}s true, and which worlds are accessible fromwhich worlds.In the case of proving completeness, however, we don't have a specific!!{formula}~$!A$ for which we are constructing a model. We want toestablish that a model exists for every $!A$ such that$\Proves/[\Sigma] \lnot !A$. This is a minimal requirement, since\emph{if} $\Proves[\Sigma] \lnot !A$, by soundness, there is no modelfor~$!A$ (in which $\Sigma$ is true).  Now note that $\Proves/[\Sigma]\lnot !A$ iff $!A$ is $\Sigma$-consistent.  (Recall that $\Sigma\Proves/[\Sigma] \lnot !A$ and $!A \Proves/[\Sigma] \lfalse$ areequivalent.)  So our task is to construct a model for every$\Sigma$-consistent !!{formula}.The trick we'll use is to find a $\Sigma$-consistent set of!!{formula}s that contains~$!A$, but also other formulas which tell uswhat the world that makes $!A$ true has to look like. Such sets are\emph{complete} $\Sigma$-consistent sets. It's not enough toconstruct a model with a single world to make~$!A$ true, it will haveto contain multiple worlds and an accessibility relation. The complete$\Sigma$-consistent set containing~$!A$ will also contain other!!{formula}s of the form $\Box !B$ and~$\Diamond !C$. In allaccessible worlds, $!B$ has to be true; in at least one, $!C$ has tobe true. In order to accomplish this, we'll simply take \emph{all}possible complete $\Sigma$-consistent sets as the basis for the set ofworlds. A tricky part will be to figure out when a complete$\Sigma$-consistent set should count as being accessible from anotherin our model.We'll show that in the model so defined, $!A$ is true at aworld---which is also a complete $\Sigma$-consistent set---iff $!A$ is!!a{element} of that set.  If $!A$ is $\Sigma$-consistent, it will be!!a{element} of at least one complete $\Sigma$-consistent set (a factwe'll prove), and so there will be a world where $!A$~is true. So wewill have a single model where every $\Sigma$-consistent!!{formula}~$!A$ is true at some world.  This single model is the\emph{canonical} model for~$\Sigma$.\end{document}

content/normal-modal-logic/completeness/complete-consistent-sets.tex

% Part: normal-modal-logic% Chapter: completeness% Section: complete-consistent-sets\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{com}{ccs}\olsection{Complete $\Sigma$-Consistent Sets}Suppose $\Sigma$ is a set of modal !!{formula}s---think of them as theaxioms or defining principles of a normal modal logic. A set $\Gamma$is $\Sigma$-consistent iff $\Gamma \Proves/[\Sigma] \lfalse$, i.e., ifthere is no !!{derivation} of~$!A_1 \lif (!A_2 \lif \cdots (!A_n \lif\lfalse)\dots)$ from $\Sigma$, where each $!A_i \in \Gamma$. We willconstruct a ``canonical'' model in which each world is taken to be aspecial kind of $\Sigma$-consistent set: one which is not just$\Sigma$-consistent, but maximally so, in the sense that it settlesthe truth value of every modal !!{formula}: for every $!A$, either $!A\in \Gamma$ or $\lnot !A \in \Gamma$:\begin{defn}  A set $\Gamma$ is \emph{complete $\Sigma$-consistent} if and  only if it is $\Sigma$-consistent and for every~$!A$, either  $!A \in \Gamma$ or $\lnot !A \in \Gamma$.\end{defn}Complete $\Sigma$-consistent sets $\Gamma$ have a number of usefulproperties. For one, they are deductively closed, i.e., if $\Gamma\Proves[\Sigma] !A$ then $!A \in \Gamma$. This means in particularthat every instance of !!a{formula}~$!A \in \Sigma$ is also $\in\Gamma$. Moreover, membership in $\Gamma$ mirrors the truth conditionsfor the propositional connectives. This will be important when wedefine the ``canonical model.''\begin{prop}\ollabel{prop:ccs-properties}  Suppose $\Gamma$ is complete $\Sigma$-consistent. Then:  \begin{enumerate}  \item \ollabel{prop:ccs-closed}%    $\Gamma$ is deductively closed in~$\Sigma$.  \item \ollabel{prop:ccs-sigma}%    $\Sigma \subseteq \Gamma$.  \tagitem{prvFalse}{\ollabel{prop:ccs-lfalse}%    $\lfalse \notin \Gamma$}{}  \tagitem{prvTrue}{\ollabel{prop:ccs-ltrue}%    $\ltrue \in \Gamma$}{}  \item \ollabel{prop:ccs-lnot}%    $\lnot!A \in \Gamma$ if and only if $!A \notin    \Gamma$.  \tagitem{prvAnd}{\ollabel{prop:ccs-land}%    $!A \land !B \in \Gamma$ iff $!A \in \Gamma$ and $!B \in \Gamma$}{}  \tagitem{prvOr}{\ollabel{prop:ccs-lor}%    $!A \lor !B \in \Gamma$ iff $!A \in \Gamma$ or $!B \in \Gamma$}{}  \tagitem{prvIf}{\ollabel{prop:ccs-lif}%    $!A \lif !B \in \Gamma$ iff $!A \notin \Gamma$ or $!B \in \Gamma$}{}  \tagitem{prvIff}{\ollabel{prop:ccs-liff}%    $!A \liff !B \in \Gamma$ iff either $!A \in \Gamma$ and $!B \in    \Gamma$, or $!A \notin \Gamma$ and $!B \notin \Gamma$}{}  \end{enumerate}\end{prop}\begin{proof}  \begin{enumerate}  \item Suppose $\Gamma \Proves[\Sigma] !A$ but $!A \notin    \Gamma$. Then since $\Gamma$ is complete $\Sigma$-consistent,    $\lnot!A \in \Gamma$. This would make $\Gamma$ inconsistent, since    $!A, \lnot !A \Proves[\Sigma] \lfalse$.      \item If $!A \in \Sigma$ then $\Gamma \Proves[\Sigma] !A$, and $!A    \in \Gamma$ by deductive closure, i.e.,    case~\olref{prop:ccs-closed}.      \tagitem{prvFalse}{If $\lfalse \in \Gamma$, then $\Gamma    \Proves[\Sigma] \lfalse$, so $\Gamma$ would be    $\Sigma$-inconsistent.}{}    \tagitem{prvTrue}{$\Gamma \Proves[\Sigma] \ltrue$, so $\ltrue \in    \Gamma$ by deductive closure, i.e.,    case~\olref{prop:ccs-closed}.}{}\item If $\lnot!A \in \Gamma$, then by consistency $!A \notin    \Gamma$; and if $!A \notin \Gamma$ then $!A \in \Gamma$ since    $\Gamma$ is complete $\Sigma$-consistent.      \tagitem{prvAnd}{\iftag{probAnd}{Exercise.}{Suppose $!A \land !B \in      \Gamma$. Since $(!A \land !B) \lif !A$ is a tautological      instance, $!A \in \Gamma$ by deductive closure, i.e.,      case~\olref{prop:ccs-closed}. Similarly for $!B \in \Gamma$. On      the other hand, suppose both $!A \in \Gamma$ and $!B \in      \Gamma$. Then deductive closure implies $(!A \land !B) \in      \Gamma$, since $!A \lif (!B \lif (!A \land !B))$ is a      tautological instance.}}{}  \tagitem{prvOr}{\iftag{probOr}{Exercise.}{Suppose $!A \lor !B \in      \Gamma$, and $!A \notin \Gamma$ and $!B \notin \Gamma$. Since      $\Gamma$ is complete $\Sigma$-consistent, $\lnot!A \in \Gamma$      and $\lnot !B \in \Gamma$. Then $\lnot(!A \lor !B) \in \Gamma$      since $\lnot !A \lif (\lnot !B \lif \lnot (!A \lor !B))$ is a      tautological instance. This would mean that $\Gamma$ is      $\Sigma$-inconsistent, a contradiction.}}{}    \tagitem{prvIf}{\iftag{probIf}{Exercise.}{Suppose $!A \lif !B \in      \Gamma$ and $!A \in \Gamma$; then $\Gamma \Proves[\Sigma] !B$,      whence $!B \in \Gamma$ by deductive closure. Conversely, if $!A      \lif !B \notin \Gamma$ then since $\Gamma$ is complete      $\Sigma$-consistent, $\lnot (!A \lif !B) \in \Gamma$. Since      $\lnot(!A \lif !B) \lif !A$ is a tautological instance, $!A \in      \Gamma$ by deductive closure. Since $\lnot(!A \lif !B) \lif      \lnot !B$ is a tautological instance, $\lnot !B \in      \Gamma$. Then $!B \notin \Gamma$ since $\Gamma$ is      $\Sigma$-consistent.}}{}    \tagitem{prvIff}{\iftag{probIff}{Exercise.}{Suppose $!A \liff !B \in      \Gamma$. If $!A \in \Gamma$, then $!B \in \Gamma$, since $(!A      \liff !B) \lif (!A \lif !B)$ is a tautological      instance. Similarly, if $!B \in \Gamma$, then $!A \in \Gamma$.      So either both $!A \in \Gamma$ and $!B \in \Gamma$, or neither      $!A \in \Gamma$ nor $!B \in \Gamma$.            Conversely, suppose $!A \lif !B \notin \Gamma$. Since $\Gamma$      is complete $\Sigma$-consistent, $\lnot (!A \liff !B) \in      \Gamma$. Since $\lnot(!A \liff !B) \lif (!A \lif \lnot !B)$ is a      tautological instance, if $!A \in \Gamma$ then $\lnot !B \in      \Gamma$, and since $\Gamma$ is $\Sigma$-consistent, $!B \notin      \Gamma$. Similarly, if $!B \in \Gamma$ then $!A \notin \Gamma$.      So neither $!A \in \Gamma$ and $!B \in \Gamma$, nor $!A \notin      \Gamma$ and $!B \notin \Gamma$.}}{}  \end{enumerate}\end{proof}\begin{probtag}{probAnd,probOr,probIf,probIff}  Complete the proof of \olref[nml][com][ccs]{prop:ccs-properties}.\end{probtag}\end{document}

content/normal-modal-logic/completeness/lindenbaums-lemma.tex

% Part: normal-modal-logic% Chapter: completeness% Section: lindenbaums-lemma\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{com}{lin}\olsection{Lindenbaum's Lemma}Lindenbaum's Lemma establishes that every $\Sigma$-consistent set of!!{formula}s is contained in at least one \emph{complete}$\Sigma$-consistent set. Our construction of the canonical model willshow that for each complete $\Sigma$-consistent set~$\Delta$, there isa world in the canonical model where all and only the !!{formula}sin~$\Delta$ are true. So Lindenbaum's Lemma guarantees that every$\Sigma$-consistent set is true at some world in the canonical model.\begin{thm}[Lindenbaum's Lemma]\ollabel{thm:lindenbaum}  If $\Gamma$ is $\Sigma$-consistent then there is a complete  $\Sigma$-consistent set $\Delta$ extending~$\Gamma$.\end{thm}\begin{proof}Let $!A_0$, $!A_1$, \dots{} be an exhaustive listing of all formulasof the language (repetitions are allowed). For instance, start bylisting $\Obj p_0$, and at each stage $n \ge 1$ list the finitely manyformulas of length~$n$ using only variables among $\Obj p_0$,\dots,~$\Obj p_n$. We define sets of !!{formula}s $\Delta_n$ byinduction on~$n$, and we then set $\Delta = \bigcup_n \Delta_n$. Wefirst put $\Delta_0 = \Gamma$. Supposing that $\Delta_n$ has beendefined, we define $\Delta_{n+1}$ by:\[\Delta_{n+1} =\begin{cases}  \Delta_n \cup \{!A_n\}, & \text{if $\Delta_n \cup \{ !A_n\}$    is $\Sigma$-consistent;} \\  \Delta_n \cup \{ \lnot !A_n\}, & \text{otherwise.}\end{cases}\]Now let $\Delta = \bigcup_{n=0}^\infty \Delta_n$.We have to show that this definition actually yields a set $\Delta$with the required properties, i.e., $\Gamma \subseteq \Delta$ and$\Delta$ is complete $\Sigma$-consistent.It's obvious that $\Gamma \subseteq \Delta$, since $\Delta_0 \subseteq\Delta$ by construction, and $\Delta_0 = \Gamma$. In fact, $\Delta_n\subseteq \Delta$ for all~$n$, since $\Delta$ is the union ofall~$\Delta_n$. (Since in each step of the construction, we add!!a{formula} to the set already constructed, $\Delta_n \subseteq\Delta_{n+1}$, so since $\subseteq$ is transitive, $\Delta_n \subseteq\Delta_{m}$ whenever $n \le m$.)  At each stage of the construction, weeither add $!A_n$ or $\lnot !A_n$, and every !!{formula} appears (atleast once) in the list of all~$!A_n$. So, for every $!A$ either $!A\in \Delta$ or $\lnot !A \in \Delta$, so $\Delta$ is complete bydefinition.Finally, we have to show, that $\Delta$ is $\Sigma$-consistent.  To dothis, we show that (a) if $\Delta$ were $\Sigma$-inconsistent, thensome $\Delta_n$ would be $\Sigma$-inconsistent, and (b) all $\Delta_n$are $\Sigma$-consistent.So suppose $\Delta$ were $\Sigma$-inconsistent. Then $\Delta\Proves[\Sigma] \lfalse$, i.e., there are $!A_1$, \dots,~$!A_k \in\Delta$ such that $\Sigma \Proves !A_1 \lif (!A_2 \lif \cdots (!A_k\lif \lfalse)\dots)$. Since $\Delta = \bigcup_{n=0}^\infty \Delta_n$, each$!A_i \in \Delta_{n_i}$ for some~$n_i$. Let $n$ be the largest ofthese. Since $n_i \le n$, $\Delta_{n_i} \subseteq \Delta_n$. So, all$!A_i$ are in some~$\Delta_n$. This would mean $\Delta_n\Proves[\Sigma] \lfalse$, i.e., $\Delta_n$ is $\Sigma$-inconsistent.To show that each $\Delta_n$ is $\Sigma$-consistent, we use a simpleinduction on~$n$. $\Delta_0 = \Gamma$, and we assumed $\Gamma$ was$\Sigma$-consistent. So the claim holds for $n = 0$. Now suppose itholds for $n$, i.e., $\Delta_n$ is $\Sigma$-consistent. $\Delta_{n+1}$is either $\Delta_n \cup \{!A_n\}$ if that is $\Sigma$-consistent,otherwise it is $\Delta_n \cup \{\lnot!A_n\}$. In the first case,$\Delta_{n+1}$ is clearly $\Sigma$-consistent. However, by\olref[prf][con]{prop:consistencyfacts}\olref[prf][con]{prop:consistencyfacts-c},either $\Delta_n \cup \{!A_n\}$ or $\Delta_n \cup \{\lnot!A_n\}$ isconsistent, so $\Delta_{n+1}$ is consistent in the other case as well.\end{proof}\begin{cor}\ollabel{cor:provability-characterization}  $\Gamma \Proves[\Sigma] !A$ if and only if $!A \in \Delta$ for  each  complete $\Sigma$-consistent set $\Delta$ extending $\Gamma$  (including when $\Gamma = \emptyset$, in which case we get another  characterization of the modal system $\Sigma$.)\end{cor}\begin{proof}  Suppose $\Gamma \Proves[\Sigma] !A$, and let $\Delta$ be any  complete $\Sigma$-consistent set extending $\Gamma$. If $!A  \notin \Delta$ then by maximality $\lnot!A \in \Delta$ and so  $\Delta \Proves[\Sigma] !A$ (by monotonicity) and $\Delta  \Proves[\Sigma] \lnot!A$ (by reflexivity), and so $\Delta$ is  inconsistent. Conversely if $\Gamma \Proves/[\Sigma] !A$, then  $\Gamma \cup \{ \lnot!A\}$ is $\Sigma$-consistent, and by  Lindenbaum's Lemma there is a complete consistent set $\Delta$  extending $\Gamma \cup \{ \lnot!A \}$. By consistency, $!A  \notin \Delta$.\end{proof}\end{document}

content/normal-modal-logic/completeness/modalities-ccs.tex

% Part: normal-modal-logic% Chapter: completeness% Section: modalities-ccs\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{com}{mod}\olsection{Modalities and Complete Consistent Sets}\begin{explain}When we construct a model~$\mModel{M^\Sigma}$ whose set of worlds isgiven by the complete $\Sigma$-consistent sets~$\Delta$ in some normalmodal logic~$\Sigma$, we will also need to define an accessibilityrelation~$R^\Sigma$ between such ``worlds.'' We want it to be the casethat the accessibility relation (and the assignment $V^\Sigma)$ aredefined in such a way that $\mSat{M^\Sigma}{!A}[\Delta]$ iff $!A \in\Delta$. How should we do this?Once the accessibility relation is defined, the definition of truth ata world ensures that \iftag{prvBox}{$\mSat{M^\Sigma}{\Box!A}[\Delta]$  iff $\mSat{M^\Sigma}{!A}[\Delta']$ for all $\Delta'$ such that  $R^\Sigma\Delta\Delta'$}{$\mSat{M^\Sigma}{\Diamond!A}[\Delta]$ iff  $\mSat{M^\Sigma}{!A}[\Delta']$ for at least one $\Delta'$ such that  $R^\Sigma\Delta\Delta'$}.  The proof that$\mSat{M^\Sigma}{!A}[\Delta]$ iff $!A \in \Delta$ requires that thisis true in particular for !!{formula}s starting with a modal operator,i.e., \iftag{prvBox}{$\mSat{M^\Sigma}{\Box!A}[\Delta]$ iff $\Box !A  \in \Delta$}{$\mSat{M^\Sigma}{\Diamond!A}[\Delta]$ iff $\Diamond !A  \in \Delta$}. Combining this requirement with the definition oftruth at a world for \iftag{prvBox}{$\Box !A$}{$\Diamond !A$} yields:\[\iftag{prvBox}{%  \Box!A \in \Delta \text{ iff } !A \in \Delta' \text{    for all $\Delta'$ with } R^\Sigma\Delta\Delta'}{%  \Diamond!A \in \Delta \text{ iff } !A \in \Delta' \text{ for at    least one } \Delta' \text{ with } R^\Sigma\Delta\Delta'}\]\iftag{prvBox}{Consider the left-to-right direction: it says that if  $\Box !A \in \Delta$, then $!A \in \Delta'$ for any $!A$ and any  $\Delta'$ with $R^\Sigma\Delta\Delta'$. If we stipulate that  $R^\Sigma\Delta\Delta'$ iff $!A \in \Delta'$ for all $\Box!A \in  \Delta$, then this holds. We can write the condition on the right of  the ``iff'' more compactly as: $\Setabs{!A}{\Box!A \in \Delta}  \subseteq \Delta'$.}{Consider the right-to-left direction: it says  that if $!A \in \Delta'$ then $\Diamond!A \in \Delta$, for any $!A$  and $\Delta'$ with $R^\Sigma\Delta\Delta'$. If we stipulate that  $R^\Sigma\Delta\Delta'$ holds whenever $\Diamond!A \in \Delta$ for  all $!A \in \Delta'$, then this holds.  We can write the condition  on the right of the ``iff'' more compactly as:  $\Setabs{\Diamond!A}{!A \in \Delta'} \subseteq \Delta$.}So the question is: does this definition of $R^\Sigma$ in factguarantee that \iftag{prvBox}{$\Box !A \in \Delta$ iff  $\mSat{M^\Sigma}{\Box !A}[\Delta]$? \iftag{prvDiamond}{Does it also    guarantee that }{}}{}\iftag{prvDiamond}{$\Diamond !A \in \Delta$  iff $\mSat{M^\Sigma}{\Diamond !A}[\Delta]$?}{} The next few resultswill establish this.\end{explain}\begin{defn}  If $\Gamma$ is a set of !!{formula}s, let  \begin{align*}    \Box\Gamma & = \Setabs{\Box !B}{!B \in \Gamma}\\    \Diamond\Gamma & = \Setabs{\Diamond !B}{!B \in \Gamma}\\    \intertext{and}    \Box^{-1}\Gamma & = \Setabs{!B}{\Box !B \in \Gamma}\\    \Diamond^{-1}\Gamma & = \Setabs{!B}{\Diamond !B \in \Gamma}\\  \end{align*}\end{defn}In other words, $\Box\Gamma$ is $\Gamma$ with $\Box$ in front of every!!{formula} in~$\Gamma$; $\Box^{-1}\Gamma$ is all the $\Box$'ed!!{formula}s of~$\Gamma$ with the initial $\Box$'s removed.  Thisdefinition is not terribly important on its own, but will simplify thenotation considerably.Note that $\Box\Box^{-1}\Gamma \subseteq \Gamma$:\[\Box\Box^{-1}\Gamma = \Setabs{\Box!B}{\Box!B \in \Gamma}\]i.e., it's just the set of all those !!{formula}s of~$\Gamma$ thatstart with~$\Box$.\begin{lem}\ollabel{lem:box1}  If $\Gamma \Proves[\Sigma] !A$ then $\Box\Gamma \Proves[\Sigma] \Box  !A$.\end{lem}\begin{proof}  If $\Gamma \Proves[\Sigma] !A$ then there are $!B_1$, \dots, $!B_k  \in \Gamma$ such that $\Sigma \Proves !B_1 \lif (!B_2 \lif \cdots  (!B_n \lif !A)\cdots)$. Since $\Sigma$ is normal, by rule \RK{},  $\Sigma \Proves \Box!B_1 \lif (\Box!B_2 \lif \cdots (\Box!B_n \lif  \Box!A)\cdots)$, where obviously $\Box!B_1$, \dots, $\Box!B_k \in  \Box\Gamma$. Hence, by definition, $\Box\Gamma \Proves[\Sigma] \Box  !A$.\end{proof}\begin{lem}\ollabel{lem:box2}  If $\Box^{-1} \Gamma \Proves[\Sigma] !A$ then $\Gamma  \Proves[\Sigma] \Box!A$.\end{lem}\begin{proof}  Suppose $\Box^{-1}\Gamma \Proves[\Sigma] !A$; then by  \olref{lem:box1}, $\Box\Box^{-1}\Gamma \Proves \Box!A$. But since  $\Box\Box^{-1}\Gamma \subseteq \Gamma$, also $\Gamma \Proves[\Sigma]  \Box!A$ by monotonicity.\end{proof}\iftag{prvBox}{%% Box is primitive  \begin{prop}\ollabel{prop:box}  If $\Gamma$ is complete $\Sigma$-consistent, then $\Box !A \in  \Gamma$ if and only if for every complete $\Sigma$-consistent  $\Delta$ such that $\Box^{-1} \Gamma \subseteq \Delta$, it holds  that $!A \in \Delta$.\end{prop}\begin{proof}  Suppose $\Gamma$ is complete $\Sigma$-consistent. The ``only if''  direction is easy: Suppose $\Box !A \in \Gamma$ and that  $\Box^{-1}\Gamma \subseteq \Delta$. Since $\Box!A \in \Gamma$, $!A  \in \Box^{-1}\Gamma \subseteq \Delta$, so $!A \in \Delta$.  For the ``if'' direction, we prove the contrapositive: Suppose  $\Box!A \notin \Gamma$. Since $\Gamma$ is complete  $\Sigma$-consistent, it is deductively closed, and hence $\Gamma  \Proves/[\Sigma] \Box !A$. By \olref{lem:box2},  $\Box^{-1}\Gamma \Proves/[\Sigma] !A$. By  \olref[prf][con]{prop:consistencyfacts}\olref[prf][con]{prop:consistencyfacts-b},  $\Box^{-1}\Gamma \cup \{ \lnot!A \}$ is $\Sigma$-consistent. By  Lindenbaum's Lemma, there is a complete $\Sigma$-consistent  set~$\Delta$ such that $\Box^{-1}\Gamma \cup \{ \lnot!A \} \subseteq  \Delta$. By consistency, $!A \notin \Delta$.\end{proof}}{%% Box is not primitive, only Diamond is\begin{prop}\ollabel{prop:diamond}  If $\Gamma$ is complete $\Sigma$-consistent, then $\Diamond !A \in  \Gamma$ if and only if for some complete $\Sigma$-consistent  $\Delta$ such that $\Diamond\Delta \subseteq  \Gamma$, it holds that $!A \in \Delta$.\end{prop}\begin{proof}  Suppose $\Gamma$ is complete $\Sigma$-consistent. The right-to-left  part is easy: Let $\Delta$ be complete $\Sigma$-consistent such that  $\Diamond\Delta \subseteq \Gamma$ and $!A \in \Delta$.  Then  $\Diamond!A \in \Diamond\Delta \subseteq \Gamma$, i.e., $\Diamond!A  \in \Gamma$.  For the left-to-right direction, assume $\Diamond !A \in \Gamma$. We  have to show that there is a complete $\Sigma$-consistent $\Delta$  with $!A \in \Delta$ and $\Diamond\Delta \subseteq \Gamma$.  Since  $\Diamond !A \in \Gamma$, and $\Gamma$ is $\Sigma$-consistent,  $\Box\lnot !A \notin \Gamma$. Since $\Gamma$ is complete  $\Sigma$-consistent, it is deductively closed, so $\Gamma  \Proves/[\Sigma] \Box\lnot !A$.  By \olref{lem:box2},  $\Box^{-1}\Gamma \Proves/[\Sigma] \lnot !A$. By  \olref[prf][con]{prop:consistencyfacts}\olref[prf][con]{prop:consistencyfacts-b},  $\Box^{-1}\Gamma \cup \{ !A \}$ is $\Sigma$-consistent. By  Lindenbaum's Lemma, there is a complete $\Sigma$-consistent  set~$\Delta$ such that $\Box^{-1}\Gamma \cup \{ !A \} \subseteq  \Delta$. Clearly, $!A \in \Delta$.  To see that $\Diamond\Delta  \subseteq \Gamma$, assume it weren't: For some $!B \in \Delta$,  $\Diamond !B \notin \Gamma$. Then, since $\Gamma$ is complete  $\Sigma$-consistent, $\Box\lnot !B \in \Gamma$. But then also $\lnot  !B \in \Box^{-1}\Gamma \subseteq \Delta$, which would make $\Delta$  inconsistent.\end{proof}}\begin{lem}\ollabel{lem:box-iff-diamond}  Suppose $\Gamma$ and $\Delta$ are complete  $\Sigma$-consistent. Then $\Box^{-1}\Gamma \subseteq \Delta$ if and  only if $\Diamond\Delta \subseteq \Gamma$.\end{lem}\begin{proof}  ``Only if'' direction: Assume $\Box^{-1}\Gamma \subseteq \Delta$ and  suppose $\Diamond!A \in \Diamond\Delta$ (i.e., $!A \in \Delta$).  In  order to show $\Diamond!A \in \Gamma$, it suffices to show  $\Box\lnot!A \notin \Gamma$, for then by maximality, $\lnot\Box\lnot  !A \in \Gamma$. Now, if $\Box\lnot!A \in \Gamma$ then by hypothesis  $\lnot!A \in \Delta$, against the consistency of $\Delta$ (since $!A  \in \Delta$). Hence $\Box\lnot!A \notin \Gamma$, as required.  ``If'' direction: Assume $\Diamond\Delta  \subseteq \Gamma$. We argue contrapositively: suppose $!A  \notin \Delta$ in order to show $\Box!A \notin \Gamma$. If  $!A \notin \Delta$ then by maximality $\lnot!A \in \Delta$  and so by hypothesis $\Diamond\lnot!A \in \Gamma$. But in a  normal modal logic $\Diamond\lnot!A$ is equivalent to  $\lnot\Box !A$, and if the latter is in $\Gamma$, by consistency  $\Box!A \notin\Gamma$, as required.\end{proof}\iftag{prvBox}{%  \iftag{prvDiamond}{%% Box and Diamond are both primitive; prove% prop:diamond using lem:box-iff-diamond  \begin{prop}\ollabel{prop:diamond}  If $\Gamma$ is complete $\Sigma$-consistent, then $\Diamond !A \in  \Gamma$ if and only if for some complete $\Sigma$-consistent  $\Delta$ such that $\Diamond\Delta \subseteq  \Gamma$, it holds that $!A \in \Delta$.\end{prop}\begin{proof}Suppose $\Gamma$ is complete $\Sigma$-consistent.  $\Diamond!A \in\Gamma$ iff $\lnot\Box\lnot !A \in \Gamma$ by \Dual{} and closure.$\lnot\Box\lnot !A \in \Gamma$ iff $\Box\lnot !A \notin \Gamma$ by\olref[ccs]{prop:ccs-properties}\olref[ccs]{prop:ccs-lnot} since$\Gamma$ is complete $\Sigma$-consistent.  By \olref{prop:box},$\Box\lnot !A \notin \Gamma$ iff, for some complete$\Sigma$-consistent $\Delta$ with $\Box^{-1}\Gamma \subseteq \Delta$,$\lnot!A \notin \Delta$.  Now consider any such~$\Delta$. By\olref{lem:box-iff-diamond}, $\Box^{-1}\Gamma \subseteq \Delta$ iff$\Diamond\Delta \subseteq \Gamma$. Also, $\lnot !A \notin \Delta$ iff$!A \in \Delta$ by\olref[ccs]{prop:ccs-properties}\olref[ccs]{prop:ccs-lnot}.  So$\Diamond!A \in \Gamma$ iff, for some complete $\Sigma$-consistent$\Delta$ with $\Diamond\Delta \subseteq \Gamma$, $!A \in \Delta$.\end{proof}}{}}{}  \begin{prob}  Show that if $\Gamma$ is complete $\Sigma$-consistent, then  \iftag{prvBox}{$\Diamond !A \in \Gamma$ if and only if there is a    complete $\Sigma$-consistent $\Delta$ such that $\Box^{-1}\Gamma    \subseteq \Delta$ and $!A \in \Delta$.}{$\Box !A \in    \Gamma$ if and only if for every complete $\Sigma$-consistent    $\Delta$ such that $\Box^{-1} \Gamma \subseteq \Delta$, it holds    that $!A \in \Delta$.}  \emph{Do this without using    \olref[nml][com][mod]{lem:box-iff-diamond}}.\end{prob}\end{document}

content/normal-modal-logic/completeness/canonical-models.tex

% Part: normal-modal-logic% Chapter: completeness% Section: canonical-models\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{com}{cmd}\olsection{Canonical Models}The \emph{canonical model} for a modal system~$\Sigma$ is a specificmodel~$\mModel{M^\Sigma}$ in which the worlds are all complete$\Sigma$-consistent sets. Its accessibility relation~$R^\Sigma$ andvaluation $V^\Sigma$ are defined so as to guarantee that the!!{formula}s true at a world~$\Delta$ are exactly the !!{formula}smaking up~$\Delta$.\begin{defn}  Let $\Sigma$ be a normal modal logic. The \emph{canonical model} for  $\Sigma$ is $\mModel{M}^\Sigma = \tuple{W^\Sigma, R^\Sigma,    V^\Sigma}$, where:  \begin{enumerate}  \item $W^\Sigma = \Setabs{ \Delta }{\Delta \text{      is complete $\Sigma$-consistent} }$.  \item $R^\Sigma \Delta\Delta'$ holds if and only if    \iftag{prvBox}{$\Box^{-1}\Delta \subseteq      \Delta'$}{$\Diamond\Delta' \subseteq \Delta$}.  \item $V^\Sigma(p) = \Setabs{\Delta}{p \in \Delta}$.  \end{enumerate}\end{defn}\end{document}

content/normal-modal-logic/completeness/truth-lemma.tex

% Part: normal-modal-logic% Chapter: completeness% Section: truth-lemma\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{com}{tru}\olsection{The Truth Lemma}The canonical model~$\mModel{M^\Sigma}$ is defined in such a way that$\mSat{M^\Sigma}{!A}[\Delta]$ iff $!A \in \Delta$. For !!{propositionalvariable}s, the definition of $V^\Sigma$ yields this directly. We haveto verify that the equivalence holds for all !!{formula}s, however. Wedo this by induction. The inductive step involves proving theequivalence for !!{formula}s involving propositional operators (wherewe have to use \olref[ccs]{prop:ccs-properties}) and the modaloperators (where we invoke the results of \olref[mod]{sec}).\begin{prop}[Truth Lemma]  \ollabel{prop:truthlemma}  For every !!{formula}~$!A$, $\mSat{M^\Sigma}{!A}[\Delta]$ if and only if  $!A \in \Delta$.\end{prop}\begin{proof}  By induction on~$!A$.  \begin{enumerate}    \tagitem{prvFalse}{\indcase{!A}{\lfalse}{$\mSat/{M^\Sigma}{\lfalse}[\Delta]$        by \olref[syn][trw]{defn:mmodels}, and $\lfalse \notin \Delta$        by        \olref[ccs]{prop:ccs-properties}\olref[ccs]{prop:ccs-lfalse}.}}{}    \tagitem{prvTrue}{\indcase{!A}{\ltrue}{$\mSat{M^\Sigma}{\ltrue}[\Delta]$        by \olref[syn][trw]{defn:mmodels}, and $\ltrue \in \Delta$ by        \olref[ccs]{prop:ccs-properties}\olref[ccs]{prop:ccs-ltrue}.}}{}    \item \indcase{!A}{p}{$\mSat{M^\Sigma}{p}[\Delta]$ iff $\Delta \in      V^\Sigma(p)$ by \olref[syn][trw]{defn:mmodels}.  Also, $\Delta      \in V^\Sigma(p)$ iff $p \in \Delta$ by definition      of~$V^\Sigma$.}    \tagitem{prvNot}{\indcase{!A}{\lnot !B}{%        \iftag{probNot}{Exercise.}{$\mSat{M^\Sigma}{\lnot !B}[\Delta]$          iff $\mSat/{M^\Sigma}{!B}[\Delta]$          (\olref[syn][trw]{defn:mmodels}) iff $!B \notin \Delta$ (by          inductive hypothesis) iff $\lnot !B \in \Delta$ (by          \olref[ccs]{prop:ccs-properties}\olref[ccs]{prop:ccs-lnot}).}}}{}    \tagitem{prvAnd}{\indcase{!A}{!B \land !C}{%        \iftag{probAnd}{Exercise.}{$\mSat{M^\Sigma}{!B \land            !C}[\Delta]$ iff $\mSat{M^\Sigma}{!B}[\Delta]$ and          $\mSat{M^\Sigma}{!C}[\Delta]$ (by          \olref[syn][trw]{defn:mmodels}) iff $!B \in \Delta$ and $!C          \in \Delta$ (by inductive hypothesis) iff $!B \land !C \in          \Delta$ (by          \olref[ccs]{prop:ccs-properties}\olref[ccs]{prop:ccs-land}).}}}{}    \tagitem{prvOr}{\indcase{!A}{!B \lor !C}{%        \iftag{probOr}{Exercise.}{$\mSat{M^\Sigma}{!B \lor            !C}[\Delta]$ iff $\mSat{M^\Sigma}{!B}[\Delta]$ or          $\mSat{M^\Sigma}{!C}[\Delta]$ (by          \olref[syn][trw]{defn:mmodels}) iff $!B \in \Delta$ or $!C          \in \Delta$ (by inductive hypothesis) iff $!B \lor !C \in          \Delta$ (by          \olref[ccs]{prop:ccs-properties}\olref[ccs]{prop:ccs-lor}).}}}{}    \tagitem{prvIf}{\indcase{!A}{!B \lif !C}{%        \iftag{probIf}{Exercise.}{$\mSat{M^\Sigma}{!B \lif            !C}[\Delta]$ iff $\mSat/{M^\Sigma}{!B}[\Delta]$ or          $\mSat{M^\Sigma}{!C}[\Delta]$ (by          \olref[syn][trw]{defn:mmodels}) iff $!B \notin \Delta$ or          $!C \in \Delta$ (by inductive hypothesis) iff $!B \lif !C          \in \Delta$ (by          \olref[ccs]{prop:ccs-properties}\olref[ccs]{prop:ccs-lif}).}}}{}    \tagitem{prvIff}{\indcase{!A}{!B \liff !C}{%        \iftag{probIff}{Exercise.}{$\mSat{M^\Sigma}{!B \liff            !C}[\Delta]$ iff either $\mSat{M^\Sigma}{!B}[\Delta]$ and          $\mSat{M^\Sigma}{!C}[\Delta]$ or          $\mSat/{M^\Sigma}{!B}[\Delta]$ and          $\mSat/{M^\Sigma}{!C}[\Delta]$ (by          \olref[syn][trw]{defn:mmodels}) iff either $!B \in \Delta$          and $!C \in \Delta$ or $!B \notin \Delta$ and $!C \notin          \Delta$ (by inductive hypothesis) iff $!B \liff !C \in          \Delta$ (by          \olref[ccs]{prop:ccs-properties}\olref[ccs]{prop:ccs-liff}).}}}{}    \tagitem{prvBox}{\indcase{!A}{\Box !B}{%        \iftag{probBox}{Exercise.}{First suppose that          $\mSat{M^\Sigma}{\Box !B}[\Delta]$. By          \olref[syn][trw]{defn:mmodels}, for every $\Delta'$ such          that $R^\Sigma \Delta\Delta'$,          $\mSat{M^\Sigma}{!B}[\Delta']$. By inductive hypothesis, for          every $\Delta'$ such that $R^\Sigma \Delta\Delta'$, $!B \in          \Delta'$. By definition of $R^\Sigma$, for every $\Delta'$          such that $\Box^{-1} \Delta \subseteq \Delta'$, $!B \in          \Delta'$. By \olref[mod]{prop:box}, $\Box !B \in          \Delta$.          Now assume $\Box !B \in \Delta$. Let $\Delta' \in W^\Sigma$          be such that $R^\Sigma \Delta\Delta'$, i.e., $\Box^{-1}\Delta          \subseteq \Delta'$. Since $\Box !B \in \Delta$, $!B \in          \Box^{-1} \Delta$. Consequently, $!B \in \Delta'$. By          inductive hypothesis, $\mSat{M^\Sigma}{!B}[\Delta']$. Since          $\Delta'$ is arbitrary with $R^\Sigma \Delta\Delta'$, for          all $\Delta' \in W^\Sigma$ such that $R^\Sigma          \Delta\Delta'$, $\mSat{M^\Sigma}{!B}[\Delta']$. By          \olref[syn][trw]{defn:mmodels}, $\mSat{M^\Sigma}{\Box            !B}[\Delta]$.}}}{}    \tagitem{prvDiamond}{\indcase{!A}{\Diamond !B}{%        \iftag{probDiamond}{Exercise.}{First suppose that          $\mSat{M^\Sigma}{\Diamond !B}[\Delta]$.  By          \olref[syn][trw]{defn:mmodels}, for some $\Delta'$ such that          $R^\Sigma \Delta\Delta'$, $\mSat{M^\Sigma}{!B}[\Delta']$.          By inductive hypothesis, for some $\Delta'$ such that          $R^\Sigma \Delta\Delta'$, $!B \in \Delta'$. By definition of          $R^\Sigma$,\iftag{prvBox}{ for some $\Delta'$ such that            $\Box^{-1} \Delta \subseteq \Delta'$, $!B \in \Delta'$.            By \olref[mod]{prop:diamond},}{} for some $\Delta'$ such          that $\Diamond \Delta' \subseteq \Delta$, $!B \in          \Delta'$. Since $!B \in \Delta'$, $\Diamond !B \in \Diamond          \Delta'$, so $\Diamond !B \in \Delta$.          Now assume $\Diamond !B \in \Delta$. By          \olref[mod]{prop:diamond}, there is a complete          $\Sigma$-consistent $\Delta' \in W^\Sigma$ such that          $\Diamond \Delta' \subseteq \Delta$ and $!B \in          \Delta'$.\iftag{prvBox}{ By \olref[mod]{lem:box-iff-diamond},            there is a $\Delta' \in W^\Sigma$ such that $\Box^{-1}            \Delta \subseteq \Delta'$, and $!B \in \Delta'$.}{} By          definition of $R^\Sigma$, $R^\Sigma \Delta\Delta'$, so there          is a $\Delta' \in W^\Sigma$ such that $R^\Sigma          \Delta\Delta'$ and $!B \in \Delta'$. By          \olref[syn][trw]{defn:mmodels}, $\mSat{M^\Sigma}{\Diamond            !B}[\Delta]$.}}}{}  \end{enumerate}\end{proof}\begin{probtag}{probFalse,probTrue,probNot,proband,probOr,probIf,probIff,probBox,probDiamond}  Complete the proof of \olref[nml][com][tru]{prop:truthlemma}.\end{probtag}\end{document}

content/normal-modal-logic/completeness/completeness-K.tex

% Part: normal-modal-logic% Chapter: completeness% Section: completeness-K\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{com}{cmk}\olsection{Determination and Completeness for  \Log{K}}We are now prepared to use the canonical model to establishcompleteness. Completeness follows from the fact that the !!{formula}strue in the canonical model for~$\Sigma$ are exactly the$\Sigma$-!!{derivable} ones. Models with this property are said to\emph{determine}~$\Sigma$.\begin{defn}  A model $\mModel{M}$ \emph{determines} a normal modal  logic~$\Sigma$ precisely when $\mSat{M}{!A}$ if and only if $\Sigma  \Proves !A$, for all !!{formula}s~$!A$.\end{defn}\begin{thm}[Determination]\ollabel{thm:determination}   $\mSat{M^\Sigma}{!A}$ if and only if $\Sigma \Proves !A$.\end{thm}\begin{proof}  If $\mSat{M^\Sigma}{!A}$, then for every complete  $\Sigma$-consistent $\Delta$, we have  $\mSat{M^\Sigma}{!A}[\Delta]$. Hence, by the Truth Lemma, $!A \in  \Delta$ for every complete $\Sigma$-consistent $\Delta$, whence by  \olref[lin]{cor:provability-characterization} (with $\Gamma =  \emptyset$), $\Sigma \Proves !A$.  Conversely, if $\Sigma \Proves !A$ then by  \olref[ccs]{prop:ccs-properties}\olref[ccs]{prop:ccs-closed}, every  complete $\Sigma$-consistent $\Delta$ contains~$!A$, and hence by  the Truth Lemma, $\mSat{M^\Sigma}{!A}[\Delta]$ for every~$\Delta \in  W^\Sigma$, i.e., $\mSat{M^\Sigma}{!A}$.\end{proof}Since the canonical model for \Log{K} determines~\Log{K}, weimmediately have completeness of~\Log{K} as a corollary:\begin{cor}\ollabel{cor:Kcomplete}  The basic modal logic \Log{K} is complete with respect to the  class of all models, i.e., if $\Entails !A$ then $\Log{K}  \Proves !A$.\end{cor}\begin{proof}  Contrapositively, if $\Log{K} \Proves/ !A$ then by Determination  $\mSat/{M^{\Log{K}}}{!A}$ and hence $!A$ is not valid.\end{proof}For the general case of completeness of a system $\Sigma$ with respectto a class of models, e.g., of \Log{KTB4} with respect to the class ofreflexive, symmetric, transitive models, determination alone is notenough.  We must also show that the canonical model for the system$\Sigma$ is a member of the class, which does not follow obviouslyfrom the canonical model construction---nor is it always true!\end{document}

content/normal-modal-logic/completeness/frame-completeness.tex

% Part: normal-modal-logic% Chapter: completeness% Section: frame-completeness\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{com}{fra}\olsection{Frame Completeness}The completeness theorem for \Log{K} can be extended to other modalsystems, once we show that the canonical model for a given logic hasthe corresponding frame property.\begin{thm}\ollabel{thm:completeframeprops}  If a normal modal logic $\Sigma$ contains one of the !!{formula}s on the  left-hand side of \olref{tab:correspondencetable},  then the canonical model for~$\Sigma$ has the corresponding property  on the right-hand side.\end{thm}\begin{table}[htp]  \centering    \begin{tabular}{| l || l |}      \hline      \emph{If $\Sigma$ contains \dots} & \emph{\dots the canonical        model for $\Sigma$ is:} \\      \hline \hline      \Ax{D}:\;\; $\Box!A \lif \Diamond !A$ & \quad serial; \\      \hline      \Ax{T}:\;\; $\Box!A \lif !A$ &\quad  reflexive;\\      \hline      \Ax{B}: \;\;$!A \lif \Box\Diamond!A$ &\quad  symmetric; \\      \hline      \Ax{4}: \;\; $\Box!A \lif \Box\Box!A$ & \quad transitive; \\      \hline       \Ax{5}: \;\; $\Diamond !A \lif \Box\Diamond!A$& \quad euclidean.\\      \hline    \end{tabular}    \caption{Basic correspondence facts.}    \ollabel{tab:correspondencetable}\end{table}\begin{proof}  We take each of these up in turn.  Suppose $\Sigma$ contains \Ax{D}, and let $\Delta \in W^\Sigma$; we  need to show that there is a $\Delta'$ such that $R^\Sigma  \Delta\Delta'$. It suffices to show that $\Box^{-1}\Delta$ is  $\Sigma$-consistent, for then by Lindenbaum's Lemma, there is a  complete $\Sigma$-consistent set $\Delta' \supseteq  \Box^{-1}\Delta$, and by definition of $R^\Sigma$  \iftag{prvBox}{}{and \olref[mod]{lem:box-iff-diamond} }we have  $R^\Sigma \Delta\Delta'$. So, suppose for contradiction that  $\Box^{-1}\Delta$ is \emph{not} $\Sigma$-consistent, i.e.,  $\Box^{-1}\Delta \Proves[\Sigma] \lfalse$. By \olref[mod]{lem:box2},  $\Delta \Proves[\Sigma] \Box\lfalse$, and since $\Sigma$ contains  \Ax{D}, also $\Delta \Proves[\Sigma] \Diamond\lfalse$. But $\Sigma$  is normal, so $\Sigma \Proves \lnot\Diamond \lfalse$  (\olref[prf][nor]{prop:notDiamondBot}), whence also $\Delta  \Proves[\Sigma] \lnot\Diamond \lfalse$, against the consistency  of~$\Delta$.  Now suppose $\Sigma$ contains \Ax{T}, and let $\Delta \in  W^\Sigma$. We want to show $R^\Sigma \Delta\Delta$,  i.e.,\iftag{prvBox}{}{ by \olref[mod]{lem:box-iff-diamond},}  $\Box^{-1}\Delta \subseteq \Delta$. But if $\Box!A \in \Delta$ then  by \Ax{T} also $!A \in \Delta$, as desired.  Now suppose $\Sigma$ contains \Ax{B}, and suppose $R^\Sigma  \Delta\Delta'$ for $\Delta$, $\Delta' \in W^\Sigma$. We need to show  that $R^\Sigma \Delta'\Delta$, i.e.,\iftag{prvBox}{    $\Box^{-1}\Delta' \subseteq \Delta$. By    \olref[mod]{lem:box-iff-diamond}, this is equivalent to}{}  $\Diamond\Delta \subseteq \Delta'$. So suppose $!A \in \Delta$. By  \Ax{B}, also $\Box\Diamond!A \in \Delta$. By the hypothesis that  $R^\Sigma \Delta\Delta'$\iftag{prvBox}{}{ and    \olref[mod]{lem:box-iff-diamond}}, we have that $\Box^{-1}\Delta  \subseteq \Delta'$, and hence $\Diamond!A \in \Delta'$, as required.  Now suppose $\Sigma$ contains \Ax{4}, and suppose $R^\Sigma  \Delta_1\Delta_2$ and $R^\Sigma \Delta_2\Delta_3$. We need to show  $R^\Sigma \Delta_1\Delta_3$. From the hypothesis\iftag{prvBox}{}{ and    \olref[mod]{lem:box-iff-diamond}} we have both $\Box^{-1}\Delta_1  \subseteq \Delta_2$ and $\Box^{-1}\Delta_2 \subseteq \Delta_3$. In  order to show $R^\Sigma \Delta_1\Delta_3$ it suffices to show  $\Box^{-1}\Delta_1 \subseteq \Delta_3$. So let $!B \in  \Box^{-1}\Delta_1$, i.e., $\Box!B \in \Delta_1$. By \Ax{4}, also  $\Box\Box!B \in \Delta_1$ and by hypothesis we get, first, that  $\Box!B \in \Delta_2$ and, second, that $!B \in \Delta_3$, as  desired.  Now suppose $\Sigma$ contains \Ax{5}, suppose $R^\Sigma  \Delta_1\Delta_2$ and $R^\Sigma \Delta_1\Delta_3$. We need to show  $R^\Sigma \Delta_2\Delta_3$. The first hypothesis gives  $\Box^{-1}\Delta_1 \subseteq \Delta_2$\iftag{prvBox}{}{ by    \olref[mod]{lem:box-iff-diamond}}, and the second hypothesis is  equivalent to $\Diamond\Delta_3 \subseteq \Delta_1$\iftag{prvBox}{,    by \olref[mod]{lem:box-iff-diamond}}{}.  To show $R^\Sigma  \Delta_2\Delta_3$\iftag{prvBox}{, by    \olref[mod]{lem:box-iff-diamond}, it suffices to}{ we have to}  show $\Diamond\Delta_3 \subseteq \Delta_2$. So let $\Diamond!A \in  \Diamond\Delta_3$, i.e., $!A \in \Delta_3$. By the second hypothesis  $\Diamond!A \in \Delta_1$ and by \Ax{5}, $\Box\Diamond!A \in  \Delta_1$ as well. But now the first hypothesis gives $\Diamond!A \in  \Delta_2$, as desired.  \end{proof}As a corollary we obtain completeness results for a number ofsystems. For instance, we know that $\Log{S5} = \Log{KT5} =\Log{KTB4}$ is complete with respect to the class of all reflexiveeuclidean models, which is the same as the class of all reflexive,symmetric and transitive models.\begin{thm}\ollabel{thm:generaldet}  Let $\mClass{C}_\Ax{D}$, $\mClass{C}_\Ax{T}$,  $\mClass{C}_\Ax{B}$, $\mClass{C}_\Ax{4}$, and  $\mClass{C}_\Ax{5}$ be the class of all serial, reflexive,  symmetric, transitive, and euclidean models (respectively). Then for  any schemas $!A_1$, \dots, $!A_n$ among \Ax{D},  \Ax{T}, \Ax{B}, \Ax{4}, and \Ax{5}, the system  $\Log{K}!A_1 \dots !A_n$ is determined by the  class of models $\mClass{C} = \mClass{C}_{!A_1} \cap \dots  \cap \mClass{C}_{!A_n}$. \end{thm}\begin{prop}  Let $\Sigma$ be a normal modal logic; then:  \begin{enumerate}  \item\ollabel{prop:anotherfive-a}%    If $\Sigma$ contains the schema $\Diamond!A \lif \Box     !A$ then the canonical model for $\Sigma$ is partially functional.   \item If $\Sigma$ contains the schema $\Diamond!A \liff \Box     !A$ then the canonical model for $\Sigma$ is functional.   \item If $\Sigma$ contains the schema $\Box\Box!A \lif \Box     !A$ then the canonical model for $\Sigma$ is weakly dense.   \end{enumerate}(see \olref[frd][acc]{tab:anotherfive} for definitions of these frame  properties).\end{prop}\begin{proof}  \begin{enumerate}  \item Suppose that $\Sigma$ contains the schema $\Diamond !A \lif    \Box !A$, to show that $R^\Sigma$ is partially functional we need    to prove that for any $\Delta_1$, $\Delta_2$, $\Delta_3 \in    W^\Sigma$, if $R^\Sigma \Delta_1\Delta_2$ and $R^\Sigma    \Delta_1\Delta_3$ then $\Delta_2=\Delta_3$. Since $R^\Sigma    \Delta_1\Delta_2$ we have $\Box^{-1}\Delta_1 \subseteq \Delta_2$    and since $R^\Sigma \Delta_1\Delta_3$ also $\Box^{-1}\Delta_1    \subseteq \Delta_3$\iftag{prvBox}{}{, both by      \olref[mod]{lem:box-iff-diamond}}. The identity    $\Delta_2=\Delta_3$ will follow if we can establish the two    inclusions $\Delta_2 \subseteq \Delta_3$ and $\Delta_3 \subseteq    \Delta_2$. For the first inclusion, let $!A \in \Delta_2$; then    $\Diamond!A \in \Delta_1$, and by the schema and deductive closure    of $\Delta_1$ also $\Box!A \in \Delta_1$, whence by the hypothesis    that $R^\Sigma \Delta_1\Delta_3$, $!A \in \Delta_3$. The second    inclusion is similar.  \item This follows immediately from part~\olref{prop:anotherfive-a}    and the seriality proof in \olref{thm:completeframeprops}.  \item Suppose $\Sigma$ contains the schema $\Box\Box!A \lif \Box!A$    and to show that $R^\Sigma$ is weakly dense, let $R^\Sigma    \Delta_1\Delta_2$. We need to show that there is a complete    $\Sigma$-consistent set $\Delta_3$ such that $R^\Sigma    \Delta_1\Delta_3$ and $R^\Sigma \Delta_3\Delta_2$. Let:    \[    \Gamma = \Box^{-1}\Delta_1 \cup \Diamond\Delta_2.    \]    It suffices to show that $\Gamma$ is $\Sigma$-consistent, for then    by Lindenbaum's Lemma it can be extended to a complete    $\Sigma$-consistent set~$\Delta_3$ such that $\Box^{-1}\Delta_1    \subseteq \Delta_3$ and $\Diamond\Delta_2 \subseteq \Delta_3$,    i.e., $R^\Sigma \Delta_1\Delta_3$\iftag{prvBox}{}{ (by      \olref[mod]{lem:box-iff-diamond})} and $R^\Sigma    \Delta_3\Delta_2$\iftag{prvBox}{ (by      \olref[mod]{lem:box-iff-diamond})}{}.    Suppose for contradiction that $\Gamma$ is not consistent. Then    there are !!{formula}s $\Box!A_1$, \dots, $\Box!A_n \in \Delta_1$    and $!B_1$, \dots,~$!B_m \in \Delta_2$ such that \[!A_1, \dots,    !A_n, \Diamond!B_1, \dots, \Diamond!B_m \Proves[\Sigma]    \lfalse.\] Since $\Diamond (!B_1 \land \dots \land !B_m) \to    (\Diamond!B_1 \land \dots \land \Diamond!B_m)$ is !!{derivable} in    every normal modal logic, we argue as follows, contradicting the    consistency of~$\Delta_2$:    \begin{align*}      !A_1, \dots, !A_n, & \Diamond!B_1, \dots,      \Diamond!B_m \Proves[\Sigma] \lfalse \\      !A_1, \dots,!A_n & \Proves[\Sigma] (\Diamond!B_1 \land      \dots \land \Diamond!B_m) \lif \lfalse\\      & \qquad\text{by the deduction theorem}\\      & \qquad\text{\olref[prf][prp]{prop:derivabilityfacts}\olref[prf][prp]{prop:derivabilityfacts-deduction}, and \Taut} \\      !A_1, \dots,!A_n & \Proves[\Sigma]      \Diamond(!B_1 \land      \dots \land !B_m) \lif \lfalse\\      & \qquad \text{since $\Sigma$ is normal} \\      !A_1, \dots,!A_n & \Proves[\Sigma]      \lnot\Diamond (!B_1 \land \dots \land !B_m)\\      & \qquad\text{by \PL} \\      !A_1, \dots,!A_n & \Proves[\Sigma]      \Box\lnot (!B_1 \land \dots \land !B_m)\\      & \qquad\text{$\Box\lnot$ for $\lnot\Diamond$} \\      \Box!A_1, \dots,\Box!A_n      & \Proves[\Sigma] \Box\Box \lnot (!B_1 \land \dots \land !B_m)\\      & \qquad\text{by \olref[mod]{lem:box1}} \\      \Box!A_1, \dots,\Box!A_n      & \Proves[\Sigma]      \Box\lnot (!B_1 \land \dots \land !B_m)\\      &\qquad\text{by schema $\Box\Box!A \lif \Box!A$} \\      \Delta_1 & \Proves[\Sigma]      \Box\lnot (!B_1 \land \dots \land !B_m)\\      &\qquad\text{by monotonicity, \olref[prf][prp]{prop:derivabilityfacts}\olref[prf][prp]{prop:derivabilityfacts-monotonicity}} \\      & \Box\lnot (!B_1 \land \dots \land !B_m) \in \Delta_1\\      &\qquad\text{by deductive closure}; \\      & \lnot (!B_1 \land \dots \land !B_m) \in \Delta_2\\      &\qquad \text{since }      R^\Sigma \Delta_1\Delta_2.     \end{align*}  \end{enumerate}\end{proof}On the strength of these examples, one might think that everysystem~$\Sigma$ of modal logic is \emph{complete}, in the sense thatit proves every formula which is valid in every frame in which everytheorem of $\Sigma$ is valid. Unfortunately, there are many systemsthat are not complete in this sense.\end{document}

Source-census fragment evidence

The complete original formula is shown in Read and Explore. These immutable census fragments are retained for traceability.

Census fragment projected-formula-0026469 — source evidence only
<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" data-expression-id="expr-48fb58a9bfb800b8" data-suppressed-composite-member="1"><semantics><mrow><mtext>source fragment rendered in the complete composite object</mtext></mrow><annotation encoding="application/x-tex">W^\Sigma = \Setabs{ \Delta }{\Delta \text{ is complete</annotation></semantics></math>
Census fragment projected-formula-0026470 — source evidence only
<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" data-expression-id="expr-1af35c81144c00e6" data-suppressed-composite-member="2"><semantics><mrow><mtext>source fragment rendered in the complete composite object</mtext></mrow><annotation encoding="application/x-tex">-consistent} }</annotation></semantics></math>