良序定理

形式陈述 ​

良序是满足以下条件的全序理路全序Total order · Linear order任意两个元素都可比较的偏序。 $(X,⪯)$：每个非空子集 $A\subseteq X$ 都存在最小元素 $a_0\in A$，即

良序定理断言：对任意集合 $X$，都存在某个关系 $⪯$，使 $(X,⪯)$ 成为良序集。

在 ZF 集合论中，良序定理与选择公理理路选择公理Axiom of choice · AC把任意集合族中逐个存在的元素同时汇成一个选择函数的公理。等价；在默认采用 ZFC 的语境中，它因而是一条定理。等价性意味着，不能把“任意集合可良序”视为完全不带选择强度的普通排序事实。

证明轮廓：选择怎样产生良序 ​

先在 ZF 中给任意集合 $X$ 找到一个不能单射进 $X$ 的序数界。所有对子集 $B\subseteq X$ 给出良序的关系 $R$，都可以作为有序对 $(B,R)$ 收集在集合 $\mathcal{P}(X)\times \mathcal{P}(X\times X)$ 中。每个已有良序都对应唯一的序数型理路序数Ordinal由属于关系良序且具有传递性的集合，表征良序的同构类型。；替换公理因此把这些序数型收集成一个集合 $H$。这里使用的是已有良序的序型结论，整个构造无需选择公理。令

每个 $\alpha \in H$ 都小于 $\eta$。如果有单射 $\eta \to X$，把 $\eta$ 的良序搬到其像上，就会得到 $X$ 的一个良序子集，其序数型为 $\eta$，即 $\eta \in H$，矛盾。这给出了所需的 Hartogs 界。[1,2]

现在假设选择公理理路选择公理Axiom of choice · AC把任意集合族中逐个存在的元素同时汇成一个选择函数的公理。。空集已有空良序；以下取 $X\ne \varnothing$，固定一个选择函数 $c:\mathcal{P}(X)\setminus \{\varnothing \}\to X$。用超限递归定理理路超限递归定理Transfinite recursion theorem允许用所有较早阶段的值唯一地定义序数长度函数的递归定理。在所有 $\alpha <\eta$ 上定义

第二分支让规则在取完元素后仍有唯一值，因此递归确实是一条处处规定好的规则。只要尚未取完，下一项就不同于全部较早项。如果所有 $\alpha <\eta$ 都还有剩余元素，$\alpha \mapsto a_{\alpha }$ 就是 $\eta \to X$ 的单射，与 Hartogs 界矛盾。故有最早的 $\gamma <\eta$ 使剩余集合为空；在此前各项互异，且此时已经取遍 $X$，所以 $\alpha \mapsto a_{\alpha }$ 给出 $\gamma \to X$ 的双射。把序数 $\gamma$ 的良序搬到 $X$，便证明了良序定理。[2]

反向假设任意集合可良序。对一族非空集合 $\mathcal{A}$，只需给它们的并集 $U=\bigcup \mathcal{A}$ 选一个良序，再把每个 $A\in \mathcal{A}$ 的最小元定义为 $c(A)$。最小元已经唯一，这个规则便给出选择函数；若 $\mathcal{A}$ 为空，取空函数即可。由此得到 ZF 上的两个方向，而没有在 Hartogs 界或递归定理中预先使用待证的良序存在性。