[FOM] Foundational Challenge

[Mario Carneiro]

On Wed, Jan 15, 2020 at 7:21 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 ?
>

CIC is an axiomatic system that contains, among its axioms, some rules
about definitional equality, that we often call a "computational
interpretation". It so happens that these axioms can be chained together in
a very straightforward and deterministic way, such that a "type checker"
can quickly put together these proofs (implicitly, by going through certain
machine states).

When put in these terms, it should be clear that ZFC is in a similar
position. If you work only from the axioms you probably won't get far, but
assuming that the formal system has the capability to construct and reuse
theorems, you can play a similar trick: use the states of a computer
program to quickly construct proofs of a certain form. The difference is
that ZFC does not specify what this form should be; this depends on the
implementation.

As a simple example, we can do some natural number arithmetic like so:

(1) 0 in nat
(2) n in nat -> S(n) in nat
(3) a in nat -> a + 0 = a
(4) a, b in nat -> a + S(b) = S(a + b)

These are all theorems of ZFC, where 0, S, and nat are ZFC sets. Now we can
prove

S(S(0)) + S(S(0)) = S(S(S(S(0))))

through an entirely algorithmic process that applies axioms (3) and (4)
using transitivity. We can either construct this as a concrete proof object
and observe that it is a valid ZFC proof, or we can write a program that
adds numbers in unary by pattern matching the second argument, and argue
that each step corresponds to an application of (3) or (4), and hence each
state the machine steps through implicitly represents a proof in ZFC. (In
this and most other cases we can also prove correctness once and for all
for the program, but this is a slightly different thing, and the CIC
analogue is closer to the sense in which each intermediate state
corresponds to a proof.)

So to my mind there is nothing particularly special about CIC's
"computational interpretation", and no need whatsoever to bake this into
the logic. If anything, it is limiting, because it means you can only
compute things in one way, whereas ZFC makes no particular commitment to
one kind of computation; the abstract logic says nothing about what is
computable but computation models can be overlaid without difficulty.

This is essentially the way that Isabelle's code generation works; although
simple type theory can be argued to have a "computational interpretation"
as well, it is not baked into the logic in the same way (there is no
convertibility judgment), and Isabelle constructs proof terms when you
execute functions in the logic.

Mario Carneiro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20200116/93d102b3/attachment-0001.html>