The axiom of constructibility $V=L$ leads to some very interesting consequences, one of which is that it becomes possible to give explicit constructions of some of the "weird" results of AC. For instance, in $L$, there is a definable well-ordering of the real numbers (since there is a definable well-ordering of the universe).


Since AC holds true in $L$, the ultrafilter lemma must be true. Does this mean that a definable non-principal ultrafilter on $\mathbb{N}$ exists in $L$, given by an explicit formula?


If so, what is the formula?



In $L$, does there exist a definable non-principal ultrafilter on $\mathbb{N}$
Yes, but it's not particularly nice: since $L$ has a definable well-ordering of the sets of reals (in fact, of all of $L$) coming from the $L$-hierarchy itself, there is a formula defining the "least" (in that well-ordering) ultrafilter, $U$.


(This $U$ isn't the only naturally definable ultrafilter in $L$; we could also consider the ultrafilter gotten by going through the infinite sets of natural numbers, in the $L$-order, and throwing in each set that we can - a sort of "greedy algorithm" for building an ultrafilter. This ultrafilter $U'$ would also be definable, and there's no reason for $U'$ to equal $U$. Other tricks exist.)


Note that, while of course there are only countably many definable ultrafilters, we can use the $L$-ordering to produce a definable ultrafilter with any given definable property ("the least ultrafilter with property X") - so there's basically nothing that can be said about the definable ultrafilters.


