\documentclass[a4]{seminar}
\usepackage{advi}
\usepackage{advi-graphicx}
\usepackage{color}
\usepackage{amssymb}
%\usepackage[all]{xypic}
\usepackage{alltt}
\usepackage{url}

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.5,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.5,.5,.5}
\definecolor{slidedarkgray}{rgb}{.4,.4,.4}
\definecolor{slidelightgray}{rgb}{.8,.8,.8}
\definecolor{slideorange}{rgb}{1,.5,0}
\def\black#1{\textcolor{black}{#1}}
\def\white#1{\textcolor{white}{#1}}
\def\blue#1{\textcolor{slideblue}{#1}}
\def\green#1{\textcolor{slidegreen}{#1}}
\def\red#1{\textcolor{slidered}{#1}}
\def\gray#1{\textcolor{slidegray}{#1}}
\def\lightgray#1{\textcolor{slidelightgray}{#1}}
\def\darkgray#1{\textcolor{slidedarkgray}{#1}}
\def\orange#1{\textcolor{slideorange}{#1}}
\newpagestyle{fw}{}{\hss\vbox to 0pt{\vspace{0.25cm}\llap{\blue{\sf\thepage}\hspace{0.1cm}}\vss}\strut}
\newpagestyle{fw0}{}{}
\slidepagestyle{fw}
\newcommand{\sectiontitle}[1]{\centerline{\textcolor{slideblue}{\textbf{#1}}}
\par\medskip}
\newcommand{\slidetitle}[1]{{\textcolor{slideblue}{\strut #1}}\par
\vspace{-1.2em}{\color{slideblue}\rule{\linewidth}{0.04em}}}
\newcommand{\xslidetitle}[1]{{\textcolor{slidered}{\strut\textbf{#1}}}\par
\vspace{-1.2em}{\color{white}\rule{\linewidth}{0.04em}}}
\newcommand{\quadskip}{{\tiny\strut}\quad}
\newcommand{\dashskip}{{\tiny\strut}\enskip{ }}
\newcommand{\enskipp}{{\tiny\strut}\enskip}
\newcommand{\exclspace}{\hspace{1pt}}
\newcommand{\notion}[1]{$\langle$#1$\rangle$}
\newcommand{\xnotion}[1]{#1}
\newcommand{\toolong}{$\hspace{-20em}$}
\def\picwidth{5em}

\begin{document}\sf
\renewcommand{\sliderightmargin}{0mm}
\renewcommand{\slideleftmargin}{20mm}
\renewcommand{\slidebottommargin}{6mm}

\setcounter{slide}{-1}
\begin{slide}
\vbox to 0pt{
\vspace{-3.45em}
\hfill\includegraphics[width=\picwidth]{/home/freek/talks/arrow/pics/arrow.eps}\par
\vss}
\vspace{2em}

\slidetitle{\Large\strut formalizing Arrow's theorem in Mizar}

\green{Freek Wiedijk} \\
Radboud University Nijmegen
\smallskip

\red{Computational Social Choice Seminar} \\
Institute for Logic, Language \& Computation \\
University of Amsterdam
\smallskip

{2009\hspace{3pt}03\hspace{3pt}06, 16\hspace{1pt}:\hspace{1.8pt}00}

\end{slide}

\begin{slide}
\sectiontitle{formalization}
\slidetitle{formalization without the computer}
\vbox to 0pt{
\vspace{-.88em}
\hfill\includegraphics[width=\picwidth]{/home/freek/talks/arrow/pics/leibniz.eps}\par
\smallskip
\hfill\includegraphics[width=\picwidth]{/home/freek/talks/arrow/pics/whitehead.eps}
\includegraphics[width=\picwidth]{/home/freek/talks/arrow/pics/russell.eps}\par
\vss}\vspace{-1.4em}

\begin{itemize}
\item[$\bullet$]
Gottfried Leibniz, 1646--1716 \\
\textbf{Calculus Ratiocinator}
\medskip

\item[$\bullet$]
Alfred North Whitehead \&
Bertrand Russell \\
\textbf{Principia Mathematica} \\ 1910--1913

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{%
\adviembed{xviewww /home/freek/talks/nmc/pix/principia.jpg}\adviwait[1]%
formalization with the computer}
\vbox to 0pt{
\vspace{-.88em}
\hfill\includegraphics[width=\picwidth]{/home/freek/talks/arrow/pics/debruijn.eps}\par
\smallskip
\hfill\advirecord{g1}{\includegraphics[width=\picwidth]{/home/freek/talks/arrow/pics/jutting.eps}}\par
\vss}\vspace{-1.4em}

N.G. de Bruijn \\
\raise-.4pt\hbox{\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/netherlands.eps}}\enskip\textbf{Automath} \\
1968--1978
\medskip

proof checker \\
proof assistant \\
interactive theorem prover
\medskip

without the computer: formalization possible in theory \\
with the computer: formalization possible in practice
\bigskip
\adviwait
\adviplay{g1}

Bert Jutting \\
\textbf{Checking Landau's `Grundlagen' in the Automath system} \\
1977
\vspace{-5pt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{%
\adviembed{xviewww /home/freek/talks/nmc/pix/automath.jpg}\adviwait[1]%
main current proof assistants}

\begin{center}
\begin{picture}(160,170)(0,-20)
\thinlines
\put(45,120){\makebox(0,0)[l]{\raise-.4pt\hbox{\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/poland.eps}}\enskip \textbf{Mizar}\enskip\raise-.4pt\hbox{\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/japan.eps}}}}
\put(45,100){\makebox(0,0)[l]{\raise-.4pt\hbox{\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/uk.eps}}\enskip HOL\enskip\raise-.4pt\hbox{\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/usa.eps}}}}
\put(45,80){\makebox(0,0)[l]{\raise-.4pt\hbox{\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/uk.eps}}\enskip Isabelle\enskip\raise-.4pt\hbox{\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/germany.eps}}}}
\put(45,60){\makebox(0,0)[l]{\raise-.4pt\hbox{\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/france.eps}}\enskip Coq}}
\put(45,40){\makebox(0,0)[l]{\raise-.4pt\hbox{\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/usa.eps}}\enskip PVS}}
\put(45,20){\makebox(0,0)[l]{\raise-.4pt\hbox{\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/france.eps}}\enskip B}}
\put(45,0){\makebox(0,0)[l]{\raise-.4pt\hbox{\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/usa.eps}}\enskip ACL2}}
\put(0,40){\framebox(140,90){}}
\put(20,-10){\framebox(140,120){}}
\put(140,135){\makebox(0,0)[rb]{\textsl{mathematics}}}
\put(160,-13){\makebox(0,0)[rt]{\textsl{computer science}}}
\end{picture}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{landmark formalizations in mathematics}
\vbox to 0pt{
\vspace{-.88em}
\hfill\includegraphics[height=7.1em]{/home/freek/talks/arrow/pics/4ct.eps}
\includegraphics[width=\picwidth]{/home/freek/talks/arrow/pics/georges.eps}\par
\smallskip
\hfill\includegraphics[width=\picwidth]{/home/freek/talks/arrow/pics/john.eps}\par
\vss}\vspace{-1.4em}

\begin{itemize}
\item[$\bullet$]
Georges Gonthier \\
INRIA \& Microsoft Corporation \\
\textbf{four color theorem},
2004 \\
{Coq}
\medskip

\item[$\bullet$]
John Harrison \\
Cambridge University \& Intel Corporation \\
\textbf{prime number theorem},
2008 \\
{HOL}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{landmark formalizations in computer science}
\vbox to 0pt{
\vspace{-.88em}
\hfill\includegraphics[height=\picwidth]{/home/freek/talks/arrow/pics/arm.eps} $\hspace{\picwidth}$\vspace{.6\smallskipamount}\\
\strut\hfill\includegraphics[height=\picwidth]{/home/freek/talks/arrow/pics/ipod.eps} $\hspace{\picwidth}$\par
%\smallskip
\hfill\includegraphics[width=\picwidth]{/home/freek/talks/arrow/pics/xavier.eps}\par
\vss}\vspace{-1.4em}

\begin{itemize}
\item[$\bullet$]
Anthony Fox \\
Cambridge University \\
\textbf{ARM processor},
1998 \\
{HOL}
\medskip

\item[$\bullet$]
Xavier Leroy \\
INRIA \\
\textbf{C compiler},
2006 \\
{Coq}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{Arrow's theorem}
\slidetitle{social choice}

$N$ individuals \\
preferences: ranking $A$ objects

combining individual preferences into a \textbf{social} preference
\bigskip
\medskip

\strut
\rlap{$\begin{array}{l}N = 3\vspace{-.7\smallskipamount}\\A = \{{\sf a},{\sf b},{\sf c}\}\end{array}$}%
\hfill\begin{picture}(200,100)(0,10)
\thicklines
\put(50,80){\line(0,1){30}}
\put(50,80){\circle*{3}}
\put(50,95){\circle*{3}}
\put(50,110){\circle*{3}}
\put(55,78){\makebox(0,0)[lb]{c}}
\put(55,93){\makebox(0,0)[lb]{b}}
\put(55,108){\makebox(0,0)[lb]{a}}
\put(100,80){\line(0,1){30}}
\put(100,80){\circle*{3}}
\put(100,95){\circle*{3}}
\put(100,110){\circle*{3}}
\put(105,78){\makebox(0,0)[lb]{a}}
\put(105,93){\makebox(0,0)[lb]{c}}
\put(105,108){\makebox(0,0)[lb]{b}}
\put(150,80){\line(0,1){30}}
\put(150,80){\circle*{3}}
\put(150,95){\circle*{3}}
\put(150,110){\circle*{3}}
\put(155,78){\makebox(0,0)[lb]{b}}
\put(155,93){\makebox(0,0)[lb]{a}}
\put(155,108){\makebox(0,0)[lb]{c}}
\thinlines
\put(100,67){\vector(0,-1){16}}
\put(60,67){\vector(1,-1){16}}
\put(140,67){\vector(-1,-1){16}}
\thicklines
\put(100,10){\line(0,1){30}}
\put(100,10){\circle*{3}}
\put(100,25){\circle*{3}}
\put(100,40){\circle*{3}}
\put(105,8){\makebox(0,0)[lb]{b}}
\put(105,23){\makebox(0,0)[lb]{c}}
\put(105,38){\makebox(0,0)[lb]{a}}
\end{picture}\hfill\strut
\vspace{-20pt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{statement of the theorem}
\vbox to 0pt{
\vspace{8.5em}
\hfill\advirecord{h1}{\includegraphics[height=7.1em]{/home/freek/talks/arrow/pics/dictator.eps}}\par
\vss}\vspace{-1.4em}

\begin{itemize}
\item[$\bullet$]
\textbf{respect unanimity} \\
if everyone prefers $a$ to $b$, the group prefers $a$ to $b$
\medskip

\item[$\bullet$]
\textbf{independent of irrelevant alternatives} \\
moving an alternative $c$ \\
does not affect the social preference between $a$ and $b$
\medskip

\item[$\bullet$]
there are at least three alternatives

\end{itemize}
\vspace{4em}
\adviwait
this is only possible in a \textbf{dictatorship}
\adviplay{h1}
\smallskip

\textsl{rule:} social preference = preference of a fixed individual
\vspace{-8pt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{naive rule does not work}

why not use majority voting?
\bigskip

\begin{center}
\begin{picture}(200,100)(0,10)
\thicklines
\put(50,80){\line(0,1){30}}
\put(50,80){\circle*{3}}
\put(50,95){\circle*{3}}
\put(50,110){\circle*{3}}
\put(55,78){\makebox(0,0)[lb]{c}}
\put(55,93){\makebox(0,0)[lb]{b}}
\put(55,108){\makebox(0,0)[lb]{a}}
\put(100,80){\line(0,1){30}}
\put(100,80){\circle*{3}}
\put(100,95){\circle*{3}}
\put(100,110){\circle*{3}}
\put(105,78){\makebox(0,0)[lb]{a}}
\put(105,93){\makebox(0,0)[lb]{c}}
\put(105,108){\makebox(0,0)[lb]{b}}
\put(150,80){\line(0,1){30}}
\put(150,80){\circle*{3}}
\put(150,95){\circle*{3}}
\put(150,110){\circle*{3}}
\put(155,78){\makebox(0,0)[lb]{b}}
\put(155,93){\makebox(0,0)[lb]{a}}
\put(155,108){\makebox(0,0)[lb]{c}}
\thinlines
\put(100,67){\vector(0,-1){16}}
\put(60,67){\vector(1,-1){16}}
\put(140,67){\vector(-1,-1){16}}
\thicklines
\put(82,10){\line(0,1){30}}
\put(82,18){\circle*{3}}
\put(82,32){\circle*{3}}
\put(87,16){\makebox(0,0)[lb]{b}}
\put(87,30){\makebox(0,0)[lb]{a}}
\put(100,10){\line(0,1){30}}
\put(100,18){\circle*{3}}
\put(100,32){\circle*{3}}
\put(105,16){\makebox(0,0)[lb]{c}}
\put(105,30){\makebox(0,0)[lb]{b}}
\put(118,10){\line(0,1){30}}
\put(118,18){\circle*{3}}
\put(118,32){\circle*{3}}
\put(123,16){\makebox(0,0)[lb]{a}}
\put(123,30){\makebox(0,0)[lb]{c}}
\end{picture}
\end{center}

not transitive\exclspace!

\vfill
\end{slide}

\begin{slide}
\slidetitle{proofs of Arrow's theorem}
\vbox to 0pt{
\vspace{-.88em}
\hfill\includegraphics[width=\picwidth]{/home/freek/talks/arrow/pics/geanakoplos.eps}\par
\vss}\vspace{-1.4em}

John Geanakoplos \\
\textbf{Three brief proofs of Arrow's impossibility theorem} \\
2001
\bigskip

paper: 4.5 pages
\smallskip

statement: 0.4 pages \\
first proof: 1.2 pages \\
second proof: 1 page \\
third proof: 0.8 pages
\adviwait
\adviembed{xviewww /home/freek/talks/arrow/pics/pages.jpg}\adviwait[1]%
\bigskip

proofs get successively more abstract

\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{first proof:} pivotal voters}

individual $n$ is \textbf{pivotal} for alternative $b$\quad$\stackrel{\sf def}{\iff}$

there is a situation where $n$ can move $b$ from the very bottom of \\
the social preference to the very top by changing just his preference
\bigskip

\begin{center}
\begin{picture}(200,100)(0,10)
\thicklines
\put(40,80){\line(0,1){30}}
\put(44,90){\makebox(0,0)[lb]{$p_l$}}
\put(80,80){\line(0,1){30}}
\put(84,90){\makebox(0,0)[lb]{$p_m$}}
\put(120,80){\line(0,1){30}}
\put(124,90){\makebox(0,0)[lb]{$p_n\!\!\!\advirecord{a1}{'}$}}
\put(160,80){\line(0,1){30}}
\put(164,90){\makebox(0,0)[lb]{$p_o$}}
\thinlines
\put(83,69){\vector(1,-2){8}}
\put(117,69){\vector(-1,-2){8}}
\put(50,69){\vector(1,-1){16}}
\put(150,69){\vector(-1,-1){16}}
\thicklines
\put(100,10){\line(0,1){30}}
\advirecord{a2}{\put(100,10){\circle*{3}}}%
\advirecord{a3}{\put(100,40){\circle*{3}}}%
\advirecord{a4}{\put(105,8){\makebox(0,0)[lb]{$b$}}}%
\advirecord{a5}{\put(105,38){\makebox(0,0)[lb]{$b$}}}%
\end{picture}
\end{center}
\adviwait
\adviplay{a2}
\adviplay{a4}
\adviwait
\adviplay[white]{a2}
\adviplay[white]{a4}
\adviplay{a1}
\adviplay{a3}
\adviplay{a5}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{first proof}, first step: conservation of extremity}

if \textbf{every} individual has an alternative $b$ at the very top or very bottom \\
(not necessarily all at the same end) \\
then in the social preference $b$ also is at the very top or very bottom
\vspace{1.645em}

\begin{center}
\begin{picture}(200,100)(0,10)
\white{\advirecord{b32}{\put(100,2){\circle*{3}}}}%
\white{\advirecord{b33}{\put(100,42){\circle*{3}}}}%
\white{\advirecord{b34}{\put(105,0){\makebox(0,0)[lb]{$b$}}}}%
\white{\advirecord{b35}{\put(105,40){\makebox(0,0)[lb]{$b$}}}}%
\thicklines
\put(40,80){\line(0,1){36}}
\advirecord{b23}{\put(40,116){\circle*{3}}}%
\advirecord{b7}{\put(40,93){\circle*{3}}}%
\advirecord{b8}{\put(40,103){\circle*{3}}}%
\advirecord{b24}{\put(45,114){\makebox(0,0)[lb]{$b$}}}%
\advirecord{b9}{\put(45,91){\makebox(0,0)[lb]{$a$}}}%
\advirecord{b10}{\put(45,101){\makebox(0,0)[lb]{$c$}}}%
\put(80,80){\line(0,1){36}}
\advirecord{b25}{\put(80,116){\circle*{3}}}%
\advirecord{b11}{\put(80,93){\circle*{3}}}%
\advirecord{b12}{\put(80,103){\circle*{3}}}%
\advirecord{b26}{\put(85,114){\makebox(0,0)[lb]{$b$}}}%
\advirecord{b13}{\put(85,91){\makebox(0,0)[lb]{$a$}}}%
\advirecord{b14}{\put(85,101){\makebox(0,0)[lb]{$c$}}}%
\put(120,80){\line(0,1){36}}
\advirecord{b27}{\put(120,80){\circle*{3}}}%
\advirecord{b15}{\put(120,93){\circle*{3}}}%
\advirecord{b16}{\put(120,103){\circle*{3}}}%
\advirecord{b28}{\put(125,78){\makebox(0,0)[lb]{$b$}}}%
\advirecord{b17}{\put(125,91){\makebox(0,0)[lb]{$a$}}}%
\advirecord{b18}{\put(125,101){\makebox(0,0)[lb]{$c$}}}%
\put(160,80){\line(0,1){36}}
\advirecord{b29}{\put(160,116){\circle*{3}}}%
\advirecord{b19}{\put(160,93){\circle*{3}}}%
\advirecord{b20}{\put(160,103){\circle*{3}}}%
\advirecord{b30}{\put(165,114){\makebox(0,0)[lb]{$b$}}}%
\advirecord{b21}{\put(165,91){\makebox(0,0)[lb]{$a$}}}%
\advirecord{b22}{\put(165,101){\makebox(0,0)[lb]{$c$}}}%
\thinlines
\put(83,69){\vector(1,-2){8}}
\put(117,69){\vector(-1,-2){8}}
\put(50,69){\vector(1,-1){16}}
\put(150,69){\vector(-1,-1){16}}
\thicklines
\advirecord{b31}{\put(100,2){\line(0,1){40}}}%
\advirecord{b1}{\put(100,7){\circle*{3}}}%
\advirecord{b2}{\put(100,22){\circle*{3}}}%
\advirecord{b3}{\put(100,37){\circle*{3}}}%
\advirecord{b4}{\put(105,5){\makebox(0,0)[lb]{$c$}}}%
\advirecord{b5}{\put(105,20){\makebox(0,0)[lb]{$b$}}}%
\advirecord{b6}{\put(105,35){\makebox(0,0)[lb]{$a$}}}%
\end{picture}
\end{center}
\adviplay{b31}
\adviwait
\adviplay{b23}
\adviplay{b24}
\adviplay{b25}
\adviplay{b26}
\adviplay{b27}
\adviplay{b28}
\adviplay{b29}
\adviplay{b30}
\adviwait
\adviplay{b32}
\adviplay{b34}
\adviwait
\adviplay[white]{b32}
\adviplay[white]{b34}
\adviplay{b31}
\adviplay{b33}
\adviplay{b35}
\adviwait
\adviplay[white]{b33}
\adviplay[white]{b35}
\adviplay{b31}
\adviplay{b2}
\adviplay{b5}
\adviwait
\adviplay{b1}
\adviplay{b3}
\adviplay{b4}
\adviplay{b6}
\adviwait
\adviplay{b7}
\adviplay{b8}
\adviplay{b9}
\adviplay{b10}
\adviplay{b11}
\adviplay{b12}
\adviplay{b13}
\adviplay{b14}
\adviplay{b15}
\adviplay{b16}
\adviplay{b17}
\adviplay{b18}
\adviplay{b19}
\adviplay{b20}
\adviplay{b21}
\adviplay{b22}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{first proof}, second step: finding a pivotal voter for an object}

\strut\phantom{(ii)}\llap{(i)} put $b$ at the very bottom everywhere \\
(ii) move $b$ to the very top one individual at the time

at some point in the social preference $b$ will `flip' from bottom to top
\bigskip

\begin{center}
\begin{picture}(200,100)(0,10)
\white{\advirecord{d1}{\put(40,80){\circle*{3}}}}%
\white{\advirecord{d5}{\put(80,80){\circle*{3}}}}%
\white{\advirecord{d3}{\put(45,78){\makebox(0,0)[lb]{$b$}}}}%
\white{\advirecord{d7}{\put(85,78){\makebox(0,0)[lb]{$b$}}}}%
\thicklines
\advirecord{d20}{\put(40,80){\line(0,1){30}}}%
\advirecord{d2}{\put(40,110){\circle*{3}}}%
\advirecord{d4}{\put(45,108){\makebox(0,0)[lb]{$b$}}}%
\advirecord{d21}{\put(80,80){\line(0,1){30}}}%
\advirecord{d6}{\put(80,110){\circle*{3}}}%
\advirecord{d8}{\put(85,108){\makebox(0,0)[lb]{$b$}}}%
\advirecord{d22}{\put(120,80){\line(0,1){30}}}%
\advirecord{d9}{\put(116,93){\makebox(0,0)[rb]{$n$}}}%
\advirecord{d10}{\put(120,80){\circle*{3}}}%
\advirecord{d11}{\put(120,110){\circle*{3}}}%
\advirecord{d12}{\put(125,78){\makebox(0,0)[lb]{$b$}}}%
\advirecord{d13}{\put(125,108){\makebox(0,0)[lb]{$b$}}}%
\put(160,80){\line(0,1){30}}
\advirecord{d14}{\put(160,80){\circle*{3}}}%
\advirecord{d15}{\put(165,78){\makebox(0,0)[lb]{$b$}}}%
\thinlines
\put(83,69){\vector(1,-2){8}}
\put(117,69){\vector(-1,-2){8}}
\put(50,69){\vector(1,-1){16}}
\put(150,69){\vector(-1,-1){16}}
\thicklines
\advirecord{d23}{\put(100,10){\line(0,1){30}}}%
\advirecord{d16}{\put(100,10){\circle*{3}}}%
\advirecord{d17}{\put(100,40){\circle*{3}}}%
\advirecord{d18}{\put(105,8){\makebox(0,0)[lb]{$b$}}}%
\advirecord{d19}{\put(105,38){\makebox(0,0)[lb]{$b$}}}%
\end{picture}
\end{center}
\adviplay{d20}
\adviplay{d21}
\adviplay{d22}
\adviplay{d23}
\adviwait
\adviplay{d1}
\adviplay{d3}
\adviplay{d5}
\adviplay{d7}
\adviplay{d10}
\adviplay{d12}
\adviplay{d14}
\adviplay{d15}
\adviwait
\adviplay{d16}
\adviplay{d18}
\adviwait
\adviplay[white]{d1}
\adviplay[white]{d3}
\adviplay{d20}
\adviplay{d2}
\adviplay{d4}
\adviwait
\adviplay[white]{d5}
\adviplay[white]{d7}
\adviplay{d21}
\adviplay{d6}
\adviplay{d8}
\adviwait
\adviplay[white]{d10}
\adviplay[white]{d12}
\adviplay{d22}
\adviplay{d11}
\adviplay{d13}
\adviplay[white]{d16}
\adviplay[white]{d18}
\adviplay{d23}
\adviplay{d17}
\adviplay{d19}
\adviwait
\adviplay{d9}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{first proof}, third step: pivotal voters are dictators for all other objects}
\bigskip

\begin{center}
\begin{picture}(200,100)(0,10)
\thicklines
\put(40,80){\line(0,1){40}}
\advirecord{f1}{\put(40,120){\circle*{3}}}%
\advirecord{f2}{\put(45,118){\makebox(0,0)[lb]{$b$}}}%
\put(80,80){\line(0,1){40}}
\advirecord{f3}{\put(80,120){\circle*{3}}}%
\advirecord{f4}{\put(85,118){\makebox(0,0)[lb]{$b$}}}%
\advirecord{f20}{\put(120,80){\line(0,1){40}}}%
\put(115,98){\makebox(0,0)[rb]{$n$}}
\advirecord{f5}{\put(120,88){\circle*{3}}}%
\advirecord{f6}{\put(120,100){\circle*{3}}}%
\advirecord{f7}{\put(120,112){\circle*{3}}}%
\advirecord{f8}{\put(125,86){\makebox(0,0)[lb]{$c$}}}%
\advirecord{f9}{\put(125,98){\makebox(0,0)[lb]{$b$}}}%
\advirecord{f10}{\put(125,110){\makebox(0,0)[lb]{$a$}}}%
\put(160,80){\line(0,1){40}}
\advirecord{f11}{\put(160,80){\circle*{3}}}%
\advirecord{f12}{\put(165,78){\makebox(0,0)[lb]{$b$}}}%
\thinlines
\put(83,69){\vector(1,-2){8}}
\put(117,69){\vector(-1,-2){8}}
\put(50,69){\vector(1,-1){16}}
\put(150,69){\vector(-1,-1){16}}
\thicklines
\advirecord{f19}{\put(100,5){\line(0,1){40}}}%
\advirecord{f13}{\put(100,13){\circle*{3}}}%
\advirecord{f14}{\put(100,25){\circle*{3}}}%
\advirecord{f15}{\put(100,37){\circle*{3}}}%
\advirecord{f16}{\put(105,11){\makebox(0,0)[lb]{$c$}}}%
\advirecord{f17}{\put(105,23){\makebox(0,0)[lb]{$b$}}}%
\advirecord{f18}{\put(105,35){\makebox(0,0)[lb]{$a$}}}%
\end{picture}
\end{center}
\adviplay{f19}
\adviplay{f20}
\adviwait
\adviplay{f5}
\adviplay{f7}
\adviplay{f8}
\adviplay{f10}
\adviwait
\adviplay{f1}
\adviplay{f2}
\adviplay{f3}
\adviplay{f4}
\adviplay{f6}
\adviplay{f9}
\adviplay{f11}
\adviplay{f12}
\adviwait
\adviplay[white]{f5}
\adviplay[white]{f8}
\adviplay{f20}
\adviplay{f7}
\adviplay{f6}
\adviplay{f14}
\adviplay{f15}
\adviplay{f17}
\adviplay{f18}
\adviwait
\adviplay[white]{f7}
\adviplay[white]{f10}
\adviplay{f20}
\adviplay{f5}
\adviplay{f6}
\adviplay{f8}
\adviplay[white]{f15}
\adviplay[white]{f18}
\adviplay{f19}
\adviplay{f13}
\adviplay{f14}
\adviplay{f16}
\adviplay{f17}
\adviwait
\adviplay{f7}
\adviplay{f10}
\adviplay{f15}
\adviplay{f18}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{first proof}, fourth step: relating pivotal voters for different objects}

$b_1 \neq b_2$

$n_1$ is a pivotal voter for $b_1$ \\
$n_2$ is a pivotal voter for $b_2$
\medskip

$n_1$ is a dictator for $b_2$ $\;\Longrightarrow\;$ only $n_1$ can move $b_2$ around \\
$n_2$ can move $b_2$ from top to bottom
\smallskip

$\phantom{n_1} \therefore$

$n_1 = n_2$
\bigskip

same individual: dictator for \textbf{all} alternatives
\medskip
\begin{flushright}
$\Box$
\end{flushright}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{Mizar}
\slidetitle{mathematics versus computer science}
\vbox to 0pt{
\vspace{-.88em}
\hfill\includegraphics[height=7.1em]{/home/freek/talks/arrow/pics/ursamajor.eps}\par
\vss}\vspace{-1.4em}

Mizar proof assistant\exclspace:
\smallskip

\strut\quad primarily designed for \textbf{mathematics}
\bigskip
\smallskip

most main current proof assistants\exclspace:
\smallskip

\strut\quad primarily designed for \textbf{computer science} \\
\strut\quad only secondarily designed for mathematics

\vfill
\end{slide}

\begin{slide}
\slidetitle{Uniwersytet w Bia{\l}ymstoku}
\vbox to 0pt{
\vspace{-.88em}
\hfill\includegraphics[width=\picwidth]{/home/freek/talks/arrow/pics/andrzej.eps}\par
\vss}\vspace{-1.4em}

Andrzej Trybulec \\
\raise-.4pt\hbox{\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/poland.eps}}\enskip\textbf{Mizar}\enskip\raise-.4pt\hbox{\includegraphics[width=12pt]{/home/freek/talks/nmc/pix/flags/japan.eps}} \\
1974--today
\bigskip

Bia{\l}ystok, Poland \\
main development
\medskip

Nagano, Japan \\
second biggest user group
\bigskip

$\approx {\sf 220}$ Mizar users \\
`{authors}'

\vfill
\end{slide}

\begin{slide}
\slidetitle{a huge library of mathematics}

\textbf{MML} \\
Mizar Mathematical Library
\bigskip

1043 `articles' = files \\
$\approx {\sf 48}$ thousand `theorems' = lemmas \\
$\approx {\sf 2.3}$ million lines \\
$\approx {\sf 75}$ Megabytes of coded mathematics

\vfill
\end{slide}

\begin{slide}
\slidetitle{set theory}
\vbox to 0pt{
\vspace{-.88em}
\hfill\includegraphics[width=\picwidth]{/home/freek/talks/arrow/pics/tarski.eps}
\includegraphics[width=\picwidth]{/home/freek/talks/arrow/pics/grothendieck.eps}\par
\vss}\vspace{-1.4em}

Mizar = \\
first order predicate logic + `schemes' + \\
axiomatic set theory
\medskip

+ `soft' type system
\bigskip
\medskip

\textbf{Tarski-Grothendieck} set theory
\medskip

ZFC + \\
arbitrarily large models of ZFC
\bigskip

= Grothendieck universes \\
= strongly inaccessible cardinals


\vfill
\end{slide}

\begin{slide}
\slidetitle{the axioms}
\vbox to 0pt{
\vspace{-1.5\bigskipamount}
\begin{center}
\footnotesize
\def\Implies{\,\Rightarrow\,}
\def\Iff{\,\Leftrightarrow\,}
\def\_{\char`\_}
\def\^{\char`\^}
%\let\red=\relax
%\let\green=\relax
\begin{tabular}{lcc}
\texttt{TARSKI:def 3} && $\red{X \subseteq Y} \Iff (\forall x.\; x \in X \Implies x \in Y)$ \\
\texttt{TARSKI:def 5} && $\red{\langle x,y\rangle} = \{\{x,y\},\{x\}\}$ \\
\texttt{TARSKI:def 6} && $\red{X \sim Y} \Iff \exists Z.\, (\forall x.\, x \in X \!\Implies\! \exists y.\, y \in Y \land \langle x,y\rangle \in Z) \land {}$ \\
&& $\phantom{X \sim Y \Iff \exists Z.\,} (\forall y.\, y \in Y \!\Implies\! \exists x.\, x \in X \land \langle x,y\rangle \in Z) \land {}$ \\
&& $(\forall x \forall y \forall z \forall u.\, \langle x,y\rangle \in Z \land \langle z,u\rangle \in Z \Implies (x = z \Iff y = u))$ \\
\noalign{\vspace{-.1em}\color{slideblue}\rule{\linewidth}{0.04em}\vspace{.2em}}%
\texttt{TARSKI:def 1} && $x \in \red{\{y\}} \Iff x = y$ \\
\texttt{TARSKI:def 2} && $x \in \red{\{y,z\}} \Iff x = y \,\lor\, x = z$ \\
\texttt{TARSKI:def 4} && $x \in \red{\bigcup X} \Iff \exists Y.\; x \in Y \,\land\, Y \in X$ \\
\noalign{\medskip}
\texttt{TARSKI:2} && $(\forall x.\; x\in X \!\Iff\! x\in Y) \Implies X = Y$ \\
\texttt{TARSKI:7} && $x \in X \Implies \exists Y.\; Y \in X \land \neg\exists x.\; x \in X \land x \in Y$ \\
\green{\texttt{TARSKI:sch 1}} && \green{$(\forall x\,\forall y\,\forall z.\, P[x,y] \land P[x,z] \!\Implies\! y = z) \rlap{${} \Implies {}$}$} \\
&& \green{$(\exists X.\; \forall x.\; x \in X \Iff \exists y.\; y \in A \,\land\, P[y,x])$} \\
\texttt{TARSKI:9} && $\exists M.\, N\in M \land (\forall X\forall Y.\, X \in M \land Y \subseteq X \!\Implies\! Y \in M) \land {}$ \\
&& $(\forall X.\, X \in M \!\Implies\! \exists Z.\, Z \in M \land \forall Y.\, Y \subseteq X \!\Implies\! Y \in Z) \land {}$ \\
&& $(\forall X.\, X \subseteq M \!\Implies\! X \sim M \lor X \in M)$
\end{tabular}
\end{center}
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{procedural versus declarative proofs}
\vspace{-\medskipamount}
\let\green=\relax
\definecolor{slidegreen}{rgb}{0,0,0}

\begin{center}
\setlength{\unitlength}{1.2em}
\linethickness{.5pt}
\begin{picture}(5,5)
\put(0.5,4.5){\makebox(0,0){\white{\advirecord{e1}{\rule{\unitlength}{\unitlength}}}}}%
\put(1.5,4.5){\makebox(0,0){\white{\advirecord{e2}{\rule{\unitlength}{\unitlength}}}}}%
\put(2.5,4.5){\makebox(0,0){\white{\advirecord{e3}{\rule{\unitlength}{\unitlength}}}}}%
\put(3.5,4.5){\makebox(0,0){\white{\advirecord{e4}{\rule{\unitlength}{\unitlength}}}}}%
\put(3.5,3.5){\makebox(0,0){\white{\advirecord{e5}{\rule{\unitlength}{\unitlength}}}}}%
\put(2.5,3.5){\makebox(0,0){\white{\advirecord{e6}{\rule{\unitlength}{\unitlength}}}}}%
\put(1.5,3.5){\makebox(0,0){\white{\advirecord{e7}{\rule{\unitlength}{\unitlength}}}}}%
\put(0.5,3.5){\makebox(0,0){\white{\advirecord{e8}{\rule{\unitlength}{\unitlength}}}}}%
\put(0.5,2.5){\makebox(0,0){\white{\advirecord{e9}{\rule{\unitlength}{\unitlength}}}}}%
\put(0.5,1.5){\makebox(0,0){\white{\advirecord{e10}{\rule{\unitlength}{\unitlength}}}}}%
\put(0.5,0.5){\makebox(0,0){\white{\advirecord{e11}{\rule{\unitlength}{\unitlength}}}}}%
\put(1.5,0.5){\makebox(0,0){\white{\advirecord{e12}{\rule{\unitlength}{\unitlength}}}}}%
\put(1.5,1.5){\makebox(0,0){\white{\advirecord{e13}{\rule{\unitlength}{\unitlength}}}}}%
\put(2.5,1.5){\makebox(0,0){\white{\advirecord{e14}{\rule{\unitlength}{\unitlength}}}}}%
\put(2.5,0.5){\makebox(0,0){\white{\advirecord{e15}{\rule{\unitlength}{\unitlength}}}}}%
\put(3.5,0.5){\makebox(0,0){\white{\advirecord{e16}{\rule{\unitlength}{\unitlength}}}}}%
\put(4.5,0.5){\makebox(0,0){\white{\advirecord{e17}{\rule{\unitlength}{\unitlength}}}}}%
\advirecord{e0}{%
\put(0,5){\line(1,0){5}}%
\put(.5,4.5){\makebox(0,0){\black{\scriptsize $0$}}}%
\put(0,4){\line(1,0){3}}%
\put(1,3){\line(1,0){2}}%
\put(2,2){\line(1,0){1}}%
\put(4,2){\line(1,0){1}}%
\put(3,1){\line(1,0){2}}%
\put(4.5,.5){\makebox(0,0){\black{\scriptsize $\infty$}}}%
\put(0,0){\line(1,0){5}}%
\put(0,0){\line(0,1){5}}%
\put(1,1){\line(0,1){2}}%
\put(2,0){\line(0,1){1}}%
\put(3,1){\line(0,1){2}}%
\put(4,2){\line(0,1){2}}%
\put(5,0){\line(0,1){5}}%
}
\adviplay[slidegreen]{e0}
\end{picture}
\end{center}
\medskip
\adviwait
\adviplay[slidelightgray]{e1}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e1}%
\adviplay[slidelightgray]{e2}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e2}%
\adviplay[slidelightgray]{e3}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e3}%
\adviplay[slidelightgray]{e4}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e4}%
\adviplay[slidelightgray]{e5}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e5}%
\adviplay[slidelightgray]{e6}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e6}%
\adviplay[slidelightgray]{e7}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e7}%
\adviplay[slidelightgray]{e8}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e8}%
\adviplay[slidelightgray]{e9}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e9}%
\adviplay[slidelightgray]{e10}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e10}%
\adviplay[slidelightgray]{e11}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e11}%
\adviplay[slidelightgray]{e12}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e12}%
\adviplay[slidelightgray]{e13}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e13}%
\adviplay[slidelightgray]{e14}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e14}%
\adviplay[slidelightgray]{e15}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e15}%
\adviplay[slidelightgray]{e16}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e16}%
\adviplay[slidelightgray]{e17}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e17}%
\adviplay[slidegreen]{e0}%

