[FOM] Alternative Foundations/philosophical

[Timothy Y. Chow]

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.

Tim