[FOM] Foundational Frameworks

[Harvey Friedman]

By permission from Mario Carneiro, I present a copy of a tail of some
correspondence with me. Here it starts with Mario, followed by my
reply, followed by Mario's reply. It is now my turn to reply, and I
will in a later posting.

Mario Carneiro
March 30, 2016 10:54 PM

I realized it was a lie when I said I reserve judgement on whether
HoTT is a good foundation because I don't understand it well enough.

I am a formalist. Math is a game of symbols, which is imbued with
meaning by our imaginations. Thus, there is meaning in any foundation
that is capable of producing "regular mathematics" such as that
Berkeley course list you posted, and is (presumed to be) consistent.
This is the case for ZFC, NBG, simple type theory, dependent type
theory, HoTT, ITT, OTT, ETCS, not sure about NF, and on and on. In
fact, pretty much any "potential foundation" has already managed to
solve these problems merely as the gateway to entry.

By virtue of this fact, within each of these theories is a part we
understand, and a part we don't, and our job should be to use the part
we understand as leverage to understand the rest. I do not subscribe
to One True Foundation-ism, because this is a matter of history and
opinion, and no progress can be made if there is no objective truth.
Use whatever foundation is convenient for you to write your theorem,
and maybe later come back and see if it maps to other foundations;
nothing else is needed.

Harvey Friedman
March 31, 2016 2:15 AM

Princeton course list.

A fairly well known point of view, but fairly unpopular nowadays.

There are well known problems with this point of view. One is that you
say "not sure about NF".

The reason you say "not sure about NF" probably is that there is no
known interpretation of NF into ZFC or ZFC with large cardinals. And
correct me if I am wrong, but all of the other systems that you accept
there are known to be interpretable in ZFC or ZFC with infinitely many
strongly inaccessibles?

So why give a preferred status to ZFC and ZFC + a little bit, over, say, NF?

Eventually, you come down to trust, and trust comes down to
philosophical coherence and also simplicity. It's tricky to avoid
these considerations.

In fact, we see a dominating position in standard f.o.m here on two counts.

1. When an alternative is proposed, people are generally quite
uncomfortable until there is an interpretation in standard f.o.m.
2. Standard f.o.m. is much simpler than all alternatives being proposed.

Now for me, the choice of general purpose foundation in the sense we
are talking about is mostly a nonissue, although I am interested in
seeing what there is to be gained, and seeing if whatever there is to
be gained, can be done better in standard f.o.m.

The reason it is such a nonissue is that for concrete mathematical
statements, if we have these interpretations, then these concrete
statements are provable in one foundation if and only if they are
provable in the others. I.e., the foundations agree in terms of
provability of concrete statements.

For high level statements, this is less clear, since a high level
statement in one foudnation might not even make any sense in another.

I thought I would take your posting above and copy it to the FOM
together with my reply above, deleting your first paragraph which
contains the word "lie". Do I have your permission to do that?

Mario Carneiro
March 31, 2016  2:54 AM

(Yes, you have my permission to repost any and all of our discussion
on the FOM.)

"The reason you say "not sure about NF" probably is that there is no
known interpretation of NF into ZFC or ZFC with large cardinals. And
correct me if I am wrong, but all of the other systems that you accept
there are known to be interpretable in ZFC or ZFC with infinitely many
strongly inaccessibles?"

Actually the main reason is because I have not been convinced that it
is consistent, although I think that there is some recent work to
build a model of NF using permutation models of ZFA or something
similar. But yes, it amounts to the same thing: I feel uncomfortable
until I see an embedding into a natural extension of ZFC.

So why the asymmetric treatment of ZFC as special here? I see some
kind of Turing-completeness or NP-completeness type property here, in
which all the foundations here are mutually interpretable.
Unfortunately, it's not a perfect correspondence, since some have
higher consistency strengths than others, but I think we can agree
that for "regular" mathematics, these sort of edge effects don't
matter.

Thus, I am justified in taking ZFC as a basis, and showing consistency
of all the others in terms of it, but importantly, I could also take
type theory or HoTT as my foundation, and show consistency of all the
others by embedding everything in HoTT. It makes no difference.

What would you answer if someone asked you to give them "the
foundational NP-complete problem"? Since they are all equivalent in a
precise sense, it makes no difference which you pick, although for
practical reasons you will have to pick one. Faced with this
situation, most people would pick the one that best fits their
application. Being inconsistent in this choice from one problem to the
next is okay, because they are all equivalent.

compiled by
Harvey Friedman