"Little Theories" and the base logic

• Mail folder: QED
• Next message: : ""
• Previous message: David McAllester: "Verification systems"
• Reply: guttman@linus.mitre.org: "Re: "Little Theories" and the base logic "

To: QED <qed@mcs.anl.gov>
Subject: "Little Theories" and the base logic
Date: Fri, 16 Apr 93 01:18:00 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-id: <"swan.cl.ca.855:16.04.93.00.18.08"@cl.cam.ac.uk>
Sender: qed-owner
Precedence: bulk

I think the idea of "little theories" is a very good one.

I'm not sure exactly how it works in IMPS, but let's suppose for the sake of
argument that a little theory is a collection of theorems with certain "axioms"
as premisses. (Or equivalently, implicational theorems with the "axioms" as
antecedents.)

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. Is this true, or am I misunderstanding the idea?

John Harrison (jrh@cl.cam.ac.uk)