% Part: normal-modal-logic
% Chapter: syntax-and-semantics
% Section: modal-validity

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

\begin{document}

\olfileid{nml}{syn}{val}

\olsection{Validity}

\begin{explain}
  !!^{formula}s that are true in all models, i.e., true at every world
  in every model, are particularly interesting. They represent those
  modal propositions which are true regardless of how $\Box$ and
  $\Diamond$ are interpreted, as long as the interpretation is
  ``normal'' in the sense that it is generated by some accessibility
  relation on possible worlds. We call such !!{formula}s
  \emph{valid}. For instance, $\Box(p \land q) \lif \Box p$ is
  valid. Some !!{formula}s one might expect to be valid on the basis
  of the alethic interpretation of $\Box$, such as $\Box p \lif p$,
  are not valid, however.  Part of the interest of relational models
  is that different interpretations of $\Box$ and $\Diamond$ can be
  captured by different kinds of accessibility relations. This
  suggests that we should define validity not just relative to
  \emph{all} models, but relative to all models \emph{of a certain
    kind}. It will turn out, e.g., that $\Box p \lif p$ is true in all
  models where every world is accessible from itself, i.e., $R$ is
  reflexive. Defining validity relative to classes of models enables
  us to formulate this succinctly: $\Box p \lif p$ is valid in the
  class of reflexive models.
\end{explain}

\begin{defn}
  !!^a{formula}~$!A$ is \emph{valid} in a class $\mClass{C}$ of
  models if it is true in every model in~$\mClass{C}$ (i.e., true at
  every world in every model in~$\mClass{C}$). If $!A$ is valid
  in~$\mClass{C}$, we write $\mClass{C} \Entails !A$, and we
  write $\Entails !A$ if $!A$ is valid in the class of
  \emph{all} models.
\end{defn}

\begin{prop}\ollabel{prop:subset-class}
  If $!A$ is valid in $\mClass{C}$ it is also valid in each class
  $\mClass{C}' \subseteq \mClass{C}$.
\end{prop}

\begin{prop}\ollabel{prop:Nec-rule}
  If $!A$ is valid, then so is $\Box!A$. 
\end{prop}

\begin{proof}
  Assume $\Entails !A$. To show $\Entails \Box!A$ let $\mModel{M} =
  \tuple{W, R, V}$ be a model and $w \in W$. If $Rww'$ then
  $\mSat{M}{!A}[w']$, since $!A$ is valid, and so also
  $\mSat{M}{\Box!A}[w]$. Since $\mModel{M}$ and $w$ were
  arbitrary, $\Entails \Box!A$.
\end{proof}

\begin{prob}
  Show that the following are valid:
  \begin{enumerate}
  \item $\Box p \lif \Box (q \lif p)$;
  \item $\Box \lnot \lfalse$;
  \item $\Box p \lif (\Box q \lif \Box p)$.
  \end{enumerate}
\end{prob}

\begin{prob}
  Show that $!A \lif \Box!A$ is valid in the class $\mClass{C}$ of
  models $\mModel{M} = \tuple{W, R, V}$ where $W = \{w\}$. Similarly,
  show that $!B \lif \Box !A$ and $\Diamond !A \lif !B$ are valid in
  the class of models $\mModel{M} = \tuple{W, R, V}$ where
  $R = \emptyset$.
\end{prob}

\end{document}