[FOM] Emulating Mathematicians

[Harvey Friedman]

This is in response to Eklund's FOM posting.

I am going to try to put together some numbered postings with some
definite proposals concerning Proof Assistants where I take

EMULATING CLEAR HEADED MATHEMATICIANS

as the clear driving force behind the approach.

> I've often remarked that set theory is untyped, and this is one example.
> That j essentially "shifts types" (from nat to real), but since types and
> type constructors are not part of set theory, things indeed "get ugly
> quickly". As most of us know, set theory is ugly as it is.

Clear headed mathematicians keep this from getting ugly.
>
> Type constructing that j is not key. Type construction for managing power
> sets is. "Before Russell", set theorists new that and found it dubious to
> use X U PX. It is dubious to use it, and things get ugly when we do.
> Kreisel's 'Two notes ...' and many others have pointed that out.

Clear headed mathematicians keep things like X U PX from getting ugly.
>
> Natural numbers is not a set. It's potentially a complicated construction of
> constructed types. Developing such things would significantly lower the
> importance of Gödel, Kleene and Princeton, and very few are prepared to try
> anything out that potentially leads to that lowering.

Clear headed mathematicians tell us that natural numbers form a set.
So therefore natural numbers form a set.
>
> Set theory is imprisoned by its own stupidity.

Clear headed mathematicians readily accept the set theoretic
framework, and work nicely and simply on top of it using subtle
conventions that it is our job to unearth systematically. This is an
entirely realistically doable enterprise, but one which I do not think
has begun properly and systematically enough, with enough imagination.
The main reason for this is that one certainly wants at least
prototyping and things get expensive unless you have crazy nerds like
me who don't sleep, without pay, and of course you need thousands of
them. So there is a notion of "essentially intellectually solving this
problem" which is often dismissed as worthless. But I maintain that
there is definitely the clear notion of "essentially intellectually
solving this problem" and I have full confidence that if somebody does
this, as long as their work is preserved say on the side of a nuclear
resistant mountain, they will smile in their grave that it eventually
did take hold and change the world.
>
> We don't have that type theory. Type theories around are inadequate e.g.
> because they don't handle the "power type", and some in early stages have
> been brave to use "the type of all types". Abandoning set theory and
> reinventing problems is not what we should do.
>
> However, we must now, and we will know.

We must embrace the standard f.o.m. that clear headed mathematicians
readily accept and adhere to, adding subtle sugar that we must lay the
proper foundations for. f.o.s. = foundations of sugar.

Harvey Friedman