Re: Qu-Prolog 3.2 and Ergo 4.0

John Harrison (
Wed, 01 Jun 94 23:38:37 +0100

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.