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