From lusk Wed Jun 1 21:18:43 1994 Received: from uqcspe.cs.uq.oz.au (uqcspe.cs.uq.oz.au [130.102.192.8]) by antares10.mcs.anl.gov (8.6.4/8.6.4) with SMTP id VAA03576 for ; Wed, 1 Jun 1994 21:17:42 -0500 Received: from everest.cs.uq.oz.au by uqcspe.cs.uq.oz.au id ; Thu, 2 Jun 94 12:17:03 +1000 Received: by everest (5.0/SMI-SVR4) id AA20160; Thu, 2 Jun 1994 12:15:02 --1000 Date: Thu, 2 Jun 1994 12:15:00 +1000 (EST) From: John Staples Subject: Re: Qu-Prolog 3.2 and Ergo 4.0 To: qed@mcs.anl.gov Cc: staples@cs.uq.oz.au Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Content-Length: 1493 (Goodness knows why this thread of discussion got this subject-heading - much as I like it!). I believe Victor is justified in expecting QED to support a number of different mathematical theories. Not only can this accommodate different formalisation preferences, and different mathematical preferences, it also provides modularity. Two reality checks. * A lot of algebra is *not* done within algebraic theories. E.g., to cite Hall's `Theory of Groups' again; after cursory inspection I conjecture there's no single page, all of whose mathematics could be formalised in the standard (first order) theory of groups. Hall's universe of discourse is obviously set theory. * The modularity benefit is obtained only when it is possible to interpret one theory in another. Specifying such interpretations needs a meta-theoretic vocabulary. I sympathise with Victor's desire to just get on with mathematics, and for that reason my own practice in contributing to QED would be to ignore constructive object theories. However we do need to confront the issues involved in getting to where we want to go. Formalisation of mathematics is certainly a major issue; modularity, and preferences for different formalisations and theories are others. Yes, we could all go off tomorrow and use/build systems which have hardwired support for our own preferences. This is the `Tower of Babel' approach, and is what we're trying to escape from, rather than what we seek. John Staples