\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}