a comparison of foundations of mathematics

Freek Wiedijk University of Nijmegen

room A4028 2003 11 10, 11:00 is ZF a hack?

Raph Levien (maintainer of Ghostscript), on a forum called Advogato

I was talking […] with Bram, and he called ZF set theory a ‘hack.’ I more or less agree, but […]

Bob Solovay does not think ZF is a hack personally I do think ZF is a bit of a hack

• distinction between ‘sets’ and ‘classes’

• two levels of ‘logic’ and ‘set theory’

similar concepts on both levels ∃ in logic ⟷ ⋃ on sets

no such distinction in HOL!

Henk’s napkin how many ZF axioms are there?

Set properties  2  ext, found
Set existence  6 8

Set(∅) Set({x, y})

(Set(⋃ x)) / (Set(F “x))

Set(Px) Set(ω)

ZFC & HOL in Automath: the simplicity shootout number of primitive notions {ZFC \atop HOL} size of the specification {ZFC \atop HOL} size of the λ-term {ZFC \atop HOL} and what about Coq?

inductive types in Coq: recursion principles Luis: the rules are nowhere explicitly spelled out

⇒ Coq logic: not simple

Thorsten: extensional Martin-Löf type theory with W types

elements of the type Wx:A. B are trees nodes are labeled with elements of A edges (from node labelled a) for each element of B[x := a]

Nordström/Petersson/Smith book: not presented as ‘system’ Peter Aczel paper (on relation between type theory and set theory):

MLW^{ext}

ZFC and MLW: nice TLAs and what about PTSs?

proper type systems Henk’s tutorial paper: problems in type theory

\begin{aligned}LF & = & λP \\ CC & = & λP ω = λC \end{aligned}

calculus of constructions by itself not powerful enough to encode mathematics

impredicative definition of ℕ only iterator no recursor Bas: and category theory?

[figure: higher order logic; set theory; type theory; category theory; foundations of mathematics]

a posting to FOM by Colin McLarty 14 axioms, numbered 1 to 15 (no axiom 8)

‘a well-pointed topos with natural numbers and choice’ even more

• ECC Luo’s original LICS paper

• New Foundations description by e-mail from Randall Holmes

• Isabelle/Pure slides of a talk by Stefan Berghofer reference manual by Larry Paulson

HOL Light context = the full system Isabelle/Pure context = an abstraction of the real system close to Church’s original version of higher order logic the whole set

set theory  ZFC

NF

higher order logic  Isabelle/Pure

HOL Light

type theory  CC

ECC MLW

category theory  Topos

intermezzo I

why should a formalist dislike constructivism? formalism rules of logic are as meaningless as the rules of chess Bas:

rules of classical math ⟷ rules of constructive math no reason for a formalist to prefer one over the other I’m a formalist and when working on these Automath contexts I found that Bas is right but… how a formalist can dislike constructivism

Mark Balaguer synonyms for formalism:

• full-blooded Platonism

\begin{matrix}ZF sets satisfying the continuum hypothesis \\ ZF sets not satisfying the continuum hypothesis \end{matrix} \} both exist

• fictionalism existence of the number π is like existence of the One Ring from the Lord of the Rings

so personally I dislike constructivism because I prefer Platonist fiction (exactly like someone might prefer romantic novels over thrillers)

intermezzo II

should a proof checker be based on a logical framework?

Isabelle:

many logics, but … almost all Isabelle users use the HOL logic

not worth the energy to support more than one logic in a system

(likewise almost all mathematicians use classical logic ¨⌣)

but basing a system on a logical framework might still be a good idea proof checking ‘micro-kernel’

the substitution operation is the ‘kernel of the de Bruijn kernel’ (two bugs in HOL Light kernel recently, both with α-conversion) are these contexts accurate?

interesting question: can you prove the same from the formalization as in the original system?

easy: a context can mimic proofs

difficult: a context cannot prove more

this kind of result is standard for the LF logical framework

I haven’t pursued this for my Automath contexts (main focus here: complexity of the systems)

on with it …

an Automath context for FOL the types

∗  prop : TYPE = PRIM
∗ [a:prop]  proof : TYPE = PRIM
∗  term : TYPE = PRIM

first order formulas

∗  false : prop = PRIM
a ∗ [b:prop]  imp : prop = PRIM
∗ [p:[z,term]prop]  for : prop = PRIM
∗ [x:term][y:term]  eq : prop = PRIM
a ∗  not : prop = imp(a,false)

an Automath context for FOL (continued) natural deduction

b ∗ [ 1:[ ,proof(a)]proof(b)] imp intro : proof(imp(a,b)) = PRIM
b ∗ [ 1:proof(imp(a,b))][ 2:proof(a)]
imp elim : proof(b)  = PRIM
p ∗ [ 1:[z,term]proof(⟨z⟩p)]  for intro : proof(for(p))  = PRIM
p ∗ [ 1:proof(for(p))][z:term]  for elim : proof(⟨z⟩p)  = PRIM
a ∗ [ 1:proof(not(not(a)))]  classical : proof(a)  = PRIM
x ∗  eq intro : proof(eq(x,x))  = PRIM
y ∗ [q:[z,term]prop][ 1:proof(eq(x,y))][ 2:proof(⟨x⟩q)]
eq elim : proof(⟨y⟩q)  = PRIM

