complete-consistent-sets.tex

% Part: first-order-logic
% Chapter: completeness
% Section: complete-sets

% Definition of complete consistent sets. Properties of complete sets required
% for completeness proved are in provability.tex in the
% chapter on the proof system used.

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

\begin{document}

\olfileid{fol}{com}{ccs}
\olsection{Complete Consistent Sets of \usetoken{P}{sentence}}

\begin{defn}[Complete set]
\ollabel{def:complete-set} A set~$\Gamma$ of !!{sentence}s is
\emph{!!{complete}} iff for any !!{sentence}~$!A$, either $!A \in
\Gamma$ or $\lnot !A \in \Gamma$.
\end{defn}

\begin{explain}
!!^{complete} sets of sentences leave no questions unanswered. For
any !!{sentence}~$A$, $\Gamma$ ``says'' if $!A$ is true or false.  The
importance of !!{complete} sets extends beyond the proof of the
completeness theorem. A theory which is !!{complete} and
axiomatizable, for instance, is always decidable.
\end{explain}

\begin{explain}
!!^{complete} consistent sets are important in the completeness proof
since we can guarantee that every consistent set of
!!{sentence}s~$\Gamma$ is contained in a !!{complete} consistent
set~$\Gamma^*$.  !!^a{complete} consistent set contains, for each
!!{sentence}~$!A$, either $!A$ or its negation $\lnot !A$, but not
both. This is true in particular for atomic !!{sentence}s, so from
!!a{complete} consistent set in a language suitably expanded by
!!{constant}s, we can construct a !!{structure} where the
interpretation of !!{predicate}s is defined according to which atomic
!!{sentence}s are in~$\Gamma^*$. This !!{structure} can then be shown
to make all !!{sentence}s in~$\Gamma^*$ (and hence also all those
in~$\Gamma$) true. The proof of this latter fact requires that $\lnot
!A \in \Gamma^*$ iff $!A \notin \Gamma^*$, $(!A \lor !B) \in \Gamma^*$
iff $!A \in \Gamma^*$ or $!B \in \Gamma^*$, etc.
\end{explain}

\begin{prop}
\ollabel{prop:ccs}
Suppose $\Gamma$ is !!{complete} and consistent. Then:
\begin{enumerate}
\item \ollabel{prop:ccs-prov-in} If $\Gamma \Proves !A$, then $!A \in
  \Gamma$.

\tagitem{prvAnd}{\ollabel{prop:ccs-and} $(!A \land !B) \in \Gamma$
  iff both $!A \in \Gamma$ and $!B \in \Gamma$.}{}

\tagitem{prvOr}{\ollabel{prop:ccs-or} $(!A \lor !B) \in \Gamma$ iff
  either $!A \in \Gamma$ or $!B \in \Gamma$.}{}

\tagitem{prvIf}{\ollabel{prop:ccs-if} $(!A \lif !B) \in \Gamma$ iff
  either $!A \notin \Gamma$ or $!B \in \Gamma$.}{}
\end{enumerate}
\end{prop}

\begin{proof}
Let us suppose for all of the following that $\Gamma$ is !!{complete} and
consistent.
\begin{enumerate}
\item If $\Gamma \Proves !A$, then $!A \in \Gamma$.

Suppose that $\Gamma \Proves !A$. Suppose to the contrary that $!A
\notin \Gamma$. Since $\Gamma$ is !!{complete}, $\lnot !A \in \Gamma$.
By
\tagrefs{prfSC/{fol:seq:prv:prop:explicit-inc},prfND/{fol:ntd:prv:prop:explicit-inc}},
$\Gamma$ is inconsistent. This contradicts the assumption that
$\Gamma$ is consistent. Hence, it cannot be the case that $!A \notin
\Gamma$, so $!A \in \Gamma$.

