Return-Path: Delivery-Date: Received: from antares.mcs.anl.gov (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Fri, 16 Apr 1993 01:24:15 +0100 Received: by antares.mcs.anl.gov id AA10740 (5.65c/IDA-1.4.4 for qed-outgoing); Thu, 15 Apr 1993 19:18:14 -0500 Received: from swan.cl.cam.ac.uk by antares.mcs.anl.gov with SMTP id AA10732 (5.65c/IDA-1.4.4 for ); Thu, 15 Apr 1993 19:18:10 -0500 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Fri, 16 Apr 1993 01:18:04 +0100 To: QED Subject: "Little Theories" and the base logic Date: Fri, 16 Apr 93 01:18:00 +0100 From: John Harrison Message-Id: <"swan.cl.ca.855:16.04.93.00.18.08"@cl.cam.ac.uk> Sender: qed-owner@gov.anl.mcs 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)