Delivery-Date: 
From: dam@edu.mit.ai (David McAllester)
Date: Sun, 18 Apr 93 17:42:58 EDT
Message-Id: <9304182142.AA00902@spock>
To: guttman@org.mitre.linus
Cc: qed@gov.anl.mcs
In-Reply-To: guttman@linus.mitre.org's message of Sun, 18 Apr 93 12:17:10 -0400 <9304181617.AA02751@circe.mitre.org>
Subject: Verification systems
Sender: qed-owner@gov.anl.mcs
Precedence: bulk

By "foundational" I mean a system that is intended to be used (or is
most commonly used) by extension with definitions lemmas and theorems.
This is to be contrasted with systems whose typical use involves new
(unjustified) axioms.  Definitions guarantee that extensions are
conservative --- no new facts can be proved about old symbols.  In
most resolution systems there is no notion of conservative extension
via definitions.

Mathematics itself seems to have made a transition at some point from
axiomatic to foundational techniques.  The modern informal approach
DEFINES a group to be a structure (or a tuple) satisfying certain
conditions.  Only rarely are really new axioms considered (such as the
existence of measurable cardinals).

Does IMPS have a conservative extension property stating that the
introduction of a new little theory does not allow the proof of new
theorems about old theories?  If so then I would call IMPS a
foundational system.  It seems to me that the theorems provable in any
given theory will be influenced by your choice of foundation.  I'm not
sure if you encorporate the axiom of choice.  Can you prove that any
group can be extended by a predicate that well orders its domain?
Can you prove that infinite groups exist?

	David