In $L$, does there exist a definable non-principal ultrafilter on $\mathbb{N}$ 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?
 A: Let me emphasize what Noah de-emphasized (by putting it in parentheses) in his answer: Instead of the "really cheap" idea of the first free ultrafilter in $L$-order, one can use the $L$-order of subsets of $\mathbb N$ to greedily construct an ultrafilter. The $L$-ordering of the subsets of $\mathbb N$ is a $\Delta^1_2$ relation with some additional properties (I believe Moschovakis uses the terminology $\Delta^1_2$-good well-ordering). One can then deduce that the greedily constructed ultrafilter is a $\Delta^1_2$ set of subsets of $\mathbb N$.
Since free ultrafilters on $\mathbb N$ never have the Baire property and are never Lebesgue measurable, this shows that the classical results, that analytic and coanalytic sets have the Baire property and are measurable, cannot be extended higher in the projective hierarchy in ZFC (without additional hypotheses like large cardinals or determinacy).
Similar greedy constructions based on the $L$-ordering of the reals produce $\Delta^1_2$ examples of lots of other sets of reals that, in the absence of $V=L$, would be obtained by applying the axiom of choice and thus might not be definable at all.  Examples include Hamel bases over $\mathbb Q$, Vitali sets, and Bernstein sets.
A: Generally formulas in set theory are not "very nice". There is very little structure to work with.
We can define when $U$ is a filter over $X$, simply by saying that every element of $U$ is a subset of $X$, and $U$ is closed under superset (below $X$), and under finite intersections (recall that in set theory we can say that within a first-order formula, simply by stating that the intersection over a finite subset of $U$ is in $U$).
Then we can define $U$ as an ultrafilter as a filter which is maximal with respect to inclusion. And $U$ is free if it doesn't contain finite sets, or a singleton, or its entire intersection is empty. Pick your pick.
Finally, from the axiom of choice we can prove that the set of ultrafilters over $\Bbb N$ is non-empty. Therefore using the canonical well-ordering of $L$ we can fully state "the least free ultrafilter over $\Bbb N$". It's just an insanely long formula (especially if you unwind all the recursive definitions everywhere and the abbreviations for subsets, finite, etc.) which is not very pretty.
A: 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.
