\begin{frame}[t]{Compactness Theorem}
  \begin{block}{Theorem (Compactness)}
    For every set\/ $\asetforms$ of formulas it holds:
    \begin{talign}
      \text{$\asetforms$ is consistent}
      \;\;\iff\;\;
      \text{every finite subset\/ $\asetformsi{0}\subseteq\asetforms$ is consistent}
    \end{talign}
  \end{block}
  \pause
  
  \begin{block}{Proof of $\Rightarrow$}
    \pause
    Every model for $\asetforms$ also is a model for all subsets $\asetformsi{0}\subseteq\asetforms$.  
  \end{block}\pause{}
  
  \begin{block}{Proof of $\Leftarrow$ (by transposition)} 
    \pause
    \begin{myitemize}[<+->]\setlength{\itemsep}{0.25ex}
      \item
        Suppose that $\asetforms$ is \emph{not} consistent. Then it follows: $\,\asetforms \satisfies \formula{\false}\,$.
      \item
        Then by the completeness theorem:  $\,\asetforms \derives \formula{\false}\,$.
      \item
        Hence there is a derivation $\aDeriv$ of $\formula{\false}$ from premises in $\asetforms$.
      \item
        As $\aDeriv$ is finite, it can only use finitely many premises $\asetformsi{0} \subseteq \asetforms$.
      \item
        Then $\aDeriv$ also shows $\,\asetformsi{0} \derives \formula{\false}\,$.
      \item
        By the soundness theorem it follows: $\,\asetformsi{0} \satisfies \formula{\false}\,$. 
      \item
        Hence the finite subset $\asetformsi{0}$ of $\asetforms$ is \emph{not} consistent.        
    \end{myitemize}
  \end{block} 
\end{frame}