[FOM] Alternative foundations?

[Timothy Y. Chow]

Harvey Friedman wrote:

> Can't we simply prove outright that all formalisms, including ZFC with 
> abbreviation power, represent large computations awkwardly? If so, 
> awkwardness of representing computations would not be a credible 
> consideration in choice of foundations.

Much of the debate here strikes me as based on a difference of opinion on 
what "foundations" are supposed to do for you.

In "ordinary mathematics," the sort of thing that people tend to mean by a 
"change in foundations" is a switch from varieties to schemes, or from 
ideal class groups to adeles and ideles, or from probability distributions 
to random variables, etc.  The principal driving force in such shifts is 
usually practical: Do the new foundations make it easier to solve new 
problems and push the field forwards?  In each of the above instances 
there was some vocal resistance at first, with the new formalism condemned 
as being needlessly abstract, but the new ideas eventually won out because 
of their success in fostering concrete advances in the subject.  At the 
same time, the old ideas were not completely abandoned; they are still 
invoked if the situation calls for it.

On the other hand, many FOM readers probably think of the purpose of 
"foundations" somewhat differently.  Foundations are supposed to show that 
everything is logically correct, to unify all of mathematics, and to 
clarify exactly what assumptions are needed for which theorems.  The other 
sense of foundations that I described above shares some of these goals, 
but the emphasis is different.  Correctness, unification, and 
clarification are all means towards the end of deeper understanding of the 
subject matter, and not ends in themselves.

For example, consider "awkward computations."  The amount of awkwardness 
that one is willing to tolerate is highly sensitive to the end goal.  If 
I'm a manager at a software engineering firm, the choice between C++ and 
Java (for example) can be a crucial one, with possibly millions of dollars 
at stake.  For a computability theorist whose primary research interest is 
in Turing degrees, the distinction between C++ and Java is irrelevant. 
These are extreme examples, but the point is that a number theorist may 
find ideal class groups "awkward" compared to adeles and ideles, even 
when a specialist in reverse mathematics may see no distinction.

In my view, homotopy type theory and univalent foundations should be 
evaluated primarily on the basis of what I called above "ordinary 
mathematical" criteria.  It is unfortunate that some proponents make 
claims for it that seem to pit the new foundations *against* the old 
foundations.  Voevodsky's famous lecture at the Institute for Advanced 
Study, which has been discussed here on FOM, is an example.  But in my 
opinion, we can throw out that bathwater without throwing out the baby. 
I am sympathetic to John Conway's "Mathematicians' Liberation Movement" 
(which of course has also been discussed before on FOM), which basically 
says that we're mature enough now to be able to pick whatever foundations 
we find convenient, knowing that we can always, in principle, translate 
between any two if them if we really want to.

In other words, if a proponent of a new system claims certain advantages 
over the old system, I do not think the reaction should be to get all 
defensive and say, "But I can do that with the old system too!"  Instead, 
one should open-mindedly explore if the new system helps foster new ideas 
that advance the field.  The sooner we abandon childish turf wars, the 
faster mathematics (and the foundations of mathematics) will advance.

Tim