% Part: first-order-logic
% Chapter: syntax-and-semantics
% Section: Semantic Notions

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

\begin{document}

\olfileid{fol}{syn}{sem}
\olsection{Semantic Notions}

\begin{explain}
Given the definition of !!{structure}s for first-order languages, we can
define some basic semantic properties of and relationships between
sentences.  The simplest of these is the notion of \emph{validity} of
a sentence.  A sentence is valid if it is satisfied in every
!!{structure}.  Valid sentences are those that are satisfied regardless of
how the non-logical symbols in it are interpreted.  Valid sentences
are therefore also called \emph{logical truths}---they are true, i.e.,
satisfied, in any !!{structure} and hence their truth depends only on the
logical symbols occurring in them and their syntactic !!{structure}, but not
on the non-logical symbols or their interpretation.
\end{explain}

\begin{defn}[Validity]
A sentence $!A$ is \emph{valid}, $\Entails !A$, iff $\Sat{M}{!A}$ for every
!!{structure}~$\Struct M$.
\end{defn}

\begin{defn}[Entailment]
A set of sentences~$\Gamma$ \emph{entails} a sentence~$!A$, $\Gamma
\Entails !A$, iff for every !!{structure}~$\Struct M$ with
$\Sat{M}{\Gamma}$, $\Sat{M}{!A}$.
\end{defn}


\begin{defn}[Satisfiability]
A set of sentences~$\Gamma$ is \emph{satisfiable} if $\Sat{M}{\Gamma}$
for some !!{structure}~$\Struct M$.  If $\Gamma$ is not satisfiable it is
called \emph{unsatisfiable}.
\end{defn}

\begin{prop}
A sentence $!A$ is valid iff $\Gamma \Entails !A$ for every set of
sentences~$\Gamma$.
\end{prop}

\begin{proof}
For the forward direction, let $!A$ be valid, and let $\Gamma$ be a
set of sentences. Let $\Struct M$ be !!a{structure} so that
$\Sat{M}{\Gamma}$. Since $!A$ is valid, $\Sat{M}{!A}$, hence $\Gamma
\Entails !A$.

For the contrapositive of the reverse direction, let $!A$ be invalid,
so there is !!a{structure}~$\Struct M$ with $\Sat/{M}{!A}$. When $\Gamma
= \{ \ltrue \}$, since $\ltrue$ is valid, $\Sat{M}{\Gamma}$. Hence,
there is !!a{structure}~$\Struct M$ so that $\Sat{M}{\Gamma}$ but
$\Sat/{M}{!A}$, hence $\Gamma$ does not entail $!A$.
\end{proof}

\begin{prop}
\ollabel{prop:entails-unsat}
$\Gamma \Entails !A$ iff $\Gamma \cup \{\lnot !A\}$ is unsatisfiable.
\end{prop}

\begin{proof}
For the forward direction, suppose $\Gamma \Entails !A$ and suppose to the
contrary that there is !!a{structure}~$\Struct M$ so that $\Sat{M}{\Gamma
  \cup \{ \lnot !A \}}$. Since $\Sat{M}{\Gamma}$ and $\Gamma \Entails
!A$, $\Sat{M}{!A}$. Also, since $\Sat{M}{\Gamma\cup \{ \lnot !A \}}$,
$\Sat{M}{\lnot !A}$, so we have both $\Sat{M}{!A}$ and $\Sat/{M}{!A}$,
a contradiction. Hence, there can be no such !!{structure}~$\Struct M$, so
$\Gamma \cup \{ \lnot !A \}$ is unsatisfiable.

For the reverse direction, suppose $\Gamma \cup \{ \lnot !A \}$ is
unsatisfiable. So for every !!{structure}~$\Struct M$, either
$\Sat/{M}{\Gamma}$ or $\Sat{M}{!A}$. Hence, for every !!{structure}
$\Struct M$ with $\Sat{M}{\Gamma}$, $\Sat{M}{!A}$, so $\Gamma \Entails
!A$.
\end{proof}

\begin{prob}
\begin{enumerate}
\item Show that $\Gamma \Entails \bot$ iff $\Gamma$ is unsatisfiable.
\item Show that $\Gamma \cup \{!A\} \Entails \bot$ iff $\Gamma \Entails \lnot !A$.
\item Suppose $c$ does not occur in $!A$ or $\Gamma$.  Show that
  $\Gamma \Entails \lforall[x][!A]$ iff $\Gamma \Entails
  \Subst{!A}{c}{x}$.