\begin{itemize}
\item[$\bullet$]
\textbf{procedural}

\begingroup
\small
\green{%
\adviwait
\adviplay[slidelightgray]{e17}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e17}%
E
\adviplay[slidelightgray]{e16}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e16}%
E
\adviplay[slidelightgray]{e15}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e15}%
S
\adviplay[slidelightgray]{e14}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e14}%
E
\adviplay[slidelightgray]{e13}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e13}%
N
\adviplay[slidelightgray]{e12}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e12}%
E
\adviplay[slidelightgray]{e11}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e11}%
S
\adviplay[slidelightgray]{e10}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e10}%
S
\adviplay[slidelightgray]{e9}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e9}%
S
\adviplay[slidelightgray]{e8}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e8}%
W
\adviplay[slidelightgray]{e7}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e7}%
W
\adviplay[slidelightgray]{e6}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e6}%
W
\adviplay[slidelightgray]{e5}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e5}%
S
\adviplay[slidelightgray]{e4}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e4}%
E
\adviplay[slidelightgray]{e3}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e3}%
E
\adviplay[slidelightgray]{e2}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e2}%
E
\adviplay[slidelightgray]{e1}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e1}%
\adviplay[slidegreen]{e0}
}
\endgroup

HOL, Isabelle, Coq, PVS, B

