Normal Modal Logics

Modal Sequent Calculus

content/normal-modal-logic/sequent-calculus/sequent-calculus.tex

% Part: normal-modal-logic% Chapter: sequent-calculus\documentclass[../../../include/open-logic-chapter]{subfiles}\begin{document}\olchapter{nml}{seq}{Modal Sequent Calculus}%\tagfalse{prvDiamond}\begin{editorial}  Draft chapter on sequent calculi for modal logic. Needs more  examples, soundness and completeness proofs.\end{editorial}\olimport{introduction}\olimport{rules-for-K}\olimport{proofs-in-K}%\olimport{soundness}\olimport{more-rules}%\olimport{more-soundness}%\olimport{hypersequents-S5}\OLEndChapterHook\end{document}

content/normal-modal-logic/sequent-calculus/introduction.tex

% Part: normal-modal-logic% Chapter: sequent-calculus% Section: introduction\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{seq}{int}\olsection{Introduction}The sequent calculus for propositional logic can be extended byadditional rules that dealwith~\iftag{prvBox}{$\Box$\iftag{prvDiamond}{ and~}{}}{}%\iftag{prvDiamond}{$\Diamond$}{}. For instance, for~$\Log{K}$, wehave \Log{LK} plus:\[  \iftag{prvBox}{\iftag{prvDiamond}{% <> and [] primitive    \Axiom$\Gamma \fCenter \Delta, !A$    \RightLabel{$\Box$}    \UnaryInf$\Box\Gamma \fCenter \Diamond\Delta, \Box!A$    \DisplayProof      \qquad    \Axiom$!A, \Gamma \fCenter \Delta$    \RightLabel{$\Diamond$}    \UnaryInf$\Diamond!A, \Box\Gamma \fCenter \Diamond\Delta$    \DisplayProof}{% only Box primitive\Axiom$\Gamma \fCenter !A$\RightLabel{$\Box$}\UnaryInf$\Box\Gamma \fCenter \Box!A$\DisplayProof}}{% only <> primitive  \Axiom$!A \fCenter \Delta$  \RightLabel{$\Diamond$}  \UnaryInf$\Diamond!A \fCenter \Diamond\Delta$  \DisplayProof}\]For extensions of~$\Log{K}$, additional rules have to be added aswell.Not every modal logic has such a sequent calculus.  Even $\Log{S5}$,which is semantically simple (it can be defined without usingaccessibility relations at all) is not known to have a sequentcalculus that results from~$\Log{LK}$ which is complete without therule~\Cut. However, it has a cut-free complete \emph{hypersequent}calculus.\end{document}

content/normal-modal-logic/sequent-calculus/rules-for-K.tex

