Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Message-Id: <m0n7kJR-0000d0C@moa.pmms.cam.ac.uk>
Date: Fri, 1 Jan 93 11:13 GMT
From: Thomas Forster <T.Forster@uk.ac.cam.pmms>
To: info-hol@edu.uidaho.cs.ted, toal@edu.ucla.cs
Subject: Re: Intersection of Nothing

    What is `obvious' is that \bigcap P is a subset of any member of P.  So,
{\sl as long as P is nonempty} we can reason in ZF (or even in Zermelo set
theory - we do not need replacement) as follows:
      Think of any member y of P, it doesn't matter which.  \bigcap P is a subset
of y, and so is a set by aussonderung, comprehension, call it what you like.
Formally we have 
$$\bigcap P = \{x \in y:(\forall z \in P)(x \in z)\}$$
(aussonderung, comprehension etc is the scheme that says that $\{x \in y: \phi\}$ is a set
for all y and all \phi.)   So \bigcap P is a set.  
    Clearly this proof depends on there being a y in P.  If P is empty this proof
doesn't work.  And we'd better hope no other proof works either beco's if it did,
Zermelo set theory would be inconsistent and then the sky would fall in.

       Thomas Forster