[FOM] Solution (?) to Mathematical Certainty Problem

[Harvey Friedman]

Reply to Lindauer 4:54PM 6/24/03.

>
>
>Some mathematical questions are more complicated, but it's thought 
>that the same notion of certainty ought to apply:
>
>"(some very large number of numbers ending in 
>....126785172389469117) are prime" is true in the same sense that "2 
>+ 2 = 4
>	THEREFORE
>There should be some way of achieving certainty about them in the same way.
>
>Unfortunately, the proofs of some such statements are too complex 
>for us mortals to comprehend, in their entirety.

I didn't address the question of whether there are statements of this 
kind that humans will not be able to prove in this exchange.

However, some time ago, I brought up the example

sin(2^2^2^2^2^2^2^2^2^2) > 0

or perhaps with other than 10 2's. I conjectured or suggested that 
this statement cannot be proved true or false in ZFC without using 
such a large number of symbols that it precludes any humanly 
generated proof in ZFC, even with the aid of a computer.

>
>You propose to build a machine that ought to rid us of our feeling 
>of uncertainty by replacing all complicated steps in reasoning with 
>mechanical ones, reproducible "in principle" by anything that could 
>read the record of the proof.
>
>But then there is the nagging question, how do we verify in any 
>particular very complicated proof, that it is accurate?

This is not a problem. Say the proof is exported from my CORE PROOF 
CHECKER as a file in two parts. The first is a purported Hilbert 
style proof in T, and the second, appended, is an extreme annotation.

Now this file (in two parts) may have bugs in it. This will be 
detected by the CORE PROOF CHECKER.

The reason is that the CORE PROOF CHECKER is a multitape Turing 
machine with a transparent program that is humanly verified by 
humanly understandable proof. This verification if NOT, as you say, 
"any particular very complicated proof." It is not complicated at all.

So there is only one proof to be convinced of - that is the one about 
the CORE PROOF CHECKER - that it does what it is supposed to.

Since its domain of application is so narrow - focused on running 
around and matching strings of fairly small length for an electronic 
system, this is not like verifying a big piece of software.

Of course, there are other places where one can raise doubts:

a) the operation of the hardware.
b) that having a Hilbert style proof in T guarantees truth.

But here is the main point: WHATEVER ISSUES REMAIN ARE A HANDFUL OF 
FIXED ISSUES THAT HAVE NOTHING WHATSOEVER TO DO WITH THE VARIED 
NATURE OF THE MATHEMATICAL PROOFS UNDER EXAMINATION.

Thus this process has removed any issues about subject matter, 
regardless of how complex. If the human comes up with a purported 
proof, and knows how to successfully interact with the interactive 
proof creator (a new name for programs like Boyer Moore, Isabelle, 
Mizar, ...), then this process kicks in and is fool proof relative to 
residual issues about which you may wish to raise doubts.

>
>In the example given, we have a proof where there are a googleplex 
>of simple steps necessary to complete it.  And so, us limited 
>computing machines, forget why and therefore whether our previous 
>estimation of the correctness of the initial 100,000 steps of the 
>proof were correct.

I am only talking about a given human declaring that they have proved 
something. I then tell him to go interact with the INTERACTIVE PROOF 
CREATOR and ship the export to the CORE PROOF CHECKER. The export is 
not going to be very large, since the human directed its creation. 
The CORE PROOF CHECKER runs a transparent, and transparently humanly 
verified multitape Turing machine program.

Unless we can agree on these fundamental aspects of the setup, there 
does not seem to be any point in continuing the discussion.

There are very interesting remaining issues if we can get past this point.

Harvey Friedman