Delivery-Date: 
Posted-Date: Sun, 18 Apr 93 12:17:10 -0400
Message-Id: <9304181617.AA02751@circe.mitre.org>
To: qed@gov.anl.mcs
Subject: Re: Verification systems
In-Reply-To: Your message of "Thu, 15 Apr 93 19:27:49 EDT." <9304152327.AA00625@spock>
Date: Sun, 18 Apr 93 12:17:10 -0400
From: guttman@org.mitre.linus
Sender: qed-owner@gov.anl.mcs
Precedence: bulk

David McAllester writes:

> [HOL] is a "foundational" system in the sense that there is one
> underlying logic with (arguably) a single intended model
> (the universe of sets).

> The Boyer-Moore prover ... is also foundational.

> IMPS has ... a foundational logic based on the "little theories"
> method of organizing mathematical theorems. 

Do Boyer and Moore think of NQTHM as foundational in the sense of
having a single intended model?  I had thought they took the free
variables to range over any arbitrary structure satisfying the axioms
that might be in use.  

In any case, if I understand what you mean by "foundational", then
"foundational" contrasts with the little theories approach.  Theorems
proved in a theory of (say) a group are not about a single intended
model.  Rather, they are about all structures that may satisfy the
group properties.  Theory interpretation is a way of bringing these
resluts to bear on another class of models, when all of them exemplify
the properties of the source theory in a particular uniform way.  

Or have I misunderstood what you had in mind by "foundational"?


	Josh