[FOM] Foundational Challenge

[Emilio Jesús Gallego Arias]

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