[FOM] Solution (?) to Mathematical Certainty Problem

[Harvey Friedman]

This is a followup to my posting 2:32AM 6/20/03.

Here is a proposal for attaining mathematical certainty with computer 
assistance.

1. THE BEGINNING - THE MASTER FORMAL SYSTEM T.

I start like everyone else in specifying the formal system in which 
proofs are required to exist.

Normally, T will be taken to be some practical version of ZFC, with 
flexible abbreviation power, and also like what I discussed in 7:03PM 
6/20/03.

We will assume that this master formal system is specified human to 
human, of course in a very careful and meticulous way.

As we shall see from my proposal, it is entirely appropriate to 
assume that this system T is a Hilbert style proof system, which is 
much easier to deal with from the human level in terms of specifying 
what proofs are. Of course, Hilbert style systems are a nightmare in 
terms of humans actually reading or casting proofs directly in them. 
But as we shall see in my proposal, humans are not going to be 
reading or casting proofs in T.

So the first step is for T to be cast in simple and clear enough 
terms, so that humans are all convinced that if there happens to be a 
proof in T of a sentence A, then this confers the desired certainty 
on (the intended interpretation of) A.

Of course, it is vital that the language of T be sufficiently 
powerful that a mathematician can identify sentences in the language 
of T that correspond exactly to the Theorems being verified. This is 
not a problem if we start with a really good version of ZFC. This 
does require a discussion of work I have been involved with, but have 
not discussed the details of, on the FOM. Work concerning appropriate 
forms of ZFC for the development of mathematics, on the language, not 
the proof, side.

One aspect of my posting 11:49PM 6/17/03 "Theory of Actual Proofs" is 
vitally important here. Statements to be verified generally have a 
line of definitions that need to be made in advance of the statement. 
And these definitions must be in proper linkage with all of the 
previous definitions made. So as we use the system T, we create a 
definitional chain, as well as a statement chain. For some purposes, 
there is no point in distinguishing between definitions and theorems, 
as they are all to be verified statements (the definitions, in proper 
form, need no verification).

The part of T other than proofs, is required to be extremely humanly 
friendly, since it is going to be part of the official record, to be 
read by mathematicians. This requires serious care, and needs to be 
discussed further, as I said above.

However, this issue is reasonably under control. I.e., this part 
without proofs. We do not require any kind of perfection in this 
respect. I know of reasonable proposals, which do require a little 
flexibility on the part of users, but are an improvement over 
anything that I have seen.

2. EXTREMELY ANNOTATED PROOFS IN T.

The overall design of this proposed system is as follows.

i. Humans interact with various existing systems like Mizar and 
Isabelle and others, New ones will be developed once our system is 
put into place. I don't care what they look like, but the purpose of 
these auxiliary systems is to use whatever tools, to

create files purporting to be formal proofs in T appended with what I 
call an "extreme annotation".

Because of this "extreme annotation", I don't care what kind of buggy 
garbage may sometimes be produced by such human/machine interactive 
systems. I don't care if they happen to be buggy, but of course that 
may, in a practical sense, waste a lot of time of their users trying 
to comply with our perfect standards.

ii. These purported formal proofs in T must start with a statement of 
what is being proved, preceded by an appropriate definitional lead 
in. This is in full accordance with the dynamic nature of the setup 
of T. Of course, the definitional lead in may be empty. (See the last 
paragraph of section 1 above).

iii. The purported proof in T, appended with the so called extreme 
annotation, is sent to the core proof checker for examination.

iv. In practice, it should not be difficult for systems like Mizar 
and Isabelle to conform to these requirements, and also to create an 
export program that supplies the required extreme annotation. Again, 
for our purposes, no verification of this is relevant for us. And if 
Mizar and Isabelle won't do it, then we can wear different hats and 
go into that human/machine interactive business ourselves.

v. If the core proof checker says "yes, this is a correct proof in 
T", then the statement that has been proved, including the 
definitional lead in to it, is posted to the world with a time stamp. 
The definitional leadin used, as well as the statement verified, 
becomes part of the official record of the system. The proof stuff, 
including the extreme annotations, are put away in a separate secure 
place, of course. This official record is meant to be read worldwide 
by mathematicians, as it is particularly friendly.

vi) All subsequently accepted purported proofs in T with extreme 
annotation, must conform and also have available to it, what has been 
done in the official record from these public postings.

We now come to the novel(?) idea here.

The idea is that so much information in the form of pointers, 
etcetera, into the proof in T is given after the end of the proof in 
T, that this alleviates the need for parsers, string searchers, and 
the like in the core proof checker. (We have not yet come to the core 
proof checker).

Also, this is to be, together with T, a universally agreed upon 
standard, adhered to throughout the world.

We also claim that

i) the specification of the formal system T (much simpler than a 
computer system or computer language!!) is humanly digestible;

ii) the specification of the extreme annotation is humanly digestible.

iii) the proof that every file with an extreme annotation is a proof 
in T over the existing posted record of the system, is humanly 
digestible.

iv) extreme annotations are not too long for practical use.

I will take a stab at how this is could be designed, in the next 
posting. That should (might) convince you of i) - iii).

Items i) - iii) are to indicate our feeling that we don't need to use 
formal verification methods in connection with i) - iii). However, we 
are entirely open to the idea that some sort of formal verification 
would be desirable in connection with 1) - iii).

3. THE CORE PROOF CHECKER.

Extreme annotation will be so explicit that the core proof checker 
has only to do completely trivial grunt work of the most elemental 
kind.

We think that one should be able to easily program the core proof 
checker in an appropriate MACHINE LANGUAGE, and have a mathematician 
write a completely readable correctness proof of the machine language 
program that is completely convincing to any mathematician. Special 
purpose hardware would circumvent a number of verification issues.

It may be valuable to do this in an agonizing machine language like 
Turing machines. In fact, that may be a real good test. To show that 
we are at a suitably low level but understandable level, we could see 
if the TM code could easily be written and understandably proved to 
be correct.

The extent to which any formal verification methods would help here 
is quite unclear, as we are at the primitive lookup level.

Harvey Friedman