Unary intersection of the empty set

In MK (Morse-Kelley) set theory life is easy: $\forall X\forall y\left(y\in\bigcap X\leftrightarrow\forall x\left(x\in X\rightarrow y\in x\right)\right)$. If $X=\left\{\right\}$ then $\bigcap X=U$, where $U$ is the universal class. So the (unary) intersection of the empty set is the class that contains all sets as elements. In ZF (Zermelo-Fraenkel) set theory, instead, proper classes are not allowed. So, how can I define $\bigcap X$ in ZF? I tried with the following definitions:

1. $\forall X\left(X\not=\left\{\right\}\rightarrow\forall y\left(y\in\bigcap X\leftrightarrow\forall x\left(x\in X\rightarrow y\in x\right)\right)\right)$. This means that $\bigcap\left\{\right\}$ is undefined, which is not that good.
2. $\forall X\forall y\left(y\in\bigcap X\leftrightarrow X\not=\left\{\right\}\land\forall x\left(x\in X\rightarrow y\in x\right)\right)$. This means that $\bigcap\left\{\right\}=\left\{\right\}$, which is the opposite of MK.

I couldn't find any other valuable definition. Any ideas? Thank you.

-

The fact that proper classes are handled differently in ZF than in MK doesn't really affect the definition of the unary intersection or other operations that can produce proper classes. So in ZF, $\bigcap z$ is defined using the same definition as in MK: $$y \in \bigcap z \Leftrightarrow (\forall w \in z) ( y \in w).$$ Just like in MK, $\bigcap \emptyset$ is a proper class in ZF.

There are treatments of ZF in which the authors don't handle proper classes at all, but there are other treatments in which proper classes are "allowed". The simplest way to allow them is to restrict to definable proper classes, and silently replace each such class with its definition whenever the class is used. In this way, for any class or set $z$ we have a (possibly proper) class $\bigcap z$ defined as above. We can prove as a theorem in ZF (just as in MK) is that if $z$ is a nonempty set then there is a set $\hat{z}$ such that $\hat{z} = \bigcap z$.

Addendum: I want to emphasize that this does not conflict with the answer given by Arturo Magidin. The definition I stated here (in which $\bigcap \emptyset$ is a proper class) is the one used by Levy, Basic Set Theory). The definition in the other answer, in which $\bigcap \emptyset = \emptyset$, is used by other authors (I believe). Kunen, Jech, and Halmos all leave $\bigcap \emptyset$ undefined in their well-known texts.

-
Let me see if I understood correctly. One should distinguish between defining something and proving its existence. In this case, the intersection of the empty set is defined as you said, but one can prove that it doesn't exist (in ZF). That is, $\bigcap\left\{\right\}$ is just a notation for something that doesn't belong to the universe of discourse. Am I right? – Francesco Turco Oct 12 '10 at 19:05
In ZF, it's often convenient to think of a proper class as a property that a particular set might or might not have. For example "$x = x$" is a property that every set has, and the property $x \in \bigcap \emptyset$ is another property that every set has (if you use the definition I wrote above). Similarly "$x$ is an ordinal number" is a property of $X$. All these properties have proper classes as their extents, and in that sense they don't exist as sets in ZF. But each of them can be represented by some formula in the language of ZF, which gives us a way to prove things about them. – Carl Mummert Oct 12 '10 at 19:14
But what if I take the property $y=y$ and the term $\bigcap\left\{\right\}$? The axiom of specification says there exists a subset of the latter such that the former holds. This contradicts the fact that the set of all sets doesn't exist. I'm using universal elimination from natural deduction here. Perhaps my error is that $\bigcap\left\{\right\}$ is a function symbol: my logic book says I should use a constant symbol instead. I'm a little confused. – Francesco Turco Oct 12 '10 at 19:42
If you want $\bigcap$ to be a term-forming operator (equivalently, if you want $\bigcap z$ to be a set whenever $z$ is), you have to use a different definition, for example the one Arturo Magidin mentioned above. However, there's no reason that you have to actually add that term-forming operation to the language of ZF. Instead, you can simply view $x \in \bigcap z$ as an abbreviation for $(\forall w \in z)(x \in w)$. Indeed, in the "orthodox" presentation of ZF, there are no term-forming operations at all; even the binary union and intersection symbols are just abbreviations for formulas. – Carl Mummert Oct 12 '10 at 20:18

The way I learned it, in ZF, we define the unary union by $$\forall y \left(y\in\cup X \Leftrightarrow \exists z(z\in X\wedge y\in z)\right).$$

The unary intersection is defined using the unary union and the Axiom of Separation: $$\cap X = \left\{ y\in\cup X\,|\, \forall z(z\in X\rightarrow y\in z)\right\}.$$

Using this definition, since $\cup\emptyset = \emptyset$, then $\cap\emptyset=\emptyset$ as well.

-
Now that you write it, I'm sure I've seen this as well. It's an elegant way to avoid the issue so that we have a definable function $\bigcap \colon V \to V$. – Carl Mummert Oct 12 '10 at 17:49

The only other way I can think of is to use specification, which is really the only way you know that such a set exists. Given a universe $U$, define $\bigcap X$ to be the unique $B$ satisfying the following formula:

$$\forall x(x\in B\Leftrightarrow(x\in U\wedge \exists y(y\in X\wedge x\in y)))$$

Then $\bigcap\emptyset=U$. Is this any more or less desirable than having $\bigcap\emptyset$ be a proper class or $\emptyset$ itself? I don't know. My topology instructor used it when defining a topology to ensure that the universe was always open, but this is just cosmetic -- there's nothing to be lost by just including this as another axiom. Ultimately, I suppose everyone but the most hardcore set theorists will just use what works and ignore the axiomatic background.

-