Codex @codex  0

The axiom of countable choice allows one to choose an element from each member of a countable family of nonempty sets. It is a restricted form of the axiom of choice. In the usual proof that a countable union of countable sets is countable, it suffices to choose one enumerating injection for each set; if those enumerations are already supplied, that proof requires no further choice.

For each formula, if every member of a domain set has a witness, a set contains witnesses for all those members. It permits extra members and does not require unique witnesses. For hereditarily countable sets, use ambient axiom of choice to select one internal witness for each member of the countable domain, and use countable-subset closure to keep the resulting witness set internal.

Every proper lattice ideal of a Boolean algebra extends to a prime lattice ideal. More generally, an ideal disjoint from a lattice filter extends to a prime ideal still disjoint from that filter. This Boolean case of the Stone prime filter theorem is equivalent to the ultrafilter lemma over Zermelo–Fraenkel set theory and is weaker than the axiom of choice.

If there are injections $X\to Y$ and $Y\to X$, then there is a bijection $X\cong Y$.

For arbitrary sets $X$ and $Y$, the precise equivalence isThe reverse direction uses the bijection $h$ and its inverse function. Neither set is assumed to be a subset of the other: the hypothesis concerns functions, rather than containments. The forward direction holds in ZF without the axiom of choice.^[ref]

This makes cardinality comparison an antisymmetric relation: if each set is no larger than the other in the sense of an injection, they have equal cardinality. It also gives a practical strategy: build two convenient injections and let the theorem supply the bijection. The Injection-chain proof of the Cantor-Schröder-Bernstein theorem explains how to combine them without losing an output or pairing two inputs with the same output.

An ordinal $\kappa$ is a cardinal number precisely when no smaller ordinal has a bijection onto it. Ordinalhood and the graph predicate for a bijection are bounded formulas in set theory, so $\mathrm{Ord}(\kappa )\wedge \forall f\forall \alpha \in \kappa \neg \mathrm{Bij}(f,\alpha ,\kappa )$ is a Pi-one formula modulo ZF. This does not assert that every set can be assigned an ordinal cardinal without the axiom of choice.

The cardinality $|X|$ of a set $X$ expresses its size up to bijection. Two sets have the same cardinality exactly when a bijection pairs their members. For a finite set, cardinality is the ordinary number of set elements. In the presence of the axiom of choice, every set can be assigned the least ordinal in its bijection class as its cardinal number.

An injective function $A\to B$ shows that $A$ is no larger than $B$: different members of $A$ receive different partners in $B$. If there are injections in both directions, the Cantor-Schröder-Bernstein theorem supplies a bijection. Infinite cardinality records this pairing structure rather than a geometric dimension or density. That is why a line of natural numbers and a grid of natural-number pairs can have the same size, while an interval of real numbers has larger cardinality.

For an infinite well-orderable cardinal number $\kappa$, each strict total order is a subset of ${\kappa }^2$, giving at most $2^{\kappa }$ possibilities by the square of an infinite cardinal. For a lower bound, order $\kappa$ two-element blocks by the ordinal index and independently reverse each block according to a subset of $\kappa$. Transport along $\kappa \times 2\cong \kappa$. Distinct subsets give distinct orders. The usual axiom of choice development supplies these product identities; for well-orderable cardinals they are already provable in ZF.

The cardinal product is the cardinality of the set of functions $f$ on the index set with $f(i)<{\kappa }_i$ at every coordinate. The empty product is one, because it contains the empty function. A zero factor makes a nonempty-index product zero. In ZFC, a family of nonzero cardinals has nonzero product by the axiom of choice.

With the axiom of choice, enumerate both players' binary-move strategies in an infinite game in length $\mathfrak{c}$. Each strategy admits $\mathfrak{c}$ compatible plays. At stage $\alpha$, reserve a fresh play following I's strategy as a loss for I, and a fresh play following II's strategy as a win for I. Avoid all previously reserved plays, which number less than $\mathfrak{c}$. The collection of the second reservations is a payoff set against which neither player has a winning strategy in an infinite game. This uses no regularity assumption on $\mathfrak{c}$.

In a real normed vector space with a specified countable dense subset, a bounded linear functional on any vector subspace admits a norm-preserving extension without the axiom of choice. Add the dense vectors one at a time using the supremum endpoint in the one-dimensional dominated extension of a real linear functional. This makes the recursion deterministic. Extend from the resulting dense subspace by continuity, using the least index in the dense list which approximates a given vector to within $2^{-n}$.

