Conceptual Question about the formal definition of $\bigcap \mathcal F$ In Kenneth Kunen's "The Foundations of Mathematics, the following definition is provided:

When $\mathcal F \neq \emptyset$, $$\bigcap \mathcal F = \bigcap_{Y\in \mathcal F}Y=\{x:\forall Y \in \mathcal F(x\in Y)\}$$

Firstly, I will mention that I recognize why we want $\mathcal F \neq \emptyset$ if the formula $\varphi$ we choose to go with is $\varphi:=\forall Y \in \mathcal F (x \in Y)$. Namely, if $\mathcal F = \emptyset$, this formula would be vacuously true so any $x$ would satisfy this formula...and thus all $x$ in our universe would be admitted into the set. The universal set is a contradiction because it contains itself (and by Axiom of Regularity and Pairing Axiom, this cannot happen).
My question is: How should I encode in First Order Logic the fact that I do not want $\mathcal F$ to equal $\emptyset$?
At first I thought that the correct approach was to replace "$\forall Y \in \mathcal F(x\in Y)$" (which is equivalent to "$\forall Y [Y \in \mathcal F \rightarrow x \in Y]$) with:
$$\forall Y ([\mathcal F = \emptyset \lor Y \in F] \rightarrow x \in Y)$$
This seemed to make sense because if $\mathcal F$ does equal $\emptyset$, the universally quantified statement will be interpreted as a false statement (because, for whatever $x$ one choses, $x \notin \emptyset$)...in which case $\bigcap \emptyset = \emptyset$. There is no contradiction here.
However, after looking around on some posts and sites, it seems as though we want to retain the fact that $\bigcap \emptyset:= \text{Universal Set}$.
Given this, what is the formal way of encoding Kunen's definition (i.e. stipulating that $\mathcal F \neq \emptyset$)?
Thank you!
 A: What you're observing here is a tension between two approaches to "$\bigcap$:"

*

*as a total operation, which takes in a set and spits out either a set or the proper class $V$ (I'm assuming we're working in $\mathsf{ZF}$ or similar, where there is no universal set), the latter iff the input is $\emptyset$; or


*as a partial operation, which takes in a set and spits out a set or is undefined, the latter iff the input is $\emptyset$.
Kunen takes approach $(2)$, while some texts/sites take approach $(1)$ (or work in a framework where a universal set is accepted, in which case you get the best of both worlds but have to leave the $\mathsf{ZF}$-context). Certainly it's important for someone starting the subject to understand why the "naive" definition of $\bigcap$ leads to interpretation $(1)$, but approach $(2)$ is more convenient if we're working in first-order logic modified to accommodate partial functions (since at that point we can treat "$\bigcap$" as a genuine function), the issue with $(1)$ being that a proper class is not an "actual object" in the relevant sense. Ultimately there isn't a huge advantage one way or the other.
What you've written is a third alternative:


*Interpret "$\bigcap$" as a total operation, which takes in a set and outputs a set, agreeing with $(1)$ and $(2)$ when the input is nonempty and using a "default value" of $\emptyset$ when the input is $\emptyset$.

In my opinion this is slightly less good: I don't think totality is worth paying the price of actively disagreeing with $(1)$. But this approach will also work fine, as long as one is careful to handle the emptyset (which one should be anyways).
