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?