From lusk Thu Jun 2 23:19:43 1994 Received: from sphinx.nmt.edu (sphinx.nmt.edu [129.138.6.92]) by antares10.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id XAA12312 for ; Thu, 2 Jun 1994 23:17:48 -0500 Received: (from yodaiken@localhost) by sphinx.nmt.edu (8.6.8.1/8.6.6) id WAA18853; Thu, 2 Jun 1994 22:17:37 -0600 Message-Id: <199406030417.WAA18853@sphinx.nmt.edu> From: yodaiken@sphinx.nmt.edu (Victor Yodaiken) Date: Thu, 2 Jun 1994 22:17:37 -0600 In-Reply-To: John Staples "Re: Qu-Prolog 3.2 and Ergo 4.0" (Jun 2, 12:15pm) reply-to: yodaiken@nmt.edu X-Mailer: Mail User's Shell (7.2.5 10/14/92) To: John Staples , qed@mcs.anl.gov Subject: Necessity of meta theory -- was Re: Qu-Prolog .. On Jun 2, 12:15pm, John Staples wrote: Subject: Re: Qu-Prolog 3.2 and Ergo 4.0 >* The modularity benefit is obtained only when it is possible > to interpret one theory in another. Specifying such interpretations > needs a meta-theoretic vocabulary. 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. >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. 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?