[FOM] Solution (?) to Mathematical Certainty Problem
Harvey Friedman
friedman at math.ohio-state.edu
Tue Jun 24 02:32:59 EDT 2003
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
More information about the FOM
mailing list