Formally Introducing the Intersection Symbol into ZFC Set Theory I am currently reading Lectures in Logic and Set Theory: Volume 2, Set Theory by Tourlakis. In the book, he formally introduces the power set notation, $\mathcal{P}(A)$, as well as union, $\bigcup A$, into the formal, first-order theory of sets as unary function symbols by extending the theory through definition. This process is described in the linked Wikipedia article and also here but, in summary, to introduce a function symbol into our theory, we must first find a defining formula for the function, \begin{equation}\forall x_1\ldots\forall x_n\phi(f(x_1,\ldots, x_n), x_1,\ldots x_n),\tag{Defining Axiom}\end{equation}
where $\phi(y,x_1,\ldots,x_n)$ is a first-order formula with free variables $y,x_1,\ldots,x_n$, then take this defining axiom and add it to our formal theory as a non-logical axiom. However, this is provided that we first have a proof of the existence and uniqueness of such an object for every possible term: $$\forall x_1\ldots\forall x_n\exists ! y\phi(y,x_1,\ldots x_n)\tag{Existential Formula}.$$
My question is how is this done for the intersection symbol, $\bigcap$? Tourlakis avoids the issue since $\bigcap\varnothing$ is not a set and thus "violates" the existential formula. Specifically, he writes, "We do not feel inclined to perform acrobatics just to get around the fact that $\bigcap\varnothing$ cannot be a formal term: it is not a set." I would like to know how this issue is resolved and, if the "acrobatics" required to get around this issue is too extreme, how I can be assured that leaving this as a loose end will not cause too many issues in the theory.
 A: A simple way around this is to just define $\bigcap\emptyset$ to be something else.  For instance, define $\bigcap X$ as usual if $X$ is not empty, and define $\bigcap X=\emptyset$ if $X$ is empty.  Then you have a perfectly good extension by definition using this symbol $\bigcap$, and you just have to make sure to prove (or assume) its argument is nonempty every time you use it so that it really does have the desired meaning (which you would have to do using $\bigcap$ informally anyways).
A: Eric Wofsey has described the "default value" approach. Another option is to simply modify the semantics of first-order logic to admit partial functions. Then any time we have a formula $\varphi(x_1,...,x_n,y)$ such that our theory proves that for each $a_1,...,a_n$ there is at most one $b$ with $\varphi(a_1,...,a_n,b)$, we can introduce a symbol for the partial function defined by $\varphi$.
Of course, doing this requires going back and modifying the proof system, which is some tedious work that the "default value" approach doesn't require us to do. However, it's ultimately not that hard, and allowing partial functions is arguably more natural anyways since in informal mathematics we use partial functions (e.g. "$x\over y$") all the time without worry.
