Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Date: Wed, 30 Dec 92 15:35:58 -0800
From: toal@edu.ucla.cs (Ray J. Toal)
Message-Id: <9212302335.AA11442@hapuna.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: Intersection of Nothing
Cc: toal@edu.ucla.cs


To any set theorists out there,

Consider the unary intersection operator

  INT P = {x | !S in P. x in S}

which, since I prefer predicates to sets I would write

  INT P = \x. !S. P S ==> S x

that forms the intersection of a set of sets, e.g.

  INT { {4, 5, 7}, {2, 7, 4}, {1 .. 10} } = {4, 7}.

It is easy to prove, in HOL (see below), that

  INT { {} } = {0, 1, 2, ... }

or, in general, the intersection of the empty set of "sets of type sigma"
is the "the set of all elements of type sigma".

Now I learned Type Theory rather than Axiomatic Set Theory as a formalization
of mathematics and am only slightly familiar with the latter.  I think that
Set Theory does not admit "the set of all sets" and avoids the paradoxes
by compilcating its axioms rather than just using types.  I am interested in
whether there is a set-theoretic analogue of the "intersection of the
empty set of sets".  In other words, can you say anything about
the (say Zermelo-Fraenkel-Choice) expression

  --
 |  |  P
 |  |   

when P = emptyset?

 
--------------------------
P.S. Here is the HOL proof

let INT_DEF =
  new_definition
    (`INT_DEF`,
    "INT(P:(*->bool)->bool) = \x. !s. P s ==> s x");;

PROVE ("INT(\x:*->bool.F) = (\x:*.T)", REWRITE_TAC [INT_DEF]);;


Ray Toal