[FOM] Concerning f.o.m./f.o.X

[Harvey Friedman]

On Fri, Aug 31, 2018 at 1:18 AM Timothy Y. Chow
<tchow at math.princeton.edu> wrote:
>
> On the topic of f.o.m. versus f.o.X., I have observed a number of cases
> that fit the following general pattern.
>
> 1. Some prominent figure vocally criticizes standard foundations as being
> inadequate, and proposes new foundations.
>
> 2. Experts in foundations push back, pointing out that the criticisms are
> overstated.  As a result, they are largely unreceptive of the possibility
> that the new foundations offer any advantages.
>
> As far as the advancement of science is concerned, I think that both
> attitudes leave something to be desired.  It is often true that the old
> foundations are capable of sustaining the proposed new ideas, at least
> initially.  At the same time, it could be that the new ideas do provide
> some kind of enormous practical advantage, such as making it
> psychologically easier to prove new results, or providing a kind of
> conceptual clarify for practitioners of X that was previously lacking.
> The critic may, in his or her own mind, link the misguided criticisms with
> the new ideas, but one should not assume that this link is a necessary
> one.  The new proposal may have significant merit in its own right,
> particularly from the viewpoint of f.o.X., whether or not the criticisms
> of the old approach are on target.

Although I generally agree with what you are saying above, it would be
preferable for an in depth discussion to mention some specific
examples for readers to focus on. There are enough important
differences in these sort of cases that such a general discussion has
its limitations.
>
> Voevodsky's objections about the consistency of PA are a case in point.
> They were not new, or even very coherently articulated.  The same might be
> said, though perhaps to a lesser degree, of many of his other criticisms
> of conventional foundations.  On the other hand, I believe that there is
> plenty of evidence that his ideas have been highly valuable, certainly
> from the point of view of f.o.X. where X = homotopy theory, and possibly
> even from the point of view of f.o.m.

I do not recognize a single example today of anybody's objections to
standard f.o.m. as compelling or even coherent. However, in many
cases, the pseudo objections can be rephrased or reinterpreted as a
quest for f.o.m. advances that shed light on aspects of mathematical
thinking that go beyond any light already shed on them by the present
standard f.o.m. Thus I like to replace pseudo objections with positive
programs.

In the case of Voevodsky, the "objections" are not coherent, but many
specialists in homotopy theory (and possibly more) think that it sheds
light on some aspects of mathematical thinking. I find this plausible,
although what I do not see is any general interest formulation of just
what these aspects of mathematical thinking are. These aspects may or
may not be highly specialized and not of any general interest - that
is not clear to me. V partly emphasized - even to me personally - that
standard f.o.m. is fatally flawed for the purpose of verifying
mathematics, and the "solution" is an f.o.m. overhaul along the lines
he was advocating. I found this totally unconvincing, and it appears
that almost all of the top verifiers are doing just fine with more or
less standard f.o.m., with some (Harrison most vocally) moving even
closer to standard f.o.m.

I expect that a fully coherent presentation of what these V
"objections" are can lead to positive programs, which are best
developed through standard f.o.m.

Standard f.o.m. is now a very highly developed and flexible tool for
shedding light of various kinds on lots of aspects of mathematical
thinking. When any clear aspect of mathematical thinking is clearly
identified, the expectation is that standard f.o.m. can be used or
refined in order to shed light in the new context, and that will
generally be far preferable to other approaches. However, extending,
restating, or modifying standard f.o.m. for such purposes is something
that, generally, only experts in standard f.o.m. can do, as there is a
wealth of techniques, approaches, cross connections, that can be
combined in myriad ways, and this can only be adequately controlled by
experts in standard f.o.m.
>
> I don't know enough about Connes's work to say for sure, but superficially
> it looks like it might be another example where his criticisms of
> nonstandard analysis are overstated, yet his new ideas have significant
> f.o.X. merit.
>
Perhaps a nice example of what we are talking about. Connes's
objections concerning nonstandard analysis can easily be turned into
the positive program of extracting constructive or even computational
content from arguments involving nonstandard analysis. Standard f.o.m.
comes in immediately in the form of conservation results. See
https://cs.nyu.edu/pipermail/fom/2018-August/021193.html

Harvey Friedman