% Part: first-order-logic
% Chapter: completeness
% Section: completeness-theorem

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

\begin{document}

\iftag{FOL}
      {\olfileid{fol}{com}{cth}}
      {\olfileid{pl}{com}{cth}}

\olsection{The Completeness Theorem}

\begin{explain}
Let's combine our results: we arrive at the completeness theorem.
\end{explain}

\begin{thm}[Completeness Theorem]
\ollabel{thm:completeness}
Let $\Gamma$ be a set of !!{sentence}s.  If $\Gamma$ is consistent, it
is satisfiable.
\end{thm}

\begin{proof}
Suppose $\Gamma$ is consistent.\iftag{FOL}{ By
  \olref[hen]{lem:henkin}, there is a saturated consistent set
  $\Gamma' \supseteq \Gamma$.}{} By \olref[lin]{lem:lindenbaum}, there
is a $\Gamma^* \supseteq \iftag{FOL}{\Gamma'}{\Gamma}$ which is
consistent and !!{complete}.
\iftag{FOL}{
  Since $\Gamma' \subseteq \Gamma^*$, for each
  !!{formula}~$!A(x)$, $\Gamma^*$ contains !!a{sentence} of the form
  \iftag{prvEx}
        {$\lexists[x][!A(x)] \lif !A(c)$}
        {$\lnot\lforall[x][!A(x)] \lif \lnot !A(c)$}
  and so $\Gamma^*$ is saturated.  If $\Gamma$
  does not contain~$\eq$, then by}{By}
\olref[mod]{lem:truth},
$\iftag{FOL}{\Sat{M(\Gamma^*)}}{\pSat{v(\Gamma^*)}}{!A}$ iff $!A \in
\Gamma^*$.  From this it follows in particular that for all $!A \in
\Gamma$, $\iftag{FOL}{\Sat{M(\Gamma^*)}}{\pSat{v(\Gamma^*)}}{!A}$, so
$\Gamma$ is satisfiable.\iftag{FOL}{
  If $\Gamma$ does contain~$\eq$,
  then by \olref[ide]{lem:truth}, for all !!{sentence}s~$!A$,
  $\Sat{\equivclass{M}{\approx}}{!A}$ iff $!A \in \Gamma^*$.  In
  particular, $\Sat{\equivclass{M}{\approx}}{!A}$ for all $!A \in
  \Gamma$, so $\Gamma$ is satisfiable.}{}
\end{proof}

\begin{cor}[Completeness Theorem, Second Version]
\ollabel{cor:completeness}
For all $\Gamma$ and !!{sentence}s~$!A$: if $\Gamma \Entails !A$ then
$\Gamma \Proves !A$.
\end{cor}

\begin{proof}
Note that the $\Gamma$'s in \olref{cor:completeness} and
\olref{thm:completeness} are universally quantified.  To make sure we
do not confuse ourselves, let us restate \olref{thm:completeness}
using a different variable: for any set of !!{sentence}s~$\Delta$, if
$\Delta$ is consistent, it is satisfiable.  By contraposition, if
$\Delta$ is not satisfiable, then $\Delta$ is inconsistent.  We will
use this to prove the corollary.

Suppose that $\Gamma \Entails !A$.  Then $\Gamma \cup \{\lnot !A\}$ is
unsatisfiable by \olref[syn][sem]{prop:entails-unsat}.  Taking $\Gamma
\cup \{\lnot !A\}$ as our $\Delta$, the previous version of
\olref{thm:completeness} gives us that $\Gamma \cup \{\lnot !A\}$ is
inconsistent.  By
\iftag{FOL}{%
  \tagrefs{prfAX/{fol:axd:prv:prop:prov-incons},
    prfSC/{fol:seq:prv:prop:prov-incons},
    prfND/{fol:ntd:prv:prop:prov-incons},
    prfTab/{fol:tab:prv:prop:prov-incons}}}{%
  \tagrefs{prfAX/{pl:axd:prv:prop:prov-incons},
    prfSC/{pl:seq:prv:prop:prov-incons},
    prfND/{pl:ntd:prv:prop:prov-incons},
    prfTab/{pl:tab:prv:prop:prov-incons}}},
$\Gamma \Proves !A$.
\end{proof}

\tagprob{FOL}
\begin{prob}
Use \olref[fol][com][cth]{cor:completeness} to prove
\olref[fol][com][cth]{thm:completeness}, thus showing that the two
formulations of the completeness theorem are equivalent.
\end{prob}
\tagendprob

\tagprob{notFOL}
\begin{prob}
Use \olref[pl][com][cth]{cor:completeness} to prove
\olref[pl][com][cth]{thm:completeness}, thus showing that the two
formulations of the completeness theorem are equivalent.
\end{prob}
\tagendprob

\tagprob{FOL}
\begin{prob}
In order for !!a{derivation} system to be complete, its rules must be
strong enough to prove every unsatisfiable set inconsistent.  Which of
the rules of !!{derivation} were necessary to prove completeness?  Are any
of these rules not used anywhere in the proof?  In order to answer
these questions, make a list or diagram that shows which of the rules
of !!{derivation} were used in which results that lead up to the proof of
\olref[fol][com][cth]{thm:completeness}.  Be sure to note any tacit
uses of rules in these proofs.
\end{prob}
\tagendprob

\tagprob{notFOL}
\begin{prob}
In order for !!a{derivation} system to be complete, its rules must be
strong enough to prove every unsatisfiable set inconsistent.  Which of
the rules of !!{derivation} were necessary to prove completeness?  Are any
of these rules not used anywhere in the proof?  In order to answer
these questions, make a list or diagram that shows which of the rules
of !!{derivation} were used in which results that lead up to the proof of
\olref[pl][com][cth]{thm:completeness}.  Be sure to note any tacit
uses of rules in these proofs.
\end{prob}
\tagendprob

\end{document}