[FOM] Formalization Thesis

Freek Wiedijk freek at cs.ru.nl
Mon Jan 7 08:13:13 EST 2008


Andrej:

>People who actually work on formalization know that
>having powerful type-theoretic infrastructure is absolutely
>necessary to keep things organized (imagine having 3000
>lemmas...). So they use type theory instead.

Nonsense.  Of the systems that are the most interesting for
formalization of mathematics (the various HOLs, Isabelle,
Coq, Mizar, maybe PVS) only Coq is based on type theory.
The rest all are as classical as possible.

Or do you call a system based on "type theory" whenever it
is has a notion of type?  That would be strange: Mizar has a
very interesting kind of types, but it is _very much_ based
on set theory.  _(And_ it has the biggest library of them
all, with an order of magnitude more lemmas than you quote.)

Freek


More information about the FOM mailing list