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