the same context for λP in Coq

Definition prop : Type := Prop.
Definition proof [a:prop] : Type := ~a.
 Inductive term : Type := i : (A:Set)A→term.
Definition false : prop := True.
Definition imp [a,b:prop] : prop := ~(~a→~b).
Definition for [p:term→prop] : prop := ~(z:term)~(p z).
Definition eq [x,y:term] : prop := ~x==y.
Definition not [a:prop] : prop := (imp a false).
Definition imp_intro
  [a,b:prop; _1:(proof a)→(proof b)] : (proof (imp a b))
 := [_2:(imp a b)](_2 _1).
Definition imp_elim
  [a,b:prop; _1:(proof (imp a b)); _2:(proof a)] : (proof b)
 := [_3:b](_1 [_4:~a→~b](_4 _2 _3)).

the same context for λP in Coq (continued)

Definition for_intro
  [p:term→prop; _1:(z:term)(proof (p z))] : (proof (for p))
 := [_2:(for p)](_2 _1).
Definition for_elim
  [p:term→prop; _1:(proof (for p)); z:term] : (proof (p z))
 := [_3:(p z)](_1 [_4:(z:term)~(p z)](_4 z _3)).
Definition classical [a:prop; _1:(proof (not (not a)))] : (proof a)
 := [_2:a](_1 [_3:~(not a)→~false](_3 [_4:(not a)](_4 [_5:~a; _:True](_5 _2)) I)).
Definition eq_intro [x:term] : (proof (eq x x))
 := [_1:~x==x](_1 (refl_eqT term x)).
Definition eq_elim
  [x,y:term; q:term→prop; _1:(proof (eq x y)); _2:(proof (q x))] :
   (proof (q y))
 := [_3:(q y)](_1 [_4:x==y](_2 (eqT_ind_r term y q _3 x _4))).

summarizing contexts

the counts

the types  3
first order formulas  4
natural deduction  7
total  14

the types

            prop

    [prop]  proof

            term

summary of ZFC

first order logic  15
definition by cases  2
set theory  6
the axioms  8
choice  1
total  32

            prop

    [prop]  proof

            set

summary of MLW^{ext}

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
total  77

summary of MLW^{ext} (continued)

                            pterm

                   [pterm]  type
            [pterm][pterm]  eq_type
            [pterm][pterm]  in
     [pterm][pterm][pterm]  eq_in

the four judgments of Martin-Löf type theory:

\begin{matrix}A set \\ A = B \\ a ∈ A \\ a = b ∈ A \end{matrix}

encoding judgments using HOAS

the type in(a,A) is inhabited

if and only if Γ ⊢ a ∈ A is derivable

the context Γ is not explicitly encoded as an Automath type so type theory binding is represented by Automath binding

                       lambda(A,b)
                    b : [x,pterm]pterm

represents

λx:A. b

an example: one of the MLW rules

introduction rule for W types

\frac{x : A ⇒ B type  a : A  f : (B[a/x] → (W x : A)B)}{sup(a, f) : (W x : A)B}

Automath rendering

* [A:pterm][B:[x,pterm]pterm]
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(sup(a,f),W(A,B)) := PRIM

pseudo-terms or putting the types inside the Automath types? alternative encoding

                                    type

                           [type]  term
                     [type][type]  eq_type
       [A:type][term(A)][term(A)]  eq

introduction rule for W types then becomes:

   * [A:type][B:[x,term(A)]type]
   B * [a:term(A)][f:term(arrow(<a>B,W(A,B)))]
     sup : term(W(A,B)) := PRIM

however this needs explicit conversions

* [A:type]
A * [B:type]
B * [a:term(A)][_2:eq_type(A,B)]
  conv : term(B) := PRIM

example:

π_{2}(pair(a, b)) : B[π_{1}(pair(a, b))/x]
π_{2}(pair(a, b)) : B[a/x]

pi_2(pair(a,b))
conv(<pi_1(pair(a,b))>B,<a>B,pi_2(pair(a,b)),
  cong_type(A,pi_1(pair(a,b)),a,B,Sigma_eq_1))

Thorsten: this approach will only work with extra equality rules Thorsten: use John Major equality instead

                                      type

                             [type]  term
                       [type][type]  eq_type
 [A:type][B:type][term(A)][term(B)]  eq

so this replaces the judgment

a = b ∈ A

by

a ∈ A = b ∈ B

I didn’t pursue this: I wanted to model, not to improve the statistics: number of primitive notions

set theory ZFC NF

higher order logic Pure HOL

type theory CC ECC MLW

category theory Topos the statistics: size of the formalization

set theory ZFC NF

higher order logic Pure HOL

type theory CC ECC MLW

category theory Topos the statistics: size of the λ-term

set theory ZFC NF

higher order logic Pure HOL

type theory CC ECC MLW

category theory Topos Thorsten’s comment

e-mail message:

I can’t help making the obvious comment that 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. E.g. if you look at some of these 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’? why can’t it be simpler?

• foundations of physics – standard model 18 dimensionless parameters ← large number (charge of electron, quark masses, etc)

• foundations of mathematics – ZFC (32 primitive notions)

– type theory (46 primitive notions)

– NF (37 primitive notions)

– category theory (45 primitive notions)

in all cases: number of primitive notions larger than 18 mathematics is even worse than physics!