良序定理

良序比全序多出“任何非空部分都有第一个元素”。全序只保证两元素可以比较，仍可能存在没有起点的下降方向；良序则允许不断选取当前剩余集合的最小元，从而把集合沿序数阶段逐步枚举。

定理并不说集合原有的自然次序已经良序。实数的通常大小关系不是良序，因为区间 $(0,1)$ 没有最小元素；良序定理只保证实数集上存在另一种可能极不直观的全序。对不可数集合，这个良序通常不能由简单公式或算法显式描述。

“存在一个良序”与“能够有效算出下一个元素”也不同。选择公理提供集合论存在性，却不自动给出可计算结构。把良序用于算法或构造时，必须额外说明表示方式和有效性。

自然数的通常次序是良序。整数的通常次序不是良序，因为整个 $\mathbb{Z}$ 没有最小元；但整数可以显式重新排列为

这个次序与通常大小无关，却使每个非空整数子集都有最先出现的元素。

有限二进制串的普通字典序可以是全序，却不是良序。在 $0<1$ 的约定下，有下降链

集合 $\{1,01,001,\dots \}$ 因而没有最小元素。仅检查“任意两串可比较”不足以判断良序。

良序也不同于一般偏序上的良基性。良基关系排除无限下降并保证非空子集有极小元，但极小元可能不唯一；良序还要求全序，所以极小元自动是唯一最小元。超限递归通常需要完整良序，而某些终止性证明只需良基关系。

每个良序集都与唯一的序数同构。因而良序定理等价于：每个集合都可以与某个序数建立双射。这个观点把任意集合纳入序数公理库序数Ordinal由属于关系良序且具有传递性的集合，表征良序的同构类型。和基数的统一框架，并允许比较任意两个集合的基数。

良序支持超限归纳公理库超限归纳法Transfinite induction若性质在每个序数处由所有更小序数上的成立推出，则它对全部序数成立。与超限递归公理库超限递归定理Transfinite recursion theorem允许用所有较早阶段的值唯一地定义序数长度函数的递归定理。。构造在每个阶段只依赖更早阶段，极限阶段再汇总此前结果；良序保证不存在尚未处理却没有第一个元素的残余部分。

在 ZF 中，良序定理、选择公理和Zorn 引理公理库佐恩引理Zorn's lemma若偏序集中每条链都有上界，则该偏序集存在极大元。互相等价。实际证明通常选择最符合问题形状的版本：递归构造偏好良序，极大对象存在性偏好 Zorn 引理，逐族选取元素则直接使用选择函数。