% Part: normal-modal-logic% Chapter: sequent-calculus% Section: rules-for-K\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{seq}{rul}\olsection{Rules for \Log{K}}The rules for the regular propositional connectives are the same asfor regular sequent calculus~$\Log{LK}$. Axioms are also the same: anysequent of the form $!A \Sequent !A$ counts as an axiom.For the modal operator\iftag{prvBox}{\iftag{prvDiamond}{s~$\Box$and}{~$\Box$}}{}\iftag{prvDiamond}{~$\Diamond$}{}, we have thefollowing additional \iftag{notprvBox,notprvDiamond}{rule}{rules}:\[  \iftag{prvBox}{\iftag{prvDiamond}{% <> and [] primitive    \Axiom$\Gamma \fCenter \Delta, !A$    \RightLabel{$\Box$}    \UnaryInf$\Box\Gamma \fCenter \Diamond\Delta, \Box!A$    \DisplayProof      \qquad    \Axiom$!A, \Gamma \fCenter \Delta$    \RightLabel{$\Diamond$}    \UnaryInf$\Diamond!A, \Box\Gamma \fCenter \Diamond\Delta$    \DisplayProof}{% only Box primitive\Axiom$\Gamma \fCenter !A$\RightLabel{$\Box$}\UnaryInf$\Box\Gamma \fCenter \Box!A$\DisplayProof}}{% only <> primitive  \Axiom$!A \fCenter \Delta$  \RightLabel{$\Diamond$}  \UnaryInf$\Diamond!A \fCenter \Diamond\Delta$  \DisplayProof}\]Here, \iftag{prvBox}{$\Box\Gamma$ means the sequence of !!{formula}sresulting from~$\Gamma$ by putting $\Box$ in front of every!!{formula} in~$\Gamma$\iftag{prvDiamond}{ and}{}}{}\iftag{prvDiamond}{$\Diamond\Delta$ is the sequence of!!{formula}s resulting from~$\Delta$ by putting $\Diamond$ in front ofevery !!{formula} in~$\Delta$}{}. \iftag{notprvDiamond}{The right sideof the premise of the $\Box$ rule must contain at most one!!{formula}~$!A$. }{}%\iftag{notprvBox}{The left side of the premise of the $\Diamond$rule must contain at most one !!{formula}~$!A$. }{}%\iftag{prvBox}{$\Gamma$\iftag{prvDiamond}{~and~}{}}{}\iftag{prvDiamond}{$\Delta$}{}may be empty; in that case the corresponding part\iftag{prvBox}{$\Box\Gamma$\iftag{prvDiamond}{~and~}{}}{}\iftag{prvDiamond}{$\Diamond\Delta$}{}of the conclusion sequent is empty as well.The restriction of adding a\iftag{prvBox}{$\Box$ on the right\iftag{prvDiamond}{ and}{}}{}\iftag{prvDiamond}{$\Diamond$ on the left}{}to a single !!{formula}~$!A$ is necessary. If we allowed to\iftag{prvBox}{add $\Box$ to any number of !!{formula}s on theright\iftag{prvDiamond}{ or to }{}}{}\iftag{prvDiamond}{add $\Diamond$to any number of !!{formula}s on the left}{} we would be able to!!{derive}:  \[    \iftag{prvBox}{      \Axiom$!A \fCenter !A$      \RightLabel{\RightR{\lnot}}      \UnaryInf$\fCenter !A, \lnot !A$      \RightLabel{$\Box*$}      \UnaryInf$\fCenter \Box!A, \Box\lnot !A$      \doubleLine      \RightLabel{\RightR{\lor}}      \UnaryInf$\fCenter \Box!A \lor \Box \lnot !A$      \DisplayProof}{}    \iftag{notprvBox,notprvDiamond}{}{\qquad}    \iftag{prvDiamond}{      \Axiom$!A \fCenter !A$      \RightLabel{\LeftR{\lnot}}      \UnaryInf$\lnot !A, !A \fCenter$      \RightLabel{$\Diamond*$}      \UnaryInf$\Diamond\lnot !A,\Diamond!A \fCenter $      \RightLabel{\RightR{\lnot}}      \UnaryInf$\Diamond!A \fCenter \lnot\Diamond\lnot !A$      \RightLabel{\RightR{\lif}}      \UnaryInf$ \fCenter \Diamond!A \lif \lnot\Diamond\lnot !A$      \DisplayProof}{}  \]But \iftag{prvBox}{$\Box!A \lor \Box \lnot !A$\iftag{prvDiamond}{ and$\Diamond!A \lif \lnot\Diamond\lnot !A$ are}{is}}{$\Diamond!A \lif\lnot\Diamond\lnot !A$ is} not valid in~$\Log{K}$.If we allowed side formulas in addition to~$!A$ in the premise, andallowed \iftag{prvBox}{the $\Box$ rule to add $\Box$ to only~$!A$ onthe right\iftag{prvDiamond}{, or allowed }{}}{}\iftag{prvDiamond}{the$\Diamond$ rule to add $\Diamond$ to only~$!A$ on the left}{} (but donothing to the side formulas) we would be able to !!{derive}:\[  \iftag{prvBox}{    \Axiom$!A \fCenter !A$    \RightLabel{\RightR{\lnot}}    \UnaryInf$\fCenter !A, \lnot !A$    \RightLabel{\RightR{\Exchange}}    \UnaryInf$\fCenter \lnot !A, !A$    \RightLabel{$\Box*$}    \UnaryInf$\fCenter \lnot!A, \Box !A$    \doubleLine    \RightLabel{\RightR{\lor}}    \UnaryInf$\fCenter \lnot!A \lor \Box !A$    \DisplayProof}{}  \iftag{notprvBox,notprvDiamond}{}{\qquad}  \iftag{prvDiamond}{    \Axiom$!A \fCenter !A$    \RightLabel{\LeftR{\lnot}}    \UnaryInf$\lnot !A, !A \fCenter$    \RightLabel{$\Diamond*$}    \UnaryInf$\Diamond\lnot !A, !A \fCenter $    \RightLabel{\RightR{\lnot}}    \UnaryInf$!A \fCenter \lnot\Diamond\lnot !A$    \RightLabel{\RightR{\lif}}    \UnaryInf$ \fCenter !A \lif \lnot\Diamond\lnot !A$    \DisplayProof}{}\]But \iftag{prvBox}{$\lnot!A \lor \Box !A$ (which is equivalent to $!A\lif \Box!A$)\iftag{prvDiamond}{ and $!A \lif \lnot\Diamond\lnot !A$are}{is}}{$!A \lif \lnot\Diamond\lnot !A$ is} not valid in~$\Log{K}$.\end{document}

