Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.2); Thu, 31 Dec 1992 00:51:18 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA15914;
          Wed, 30 Dec 92 16:36:35 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA15909;
          Wed, 30 Dec 92 16:36:29 -0800
Received: by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA16064;
          Wed, 30 Dec 92 16:36:00 -0800
Date: Wed, 30 Dec 92 16:36:00 -0800
From: toal@edu.ucla.cs (Ray J. Toal)
Message-Id: <9212310036.AA16064@maui.cs.ucla.edu>
To: kaufmann@com.cli
Subject: Re: Intersection of Nothing
Cc: info-hol@edu.uidaho.cs.ted

Hi Matt,

Thanks for the reply.  Intuitively I know that a "universal set" of
some sort is like an identity for iterated intersection -- I mean
that if you had that

  INT P = Q

and you added another set to P you'd likely make Q smaller, so
of course INT {} = U makes intuitive sense.  But because ZFC
has no types in the sense of HOL, then is the "relative
intersection" operator *necessary*?

Ray Toal