[FOM] Urquhart on Friedman on Urquhart on Corfield

David Corfield david.corfield at philosophy.oxford.ac.uk
Sat Oct 18 06:39:20 EDT 2003

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

More information about the FOM mailing list