\adviwait
\item[$\bullet$]
\textbf{declarative}

\begingroup
\scriptsize
\green{
\adviwait
(0,0)
\adviplay[slidelightgray]{e1}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e1}%
(1,0)
\adviplay[slidelightgray]{e2}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e2}%
(2,0)
\adviplay[slidelightgray]{e3}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e3}%
(3,0)
\adviplay[slidelightgray]{e4}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e4}%
(3,1)
\adviplay[slidelightgray]{e5}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e5}%
(2,1)
\adviplay[slidelightgray]{e6}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e6}%
(1,1)
\adviplay[slidelightgray]{e7}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e7}%
(0,1)
\adviplay[slidelightgray]{e8}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e8}%
(0,2)
\adviplay[slidelightgray]{e9}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e9}%
(0,3)
\adviplay[slidelightgray]{e10}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e10}%
(0,4)
\adviplay[slidelightgray]{e11}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e11}%
(1,4)
\adviplay[slidelightgray]{e12}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e12}%
(1,3)
\adviplay[slidelightgray]{e13}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e13}%
(2,3)
\adviplay[slidelightgray]{e14}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e14}%
(2,4)
\adviplay[slidelightgray]{e15}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e15}%
(3,4)
\adviplay[slidelightgray]{e16}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e16}%
(4,4)
\adviplay[slidelightgray]{e17}\adviplay[slidegreen]{e0}\adviwait\adviplay[white]{e17}%
\adviplay[slidegreen]{e0}%
}\toolong
\endgroup

