% Part: normal-modal-logic
% Chapter: axioms-systems
% Section: systems-distinct

\documentclass[../../../include/open-logic-section]{subfiles}

\begin{document}

\olfileid{nml}{prf}{dis}

\olsection{Showing Systems are Distinct}

In \olref[prs]{sec} we saw how to prove that two systems of modal
logic are in fact the same system. \olref[snd]{thm:soundness} allows
us to show that two modal systems $\Sigma$ and $\Sigma'$ are distinct,
by finding !!a{formula}~$!A$ such that $\Sigma' \Proves !A$ that fails in
a model of~$\Sigma$.

\begin{prop}
  $\Log{KD} \subsetneq \Log{KT}$
\end{prop}

\begin{proof} This is the syntactic counterpart to the semantic fact
  that all reflexive relations are serial. To show $\Log{KD} \subseteq
  \Log{KT}$ we need to see that $\Log{KD} \Proves !B$ implies
  $\Log{KT} \Proves !B$, which follows from $\Log{KT} \Proves
  \Log{D}$, as shown in
  \olref[prs]{prop:S5facts}\olref[prs]{prop:S5facts-KT-D}.  To show
  that the inclusion is proper, by Soundness
  (\olref[snd]{thm:soundness}), it suffices to exhibit a model of
  \Log{KD} where \Ax{T}, i.e., $\Box p \lif p$, fails (an
  easy task left as an exercise), for then by Soundness $\Log{KD}
  \Proves/ \Box p \lif p$.
\end{proof}

\begin{prop}
  $\Log{KB} \neq \Log{K4}$. 
\end{prop}

\begin{proof}
  We construct a symmetric model where some instance of \Ax{4} fails;
  since obviously the instance is !!{derivable} for \Log{K4} but not
  in \Log{KB}, it will follow $\Log{K4} \nsubseteq \Log{KB}$.
  Consider the symmetric model $\mModel{M}$ of \olref{fig:Bnot4}. Since
  the model is symmetric, \Ax{K} and~\Ax{B} are true in~$\mModel{M}$
  (by \olref[syn][sch]{prop:Kvalid} and
  \olref[frd][acc]{thm:soundschemas}, respectively). However,
  $\mSat/{M}{\Box p \lif \Box\Box p}[w_1]$.
\end{proof}

\begin{figure}[htpb]
  \centering
  \begin{tikzpicture}[modal]
    \node[world] (w1) [label=above:\mFalse{p},
    label={below:$\mSat{{}}{\Box p}$\\ $\mSat/{{}}{\Box\Box p}$}] {$w_1$}; 
    \node[world] (w2) [label=above:\mTrue{p},
      label=below:$\mSat/{{}}{\Box p}$, right=of w1]{$w_2$}; 
    \draw[->, bend left] (w1) to (w2); 
    \draw[->, bend left] (w2) to (w1); 
  \end{tikzpicture}
  \caption{A symmetric model falsifying an instance of \Ax{4}.}
  \ollabel{fig:Bnot4}
\end{figure}
 
\begin{thm}\ollabel{thm:KTBnot45}
  $\Log{KTB} \Proves/ \Log{4}$ and $\Log{KTB} \Proves/ \Log{5}$.
\end{thm}

\begin{proof}
  By \olref[frd][acc]{thm:soundschemas} we know that all instances of
  \Ax{T} and \Ax{B} are true in every reflexive symmetric model
  (respectively). So by soundness, it suffices to find a reflexive
  symmetric model containing a world at which some instance of~\Ax{4}
  fails, and similarly for~\Ax{5}.  We use the same model for both
  claims. Consider the symmetric, reflexive model in
  \olref{fig:KTBnot45}.  Then $\mSat/{M}{\Box p \to \Box \Box
    p}[w_1]$, so \Ax{4} fails at $w_1$. Similarly, $\mSat/{M}{\Diamond
    \lnot p \lif \Box \Diamond \lnot p}[w_2]$, so the instance
  of~\Ax{5} with $!A = \lnot p$ fails at~$w_2$.
\end{proof}

\begin{figure}[htpb]
  \centering
  \begin{tikzpicture}[modal]
    \node[world] (w1) [label={right:\mTrue{p}},
      label={below: $\mSat{{}}{\Box p}$\\
        $\mSat/{{}}{\Box\Box p}$\\
        $\mSat/{{}}{\Diamond\lnot p}$}] {$w_1$};
    \draw[reflexive above] (w1) to (w1);
    \node[world] (w2) [label={right:\mTrue{p}}, label={below:
        $\mSat{{}}{\Diamond\lnot p}$\\
        $\mSat/{{}}{\Box\Diamond\lnot p}$}, right=of w1] {$w_2$} ;
    \draw[reflexive above] (w2) to (w2);
    \node[world] (w3) [label={right:\mFalse{p}},right=of w2] {$w_3$};
    \draw[reflexive above] (w3) to (w3);
    \draw[->, bend left] (w1) to (w2);  
    \draw[->, bend left] (w2) to (w3);  
    \draw[->, bend left] (w3) to (w2);  
    \draw[->, bend left] (w2) to (w1);  
  \end{tikzpicture}
  \caption{The model for \olref{thm:KTBnot45}.}
  \ollabel{fig:KTBnot45}
\end{figure}

\begin{thm}\ollabel{thm:KD5not4}
  $\Log{KD5} \neq \Log{KT4} = \Log{S4}$.
\end{thm}

\begin{proof}
  By \olref[frd][acc]{thm:soundschemas} we know that all instances of
  \Ax{D} and~\Ax{5} are true in all serial euclidean models.
  So  it suffices to find a serial euclidean model containing a world
  at which some instance of~\Ax{4} fails.  Consider the model of
  \olref{fig:KD5not4}, and notice that $\mSat/{M}{\Box p
  \lif \Box\Box p}[w_1]$. 
\end{proof}

\begin{figure}[t]
  \centering
  \begin{tikzpicture}[modal]
    \node[world] (w2) [label=north west:\mTrue{p}]{$w_2$} ;
    \draw[reflexive left] (w2) to (w2);
    \node[world] (w1) [label=right:\mFalse{p},
      label=below:{$\mSat{{}}{\Box p}, \mSat/{{}}{\Box\Box p}$},
      below right=of w2]{$w_1$};
    \node[world] (w3) [label=north east:\mTrue{p}, above right=of w1]{$w_3$} ;
    \draw[reflexive right] (w3) to (w3);
    \node[world] (w4) [label=right:\mFalse{p},above right=of w2]{$w_4$};
    \draw[reflexive above] (w4) to (w4);
    \draw[->] (w1) to (w2);  
    \draw[->] (w1) to (w3);  
    \draw[->, bend left=15] (w2) to (w3);
    \draw[->, bend left=15] (w3) to (w2);  
    \draw[->, bend left=15] (w2) to (w4);
    \draw[->, bend left=15] (w4) to (w2);  
    \draw[->, bend left=15] (w3) to (w4);
    \draw[->, bend left=15] (w4) to (w3);  
  \end{tikzpicture}
  \caption{The model for \olref{thm:KD5not4}.}
  \ollabel{fig:KD5not4}
\end{figure}

\begin{prob}
  Give an alternative proof of \olref[nml][prf][dis]{thm:KD5not4} using a model
  with $3$ worlds.
\end{prob}

\begin{prob}
  Provide a single reflexive transitive model showing that both
  $\Log{KT4} \Proves/ \Ax{B}$ and $\Log{KT4} \Proves/ \Ax{5}$.
\end{prob}

\end{document}