[FOM] Alternative foundations?
Timothy Y. Chow
tchow at alum.mit.edu
Mon Feb 24 11:36:37 EST 2014
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.
More information about the FOM