[FOM] Foundational Challenge

[Joe Shipman]

It’s an advantage of some constant factor, probably. A sufficiently well-developed ZFC proof verifier will be a program which will include libraries that translate specifications of algorithms into executions of those algorithms, which will have some kernel that is a provably correct virtual machine. As of 2020, it may be the case that Coq does this much better than any set-theory based system; I’d like to hear from some experts on how big the savings factor there is.

More interesting would be a nonlinear improvement. Perhaps a powerful axiom like Voevodsky’s Univalence Axiom might provide that in the context of homotopy calculations?

— JS

Sent from my iPhone

> On Jan 15, 2020, at 12:30 PM, Emilio Jesús Gallego Arias <e+fom at x80.org> wrote:
> 
> Joe Shipman <joeshipman at aol.com> writes:
> 
>> 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).
> 
> Precisely, the Coq proof doesn't need step 3, as the algorithms are
> written (and verified) in Coq itself. The only witness you need is the
> output, not the trace.
> 
>> 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.
> 
> My point indeed is "ZFC" cannot _run_ computation, other foundational
> systems can; isn't this a fundamental advantage in some cases ?
> 
> Kind regards,
> Emilio J. Gallego Arias