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