[FOM] Solution (?) to Mathematical Certainty Problem
robblin at thetip.org
Mon Jun 23 22:34:13 EDT 2003
On Sunday, June 22, 2003, at 11:20 AM, Harvey Friedman wrote:
>> The point is simple, what improvement over the ordinary "looks like a
>> proof to me" is your method?
> There seems to be no problem. See the postings of Jones 7:31AM
> 6/21/03, Jones 5:36PM 6/21/03, Wiedjk, 8:17PM 6/21/03, Vestergaard
> 11:07AM 6/22/04.
> Intuition plays no role in this. Perhaps you doubt if any
> hardware/software system, no matter how low level, can be truly
The machine spits out the step-by-step proof that it is a palindrome or
prime or divisible by 17 or whatever, which proof is a billion^billion
steps long. You check it, but have lost the certainty that the first
100,000,000 steps were correct by the time you get to the last
100,000,000. Imagine, for instance, that step 100,000,001 refers to
the prime-numbered steps between (100,000 and 100,000,000) for its
proof (there are LOTS, I know not how many). You might be able to
look at the volumes of proof that it produces and spot-check it, but
you would never be able to check the whole thing yourself.
You build another machine to verify the proof.
Machine II says the proof is sound.
Have you verified the proof or verified that machine II says that the
proof is sound? How can I verify the proof without understanding it
and how can I understand it if it's too long to fit in my primitive
9-item stack-oriented brain? If I understand "how in principle the
matter would be solved" because I programmed the computer, I still
don't know that that's the way the computer actually did it. And to
verify that Machine II worked "In very large cases" I'd still have to
check in the very large case.
Maybe there was a power-surge during the computation. Maybe there's a
micro-flaw that only becomes relevant for numbers with more than
100,000,000 digits. I couldn't test it because in the end, I'd still
have to trust myself to reidentify two very long numbers, which I know
I can't do.
> For example, I want to build a system that can tell whether or not a
> given input string of length 1 billion is a palindrome. I.e., is the
> same as its reverse. And I want to verify that system. Custom built
> hardware. You doubt if this can be done?
I doubt that it would make it CERTAIN that the string was a palindrome.
We would accept it because we respect your ability to make good
computers, not because it's a logical consequence of any argument that
it must be correct. We would have confidence, but not certainty.
> I wouldn't trust unaided humans to tell me whether or not a given
> input string of length 1 billion is a palindrome.
Agreed, or even to re-identify string more than 100,000 items long.
> The idea is to reduce proof checking to things like this.
Which it is agreed could be done for relatively small parts of
mathematics, say integer mathematics with arguments less than 100
digits long. But I've seen people who can do math like that in their
heads without the aid of any computer. Beyond that, I'm pretty sure
most people are lost. Super geniuses make it to 1000 digits.
The question is can you actually be certain in a way that's better than
"seems right to me" or "Andy Clark is a really good system designer".
As far as I can tell, that would have to amount to a proof that you
couldn't be wrong if you did so-and-so. But for an infinite number of
proofs, you wouldn't be able to tell if you'd done so-and-so (or that
the computer had done so-and-so).
Granted, there is an end to doubt - We shouldn't wonder whether or not
we were born or whether we have been living this way forever. But with
information, the bounds of doubt are immediate - how do we re-identify
numbers with more than 100,000 digits in practice?
More information about the FOM