[FOM] formal proofs

[Harvey Friedman]

On Tue, Oct 21, 2014 at 8:27 PM, Timothy Y. Chow <tchow at alum.mit.edu> wrote:
> I don't understand your point here.  It sounds to me like you're insisting
> that someone state precisely the minimum number of grains of sand in a heap.
> Why is that necessary?
>
> It seems to me that the "Blakers-Massey challenge," as spelled out in more
> detail by David Roberts, is a fine challenge.  If it is met, then the
> traditionalists "win."  If not, then presumably the difficulties encountered
> along the way will reveal where the critical problem or problems lie.  I
> don't see why the sticking points need to be spelled out in advance.
>

When I wrote "simplest possible" I just meant in the sense that  "as
simple as the people I am talking to can reasonably make it, with an
honest serious effort, and the simpler the better".  I wasn't posing
any scientific challenge. This misunderstanding is merely a
misunderstanding of informal English.

WIth regard to this "Blakers-Massey challenge", a crucial point I see
is that there is the claim that one cannot even reasonably formalize
the statement at all in "traditional foundations". If that is the
case, then even 10^1000 years is not enough.

I have a side channel who wishes to remain anonymous, who thinks such
a statement about no reasonable traditional formalization is as least
exaggerated. But it does add additional caution to the whole business
of this "challenge". Here are my thoughts.

1. I do not regard any purported mathematical statement meant to be in
finished publishable form, as rigorous unless there is an "obvious"
path back to sugared set theory. This also applies to the proof, not
just the statement.

2. 1 above is the stated standard of a very famous senior fields
medalist, still very active, when he was acting as an Editor (maybe as
principal editor, I think) of the Annals of Mathematics. I got the
impression that this was an actual policy of the Annals of
Mathematics, but I am not sure about the details.

3. Will 1,2 always be the standard? Not until there is an
overwhelmingly clear philosophically and foundationally coherent
mathematically totally transparent and convincing foundational idea
that is really alternative to ZFC. Category theory did not, upon
reflection, be such a thing, and people are generally happy to just
start like MacClane did in his Categories for the Working
Mathematician, with the definition of a category is a set of objects
together with a set of arrows, etcetera. I.e., people are generally
quite content to take set theory as the UMBRELLA. Of course, under
this umbrella, for some math, one may want to very quickly build up a
basic infrastructure for category theory within the set theory
umbrella. Trying to instead take categories as the umbrella, and put
set theory under that umbrella may have some adherents, but is
generally regarded as a bad idea, causing much more unnecessary
trouble that it is worth.  Of course, as  a true foundationalist, I am
entirely open to a truly legitimate attempt to replace the set theory
umbrella with category theory or anything else, but it had better be
really really convincing, philosophically, foundationally, and
incredibly so.

4. I have not seen even a suggestion that there is any kind of
comparably compelling transparent philosophically and foundationally
transparent idea that one should even consider using a as a new
umbrella. For that, the discussion has to be sensationally simple and
of great understandability to the general mathematical community and
beyond. And as in the case of category theory, there can be absolutely
no objection to adhering to set theory (sugared ZFC) as the umbrella,
and for some areas of math, very quickly developing an infrastructure
for this new homotopy theory within the sugared ZFC umbrella.

5. So the key point I am making is that, as far as rigorous
mathematics is concerned, there is a Blakers-Massey theorem (and the
like) only to the extent that mathematicians can readily "see", on a
*semi formal* level, a path back to sugared ZFC.

6. So the only coherent challenge that I see here is this: do a) or b).

a. Give a formally rigorous path from Blakers-Massey to sugared ZFC; or
b. Argue that this is not needed because sugared ZFC is or should be
overthrown as the umbrella for mathematics.

WIth a, there is no issue of Mizar versus anything.
WIth b, it had better be awfully good foundations and philosophy.
Terribly convincing and highly sensitive to a myriad of foundational
and philosophical considerations. That is a very very very tall order.

With b, you simply cannot avoid talking down to IGNORANT IDIOTS like
me. That is the very definition of b.

So prima facie, there is no legitimate challenge being offered here
surrounding Blakers-Massey and the like. UNLESS - and this is a key
point, UNLESS

*) this new homotopy theory is the only way or a good way to prove a
statement that falls under the usual umbrella. E.g., if you tell me
that Blakers-Massey and the like is the preferred vehicle for the
classification of finite simple groups, the proof of the Poincare
Conjecture, the proof of FLT, the proof of Falting's Mordell, the
proof of optimal sphere packing, the proof of the almost Twin Prime
Conjecture, the proof of the four color theorem, the proof of iterated
exponential bounds on Hales-Jewett, the proof the recent theorems on
arithmetic progressions in primes, the proof of the Weil Conjectures,
etcetera, then we have a REAL CHALLENGE. For each of such target
theorems, whose statement is completely non problematic (or mostly
so), how does Mizar compare with these new provers?

Even with *), there is of course the issue of whether we should first
have some sort of rigorous formulation of the basics like
Blakers-Massey and others, back to sugared ZFC, in hand to work with,
BEFORE we start such a challenge.

Harvey Friedman