\end{enumerate}
\end{prob}

\begin{prop}
If $\Gamma \subseteq \Gamma'$ and $\Gamma \Entails !A$, then $\Gamma'
\Entails !A$.
\end{prop}

\begin{proof}
Suppose that $\Gamma \subseteq \Gamma'$ and $\Gamma \Entails !A$. Let
$\Struct M$ be a structure such that $\Sat{M}{\Gamma'}$; then $\Sat{M}{\Gamma}$,
and since $\Gamma \Entails !A$, we get that $\Sat{M}{!A}$. Hence,
whenever $\Sat{M}{\Gamma'}$, $\Sat{M}{!A}$, so $\Gamma' \Entails !A$.
\end{proof}


\begin{thm}[Semantic Deduction Theorem]
\ollabel{thm:sem-deduction}
$\Gamma \cup \{!A\} \Entails !B$ iff $\Gamma \Entails !A \lif !B$.
\end{thm}

\begin{proof}
For the forward direction, let $\Gamma \cup \{ !A \} \Entails !B$ and
let $\Struct M$ be !!a{structure} so that $\Sat{M}{\Gamma}$. If
$\Sat{M}{!A}$, then $\Sat{M}{\Gamma \cup \{ !A \} }$, so since $\Gamma
\cup \{ !A \}$ entails $!B$, we get $\Sat{M}{!B}$. Therefore,
$\Sat{M}{!A \lif !B}$, so $\Gamma \Entails !A \lif !B$.

For the reverse direction, let $\Gamma \Entails !A \lif !B$ and
$\Struct M$ be !!a{structure} so that $\Sat{M}{\Gamma \cup \{ !A
  \}}$. Then $\Sat{M}{\Gamma}$, so $\Sat{M}{!A \lif !B}$, and since
$\Sat{M}{!A}$, $\Sat{M}{!B}$. Hence, whenever $\Sat{M}{\Gamma \cup \{
  !A \} }$, $\Sat{M}{!B}$, so $\Gamma \cup \{ !A \} \Entails !B$.
\end{proof}

\begin{prop}\ollabel{prop:quant-terms}
  Let $\Struct{M}$ be !!a{structure}, and $!A(x)$ !!a{formula} with
  one free variable~$x$, and $t$~a closed term. Then:
  \begin{tagenumerate}{prvEx,prvAll}
    \tagitem{prvEx}{$!A(t) \Entails \lexists[x][!A(x)]$}{}
    \tagitem{prvAll}{$\lforall[x][!A(x)] \Entails !A(t)$}{}
  \end{tagenumerate}
\end{prop}

\begin{proof}
  \begin{tagenumerate}{prvEx,prvAll}
    \tagitem{prvEx}{%
      \iftag{probEx}{Exercise.}{Suppose $\Sat{M}{!A(t)}$. Let $s$ be a
        variable assignment with $s(x) = \Value{t}{M}$. Then
        $\Sat{M}{!A(t)}[s]$ since $!A(t)$ is !!a{sentence}. By
        \olref[ext]{prop:ext-formulas}, $\Sat{M}{!A(x)}[s]$. By
        \olref[ass]{prop:sat-quant},
        $\Sat{M}{\lexists[x][!A(x)]}$.}}{}
    \tagitem{prvAll}{%
      \iftag{probAll}{Exercise.}{Suppose
        $\Sat{M}{\lforall[x][!A(x)]}$. Let $s$ be a variable
        assignment with $s(x) = \Value{t}{M}$. By
        \olref[ass]{prop:sat-quant}, $\Sat{M}{!A(x)}[s]$.  By
        \olref[ext]{prop:ext-formulas}, $\Sat{M}{!A(t)}[s]$. By
        \olref[ass]{prop:sentence-sat-true}, $\Sat{M}{!A(t)}$ since
        $!A(t)$ is !!a{sentence}.}}{}
  \end{tagenumerate}
\end{proof}

\begin{probtag}{probEx,probAll}
  Complete the proof of \olref[fol][syn][sem]{prop:quant-terms}.
\end{probtag} 

\end{document}