Dickson 引理

一个坐标往下走的次数有限，除非它重新升高。把整列看作无限对象时，总能找到一个无限子列，使这个坐标以后不再下降；在第二个坐标上重复筛选，有限次后所有坐标同时有序。

这不是贪心地拿当前最小向量等待后继。两个向量可能一个横坐标小、另一个纵坐标小，互不支配；证明靠的是无限子列抽取。

一维引理与维数归纳 ​

任取自然数列 $(a_n)$。若某个值出现无限次，取常值子列。否则每个值只出现有限次；任意有限集合 $\{0,\dots ,M\}$ 总共也只出现有限次，于是可递归选取严格递增子列。

现在对 ${\mathbb{N}}^d$ 中的无限列，先按第一个坐标抽无限非减子列，再在它内部按第二坐标抽取，依次处理 $d$ 个坐标。后续抽取不会破坏前面坐标的非减性。最终任意前后两项都逐坐标可比，因此不存在无限坏序列。

证明没有给“读到第几项一定发现一对”的统一常数。即使 $d=1$，$N,N-1,\dots ,0$ 也是长度 $N+1$ 的坏序列。

手工删去多余阈值 ​

给出有限候选集

$(3,3)$ 被 $(2,2)$ 支配，$(1,6)$ 被 $(0,5)$ 支配，所以表示同一向上闭集的最小基为

逐对比较的直接算法对 $r$ 个 $d$ 维候选需要 $O(r^{2}d)$ 次坐标比较。Dickson 引理保证无限向上闭集也有有限基，却不从任意黑箱成员谓词自动算出它。

两种删掉假设的反例 ​

若允许整数，$(-n,0)$ 构成无限坏序列。若允许可数无穷多个坐标，单位向量 $e_0,e_1,\dots$ 互不支配，构成无限反链。有限维数和自然数下界各自排除一种不同失败。

在固定 ${\mathbb{N}}^2$ 中也可有任意大的有限反链，例如 $\{(i,N-i):0\le i\le N\}$。有限基不表示基的大小只由维数决定。

Petri 网公理库Petri 网Petri net · Place-transition net · P/T net以库所、变迁和 token 多重集建模资源、同步与真正并发，并研究可达标识。用库所 token 数组成 ${\mathbb{N}}^d$。其逐坐标顺序由本引理得到 wqo，再配合变迁的单调性，形成 良结构转移系统公理库良结构迁移系统Well structured transition system · WSTS把良拟序与迁移兼容性分开验证，以普通 Petri 网和零测试说明何时能安全地用大状态模拟小状态。。本引理只处理顺序；添加零测试后，顺序仍 wqo，迁移却可能失去单调性。

单项式 $x_1^{a_1}\cdots x_d^{a_d}$ 的整除恰对应指数向量逐坐标比较，因此单项式理想拥有有限个极小单项式生成元。相同的有限基机制在代数与验证中分别压缩生成元和坏状态阈值。