[FOM] Solution (?) to Mathematical Certainty Problem

[Harvey Friedman]

Reply to Lindauer 7:34PM 6/23/03.

Here is the kind of solution I have in mind. I would rather consider 
a simpler case. We want to prove that a given bit string has an even 
number of 1's, if it has.

1. As a first pass, use the Turing machine model of computation. 
Later, one can attempt to go even lower than this, getting involved 
in very detailed hardware issues. At some point, if desired, there 
will be Theorems of a very detailed nature concerning hardware 
implementations of Turing machines.

2. Write the obvious Turing machine program in symbols 0,1,B (B for 
blank), with states 0,1, that halts in state 0 if even, state 1 if 
odd.

Reading 0 in state 0. Go to state 0 and move to the right.
Reading 0 in state 1. Go to state 0 and move to the right.
Reading 1 in state 0. Go to state 1 and move to the right.
Reading 1 in state 1. Go to state 0 and move to the right.

We follow the setup for Turing machines that they halt if there is no 
applicable instruction.

There is a very humanly digestible proof that this Turing machine 
algorithm works. And this proof can be formalized in an appropriate 
formalization for mathematics, so that the formal proof is very 
humanly digestible.

By the way, I now think that I have an interesting proposal 
concerning the famed CORE PROOF CHECKER of the UMD (universal 
mathematical database).

The core proof checker might as well be a Turing machine!!!!!

Well, maybe, a multitape Turing machine.

The idea is that I want a simple digestible multitape Turing machine, 
not too many tapes, and not too many quadruples. We want a formally 
verification that is does what it is supposed to do - that is, it 
certifies properly, Hilbert proofs with extreme annotation.

So the only proofs that have to be certain are:

i. The proof that this multitape Turing machine code properly 
certifies whether a file is actually a (Hilbert style proof in T 
appended with correct extreme annotation) - taken as a whole.

ii. The proof that if a file meets the specs used in i, then the 
first half of it is a Hilbert style proof in T.

iii. The proof of soundness. I.e., if a statement has a Hilbert style 
proof in T, in the sense specified for ii, then it is certainly true.

So if these three proofs can be made certain, or certainly correct, 
then we should accept all purported proofs that pass the process.

Of course, we have to be certain that we are using a working Turing 
machine of the appropriate size.

That spills over into hardware engineering issues. But they can also 
be addressed, with some care.

This process is entirely applicable to sophisticated mathematical 
proofs, with the help of the auxiliary IPC (interactive proof 
checker). We don't try to prove anything at all about the IPC, except 
maybe the developers would want to see something to help them put out 
a good piece of software. This is because errors in the IPC cannot 
pass the CORE PROOF CHECKER'S scrutiny.

So there is no problem.

Harvey Friedman