is an ultrafilter on the finite–cofinite algebra of Every filter on a Boolean algebra (or more generally, any subset with the finite intersection property) is contained in an ultrafilter (see ultrafilter lemma) and that free ultrafilters therefore exist, but the proofs involve the axiom of choice (AC) in the form of Zorn's lemma. On the other hand, the statement that every filter is contained in an ultrafilter does not imply AC. Indeed, it is equivalent to the Boolean prime ideal theorem (BPIT), a well-known intermediate point between the axioms of Zermelo–Fraenkel set theory (ZF) and the ZF theory augmented by the axiom of choice (ZFC). In general, proofs involving the axiom of choice do not produce explicit examples of free ultrafilters, though it is possible to find explicit examples in some models of ZFC; for example, Gödel showed that this can be done in the constructible universe where one can write down an explicit global choice function. In ZF without the axiom of choice, it is possible that every ultrafilter is principal. Ultrafilter on a Boolean algebra An important special case of the concept occurs if the considered poset is a Boolean algebra. In this case, ultrafilters are characterized by containing, for each element of the Boolean algebra, exactly one of the elements and (the latter being the Boolean complement of ): If is a Boolean algebra and is a proper filter on then the following statements are equivalent: is an ultrafilter on is a prime filter on for each either or () A proof that 1. and 2. are equivalent is also given in (Burris, Sankappanavar, 2012, Corollary 3.13, p.133). Moreover, ultrafilters on a Boolean algebra can be related to maximal ideals and homomorphisms to the 2-element Boolean algebra {true, false} (also known as 2-valued morphisms) as follows: Given a homomorphism of a Boolean algebra onto {true, false}, the inverse image of "true" is an ultrafilter, and the inverse image of "false" is a maximal ideal. Given a maximal ideal of a Boolean algebra, its complement is an ultrafilter, and there is a unique homomorphism onto {true, false} taking the maximal ideal to "false". Given an ultrafilter on a Boolean algebra, its complement is a maximal ideal, and there is a unique homomorphism onto {true, false} taking the ultrafilter to "true". Ultrafilter on the power set of a set Given an arbitrary set its power set ordered by set