| author | Christian Urban <christian.urban@kcl.ac.uk> | 
| Sun, 25 Oct 2020 01:25:01 +0000 | |
| changeset 789 | 966c9fd84693 | 
| parent 500 | 91b888c91d73 | 
| child 871 | 358a72d7bf71 | 
| permissions | -rw-r--r-- | 
| 
392
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
1  | 
\documentclass[dvipsnames,14pt,t]{beamer}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
2  | 
\usepackage{../slides}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
3  | 
\usepackage{../graphics}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
4  | 
\usepackage{../langs}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
5  | 
\usepackage{../data}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
6  | 
\usepackage{../grammar}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
7  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
8  | 
% beamer stuff  | 
| 458 | 9  | 
\renewcommand{\slidecaption}{CFL, King's College London}
 | 
| 
392
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
10  | 
\newcommand{\bl}[1]{\textcolor{blue}{#1}}       
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
11  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
12  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
13  | 
\begin{document}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
14  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
15  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
16  | 
\begin{frame}[t]
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
17  | 
\frametitle{%
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
18  | 
  \begin{tabular}{@ {}c@ {}}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
19  | 
\\[-3mm]  | 
| 458 | 20  | 
\LARGE Compilers and \\[-2mm]  | 
| 
392
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
21  | 
\LARGE Formal Languages\\[3mm]  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
22  | 
  \end{tabular}}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
23  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
24  | 
\normalsize  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
25  | 
  \begin{center}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
26  | 
  \begin{tabular}{ll}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
27  | 
Email: & christian.urban at kcl.ac.uk\\  | 
| 500 | 28  | 
Office: & N7.07 (North Wing, Bush House)\\  | 
| 
392
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
29  | 
Slides: & KEATS (also home work is there)\\  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
30  | 
  \end{tabular}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
31  | 
  \end{center}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
32  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
33  | 
\end{frame}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
34  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
35  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
36  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
37  | 
\begin{frame}[c]
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
38  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
39  | 
\Large\bf There are more problems, than there are  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
40  | 
programs.\bigskip\bigskip\pause\\  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
41  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
42  | 
There must be a problem for which there is no program.  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
43  | 
\end{frame}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
44  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
45  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
46  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
47  | 
\begin{frame}[c]
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
48  | 
\frametitle{Subsets}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
49  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
50  | 
\Large  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
51  | 
If \bl{$A \subseteq B$} then \bl{$A$} has fewer elements
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
52  | 
than \bl{$B$}\bigskip\bigskip
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
53  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
54  | 
\Large  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
55  | 
\bl{$A \subseteq B$} and \bl{$B \subseteq A$}\bigskip
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
56  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
57  | 
then \bl{$A = B$}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
58  | 
\end{frame}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
59  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
60  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
61  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
62  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
63  | 
  \begin{frame}[c]
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
64  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
65  | 
  \begin{center}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
66  | 
  \begin{tikzpicture}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
67  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
68  | 
\draw (-4,2.5) node [scale=2.5] (X)  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
69  | 
    {\begin{tabular}{l}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
70  | 
     $\{$  
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
71  | 
     \!\includegraphics[scale=0.02]{../pics/o1.jpg},
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
72  | 
     \includegraphics[scale=0.02]{../pics/o2.jpg},
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
73  | 
     \!\includegraphics[scale=0.02]{../pics/o3.jpg},
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
74  | 
     \includegraphics[scale=0.02]{../pics/o4.jpg},
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
75  | 
     \!\includegraphics[scale=0.027]{../pics/o5.jpg}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
76  | 
$\}$  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
77  | 
    \end{tabular}};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
78  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
79  | 
\draw (-5.6,-2.5) node [scale=2.5] (Y)  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
80  | 
    {\begin{tabular}{l}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
81  | 
     $\{$  
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
82  | 
     \!\includegraphics[scale=0.059]{../pics/a1.jpg},
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
83  | 
     \includegraphics[scale=0.048]{../pics/a2.jpg},
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
84  | 
     \includegraphics[scale=0.02]{../pics/a3.jpg}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
85  | 
$\}$  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
86  | 
    \end{tabular}};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
87  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
88  | 
     \draw (0,1.5) node (X1) {5 elements};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
89  | 
     \draw (0,-3.5) node (y1) {3 elements};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
90  | 
  \end{tikzpicture}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
91  | 
  \end{center}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
92  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
93  | 
  \end{frame}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
94  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
95  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
96  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
97  | 
  \begin{frame}[c]
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
98  | 
  \frametitle{Newton vs Feynman}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
99  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
100  | 
  \begin{center}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
101  | 
  \begin{tabular}{cc}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
102  | 
  \includegraphics[scale=0.2]{../pics/newton.jpg} &
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
103  | 
  \includegraphics[scale=0.2]{../pics/feynman.jpg}\\
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
104  | 
classical physics & quantum physics  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
105  | 
  \end{tabular}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
106  | 
  \end{center}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
107  | 
  \end{frame}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
108  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
109  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
110  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
111  | 
  \begin{frame}[c]
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
112  | 
  \frametitle{The Goal of the Talk}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
113  | 
\large  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
114  | 
  \begin{itemize}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
115  | 
\item show you that something very unintuitive happens with very large sets  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
116  | 
\bigskip\bigskip  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
117  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
118  | 
  \item convince you that there are more {\bf problems} than {\bf programs}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
119  | 
  \end{itemize}	
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
120  | 
  \end{frame}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
121  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
122  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
123  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
124  | 
\begin{frame}[t]
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
125  | 
%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
126  | 
  \begin{center}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
127  | 
  \begin{tikzpicture}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
128  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
129  | 
\draw (-5,2.5) node [scale=2.3] (X)  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
130  | 
    {\begin{tabular}{@ {\hspace{-3mm}}l}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
131  | 
     \bl{$B$ $=$ $\{$  
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
132  | 
     \!\includegraphics[scale=0.02]{../pics/o1.jpg},
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
133  | 
     \includegraphics[scale=0.02]{../pics/o2.jpg},
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
134  | 
     \!\includegraphics[scale=0.02]{../pics/o3.jpg},
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
135  | 
     \includegraphics[scale=0.02]{../pics/o4.jpg},
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
136  | 
     \!\includegraphics[scale=0.027]{../pics/o5.jpg}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
137  | 
$\}$}  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
138  | 
    \end{tabular}};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
139  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
140  | 
\draw (-6.6,-0.5) node [scale=2.3] (Y)  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
141  | 
    {\begin{tabular}{@ {\hspace{-3mm}}l}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
142  | 
     \bl{$A$ $=$ $\{$  
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
143  | 
     \!\includegraphics[scale=0.059]{../pics/a1.jpg},
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
144  | 
     \includegraphics[scale=0.048]{../pics/a2.jpg},
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
145  | 
     \includegraphics[scale=0.02]{../pics/a3.jpg}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
146  | 
$\}$}  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
147  | 
     \end{tabular}};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
148  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
149  | 
     \only<1>{\draw (-5, -3) node[scale=2] 
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
150  | 
       {\bl{$|A|$ $=$ $5$}, \bl{$|B|$ $=$ $3$}};}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
151  | 
     \only<2>{
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
152  | 
\draw [->, line width=1mm, red] (-7.4, 0.2) -- (-6.1, 2.1);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
153  | 
\draw [->, line width=1mm, red] (-5.8, 0.2) -- (-3.1, 2.1);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
154  | 
\draw [->, line width=1mm, red] (-4.5, 0.2) -- (-7.6, 2.1);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
155  | 
       \draw (-5, -3) node[scale=2] {then \bl{$|A|$ $\le$ $|B|$}};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
156  | 
}  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
157  | 
    \only<3>{
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
158  | 
\draw [<-, line width=1mm, red] (-7.5, 0.2) -- (-6.1, 2.1);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
159  | 
\draw [<-, line width=1mm, red] (-7.3, 0.2) -- (-3.1, 2.1);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
160  | 
\draw [<-, line width=1mm, red] (-6, 0.2) -- (-7.5, 2.1);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
161  | 
\draw [<-, line width=1mm, red] (-4.5, 0.2) -- (-4.5, 2.1);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
162  | 
\draw [<-, line width=1mm, red] (-4.3, 0.2) -- (-1.3, 2.1);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
163  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
164  | 
       \draw (-5, -3) node[scale=1.5] {\small{}for \bl{$=$}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
165  | 
        has to be a {\bf one-to-one} mapping};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
166  | 
}  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
167  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
168  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
169  | 
  \end{tikzpicture}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
170  | 
  \end{center}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
171  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
172  | 
\end{frame}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
173  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
174  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
175  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
176  | 
\begin{frame}[c]
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
177  | 
\frametitle{Cardinality}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
178  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
179  | 
\Large  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
180  | 
\bl{$|A|$} $\dn$ ``how many elements''\bigskip\\
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
181  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
182  | 
\bl{$A \subseteq B  \Rightarrow |A| \leq |B|$}\bigskip\\\pause
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
183  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
184  | 
if there is an injective function \bl{$f: A \rightarrow B$} then \bl{$|A| \leq |B|$}\
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
185  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
186  | 
\begin{center}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
187  | 
\bl{\large$\forall x y.\; f(x) = f(y) \Rightarrow x = y$}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
188  | 
\end{center}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
189  | 
\end{frame}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
190  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
191  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
192  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
193  | 
\begin{frame}[t]
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
194  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
195  | 
  \begin{center}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
196  | 
  \begin{tikzpicture}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
197  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
198  | 
\draw (-6.6,2.5) node [scale=2.3] (X)  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
199  | 
    {\begin{tabular}{@ {\hspace{-3mm}}l}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
200  | 
     $A$ $=$ $\{$  
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
201  | 
     \!\includegraphics[scale=0.02]{../pics/o1.jpg},
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
202  | 
     \includegraphics[scale=0.02]{../pics/o2.jpg},
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
203  | 
     \!\includegraphics[scale=0.02]{../pics/o3.jpg}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
204  | 
$\}$  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
205  | 
    \end{tabular}};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
206  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
207  | 
\draw (-6.6,-0.5) node [scale=2.3] (Y)  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
208  | 
    {\begin{tabular}{@ {\hspace{-3mm}}l}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
209  | 
     $B$ $=$ $\{$  
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
210  | 
     \!\includegraphics[scale=0.059]{../pics/a1.jpg},
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
211  | 
     \includegraphics[scale=0.048]{../pics/a2.jpg},
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
212  | 
     \includegraphics[scale=0.02]{../pics/a3.jpg}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
213  | 
$\}$  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
214  | 
     \end{tabular}};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
215  | 
   \onslide<3->{\draw (-7, -3) node[scale=1.5] 
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
216  | 
      {then \bl{$|A|$ \alert{$=$} $|B|$}};}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
217  | 
     \only<1>{
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
218  | 
\draw [->, line width=1mm, red] (-7.4, 0.2) -- (-6.1, 2.1);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
219  | 
\draw [->, line width=1mm, red] (-5.8, 0.2) -- (-4.3, 2.1);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
220  | 
\draw [->, line width=1mm, red] (-4.5, 0.2) -- (-7.6, 2.1);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
221  | 
}  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
222  | 
    \only<2->{
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
223  | 
\draw [<-, line width=1mm, blue] (-7.5, 0.2) -- (-7.5, 2.1);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
224  | 
\draw [<-, line width=1mm, blue] (-5.8, 0.2) -- (-4.3, 2.1);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
225  | 
\draw [<-, line width=1mm, blue] (-4.5, 0.2) -- (-6.1, 2.1);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
226  | 
}  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
227  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
228  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
229  | 
  \end{tikzpicture}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
230  | 
  \end{center}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
231  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
232  | 
\end{frame}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
233  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
234  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
235  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
236  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
237  | 
\begin{frame}[c]
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
238  | 
\frametitle{Natural Numbers}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
239  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
240  | 
\Large  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
241  | 
\bl{$\mathbb{N}$} \bl{$\dn$} \bl{$\{0, 1, 2, 3, .......\}$}\bigskip\pause 
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
242  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
243  | 
\bl{$A$} is \alert{countable} iff \bl{$|A| \leq |\mathbb{N}|$}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
244  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
245  | 
\end{frame}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
246  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
247  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
248  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
249  | 
\begin{frame}[c]
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
250  | 
\frametitle{First Question}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
251  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
252  | 
\Large  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
253  | 
\bl{$|\mathbb{N} - \{0\}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\bigskip 
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
254  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
255  | 
\large  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
256  | 
\bl{$\geq$} or \bl{$\leq$} or \bl{$=$} ?
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
257  | 
\bigskip\bigskip\bigskip\pause  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
258  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
259  | 
\bl{$x$ $\mapsto$ $x + 1$},\\  \bl{$|\mathbb{N} - \{0\}|$ $=$  
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
260  | 
$|\mathbb{N}|$}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
261  | 
\end{frame}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
262  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
263  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
264  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
265  | 
\mode<presentation>{
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
266  | 
\begin{frame}[c]
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
267  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
268  | 
\Large  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
269  | 
\bl{$|\mathbb{N} - \{0, 1\}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\pause 
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
270  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
271  | 
\bl{$|\mathbb{N} - \mathbb{O}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\bigskip
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
272  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
273  | 
\normalsize  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
274  | 
\bl{$\mathbb{O}$} $\dn$ odd numbers\quad   \bl{$\{1,3,5......\}$}\\ \pause
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
275  | 
\bl{$\mathbb{E}$} $\dn$ even numbers\quad   \bl{$\{0,2,4......\}$}\\
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
276  | 
\end{frame}}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
277  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
278  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
279  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
280  | 
\mode<presentation>{
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
281  | 
\begin{frame}[c]
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
282  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
283  | 
\Large  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
284  | 
\bl{$|\mathbb{N} \cup \mathbb{-N}|   \;\;\;\alert{?}\;\;\;  |\mathbb{N}| $}\bigskip\bigskip
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
285  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
286  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
287  | 
\normalsize  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
288  | 
\bl{$\mathbb{\phantom{-}N}$} $\dn$ positive numbers\quad   \bl{$\{0,1,2,3,......\}$}\\
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
289  | 
\bl{$\mathbb{-N}$} $\dn$ negative numbers\quad   \bl{$\{0,-1,-2,-3,......\}$}\\
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
290  | 
\end{frame}}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
291  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
292  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
293  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
294  | 
\mode<presentation>{
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
295  | 
\begin{frame}[c]
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
296  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
297  | 
\Large  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
298  | 
\bl{$A$} is \alert{countable} if there exists an injective \bl{$f : A \rightarrow \mathbb{N}$}\bigskip
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
299  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
300  | 
\bl{$A$} is \alert{uncountable} if there does not exist an injective \bl{$f : A \rightarrow \mathbb{N}$}\bigskip\bigskip 
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
301  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
302  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
303  | 
countable:  \bl{$|A| \leq |\mathbb{N}|$}\\
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
304  | 
uncountable:  \bl{$|A| > |\mathbb{N}|$}\pause\bigskip
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
305  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
306  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
307  | 
Does there exist such an \bl{$A$} ?
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
308  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
309  | 
\end{frame}}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
310  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
311  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
312  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
313  | 
  \mode<presentation>{
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
314  | 
  \begin{frame}[c]
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
315  | 
  \frametitle{Hilbert's Hotel}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
316  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
317  | 
  \begin{center}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
318  | 
 \includegraphics[scale=0.8]{../pics/hilberts_hotel.jpg}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
319  | 
  \end{center}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
320  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
321  | 
  \begin{itemize}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
322  | 
\item \ldots has as many rooms as there are natural numbers  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
323  | 
  \end{itemize}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
324  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
325  | 
  \end{frame}}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
326  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
327  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
328  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
329  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
330  | 
\begin{frame}[t]
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
331  | 
 \frametitle{\begin{tabular}{c}Real Numbers between\\[-2mm] 0 and 1\end{tabular}}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
332  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
333  | 
  \begin{center}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
334  | 
  \begin{tikzpicture}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
335  | 
\draw [fill, color=black!50] (1,4) rectangle (2, 3);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
336  | 
\draw [fill, color=black!50] (2,3) rectangle (3, 2);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
337  | 
\draw [fill, color=black!50] (3,2) rectangle (4, 1);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
338  | 
\draw [fill, color=black!50] (4,1) rectangle (5, 0);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
339  | 
\draw (0, 0) grid (8, 5);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
340  | 
\draw [line width = 1.mm] (1,0) -- (1, 5);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
341  | 
\draw [line width = 1.mm] (0, 4) -- (8, 4);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
342  | 
  \draw (0.5,3.5) node {$1$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
343  | 
  \draw (0.5,2.5) node {$2$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
344  | 
  \draw (0.5,1.5) node {$3$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
345  | 
  \draw (0.5,0.5) node {$4$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
346  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
347  | 
  \draw (1.5,3.5) node {\only<1>{$3$}\only<2->{$4$}};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
348  | 
  \draw (2.5,3.5) node {$3$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
349  | 
  \draw (3.5,3.5) node {$3$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
350  | 
  \draw (4.5,3.5) node {$3$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
351  | 
  \draw (5.5,3.5) node {$3$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
352  | 
  \draw (6.5,3.5) node {$3$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
353  | 
  \draw (7.5,3.5) node {$\ldots$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
354  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
355  | 
  \draw (1.5,2.5) node {$1$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
356  | 
  \draw (2.5,2.5) node {\only<1-2>{$2$}\only<3->{$3$}};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
357  | 
  \draw (3.5,2.5) node {$3$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
358  | 
  \draw (4.5,2.5) node {$4$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
359  | 
  \draw (5.5,2.5) node {$5$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
360  | 
  \draw (6.5,2.5) node {$6$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
361  | 
  \draw (7.5,2.5) node {$7$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
362  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
363  | 
  \draw (1.5,1.5) node {$0$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
364  | 
  \draw (2.5,1.5) node {$1$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
365  | 
  \draw (3.5,1.5) node {\only<1-3>{$0$}\only<4->{$1$}};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
366  | 
  \draw (4.5,1.5) node {$1$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
367  | 
  \draw (5.5,1.5) node {$0$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
368  | 
  \draw (6.5,1.5) node {$\ldots$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
369  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
370  | 
   \draw (1.5,0.5) node {$7$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
371  | 
  \draw (2.5,0.5) node {$8$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
372  | 
  \draw (3.5,0.5) node {$5$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
373  | 
  \draw (4.5,0.5) node {\only<1-4>{$3$}\only<5->{$4$}};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
374  | 
  \draw (5.5,0.5) node {$9$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
375  | 
  \draw (6.5,0.5) node {$\ldots$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
376  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
377  | 
   \draw (1.5,-0.5) node {$\ldots$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
378  | 
   \draw (8.5,3.5) node {$\ldots$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
379  | 
  \end{tikzpicture}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
380  | 
  \end{center}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
381  | 
  \mbox{}\\[-20mm]\mbox{}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
382  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
383  | 
  \onslide<6->{
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
384  | 
  \begin{center}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
385  | 
  \Large\bl{$|\mathbb{N}| < |R|$}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
386  | 
  \end{center}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
387  | 
}  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
388  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
389  | 
\end{frame}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
390  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
391  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
392  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
393  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
394  | 
\mode<presentation>{
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
395  | 
\begin{frame}[t]
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
396  | 
 \frametitle{The Set of Problems}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
397  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
398  | 
$\aleph_0$  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
399  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
400  | 
  \begin{center}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
401  | 
  \begin{tikzpicture}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
402  | 
\draw [fill, color=black!50] (1,4) rectangle (2, 3);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
403  | 
\draw [fill, color=black!50] (2,3) rectangle (3, 2);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
404  | 
\draw [fill, color=black!50] (3,2) rectangle (4, 1);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
405  | 
\draw [fill, color=black!50] (4,1) rectangle (5, 0);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
406  | 
\draw (0, 0) grid (8, 5);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
407  | 
\draw [line width = 1.mm] (1,0) -- (1, 5);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
408  | 
\draw [line width = 1.mm] (0, 4) -- (8, 4);  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
409  | 
  \draw (0.5,3.5) node {$1$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
410  | 
  \draw (0.5,2.5) node {$2$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
411  | 
  \draw (0.5,1.5) node {$3$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
412  | 
  \draw (0.5,0.5) node {$4$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
413  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
414  | 
  \draw (1.5,4.5) node {$0$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
415  | 
  \draw (2.5,4.5) node {$1$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
416  | 
  \draw (3.5,4.5) node {$2$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
417  | 
  \draw (4.5,4.5) node {$3$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
418  | 
  \draw (5.5,4.5) node {$4$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
419  | 
  \draw (6.5,4.5) node {$5$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
420  | 
  \draw (7.5,4.5) node {$\ldots$}; 
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
421  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
422  | 
  \draw (1.5,3.5) node {$0$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
423  | 
  \draw (2.5,3.5) node {$1$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
424  | 
  \draw (3.5,3.5) node {$0$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
425  | 
  \draw (4.5,3.5) node {$1$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
426  | 
  \draw (5.5,3.5) node {$0$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
427  | 
  \draw (6.5,3.5) node {$1$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
428  | 
  \draw (7.5,3.5) node {$\ldots$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
429  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
430  | 
  \draw (1.5,2.5) node {$0$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
431  | 
  \draw (2.5,2.5) node {$0$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
432  | 
  \draw (3.5,2.5) node {$0$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
433  | 
  \draw (4.5,2.5) node {$1$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
434  | 
  \draw (5.5,2.5) node {$1$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
435  | 
  \draw (6.5,2.5) node {$0$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
436  | 
  \draw (7.5,2.5) node {$0$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
437  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
438  | 
  \draw (1.5,1.5) node {$0$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
439  | 
  \draw (2.5,1.5) node {$0$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
440  | 
  \draw (3.5,1.5) node {$0$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
441  | 
  \draw (4.5,1.5) node {$0$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
442  | 
  \draw (5.5,1.5) node {$0$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
443  | 
  \draw (6.5,1.5) node {$\ldots$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
444  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
445  | 
   \draw (1.5,0.5) node {$1$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
446  | 
  \draw (2.5,0.5) node {$1$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
447  | 
  \draw (3.5,0.5) node {$0$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
448  | 
  \draw (4.5,0.5) node {$1$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
449  | 
  \draw (5.5,0.5) node {$1$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
450  | 
  \draw (6.5,0.5) node {$\ldots$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
451  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
452  | 
  \draw (1.5,-0.5) node {$\ldots$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
453  | 
   \draw (8.5,3.5) node {$\ldots$};
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
454  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
455  | 
  \end{tikzpicture}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
456  | 
  \end{center}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
457  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
458  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
459  | 
  \onslide<2>{
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
460  | 
  \begin{center}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
461  | 
  \large \bl{|Progs| $=$ $|\mathbb{N}|$ $<$ |Probs|}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
462  | 
 \end{center}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
463  | 
}  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
464  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
465  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
466  | 
\end{frame}}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
467  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
468  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
469  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
470  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
471  | 
\mode<presentation>{
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
472  | 
\begin{frame}[c]
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
473  | 
\frametitle{Halting Problem}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
474  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
475  | 
\large  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
476  | 
Assume a program \bl{$H$} that decides for all programs \bl{$A$} and all 
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
477  | 
input data \bl{$D$} whether\bigskip
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
478  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
479  | 
\begin{itemize}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
480  | 
\item \bl{$H(A, D) \dn 1$} iff \bl{$A(D)$} terminates
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
481  | 
\item \bl{$H(A, D) \dn 0$} otherwise
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
482  | 
\end{itemize}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
483  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
484  | 
\end{frame}}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
485  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
486  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
487  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
488  | 
\mode<presentation>{
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
489  | 
\begin{frame}[c]
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
490  | 
\frametitle{Halting Problem (2)}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
491  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
492  | 
\large  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
493  | 
Given such a program \bl{$H$} define the following program \bl{$C$}:
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
494  | 
for all programs \bl{$A$}\bigskip
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
495  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
496  | 
\begin{itemize}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
497  | 
\item \bl{$C(A) \dn 0$} iff \bl{$H(A, A) = 0$} 
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
498  | 
\item \bl{$C(A) \dn$ loops} otherwise
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
499  | 
\end{itemize}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
500  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
501  | 
\end{frame}}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
502  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
503  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
504  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
505  | 
\mode<presentation>{
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
506  | 
\begin{frame}[c]
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
507  | 
\frametitle{Contradiction}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
508  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
509  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
510  | 
\bl{$H(C, C)$} is either \bl{$0$} or \bl{$1$}.
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
511  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
512  | 
\begin{itemize}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
513  | 
\item \bl{$H(C, C) = 1$} $\stackrel{\text{def}\,H}{\Rightarrow}$ \bl{$C(C)\downarrow$} $\stackrel{\text{def}\,C}{\Rightarrow}$ \bl{$H(C, C)=0$} 
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
514  | 
\item \bl{$H(C, C) = 0$} $\stackrel{\text{def}\,H}{\Rightarrow}$ \bl{$C(C)$} loops $\stackrel{\text{def}\,C}{\Rightarrow}$\\ 
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
515  | 
\hspace{7cm}\bl{$H(C, C)=1$} 
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
516  | 
\end{itemize}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
517  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
518  | 
Contradiction in both cases. So \bl{$H$} cannot exist.
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
519  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
520  | 
\end{frame}}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
521  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
522  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
523  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
524  | 
  \mode<presentation>{
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
525  | 
  \begin{frame}[c]
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
526  | 
  \frametitle{Take Home Points}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
527  | 
\large  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
528  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
529  | 
  \begin{itemize}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
530  | 
\item there are sets that are more infinite than others\bigskip  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
531  | 
\item even with the most powerful computer we can imagine, there  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
532  | 
are problems that cannot be solved by any program\bigskip\bigskip  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
533  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
534  | 
\item in CS we actually hit quite often such problems (halting problem)  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
535  | 
  \end{itemize}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
536  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
537  | 
  \end{frame}}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
538  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
539  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
540  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
541  | 
\end{document}
 | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
542  | 
|
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
543  | 
%%% Local Variables:  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
544  | 
%%% mode: latex  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
545  | 
%%% TeX-master: t  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
546  | 
%%% End:  | 
| 
 
2d0a59127694
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
547  |