What the Vitali set, Bernstein sets and free ultrafilters cost in choice

Choice enters this page in three genuinely different ways.

First, Assuming choice on the cosets of $\mathbb{Q}$ in $\mathbb{R}$, a Vitali set in $[0,1]$ exists uses a selector on the family of rational-equivalence classes meeting $[0,1]$. Assuming the Axiom of Choice, a Vitali set is not Lebesgue measurable treats an already given selector by countably many rational translates. Its statement also assumes AC, which supplies the countable choice inherited from the local Lebesgue measure construction; the measure argument therefore has an explicit inherited cost.

Second, Assuming the real line can be well ordered, a Bernstein set exists uses a well-order of the real line and a transfinite construction through the perfect subsets. That is a different cost from the Vitali selector: the page isolates it because a Bernstein set is built by repeatedly choosing fresh points from a well-ordered development, not by one choice function on one fixed family.

Third, A free ultrafilter on $\mathbb{N}$, viewed as a subset of $\{0,1{\}}^{\mathbb{N}}$ and hence of $[0,1]$, is not Lebesgue measurable is intentionally one-directional. It proves what follows from being given a free ultrafilter, namely nonmeasurability; it does not produce a free ultrafilter. Under AC, take the family of cofinite subsets of $\mathbb{N}$. It is a proper filter (Filter on a set): $\mathbb{N}$ is cofinite, $\mathrm{\varnothing }$ is not because $\mathbb{N}$ is infinite, the complement of the intersection of two members is a finite union of finite sets, and a superset of a cofinite set is cofinite. The ultrafilter lemma, from the Axiom of Choice: every filter extends to an ultrafilter extends this filter to an ultrafilter. For every $n\in \mathbb{N}$ that extension contains $\mathbb{N}\setminus \{n\}$, which is absent from the principal ultrafilter at $n$; hence the extension is free (Ultrafilter). As The proved choice cost of the ultrafilter lemma explains, the local proof of the extension theorem uses AC (The Axiom of Choice).

These are upper bounds supplied by the local constructions. The page makes no claim that any displayed hypothesis is weakest possible. The arguments summarized here establish no lower bounds.