In model theory, for the construction of an ultraproduct one needs the existence of an ultrafilter.
I heard that one can't construct an ultrafilter by hand, one cannot write it down, just merely knowing that one exists by using the axiom of choice. How is this meant? Even if I give you a concrete base set, say $X=\mathbb N$, is it not possible to write down an ultrafilter on $X$? (I just notice, that $U$ defined by $A\in U:\Longleftrightarrow 3\in A$ probably is an ultrafilter on $\mathbb N$, but it is a boring one, so my question should ask for real examples.)
Of course, up to now, my question is quite imprecise. Maybe one can formalize it like so: in ZF (without AC), is it possible to prove the existence of an ultrafilter on $\mathbb N$ which is non-principal?
What about other base sets, say finite ones? Can ZF prove the existence of an ultrafilter on a finite set?