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