[FOM] New Umbrella?/big picture

[Harvey Friedman]

There are people claiming that at least from the point of view of
creating formal proofs, the usual set theoretic foundation can,
should, or must be replaced.

There are degrees of forcefulness of this view. They range, roughly, from 1-4:

1. In certain specialized areas of modern pure mathematics, using a
different foundational setup does make it considerably easier to write
rigorous proofs, document rigorous proofs, and above all, create
formally verified proofs. New foundational setups are superior to the
usual set theoretic foundational setup, in that they make it easier to
do so.

2. In certain specialized areas of modern pure mathematics, using a
different foundational setup does make it even possible to write
rigorous proofs, document rigorous proofs, and above all, create
formally verified proofs. New foundational setups are superior to the
usual set theoretic foundational setup in that they make these
possible in a practical sense, whereas the usual set theoretic
foundational setups cannot be used, practically.

3. Throughout the whole of modern pure mathematics, using a different
foundational setup does make it considerably easier to write rigorous
proofs, document rigorous proofs, and above all, create formally
verified proofs. New foundational setups are superior to the usual set
theoretic foundational setup, in that they make it easier to do so.

4. Throughout the whole of modern pure mathematics, using a different
foundational setup does make it even possible to write rigorous
proofs, document rigorous proofs, and above all, create formally
verified proofs. New foundational setups are superior to the usual set
theoretic foundational setup in that they make these possible in a
practical sense, whereas the usual set theoretic foundational setups
cannot be used, practically.

There is one quite friendly modification of the usual set theoretic
orthodoxy of ZFC and its principal fragments, and that is Flat
Foundations:

http://www.cs.nyu.edu/pipermail/fom/2014-October/018337.html
http://www.cs.nyu.edu/pipermail/fom/2014-October/018340.html
http://www.cs.nyu.edu/pipermail/fom/2014-October/018344.html

With regard to the last of these links, I think Leibniz is credited
for the general principle

x = y if and only if for all unary predicates P, P(x) iff P(y)

whereby giving a way of defining equality in practically any context
(supporting general predication).

Flat Foundations obviously goes to some limited distance to address
some "issues" or "needs" raised by foundational category theorists.

I have consistently asked for feedback from categorical
foundationalists, including those involved in HoTT, for feedback. I
have a very limited amount of feedback, and I suspect that
foundational category theorists may not understand Flat Foundations
any more than I understand foundational category theory.

Paul Levy, obviously an interested party here on the FOM, has given
some insights into the foundational category theory approach. Above
and beyond all, as I suspected, all traces of equality are to be
expunged. All functions from structures to structures must respect
isomorphism. Both of these needs can be, I believe, fully accommodated
by further intelligible modifications of Flat Foundations. No doubt,
there may be other challenges to meet.

In fact, I think that the disjointification ideas in
http://www.cs.nyu.edu/pipermail/fom/2014-October/018340.html are on
the right track. I need to formulate an axiom to the effect that all
functions from objects to objects interact nicely with local
isomorphisms. I once wrote a paper many years ago that now seems
relevant(!):

On the Naturalness of Definable Operations, Houston J. Math., Vol. 5,
No. 3, (1979), pp. 325-330.

But before plunging further into this enterprise, I need more
confidence that this is really worth doing.

There is a reasonable notion of

*bottom line mathematics*

whereby there are no real issues of formulation of the statement of
the theorem. The most extreme case I can think of, that is universally
highly regarded, is FLT = Fermat's Last Theorem.

We are not even close to any formal verification of FLT, as far as I know.

How convincing is the claim surely out there that formal verification
of FLT is going to be seriously impacted by the issues at hand? Or of
Poincare Conjecture? Or of recent breakthroughs on the Twin Prime
Conjecture? Or, for that matter, of the relatively consistency with
MKGC of "all definable sets of real numbers are Lebesgue measurable"?

Harvey Friedman