37/160
\begin{frame}[t]{Consistency Theorem (Proof)}
\begin{block}{Theorem (Consistency)}
\begin{malign}
\exists \model{\amodel}\exists \saluf \;\; \model{\amodel} \satisfieslookup{\saluf} \asetforms
\;\; &\iff\;\;
\asetforms \derivesnot \formula{\false}
\end{malign}
\end{block}
\pause

\begin{block}{Proof of $\Rightarrow$}
\begin{itemize}
\pause
\item
Let $\model{\amodel}$ and $\saluf$ such that $\model{\amodel} \satisfieslookup{\saluf} \asetforms$.
\pause
\item
Note that $\model{\amodel} \satisfiesnotlookup{\saluf} \formula{\false}$.  %(actually, in no model $\formula{\false}$ is true).
\pause
\item
We conclude $\asetforms \satisfiesnot \formula{\false}$.
\pause
\item
Then by the soundness theorem: $\;\asetforms \derivesnot \formula{\false}\;$.
\end{itemize}
\end{block}
\pause

\begin{block}{Proof of $\Leftarrow$}
\begin{itemize}
\pause
\item
Suppose that $\;\asetforms \derivesnot \formula{\false}\;$.
\pause
\item
Then by the completeness theorem: $\;\asetforms \satisfiesnot \formula{\false}\;$.
\pause
\item
Hence there are $\model{\amodel}$ and $\saluf$ such that
$\model{\amodel} \satisfieslookup{\saluf} \asetforms$ and
$\model{\amodel} \satisfiesnotlookup{\saluf} \false$.
\pause
\item
Hence $\asetforms$ is consistent.
\end{itemize}
\end{block}
\end{frame}