content/normal-modal-logic/sequent-calculus/proofs-in-K.tex

% Part: normal-modal-logic% Chapter: sequent-calculus% Section: proofs-in-K\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{seq}{prk}\olsection{Sequent \usetoken{P}{derivation} for \Log{K}}\iftag{prvBox}{\begin{ex}  We give a sequent calculus !!{derivation} that shows $\Proves (\Box!A \land \Box!B)  \lif \Box (!A \land !B)$.  \begin{prooftree}    \Axiom$!A \fCenter !A$    \doubleLine    \UnaryInf$!B, !A \fCenter !A$       \Axiom$!B \fCenter !B$    \doubleLine    \UnaryInf$!B, !A \fCenter !B$       \RightLabel{\RightR{\land}}    \BinaryInf$!B, !A \fCenter !A \land !B$        \RightLabel{$\Box$}    \UnaryInf$\Box!B, \Box!A \fCenter \Box    (!A \land !B)$    \RightLabel{\LeftR{\land}}    \UnaryInf$\Box!A \land \Box!B, \Box!A \fCenter \Box    (!A \land !B)$    \RightLabel{\LeftR{\Exchange}}    \UnaryInf$\Box!A, \Box!A \land \Box!B \fCenter \Box    (!A \land !B)$    \RightLabel{\LeftR{\land}}    \UnaryInf$\Box!A \land \Box!B, \Box!A \land \Box!B \fCenter \Box (!A \land !B)$    \RightLabel{\LeftR{\Contraction}}    \UnaryInf$\Box!A \land \Box!B \fCenter \Box (!A \land !B)$    \RightLabel{\RightR{\lif}}    \UnaryInf$\fCenter (\Box!A \land \Box!B)    \lif \Box (!A \land !B)$  \end{prooftree}\end{ex}}{}\iftag{prvDiamond}{  \begin{ex}    We give a sequent calculus !!{derivation} that shows $\Proves \Diamond(!A    \lor !B) \lif (\Diamond !A \lor \Diamond!B)$.    \begin{prooftree}      \Axiom$!A \fCenter !A$      \doubleLine      \UnaryInf$!A \fCenter !A, !B$         \Axiom$!B \fCenter !B$      \doubleLine      \UnaryInf$!B \fCenter !A, !B$         \RightLabel{\LeftR{\lor}}      \BinaryInf$!A \lor !B \fCenter !A, !B$          \RightLabel{$\Diamond$}      \UnaryInf$\Diamond(!A \lor !B) \fCenter       \Diamond !A, \Diamond!B$      \RightLabel{\RightR{\lor}}      \UnaryInf$\Diamond(!A \lor !B) \fCenter       \Diamond !A, \Diamond !A \lor \Diamond!B$      \RightLabel{\RightR{\Exchange}}      \UnaryInf$\Diamond(!A \lor !B) \fCenter \Diamond !A \lor \Diamond!B, \Diamond !A$      \RightLabel{\RightR{\lor}}      \UnaryInf$\Diamond(!A \lor !B) \fCenter       \Diamond !A \lor \Diamond!B, \Diamond !A \lor \Diamond!B$      \RightLabel{\RightR{\Contraction}}      \UnaryInf$\Diamond(!A      \lor !B) \fCenter \Diamond !A \lor \Diamond!B$      \RightLabel{\RightR{\lif}}      \UnaryInf$\fCenter \Diamond(!A      \lor !B) \lif (\Diamond !A \lor \Diamond!B)$    \end{prooftree}  \end{ex}}{}\iftag{notprvBox,notprvDiamond}{}{  Here is !!a{derivation} of~\Dual.  \begin{prooftree}    \Axiom$!A \fCenter !A$    \RightLabel{\RightR{\lnot}}    \UnaryInf$\lnot !A, !A \fCenter $    \RightLabel{$\Diamond$}    \UnaryInf$\Diamond\lnot !A, \Box !A \fCenter $    \RightLabel{\RightR{\lnot}}    \UnaryInf$\Box !A \fCenter \lnot\Diamond\lnot !A$    \RightLabel{\RightR{\lif}}    \UnaryInf$\fCenter \Box !A \lif \lnot\Diamond\lnot !A$    \Axiom$!A \fCenter !A$    \RightLabel{\RightR{\lnot}}    \UnaryInf$\fCenter !A, \lnot !A $    \RightLabel{\RightR{\Exchange}}    \UnaryInf$\fCenter \lnot !A, !A $    \RightLabel{$\Box$}    \UnaryInf$\fCenter \Diamond\lnot !A, \Box !A$    \RightLabel{\RightR{\Exchange}}    \UnaryInf$\fCenter \Box !A, \Diamond\lnot !A$    \RightLabel{\RightR{\lnot}}    \UnaryInf$\lnot\Diamond\lnot !A \fCenter \Box !A$    \RightLabel{\RightR{\lif}}    \UnaryInf$\fCenter \lnot \Diamond \lnot !A \lif \Box !A$    \RightLabel{\RightR{\land}}    \BinaryInf$\fCenter \Box !A \liff \lnot\Diamond\lnot !A$   \end{prooftree} % this does not work if problems are deferred% \begin{prob}%     Give !!a{derivation} of $\Diamond!A \liff \lnot\Box\lnot !A$%     in~$\Log{K}$.% \end{prob}}\begin{prob}  Find sequent calculus proofs 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/sequent-calculus/more-rules.tex

