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

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.5,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.6,.6,.6}
\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}}
\newpagestyle{fw}{}{\hfil\textcolor{slideblue}{\sf\thepage}\qquad\qquad}
\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{\quadskip}{{\tiny\strut}\quad}
\newcommand{\dashskip}{{\tiny\strut}\enskip{ }}
\newcommand{\enskipp}{{\tiny\strut}\enskip}
\newcommand{\exclspace}{\hspace{.45pt}}
\newcommand{\notion}[1]{$\langle$#1$\rangle$}
\newcommand{\xnotion}[1]{#1}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large a comparison of foundations of mathematics}

Freek Wiedijk \\
University of Nijmegen

room A4028 \\
2003 11 10, 11:00
\end{slide}

\begin{slide}
\slidetitle{is ZF a hack?}
Raph Levien (maintainer of Ghostscript),
on a forum called Advogato
\begin{quote}\green{I was talking $[\ldots]$ with Bram, and he called ZF set theory a `hack.' I more or less agree, but $[\ldots]$}
\end{quote}
\medskip

Bob Solovay does not think ZF is a hack \\
personally I \textbf{do} think ZF is a bit of a hack
\medskip
\adviwait

\begin{itemize}
\item[$\bullet$]
distinction between `sets' and `classes'
\adviwait

\item[$\bullet$]
two levels of `logic' and `set theory' \\
\red{similar concepts on both levels}
\begin{center}
\red{{\large $\exists\,$} in logic $\;\longleftrightarrow\;$ \raise 1pt\hbox{$\bigcup\,$} on sets}
\end{center}
\medskip
\adviwait

no such distinction in HOL!

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Henk's napkin}
\green{how many Z\advirecord{a1}{\rlap{\raise.85ex\hbox{\underbar{\phantom{F}}}}}F axioms are there?}
\medskip

\hfill\green{\framebox{\black{\begin{tabular}{lll}
\advirecord{a5}{Set properties & 2 & ext, found} \\
\advirecord{a4a}{Set existence & 6}\quad \advirecord{a3}{8}\enskip\strut \\
\noalign{\medskip}
\qquad \advirecord{a4c}{$\mbox{Set}(\emptyset)$} \\
\qquad \advirecord{a4d}{$\mbox{Set}(\{x,y\})$}\enskip\strut \\
\qquad \advirecord{a4e}{$\mbox{Set}(\bigcup x)$} \\
\setbox0=\hbox{${\mbox{Set}(F``x)}$}%
\qquad \advirecord{a4f}{\advirecord{a2}{\rlap{\raise.85ex\hbox{\underbar{\hbox to\wd0{\hss}}}}}\unhbox0} \\
\qquad \advirecord{a4g}{$\mbox{Set}({\cal P} x)$} \\
\qquad \advirecord{a4h}{$\mbox{Set}(\omega)$} \\
\noalign{\smallskip}
\end{tabular}}}}\hfill\strut\par
\adviwait
\adviplay{a5}
\adviwait
\adviplay{a4a}
\adviplay{a4c}
\adviplay{a4d}
\adviplay{a4e}
\adviplay{a4f}
\adviplay{a4g}
\adviplay{a4h}
\adviwait
\adviplay[slidegreen]{a3}
\adviwait
\adviplay[slidered]{a1}
\adviplay[slidered]{a2}

\vfill
\end{slide}

\newdimen\statbarunit
\def\statbar#1{\raise0.3ex\hbox{\rule{#1\statbarunit}{3pt}}}%
\def\graystatbar#1{\color{slidegray}{\statbar{#1}}}%

\begin{slide}
\slidetitle{ZFC \& HOL in Automath: the simplicity shootout}
\textbf{number of \green{primitive notions}}

\statbarunit=3.31pt
\begin{tabular}{rl}
ZFC & \statbar{32} \\
\red{HOL} & \statbar{25}
\end{tabular}
\medskip
\adviwait

\textbf{size of the \green{specification}}

\statbarunit=.221pt
\begin{tabular}{rl}
\red{ZFC} & \statbar{751} \\
HOL & \statbar{928}
\end{tabular}
\medskip
\adviwait

\textbf{size of the \green{$\lambda$-term}}

\statbarunit=.0711pt
\begin{tabular}{rl}
\red{ZFC} & \statbar{1487} \\
HOL & \statbar{2868}
\end{tabular}

\vfill
\end{slide}

\begin{slide}
\slidetitle{and what about Coq?}
inductive types in Coq: recursion principles \\
Luis: the rules are nowhere explicitly spelled out

$\Rightarrow\;$ \textbf{Coq logic: not simple}
\medskip
\adviwait

Thorsten: \blue{extensional Martin-L\"of type theory with W types}
\begin{quote}
{
elements of the type \red{${\sf W}x{:}A.\, B$} are trees \\
\dashskip nodes are labeled with elements of $A$ \\
\dashskip edges (from node labelled $a$) for each element of $B[x:=a]$
}
\end{quote}
\medskip
\adviwait

Nordstr\"om/Petersson/Smith book: not presented as `system' \\
\adviwait
\green{Peter Aczel paper (on relation between type theory and set theory):}
\begin{center}
{\blue{\phantom{$\,^{\sf ext}$}MLW\advirecord{b}{$\,^{\sf ext}$}}}
\end{center}
ZFC and MLW: nice TLAs
\adviwait
\adviplay[slideblue]{b}

\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{and what about PTS{\tiny $\,$}s?}
proper type systems \\
Henk's tutorial paper: \green{problems in type theory}
\medskip

\begin{center}
\begin{tabular}{lcl}
LF &$=$& $\lambda P$ \\
CC &$=$& $\lambda P\omega = \blue{\lambda C}$
\end{tabular}
\end{center}
\medskip

\blue{calculus of constructions} \\
\adviwait
by itself not powerful enough to encode mathematics
\medskip

impredicative definition of $\,{\mathbb N}$ \\
\dashskip only iterator \\
\dashskip \red{no recursor}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Bas: and category theory?}
\begin{center}
\begin{picture}(200,100)
\advirecord{c1}{\put(0,70){\makebox(0,0){\gray{higher order logic}}}}
\advirecord{c2}{\put(70,22){\gray{\line(-3,2){56}}}}
\put(70,90){\makebox(0,0){set theory}}
\put(90,21){\line(-1,3){20}}
\put(130,90){\makebox(0,0){type theory}}
\put(110,21){\line(1,3){20}}
\advirecord{c3}{\put(200,70){\makebox(0,0){\red{category theory}}}}
\advirecord{c4}{\put(130,22){\red{\line(3,2){56}}}}
\put(100,10){\makebox(0,0){\textbf{foundations of mathematics}}}
\end{picture}
\end{center}
\adviwait
\adviplay{c3}
\adviplay{c4}
\adviwait
\adviplay{c1}
\adviplay{c2}
\bigskip
\adviwait

\blue{a posting to FOM by Colin McLarty} \\
14 axioms, numbered 1 to 15\quad (no axiom 8)
\medskip

\green{`a well-pointed topos with natural numbers and choice'}
\vfill
\end{slide}

\begin{slide}
\slidetitle{even more}

\begin{itemize}
\item[$\bullet$]
\blue{ECC}

Luo's original LICS paper
\medskip
\adviwait

\item[$\bullet$]
\blue{New Foundations}

description by e-mail from Randall Holmes
\medskip
\adviwait

\item[$\bullet$]
\blue{Isabelle/Pure}

slides of a talk by Stefan Berghofer \\
reference manual by Larry Paulson
\medskip

HOL Light context = the full system \\
Isabelle/Pure context = an abstraction of the real system

\green{close to Church's original version of higher order logic}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the whole set}

\medskip
\begin{quote}
\begin{tabular}{ll}
\textbf{set theory} & \advirecord{d3}{ZFC} \\
& \advirecord{d5}{NF} \\
\noalign{\medskip}
\textbf{higher order logic\qquad} & \advirecord{d1}{Isabelle/Pure} \\
& HOL Light \\
\noalign{\medskip}
\textbf{type theory} & \advirecord{d2}{CC} \\
& ECC \\
& \advirecord{d4}{MLW} \\
\noalign{\medskip}
\textbf{category theory} & Topos
\end{tabular}
\end{quote}
\adviplay{d1}
\adviplay{d2}
\adviplay{d3}
\adviplay{d4}
\adviplay{d5}
\adviwait
\adviplay[slidegray]{d1}
\adviplay[slidegray]{d2}
\adviwait
\adviplay{d1}
\adviplay{d2}
%\adviplay[slidegreen]{d5}
%\adviwait
%\adviplay{d5}
\adviplay[slidered]{d3}
\adviplay[slidered]{d4}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{intermezzo I}
\slidetitle{why should a formalist dislike constructivism?}
formalism \\
\green{rules of logic are as meaningless as the rules of chess}
\medskip

\blue{Bas:}
\begin{center}
rules of classical math $\;\longleftrightarrow\;$ rules of constructive math
\end{center}

no reason for a formalist to prefer one over the other
\bigskip
\adviwait

I'm a formalist and \\
\red{when working on these Automath contexts I found that Bas is right}
\medskip
\adviwait

but\dots

\vfill
\end{slide}

\begin{slide}
\slidetitle{how a formalist can dislike constructivism}
Mark Balaguer \\
\green{synonyms for formalism:}

\begin{itemize}
\item[$\bullet$]
\textbf{full-blooded Platonism}

$\left.
\begin{array}{l}
\mbox{ZF sets satisfying the continuum hypothesis} \\
\mbox{ZF sets not satisfying the continuum hypothesis}
\end{array}
\right\rbrace
\mbox{ both exist}$
\adviwait

\item[$\bullet$]
\textbf{fictionalism}

existence of the number $\pi$ is like \\
existence of the One Ring from the Lord of the Rings

\end{itemize}
\medskip
\adviwait

\red{so personally I dislike constructivism because I prefer \rlap{Platonist fiction}} \\
(exactly like someone might prefer romantic novels over thrillers)

\vfill
\end{slide}

\begin{slide}
\sectiontitle{intermezzo II}
\slidetitle{should a proof checker be based on a logical framework?}
Isabelle: \\
\dashskip {\tiny $\!$}many logics, but$\,\ldots$ \\
\dashskip \red{almost all Isabelle users use the HOL logic}

\green{not worth the energy to support more than one logic in a system}
\adviwait

\dashskip {(likewise almost all mathematicians use classical logic \red{$\ddot\smallsmile$})}
\bigskip
\adviwait

\green{but basing a system on a logical framework might still be a good idea} \\
proof checking `micro-kernel'
\medskip

the substitution operation is the `kernel of the de Bruijn kernel' \\
(\textbf{two} bugs in HOL Light kernel recently, \textbf{both} with $\alpha$-conversion)

\vfill
\end{slide}

\begin{slide}
\slidetitle{are these contexts accurate?}

interesting question: \\
\green{can you prove the same from the formalization as in the original system?}
\medskip

\begin{itemize}
\item[]
\red{easy:} a context can mimic proofs

\item[]
\red{difficult:} a context cannot prove \textbf{more}

\end{itemize}
\bigskip
\adviwait

this kind of result is standard for the LF logical framework
\medskip

\green{I haven't pursued this for my Automath contexts} \\
(main focus here: complexity of the systems)

\vfill
\end{slide}

\begin{slide}
\sectiontitle{on with it$\,\ldots$}
\slidetitle{an Automath context for FOL}

\begin{tabular}{rlrll}
\noalign{\textbf{the types}}
\noalign{\medskip}
$*$& & \red{prop} &$:$ {\small TYPE} &$=$ {\small PRIM} \\
$*$& $[$a$:$prop$]$ & \red{proof} &$:$ {\small TYPE} &$=$ {\small PRIM} \\
$*$& & \red{term} &$:$ {\small TYPE} &$=$ {\small PRIM} \adviwait\\
\noalign{\medskip}
\noalign{\textbf{first order formulas}}
\noalign{\medskip}
$*$& & \red{false} &$:$ prop &$=$ {\small PRIM} \\
a $*$& $[$b$:$prop$]$ & \red{imp} &$:$ prop &$=$ {\small PRIM} \\
$*$& $[$p$:${}$[$z,term$]$prop$]$ & \red{for} &$:$ prop &$=$ {\small PRIM} \\
%\noalign{\medskip}
%\adviwait
$*$& $[$x$:$term$][$y$:$term$]$ & \red{eq} &$:$ prop &$=$ {\small PRIM} \\
%\noalign{\medskip}
\adviwait
a $*$& & \red{not} &$:$ prop &$=$ \green{imp$($a,false$)$}
\end{tabular}

\vspace{-1em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{an Automath context for FOL (continued)}

\begingroup
\small
\begin{tabular}{rlrll}
\noalign{{\normalsize \textbf{natural deduction}}}
\noalign{\medskip}
b $*$& $[$\_1$:${}$[$\_,proof$($a$)]$proof$($b$)]$ & \red{imp\_intro} &$:$ proof$($imp$($a,b$))$ &$=$ {\footnotesize PRIM} \\
b $*$& \rlap{$[$\_1$:$proof$($imp$($a,b$))][$\_2$:$proof$($a$)]$} \\
& & \red{imp\_elim} &$:$ proof$($b$)$ &$=$ {\footnotesize PRIM} \\
\noalign{\medskip}
p $*$& $[$\_1$:${}$[$z,term$]$proof$(\langle$z$\rangle$p$)]$ & \red{for\_intro} &$:$ proof$($for$($p$))$ &$=$ {\footnotesize PRIM} \\
p $*$& $[$\_1$:$proof$($for$($p$))][$z$:$term$]$ & \red{for\_elim} &$:$ proof$(\langle$z$\rangle$p$)$ &$=$ {\footnotesize PRIM} \adviwait\\
\noalign{\medskip}
a $*$& $[$\_1$:$proof$($not$($not$($a$)))]$ & \red{classical} &$:$ proof$($a$)$ &$=$ {\footnotesize PRIM} \adviwait\\
\noalign{\medskip}
x $*$& & \red{eq\_intro} &$:$ proof$($eq$($x,x$))$ &$=$ {\footnotesize PRIM} \\
y $*$& \rlap{$[$q$:${}$[$z,term$]$prop$][$\_1$:$proof$($eq$($x,y$))][$\_2$:$proof$(\langle$x$\rangle$q$)]$} \\
& & \red{eq\_elim} &$:$ proof$(\langle$y$\rangle$q$)$ &$=$ {\footnotesize PRIM}
\end{tabular}
\endgroup

\vfill
\end{slide}

\def\arrow{$\to$}
\begin{slide}
\slidetitle{the same context for $\lambda P$ \advirecord{e1}{in Coq}}
\vspace{-\bigskipamount}
\vspace{-\medskipamount}
\begingroup
\small
\begin{alltt}
\advirecord{e2}{{Definition}} \red{prop} : Type \advirecord{e3}{{:=} \green{Prop}.}
\advirecord{e4}{{Definition}} \red{proof} [a:prop] : Type \advirecord{e5}{{:=} \green{~a}.}
 \advirecord{e6}{{Inductive}} \red{term} : Type \advirecord{e7}{{:=} {i : (A:Set)A{\arrow}term}.}
\end{alltt}
\begin{alltt}
\advirecord{e8}{{Definition}} \red{false} : prop \advirecord{e9}{{:=} \green{True}.}
\advirecord{e10}{{Definition}} \red{imp} [a,b:prop] : prop \advirecord{e11}{{:=} \green{~(~a{\arrow}~b)}.}
\advirecord{e12}{{Definition}} \red{for} [p:term{\arrow}prop] : prop \advirecord{e13}{{:=} \green{~(z:term)~(p z)}.}
\advirecord{e14}{{Definition}} \red{eq} [x,y:term] : prop \advirecord{e15}{{:=} \green{~x==y}.}
\end{alltt}
\begin{alltt}
\advirecord{e16}{{Definition}} \red{not} [a:prop] : prop \advirecord{e17}{{:=} \green{(imp a false)}}\advirecord{e17a}{.}
\end{alltt}
\begin{alltt}
\advirecord{e18}{{Definition}} \red{imp_intro}
  [a,b:prop; _1:(proof a){\arrow}(proof b)] : (proof (imp a b))
 \advirecord{e19}{{:=} \green{[_2:(imp a b)](_2 _1)}.}
\advirecord{e20}{{Definition}} \red{imp_elim}
  [a,b:prop; _1:(proof (imp a b)); _2:(proof a)] : (proof b)
 \advirecord{e21}{{:=} \green{[_3:b](_1 [_4:~a{\arrow}~b](_4 _2 _3))}.}
\end{alltt}
\endgroup
\adviplay{e17}
\adviwait
\adviplay[slideblue]{e1}
\adviplay{e2}
\adviplay{e3}
\adviplay{e4}
\adviplay{e5}
\adviplay{e6}
\adviplay{e7}
\adviplay{e8}
\adviplay{e9}
\adviplay{e10}
\adviplay{e11}
\adviplay{e12}
\adviplay{e13}
\adviplay{e14}
\adviplay{e15}
\adviplay{e16}
\adviplay{e17a}
\adviplay{e18}
\adviplay{e19}
\adviplay{e20}
\adviplay{e21}
\vspace{-1em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{the same context for $\lambda P$ in Coq (continued)}
\vspace{-\bigskipamount}
\vspace{-\medskipamount}
\begingroup
\small
\begin{alltt}
{Definition} \red{for_intro}
  [p:term{\arrow}prop; _1:(z:term)(proof (p z))] : (proof (for p))
 {:=} \green{[_2:(for p)](_2 _1)}.
{Definition} \red{for_elim}
  [p:term{\arrow}prop; _1:(proof (for p)); z:term] : (proof (p z))
 {:=} \green{[_3:(p z)](_1 [_4:(z:term)~(p z)](_4 z _3))}.
\end{alltt}
\begin{alltt}
{Definition} \red{classical} \rlap{[a:prop; _1:(proof (not (not a)))] : (proof a)}
 {:=} \rlap{\green{\footnotesize[_2:a](_1 [_3:~(not a){\arrow}~false](_3 [_4:(not a)](_4 [_5:~a; _:True](_5 _2)) I))}.}
\end{alltt}
\begin{alltt}
{Definition} \red{eq_intro} [x:term] : (proof (eq x x))
 {:=} \green{[_1:~x==x](_1 (refl_eqT term x))}.
{Definition} \red{eq_elim}
  \rlap{[x,y:term; q:term{\arrow}prop; _1:(proof (eq x y)); _2:(proof (q x))] :}
   (proof (q y))
 {:=} \green{[_3:(q y)](_1 [_4:x==y](_2 (eqT_ind_r term y q _3 x _4)))}.
\end{alltt}
\endgroup
\vspace{-1em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{summarizing contexts}
\begin{itemize}
\item[]
\textbf{the counts}
\begin{center}
\begin{tabular}{lcr}
the types && 3 \\
first order formulas && 4 \\
natural deduction && 7 \\
\noalign{\smallskip}
\hline
\noalign{\smallskip}
total && \red{14}
\end{tabular}
\end{center}
\adviwait

\item[]
\textbf{the types}
\begin{center}\tt
\green{\begin{tabular}{rl}
 & prop \\
{}[prop] & proof \\
 & term
\end{tabular}}
\end{center}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{summary of ZFC}
\begin{center}
\begin{tabular}{lcr}
first order logic && 15 \\
definition by cases && 2 \\
set theory && 6 \\
the axioms && 8 \\
choice && 1 \\
\noalign{\smallskip}
\hline
\noalign{\smallskip}
total && \red{32}
\end{tabular}
\end{center}
\medskip

\begin{center}\tt
\green{\begin{tabular}{rl}
 & prop \\
{}[prop] & proof \\
 & set
\end{tabular}}
\end{center}
\vfill
\end{slide}

\begin{slide}
\slidetitle{summary of MLW$\,^{\sf ext}$}
\vspace{-2.2\bigskipamount}
\ 
\vbox to 0pt{
\begin{center}
\begin{tabular}{lcr}
pseudoterms && 1 \\
judgements && 4 \\
equality rules && 8 \\
congruence rules && 2 \\
the empty type && 4 \\
the unit type && 7 \\
the Booleans && 13 \\
product types && 9 \\
sum types && 11 \\
W types && 8 \\
extensionality && 10 \\
\noalign{\smallskip}
\hline
\noalign{\smallskip}
total && \red{77}
\end{tabular}
\end{center}
\vss
}
\adviwait
\adviembed{gv -g 1113x781+-89+-28 -spartan -page 7 -nocenter /home/freek/math/zfc-etc/PAPERS/ts-st.ps.gz}
\adviwait
\adviembed{xterm -g 100x37 -fn 10x20 -T mlw-ext-j.aut -e less /home/freek/math/zfc-etc/mlw-ext-j.aut}
\adviwait
\adviembed{xterm -g 100x37 -fn 10x20 -T mlw-ext-j.term -e /home/freek/talks/zfc-etc/showterm}

\vfill
\end{slide}

\begin{slide}
\slidetitle{summary of MLW$\,^{\sf ext}$ (continued)}
\begin{center}\tt
\green{\begin{tabular}{rl}
 & pterm \\
{}[pterm] & type \\
{}[pterm][pterm] & eq\char`\_type\hspace{9em} \\
{}[pterm][pterm] & in \\
{}[pterm][pterm][pterm] & eq\char`\_in
\end{tabular}}
\end{center}
\bigskip

\red{the four judgments of Martin-L\"of type theory:}
\begin{center}
\begin{tabular}{c}
$A\;{\sf set}$ \\
$A = B$ \\
$a \in A$ \\
$a = b \in A$
\end{tabular}
\end{center}

\vspace{-1em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{encoding judgments using HOAS}
\begin{center}
\strut\llap{the type\quad}\red{\texttt{in($a$,$A$)}}\rlap{\quad is inhabited}
\end{center}
if and only if
$$\blue{\Gamma} \vdash \red{a \in A}\rlap{ \quad is derivable}\phantom{\vdash \Gamma}\medskip\adviwait$$

the context \blue{$\Gamma$} is not explicitly encoded as an Automath type
\adviwait

so type theory binding is represented by Automath binding
\medskip

\begin{center}
\red{\texttt{lambda($A$,$b$)}} \\
\strut\rlap{}\hfill \llap{}\green{$b : \texttt{[x,pterm]pterm}$}\rlap{} \hfill\strut
\end{center}
represents
$$\red{\lambda x{:}A.\, b}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{an example: one of the MLW rules}
%Peter Aczel's paper: MLW$\,^{\sf ext}$ in exactly three pages
%\medskip
%
\green{introduction rule for W types}
$$
x:A\Rightarrow B\;{\sf type}\qquad a:A\qquad f:(B[a/x]\to(Wx:A)B)
\over
{\it \red{sup}}(a,f):(Wx:A)B
$$

\green{Automath rendering}
\begin{quote}
\begin{alltt}
\gray{* [A:pterm][B:[x,pterm]pterm]}
\end{alltt}
\begin{alltt}
B * [a,pterm][f:pterm]
  [_1:[x,pterm][_:in(x,A)]type(<x>B)]
  [_2:in(a,A)]
  [_3:in(f,arrow(<a>B,W(A,B)))]
  W_intro : in(\red{sup}(a,f),W(A,B)) := PRIM
\end{alltt}
\end{quote}

\vfill
\end{slide}

\begin{slide}
\slidetitle{pseudo-terms or putting the types inside the Automath types?}
alternative encoding

\begin{center}\tt
\green{\begin{tabular}{rl}
& type \\
{}[type] & term \\
{}[type][type] & eq\char`\_type\hspace{4em} \\
{}[A:type][term(A)][term(A)] & eq
\end{tabular}}
\end{center}
\bigskip
\adviwait

introduction rule for W types then becomes:
\begin{quote}
\begin{alltt}
\gray{* [A:type][B:[x,term(A)]type]}
\end{alltt}
\begin{alltt}
B * [a:term(A)][f:term(arrow(<a>B,W(A,B)))]
  \red{sup} : term(W(A,B)) := PRIM
\end{alltt}
\end{quote}

\vfill
\end{slide}

\begin{slide}
\slidetitle{however this needs explicit conversions}
\begin{quote}
\begin{alltt}
\gray{* [A:type]}
\gray{A * [B:type]}
\end{alltt}
\begin{alltt}
B * [a:term(A)][_2:eq_type(A,B)]
  \red{conv} : term(B) := PRIM
\end{alltt}
\end{quote}
\vspace{-\bigskipamount}
\vspace{-\medskipamount}
\ 
\adviwait

\textbf{example:}
\vspace{-\medskipamount}
\begin{eqnarray*}
\pi_2(\mbox{\it pair\/}(a,b)) &:& B[\pi_1(\mbox{\it pair\/}(a,b))/x] \\
\pi_2(\mbox{\it pair\/}(a,b)) &:& B[a/x]
\end{eqnarray*}
\vspace{-\bigskipamount}
\vspace{-\medskipamount}

\begin{quote}
\begin{alltt}
\green{pi_2(pair(a,b))}
\end{alltt}
\begin{alltt}
\red{conv}(<pi_1(pair(a,b))>B,<a>B,\green{pi_2(pair(a,b))},
  cong_type(A,pi_1(pair(a,b)),a,B,Sigma_eq_1))
\end{alltt}
\end{quote}
\medskip
\adviwait

\blue{Thorsten: {this approach will only work with {extra equality rules}}}

\vspace{-1em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{Thorsten: use John Major equality instead}
\begin{center}\tt
\green{\begin{tabular}{rl}
 & type \\
{}[type] & term \\
{}[type][type] & eq\char`\_type\hspace{2em} \\
{}\phantom{[A:type][term(A)][term(A)]}\llap{[A:type][B:type][term(A)][term(B)]} & eq
\end{tabular}}
\end{center}
\bigskip
\adviwait

so this \red{replaces} the judgment
$$a = b \in A$$
by
$$a \in A = b \in B\bigskip$$
\adviwait
\red{I didn't pursue this: I wanted to model, not to improve}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the statistics: number of primitive notions}
\vspace{-2.2\bigskipamount}
\ 
\vbox to 0pt{
\statbarunit=3.31pt
\hfill\begin{tabular}{rl}
& \rlap{\textbf{set theory}} \\
ZFC & \statbar{32} \\
NF & \green{\statbar{37}} \\
& \rlap{\textbf{higher order logic}} \\
Pure & \graystatbar{23} \\
\red{HOL} & \statbar{25} \\
& \rlap{\textbf{type theory}} \\
CC & \graystatbar{30} \\
ECC & \statbar{46} \\
MLW & \statbar{77} \\
& \rlap{\textbf{category theory}} \\
Topos & \statbar{45}
\end{tabular}\hfill\strut
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the statistics: size of the formalization}
\vspace{-2.2\bigskipamount}
\ 
\vbox to 0pt{
\statbarunit=.221pt
\hfill\begin{tabular}{rl}
& \rlap{\textbf{set theory}} \\
ZFC & \statbar{751} \\
NF & \green{\statbar{640}} \\
& \rlap{\textbf{higher order logic}} \\
Pure & \graystatbar{532} \\
HOL & \statbar{928} \\
& \rlap{\textbf{type theory}} \\
CC & \graystatbar{515} \\
\red{ECC} & \statbar{696} \\
MLW & \statbar{1154} \\
& \rlap{\textbf{category theory}} \\
Topos & \statbar{1153}
\end{tabular}\hfill\strut
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{the statistics: size of the $\lambda$-term}
\vspace{-2.2\bigskipamount}
\ 
\vbox to 0pt{
\statbarunit=.0711pt
\hfill\begin{tabular}{rl}
& \rlap{\textbf{set theory}} \\
\red{ZFC} & \statbar{1487} \\
NF & \green{\statbar{972}} \\
& \rlap{\textbf{higher order logic}} \\
Pure & \graystatbar{1200} \\
HOL & \statbar{2868} \\
& \rlap{\textbf{type theory}} \\
CC & \graystatbar{784} \\
ECC & \statbar{1636} \\
MLW & \statbar{3589} \\
& \rlap{\textbf{category theory}} \\
Topos & \statbar{2601}
\end{tabular}\hfill\strut
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Thorsten's comment}
e-mail message:

\begin{quote}
\rightskip=0pt
\green{
I can't help making the obvious comment that \red{simplicity can't be
measured by size.} Actually, I often find that the contrary is the case
that simpler systems are slightly longer than more complicated ones.
}

\green{
E.g.\ if you look at some of these \black{obfuscated C-programs} which are very
short but doing something very subtle (people sometimes put them into
their sigs), would you call them `simple'? Are those not precisely
what people call a `hack'?
}
\end{quote}

\vfill
\end{slide}

\begin{slide}
\slidetitle{why can't it be simpler?}
\begin{itemize}
\item[$\bullet$]
\textbf{foundations of physics}

\begin{itemize}
\item \green{standard model}
\end{itemize}
\adviwait

18 dimensionless parameters \qquad\qquad\qquad \advirecord{f}{$\leftarrow$ large number} \\
(charge of electron, quark masses, etc)
\medskip
\adviwait
\adviplay[slidered]{f}
\adviwait

\item[$\bullet$]
\textbf{foundations of mathematics}

\begin{itemize}
\item \advirecord{f1}{{\tiny\strut}\rlap{ZFC}}
\hspace{4cm}\advirecord{f5}{(32 primitive notions)}
\adviplay[slidegreen]{f1}
\adviwait
\item \advirecord{f2}{{\tiny\strut}\rlap{type theory}}
\hspace{4cm}\advirecord{f6}{(46 primitive notions)}
\adviplay{f1}
\adviplay[slidegreen]{f2}
\adviwait
\adviplay{f2}
\item \advirecord{f3}{{\tiny\strut}\rlap{NF}}
\hspace{4cm}\advirecord{f7}{(37 primitive notions)}
\adviplay[slidegreen]{f3}
\adviwait
\adviplay{f3}
\item \advirecord{f4}{{\tiny\strut}\rlap{category theory}}
\hspace{4cm}\advirecord{f8}{(45 primitive notions)}
\adviplay[slidegreen]{f4}
\end{itemize}
\medskip
\adviwait
\adviplay{f4}
\adviplay[slidegreen]{f5}
\adviplay[slidegreen]{f6}
\adviplay[slidegreen]{f7}
\adviplay[slidegreen]{f8}

\green{in all cases:} number of primitive notions larger than 18 \\
\red{mathematics is even worse than physics!}

\end{itemize}

\vspace{-1em}
\vfill
\end{slide}

\end{document}
