Normal Modal Logics

Modal Tableaux

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

% Part: normal-modal-logic% Chapter: axioms-systems\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{nml}{tab}{Modal \usetoken{P}{tableau}}\begin{editorial}  Draft chapter on prefixed tableaux for modal logic. Needs more  examples, completeness proofs, and discussion of how one can find  countermodels from unsuccessful searches for closed tableaux.\end{editorial}\olimport{introduction}\olimport{rules-for-K}\olimport{proofs-in-K}\olimport{soundness}\olimport{more-rules}\olimport{more-soundness}\olimport{simple-S5}\olimport{completeness}\olimport{countermodels}\OLEndChapterHook\end{document}

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

% Part: normal-modal-logic% Chapter: tableaux% Section: introduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{tab}{int}\olsection{Introduction}!!^{tableau}s are certain (downward-branching) trees of !!{signed  formula}s, i.e., pairs consisting of a truth value sign ($\True$ or$\False$) and !!a{sentence}\[\sFmla{\True}{!A} \text{ or } \sFmla{\False}{!A}.\]!!^a{tableau} begins with a number of \emph{assumptions}. Each further!!{signed formula} is generated by applying one of the inferencerules. Some inference rules add one or more !!{signed formula}s to atip of the tree; others add two new tips, resulting in two branches.Rules result in !!{signed formula}s where the !!{formula} isless complex than that of the !!{signed formula} to which it wasapplied. When a branch contains both $\sFmla{\True}{!A}$ and$\sFmla{\False}{!A}$, we say the branch is \emph{closed}. If everybranch in !!a{tableau} is closed, the entire !!{tableau} is closed. Aclosed !!{tableau} constitutes !!a{derivation} that shows that the setof !!{signed formula}s which were used to begin the !!{tableau} areunsatisfiable.  This can be used to define a $\Proves$ relation:$\Gamma \Proves !A$ iff there is some finite set~$\Gamma_0 = \{!B_1,\dots, !B_n\} \subseteq \Gamma$ such that there is a closed!!{tableau} for the assumptions\[\{\sFmla{\False}{!A}, \sFmla{\True}{!B_1}, \dots, \sFmla{\True}{!B_n}\}.\]For modal logics, we have to both extend the notion of !!{signedformula} and add rules thatcover~\iftag{prvBox}{$\Box$\iftag{prvDiamond}{ and    $\Diamond$}}{$\Diamond$}. In addition to a sign($\True$ or$\False$), !!{formula}s in modal !!{tableau}s also have\emph{prefixes}~$\sigma$. The prefixes are non-empty sequences ofpositive integers, i.e., $\sigma \in (\PosInt)^* \setminus\{\emptyseq\}$. When we write such prefixes without the surrounding$\tuple{\ }$, and separate the individual !!{element}s by~$.$'sinstead of $,$'s. If $\sigma$ is a prefix, then $\sigma.n$ is $\sigma\concat \tuple{n}$; e.g., if $\sigma = 1.2.1$, then $\sigma.3$ is$1.2.1.3$. So for instance,\[\sFmla{\True}{\Box !A \lif !A}[1.2]\]is a \emph{prefixed !!{signed formula}} (or just a \emph{prefixed  !!{formula}} for short).Intuitively, the prefix names a world in a model that might satisfythe !!{formula}s on a branch of !!a{tableau}, and if $\sigma$ namessome world, then $\sigma.n$ names a world accessible from (the worldnamed by)~$\sigma$.\end{document}

content/normal-modal-logic/tableaux/rules-for-K.tex

