\begin{frame}{Second Incompleteness Theorem}
  \begin{block}{Theorem (G\"{o}del, von Neumann, 1930-31)}
    For every axiomatizable theory $\derives$ of first-order logic
    for number theory with language $\pair{\asetfuncs}{\asetpreds}$
    \begin{itemize}
      \item 
        that is rich enough to express its own consistency by a sentence $\aform_{\sderives}$
    \end{itemize}
    \pause
    it holds that either:
    \begin{itemize}
      \item
        $\derives \!\false$ \tabto{1.3cm} ($\;\sderives$ is inconsistent\;)\;, or
      \item
        $\derivesnot \!\aform_{\sderives}\;$ \tabto{1.3cm} (\;hence $\;\sderives$ is incomplete\;) 
    \end{itemize}
  \end{block}
  \pause\medskip
  
  \begin{itemize}
    \item[$\Longrightarrow$]
      First-order theories (based on predicate logic) of number theory
      are not able to prove their own consistency.
  \end{itemize}
\end{frame}