[FOM] Foundational Challenge

[Joe Shipman]

In case you’re wondering why I chose these criteria:

I don’t want to disparage, say, homotopy type theory as a better way of either finding or formalizing results in homotopy theory or other areas of mathematics. I only want to challenge claims that such systems improve on ZFC as a foundation for mathematics in general. If you not only can’t prove anything new, but can’t improve on the standard foundation for proving theorems  in the fundamental core that any proposed general foundation must cover, then however nice your system is I don’t have a reason to prefer it to ZFC as the standard.

Alternative set theories like NF seem like possible candidates for meeting my second criterion but not my first, however I don’t have an example.

Non-set theories like homotopy type theory don’t seem to be able to handle arithmetic without going through the same steps set theory does after first building a set theory, but I’d love to be proven wrong about this.

Ordinary type theory is fine but almost trivial to interpret in ZFC (or even just ZC) so doesn’t satisfy either of my criteria.

— JS

Sent from my iPhone

> On Jan 9, 2020, at 10:45 AM, Joe Shipman <joeshipman at aol.com> wrote:
> 
> When I read about “alternative foundations”, I feel a bit like the physicists who wade through many papers on “Interpretations of Quantum Mechanics” and “Alternative Theories” without ever getting to either an honest new prediction of an experimental result that the standard theories can’t predict, or insights allowing standard predictions to be derived significantly more easily.
> 
> Therefore I issue the following challenge to proponents of any kind of “alternative foundations” to “ZFC plus large cardinals”.
> 
> I CHALLENGE YOU TO IDENTIFY:
> 
> An EXAMPLE of mathematics done in any “alternative foundation” to set theory, where EITHER
> a) it is not obvious that any result derived that is statable in set theory will be provable in ZFC plus a large cardinal of some kind
> OR
> b) it is an ARITHMETICAL result with a significantly shorter formal derivation from first principles than is possible in ZFC (“significantly” means “more than the usual amount of work to translate proofs formalized in Second Order Arithmetic into ZFC proofs”, which is a well-understood quantity).
> 
> — JS
> 
> Sent from my iPhone