\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(B)] [_2:in(a,A)] [_3:in(f,arrow(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(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}(B,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}