Mizar, Isabelle, ACL2

\end{itemize}

\vspace{-4pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{versje}
\vbox to 0pt{
\definecolor{slidegreen}{rgb}{0,0,0}
%\definecolor{slidered}{rgb}{0,0,0}
\vspace{-1.4em}
\def\mizar#1{\strut\rlap{\hspace{160pt}\texttt{\strut #1}}}
\begin{flushleft}\footnotesize
\offinterlineskip
\mizar{}%
\advirecord{c1}{Een bolleboos riep laatst met zwier} \\
\advirecord{c2}{\mizar{theorem}}%
\advirecord{c3}{gewapend met een vel A-vijf:} \\
{\advirecord{c4}{\mizar{\ \ not ex n st for m holds n >= m}}}%
\advirecord{c5}{Er is geen allergrootst getal,} \\
\advirecord{c6}{\mizar{proof}}%
\advirecord{c7}{dat is wat ik bewijzen ga.} \\
\mizar{}%
\advirecord{c8}{Stel, dat ik u nu zou bedriegen} \\
\green{\advirecord{c9}{\mizar{\ \ assume not thesis;}}}%
\advirecord{c10}{en hier een potje stond te jokken,} \\
\green{\advirecord{c11}{\mizar{\ \ then consider n such that}}}%
\advirecord{c12}{dan ik zou zonder overdrijven} \\
\white{\advirecord{cx1}{\mizar{\ \ let n;}}}%
\green{\advirecord{c13}{\mizar{\rlap{\advirecord{c37}{A1:}}\ \ \ \ for m holds n \char`\>= m;}}}%
\advirecord{c14}{het grootste kunnen op gaan noemen.} \\
\mizar{}%
\advirecord{c15}{Maar ben ik klaar, roept u gemeen:} \\
\green{\advirecord{c16}{\mizar{\ \ set n' = n + 2;}}}%
\advirecord{c17}{`Vermeerder dat getal met twee!'} \\
\mizar{}%
\advirecord{c18}{En zien we zeker en gewis} \\
\white{\advirecord{cx2}{\mizar{\ \ n + 2 > n by XREAL\char`\_1:31;}}}%
\green{\advirecord{c19}{\mizar{\ \ n' > n\rlap{\white{\advirecord{c35}{;}}}\ \advirecord{c38}{by XREAL\char`\_1:31;}}}}%
\advirecord{c20}{dat dit toch niet het grootste was.} \\
{\mizar{\ \ \ \ \ \ \ \white{\advirecord{c33}{*4}}}}%
\advirecord{c22}{En gaan we zo nog door een poos,} \\
\green{\advirecord{c23}{\mizar{\ \ then not for m holds n >= m;}}}%
\advirecord{c24}{dan merkt u: dit is onbegrensd.} \\
\mizar{}%
\advirecord{c25}{En daarmee heb ik q.e.d.} \\
\white{\advirecord{cx3}{\mizar{\ \ hence thesis;}}}%
\green{\advirecord{c26}{\mizar{\ \ hence contradiction\rlap{\white{\advirecord{c36}{;}}}\ \advirecord{c39}{by A1;}}}}%
\advirecord{c27}{Ik ben hier diep gelukkig door.} \\
{\mizar{\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \white{\advirecord{c34}{*1}}}}%
\advirecord{c29}{`Zo gaan', zei hij voor hij bezwijmde,} \\
\advirecord{c30}{\mizar{end;}}%
\advirecord{c31}{`bewijzen uit het ongedichte'.}
\end{flushleft}
\vss
\adviplay{c1}
\adviplay{c3}
\adviplay{c5}
\adviplay{c7}
\adviplay{c8}
\adviplay{c10}
\adviplay{c12}
\adviplay{c14}
\adviplay{c15}
\adviplay{c17}
\adviplay{c18}
\adviplay{c20}
\adviplay{c22}
\adviplay{c24}
\adviplay{c25}
\adviplay{c27}
\adviplay{c29}
\adviplay{c31}
\adviplay[slidered]{c32}
\adviwait
\adviplay[slideblue]{x1}
\adviplay[slideblue]{x2}
\adviplay[white]{c32}
\adviplay[slidered]{c32a}
\adviplay[slidegray]{c1}
\adviplay[slidegray]{c3}
\adviplay[slidegray]{c5}
\adviplay[slidegray]{c7}
\adviplay[slidegray]{c8}
\adviplay[slidegray]{c10}
\adviplay[slidegray]{c12}
\adviplay[slidegray]{c14}
\adviplay[slidegray]{c15}
\adviplay[slidegray]{c17}
\adviplay[slidegray]{c18}
\adviplay[slidegray]{c20}
\adviplay[slidegray]{c22}
\adviplay[slidegray]{c24}
\adviplay[slidegray]{c25}
\adviplay[slidegray]{c27}
\adviplay[slidegray]{c29}
\adviplay[slidegray]{c31}
\adviplay[slidegreen]{c1}
\adviplay[slidegreen]{c2}
\adviplay[slidegreen]{c3}
\adviwait
\adviplay[slideblue]{c32a}
\adviplay{c1}
\adviplay{c2}
\adviplay{c3}
\adviplay[slidegreen]{c4}
\adviplay[slidegreen]{c5}
\adviwait
\adviplay{c4}
\adviplay{c5}
\adviplay[slidegreen]{c6}
\adviplay[slidegreen]{c7}
\adviwait
\adviplay{c6}
\adviplay{c7}
\adviplay[slidegreen]{c8}
\adviplay[slidegreen]{c9}
\adviplay[slidegreen]{c10}
\adviwait
\adviplay{c8}
\adviplay{c9}
\adviplay{c10}
\adviplay[slidegreen]{c11}
\adviplay[slidegreen]{c12}
\adviplay[slidegreen]{c13}
\adviplay[slidegreen]{c14}
\adviwait
\adviplay{c11}
\adviplay{c12}
\adviplay{c13}
\adviplay{c14}
\adviplay[slidegreen]{c15}
\adviplay[slidegreen]{c16}
\adviplay[slidegreen]{c17}
\adviwait
\adviplay{c15}
\adviplay{c16}
\adviplay{c17}
\adviplay[slidegreen]{c18}
\adviplay[slidegreen]{c19}
\adviplay[slidegreen]{c20}
\adviplay[slidegreen]{c35}
\adviwait
\adviplay{c18}
\adviplay{c19}
\adviplay{c20}
\adviplay{c35}
\adviplay[slidegreen]{c22}
\adviplay[slidegreen]{c23}
\adviplay[slidegreen]{c24}
\adviwait
\adviplay{c22}
\adviplay{c23}
\adviplay{c24}
\adviplay[slidegreen]{c25}
\adviplay[slidegreen]{c26}
\adviplay[slidegreen]{c27}
\adviplay[slidegreen]{c36}
\adviwait
\adviplay{c25}
\adviplay{c26}
\adviplay{c27}
\adviplay{c36}
\adviplay[slidegreen]{c29}
\adviplay[slidegreen]{c30}
\adviplay[slidegreen]{c31}
\adviwait
\adviplay[slidegray]{c1}
\adviplay[slidegray]{c3}
\adviplay[slidegray]{c5}
\adviplay[slidegray]{c7}
\adviplay[slidegray]{c8}
\adviplay[slidegray]{c10}
\adviplay[slidegray]{c12}
\adviplay[slidegray]{c14}
\adviplay[slidegray]{c15}
\adviplay[slidegray]{c17}
\adviplay[slidegray]{c18}
\adviplay[slidegray]{c20}
\adviplay[slidegray]{c22}
\adviplay[slidegray]{c24}
\adviplay[slidegray]{c25}
\adviplay[slidegray]{c27}
\adviplay[slidegray]{c29}
\adviplay[slidegray]{c31}
\adviplay{c30}
\adviplay[slidered]{c33}
\adviplay[slidered]{c34}
\adviwait
\adviplay[white]{c34}
\adviplay[white]{c36}
\adviplay[slidegreen]{c37}
\adviplay[slidegreen]{c39}
\adviwait
\adviplay[white]{c33}
\adviplay[white]{c35}
\adviplay[slidegreen]{c38}
%\adviwait
\adviplay{c37}
\adviplay{c38}
\adviplay{c39}
\adviplay{c4}
\adviplay[slidegreen]{c9}
\adviplay[slidegreen]{c11}
\adviplay[slidegreen]{c13}
\adviplay[slidegreen]{c37}
\adviplay[slidegreen]{c16}
\adviplay[slidegreen]{c19}
\adviplay[slidegreen]{c38}
\adviplay[slidegreen]{c23}
\adviplay[slidegreen]{c26}
\adviplay[slidegreen]{c39}
\adviwait
\adviplay[white]{c9}
\adviplay[white]{c11}
\adviplay[white]{c13}
\adviplay[white]{c37}
\adviplay[white]{c16}
\adviplay[white]{c19}
\adviplay[white]{c38}
\adviplay[white]{c23}
\adviplay[white]{c26}
\adviplay[white]{c39}
\adviplay[slidegreen]{cx1}
\adviplay[slidegreen]{cx2}
\adviplay[slidegreen]{cx3}
}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{formalizing Arrow's theorem in Mizar}
\slidetitle{a suggestion}
\vbox to 0pt{
\vspace{-.88em}
\hfill\includegraphics[width=\picwidth]{/home/freek/talks/arrow/pics/krz.eps}\par
\vss}\vspace{-1.4em}

{Krzysztof Apt}, 2006\exclspace:
\vspace{3.2em}

\begin{tabular}{c}
{formalization} of Arrow's theorem \\
\noalign{\smallskip}
$\Downarrow$ \\
\noalign{\smallskip}
{attention} for formalization from the economics community
\end{tabular}

\vfill
\end{slide}

\begin{slide}
\slidetitle{formalizations of social choice theory}
\vbox to 0pt{
\vspace{-.88em}
\hfill\includegraphics[width=\picwidth]{/home/freek/talks/arrow/pics/tobias.eps}\par
\vss}\vspace{-1.4em}

\begin{itemize}
\item[$\bullet$]
Tobias Nipkow \\
Technische Universit\"at M\"unchen, Germany \\
\textbf{Arrow},
2002 \&
\textbf{Gibbard-Satterthwaite} \\
Isabelle
\medskip

\item[$\bullet$]
Peter Gammie \\
University of New South Wales, Sydney, Australia \\
\textbf{Arrow}, 2006 \& \textbf{Gibbard-Satterthwaite}, 2007 \\
Isabelle
\medskip

\item[$\bullet$]
\textsl{this talk} \\
\textbf{Arrow}, 2007 \\
Mizar

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the formal Mizar statement}
\vspace{-1.86em}
\begin{alltt}\small
reserve {A,N} for finite non empty set;
reserve {a,b} for Element of A;
reserve {i,n} for Element of N;
reserve {o} for Element of LinPreorders A;
reserve {p,p'} for Element of Funcs(N,LinPreorders A);
reserve {f} for Function of Funcs(N,LinPreorders A),LinPreorders A;\toolong\medskip\smallskip
{theorem} Th14:
  {(for p,a,b st for i holds a <_p.i, b holds a <_f.p, b) &
  (for p,p',a,b st
      for i holds (a <_p.i, b iff a <_p'.i, b) &
                  (b <_p.i, a iff b <_p'.i, a)
    holds a <_f.p, b iff a <_f.p', b) &
  card A >= 3 implies
  ex n st for p,a,b st a <_p.n, b holds a <_f.p, b}
\end{alltt}
\vspace{-3pt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Mizar in action}
\vspace{5em}
\begin{center}
\textbf{demo}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{errors in the original?}

not really
\bigskip

\textbf{one small detail} \\
step one, conservation of extremity\exclspace:
\medskip

\begin{center}
\textsl{suppose to the contrary that for some $a$ and $c$, both \\ distinct from $b$, the social preference puts $a \ge b \ge c$}
\end{center}
\medskip

proof only works if also $a \neq c$ \\
does not directly folllow from the `to the contrary'
\bigskip

in the formalization this is handled as a trivial separate case


\vfill
\end{slide}

\begin{slide}
\sectiontitle{variants}
\slidetitle{orders versus preorders}

maybe allowing alternatives to be `equivalent' helps?
\bigskip

\begin{center}
\begin{picture}(200,100)(0,10)
\thicklines
\put(50,80){\line(0,1){30}}
\put(50,80){\circle*{3}}
\put(50,95){\circle*{3}}
\put(50,110){\circle*{3}}
\put(55,78){\makebox(0,0)[lb]{c}}
\put(55,93){\makebox(0,0)[lb]{b}}
\put(55,108){\makebox(0,0)[lb]{a}}
\put(100,80){\line(0,1){30}}
\put(100,80){\circle*{3}}
\put(100,95){\circle*{3}}
\put(100,110){\circle*{3}}
\put(105,78){\makebox(0,0)[lb]{a}}
\put(105,93){\makebox(0,0)[lb]{c}}
\put(105,108){\makebox(0,0)[lb]{b}}
\put(150,80){\line(0,1){30}}
\put(150,80){\circle*{3}}
\put(150,95){\circle*{3}}
\put(150,110){\circle*{3}}
\put(155,78){\makebox(0,0)[lb]{b}}
\put(155,93){\makebox(0,0)[lb]{a}}
\put(155,108){\makebox(0,0)[lb]{c}}
\thinlines
\put(100,67){\vector(0,-1){16}}
\put(60,67){\vector(1,-1){16}}
\put(140,67){\vector(-1,-1){16}}
\thicklines
\put(100,10){\line(0,1){30}}
\put(100,25){\circle*{3}}
\put(105,23){\makebox(0,0)[lb]{${\sf a} \approx {\sf b} \approx {\sf c}$}}
\end{picture}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{specifics of the statement}
\let\lessapprox=\lesssim

\begin{itemize}
\item[$\bullet$]
\textbf{respect unanimity} \\
should we respect $<$\exclspace? \\
should we respect $\lessapprox$\exclspace?

\textsl{the first is enough, the second does not work}
\medskip

\item[$\bullet$]
\textbf{independent of irrelevant alternatives} \\
should $<$ be independent? \\
should $\lessapprox$ be independent?

\textsl{both are needed}
\medskip

\item[$\bullet$]
\textbf{dictator} \\
dictator for $<$\exclspace? \\
dictator for $\lessapprox$\exclspace?

\textsl{the second does not follow}
\end{itemize}
\vspace{-15pt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{a variant of Geanakoplos' statement}

\begin{itemize}
\item[$\bullet$]
Geanakoplos' proof\exclspace:

\begin{tabular}{lcl}
individual preferences &$\to$& preorders \\
\noalign{\vspace{-\smallskipamount}}
social preference &$\to$& preorder
\end{tabular}
\medskip

\item[$\bullet$]
seems stronger, but really is just different\exclspace:

\begin{tabular}{lcl}
individual preferences &$\to$& orders \\
\noalign{\vspace{-\smallskipamount}}
social preference &$\to$& preorder
\end{tabular}
\medskip

theorem statement becomes a bit simpler

\end{itemize}
\medskip

follows easily from the first \\
formalization of this argument is surprisingly laborious

\vfill
\end{slide}

\begin{slide}
\slidetitle{and how about Gibbard-Satterthwaite?}
\vbox to 0pt{
\vspace{-.88em}
\hfill\includegraphics[width=\picwidth]{/home/freek/talks/arrow/pics/reny.eps}\par
\vss}\vspace{-1.4em}

Philip J. Reny \\
\textbf{Arrow's theorem and the Gibbard-Satterthwaite \\ theorem: a unified approach} \\
2000
\bigskip

both proofs next to each other in two columns
\adviwait
\adviembed{xviewww /home/freek/talks/arrow/pics/gibsat.jpg}\adviwait[1]%
\bigskip
\bigskip

would be fun to do the same with two Mizar proofs \\
(or maybe have both proofs be instances of a single Mizar scheme)

\vfill
\end{slide}

\begin{slide}
\sectiontitle{the future}
\slidetitle{is formalization difficult?}

not really \\
\textbf{but} labor intensive
\bigskip

given

\begin{itemize}
\item[$\bullet$]
correct informal textbook source

\item[$\bullet$]
declarative proof assistant

\end{itemize}
\smallskip

formalization is straight-forward \\
just transcribe the textbook source

\vfill
\end{slide}

\begin{slide}
\slidetitle{de Bruijn factor}

\begin{itemize}
\item[$\bullet$]
de Bruijn factor \textbf{in space}

$${\mbox{size of formalization}\over\mbox{size of informal textbook source}}\approx {\sf 4}$$
\medskip

\item[$\bullet$]
de Bruijn factor \textbf{in time}

$${\mbox{time to formalize}\over\mbox{size of informal textbook source}}\approx {\sf 1}\; {\mbox{man}\cdot\mbox{week}\over\mbox{textbook page}}$$


\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{getting it right}

\begin{itemize}
\item[$\bullet$]
first {`proof'} of Arrow's theorem
\medskip

Kenneth Arrow \\
\textbf{A difficulty in the concept of social welfare} \\
Journal of Political Economy \\
1950
\medskip

\item[$\bullet$]
first \textsl{fully} {correct} proof of Arrow's theorem?
\medskip

Richard Routley (= Richard Sylvan) \\
\textbf{Repairing proofs of Arrow's general impossibility theorem} \\
Notre Dame Journal of Formal Logic \\
1979 

\end{itemize}
\bigskip

\vfill
\end{slide}

\begin{slide}
\slidetitle{formalization of the real world}
\vbox to 0pt{
\vspace{-.88em}
\hfill\includegraphics[height=7.1em]{/home/freek/talks/arrow/pics/crisis.eps}\par
\vss}\vspace{-1.4em}

\begin{itemize}
\item[$\bullet$]
mathematics: abstractions

\item[$\bullet$]
computer science: man-made abstractions

\item[$\bullet$]
economics: the real world\exclspace!

\end{itemize}
\bigskip

formalization useful for economists?

\vfill
\end{slide}

\end{document}