[FOM] Urquhart on Friedman on Urquhart on Corfield

[David Corfield]

Hmmm, this style of forming the post subject is heading for disaster.

Urquhart wrote:

> Well, actually, I have quite a few criticisms.  The discussion
> of computer proofs is rather weak, because it makes the mistake
> of thinking that the "Robbins problem" was an important 
> problem in logic.  That's just an example.

I thought I had made it clear on page 50 that I don't think the Robbins
problem is important. Trouble is automated theorem provers don't
have too many other successes to report, discounting projects like Mizar to
prove what we already know.

I found the case illuminating in that even in the unpromising, albeit very
short, syntactical trace of the EQP prover, a real mathematician such as 
Louis Kauffman desperately searches for meaning. It throws into stark 
contrast the drive for certainty and the drive for explanation.

David Corfield