Date: 11 May 89 01:18:06 EDT
From: Francisco Corella <CORELLA%ibm.com@munnari.oz>
To: info-hol@clover.ucdavis.edu
Subject: sets in hol

I also agree with Elsa.  Type theory started out as a particular variant
of set theory.  More precisely, type theory without lambda-abstraction
is a many-sorted, first-order theory of sets, the set-membership
construct being "(P:*->bool X:*)", which is often written "X in P".

But I would like to add something: type theory can also be viewed as an
extension of F.O.L.; that's why we call it H.O.L. (These two different
views can actually be formalized as two different model theoretic
interpretations of the same logistic system: the interpretation as
H.O.L. corresponds to Henkin's standard models; the interpretation as
many-sorted F.O. set theory corresponds, roughly, to Henkin's general
models.)

So there is another way of doing set theory within H.O.L.: by making
set-membership a constant of type ind->ind->bool, i.e. a binary
predicate, and axiomatizing it with the axioms of, say, Zermelo-Fraenkel
set theory, or those of Bernays' (with the distinction between sets and
classes), or those of any other flavor of first-order set theory.  The
way to look at the resulting system is as an extension of set theory
within F.O.L.; and it turns out that the extension is conservative.

Francisco Corella