\begin{frame}{Undecidability of Validity and Provability}
  \begin{block}{Theorem (Church, Turing, 1936/37)}
    The \emph{validity problem} in predicate logic is \alert{undecidable}.
    \medskip
    
    There cannot be a program that, given any formula $\aform$,
    decides whether or not $\;\ssatisfies\: \aform\,$ holds.
  \end{block} 
  \pause\medskip

  Using the soundness and completeness theorem we obtain:
  %
  \begin{block}{Corollary (Undecidability of Provability)}
    The \emph{provability problem} in predicate logic is \alert{undecidable}.
    \medskip
    
    There cannot be a program that, given any formula $\aform$,
    decides whether or not $\;\sderives\: \aform\,$ holds.
  \end{block}
  \begin{itemize}
  \pause
    \item
      limits the power of theorem provers
  \pause
    \item  
      building better theorem provers is an open-ended endeavour
      (creativity will always be needed)
  \end{itemize}
\end{frame}