% part: intuitionistic-logic
% chapter: semantics
% section: semantic-notions

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

\begin{document}

\olfileid{int}{sem}{sem}

\olsection{Semantic Notions}

\begin{defn}
  We say $!A$ is \emph{true in the model $\mModel{M} = \tuple{W,R,V}$,} $
  \mSat{M}{!A}$, iff $\mSat{M}{!A}[w]$ for all $w \in W$.
  $!A$ is \emph{valid}, $\Entails !A$, iff it is true in all models.
  We say a set of !!{formula}s~$\Gamma$ \emph{entails}~$!A$, $\Gamma
  \Entails !A$, iff for every model~$\mModel{M}$ and every~$w$ such
  that $\mSat{M}{\Gamma}[w]$, $\mSat{M}{!A}[w]$.
\end{defn}

\begin{prop}\ollabel{prop:sat-entails}
  \begin{enumerate}
  \item\ollabel{prop:sat-entails1} If $\mSat{M}{\Gamma}[w]$ and
    $\Gamma \Entails !A$, then $\mSat{M}{!A}[w]$.
  \item\ollabel{prop:sat-entails2} If $\mSat{M}{\Gamma}$ and $\Gamma
    \Entails !A$, then $\mSat{M}{!A}$.
  \end{enumerate}
\end{prop}

\begin{proof}
  \begin{enumerate}
  \item Suppose $\mSat{M}{\Gamma}$. Since $\Gamma \Entails !A$, we
    know that if $\mSat{M}{\Gamma}[w]$, then $\mSat{M}{!A}[w]$. Since
    $\mSat{M}{\Gamma}[u]$ for all every $u \in W$,
    $\mSat{M}{\Gamma}[w]$. Hence $\mSat{M}{!A}[w]$.
  \item Follows immediately from \olref{prop:sat-entails1}.
  \end{enumerate}
\end{proof}


\begin{defn}\ollabel{defn:restrict}
  Suppose $\mModel{M}$ is a relational model and $w \in W$. The
  \emph{restriction} $\mModel{M}_w=\tuple{W_w, R_w, V_w}$
  of~$\mModel{M}$ to~$w$ is given by:
  \begin{align*}
    W_w & = \Setabs{u \in W}{Rwu},\\
    R_w  & = R \cap (W_w)^2, \text{ and}\\
    V_w(p) & = V(p) \cap W_w.
  \end{align*}
\end{defn}

\begin{prop}\ollabel{prop:restrict}
  $\mSat{M}{!A}[w]$ iff $\mSat{M_w}{!A}$.
\end{prop}

\begin{prob}
  Prove \olref[int][sem][sem]{prop:restrict}. 
\end{prob}

\begin{prop}
  Suppose for every model~$\mModel{M}$ such that $\mSat{M}{\Gamma}$,
  $\mSat{M}{!A}$. Then $\Gamma \Entails !A$.
\end{prop}

\begin{proof}
  Suppose that $\mSat{M}{\Gamma}[w]$. By the \olref{prop:restrict}
  applied to every~$!B \in \Gamma$, we have $\mSat{M_w}{\Gamma}$. By
  the assumption, we have $\mSat{M_w}{!A}$. By \olref{prop:restrict}
  again, we get $\mSat{M}{!A}[w]$.
\end{proof}

\end{document}