[FOM] Ultimate Rigor?

[Freek Wiedijk]

Dear Harvey,

>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.

But isn't ZFC (and even PA) in danger of being inconsistent.
For instance isn't impredicativism a reason for worry?
I'm not a philosopher, but I do know that professor De
Bruijn (who created the whole field of formal proof) told
me that he wouldn't be surprised at all if a fundamental
inconsistency in PA were discovered.

>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.

You just described the LCF architecture.  And there the
"pure proofs" are checked _all the time._  Only there is
no export, every proof is always routed through a kernel
(or "logical core") that is part of the system.  And these
kernels can be tiny.  In the case of HOL Light (the system
in which I demoed a formal version of that example about
monotonically increasing sequences going to infinity)
that code fits on a T-shirt.

>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.

So this all exists, only not for ZFC.  It does exist very
much for the HOL logic.

>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?

Well, you need to understand the rules of the logic, so
for people who don't know math/logic it still won't be
transparent, I guess?

And when you think of a logic with variables, and you
use named variables, the substitution code will not be
very transparent.  So if you want as much transparency
as possible, you better use De Bruijn indices for your
variable names!  (Coq: yes; HOL Light: no, but then it
has been formally proved correct that that substitution
code is okay; HOL4: you can choose between two kernels,
one with names and one with De Bruijn indices; Isabelle:
I don't know.)

Freek