Why can we not explicitly construct a non-principal ultrafilter in ZFC? I'm writing an essay on the construction of the hyperreal numbers as an ultraproduct, and would like to include some kind of reference or footnote as to why we can't give an explicit example. I've seen multiple threads here discussing the non-existence of non-principal ultrafilters in ZF, but would like some details on why there's no way to construct one, even in ZFC.
 A: The idea here is that things that require the axiom of choice to exist tend to encode "a certain amount of choice" in them. While the axiom of choice lets you prove the existence of a well-ordering, it is not strong enough to provide you with a distinguished well-ordering for each and every set (this would be equivalent to global choice).
In other words, well-orders are kind of like cockroaches, if there is one, there are usually a lot, and they "kinda look the same", so none of them is distinguished.
And non-principal ultrafilters require the axiom of choice to exist. Indeed, it is consistent with $\sf ZF$ that there are no such ultrafilters at all. So it means that we can define a distinguished ultrafilter on $X$ given a well-ordering of $\mathcal P(X)$, but different well-orderings will give you a different ultrafilter. Since there is no distinguished well-ordering, there is no reason to expect there is a distinguished ultrafilter.
Of course, as we remarked above, if we do have global choice (in models of $V=L$, or more generally $V=\rm HOD$, or even modulo a paremeter, in $V=\mathrm{HOD}[x]$), then we do have a distinguished well-order for every set, in particular for the power set of every set, and so we can in fact define a distinguished non-principal ultrafilter on every infinite set (or more simply, apply the global choice function!).
More formally, we need to construct a model of $\sf ZFC$ in which there is no formula $\varphi(x,u)$, such that for every infinite set $x$ there is a unique non-principal ultrafilter $u$ such that $\varphi(x,u)$ holds. We may want to allow a parameter, but it's a set parameter. Doing this is more technical, but can be done by forcing (or rather class forcing).
