[FOM] Ultimate Rigor?

[Harvey Friedman]

On Tue, Oct 21, 2014 at 4:16 PM, Freek Wiedijk <freek at cs.ru.nl> wrote:
...
> With such a verified LCF-style system, I'd much rather
> doubt the consistency of the logical foundations of the
> system than the quality of the implementation.  If there
> turned out to be a problem, I would wager it would mean we
> turned out to have an absolutely rigorous implementation
> of an inconsistent foundations.  But if the foundations was
> consistent we would have as much "absolute rigor" as would
> be philosphically possible.

That's why I keep mentioning pure unsugared ZFC. The setup I am
thinking of is this. We want to verify that a given file is literally
a pure unsugared proof in ZFC.

In this setup, we don't care about whether the proof assistant is
buggy. To succeed, it just has to export pure ZFC proofs - and maybe
not all the time.

So in this setup, the issue is: just how certain can I be that the
tester of whether or not a file is a pure ZFC proof is correct.

I was thinking of two ways to go here.

1. Deal with purported pure ZFC proofs as indicated.
2. Require not just a pure ZFC proof, but also a pure ZFC proof with
added information - obvious pointers. So a little bit more burden
placed on the proof assistants. But really not much, since the proof
assistant, in order to communicate with a person, must already have in
convenient form such extra information.

Of course, we need to prove that this added information is designed
correctly. That seems to be a proof of a very special kind of
assertion whose proof has a very simple structure - basically one
induction where the basis and induction are trivial.

Also, there can be a very special purpose very low level code for
this, where the proof that it is correct also has a trivial structure.

What is not clear to me is just how one explains or quantifies just
how rigorous this is. It is extremely transparent, but how do I say
that it is ultimately transparent, that it cannot be made more
transparent? Or if it can, are we talking about a series of more and
more transparent processes?

Harvey