[FOM] Alternative Foundations/philosophical
Timothy Y. Chow
tchow at alum.mit.edu
Fri Feb 28 16:27:40 EST 2014
Joe Shipman wrote:
> The claims of the proponents of Homotopy Type Theory (the currently
> fashionable alternative foundation) are bolder; they seem to be that (1)
> HTT is more natural than ZFC for research in certain areas of
> mathematics (2) HTT is more amenable to mechanical formal verification
> than ZFC (3) ZFC can be represented in HTT.
> In my view, (1) seems plausible and (2) seems doubtful, and I'd like to
> see the details of (3). However, the real question (taking
> bi-interpretability for granted) should be:
> What fraction of mathematical research can be more easily formalized in
> HTT than in ZFC?
> This is what ought to influence which "foundation" is taught to
> mathematics students.
Now we're getting into questions that I think are more interesting.
I think there are two different (albeit related) ways to measure whether
some piece of mathematics can be "easily formalized." The first is how
much time and effort is required to produce the relevant bit of code in a
computerized proof assistant. The second is how much time and effort is
required to convince oneself that the formalization can be carried out in
principle. The two measures are correlated but not identical. I admit
that I have never actually bitten the bullet and learned the details of
any specific proof assistant, but my general impression is that the
assistants that are based on type theory (not homotopy type theory) are
easier to work with than Mizar, the best-known set-theoretical assistant.
Is this impression correct? If we assume this is true for the sake of
argument, then it's still not clear to me that these are the right
foundations to teach to students, unless we envisage them spending a lot
of time with a proof assistant in the future. Conceptual simplicity seems
like it might be a more important criterion than engineering efficiency,
from a pedagogical point of view. Now maybe type theory (or homotopy type
theory) wins on both fronts, but there are still separate questions here.
More information about the FOM