% Part: normal-modal-logic% Chapter: sequent-calculus% Section: more-rules\documentclass[../../../include/open-logic-section]{subfiles}\begin{document}\olfileid{nml}{seq}{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}.\iftag{prvBox}{\iftag{prvDiamond}{% [] and <> primitive\begin{table}  \begin{center}    \def\arraystretch{3}    \begin{tabular}{cc}    \hline      \Axiom$!A, \Gamma \fCenter \Delta$      \RightLabel{T$\Box$}      \UnaryInf$\Box!A, \Gamma \fCenter \Delta$      \DisplayProof    &      \Axiom$\Gamma \fCenter \Delta, !A$      \RightLabel{T$\Diamond$}      \UnaryInf$\Gamma \fCenter \Delta, \Diamond!A$      \DisplayProof    \\[1ex]%    \hline    \multicolumn{2}{c}{      \Axiom$\Gamma \fCenter \Delta$      \RightLabel{D}      \UnaryInf$\Box\Gamma \fCenter \Diamond\Delta$      \DisplayProof}    \\[1ex]%    \hline      \Axiom$\Gamma, \Diamond\Pi \fCenter \Box\Delta, \Lambda, !A$      \RightLabel{B$\Box$}      \UnaryInf$\Box\Gamma, \Pi \fCenter \Delta, \Diamond\Lambda, \Box!A$      \DisplayProof      &      \Axiom$!A, \Diamond\Gamma, \Pi \fCenter \Box\Lambda, \Delta$      \RightLabel{B$\Diamond$}      \UnaryInf$\Diamond!A, \Gamma, \Box\Pi \fCenter \Lambda, \Diamond\Delta$      \DisplayProof    \\[1ex]%    \hline      \Axiom$\Box\Gamma \fCenter \Diamond\Delta, !A$      \RightLabel{4$\Box$}      \UnaryInf$\Box\Gamma \fCenter \Diamond\Delta, \Box!A$      \DisplayProof      &      \Axiom$!A, \Box\Gamma \fCenter \Diamond\Delta$      \RightLabel{4$\Diamond$}      \UnaryInf$\Diamond!A, \Box\Gamma \fCenter \Diamond\Delta$      \DisplayProof    \\[1ex]%    \hline      \Axiom$\Box\Gamma, \Diamond\Pi \fCenter \Box\Delta,      \Diamond\Lambda, !A$      \RightLabel{5$\Box$}      \UnaryInf$\Box\Gamma, \Diamond\Pi \fCenter \Box\Delta,      \Diamond\Lambda, \Box!A$      \DisplayProof&      \Axiom$!A, \Diamond\Gamma, \Box\Pi \fCenter \Diamond\Delta, \Box\Lambda$      \RightLabel{5$\Diamond$}      \UnaryInf$\Diamond!A,\Diamond\Gamma,\Box\Pi \fCenter \Diamond\Delta,\Box\Lambda$      \DisplayProof    \\[1ex]    \hline    \end{tabular}  \end{center}  \caption{More modal rules.}  \ollabel{tab:more-rules}\end{table}}{ % only [] primitive\begin{table}  \begin{center}    \def\arraystretch{3}    \begin{tabular}{cc}    \hline      \Axiom$!A,\Gamma \fCenter \Delta$      \RightLabel{T$\Box$}      \UnaryInf$\Box!A, \Gamma \fCenter \Delta$      \DisplayProof    &    %\hline      \Axiom$\Gamma \fCenter$      \RightLabel{D$\Box$}      \UnaryInf$\Box\Gamma \fCenter$      \DisplayProof    \\[1ex]    %\hline      \Axiom$\Gamma \fCenter \Box\Delta, !A$      \RightLabel{B$\Box$}      \UnaryInf$\Box\Gamma \fCenter \Delta, \Box!A$      \DisplayProof    &    %\hline      \Axiom$\Box\Gamma \fCenter !A$      \RightLabel{4$\Box$}      \UnaryInf$\Box\Gamma \fCenter \Box!A$      \DisplayProof    \\[1ex]    %\hline    \multicolumn{2}{c}{\Axiom$\Box\Gamma \fCenter \Box\Delta, !A$      \RightLabel{5$\Box$}      \UnaryInf$\Box\Gamma \fCenter \Box\Delta, \Box!A$      \DisplayProof}    \\[1ex]    \hline    \end{tabular}  \end{center}  \caption{More modal rules.}  \ollabel{tab:more-rules}\end{table}}}{% only <> primitive\begin{table}  \begin{center}    \def\arraystretch{3}    \begin{tabular}{cc}    \hline      \Axiom$\Gamma \fCenter \Delta, !A$      \RightLabel{T$\Diamond$}      \UnaryInf$\Gamma \fCenter \Delta, \Diamond!A$      \DisplayProof    &    %\hline      \Axiom$\fCenter \Delta$      \RightLabel{D$\Diamond$}      \UnaryInf$\fCenter \Diamond\Delta$      \DisplayProof    \\[1ex]    %\hline      \Axiom$!A, \Diamond\Gamma \fCenter \Delta$      \RightLabel{B$\Diamond$}      \UnaryInf$\Diamond!A, \Gamma \fCenter \Diamond\Delta$      \DisplayProof    &    %\hline      \Axiom$!A \fCenter \Diamond\Delta$      \RightLabel{4$\Diamond$}      \UnaryInf$\Diamond!A \fCenter \Diamond\Delta$      \DisplayProof    \\[1ex]    %\hline    \multicolumn{2}{c}{      \Axiom$!A, \Diamond\Gamma \fCenter \Diamond\Delta$      \RightLabel{5$\Diamond$}      \UnaryInf$\Diamond!A,\Diamond\Gamma \fCenter \Diamond\Delta$      \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 & $\Box$,      \iftag{prvBox}{T$\Box$}{}%      \iftag{notprvBox,notprvDiamond}{}{, }%      \iftag{prvDiamond}{T$\Diamond$}{}      \\ \hline      $\Log{D} = \Log{KD}$ & serial & $\Box$,      \iftag{prvBox}{%        \iftag{prvDiamond}{D}{D$\Box$}}{D$\Diamond$}      \\ \hline      $\Log{K4}$ & transitive & $\Box$,      \iftag{prvBox}{4$\Box$}{}%       \iftag{notprvBox,notprvDiamond}{}{, }%      \iftag{prvDiamond}{4$\Diamond$}{}      \\ \hline      $\Log{B} = \Log{KTB}$ & reflexive, & $\Box$,      \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, & $\Box$,      \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{KT5}$ & reflexive, & $\Box$,      \iftag{prvBox}{T$\Box$}{}%      \iftag{notprvBox,notprvDiamond}{}{, }%      \iftag{prvDiamond}{T$\Diamond$}{}\\      & transitive, &      \iftag{prvBox}{5$\Box$}{}%      \iftag{notprvBox,notprvDiamond}{}{, }%      \iftag{prvDiamond}{5$\Diamond$}{}\\      &  euclidean &      \\ \hline    \end{tabular}  \end{center}  \caption{Sequent rules for various modal logics.}  \ollabel{tab:logics-rules}\end{table}\iftag{prvBox}{\begin{ex}  We give a sequent !!{derivation} that shows $\Log{K4} \Proves \Ax{4}$, i.e.,  $\Box!A \lif \Box\Box!A$.  \begin{prooftree}    \Axiom$\Box!A \fCenter \Box!A$    \RightLabel{4$\Box$}    \UnaryInf$\Box!A \fCenter \Box\Box!A$    \RightLabel{\RightR{\lif}}    \UnaryInf$\fCenter \Box!A \lif \Box\Box!A$  \end{prooftree}\end{ex}}{\iftag{prvDiamond}{\begin{ex}  We give a sequent !!{derivation} that shows $\Log{K4} \Proves \Ax{4}$, i.e.,  $\Diamond\Diamond!A \lif \Diamond!A$.  \begin{prooftree}    \Axiom$\Diamond!A \fCenter \Diamond!A$    \RightLabel{4$\Diamond$}    \UnaryInf$\Diamond\Diamond!A \fCenter \Diamond!A$    \RightLabel{\RightR{\lif}}    \UnaryInf$\fCenter \Diamond\Diamond!A \lif \Diamond!A$  \end{prooftree}\end{ex}}{}}\iftag{prvBox}{\iftag{prvDiamond}{% <> and [] primitive\begin{ex}  We give a sequent !!{derivation} that shows $\Log{S5} \Proves \Ax{5}$, i.e.,  $\Diamond!A \lif \Box\Diamond!A$.  \begin{prooftree}    \Axiom$\Diamond!A \fCenter \Diamond!A$    \RightLabel{5$\Box$}    \UnaryInf$\Diamond!A \fCenter \Box\Diamond!A$    \RightLabel{\RightR{\lif}}    \UnaryInf$\fCenter \Diamond!A \lif \Box\Diamond!A$  \end{prooftree}\end{ex}}{% only Box primitive\begin{ex}  We give a sequent !!{derivation} that shows $\Log{S5} \Proves \Ax{5}$, i.e.,  $\Diamond!A \lif \Box\Diamond!A$.  \begin{prooftree}    \Axiom$\Box\lnot!A \fCenter \Box\lnot!A$    \RightLabel{\RightR{\lnot}}    \UnaryInf$\fCenter \Box\lnot!A, \lnot\Box\lnot!A$    \RightLabel{5$\Box$}    \UnaryInf$ \fCenter \Box\lnot!A, \Box\lnot\Box\lnot!A$    \RightLabel{\LeftR{\lnot}}    \UnaryInf$\lnot\Box\lnot!A \fCenter \Box\lnot\Box\lnot!A$    \RightLabel{\RightR{\lif}}    \UnaryInf$\fCenter \lnot\Box\lnot!A \lif \Box\lnot\Box\lnot!A$  \end{prooftree}\end{ex}}}{% only <> prmitive\begin{ex}  We give a sequent !!{derivation} that shows $\Log{S5} \Proves \Ax{5}$, i.e.,  $\Diamond!A \lif \Box\Diamond!A$.  \begin{prooftree}    \Axiom$\Diamond!A \fCenter\Diamond!A$    \RightLabel{\LeftR{\lnot}}    \UnaryInf$\lnot\Diamond !A, \Diamond!A \fCenter $    \RightLabel{5$\Diamond$}    \UnaryInf$\Diamond\lnot\Diamond!A, \Diamond!A \fCenter $    \RightLabel{\RightR{\lnot}}    \UnaryInf$\Diamond!A \fCenter \lnot\Diamond\lnot\Diamond!A$    \RightLabel{\RightR{\lif}}    \UnaryInf$\fCenter \Diamond!A \lif \lnot\Diamond\lnot\Diamond!A$  \end{prooftree}\end{ex}}\begin{ex}The sequent calculus for \Log{S5} is not complete without the \Cut{}rule; e.g., \iftag{prvBox}{$\Diamond\Box !A \lif !A$}{$!A \lif\Box\Diamond !A$}, which is valid in~$\Log{S5}$, has no proofwithout~\Cut. Here is !!a{derivation} using~\Cut:\begin{prooftree}\iftag{prvBox}{\iftag{prvDiamond}{% both [] and <> primitive\Axiom$\Box !A \fCenter \Box!A$\RightLabel{5$\Diamond$}\UnaryInf$\Diamond\Box!A \fCenter \Box!A$\Axiom$!A \fCenter !A$\RightLabel{T$\Box$}\UnaryInf$\Box!A \fCenter !A$\RightLabel{\Cut}\BinaryInf$\Diamond\Box!A \fCenter !A$\RightLabel{\RightR{\lif}}\UnaryInf$\fCenter \Diamond\Box!A \lif !A$}{% only [] primitive\Axiom$\Box !A \fCenter \Box!A$\RightLabel{\RightR{\lnot}}\UnaryInf$\fCenter \Box!A, \lnot\Box!A$\RightLabel{5$\Box$}\UnaryInf$\fCenter \Box!A, \Box\lnot\Box!A$\RightLabel{\RightR{\Exchange}}\UnaryInf$\fCenter \Box\lnot\Box!A, \Box!A$\Axiom$!A \fCenter !A$\RightLabel{T$\Box$}\UnaryInf$\Box!A \fCenter !A$\RightLabel{\Cut}\BinaryInf$ \fCenter \Box\lnot\Box!A, !A$\RightLabel{\LeftR{\lnot}}\UnaryInf$\lnot\Box\lnot\Box!A \fCenter !A$\RightLabel{\RightR{\lif}}\UnaryInf$\fCenter \lnot\Box\lnot\Box!A \lif !A$}}{% only <> primitive\Axiom$!A \fCenter !A$\RightLabel{T$\Diamond$}\UnaryInf$!A \fCenter \Diamond!A$\Axiom$\Diamond !A \fCenter \Diamond!A$\RightLabel{\LeftR{\lnot}}\UnaryInf$\lnot\Diamond!A , \Diamond!A \fCenter$\RightLabel{5$\Diamond$}\UnaryInf$\Diamond\lnot\Diamond!A , \Diamond!A\fCenter$\RightLabel{\RightR{\Exchange}}\UnaryInf$\Diamond!A, \Diamond\lnot\Diamond!A\fCenter $\RightLabel{\Cut}\BinaryInf$\Diamond\lnot\Diamond!A, !A\fCenter $\RightLabel{\RightR{\lnot}}\UnaryInf$!A \fCenter \lnot\Diamond\lnot\Diamond!A$\RightLabel{\RightR{\lif}}\UnaryInf$\fCenter !A \lif \lnot\Diamond\lnot\Diamond!A$}\end{prooftree}\end{ex}\begin{prob}Give sequent !!{derivation}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}