[FOM] Formalization Thesis

[Andrej Bauer]

Freek Wiedijk wrote:
> 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.

It is really uneccesary to get into any sort of competition here. I am
sorry I contributed to this thread, and I would prefer if my posts were
not so easily branded as nonsense. Can we have a little more respect and
understanding on this mailing list, please? Please bare in mind that
electronic communication has the unfortunate tendency to make people's
statements sound more negative than intended.

Let me just say that "classical" and "type theory" are not disjoint
concepts. You can perfectly well have classical type theory. I did not
say "constructive type theory", nor did I say "Martin-Lof type theory".
That _would_ imply non-classical.

> Or do you call a system based on "type theory" whenever it
> is has a notion of type?

I always thought that HOL and Isabelle rely on rather large amounts of
type theory. Is it not the case that Isabelle essentially verifies the
correctness of a proof by type checking? Please correct me if I am wrong.

I would say a system is based on type theory when types play an
important role. For example, type constructions such as dependent
products and sums of types should play an essential part, and there
should be some relation with the propositions-as-types "paradigm".

A system not based on type theory would presumably be one that is
essentially first-order logic with a single sort (or maybe a small
number of sorts, such as "set" and "class") that cannot be combined into
new fancy sorts (other than perhaps finite products of sorts).

Good bye.

Andrej Bauer