Re: "Little Theories" and the base logic
guttman@linus.mitre.org
Message-id: <9304181601.AA02738@circe.mitre.org>
To: John Harrison <John.Harrison@cl.cam.ac.uk>
Cc: QED <qed@mcs.anl.gov>
Subject: Re: "Little Theories" and the base logic
In-reply-to: Your message of "Fri, 16 Apr 93 01:18:00 BST."
<"swan.cl.ca.855:16.04.93.00.18.08"@cl.cam.ac.uk>
X-Postal-Address: MITRE, Mail Stop A156 \\ 202 Burlington Rd. \\ Bedford, MA 01730
X-Telephone-Number: 617 271 2654; Fax 617 271 3816
Date: Sun, 18 Apr 93 12:01:50 -0400
From: guttman@linus.mitre.org
Sender: qed-owner
Precedence: bulk
John Harrison (jrh@cl.cam.ac.uk) writes:
> However it seems that for this to work properly, the "base" logic that strings
> all these statements together has to be reasonably powerful. For example, lots
> of interesting algebraic structures, e.g. real-closed fields, aren't finitely
> axiomatizable in first-order logic, so you would seem to be committed to some
> form of higher order logic to accommodate them, or else to carrying set theory
> around in all the theories.
As Javier mentioned, our preference is certainly also for a form of
higher order logic. But it seems quite feasible that an
implementation (if for some reason it was wedded to first order logic)
could offer a mechanism for axiom schemes.
I don't know whether it would be workable to cover any very wide class
of axiomatizable (r.e.) first order theories. However, in practical
cases infinite sets of axioms have very simple structure (generally
just plugging any syntactic predicate into a hole). A first order
logic with predicate variables (but no quantification or other binding
on them, and with no variables of higher types than predicates) might
be suitable syntax. And I think it could be arranged to have just the
same meta-logical properties as a more ordinary first order logic.
Josh