% Part: normal-modal-logic% Chapter: tableaux% Section: rules-for-K\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{tab}{rul}\olsection{Rules for \Ax{K}}The rules for the regular propositional connectives are the same asfor regular propositional signed !!{tableau}s, just with prefixesadded. In each case, the rule applied to a signed !!{formula}$\sFmla{S}{!A}[\sigma]$ produces new !!{formula}s that are alsoprefixed by~$\sigma$. This should be intuitively clear: e.g., if $!A\land !B$ is true at (a world named by)~$\sigma$, then $!A$ and $!B$are true at~$\sigma$ (and not at any other world). We collect thepropositional rules in \olref{tab:prop-rules}.\begin{table}  \[\def\arraystretch{3}\begin{array}{|c|c|}    \hline    \AxiomC{\sFmla{\True}{\lnot !A}[\sigma]}    \RightLabel{\TRule{\True}{\lnot}}    \UnaryInfC{\sFmla{\False}{!A}[\sigma]}    \DisplayProof    &    \AxiomC{\sFmla{\False}{\lnot !A}[\sigma]}    \RightLabel{\TRule{\False}{\lnot}}    \UnaryInfC{\sFmla{\True}{!A}[\sigma]}    \DisplayProof    \\[1ex]    \hline    \AxiomC{\sFmla{\True}{!A \land !B}[\sigma]}    \RightLabel{\TRule{\True}{\land}}    \UnaryInfC{\sFmla{\True}{!A}[\sigma]}    \noLine    \UnaryInfC{\sFmla{\True}{!B}[\sigma]}    \DisplayProof    &    \AxiomC{\sFmla{\False}{!A \land !B}[\sigma]}    \RightLabel{\TRule{\False}{\land}}    \UnaryInfC{$\sFmla{\False}{!A}[\sigma] \quad \mid \quad      \sFmla{\False}{!B}[\sigma]$}    \DisplayProof    \\[2ex]    \hline    \AxiomC{\sFmla{\True}{!A \lor !B}[\sigma]}    \RightLabel{\TRule{\True}{\lor}}    \UnaryInfC{$\sFmla{\True}{!A}[\sigma] \quad \mid \quad      \sFmla{\True}{!B}[\sigma]$}    \DisplayProof    &    \AxiomC{\sFmla{\False}{!A \lor !B}[\sigma]}    \RightLabel{\TRule{\False}{\lor}}    \UnaryInfC{\sFmla{\False}{!A}[\sigma]}    \noLine    \UnaryInfC{\sFmla{\False}{!B}[\sigma]}    \DisplayProof    \\[2ex]    \hline    \AxiomC{\sFmla{\True}{!A \lif !B}[\sigma]}    \RightLabel{\TRule{\True}{\lif}}    \UnaryInfC{$\sFmla{\False}{!A}[\sigma] \quad \mid      \quad \sFmla{\True}{!B}[\sigma]$}    \DisplayProof    &    \AxiomC{\sFmla{\False}{!A \lif !B}[\sigma]}    \RightLabel{\TRule{\False}{\lif}}    \UnaryInfC{\sFmla{\True}{!A}[\sigma]}    \noLine    \UnaryInfC{\sFmla{\False}{!B}[\sigma]}    \DisplayProof    \\[2ex]    \hline  \end{array}\]  \caption{Prefixed !!{tableau} rules for the propositional    connectives}  \ollabel{tab:prop-rules}\end{table}The closure condition is the same as for ordinary !!{tableau}s,although we require that not just the !!{formula}s but also theprefixes must match. So a branch is closed if it contains both\[\sFmla{\True}{!A}[\sigma] \quad\text{and}\quad \sFmla{\False}{!A}[\sigma]\]for some prefix $\sigma$ and !!{formula}~$!A$.The rules for setting up assumptions is also as for ordinary!!{tableau}s, except that for assumptions we always use theprefix~$1$. (It does not matter which prefix we use, as long as it'sthe same for all assumptions.) So, e.g., we say that\[!B_1, \dots, !B_n \Proves !A\]iff there is a closed tableau for the assumptions\[\sFmla{\True}{!B_1}[1], \dots, \sFmla{\True}{!B_n}[1],\sFmla{\False}{!A}[1].\]For the modal operator\iftag{prvBox}{\iftag{prvDiamond}{s~$\Box$    and}{~$\Box$}}{}\iftag{prvDiamond}{~$\Diamond$}{}, the prefix ofthe conclusion of the rule applied to !!a{formula} withprefix~$\sigma$ is $\sigma.n$. However, which $n$ is allowed dependson whether the sign is~$\True$ or~$\False$.\iftag{prvBox}{The $\TRule{\True}{\Box}$ rule extends a branch  containing $\sFmla{\True}{\Box !A}[\sigma]$ by  $\sFmla{\True}{!A}[\sigma.n]$.\iftag{prvDiamond}{ Similarly,    t}{}}{T}\iftag{prvDiamond}{he $\TRule{\False}{\Diamond}$ rule  extends a branch containing $\sFmla{\False}{\Diamond !A}[\sigma]$ by  $\sFmla{\False}{!A}[\sigma.n]$.}{}\iftag{notprvBox,notprvDiamond}{It}{They} can only be applied for aprefix~$\sigma.n$ which \emph{already} occurs on the branch in whichit is applied. Let's call such a prefix ``used'' (on the branch).\iftag{prvBox}{The $\TRule{\False}{\Box}$ rule extends a branch  containing $\sFmla{\False}{\Box !A}[\sigma]$ by  $\sFmla{\False}{!A}[\sigma.n]$.\iftag{prvDiamond}{ Similarly,    t}{}}{T}\iftag{prvDiamond}{he $\TRule{\True}{\Diamond}$ rule extends  a branch containing $\sFmla{\True}{\Diamond !A}[\sigma]$ by  $\sFmla{\True}{!A}[\sigma.n]$.}{}\iftag{notprvBox,notprvDiamond}{This rule}{These rules}, however, canonly be applied for a prefix~$\sigma.n$ which \emph{does not} alreadyoccur on the branch in which it is applied. We call such prefixes``new'' (to the branch).The rules are given in \olref{tab:rules-K}.\begin{table}  \begin{center}    \def\arraystretch{3}\def\fCenter{}    \begin{tabular}{|c|c|}    \hline    \iftag{prvBox}{      \AxiomC{\sFmla{\True}{\Box !A}[\sigma]}      \RightLabel{\TRule{\True}{\Box}}      \UnaryInfC{\sFmla{\True}{!A}[\sigma.n]}      \DisplayProof      &      \AxiomC{\sFmla{\False}{\Box !A}[\sigma]}      \RightLabel{\TRule{\False}{\Box}}      \UnaryInfC{\sFmla{\False}{!A}[\sigma.n]}      \DisplayProof\\      $\sigma.n$ is used & $\sigma.n$ is new      \\[1ex]      \hline}{}    \iftag{prvDiamond}{      \AxiomC{\sFmla{\True}{\Diamond !A}[\sigma]}      \RightLabel{\TRule{\True}{\Diamond}}      \UnaryInfC{\sFmla{\True}{!A}[\sigma.n]}      \DisplayProof      &      \AxiomC{\sFmla{\False}{\Diamond !A}[\sigma]}      \RightLabel{\TRule{\False}{\Diamond}}      \UnaryInfC{\sFmla{\False}{!A}[\sigma.n]}      \DisplayProof\\      $\sigma.n$ is new & $\sigma.n$ is used      \\[1ex]      \hline}{}    \end{tabular}  \end{center}  \caption{The modal rules for \Ax{K}.}  \ollabel{tab:rules-K}\end{table}The requirement that the restriction that the prefix for\iftag{prvBox}{\TRule{\True}{\Box}}{\TRule{\False}{\Diamond}} must beused is necessary as otherwise we would count the following as aclosed !!{tableau}:\iftag{notprvBox,notprvDiamond}{%  \iftag{prvBox}{%  \begin{oltableau}    [\pFmla{\True}{\Box \formula{A}}{1}, just = \TAss      [\pFmla{\False}{\lnot\Box\lnot \formula{A}}{1}, just = \TAss        [\pFmla{\True}{\formula{A}}{1.1}, just = {\TRule{\True}{\Box}[1]}          [\pFmla{\True}{\Box\lnot\formula{A}}{1},            just ={\TRule{\False}{\lnot}[2]}            [\pFmla{\True}{\lnot\formula{A}}{1.1},              just = {\TRule{\True}{\Box}[4]}              [\pFmla{\False}{\formula{A}}{1.1},                  just ={\TRule{\True}{\lnot}[5]}, close]            ]          ]        ]      ]    ]  \end{oltableau}  }{  \begin{oltableau}    [\pFmla{\True}{\lnot\Diamond\lnot \formula{A}}{1}, just = \TAss      [\pFmla{\False}{\Diamond\formula{A}}{1}, just = \TAss        [\pFmla{\False}{\formula{A}}{1.1}, just = {\TRule{\False}{\Diamond}[2]}          [\pFmla{\False}{\Diamond\lnot\formula{A}}{1},            just ={\TRule{\True}{\lnot}[1]}            [\pFmla{\False}{\lnot\formula{A}}{1.1},              just = {\TRule{\False}{\Diamond}[4]}              [\pFmla{\True}{\formula{A}}{1.1},                  just ={\TRule{\True}{\lnot}[5]}, close]            ]          ]        ]      ]    ]  \end{oltableau}}}{  \begin{oltableau}    [\pFmla{\True}{\Box \formula{A}}{1}, just = \TAss      [\pFmla{\False}{\Diamond \formula{A}}{1}, just = \TAss        [\pFmla{\True}{\formula{A}}{1.1}, just = {\TRule{\True}{\Box}[1]}          [\pFmla{\False}{\formula{A}}{1.1},            just = {\TRule{\False}{\Diamond}[2]}, close]        ]      ]    ]\end{oltableau}}But $\Box \formula{A} \Entails/ \Diamond \formula{A}$, so our proofsystem would be unsound. Likewise, $\Diamond \formula{A} \Entails/\Box \formula{A}$, but without the restriction that the prefix for\iftag{prvBox}{\TRule{\False}{\Box}}{\TRule{\True}{\Diamond}} must benew, this would be a closed tableau: \iftag{notprvBox,notprvDiamond}{%  \iftag{prvBox}{%  \begin{oltableau}    [\pFmla{\True}{\lnot\Box\lnot \formula{A}}{1}, just = \TAss      [\pFmla{\False}{\Box \formula{A}}{1}, just = \TAss        [\pFmla{\False}{\formula{A}}{1.1}, just = {\TRule{\True}{\Box}[2]}          [\pFmla{\False}{\Box\lnot\formula{A}}{1},            just ={\TRule{\True}{\lnot}[1]}            [\pFmla{\False}{\lnot\formula{A}}{1.1},              just = {\TRule{\False}{\Box}[4]}              [\pFmla{\True}{\formula{A}}{1.1},                  just ={\TRule{\False}{\lnot}[5]}, close]            ]          ]        ]      ]    ]  \end{oltableau}  }{  \begin{oltableau}    [\pFmla{\True}{\Diamond \formula{A}}{1}, just = \TAss      [\pFmla{\False}{\lnot\Diamond\lnot\formula{A}}{1}, just = \TAss        [\pFmla{\True}{\formula{A}}{1.1}, just = {\TRule{\True}{\Diamond}[1]}          [\pFmla{\True}{\Diamond\lnot\formula{A}}{1},            just ={\TRule{\False}{\lnot}[2]}            [\pFmla{\True}{\lnot\formula{A}}{1.1},              just = {\TRule{\True}{\Diamond}[4]}              [\pFmla{\False}{\formula{A}}{1.1},                  just ={\TRule{\True}{\lnot}[5]}, close]            ]          ]        ]      ]    ]  \end{oltableau}}}{  \begin{oltableau}    [\pFmla{\True}{\Diamond \formula{A}}{1}, just = \TAss,name=one      [\pFmla{\False}{\Box \formula{A}}{1}, just = \TAss, name=two        [\pFmla{\True}{\formula{A}}{1.1}, just = {\TRule{\True}{\Diamond}[1]}          [\pFmla{\False}{\formula{A}}{1.1},            just = {\TRule{\False}{\Box}[2]}, close]        ]      ]    ]  \end{oltableau}}\end{document}

content/normal-modal-logic/tableaux/proofs-in-K.tex

% Part: normal-modal-logic% Chapter: tableaux% Section: proofs-in-K\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{tab}{prk}\olsection{\usetoken{P}{tableau} for \Log{K}}\iftag{prvBox}{\begin{ex}  We give a closed tableau that shows $\Proves (\Box!A \land \Box!B)  \lif \Box (!A \land !B)$.  \begin{oltableau}    [\pFmla{\False}{(\Box\formula{A} \land \Box\formula{B}) \lif        \Box (\formula{A} \land \formula{B})}{1},      just =\TAss      [\pFmla{\True}{\Box\formula{A} \land \Box\formula{B}}{1},        just = {\TRule{\False}{\lif}[1]}        [\pFmla{\False}{\Box(\formula{A} \land \formula{B})}{1},          just = {\TRule{\False}{\lif}[1]}          [\pFmla{\True}{\Box\formula{A}}{1},            just = {\TRule{\True}{\land}[2]}            [\pFmla{\True}{\Box\formula{B}}{1},              just = {\TRule{\True}{\land}[2]}              [\pFmla{\False}{\formula{A} \land \formula{B}}{1.1},                just = {\TRule{\False}{\Box}[3]}                [\pFmla{\False}{\formula{A}}{1.1},                  just = {\TRule{\False}{\land}[6]}                  [\pFmla{\True}{\formula{A}}{1.1},                    just= {\TRule{\True}{\Box}[4]}, close]]                [\pFmla{\False}{\formula{B}}{1.1},                  just = {\TRule{\False}{\land}[6]}                  [\pFmla{\True}{\formula{B}}{1.1},                    just= {\TRule{\True}{\Box}[5]}, close]]              ]            ]          ]        ]      ]    ]  \end{oltableau}\end{ex}}{}\iftag{prvDiamond}{\begin{ex}  We give a closed tableau that shows $\Proves \Diamond(!A \lor !B)  \lif (\Diamond !A \lor \Diamond !B)$:  \begin{oltableau}    [\pFmla{\False}{\Diamond(\formula{A} \lor \formula{B}) \lif        (\Diamond \formula{A} \lor \Diamond \formula{B})}{1},      just =\TAss      [\pFmla{\True}{\Diamond(\formula{A} \lor \formula{B})}{1},        just = {\TRule{\False}{\lif}[1]}        [\pFmla{\False}{\Diamond\formula{A} \lor \Diamond\formula{B}}{1},          just = {\TRule{\False}{\lif}[1]}          [\pFmla{\False}{\Diamond\formula{A}}{1},            just = {\TRule{\False}{\lor}[3]}            [\pFmla{\False}{\Diamond\formula{B}}{1},              just = {\TRule{\False}{\lor}[3]}              [\pFmla{\True}{\formula{A} \lor \formula{B}}{1.1},                just = {\TRule{\True}{\Diamond}[2]},                [\pFmla{\True}{\formula{A}}{1.1},                  just = {\TRule{\True}{\lor}[6]}                  [\pFmla{\False}{\formula{A}}{1.1},                    just= {\TRule{\False}{\Diamond}[4]}, close]]                [\pFmla{\True}{\formula{B}}{1.1},                  just = {\TRule{\True}{\lor}[6]}                  [\pFmla{\False}{\formula{B}}{1.1},                    just= {\TRule{\False}{\Diamond}[5]}, close]]              ]            ]          ]        ]      ]    ]  \end{oltableau}\end{ex}}{}\begin{prob}  Find closed !!{tableau}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)$    \item $\Box(p \land q) \lif \Box p$  \end{enumerate}\end{prob}\end{document}

content/normal-modal-logic/tableaux/soundness.tex

