An ultrafilter on a set I is a maximal collection of subsets closed under supersets and finite intersections. Unlike principal filters, free ultrafilters exist on infinite sets (requiring the axiom of choice). Ultrafilters enable ultraproduct constructions by identifying sequences that 'agree on a U-large set', providing a natural notion of 'genericity'.
Think of an ultrafilter on a set I as a coherent "notion of largeness" for subsets of I. A filter F is a collection of subsets closed upward (if A ∈ F and A ⊆ B, then B ∈ F) and closed under finite intersections. The trivial filter {I} says only I itself is "large." An ultrafilter is a maximal filter: for every subset A ⊆ I, exactly one of A or its complement Iˢ∖A belongs to the filter—the ultrafilter forces a binary verdict on every subset with no abstentions. This maximality condition makes ultrafilters the set-theoretic analogue of a decisive voting system where every issue is resolved.
Principal ultrafilters are transparent: fix an element i₀ ∈ I and declare A "large" if and only if i₀ ∈ A. This filter is just evaluation at a point. Free (non-principal) ultrafilters are more subtle: they contain all cofinite sets (those with finite complement) but are generated by no single element. Their existence on infinite sets requires the axiom of choice (via Zorn's lemma); they cannot be constructed explicitly. Despite being non-constructive, free ultrafilters are the logically significant ones, because they capture a notion of "almost everywhere" that is genuinely non-trivial—a set is "large" not because it contains a fixed special point, but because it is pervasive in a sense that cannot be located.
The connection to logic and your prerequisite on types comes through Łoś's theorem (the fundamental theorem of ultraproducts). Given a family of structures Mᵢ indexed by I and an ultrafilter U on I, form the Cartesian product ∏ Mᵢ and declare two sequences (aᵢ) and (bᵢ) U-equivalent if they agree on a U-large index set: {i : aᵢ = bᵢ} ∈ U. The quotient is the ultraproduct ∏ Mᵢ / U. Łoś's theorem states that a first-order sentence φ holds in this ultraproduct if and only if the set of indices where φ holds in Mᵢ is U-large. In other words, the ultraproduct "votes" on which sentences to satisfy, with U as the voting rule. Because U is an ultrafilter, every sentence is decided—the ultraproduct is always a model, not a partial structure.
This machinery connects directly to types. A type is a maximal consistent set of formulas, and the ultraproduct realizes the "average" first-order theory of the Mᵢ as voted by U. Ultraproducts are the primary tool for proving the compactness theorem (any finitely satisfiable theory is satisfiable) algebraically rather than syntactically, and for transferring properties between models—if all Mᵢ satisfy some first-order sentence, the ultraproduct does too, and conversely. The construction also shows how non-standard analysis arises naturally: take the ultraproduct of ℝ over the natural numbers with a free ultrafilter, and you obtain a field of hyperreals containing infinitesimals and infinitely large elements, yet satisfying every first-order sentence true of ℝ.