# Re: Verification systems

guttman@linus.mitre.org
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