[FOM] Ultimate Rigor?
hmflogic at gmail.com
Wed Oct 22 10:58:33 EDT 2014
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?
More information about the FOM