\begin{frame}{First Incompleteness Theorem}
  \begin{goal}{}
    Desirable: an \emph{axiomatizable first-order theory} $\derives$ for $\standardN$:
    \begin{itemize}
    \pause
      \item
        an effective list \colemph{$\mathcal{A}$} of axioms (pred.\ logic $\pair{\asetfuncs}{\asetpreds}$-formulas)
    \pause
      \item
        finitely many rules \colemph{$\mathcal{R}$}
    \pause
      \item 
        $\sderives\:\aform\;$ means: 
        \parbox[t]{0.62\textwidth}{
          there is a derivation of $\aform$ from axioms \colemph{$\mathcal{A}$}\\
          that only used rules from \colemph{$\mathcal{R}$}
        } 
    \end{itemize}
    \pause\medskip
    that is sound and complete for $\standardN$:
    \begin{talign}
      \standardN \satisfies \aform \;\;\Longleftrightarrow\;\; \derives \aform  
      \hspace*{6ex}
      \text{(for all $\pair{\asetfuncs}{\asetpreds}$-formulas $\aform$)}
    \end{talign}
  \end{goal}
  \pause\medskip
  
  Yet it turned out that this is impossible.
  \pause
  \begin{block}{First incompleteness theorem (G\"{o}del, 1931)}
    Every axiomatizable and sound theory $\derives$ of first-order logic
    for number theory with language $\pair{\asetfuncs}{\asetpreds}$
    is \alert{incomplete}. That is,
    it contains sentences $\aform$ that are \alert{true} in $\standardN$, \alert{but unprovable} in $\sderives\,$:
    \begin{talign}
      \standardN \satisfies \aform \, , \;\;\text{yet}\;\;\;\; \sderivesnot \:\aform  
    \end{talign} 
  \end{block}
\end{frame}