[FOM] Foundational Challenge

[Joe Shipman]

Finney wrote (abridged):

> That is not the purpose of alternative foundations. Generally, alternative
> foundations seek to either
> 
> 1. Restrict certain modes of reasoning for one reason or another. This may and
> usually does eliminate some classical results. ...
> 
> 2. Provide a better foundation for mathematics. This may or may not increase
> the theorems reachable by a mathematician, or may change them in some way....
> 
> 3. Provide a completely different foundation of mathematics. Perhaps there is
> some alternative foundation that would be better than ZFC. It could even
> subsume ZFC. But that doesn't necessarily mean new or different theorems in
> most classical areas.
> 
> 4. Simply to study the structure of some part or all of mathematics. I am not
> up on this, but I believe that is the point of Reverse Mathematics.
> 
> 5. Apply a different type of constraint to the underlying logic....
> 6. Then there are alternative foundations such as Quantum Logic that may not
> be directly usable for conventional mathematics at all....
> 
> ....perhaps there is a better foundation than ZFC. Perhaps
> more of Cantor's lost paradise can be regained.
> 
> Large cardinals may not, and usually don't, play a direct role in alternative
> foundations. Alternative foundations is a very rich and interesting area of
> research. We still don't have a foundation that restores all of Cantor's
> paradise. We have just cleaned up part of the garden.


None of this comes close to giving a positive answer to my challenge, and I’m not interested in changing the subject, because my challenge is intended to address the PRACTICAL question “would an ordinary mathematician whose primary interest is in finding and proving theorems become any more effective at doing so by using an alternative foundation than ZFC (plus large cardinals if necessary)?”

If no positive answer to my challenge is forthcoming, I conclude that the only mathematicians who might need to care about alternative foundations are those working in areas of math that relate directly to the alternative foundation.

This isn’t so easy, though. For example, homotopy theorists obviously benefit from homotopy type theory, but If they care about calculating actual homotopy groups of n-manifolds or other important concrete spaces, then my challenge better have a positive answer, because those groups are arithmetically definable! 

So here’s a good way of putting the issue even more concretely. Does the development of mathematics in homotopy type theory lead to algorithms to calculate the homotopy groups of n-manifolds that are either easier to find, easier to prove correct, or run faster, than the algorithms found by homotopy theorists who were not using the HTT formalism?

This sounds like your best chance: if HTT can’t do homotopy calculations distinctly better than ZFC can, I wouldn’t expect math formalized in HTT to beat math formalized in ZFC In any other respect.

— JS