\tagitem{defAnd}{}{%
\iftag{probAnd}{Exercise.}{%
$(!A \land !B) \in \Gamma$ iff both $!A \in \Gamma$ and $!B \in \Gamma$:

For the forward direction, suppose $(!A \land !B) \in \Gamma$. Then
$\Gamma \Proves !A \land !B$. By
\tagrefs{prfSC/{fol:seq:prv:prop:provability-land-left},prfND/{fol:ntd:prv:prop:provability-land-left}},
$\Gamma \Proves !A$ and $\Gamma \Proves !B$. By
\olref{prop:ccs-prov-in}, $!A \in \Gamma$ and $!B \in \Gamma$, as
required.

For the reverse direction, let $!A \in \Gamma$ and $!B \in
\Gamma$. Then $\Gamma \Proves !A$ and $\Gamma \Proves !B$. By
\tagrefs{prfSC/{fol:seq:prv:prop:provability-land-right},prfND/{fol:ntd:prv:prop:provability-land-right}},
$\Gamma \Proves !A \land !B$. By \olref{prop:ccs-prov-in}, $(!A \land
!B) \in \Gamma$.}}

\tagitem{defOr}{}{%
\iftag{probOr}{Exercise.}{%
$(!A \lor !B) \in \Gamma$ iff either $!A \in \Gamma$ or $!B \in \Gamma$.

For the contrapositive of the forward direction, suppose that $!A
\notin \Gamma$ and $!B \notin \Gamma$. We want to show that $(!A \lor
!B) \notin \Gamma$. Since $\Gamma$ is !!{complete}, $\lnot !A \in
\Gamma$ and $\lnot !B \in \Gamma$.  By
\tagrefs{prfSC/{fol:seq:prv:prop:provability-lnot},prfND/{fol:ntd:prv:prop:provability-lnot}},
$\Gamma \cup \{!A\} \Proves \lfalse$ and $\Gamma \cup \{!B\} \Proves
\lfalse$.  By
\tagrefs{prfSC/{fol:seq:prv:prop:provability-lor-left},prfND/{fol:ntd:prv:prop:provability-lor-left}} (taking $\lfalse$ for $C$),
$\Gamma \cup \{(!A \lor !B)\}$ is inconsistent. Hence, $(!A \lor !B)
\notin \Gamma$, as required.

For the reverse direction, suppose that $!A \in \Gamma$ or $!B \in
\Gamma$. Then $\Gamma \Proves !A$ or $\Gamma \Proves !B$. By
\tagrefs{prfSC/{fol:seq:prv:prop:provability-lor-right},prfND/{fol:ntd:prv:prop:provability-lor-right}},
$\Gamma \Proves !A \lor !B$. By \olref{prop:ccs-prov-in}, $(!A \lor
!B) \in \Gamma$, as required.}}

\tagitem{defIf}{}{%
\iftag{probIf}{Exercise.}{%
$(!A \lif !B) \in \Gamma$ iff either $!A \notin \Gamma$ or $!B \in \Gamma$:

For the forward direction, let $(!A \lif !B) \in \Gamma$, and suppose
to the contrary that $!A \in \Gamma$ and $!B \notin \Gamma$. On these
assumptions, $\Gamma \Proves !A \lif !B$ and $\Gamma \Proves !A$. By
\tagrefs{prfSC/{fol:seq:prv:prop:provability-mp},prfND/{fol:ntd:prv:prop:provability-mp}},
$\Gamma \Proves !B$. But then by \olref{prop:ccs-prov-in}, $!B \in
\Gamma$, contradicting the assumption that $!B \notin \Gamma$.

For the reverse direction, first consider the case where $!A \notin
\Gamma$. Since $\Gamma$ is !!{complete}, $\lnot !A \in \Gamma$ and
hence $\Gamma \Proves \lnot !A$. By
\tagrefs{prfSC/{fol:seq:prv:prop:provability-lif},prfND/{fol:ntd:prv:prop:provability-lif}},
$\Gamma \Proves !A \lif !B$. Again by \olref{prop:ccs-prov-in}, we get
that $(!A \lif !B) \in \Gamma$, as required.

Now consider the case where $!B \in \Gamma$. Then $\Gamma \Proves !B$
and by
\tagrefs{prfSC/{fol:seq:prv:prop:provability-lif},prfND/{fol:ntd:prv:prop:provability-lif}},
$\Gamma \Proves !A \lif !B$. By \olref{prop:ccs-prov-in}, $(!A \lif
!B) \in \Gamma$.}}
\end{enumerate}
\end{proof}

\begin{prob}
Complete the proof of \olref[fol][com][ccs]{prop:ccs}.
\end{prob}

\end{document}