% part: intuitionistic-logic
% chapter: soundness-completeness
% section: completeness-thm

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

\begin{document}

\olfileid{int}{sc}{cpl}

\olsection{The Completeness Theorem}

\begin{thm}\ollabel{thm:completeness}
  If $\Gamma \Entails !A$ then $\Gamma \Proves !A$.
\end{thm}

\begin{proof}
  We prove the contrapositive: Suppose $\Gamma \Proves/ !A$. Then by
  \olref[lin]{lem:lindenbaum}, there is a prime set~$\Gamma^*
  \supseteq \Gamma$ such that $\Gamma^* \Proves/ !A$. Consider the
  canonical model~$\mModel{M(\Gamma^*)}$ for $\Gamma^*$ as defined in
  \olref[mod]{defn:canonical-model}. For any $!B \in \Gamma$, $\Gamma^*
  \Proves !B$. Note that $\Gamma^*(\emptyseq) = \Gamma^*$. By the Truth
  Lemma (\olref[tru]{lem:truth}), we have
  $\mSat{M(\Gamma^*)}{!B}[\emptyseq]$ for all $!B \in \Gamma$ and
  $\mSat/{M(\Gamma^*)}{!A}[\emptyseq]$. This shows that $\Gamma
  \Entails/ !A$.
\end{proof}

\begin{prob}
  Show that if $!A$ only contains !!{propositional variable}s, $\lor$,
  and~$\land$, then $\Entails/ !A$. Use this to conclude that $\lif$ is
  not definable in intuitionistic logic from $\lor$ and~$\land$. 
\end{prob}
  
\begin{prob}
  By using the completeness theorem prove that if $\Proves !A \lor !B$ then
  $\Proves !A$ or $\Proves !B$. (Hint: Assume $\mSat/{M_1}{!A}$ and
  $\mSat/{M_2}{!B}$ and construct a new model $\mModel{M}$ such that
  $\mSat/{M}{!A \lor !B}$.)
\end{prob}
  
\begin{prob} 
  Show that if $\mModel{M}$ is a relational model using a linear order then
  $\mSat{M}{(!A \lif !B)\lor(!B \lif !A)}$.
\end{prob}

\end{document}