From lusk Mon Jun 6 00:59:51 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 AAA18611 for ; Mon, 6 Jun 1994 00:58:24 -0500 Received: from everest.cs.uq.oz.au by uqcspe.cs.uq.oz.au id ; Mon, 6 Jun 94 15:57:04 +1000 Received: by everest (5.0/SMI-SVR4) id AA03645; Mon, 6 Jun 1994 15:57:01 --1000 Date: Mon, 6 Jun 1994 15:57:01 +1000 (EST) From: John Staples Sender: John Staples Reply-To: John Staples Subject: Re: Necessity of meta theory -- was Re: Qu-Prolog .. To: yodaiken@nmt.edu, qed@mcs.anl.gov Cc: staples@cs.uq.oz.au In-Reply-To: <199406030417.WAA18853@sphinx.nmt.edu> Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; CHARSET=US-ASCII Content-Length: 2070 On Thu, 2 Jun 1994, Victor Yodaiken wrote: > What about an a-theoretic vocabulary? From algebra and arithmetic > a logical theory is just a set of elements (formulae) and a collection > of operators on the elements. and > My question is whether we need to "formalize" in the sense of logicians > at all. To make the discussion a little more concrete, suppose that > we were to extend Mathematica with a collection of deductive systems > and proof checking operators. You wish to work within pure FO Peano > arithmetic, I want to restrict myself to Yessenin-Volpin's realm > (assuming I could understand it at all) and an engineer wants to > prove theorems about some differential equations and doesn't care > how its done. It should be possible to load the appropriate libraries > and use deductive operators and syntax checkers for each of these > three choices. Is there a reason why there should be a formal meta-theory > behaind each of these systems? Is there an advantage if we require > that all three types of systems be translatable into some ur-logic? I agree that a naive user should be able to get on with deductive reasoning in a particular theory, without being aware of any metatheory. Explicit use of metatheory is important for power users (e.g. appreciating whether results available in another theory or logic could be applied, and then prescribing how) and for system implementors (for whom it is a large part of their conceptual framework). The three users you mention are almost certainly not interested in exchanging the results of their labours, so that the other two can reuse them. I believe exchange and reuse are major goals of QED however. If we all agreed on one object theory - and stuck to it forever - then we could have exchange and reuse without explicit metatheory. Even then, explicit metatheory could improve the quality of the common object theory, e.g. by providing a way of specifying and justifying derived rules of inference so as to increase the productivity of proof-checking; but that's another story. John