Re: Verification systems

• Mail folder: QED
• Next message: Robert S. Boyer: "Answer to a question, and further speculation on a QED foundation"
• Previous message: guttman@linus.mitre.org: "Re: "Little Theories" and the base logic "
• In-reply-to: David McAllester: "Verification systems"
• Reply: David McAllester: "Verification systems "

Message-id: <9304181617.AA02751@circe.mitre.org>
To: qed@mcs.anl.gov
Subject: Re: Verification systems 
In-reply-to: Your message of "Thu, 15 Apr 93 19:27:49 EDT."
             <9304152327.AA00625@spock> 
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:17:10 -0400
From: guttman@linus.mitre.org
Sender: qed-owner
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