Re: Some Simple Questions

From: David Bernier (david250_at_videotron.ca)
Date: 03/22/05 

Date: Tue, 22 Mar 2005 03:01:00 -0500

Charlie-Boo wrote:
> Alan Smaill wrote:
>
>>G. Frege <no_spam@gmx.de> writes:
>>
>>>On Mon, 21 Mar 2005 19:36:02 GMT, "W. Dale Hall"
>
> <mailtodhall@farir.com>
>
>>>wrote:
>
>
>>>>Were you going somewhere with all this?
>>>>
>>>
>>>Sure, he's raving against the paper "A Mechanical Proof of the
>>>Unsolvability of the Halting Problem" (1982) by Boyer and Moore.
>>>
>>>Source:
>>>http://www.cs.utexas.edu/users/boyer/ftp/ics-reports/cmp28.pdf
>>>
>>>
>>>*sigh*
>>
>>*sigh* indeed.
>>
>>far from being the first presentation of the theorem prover in
>
> question,
>
>>we can notice in the references to this paper a citation to the 1979
>>book, which has plentiful details on the proving system.
>>
>>If Charlie Boo is so exercised about this particular proof,
>>he might have found his way to
>>
>> www.cs.utexas.edu/users/boyer/ftp/nqthm/
>
>
> This is just one paper that my analysis debunks. Since you seem to be
> presenting yourself as someone who knows and/or believes in this
> particular paper, then please tell me:
>
> 1. What is the logical convincing argument that HP is unsolvable that
> is formalized in that paper?
>
> 2. What is its (1) formal representation?
>
> 3. How was that formal representation (2) created?
>
> 4. What is the general means of mapping such a formal representation
> into a logical convincing argument?
>
> 5. How is that general means (4) applied to this formal representation
> (2) to produce the logical convincing argument (1)?
>
> What is a proof? It's a convincing argument, right? So what is the
> convincing argument in that paper that HP is unsolvable?
>
> The entire paper does not contain any output from their purported
> system. Why not?
[...]

If a proof is generated with the aid of a computer, it can
be most impractical to include detailed output from
the computer's computations.

For example, around 1962, there was a paper in "Mathematics
of Computation" containing 100,000 digits of Pi.
(by D. Shanks, J. W. Wrench, I think).

The authors claimed to have a proof that
Pi = 3.14159.....5493624646 etc.

The review is available from here:
http://www.emis.de/cgi-bin/Zarchive?an=0104.36002
in German...

David Bernier

Relevant Pages

  • Re: Some Simple Questions
    ... Charlie-Boo wrote: ... What is the general means of mapping such a formal representation ... > into a logical convincing argument? ... be most impractical to include detailed output from ...
    (sci.logic)
  • Re: Some Simple Questions
    ... Alan Smaill wrote: ... which has plentiful details on the proving system. ... What is the logical convincing argument that HP is unsolvable that ... How was that formal representation created? ...
    (sci.math)
  • Re: Some Simple Questions
    ... Alan Smaill wrote: ... which has plentiful details on the proving system. ... What is the logical convincing argument that HP is unsolvable that ... How was that formal representation created? ...
    (sci.logic)
  • Re: Some Simple Questions
    ... > the unsolvability of the halting problem. ... How in particular was that formal representation created? ... into a logical convincing argument? ... haven't even checked out the tires yet." ...
    (sci.math)