From lusk Wed Jun 1 17:40:22 1994 Received: from swan.cl.cam.ac.uk (pp@swan.cl.cam.ac.uk [128.232.0.56]) by antares10.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id RAA00955 for ; Wed, 1 Jun 1994 17:38:58 -0500 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 1 Jun 1994 23:38:44 +0100 To: qed@mcs.anl.gov Subject: Re: Qu-Prolog 3.2 and Ergo 4.0 In-reply-to: Your message of "Wed, 01 Jun 94 04:30:54 MDT." <199406011030.EAA07799@sphinx.nmt.edu> Date: Wed, 01 Jun 94 23:38:37 +0100 From: John Harrison Message-ID: <"swan.cl.cam.:274710:940601223852"@cl.cam.ac.uk> Victor Yodaiken writes: | Proposition: The purpose of the QED project is to mechanize the algebra | of proofs in working mathematics. For this purpose, the language | of ordinary mathematics suffices and there is no need to adopt | any meta-mathematical framework. I might agree if by "purpose" you mean "ultimate goal". In much the same way the purpose of AI is to produce machines that can hold an everyday conversation with a human being, but experience shows that it's wise for AI to lower its sights. In the same way, computerizing even a more stylized subset of natural language, viz. the "mathematical vernacular", may be well-nigh impossible in the foreseeable future. This is not to say that a metamathematical framework is necessarily called for. However at the workshop there seemed to be a clear majority (everyone except me, in fact!) in favour of such a scheme. Certainly it offers many interesting challenges, although I can understand that it might try the patience of those mathematicians uninterested in logic. John.