[FOM] Foundational Challenge

[Joe Shipman]

In the case of the 4-color theorem it is the same as with other computer proofs. There are 3 parts:

1) an ordinary humanly verifiable proof that an algorithm is correct, translated into formalized ZFC or whatever other system in the usual way,
2) the input to the algorithm (in this case, an unavoidable set of reducible configurations, generated by earlier iterative man-machine interaction), and
3) the trace of the algorithm (proof it halts successfully obtained by actually running the computation and translating its state into the formal system’s representation; in this case, the reduction-finding subroutine for each reducible configuration can itself emit a smaller more easily verified piece representing the particular reductions found).

The paper you reference builds a lot of its own infrastructure for the special purpose of this proof. But there is no particular disadvantage in using a ZFC-based system to prove a statement of the form “algorithm X on input Y halts with output Z” compared with other formal systems, once the once-and-for-all work to represent algorithms conveniently has been done.

This might be different, I suspect, from the situation with HTT and calculating homotopy groups. The question is whether the special axioms of HTT such as Voevodsky’s Univalence Axiom lead either to an algorithm which is superior in performance to algorithms coming from the standard Set Theory based developments, or lead significantly more easily to equivalent algorithms. By “significantly more easily” I mean “proving the algorithm is correct in HTT is easier than in Set Theory even if you don’t count the cost of the infrastructure set theory needs to *state* propositions in homotopy theory”, because that cost is a once-and-for-all expense, already accomplished. 

— JS

Sent from my iPhone

> On Jan 15, 2020, at 10:06 AM, Emilio Jesús Gallego Arias <e at x80.org> wrote:
> 
> Dear all,
> 
> Joe Shipman <joeshipman at aol.com> writes:
> 
>> 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.
> 
> The first that came to my mind when reading the challenge was "how would
> a formal/complete proof of the 4-color theorem would look in ZFC" ?
> 
> Do you think Gonthier's proof [1], as done in the CIC type theory does
> qualify to improve the ZFC version?
> 
> I'm unsure I know how to answer that question, and whether type theories
> would be considered to be related directly to the area of mathematics
> doing proofs with large computational content.
> 
> Kind regards,
> Emilio J. Gallego Arias
> 
> [1] https://www.ams.org/notices/200811/tx081101382p.pdf