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

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

\begin{document}

\olfileid{nml}{syn}{sch}

\olsection{Schemas and Validity}

\begin{defn}
  A \emph{schema} is a set of !!{formula}s comprising all
  and only the substitution instances of some modal !!{formula}~$!C$, i.e.,
  \[
  \Setabs{!B}{\lexists[!D_1], \dots, \lexists[!D_n] \left(!B =
  \SSubst{!C}{\subst{!D_1}{p_1}, \dots, \subst{!D_n}{p_n}} \right) }.
  \]
  The !!{formula}~$!C$ is called the \emph{characteristic} !!{formula} of
  the schema, and it is unique up to a renaming of the !!{propositional
  variable}s. !!^a{formula}~$!A$ is an \emph{instance} of a schema if
  it is a member of the set.
\end{defn}

It is convenient to denote a schema by the meta-linguistic expression
obtained by substituting `$!A$', `$!B$',~\dots, for the atomic
components of~$!C$. So, for instance, the following denote schemas:
`$!A$', `$!A \lif \Box!A$', `$!A \lif (!B \lif !A)$'. They correspond
to the characteristic !!{formula}s $p$, $p \lif \Box p$, $p \lif (q
\lif p)$. The schema `$!A$' denotes the set of \emph{all}
!!{formula}s.

\begin{defn}
  A schema is \emph{true} in a model if and only if all of its instances
  are; and a schema is \emph{valid} if and only if it is true in every
  model.
\end{defn}

\begin{prop}\ollabel{prop:Kvalid}
  The following schema \Ax{K} is valid
  \begin{equation*}
  \Box(!A \lif !B) \lif (\Box !A \lif \Box !B). \tag{\Ax{K}}
  \end{equation*}
\end{prop}

\begin{proof}
  We need to show that all instances of the schema are true at every
  world in every model. So let $\mModel{M} = \tuple{W,R,V}$ and $w \in
  W$ be arbitrary. To show that a conditional is true at a world we
  assume the antecedent is true to show that the consequent is true as
  well. In this case, let $\mSat{M}{\Box(!A \lif !B)}[w]$ and
  $\mSat{M}{\Box !A}[w]$. We need to show $\mSat{M}{\Box !B}[w]$. So let
  $w'$ be arbitrary such that $Rww'$. Then by the first assumption
  $\mSat{M}{!A \lif !B}[w']$ and by the second assumption
  $\mSat{M}{!A}[w']$. It follows that $\mSat{M}{!B}[w']$. Since $w'$
  was arbitrary, $\mSat{M}{\Box !B}[w]$.
\end{proof}

\begin{prop}\ollabel{prop:Dual-valid}
  The following schema \Dual{} is valid
  \begin{equation*}
  \Diamond !A \liff \lnot\Box\lnot !A. \tag{\Dual}
  \end{equation*}
\end{prop}

\begin{proof}
  Exercise.
\end{proof}

\begin{prob}
  Prove \olref[nml][syn][sch]{prop:Dual-valid}.
\end{prob}

\begin{prop}\ollabel{prop:soundMP}
  If $!A$ and $!A \lif !B$ are true at a world in a model
  then so is $!B$. Hence, the valid !!{formula}s are closed under
  modus ponens.
\end{prop}

\begin{prop}\ollabel{prop:valid-instances}
  !!^a{formula}~$!A$ is valid iff all its substitution instances
  are. In other words, a schema is valid iff its characteristic
  !!{formula} is.
\end{prop}

\begin{proof}
  The ``if'' direction is obvious, since $!A$ is a substitution
  instance of itself.

  To prove the ``only if'' direction, we show the following: Suppose
  $\mModel{M} = \tuple{W, R, V}$ is a modal model, and $!B \ident
  \SSubst{!A}{\subst{!D_1}{p_1},\dots,\subst{!D_n}{p_n}}$ is a
  substitution instance of~$!A$. Define $\mModel{M'} = \tuple{W, R,
    V'}$ by $V'(p_i) = \Setabs{w}{\mSat{M}{!D_i}[w]}$.  Then
  $\mSat{M}{!B}[w]$ iff $\mSat{M'}{!A}[w]$, for any~$w \in W$. (We
  leave the proof as an exercise.) Now suppose that $!A$ was valid,
  but some substitution instance $!B$ of~$!A$ was not valid. Then for
  some $\mModel{M} = \tuple{W, R, V}$ and some $w \in W$,
  $\mSat/{M}{!B}[w]$. But then $\mSat/{M'}{!A}[w]$ by the claim, and
  $!A$ is not valid, a contradiction.
\end{proof}

\begin{prob}
  Prove the claim in the ``only if'' part of the proof of
  \olref[nml][syn][sch]{prop:valid-instances}. (Hint: use induction
  on~$!A$.)
\end{prob}

Note, however, that it is not true that a schema is true in a model
iff its characteristic formula is. Of course, the ``only if''
direction holds: if every instance of $!A$ is true in~$\mModel{M}$,
$!A$~itself is true in~$\mModel{M}$. But it may happen that $!A$ is
true in~$\mModel{M}$ but some instance of~$!A$ is false at some world
in~$\mModel{M}$. For a very simple counterexample consider~$p$ in a
model with only one world~$w$ and $V(p) = \{w\}$, so that $p$ is true
at~$w$. But $\lfalse$ is an instance of~$p$, and not true at~$w$.

\begin{prob}
  Show that none of the following !!{formula}s are valid:
  \begin{enumerate}
    \item[\Ax{D}:] \quad $\Box p \lif \Diamond p$;
    \item[\Ax{T}:] \quad $\Box p \lif p$;
    \item[\Ax{B}:] \quad $p \lif \Box\Diamond p$;
    \item[\Ax{4}:] \quad $\Box p \lif \Box \Box p$;
    \item[\Ax{5}:] \quad $\Diamond p \lif \Box \Diamond
      p$.
  \end{enumerate}
\end{prob}

\begin{table}[t]
    \centering
    \begin{tabular}{| l || l |}
      \hline
      {\emph{Valid Schemas}} & {\emph{Invalid Schemas}} \\
      \hline\hline
      $\Box(!A \lif !B) \lif (\Diamond !A \lif \Diamond !B)$
      & $\Box (!A \lor !B) \lif (\Box !A \lor \Box !B)$ \\
      $\Diamond (!A \lif !B) \lif (\Box !A \lif \Diamond
      !B)$
      & $(\Diamond !A \land \Diamond !B) \lif \Diamond (!A
      \land !B)$\\
      $\Box (!A \land !B) \liff (\Box !A \land \Box !B)$
      & $!A \lif \Box !A$ \\
      $\Box !A \lif \Box (!B \lif !A)$
      & $\Box \Diamond !A \lif !B$ \\
      $\lnot \Diamond !A \lif \Box (!A \lif !B)$
      & $\Box \Box !A \lif \Box !A$ \\
      $\Diamond (!A \lor !B) \liff (\Diamond !A \lor
      \Diamond !B)$
      & $\Box \Diamond !A \lif \Diamond \Box !A$. \\
      \hline
    \end{tabular}
    \caption{Valid and (or?) invalid schemas.}
    \ollabel{tab:valid-invalidSchemas}
\end{table}

\begin{prob}%\ollabel{ex:in/validSchemas}
  Prove that the schemas in the first column of
  \olref[nml][syn][sch]{tab:valid-invalidSchemas} are valid and those in
  the second column are not valid.
\end{prob}

\begin{prob}
  Decide whether the following schemas are valid or invalid:
  \begin{enumerate}
  \item $(\Diamond !A \lif \Box !B) \lif (\Box !A \lif \Box
    !B)$;
  \item $\Diamond(!A \lif !B) \lor \Box(!B \lif !A)$.
  \end{enumerate}
\end{prob}

\begin{prob}
  For each of the following schemas find a model $\mModel{M}$ such
  that every instance of the !!{formula} is true in $\mModel{M}$:
  \begin{enumerate}
  \item $p \lif \Diamond\Diamond p$;
  \item $\Diamond p \lif \Box p$.
  \end{enumerate}
\end{prob}

\end{document}