In this chapter we prove the compactness theorem using a model-theoretic construction known as an ultraproduct. To motivate the introduction of ultraproducts, we briefly revisit ideas from Chap. 1 . An ultraproduct arises from a family of factor structures, which may be conceived as voters choosing which first-order formulae will hold in the product structure. The reference to elections is not purely metaphorical. There is an interesting connection between pairwise decision methods and ultraproducts, which we explore in Sect. 5.1. The ultraproduct construction is given in Sect. 5.2, where the fundamental theorem governing the first-order properties of ultraproducts (i.e. Łos’ theorem) is proved. Instead of moving immediately to compactness, in Sect. 5.3 we obtain the field of real numbers from an ultraproduct construction. The reader who has never seen a rigorous construction of the reals will find this section helpful for its own sake and as a point of reference for the discussion of real closed fields in Chap. 11 . The reader who is familiar with a rigorous construction of the reals is likely not to have encountered the one we describe and may find it of some interest. Essentially the same ultraproduct construction employed in Sect. 5.3 can be iterated on the real field to obtain an elementary extension containing infinitely small and large numbers. In Sect. 5.4 we provide a brief taster of the model-theoretic approach to real analysis afforded by this expansion of numerical resources. We finally prove compactness in a few equivalent forms in Sect. 5.5 and proceed to obtain from it a characterisation of elementary classes (introduced in Sect. 3.1 ) in terms of ultraproducts. The addendum, i.e. Sect. 5.7, discusses a little known but remarkable application of ultrafilters due to the philosopher Clarence Irving Lewis.