\documentclass{beamer}

\mode<presentation>
{
  %\usetheme{Frankfurt}
  %\usetheme{Boadilla}
  % or ...

  %\useoutertheme[subsection=false]{smoothbars}
  \useinnertheme{default}
  %\useinnertheme[shadow=false]{rounded}
  %\usecolortheme{orchid}
  %\usecolortheme{whale}
  \usecolortheme{albatross}

  \setbeamerfont{block title}{size={}}

  %\setbeamercovered{transparent=30}
  % or whatever (possibly just delete it)

  \setbeamersize{text margin left=1.5cm, text margin right=1.5cm}

  \setbeamercolor{alerted text}{fg=yellow}
}

\usepackage[english]{babel}
% or whatever

\usepackage[latin1]{inputenc}
% or whatever

\usepackage{times}
\usepackage[T1]{fontenc}
% Or whatever. Note that the encoding and the font should match. If T1
% does not look nice, try deleting the line with the fontenc.

\usepackage{mt}
\usepackage{covers}

\theoremstyle{plain}
\newtheorem{conjecture}[theorem]{Conjecture}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{claim}[theorem]{Claim}

\theoremstyle{remark}
\newtheorem{remark}{Remark}[section]

\usepackage[all,cmtip]{xy}
\providecommand{\epar}{\ar@{->>}}
\providecommand{\embar}{\ar@{^{(}->}}

\CompileMatrices

\title % (optional, use only with long paper titles)
{Introduction to 3TP3:\\Hilbert's Programme and G\"{o}del's Incompleteness Theorems}

\author%[Author, Another] % (optional, use only with lots of authors)
{Martin Bays}
% - Use the \inst{?} command only if the authors have different
%   affiliation.

\institute[McMaster University] % (optional, but mostly needed)

%\date[07-12-14] % (optional)
%{Friday}

%\subject{Talks}
% This is only inserted into the PDF information catalog. Can be left
% out. 



% If you have a file called "university-logo-filename.xxx", where xxx
% is a graphic format that can be processed by latex or pdflatex,
% resp., then you can add a logo as follows:

% \pgfdeclareimage[height=0.5cm]{university-logo}{university-logo-filename}
% \logo{\pgfuseimage{university-logo}}



% Delete this, if you do not want the table of contents to pop up at
% the beginning of each subsection:
%\AtBeginSubsection[]
%{
  %\begin{frame}<beamer>
    %\frametitle{Outline}
    %\tableofcontents[currentsection,currentsubsection]
  %\end{frame}
%}


% If you wish to uncover everything in a step-wise fashion, uncomment
% the following command: 

%\beamerdefaultoverlayspecification{<+->}

% changemargin: nabbed from
% http://newsgroups.derkeiler.com/Archive/Comp/comp.text.tex/2006-06/msg00677.html 
\newenvironment{changemargin}[2]{%
\begin{list}{}{%
\setlength{\topsep}{0pt}%
\setlength{\leftmargin}{#1}%
\setlength{\rightmargin}{#2}%
\setlength{\listparindent}{\parindent}%
\setlength{\itemindent}{\parindent}%
\setlength{\parsep}{\parskip}%
}%
\item[]}{\end{list}}

\begin{document}
\begin{frame}
  \titlepage
\end{frame}

\begin{frame}
  \frametitle{Hilbert's 2nd problem}
  In the second of David Hilbert's famous series of problems from his
  1900 address to the ICM, he set forth the problem of proving consistency of
  axioms for analysis:

  \begin{quote}
    ``When we are engaged in investigating the
    foundations of a science, we must set up a system of axioms which contains
    an exact and complete description of the relations subsisting between the
    elementary ideas of that science.
    %The axioms so set up are at the same time the definitions of those
    %elementary ideas; and no statement within the realm of the science whose
    %foundation we are testing is held to be correct unless it can be derived
    %from those axioms by means of a finite number of logical steps.
    [...] above all I wish to designate the following as the most
    important among the numerous questions which can be asked with regard to the
    axioms: To prove that they are not contradictory, that is, that a definite
    number of logical steps based upon them can never lead to contradictory
    results. [...] I am convinced that it must be possible to find a direct
    proof for the compatibility of the arithmetical axioms''
  \end{quote}
\end{frame}

\begin{frame}
  \frametitle{Consistency}
  In modern terminology:
  \begin{itemize}
    \item A \defnstyle{formal system} is a collection of axioms and rules of
      inference for making deductions from those axioms.
    \item A formal system is \defnstyle{inconsistent} if it allows us to deduce
      a statement $S$ and also to deduce its negation ``not $S$''.
  \end{itemize}
  Hilbert wanted a formal system in which the achievements of mathematics could
  be deduced, and which could satisfactorily be {\bf proven} to be consistent.
\end{frame}

\begin{frame}
  \frametitle{Frege's {\em Grundgesetze} and Russel's Paradox}
  Finding consistent formal systems for mathematics is not so easy!
  
  \vfill
  An early attempt by Gottlob Frege ("Basic Laws of Arithmetic", 1903) was
  foiled by Bertrand Russel:

  \pause
  \vfill
  For any expressible property $P(x)$, Frege's system posited the existence of
  ``the set of those $x$ which satisfy $P(x)$''. e.g. taking $P(x)$ to be
  ``$x$ is an integer divisible by 2'', we get the set whose elements are
  precisely the even numbers.

  \pause
  \vfill
  Russel's paradox:
  \begin{itemize} 
    \item Take $P(x)$ to be ``$x$ is not an element of $x$''. 
      \pause
    \item So we get a set $R$ such that $x$ is an element of $R$ if and only
      if $x$ is not an element of $x$.
      \pause
    \item Is $R$ an element of $R$?
      \pause
    \item $R$ is an element of $R$ iff $R$ is not an element of $R$.
      \pause
    \item
      Oh dear.
      % and from (Q <-> \not Q) the system derives (Q /\ \not Q)
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Avoiding Russel}
  1900-1930: attempts at formalisation which avoided Russel's paradox, by
  disallowing self-reference of the kind used to define $R$.
  \begin{itemize}
    \item Whitehead and Russel's {\em Principia Mathematica};
    \item Zermelo-Frankel set theory.
  \end{itemize}
\end{frame}


\begin{frame}
  \frametitle{Hilbert's Programme}
  \begin{quote}
    ``The definitive clarification of the nature of the infinite has become
    necessary, not merely for the special interests of the individual
    sciences but for the honor of human understanding itself.'' -- Hilbert
  \end{quote}
  \pause

  In the 1920s, Hilbert proposed a programme for settling the consistency
  issue:
  \begin{itemize}
    \item[Step 1]: Find an appropriate formal system (perhaps PM);
  \pause
    \item[Step 2]: Consider the statements and proofs in the formal system as
      mathematical objects in themselves;
  \pause
    \item[Step 3]: Apply purely ``finitistic'' mathematical reasoning to these
      objects to prove the mathematical statement: there does not exist a
      formal statement $S$ such that there exist formal proofs of $S$ and of
      ``not $S$''.
  \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{No {\em ignorabimus}}

 Hilbert 1900: ``Take any definite unsolved problem, such as the question
 as to the irrationality of the Euler-Mascheroni constant $C$, or the existence
 of an infinite number of prime numbers of the form $2^n + 1$.
 % FIXME: did he really mean that??
 However unapproachable these problems may seem to us and however helpless we
 stand before them, we have, nevertheless, the firm conviction that
 their solution must follow by a finite number of purely logical processes.
 [...] This conviction of the solvability of every mathematical problem is a
 powerful incentive to the worker. We hear within us the perpetual call: There
 is the problem. Seek its solution. You can find it by pure reason, for in
 mathematics there is no {\em ignorabimus}.''
\end{frame}

\begin{frame}
  \frametitle{Completeness}
  A formal system is \defnstyle{complete} if for any statement $S$ in the
  system, either there is proof in the system of $S$, or there is a proof of
  ``not $S$''.
\end{frame}

\begin{frame}
  \frametitle{Mechanisation of Mathematics}
  Suppose we have a complete formal system, we believe the axioms to be true
  and the rules of inference to be valid, and we want to know whether or not a
  statement $S$ is true.

  Mechanically run through all possible proofs in the system, blindly applying
  the rules of inference to the axioms in all possible combinations. By
  completeness, eventually one of $S$ or ``not $S$'' will be proved.
\end{frame}

\begin{frame}
  \frametitle{G\"{o}del}
  1931: Kurt G\"{o}del published ``On Formally Undecidable Propositions of
  Principia Mathematica and Related Systems''.

  \vfill
  We will see in this course how this destroyed the dream of finding a
  complete consistent system for mathematics, and simultaneously wrecked
  Hilbert's programme for finding finitistically provably consistent systems.

  \vfill
  \pause
  He showed
  \begin{itemize}
    \item G\"{o}del's First Theorem: Assuming it is consistent, Principia
      Mathematica, or {\bf any} formal system of anything like its scope, is
      incomplete.
    \item G\"{o}del's Second Theorem: Assuming it is consistent, such a formal
      system can not prove that it is consistent.
      % (hence nor can any fragment)
  \end{itemize}
\end{frame}

%  First theorem: No consistent formal system $T$ which is able to talk about
%  some basic properties of arithmetic on the natural numbers is complete.
%
%  Second theorem: Moreover, this incompleteness is witnessed by a statement
%  $Con(T)$ which ``says'' ``$T$ is consistent'' - so $T$ can not prove its
%  own consistency (nor its own inconsistency!).
%
%  So even a powerful system like PM or ZF is unable to prove its own
%  consistency - so certainly the basic ``finitistic'' reasoning Hilbert hoped
%  for won't be able to.
%\end{frame}
%
%\begin{frame}
%  \frametitle{Sketch of G\"{o}del's proof}
%  \begin{itemize}
%    \item Code the formal system in arithmetic;
%    \item Construct a sentence $G_T$ which ``says'' ``$T$ can't prove $G_T$''.
%    \item If $T$ proved $G_T$, then $T$ would prove that $T$ proves $G_T$, so $T$
%      would also prove ``not $G_T$''.
%    \item So by consistency, $T$ doesn't prove $G_T$.
%    \item Similarly, $T$ doesn't prove ``not $G_T$''.
%   % actually, this isn't a very accurate sketch... and an accurate one
%   % probably wouldn't be appropriate.
%  \end{itemize}
%\end{frame}
\end{document}
