Construction of Ultrafilters I've been doing a lot of work with ultrapowers and saturation recently. In particular, I am reading chapter 6 of Chang and Keisler as well as Keisler's paper on "Ultraproducts which are not saturated". In chapter 6 of C&K, they give define what it means to be a $\alpha-good$ ultrafilter and spend a long time on the existence of such types of filters. But then it hits me, I know about all these "different types" of ultrafilters, but I don't $know$ any $examples$ of such ultrafilters.   
Is it provable that one cannot actually give an explicit example of a non-principal ultrafilter of $\mathbb{N}$? Or can someone give an explicit example of one (defined recursively)?
Edit: As André Nicolas pointed out, $ZF\not\vdash $ "There exists a non-principal ultrafilter". How do you construct a model of ZF which does not have any non-principal ultrafilters?
 A: Constructing any model of $\sf ZF$ where the axiom of choice fails requires some preliminary amount of knowledge. Here are some of the usual perquisites, some constructions may require only part of them.


*

*Permutation models of set theory with atoms. These are not quite models of $\sf ZF$, but they are relatively simpler to understand. Some statements can be transfered from such models to models of $\sf ZF$, and that makes a lot of examples relatively easy to grasp.

*Forcing. Forcing is an important tool for constructing any models of set theory in modern set theory, and one should be comfortable with the basics of forcing. Class forcing is worth mentioning, because sometimes it is needed in these contexts.

*Symmetric extensions. This is an extension of the method of forcing, but it deserves a separate mention. This is one of the two major tools of constructing models of $\sf ZF$ without the axiom of choice. The transfer theorems mentioned in the first point make use of this technique.

*Relative constructibility. This is another method of constructing models where the axiom of choice fails. In some cases it allows us to avoid using forcing, and in other cases it just allows us to avoid using symmetric extensions. But in either case this method is very useful and very common in papers where the axiom of choice fails.
For some purposes you might need more tools. Things like large cardinals can come into play, or infinitary combinatorics, and so on. There is also the things about understanding mathematical ideas that you wish to interact with. If you wish to construct a model without free ultrafilters on $\Bbb N$, then it is good to understand what are the properties of such sets, and what sort of things follow from their existence.
Now we can approach the examples for models where there are no free ultrafilters. The case where we are only interested in "No free ultrafilters over $\Bbb N$" is somewhat simpler, and this is a problem given in Jech The Axiom of Choice (Ch. 5, Problem 24, p.82).
This, as Paul McKenney pointed out a consequence of statements like "all sets of reals are measurable" and "all sets of reals have the Baire property". Since both properties become cumbersome in models where $\Bbb R$ is a countable union of countable sets, let me talk about them in conjunction of $\sf DC$ (or at least "$\omega_1$ is regular").
Both the statements hold in Solovay's model, which as far as models of $\sf ZF$ go, is relatively simple to construct. The proofs that both these properties hold require deeper and better understanding of set theory, though. Shelah proved that to obtain a model where all sets of reals are measurable requires the existence of an inaccessible cardinal, while the construction of a model of $\sf ZF+DC+BP$ does not require an inaccessible. Naturally, his construction is considerably more difficult than that of Solovay.
The general case of "There are no free ultrafilters" is more difficult, as expected. The proof is due to Andreas Blass, and can be found in his paper:

Blass, Andreas "A model without ultrafilters." Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys. 25 (1977), no. 4, 329–331. 

