Is the intersection of an arbitrary nonempty collection of sets a set in ZFC? How do you prove this? Is the intersection of an arbitrary nonempty collection of sets a set? How do you prove it one way or the other? Do we run afoul of the undefinability of truth or anything similar by even asking this question?

For an ordinal $\alpha$, I think the successor ordinal $\alpha^+$ can be defined in two ways:

*

*It is the least ordinal greater than $\alpha$.

*It is the intersection of the class of all the ordinals greater than $\alpha$.

I am curious how you would prove the simple fact that (2) is equivalent to (1).
The first thing that puzzles me is how to show that (2) is even a set in the first place.
Intuitively, it seems obvious that, given a non-empty collection of sets, its intersection should be a set, whether the collection is set-sized or not or definable or not.
However, I'm not sure that this principle actually follows from the axioms. Comprehension gives us the following:
$$ \exists x (\forall a (a \in x \leftrightarrow a \in A \land \varphi(a, \cdots))) \\ \text{where $A$ is a parameter is the axiom of schema of comprehension} $$
One way of interpreting this is that we can take any arbitrary single set $A$ and intersect it with a definable class $\{ x : \varphi(x, \cdots) \}$ and get back a set.
The ability to intersect arbitrary nonempty collections of sets and get back a set is consistent with this principle, but isn't implied by it.
So, is the intersection of an arbitrary nonempty collection of sets a set?
 A: First, it is meaningless to discuss collections of sets that are not definable in ZFC. So your question is not well-formed. Technically, it doesn’t even make sense to discuss collections of sets that aren’t themselves sets. We do this on the level of the metatheory.
The appropriate setting for discussing collections of sets which may not themselves be sets and which may not be definable is a class theory such as NBG or MK. In NBG, we can show that the intersection of any non-empty class is a set.
Given any nonempty class $C$ of sets, take an element $c \in C$. The intersection of all sets in $C$ can be given as $\{x \in c \mid \forall d \in C (x \in d)\}$, which is clearly a set by the axiom of separation.
Another possible interpretation of your question is this. Let $L’$ be the language of set theory plus a unwary predicate $P$. Let $M$ be an $L’$ structure and a model of ZFC. Does $M \models \exists x (P(x)) \to \exists y \forall z (z \in y \iff \forall w (P(w) \to z \in w))$?
In other words, given a model $M$ of ZFC and some nonempty $P \subseteq M$, is there some $y \in M$ such that for all $z \in M$, $z \in_M y$ if and only if for all $w \in P$, $z \in_M w$?
The answer is no, assuming ZFC is consistent. Take a model $M$ of ZFC with nonstandard natural numbers (for instance, a model which believes ZFC is inconsistent), and let $P$ be the set of nonstandard natural numbers in $M$. Then $\bigcap P$ would be exactly the set of standard natural numbers, since a nonstandard number is larger than all standard numbers, but is not larger than itself. But the set of standard natural numbers in $M$ doesn’t exist, since if it did, $M$ would recognise the set of standard natural numbers as the set of natural numbers, and thus wouldn’t have any nonstandard natural numbers.
