[FOM] Solution (?) to Mathematical Certainty Problem

[Robbie Lindauer]

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 
> verified?


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?

Best,

Robbie Lindauer