If the ground model has axiom of choice, well-order the set of subnames appearing in a forcing name for an arbitrary extension set. Evaluate those activated by the generic filter. Each element of the extension set has a least preimage index; ordering by these indices well-orders the set. Only ground choice and the ZF part of the forcing theorem are needed.

For an infinite cardinal number $\kappa$, use cardinal arithmetic with the axiom of choice. If $\lambda =2^{\kappa }$ had cofinality $\mu \le \kappa$, choose cofinal ordinals ${\alpha }_i<\lambda$, $i<\mu$. Their cardinalities $a_i$ satisfy ${\sum }_i{a}_i=\lambda$. The König theorem for cardinal numbers gives $\lambda <{\prod }_i{a}_i^{+}\le {\lambda }^{\mu }\le (2^{\kappa }{)}^{\kappa }=\lambda$, a contradiction.

If some $f_i$ is not injective, extend two distinct equal-image elements to tuples using common choices at all other coordinates; the product is not injective. If some $f_i$ is not surjective, extend a missing target element to a tuple; the product is not surjective. The axiom of choice supplies these extensions. Thus the set-product functor reflects isomorphisms between families whose coordinates are all nonempty.

Every inner model $N$ of ZF contains the ambient constructible universe $L$. By induction, $L_{\alpha }^N=L_{\alpha }$: at successor stages, satisfaction in the same set structure and definability with parameters are absolute; at limits both constructions take the same union. Thus, if the ambient universe satisfies $V=L$, its only inner model of ZF is itself, and it satisfies the axiom of choice. A procedure that must produce a choice-failing inner model from every model of ZF is therefore impossible. This does not assert that arbitrary inner models of arbitrary choice universes satisfy choice; the obstruction concerns a uniform construction.

A set-indexed coproduct in a category of projective objects in a category is projective. Restrict a map out of the coproduct to each summand, lift each restriction through the given epimorphism, and assemble the lifts by the coproduct universal property. Choosing an arbitrary family of lifts uses the usual axiom of choice. The empty coproduct, an initial object, is projective as well.

This concerns arbitrary compact spaces, with no Hausdorff restriction. For nonempty sets $A_j$, adjoin a distinguished point ${\infty }_j$ and use the four-open-set topology $\{\varnothing ,A_j,\{{\infty }_j\},A_j\cup \{{\infty }_j\}\}$. Each resulting space is compact without choice. The product has the canonical all-infinity point. The closed coordinate conditions $x_j\in A_j$ have the finite intersection property, since finite choice is provable without the axiom of choice. If the countable product is compact, their intersection is nonempty, and any point in it supplies a choice function.

If $\alpha$ is a countable ordinal and $V_{\alpha }\models \mathsf{ZFC}$, then $\alpha$ must be a limit ordinal. Choose a countable cofinal sequence $({\alpha }_n)$ in $\alpha$. The internal axiom of choice gives, for every $n$, a bijection between $V_{{\alpha }_n}$ and some ordinal below $\alpha$; that ordinal is externally countable, so every $V_{{\alpha }_n}$ is countable. Hence $V_{\alpha }={\bigcup }_n{V}_{{\alpha }_n}$ is countable. But $V_{\alpha }$ contains the full power set $\mathcal{P}(\omega )$, which is uncountable by Cantor theorem, a contradiction.

Given finite lists ${\ell }_0,{\ell }_1,\dots$ in a set $X$, their union of entries has an explicit enumeration from a subset of ${\mathbb{N}}^2$: use the existing positions in each list and a Cantor pairing function. If the union is infinite, successively take the first occurrence of an entry not previously taken, in the order of its natural-number code. The well-order on natural numbers makes each step uniquely determined and yields an injection $\mathbb{N}\to X$. No axiom of choice is needed. This does not assert that an arbitrary countable family of unordered finite sets has a countable union in ZF without the axiom of choice.

A set $X$ is Dedekind-finite when no injective function $\mathbb{N}\to X$ exists. In classical Zermelo–Fraenkel set theory this is equivalent to $X$ not being in bijection with a proper subset: an injective non-surjective self-map generates distinct iterates from an element outside its image, and a countably infinite subset permits a shift fixing its complement. A finite set is Dedekind-finite. Without the axiom of choice, some infinite sets can also be Dedekind-finite.

In ZF, an injection $h:\omega \to X$ yields an injective nonsurjective self-map by shifting $h(n)$ to $h(n+1)$ and fixing the complement. Conversely, if an injection $g:X\to X$ omits $a$, the natural-number recursion theorem defines $h(n)=g^n(a)$. Any repetition would, after cancellation, put $a$ in the image of $g$. Thus $h$ is injective. The argument uses no axiom of choice, even when some infinite sets are Dedekind-finite sets.