Via:  uk.ac.nsf; 11 May 89 11:56 BST  (UK.AC.Cam.Cl.scaup)
Message-Id: <8905111028.AA29009@clover.ucdavis.edu>
From: ac@com.hp.hpl.hplb
Subject: Re: theory of sets
To: info-hol <info-hol@edu.ucdavis.clover>
Date: Thu, 11 May 89 11:26:52 BST
Sender: ac <ac%com.hp.hpl.hplb@edu.ucdavis.clover>
Status: R


I have been using a simple theory of sets for some of the work I
have been doing recently. The approach I took was precisely that
suggested by most people so far, i.e. to represent sets as
predicates of type *->bool. I've been using the theories for 4 to
5 months now and I've found it to be a good representation to
work with.

I basically followed the same style as David Shepherd in working
through Halmos, setting up the definitions and proving the
properties described in the book. All the definitions are
conservative of course, no new_axiom. This has been sufficient for my
needs: I have theories for element, subset, strict subset, union,
intersection, power set, difference, big union and big
intersection. I haven't started playing around with finite sets
yet, but I may need to shortly, so I'll have to extend this
further.

What I have found so nice about this representation is that the
proofs of set properties all fall out relatively easily since
they mostly involve laws of functional application and boolean
algebra. E.g. The associativity of union and intersection come
down to associativity of disjunction and conjunction
respectively. And a lot of other properties had similar
analogies.

I have forwarded the theory files to Mike Gordon in case some of
them come in handy in building a set theory library.

Albert Camilleri

ac@hplb.hpl.hp.com      (U.S.)
ac@hpl.hp.co.uk         (Europe)