一句话：为 Dickson 引理的一个特例构造显式界，并通过 realizability 从形式化证明中抽取该界。
本文研究 Dickson 引理的一个特例：对任意两个自然数函数 f、g，存在 i<j 使得 f_i≤f_j 且 g_i≤g_j。作者基于有限鸽巢原理给出组合论证，导出 descent lemma，并由此证明 Dickson 引理；随后猜测该界的形式，并用恰当的证明加以验证。论文还通过 realizability 从 descent lemma 证明的形式化中抽取出一个界，过程中使用了 non-computational quantifiers。结果给出了该特例中 i、j 的简单显式上界，并展示了从证明抽取计算内容的途径。
We consider a special case of Dickson's lemma: for any two functions $f,g$ on the natural numbers there are two numbers $i<j$ such that both $f$ and $g$ weakly increase on them, i.e., $f_i\le f_j$ and $g_i \le g_j$. By a combinatorial argument (due to the first author) a simple bound for such $i,j$ is constructed. The combinatorics is based on the finite pigeon hole principle and results in a descent lemma. From the descent lemma one can prove Dickson's lemma, then guess what the bound might be, and verify it by an appropriate proof. We also extract (via realizability) a bound from (a formalization of) our proof of the descent lemma. Keywords: Dickson's lemma, finite pigeon hole principle, program extraction from proofs, non-computational quantifiers.