% Part: normal-modal-logic% Chapter: tableaux% Section: soundness\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{tab}{sou}\olsection{Soundness for \Log{K}}\begin{editorial}  This soundness proof reuses the soundness proof for classical  propositional logic, i.e., it proves everything from scratch. That's  ok if you want a self-contained soundness proof. If you already have  seen soundness for ordinary tableau this will be repetitive. It's  planned to make it possible to switch between self-contained version  and a version building on the non-modal case.\end{editorial}\begin{explain}  In order to show that prefixed !!{tableau}s are sound, we have to  show that if  \[  \sFmla{\True}{!B_1}[1], \dots, \sFmla{\True}{!B_n}[1], \sFmla{\False}{!A}[1]  \]  has a closed !!{tableau} then $!B_1, \dots, !B_n \Entails !A$. It is  easier to prove the contrapositive: if for some $\mModel{M}$ and  world~$w$, $\mSat{M}{!B_i}[w]$ for all $i=1$, \dots,~$n$ but  $\mSat{M}{!A}[w]$, then no !!{tableau} can close. Such a  countermodel shows that the initial assumptions of the !!{tableau}  are satisfiable. The strategy of the proof is to show that whenever  all the prefixed !!{formula}s on !!a{tableau} branch are  satisfiable, any application of a rule results in at least one  extended branch that is also satisfiable. Since closed branches are  unsatisfiable, any !!{tableau} for a satisfiable set of prefixed  !!{formula}s must have at least one open branch.  In order to apply this strategy in the modal case, we have to extend  our definition of ``satisfiable'' to modal modals and prefixes. With  that in hand, however, the proof is straightforward.\end{explain}\begin{defn}  Let $P$ be some set of prefixes, i.e., $P \subseteq (\PosInt)^*  \setminus \{\emptyseq\}$ and let $\mModel{M}$ be a model.  A  function~$f\colon P \to W$ is an \emph{interpretation of}~$P$  in~$\mModel{M}$ if, whenever $\sigma$ and $\sigma.n$ are both  in~$P$, then $Rf(\sigma)f(\sigma.n)$.  Relative to an interpretation of prefixes~$P$ we can define:  \begin{enumerate}  \item $\mModel{M}$ satisfies $\sFmla{\True}{!A}[\sigma]$ iff    $\mSat{M}{!A}[f(\sigma)]$.  \item $\mModel{M}$ satisfies $\sFmla{\False}{!A}[\sigma]$ iff    $\mSat/{M}{!A}[f(\sigma)]$.  \end{enumerate}\end{defn}\begin{defn}  Let $\Gamma$ be a set of prefixed !!{formula}s, and let $P(\Gamma)$  be the set of prefixes that occur in it. If $f$ is an interpretation  of~$P(\Gamma)$ in $\mModel{M}$, we say that $\mModel{M}$ satisfies  $\Gamma$ with respect to~$f$, $\mSat{M}{\Gamma}[f]$, if $\mModel{M}$  satisfies every prefixed !!{formula} in~$\Gamma$ with respect  to~$f$. $\Gamma$ is \emph{satisfiable} iff there is a  model~$\mModel{M}$ and interpretation~$f$ of $P(\Gamma)$ such that  $\mSat{M}{\Gamma}[f]$.\end{defn}\begin{prop}  If $\Gamma$ contains both $\sFmla{\True}{!A}[\sigma]$ and  $\sFmla{\False}{!A}[\sigma]$, for some !!{formula}~$!A$ and  prefix~$\sigma$, then $\Gamma$ is unsatisfiable.\end{prop}\begin{proof}  There cannot be a model~$\mModel{M}$ and interpretation~$f$ of  $P(\Gamma)$ such that both $\mSat{M}{!A}[f(\sigma)]$ and  $\mSat/{M}{!A}[f(\sigma)]$.\end{proof}\begin{thm}[Soundness]  \ollabel{thm:tableau-soundness}  If $\Gamma$ has a closed !!{tableau}, $\Gamma$ is unsatisfiable.\end{thm}\begin{proof}We call a branch of !!a{tableau} satisfiable iff the set of!!{signed formula}s on it is satisfiable, and let's call !!a{tableau}satisfiable if it contains at least one satisfiable branch.We show the following: Extending a satisfiable !!{tableau} by one ofthe rules of inference always results in a satisfiable !!{tableau}.This will prove the theorem: any closed !!{tableau} results byapplying rules of inference to the !!{tableau} consisting only ofassumptions from~$\Gamma$. So if $\Gamma$ were satisfiable, any!!{tableau} for it would be satisfiable. A closed !!{tableau},however, is clearly not satisfiable, since all its branches are closedand closed branches are unsatisfiable.Suppose we have a satisfiable !!{tableau}, i.e., !!a{tableau} with atleast one satisfiable branch. Applying a rule of inference either adds!!{signed formula}s to a branch, or splits a branch in two. If the!!{tableau} has a satisfiable branch which is not extended by the ruleapplication in question, it remains a satisfiable branch in theextended !!{tableau}, so the extended tableau is satisfiable. So weonly have to consider the case where a rule is applied to asatisfiable branch.Let $\Gamma$ be the set of !!{signed formula}s on that branch, and let$\sFmla{S}{!A}[\sigma] \in \Gamma$ be the !!{signed formula} to whichthe rule is applied. If the rule does not result in a split branch, wehave to show that the extended branch, i.e., $\Gamma$ together withthe conclusions of the rule, is still satisfiable. If the rule resultsin split branch, we have to show that at least one of the tworesulting branches is satisfiable.\tagfalse{prvDiamond}First, we consider the possible inferences with only one premise.\begin{enumerate}\item The branch is expanded by applying $\TRule{\True}{\lnot}$ to  $\sFmla{\True}{\lnot !B}[\sigma] \in \Gamma$. Then the extended  branch contains the !!{signed formula}s $\Gamma \cup  \{\sFmla{\False}{!B}[\sigma]\}$.  Suppose $\mSat{M}{\Gamma}[f]$. In  particular, $\mSat{M}{\lnot !B}[f(\sigma)]$. Thus,  $\mSat/{M}{!B}[f(\sigma)]$, i.e., $\mModel{M}$ satisfies  $\sFmla{\False}{!B}[\sigma]$ with respect to~$f$.\item The branch is expanded by applying $\TRule{\False}{\lnot}$ to  $\sFmla{\False}{\lnot !B}[\sigma] \in \Gamma$: Exercise.\item The branch is expanded by applying $\TRule{\True}{\land}$ to  $\sFmla{\True}{!B \land !C}[\sigma] \in \Gamma$, which results in  two new !!{signed formula}s on the branch:  $\sFmla{\True}{!B}[\sigma]$ and $\sFmla{\True}{!C}[\sigma]$. Suppose  $\mSat{M}{\Gamma}[f]$, in particular $\mSat{M}{!B \land    !C}[f(\sigma)]$. Then $\mSat{M}{!B}[f(\sigma)]$ and  $\mSat{M}{!C}[f(\sigma)]$. This means that $\mModel{M}$ satisfies  both $\sFmla{\True}{!B}[\sigma]$ and $\sFmla{\True}{!C}[\sigma]$  with respect to~$f$.\item The branch is expanded by applying $\TRule{\False}{\lor}$ to  $\sFmla{\False}{!B \lor !C} \in \Gamma$: Exercise.\item The branch is expanded by applying $\TRule{\False}{\lif}$ to  $\sFmla{\False}{!B \lif !C}[\sigma] \in \Gamma$: This results in two  new !!{signed formula}s on the branch: $\sFmla{\True}{!B}[\sigma]$ and  $\sFmla{\False}{!C}[\sigma]$. Suppose  $\mSat{M}{\Gamma}[f]$, in particular  $\mSat/{M}{!B \lif !C}[f(\sigma)]$. Then  $\mSat{M}{!B}[f(\sigma)]$ and  $\mSat/{M}{!C}[f(\sigma)]$. This means that  $\mModel{M}, f$ satisfies both  $\sFmla{\True}{!B}[\sigma]$ and $\sFmla{\False}{!C}[\sigma]$.\iftag{prvBox}{%\item The branch is expanded by applying $\TRule{\True}{\Box}$ to  $\sFmla{\True}{\Box !B}[\sigma] \in \Gamma$:  \iftag{probBox}{Exercise.}{This results in a new !!{signed      formula}~$\sFmla{\True}{!B}[\sigma.n]$ on the branch, for some    $\sigma.n \in P(\Gamma)$ (since $\sigma.n$ must be used).  Suppose    $\mSat{M}{\Gamma}[f]$, in particular, $\mSat{M}{\Box      !B}[f(\sigma)]$. Since $f$ is an interpretation of prefixes and    both $\sigma$, $\sigma.n \in P(\Gamma)$, we know that    $Rf(\sigma)f(\sigma.n)$.  Hence, $\mSat{M}{!B}[f(\sigma.n)]$,    i.e., $\mModel{M}, f$ satisfies $\sFmla{\True}{!B}[\sigma.n]$.}\item The branch is expanded by applying $\TRule{\False}{\Box}$ to  $\sFmla{\False}{\Box !B}[\sigma] \in \Gamma$:  \iftag{probBox}{Exercise.}{This results in a new !!{signed      formula}~$\sFmla{\False}{!A}[\sigma.n]$, where $\sigma.n$ is a    new prefix on the branch, i.e., $\sigma.n \notin P(\Gamma)$.    Since $\Gamma$ is satisfiable, there is a $\Struct{M}$ and    interpretation~$f$ of $P(\Gamma)$ such that $\Sat{M}{\Gamma}[f]$,    in particular $\mSat/{M}{\Box !B}[f(\sigma)]$. We have to show    that $\Gamma \cup \{\sFmla{\False}{!B}[\sigma.n]\}$ is    satisfiable. To do this, we define an interpretation of $P(\Gamma)    \cup \{\sigma.n\}$ as follows:  Since $\mSat/{M}{\Box !B}[f(\sigma)]$, there is a $w \in W$ such that  $Rf(\sigma)w$ and $\mSat/{M}{!B}[w]$. Let $f'$ be like $f$, except  that $f'(\sigma.n) = w$. Since $f'(\sigma) = f(\sigma)$ and  $Rf(\sigma)w$, we have $Rf'(\sigma)f'(\sigma.n)$, so $f'$ is an  interpretation of $P(\Gamma) \cup \{\sigma.n\}$.  Obviously  $\mSat/{M}{!B}[f'(\sigma.n)]$. Since $f(\sigma') = f'(\sigma')$ for  all prefixes $\sigma' \in P(\Gamma)$, $\mSat{M}{\Gamma}[f']$.  So,  $\mModel{M}, f'$ satisfies $\Gamma \cup  \{\sFmla{\False}{!B}[\sigma.n]\}$.}  }{}\iftag{prvDiamond}{%\item The branch is expanded by applying $\TRule{\True}{\Diamond}$ to  $\sFmla{\True}{\Diamond !B}[\sigma] \in \Gamma$:  \iftag{probDiamond}{Exercise.}{This results in a new !!{signed      formula}~$\sFmla{\True}{!A}[\sigma.n]$, where $\sigma.n$ is a    new prefix on the branch, i.e., $\sigma.n \notin P(\Gamma)$.    Since $\Gamma$ is satisfiable, there is a $\Struct{M}$ and    interpretation~$f$ of $P(\Gamma)$ such that $\Sat{M}{\Gamma}[f]$,    in particular $\mSat{M}{\Diamond !B}[f(\sigma)]$. We have to show    that $\Gamma \cup \{\sFmla{\True}{!B}[\sigma.n]\}$ is    satisfiable. To do this, we define an interpretation of $P(\Gamma)    \cup \{\sigma.n\}$ as follows:  Since $\mSat{M}{\Diamond !B}[f(\sigma)]$, there is a $w \in W$ such that  $Rf(\sigma)w$ and $\mSat{M}{!B}[w]$. Let $f'$ be like $f$, except  that $f'(\sigma.n) = w$. Since $f'(\sigma) = f(\sigma)$ and  $Rf(\sigma)w$, we have $Rf'(\sigma)f'(\sigma.n)$, so $f'$ is an  interpretation of $P(\Gamma) \cup \{\sigma.n\}$.  Obviously  $\mSat{M}{!B}[f'(\sigma.n)]$. Since $f(\sigma') = f'(\sigma')$ for  all prefixes $\sigma' \in P(\Gamma)$, $\mSat{M}{\Gamma}[f']$.  So,  $\mModel{M}, f'$ satisfies $\Gamma \cup  \{\sFmla{\True}{!B}[\sigma.n]\}$.}\item The branch is expanded by applying $\TRule{\False}{\Diamond}$ to  $\sFmla{\False}{\Diamond !B}[\sigma] \in \Gamma$:  \iftag{probDiamond}{Exercise.}{This results in a new !!{signed      formula}~$\sFmla{\False}{!B}[\sigma.n]$ on the branch, for some    $\sigma.n \in P(\Gamma)$ (since $\sigma.n$ must be used).  Suppose    $\mSat{M}{\Gamma}[f]$, in particular, $\mSat/{M}{\Diamond      !B}[f(\sigma)]$. Since $f$ is an interpretation of prefixes and    both $\sigma$, $\sigma.n \in P(\Gamma)$, we know that    $Rf(\sigma)f(\sigma.n)$.  Hence, $\mSat/{M}{!B}[f(\sigma.n)]$,    i.e., $\mModel{M}, f$ satisfies $\sFmla{\False}{!B}[\sigma.n]$.}  }{}\end{enumerate}Now let's consider the possible inferences with two premises.\begin{enumerate}\item The branch is expanded by applying $\TRule{\False}{\land}$ to  $\sFmla{\False}{!B \land !C}[\sigma] \in \Gamma$, which results in  two branches, a left one continuing through  $\sFmla{\False}{!B}[\sigma]$ and a right one through  $\sFmla{\False}{!C}[\sigma]$. Suppose $\mSat{M}{\Gamma}[f]$, in  particular $\mSat/{M}{!B \land !C}[f(\sigma)]$.  Then  $\mSat/{M}{!B}[f(\sigma)]$ or $\mSat/{M}{!C}[f(\sigma)]$. In the  former case, $\mModel{M}, f$ satisfies $\sFmla{\False}{!B}[\sigma]$,  i.e., the left branch is satisfiable. In the latter, $\mModel{M}, f$  satisfies $\sFmla{\False}{!C}[\sigma]$, i.e., the right branch is  satisfiable.\item The branch is expanded by applying $\TRule{\True}{\lor}$ to    $\sFmla{\True}{!B \lor !C}[\sigma] \in \Gamma$: Exercise.\item The branch is expanded by applying $\TRule{\True}{\lif}$ to    $\sFmla{\True}{!B \lif !C}[\sigma] \in \Gamma$: Exercise.\end{enumerate}\end{proof}\begin{prob}Complete the proof of \olref[nml][tab][sou]{thm:tableau-soundness}.\end{prob}\begin{cor}\ollabel{cor:entailment-soundness}If $\Gamma \Proves !A$ then $\Gamma \Entails !A$.\end{cor}\begin{proof}  If $\Gamma \Proves !A$ then for some $!B_1$, \dots, $!B_n \in  \Gamma$, $\Delta = \{\sFmla{\False}{!A}[1], \sFmla{\True}{!B_1}[1],  \dots, \sFmla{\True}{!B_n}[1]\}$ has a closed !!{tableau}. We want  to show that $\Gamma \Entails !A$. Suppose not, so for some  $\mModel{M}$ and $w$, $\mSat{M}{!B_i}[w]$ for $i=1$, \dots,~$n$, but  $\mSat/{M}{!A}[w]$. Let $f(1) = w$; then $f$ is an interpretation  of~$P(\Delta)$ into~$\mModel{M}$, and $\mModel{M}$ satisfies~$\Delta$ with  respect to~$f$. But by \olref{thm:tableau-soundness}, $\Delta$ is  unsatisfiable since it has a closed !!{tableau}, a  contradiction. So we must have $\Gamma \Proves !A$ after all.\end{proof}\begin{cor}\ollabel{cor:weak-soundness}If $\Proves !A$ then $!A$ is true in all models.\end{cor}\end{document}

content/normal-modal-logic/tableaux/more-rules.tex

% Part: normal-modal-logic% Chapter: tableaux% Section: more-rules\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{tab}{mru}\olsection{Rules for Other Accessibility Relations}In order to deal with logics determined by special accessibilityrelations, we consider the additional rules in \olref{tab:more-rules}.\begin{table}  \begin{center}    \def\arraystretch{3}\def\fCenter{}    \iftag{notprvBox,notprvDiamond}          {\begin{tabular}{|c|}}          {\begin{tabular}{|c|c|}}    \hline    \iftag{prvBox}{      \AxiomC{\sFmla{\True}{\Box !A}[\sigma]}      \RightLabel{T$\Box$}      \UnaryInfC{\sFmla{\True}{!A}[\sigma]}      \DisplayProof}{}    \iftag{notprvBox,notprvDiamond}{}{&}    \iftag{prvDiamond}{      \AxiomC{\sFmla{\False}{\Diamond !A}[\sigma]}      \RightLabel{T$\Diamond$}      \UnaryInfC{\sFmla{\False}{!A}[\sigma]}      \DisplayProof}{}    \\[1ex]    \hline    \iftag{prvBox}{      \AxiomC{\sFmla{\True}{\Box !A}[\sigma]}      \RightLabel{D$\Box$}      \UnaryInfC{\sFmla{\True}{\Diamond!A}[\sigma]}      \DisplayProof}{}    \iftag{notprvBox,notprvDiamond}{}{&}    \iftag{prvDiamond}{      \AxiomC{\sFmla{\False}{\Diamond !A}[\sigma]}      \RightLabel{D$\Diamond$}      \UnaryInfC{\sFmla{\False}{\Box!A}[\sigma]}      \DisplayProof}{}    \\[1ex]    \hline    \iftag{prvBox}{      \AxiomC{\sFmla{\True}{\Box !A}[\sigma.n]}      \RightLabel{B$\Box$}      \UnaryInfC{\sFmla{\True}{!A}[\sigma]}      \DisplayProof}{}    \iftag{notprvBox,notprvDiamond}{}{&}    \iftag{prvDiamond}{      \AxiomC{\sFmla{\False}{\Diamond !A}[\sigma.n]}      \RightLabel{B$\Diamond$}      \UnaryInfC{\sFmla{\False}{!A}[\sigma]}      \DisplayProof}{}    \\[1ex]    \hline    \iftag{prvBox}{      \AxiomC{\sFmla{\True}{\Box !A}[\sigma]}      \RightLabel{4$\Box$}      \UnaryInfC{\sFmla{\True}{\Box!A}[\sigma.n]}      \DisplayProof}{}    \iftag{notprvBox,notprvDiamond}{}{&}    \iftag{prvDiamond}{      \AxiomC{\sFmla{\False}{\Diamond !A}[\sigma]}      \RightLabel{4$\Diamond$}      \UnaryInfC{\sFmla{\False}{\Diamond!A}[\sigma.n]}      \DisplayProof}{}    \\    \iftag{notprvBox,notprvDiamond}         {$\sigma.n$ is used}         {$\sigma.n$ is used & $\sigma.n$ is used}    \\[1ex]    \hline    \iftag{prvBox}{      \AxiomC{\sFmla{\True}{\Box !A}[\sigma.n]}      \RightLabel{4r$\Box$}      \UnaryInfC{\sFmla{\True}{\Box!A}[\sigma]}      \DisplayProof}{}    \iftag{notprvBox,notprvDiamond}{}{&}    \iftag{prvDiamond}{      \AxiomC{\sFmla{\False}{\Diamond !A}[\sigma.n]}      \RightLabel{4r$\Diamond$}      \UnaryInfC{\sFmla{\False}{\Diamond!A}[\sigma]}      \DisplayProof}{}    \\[1ex]    \hline    \end{tabular}  \end{center}  \caption{More modal rules.}  \ollabel{tab:more-rules}\end{table}Adding these rules results in systems that are sound and complete forthe logics given in \olref{tab:logics-rules}.\begin{table}  \begin{center}    \begin{tabular}{lll}      \hline      Logic & $R$ is \dots & Rules\\      \hline      $\Log{T} = \Log{KT}$ & reflexive &      \iftag{prvBox}{T$\Box$}{}%      \iftag{notprvBox,notprvDiamond}{}{, }%      \iftag{prvDiamond}{T$\Diamond$}{}      \\ \hline      $\Log{D} = \Log{KD}$ & serial &      \iftag{prvBox}{D$\Box$}{}%      \iftag{notprvBox,notprvDiamond}{}{, }%      \iftag{prvDiamond}{D$\Diamond$}{}      \\ \hline      $\Log{K4}$ & transitive &      \iftag{prvBox}{4$\Box$}{}%      \iftag{notprvBox,notprvDiamond}{}{, }%      \iftag{prvDiamond}{4$\Diamond$}{}      \\ \hline      $\Log{B} = \Log{KTB}$ & reflexive, &      \iftag{prvBox}{T$\Box$}{}%      \iftag{notprvBox,notprvDiamond}{}{, }%      \iftag{prvDiamond}{T$\Diamond$}{}\\      & symmetric &      \iftag{prvBox}{B$\Box$}{}%      \iftag{notprvBox,notprvDiamond}{}{, }%      \iftag{prvDiamond}{B$\Diamond$}{}      \\ \hline      $\Log{S4} = \Log{KT4}$ & reflexive, &      \iftag{prvBox}{T$\Box$}{}%      \iftag{notprvBox,notprvDiamond}{}{, }%      \iftag{prvDiamond}{T$\Diamond$}{},\\      & transitive &      \iftag{prvBox}{4$\Box$}{}%      \iftag{notprvBox,notprvDiamond}{}{, }%      \iftag{prvDiamond}{4$\Diamond$}{}      \\ \hline      $\Log{S5} = \Log{KT4B}$ & reflexive, &      \iftag{prvBox}{T$\Box$}{}%      \iftag{notprvBox,notprvDiamond}{}{, }%      \iftag{prvDiamond}{T$\Diamond$}{},\\      & transitive, &      \iftag{prvBox}{4$\Box$}{}%      \iftag{notprvBox,notprvDiamond}{}{, }%      \iftag{prvDiamond}{4$\Diamond$}{},\\      &  euclidean &      \iftag{prvBox}{4r$\Box$}{}%      \iftag{notprvBox,notprvDiamond}{}{, }%      \iftag{prvDiamond}{4r$\Diamond$}{}      \\ \hline    \end{tabular}  \end{center}  \caption{!!^{tableau} rules for various modal logics.}  \ollabel{tab:logics-rules}\end{table}\begin{ex}  We give a closed tableau that shows $\Log{S5} \Proves \Ax{5}$, i.e.,  $\Box!A \lif \Box\Diamond!A$.  \begin{oltableau}    [\pFmla{\False}{\Box\formula{A} \lif \Box\Diamond \formula{A}}{1},      just = \TAss      [\pFmla{\True}{\Box \formula{A}}{1}, just = {\TRule{\False}{\lif}[1]}        [\pFmla{\False}{\Box\Diamond \formula{A}}{1},          just = {\TRule{\False}{\lif}[1]}          [\pFmla{\False}{\Diamond \formula{A}}{1.1},            just = {\TRule{\False}{\Box}[3]}            [\pFmla{\False}{\Diamond \formula{A}}{1},              just = {4r$\Diamond$ 4}              [\pFmla{\False}{\formula{A}}{1.1},                just = {\TRule{\False}{\Diamond}[5]}                [\pFmla{\True}{\formula{A}}{1.1},                  just = {\TRule{\True}{\Box}[2]}, close]              ]            ]          ]        ]      ]    ]  \end{oltableau}\end{ex}\begin{prob}Give closed !!{tableau}s that show the following:  \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 $\Log{KT} \Proves \Ax{D}$.  \end{enumerate}\end{prob}\end{document}

content/normal-modal-logic/tableaux/more-soundness.tex

% Part: normal-modal-logic% Chapter: tableaux% Section: more-soundness\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{tab}{msn}      \olsection{Soundness for Additional Rules}We say a rule is sound for a class of models if, whenever a branch in!!a{tableau} is satisfiable in a model from that class, the branchresulting from applying the rule is also satisfiable in a model fromthat class.\begin{prop}  \ollabel{prop:soundness-T}   \iftag{prvBox}{\Ax{T}$\Box$}{}%  \iftag{notprvBox,notprvDiamond}{}{ and }%  \iftag{prvDiamond}{\Ax{T}$\Diamond$}{}  \iftag{notprvBox,notprvDiamond}{is}{are}  sound for reflexive models.\end{prop}\begin{proof}\begin{tagenumerate}{prvBox,prvDiamond}\tagitem{prvBox}{The branch is expanded by applying T$\Box$ to  $\sFmla{\True}{\Box !B}[\sigma] \in \Gamma$:  \iftag{probBox}{Exercise.}{This results in a new !!{signed      formula}~$\sFmla{\True}{!B}[\sigma]$ on the branch. Suppose    $\mSat{M}{\Gamma}[f]$, in particular, $\mSat{M}{\Box      !B}[f(\sigma)]$. Since $R$ is reflexive, we know that    $Rf(\sigma)f(\sigma)$.  Hence, $\mSat{M}{!B}[f(\sigma)]$, i.e.,    $\mModel{M}, f$ satisfies $\sFmla{\True}{!B}[\sigma]$.}}{}\tagitem{prvDiamond}{The branch is expanded by applying T$\Diamond$ to  $\sFmla{\False}{\Diamond !B}[\sigma] \in \Gamma$:  \iftag{probDiamond}{Exercise.}{This results in a new !!{signed      formula}~$\sFmla{\False}{!B}[\sigma]$ on the branch. Suppose    $\mSat{M}{\Gamma}[f]$, in particular, $\mSat/{M}{\Diamond      !B}[f(\sigma)]$. Since $R$ is reflexive, we know that    $Rf(\sigma)f(\sigma)$.  Hence, $\mSat/{M}{!B}[f(\sigma)]$, i.e.,    $\mModel{M}, f$ satisfies $\sFmla{\False}{!B}[\sigma]$.}}{}\end{tagenumerate}\end{proof}\tagprob{probBox,probDiamond}\begin{prob}  Complete the proof of \olref[nml][tab][msn]{prop:soundness-T}\end{prob}\tagendprob\begin{prop}  \ollabel{prop:soundness-D}   \iftag{prvBox}{\Ax{D}$\Box$}{}%  \iftag{notprvBox,notprvDiamond}{}{ and }%  \iftag{prvDiamond}{\Ax{D}$\Diamond$}{}  \iftag{notprvBox,notprvDiamond}{is}{are}  sound for serial models.\end{prop}\begin{proof}\begin{tagenumerate}{prvBox,prvDiamond}\tagitem{prvBox}{The branch is expanded by applying D$\Box$ to  $\sFmla{\True}{\Box !B}[\sigma] \in \Gamma$:  \iftag{probBox}{Exercise.}{This results in a new !!{signed      formula}~$\sFmla{\True}{\Diamond !B}[\sigma]$ on the    branch. Suppose $\mSat{M}{\Gamma}[f]$, in particular,    $\mSat{M}{\Box !B}[f(\sigma)]$. Since $R$ is serial, there is a $w    \in W$ such that $Rf(\sigma)w$. Then $\mSat{M}{!B}[w]$, and hence    $\mSat{M}{\Diamond !B}[f(\sigma)]$.  So, $\mModel{M}, f$    satisfies $\sFmla{\True}{\Diamond!B}[\sigma]$.}}{}\tagitem{prvDiamond}{The branch is expanded by applying D$\Diamond$ to  $\sFmla{\False}{\Diamond !B}[\sigma] \in \Gamma$:  \iftag{probDiamond}{Exercise.}{This results in a new !!{signed      formula}~$\sFmla{\False}{\Box !B}[\sigma]$ on the    branch. Suppose $\mSat{M}{\Gamma}[f]$, in particular,    $\mSat/{M}{\Diamond !B}[f(\sigma)]$. Since $R$ is serial, there is a $w    \in W$ such that $Rf(\sigma)w$. Then $\mSat/{M}{!B}[w]$, and hence    $\mSat/{M}{\Box !B}[f(\sigma)]$.  So, $\mModel{M}, f$    satisfies $\sFmla{\False}{\Box!B}[\sigma]$.}}{}\end{tagenumerate}\end{proof}\tagprob{probBox,probDiamond}\begin{prob}  Complete the proof of \olref[nml][tab][msn]{prop:soundness-D}\end{prob}\tagendprob\begin{prop}  \ollabel{prop:soundness-B}   \iftag{prvBox}{\Ax{B}$\Box$}{}%  \iftag{notprvBox,notprvDiamond}{}{ and }%  \iftag{prvDiamond}{\Ax{B}$\Diamond$}{}  \iftag{notprvBox,notprvDiamond}{is}{are}  sound for symmetric models.\end{prop}\begin{proof}\begin{tagenumerate}{prvBox,prvDiamond}\tagitem{prvBox}{The branch is expanded by applying B$\Box$ to  $\sFmla{\True}{\Box !B}[\sigma.n] \in \Gamma$:  \iftag{probBox}{Exercise.}{This results in a new !!{signed      formula}~$\sFmla{\True}{!B}[\sigma]$ on the branch. Suppose    $\mSat{M}{\Gamma}[f]$, in particular, $\mSat{M}{\Box      !B}[f(\sigma.n)]$. Since $f$ is an interpretation of prefixes on    the branch into~$\mModel{M}$, we know that    $Rf(\sigma)f(\sigma.n)$.  Since $R$ is symmetric,    $Rf(\sigma.n)f(\sigma)$.  Since $\mSat{M}{\Box !B}[f(\sigma.n)]$,    $\mSat{M}{!B}[f(\sigma)]$. Hence, $\mModel{M}, f$ satisfies    $\sFmla{\True}{!B}[\sigma]$.}}{}\tagitem{prvDiamond}{The branch is expanded by applying B$\Diamond$ to  $\sFmla{\False}{\Diamond !B}[\sigma.n] \in \Gamma$:  \iftag{probDiamond}{Exercise.}{This results in a new !!{signed      formula}~$\sFmla{\False}{!B}[\sigma]$ on the branch. Suppose    $\mSat{M}{\Gamma}[f]$, in particular, $\mSat/{M}{\Diamond      !B}[f(\sigma.n)]$. Since $f$ is an interpretation of prefixes on    the branch into~$\mModel{M}$, we know that    $Rf(\sigma)f(\sigma.n)$.  Since $R$ is symmetric,    $Rf(\sigma.n)f(\sigma)$.  Since $\mSat/{M}{\Diamond !B}[f(\sigma.n)]$,    $\mSat/{M}{!B}[f(\sigma)]$. Hence, $\mModel{M}, f$ satisfies    $\sFmla{\False}{!B}[\sigma]$.}}{}\end{tagenumerate}\end{proof}\tagprob{probBox,probDiamond}\begin{prob}  Complete the proof of \olref[nml][tab][msn]{prop:soundness-B}\end{prob}\tagendprob\begin{prop}  \ollabel{prop:soundness-4}   \iftag{prvBox}{\Ax{4}$\Box$}{}%  \iftag{notprvBox,notprvDiamond}{}{ and }%  \iftag{prvDiamond}{\Ax{4}$\Diamond$}{}  \iftag{notprvBox,notprvDiamond}{is}{are}  sound for transitive models.\end{prop}\begin{proof}\begin{tagenumerate}{prvBox,prvDiamond}\tagitem{prvBox}{The branch is expanded by applying 4$\Box$ to  $\sFmla{\True}{\Box !B}[\sigma] \in \Gamma$:  \iftag{probBox}{Exercise.}{This results in a new !!{signed      formula}~$\sFmla{\True}{\Box!B}[\sigma.n]$ on the    branch. Suppose $\mSat{M}{\Gamma}[f]$, in particular,    $\mSat{M}{\Box !B}[f(\sigma)]$. Since $f$ is an interpretation of    prefixes on the branch into~$\mModel{M}$ and $\sigma.n$ must be    used, we know that $Rf(\sigma)f(\sigma.n)$. Now let $w$ be any    world such that $Rf(\sigma.n)w$.  Since $R$ is transitive,    $Rf(\sigma)w$.  Since $\mSat{M}{\Box !B}[f(\sigma)]$,    $\mSat{M}{!B}[w]$. Hence, $\mSat{M}{\Box !B}[f(\sigma.n)]$, and    $\mModel{M}, f$ satisfies $\sFmla{\True}{\Box !B}[\sigma.n]$.}}{}\tagitem{prvDiamond}{The branch is expanded by applying 4$\Diamond$ to  $\sFmla{\False}{\Diamond !B}[\sigma] \in \Gamma$:  \iftag{probDiamond}{Exercise.}{This results in a new !!{signed      formula}~$\sFmla{\False}{\Diamond!B}[\sigma.n]$ on the    branch. Suppose $\mSat{M}{\Gamma}[f]$, in particular,    $\mSat/{M}{\Diamond !B}[f(\sigma)]$. Since $f$ is an interpretation of    prefixes on the branch into~$\mModel{M}$ and $\sigma.n$ must be    used, we know that $Rf(\sigma)f(\sigma.n)$. Now let $w$ be any    world such that $Rf(\sigma.n)w$.  Since $R$ is transitive,    $Rf(\sigma)w$.  Since $\mSat/{M}{\Diamond !B}[f(\sigma)]$,    $\mSat/{M}{!B}[w]$. Hence, $\mSat/{M}{\Diamond !B}[f(\sigma.n)]$, and    $\mModel{M}, f$ satisfies $\sFmla{\False}{\Diamond !B}[\sigma.n]$.}}{}\end{tagenumerate}\end{proof}\tagprob{probBox,probDiamond}\begin{prob}  Complete the proof of \olref[nml][tab][msn]{prop:soundness-4}\end{prob}\tagendprob\begin{prop}  \ollabel{prop:soundness-4r}   \iftag{prvBox}{\Ax{4r}$\Box$}{}%  \iftag{notprvBox,notprvDiamond}{}{ and }%  \iftag{prvDiamond}{\Ax{4r}$\Diamond$}{}  \iftag{notprvBox,notprvDiamond}{is}{are}  sound for euclidean models.\end{prop}\begin{proof}\begin{tagenumerate}{prvBox,prvDiamond}\tagitem{prvBox}{The branch is expanded by applying 4r$\Box$ to  $\sFmla{\True}{\Box !B}[\sigma.n] \in \Gamma$:  \iftag{probBox}{Exercise.}{This results in a new !!{signed      formula}~$\sFmla{\True}{\Box!B}[\sigma]$ on the branch. Suppose    $\mSat{M}{\Gamma}[f]$, in particular, $\mSat{M}{\Box      !B}[f(\sigma.n)]$. Since $f$ is an interpretation of prefixes on    the branch into~$\mModel{M}$, we know that    $Rf(\sigma)f(\sigma.n)$. Now let $w$ be any world such that    $Rf(\sigma)w$.  Since $R$ is euclidean, $Rf(\sigma.n)w$.  Since    $\mSat{M}{\Box !B}[f(\sigma).n]$, $\mSat{M}{!B}[w]$. Hence,    $\mSat{M}{\Box !B}[f(\sigma)]$, and $\mModel{M}, f$ satisfies    $\sFmla{\True}{\Box !B}[\sigma]$.}}{}\tagitem{prvDiamond}{The branch is expanded by applying 4r$\Diamond$ to  $\sFmla{\False}{\Diamond !B}[\sigma.n] \in \Gamma$:  \iftag{probDiamond}{Exercise.}{This results in a new !!{signed      formula}~$\sFmla{\True}{\Box!B}[\sigma]$ on the branch. Suppose    $\mSat{M}{\Gamma}[f]$, in particular, $\mSat/{M}{\Diamond      !B}[f(\sigma.n)]$. Since $f$ is an interpretation of prefixes on    the branch into~$\mModel{M}$, we know that    $Rf(\sigma)f(\sigma.n)$. Now let $w$ be any world such that    $Rf(\sigma)w$.  Since $R$ is euclidean, $Rf(\sigma.n)w$.  Since    $\mSat/{M}{\Diamond !B}[f(\sigma).n]$, $\mSat/{M}{!B}[w]$. Hence,    $\mSat/{M}{\Diamond !B}[f(\sigma)]$, and $\mModel{M}, f$ satisfies    $\sFmla{\False}{\Diamond !B}[\sigma]$.}}{}\end{tagenumerate}\end{proof}\tagprob{probBox,probDiamond}\begin{prob}  Complete the proof of \olref[nml][tab][msn]{prop:soundness-4r}\end{prob}\tagendprob\begin{cor}\ollabel{cor:soundness-logics} The !!{tableau} systems given in\olref[mru]{tab:logics-rules} are sound for the respective classes ofmodels.\end{cor}\end{document}

content/normal-modal-logic/tableaux/simple-S5.tex

% Part: normal-modal-logic% Chapter: tableaux% Section: simple-S5\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{tab}{s5}\olsection{Simple \usetoken{P}{tableau} for \Log{S5}}\Log{S5} is sound and complete with respect to the class of universalmodels, i.e., models where every world is accessible from everyworld. In universal models the accessibility relation doesn't matter:``there is a world~$w$ where $\mSat{M}{!A}[w]$'' is true if and onlyif there is such a $w$ that's accessible from~$u$. So in \Log{S5}, wecan define models as simply a set of worlds and a valuation~$V$. Thissuggests that we should be able to simplify the !!{tableau} rules aswell. In the general case, we take as prefixes sequences of positiveintegers, so that we can keep track of which such prefixes name worldswhich are accessible from others: $\sigma.n$ names a world accessiblefrom~$\sigma$. But in \Log{S5} any world is accessible from any world,so there is no need to so keep track. Instead, we can use positiveintegers as prefixes. The simplified rules are given in\olref{tab:rules-S5}.\begin{table}  \begin{center}    \def\arraystretch{3}\def\fCenter{}    \begin{tabular}{|c|c|}    \hline    \iftag{prvBox}{      \AxiomC{\sFmla{\True}{\Box !A}[n]}      \RightLabel{\TRule{\True}{\Box}}      \UnaryInfC{\sFmla{\True}{!A}[m]}      \DisplayProof      &      \AxiomC{\sFmla{\False}{\Box !A}[n]}      \RightLabel{\TRule{\False}{\Box}}      \UnaryInfC{\sFmla{\False}{!A}[m]}      \DisplayProof\\      $m$ is used & $m$ is new      \\[1ex]      \hline}{}    \iftag{prvDiamond}{      \AxiomC{\sFmla{\True}{\Diamond !A}[n]}      \RightLabel{\TRule{\True}{\Diamond}}      \UnaryInfC{\sFmla{\True}{!A}[m]}      \DisplayProof      &      \AxiomC{\sFmla{\False}{\Diamond !A}[n]}      \RightLabel{\TRule{\False}{\Diamond}}      \UnaryInfC{\sFmla{\False}{!A}[m]}      \DisplayProof\\      $m$ is new & $m$ is used      \\[1ex]      \hline}{}    \end{tabular}  \end{center}  \caption{Simplified rules for \Log{S5}.}  \ollabel{tab:rules-S5}\end{table}\begin{ex}  We give a simplified closed tableau that shows $\Log{S5} \Proves  \Ax{5}$, i.e., $\Diamond!A \lif \Box\Diamond!A$.  \begin{oltableau}    [\pFmla{\False}{\Diamond\formula{A} \lif \Box\Diamond \formula{A}}{1},      just = \TAss      [\pFmla{\True}{\Diamond \formula{A}}{1}, just = {\TRule{\False}{\lif}[1]}        [\pFmla{\False}{\Box\Diamond \formula{A}}{1},          just = {\TRule{\False}{\lif}[1]}          [\pFmla{\False}{\Diamond \formula{A}}{2},            just = {\TRule{\False}{\Box}[3]}            [\pFmla{\True}{\formula{A}}{3},              just = {\TRule{\True}{\Diamond}[2]}                [\pFmla{\False}{\formula{A}}{3},                  just = {\TRule{\False}{\Diamond}[4]}, close]            ]          ]        ]      ]    ]  \end{oltableau}\end{ex}\end{document}

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

% Part: normal-modal-logic% Chapter: tableaux% Section: completeness\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{tab}{cpl}\olsection{Completeness for \Log{K}}\begin{explain}  To show that the method of !!{tableau}s is complete, we have to show  that whenever there is no closed !!{tableau} to show $\Gamma \Proves  !A$, then $\Gamma \Entails/ !A$, i.e., there is a countermodel. But  ``there is no closed !!{tableau}'' means that every way we could try  to construct one has to fail to close. The trick is to see that if  every such way fails to close, then a specific, \emph{systematic and    exhaustive} way also fails to close. And this systematic and  exhaustive way would close if a closed !!{tableau} exists. The  single tableau will contain, among its open branches, all the  information required to define a countermodel. The countermodel  given by an open branch in this tableau will contain the all the  prefixes used on that branch as the worlds, and !!a{propositional    variable}~$p$ is true at $\sigma$ iff $\sFmla{\True}{p}[\sigma]$  occurs on the branch.\end{explain}\begin{defn}  A branch in !!a{tableau} is called complete if, whenever it contains  a prefixed !!{formula} $\sFmla{S}{!A}[\sigma]$ to which a rule can  be applied, it also contains  \begin{enumerate}    \item the prefixed !!{formula}s that are the corresponding      conclusions of the rule, in the case of propositional stacking      rules;    \item one of the corresponding conclusion !!{formula}s in the case      of propositional branching rules;    \item at least one possible conclusion in the case of modal rules      that require a new prefix;    \item the corresponding conclusion for every prefix occurring on      the branch in the case of modal rules that require a used      prefix.  \end{enumerate}\end{defn}\begin{explain}For instance, a complete branch contains $\sFmla{\True}{!B}[\sigma]$and $\sFmla{\True}{!C}[\sigma]$ whenever it contains $\sFmla{\True}{!B  \land !C}$. If it contains $\sFmla{\True}{!B \lor !C}[\sigma]$ itcontains at least one of $\sFmla{\False}{!B}[\sigma]$ and$\sFmla{\True}{!C}[\sigma]$. If it contains \iftag{prvBox}{$\sFmla{\False}{\Box}[\sigma]$} {$\sFmla{\True}{\Diamond}[\sigma]$}it also contains \iftag{prvBox} {$\sFmla{\False}{\Box}[\sigma.n]$}{$\sFmla{\True}{\Diamond}[\sigma.n]$} for at least one~$n$.  Andwhenever it contains \iftag{prvBox} {$\sFmla{\True}{\Box}[\sigma]$}{$\sFmla{\False}{\Diamond}[\sigma]$} it also contains \iftag{prvBox}{$\sFmla{\True}{\Box}[\sigma.n]$}{$\sFmla{\False}{\Diamond}[\sigma.n]$} for every~$n$ such that$\sigma.n$ is used on the branch.\end{explain}\begin{prop}\ollabel{prop:complete-tableau}  Every finite $\Gamma$ has !!a{tableau} in which every branch is complete.\end{prop}\begin{proof}  Consider an open branch in !!a{tableau} for~$\Gamma$. There are  finitely many prefixed !!{formula}s in the branch to which a rule  could be applied. In some fixed order (say, top to bottom), for each  of these prefixed !!{formula}s for which the conditions (1)--(4) do  not already hold, apply the rules that can be applied to it to  extend the branch. In some cases this will result in branching;  apply the rule at the tip of each resulting branch for all remaining  prefixed !!{formula}s. Since the number of prefixed !!{formula}s is  finite, and the number of used prefixes on the branch is finite,  this procedure eventually results in (possibly many) branches  extending the original branch. Apply the procedure to each, and  repeat. But by construction, every branch is closed.\end{proof}\begin{thm}[Completeness]  \ollabel{thm:tableau-completeness}  If $\Gamma$ has no closed !!{tableau}, $\Gamma$ is satisfiable.\end{thm}\begin{proof}By the proposition, $\Gamma$ has !!a{tableau} in which every branch iscomplete. Since it has no closed !!{tableau}, it thas has !!a{tableau} inwhich at least one branch is open and complete. Let $\Delta$ be theset of prefixed !!{formula}s on the branch, and $P(\Delta)$ the set ofprefixes occurring in it.We define a model~$\mModel{M(\Delta)} = \tuple{P(\Delta), R, V}$ wherethe worlds are the prefixes occurring in~$\Delta$, the accessibilityrelation is given by:\[R\sigma\sigma' \quad \text{iff} \quad\sigma'=\sigma.n \quad \text{for some~$n$}\]and\[V(p) = \Setabs{\sigma}{\sFmla{\True}{p}[\sigma] \in \Delta}.\]We show by induction on~$!A$ that if $\sFmla{\True}{!A}[\sigma] \in\Delta$ then $\mSat{M(\Delta)}{!A}[\sigma]$, and if$\sFmla{\False}{!A}[\sigma] \in \Delta$ then$\mSat/{M(\Delta)}{!A}[\sigma]$.\begin{enumerate}  \item \indcase{!A}{p}{If $\sFmla{\True}{\indfrm}[\sigma] \in \Delta$    then $\sigma \in V(p)$ (by definition of~$V$) and so    $\mSat{M(\Delta)}{\indfrm}[\sigma]$.    If $\sFmla{\False}{\indfrm}[\sigma] \in \Delta$ then    $\sFmla{\True}{\indfrm}[\sigma] \notin \Delta$, since the branch    would otherwise be closed. So $\sigma \notin V(p)$ and thus    $\mSat/{M(\Delta)}{\indfrm}[\sigma]$.}  \item \indcase{!A}{\lnot !B}{\iftag{probNot}{Exercise.}{If      $\sFmla{\True}{\indfrm}[\sigma] \in \Delta$, then      $\sFmla{\False}{!B}[\sigma] \in \Delta$ since the branch is      complete. By induction hypothesis,      $\mSat/{M(\Delta)}{!B}[\sigma]$ and thus      $\mSat{M(\Delta)}{\indfrm}[\sigma]$.      If $\sFmla{\False}{\indfrm}[\sigma] \in \Delta$, then      $\sFmla{\True}{!B}[\sigma] \in \Delta$ since the branch is      complete. By induction hypothesis,      $\mSat{M(\Delta)}{!B}[\sigma]$ and thus      $\mSat/{M(\Delta)}{\indfrm}[\sigma]$.}}  \item \indcase{!A}{!B \land !C}{\iftag{probAnd}{Exercise.}{If      $\sFmla{\True}{\indfrm}[\sigma] \in \Delta$, then both      $\sFmla{\True}{!B}[\sigma] \in \Delta$ and      $\sFmla{\True}{!C}[\sigma] \in \Delta$ since the branch is      complete. By induction hypothesis,      $\mSat{M(\Delta)}{!B}[\sigma]$ and      $\mSat{M(\Delta)}{!C}[\sigma]$. Thus      $\mSat{M(\Delta)}{\indfrm}[\sigma]$.      If $\sFmla{\False}{\indfrm}[\sigma] \in \Delta$, then either      $\sFmla{\False}{!B}[\sigma] \in \Delta$ or      $\sFmla{\False}{!C}[\sigma] \in \Delta$ since the branch is      complete. By induction hypothesis, either      $\mSat/{M(\Delta)}{!B}[\sigma]$ or      $\mSat/{M(\Delta)}{!B}[\sigma]$. Thus      $\mSat/{M(\Delta)}{\indfrm}[\sigma]$.}}  \item \indcase{!A}{!B \lor !C}{\iftag{probOr}{Exercise.}{If      $\sFmla{\True}{\indfrm}[\sigma] \in \Delta$, then either      $\sFmla{\True}{!B}[\sigma] \in \Delta$ or      $\sFmla{\True}{!C}[\sigma] \in \Delta$ since the branch is      complete. By induction hypothesis, either      $\mSat{M(\Delta)}{!B}[\sigma]$ or      $\mSat{M(\Delta)}{!C}[\sigma]$. Thus      $\mSat{M(\Delta)}{\indfrm}[\sigma]$.      If $\sFmla{\False}{\indfrm}[\sigma] \in \Delta$, then both      $\sFmla{\False}{!B}[\sigma] \in \Delta$ and      $\sFmla{\False}{!C}[\sigma] \in \Delta$ since the branch is      complete. By induction hypothesis, both      $\mSat/{M(\Delta)}{!B}[\sigma]$ and      $\mSat/{M(\Delta)}{!B}[\sigma]$. Thus      $\mSat/{M(\Delta)}{\indfrm}[\sigma]$.}}  \item \indcase{!A}{!B \lif !C}{\iftag{probIf}{Exercise.}{If      $\sFmla{\True}{\indfrm}[\sigma] \in \Delta$, then either      $\sFmla{\False}{!B}[\sigma] \in \Delta$ or      $\sFmla{\True}{!C}[\sigma] \in \Delta$ since the branch is      complete. By induction hypothesis, either      $\mSat/{M(\Delta)}{!B}[\sigma]$ or      $\mSat{M(\Delta)}{!C}[\sigma]$. Thus      $\mSat{M(\Delta)}{\indfrm}[\sigma]$.      If $\sFmla{\False}{\indfrm}[\sigma] \in \Delta$, then both      $\sFmla{\True}{!B}[\sigma] \in \Delta$ and      $\sFmla{\False}{!C}[\sigma] \in \Delta$ since the branch is      complete. By induction hypothesis, both      $\mSat{M(\Delta)}{!B}[\sigma]$ and      $\mSat/{M(\Delta)}{!B}[\sigma]$. Thus      $\mSat/{M(\Delta)}{\indfrm}[\sigma]$.}}  \item \indcase{!A}{\Box !B}{\iftag{probBox}{Exercise.}{If      $\sFmla{\True}{\indfrm}[\sigma] \in \Delta$, then, since the      branch is complete, $\sFmla{\True}{!B}[\sigma.n] \in \Delta$ for      every $\sigma.n$ used on the branch, i.e., for every $\sigma'      \in P(\Delta)$ such that $R\sigma\sigma'$.  By induction      hypothesis, $\mSat{M(\Delta)}{!B}[\sigma']$ for every $\sigma'$      such that $R\sigma\sigma'$. Therefore,      $\mSat{M(\Delta)}{\indfrm}[\sigma]$.      If $\sFmla{\False}{\indfrm}[\sigma] \in \Delta$, then for some      $\sigma.n$, $\sFmla{\False}{!B}[\sigma.n] \in \Delta$ since the      branch is complete.  By induction hypothesis,      $\mSat/{M(\Delta)}{!B}[\sigma.n]$.  Since $R\sigma(\sigma.n)$,      there is a~$\sigma'$ such that      $\mSat/{M(\Delta)}{!B}[\sigma']$. Thus      $\mSat/{M(\Delta)}{\indfrm}[\sigma]$.}}  \item \indcase{!A}{\Diamond !B}{\iftag{probDiamond}{Exercise.}{If      $\sFmla{\True}{\indfrm}[\sigma] \in \Delta$, then for some      $\sigma.n$, $\sFmla{\True}{!B}[\sigma.n] \in \Delta$ since the      branch is complete. By induction hypothesis,      $\mSat{M(\Delta)}{!B}[\sigma.n]$.  Since $R\sigma(\sigma.n)$,      there is a~$\sigma'$ such that      $\mSat{M(\Delta)}{!B}[\sigma']$. Thus      $\mSat{M(\Delta)}{\indfrm}[\sigma]$.      If $\sFmla{\False}{\indfrm}[\sigma] \in \Delta$, then, since the      branch is complete, $\sFmla{\False}{!B}[\sigma.n] \in \Delta$      for every $\sigma.n$ used on the branch, i.e., for every      $\sigma' \in P(\Delta)$ such that $R\sigma\sigma'$.  By      induction hypothesis, $\mSat/{M(\Delta)}{!B}[\sigma']$ for every      $\sigma'$ such that $R\sigma\sigma'$. Therefore,      $\mSat/{M(\Delta)}{\indfrm}[\sigma]$.}}\end{enumerate}Since $\Gamma \subseteq \Delta$, $\mSat{M(\Delta)}{\Gamma}$.\end{proof}\begin{prob}Complete the proof of \olref[nml][tab][cpl]{thm:tableau-completeness}.\end{prob}\begin{cor}\ollabel{cor:entailment-completeness}If $\Gamma \Entails !A$ then $\Gamma \Proves !A$.\end{cor}\begin{cor}\ollabel{cor:weak-completeness}If $!A$ is true in all models, then $\Proves !A$.\end{cor}\end{document}

content/normal-modal-logic/tableaux/countermodels.tex

% Part: normal-modal-logic% Chapter: tableaux% Section: countermodels\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{tab}{cou}      \olsection{Countermodels from \usetoken{P}{tableau}}\begin{explain}  The proof of the completeness theorem doesn't just show that if  $\Entails !A$ then $\Proves !A$, it also gives us a method for  constructing countermodels to~$!A$ if $\Entails/ A$. In the case  of~$\Log{K}$, this method constitutes a \emph{decision    procedure}. For suppose $\Entails/ !A$. Then the proof of  \olref[cpl]{prop:complete-tableau} gives a method for constructing a  complete !!{tableau}. The method in fact always terminates. The  propositional rules for~$\Log{K}$ only add prefixed !!{formula}s of  lower complexity, i.e., each propositional rule need only be applied  once on a branch for any signed formula $\sFmla{S}{!A}[\sigma]$. New  prefixes are only generated by the  \iftag{prvBox}{$\TRule{\False}{\Box}$}{}\iftag{notprvBox,notprvDiamond}{}{    and }\iftag{prvDiamond}{$\TRule{\True}{\Diamond}$}{}  \iftag{notprvBox,notprvDiamond}{rule}{rules}, and also only have to  be applied once (and produce a single new prefix).  \iftag{prvBox}{$\TRule{\True}{\Box}$}{}\iftag{notprvBox,notprvDiamond}{}{    and }\iftag{prvDiamond}{$\TRule{\False}{\Diamond}$}{}  \iftag{notprvBox,notprvDiamond}{has}{have} to be applied potentially  multiple times, but only once per prefix, and only finitely many new  prefixes are generated. So the construction either results in a  closed branch or a complete branch after finitely many stages.  Once a tableau with an open complete branch is constructed, the  proof of \olref[cpl]{thm:tableau-completeness} gives us an explict model  that satisfies the original set of prefixed !!{formula}s. So not  only is it the case that if $\Gamma \Entails !A$, then a closed  !!{tableau} exists and $\Gamma \Proves !A$, if we look for the  closed !!{tableau} in the right way and end up with a ``complete''  !!{tableau}, we'll not only know that $\Gamma \Entails/ !A$ but  actually be able to construct a countermodel.\end{explain}\iftag{prvBox}{\begin{ex}  We know that $\Proves/ \Box(p \lor q) \lif (\Box p \lor \Box  q)$. The construction of a tableau begins with:  \begin{oltableau}    [\pFmla{\False}{\Box(p \lor q) \lif (\Box p \lor \Box q)}{1},      just = \TAss, checked      [\pFmla{\True}{\Box(p \lor q)}{1},        just = {\TRule{\False}{\lif}[1]},         [\pFmla{\False}{\Box p \lor \Box q}{1},          just = {\TRule{\False}{\lif}[1]}, checked          [\pFmla{\False}{\Box p}{1},            just = {\TRule{\False}{\lor}[3]}, checked            [\pFmla{\False}{\Box q}{1},              just = {\TRule{\False}{\lor}[3]}, checked              [\pFmla{\False}{p}{1.1},                 just = {\TRule{\False}{\Box}[4]}, checked                [\pFmla{\False}{q}{1.2},                   just = {\TRule{\False}{\Box}[5]}, checked                ]              ]            ]          ]        ]      ]    ]  \end{oltableau}  The !!{tableau} is of course not finished yet. In the next step, we  consider the only line without a checkmark: the prefixed !!{formula}  $\sFmla{\True}{\Box(p \lor q)}[1]$ on line~$2$. The construction of  the closed tableau says to apply the $\TRule{\True}{\Box}$ rule for  every prefix used on the branch, i.e., for both $1.1$ and $1.2$:  \begin{oltableau}    [\pFmla{\False}{\Box(p \lor q) \lif (\Box p \lor \Box q)}{1},      just = \TAss, checked      [\pFmla{\True}{\Box(p \lor q)}{1},        just = {\TRule{\False}{\lif}[1]},         [\pFmla{\False}{\Box p \lor \Box q}{1},          just = {\TRule{\False}{\lif}[1]}, checked          [\pFmla{\False}{\Box p}{1},            just = {\TRule{\False}{\lor}[3]}, checked            [\pFmla{\False}{\Box q}{1},              just = {\TRule{\False}{\lor}[3]}, checked              [\pFmla{\False}{p}{1.1},                 just = {\TRule{\False}{\Box}[4]}, checked                [\pFmla{\False}{q}{1.2},                   just = {\TRule{\False}{\Box}[5]}, checked                  [\pFmla{\True}{p \lor q}{1.1},                     just = {\TRule{\True}{\Box}[2]}                    [\pFmla{\True}{p \lor q}{1.2},                       just = {\TRule{\True}{\Box}[2]}                    ]                  ]                ]              ]            ]          ]        ]      ]    ]  \end{oltableau}  Now lines 2, 8, and 9, don't have checkmarks. But no new prefix has  been added, so we apply $\TRule{\True}{\lor}$ to lines~8 and~9, on  all resulting branches (as long as they don't close):  \begin{oltableau}    [\pFmla{\False}{\Box(p \lor q) \lif (\Box p \lor \Box q)}{1},      just = \TAss, checked      [\pFmla{\True}{\Box(p \lor q)}{1},        just = {\TRule{\False}{\lif}[1]}, checked        [\pFmla{\False}{\Box p \lor \Box q}{1},          just = {\TRule{\False}{\lif}[1]}, checked          [\pFmla{\False}{\Box p}{1},            just = {\TRule{\False}{\lor}[3]}, checked            [\pFmla{\False}{\Box q}{1},              just = {\TRule{\False}{\lor}[3]}, checked              [\pFmla{\False}{p}{1.1},                 just = {\TRule{\False}{\Box}[4]}, checked                [\pFmla{\False}{q}{1.2},                   just = {\TRule{\False}{\Box}[5]}, checked                  [\pFmla{\True}{p \lor q}{1.1},                     just = {\TRule{\True}{\Box}[2]}, checked                    [\pFmla{\True}{p \lor q}{1.2},                       just = {\TRule{\True}{\Box}[2]}, checked                      [\pFmla{\True}{p}{1.1},                        just = {\TRule{\True}{\lor}[8]}, checked, close                      ]                      [\pFmla{\True}{q}{1.1},                        just = {\TRule{\True}{\lor}[8]}, checked                        [\pFmla{\True}{p}{1.2},                          just = {\TRule{\True}{\lor}[9]}, checked]                        [\pFmla{\True}{q}{1.2},                          just = {\TRule{\True}{\lor}[9]}, checked, close]                      ]                    ]                  ]                ]              ]            ]          ]        ]      ]    ]  \end{oltableau}  There is one remaining open branch, and it is complete. From it we  define the model with worlds $W = \{1, 1.1, 1.2\}$ (the only  prefixes appearing on the open branch), the accessibility relation  $R = \{\tuple{1, 1.1}, \tuple{1, 1.2}\}$, and the assignment $V(p) =  \{1.2\}$ (because line~11 contains $\sFmla{\True}{p}[1.2]$) and  $V(q) = \{1.1\}$ (because line~10 contains  $\sFmla{\True}{q}[1.1]$). The model is pictured in  \olref{fig:counter-Box}, and you can verify that it is a  countermodel to $\Box(p \lor q) \lif (\Box p \lor \Box q)$.  \begin{figure}  \begin{center}    \begin{tikzpicture}[modal]      \node[world] (w1) [label={[align=right]right:\mFalse{p}\\ \mFalse{q}}]{$1$};       \node[world] (w2) [label={[align=right]right:\mFalse{p}\\ \mTrue{q}},        above left=of w1]{$1.1$};       \node[world] (w3) [label={[align=right]right:\mTrue{p}\\ \mFalse{q}},        above right=of w1] {$1.2$};      \draw[->] (w1) to (w2);      \draw[->] (w1) to (w3);    \end{tikzpicture}  \end{center}  \caption{A countermodel to $\Box(p \lor q) \lif (\Box p \lor \Box    q)$.}  \ollabel{fig:counter-Box}\end{figure}\end{ex}          }{\begin{ex}  We know that $\Proves/ (\Diamond p \land \Diamond q) \lif \Diamond(p  \land q)$. The construction of a tableau begins with:  \begin{oltableau}    [\pFmla{\False}{(\Diamond p \land \Diamond q) \lif \Diamond(p \land q)}{1},      just = \TAss, checked      [\pFmla{\True}{\Diamond p \land \Diamond q}{1},        just = {\TRule{\False}{\lif}[1]}, checked        [\pFmla{\False}{\Diamond(p \land q)}{1},          just = {\TRule{\False}{\lif}[1]}          [\pFmla{\True}{\Diamond p}{1},            just = {\TRule{\True}{\land}[2]}, checked            [\pFmla{\True}{\Diamond q}{1},              just = {\TRule{\True}{\land}[2]}, checked              [\pFmla{\True}{p}{1.1},                 just = {\TRule{\True}{\Diamond}[4]}, checked                [\pFmla{\True}{q}{1.2},                   just = {\TRule{\True}{\Diamond}[5]}, checked                ]              ]            ]          ]        ]      ]    ]  \end{oltableau}  The !!{tableau} is of course not finished yet. In the next step, we  consider the only line without a checkmark: the prefixed !!{formula}  $\sFmla{\True}{\Diamond(p \land q)}[1]$ on line~$3$. The construction of  the closed tableau says to apply the $\TRule{\True}{\Diamond}$ rule for  every prefix used on the branch, i.e., for both $1.1$ and $1.2$:  \begin{oltableau}    [\pFmla{\False}{\Diamond(p \land q) \lif (\Diamond p \land \Diamond q)}{1},      just = \TAss, checked      [\pFmla{\True}{\Diamond p \land \Diamond q}{1},        just = {\TRule{\False}{\lif}[1]}, checked        [\pFmla{\False}{\Diamond (p \land q)}{1},          just = {\TRule{\False}{\lif}[1]}          [\pFmla{\True}{\Diamond p}{1},            just = {\TRule{\True}{\land}[2]}, checked            [\pFmla{\True}{\Diamond q}{1},              just = {\TRule{\True}{\land}[2]}, checked              [\pFmla{\True}{p}{1.1},                 just = {\TRule{\True}{\Diamond}[4]}, checked                [\pFmla{\True}{q}{1.2},                   just = {\TRule{\True}{\Diamond}[5]}, checked                  [\pFmla{\False}{p \land q}{1.1},                     just = {\TRule{\False}{\Diamond}[3]}                    [\pFmla{\False}{p \land q}{1.2},                       just = {\TRule{\False}{\Diamond}[3]}                    ]                  ]                ]              ]            ]          ]        ]      ]    ]  \end{oltableau}  Now lines 3, 8, and 9, don't have checkmarks. But no new prefix has  been added, so we apply $\TRule{\False}{\land}$ to lines~8 and~9, on  all resulting branches (as long as they don't close):  \begin{oltableau}    [\pFmla{\False}{(\Diamond p \land \Diamond q) \lif \Diamond(p \land q)}{1},      just = \TAss, checked      [\pFmla{\True}{\Diamond p \land \Diamond q}{1},        just = {\TRule{\False}{\lif}[1]}, checked        [\pFmla{\False}{\Diamond(p \land q)}{1},          just = {\TRule{\False}{\lif}[1]}          [\pFmla{\True}{\Diamond p}{1},            just = {\TRule{\True}{\land}[2]}, checked            [\pFmla{\True}{\Diamond q}{1},              just = {\TRule{\True}{\land}[2]}, checked              [\pFmla{\True}{p}{1.1},                 just = {\TRule{\True}{\Diamond}[4]}, checked                [\pFmla{\True}{q}{1.2},                   just = {\TRule{\True}{\Diamond}[5]}, checked                  [\pFmla{\False}{p \land q}{1.1},                     just = {\TRule{\False}{\Diamond}[3]}, checked                    [\pFmla{\False}{p \land q}{1.2},                       just = {\TRule{\False}{\Diamond}[3]}, checked                      [\pFmla{\False}{p}{1.1},                        just = {\TRule{\False}{\land}[8]}, checked, close                      ]                      [\pFmla{\False}{q}{1.1},                        just = {\TRule{\False}{\land}[8]}, checked                        [\pFmla{\False}{p}{1.2},                          just = {\TRule{\False}{\land}[9]}, checked]                        [\pFmla{\False}{q}{1.2},                          just = {\TRule{\False}{\land}[9]}, checked, close]                      ]                    ]                  ]                ]              ]            ]          ]        ]      ]    ]  \end{oltableau}  There is one remaining open branch, and it is complete. From it we  define the model with worlds $W = \{1, 1.1, 1.2\}$ (the only  prefixes appearing on the open branch), the accessibility relation  $R = \{\tuple{1, 1.1}, \tuple{1, 1.2}\}$, and the assignment $V(p) =  \{1.1\}$ (because line~6 contains $\sFmla{\True}{p}[1.1]$) and  $V(q) = \{1.2\}$ (because line~7 contains  $\sFmla{\True}{q}[1.1]$). The model is pictured in  \olref{fig:counter-Diamond}, and you can verify that it is a  countermodel to $(\Diamond p \land \Diamond q) \lif \Diamond (p \land q)$.  \begin{figure}  \begin{center}    \begin{tikzpicture}[modal]      \node[world] (w1) [label={[align=right]right:\mFalse{p}\\ \mFalse{q}}]{$1$};       \node[world] (w2) [label={[align=right]right:\mTrue{p}\\ \mFalse{q}},        above left=of w1]{$1.1$};       \node[world] (w3) [label={[align=right]right:\mFalse{p}\\ \mTrue{q}},        above right=of w1] {$1.2$};      \draw[->] (w1) to (w2);      \draw[->] (w1) to (w3);    \end{tikzpicture}  \end{center}  \caption{A countermodel to $(\Diamond p \land \Diamond q) \lif    \Diamond (p \land q)$.}  \ollabel{fig:counter-Diamond}\end{figure}\end{ex}          }\end{document}