论文标题
迪克森引理的建设性组合
Constructive Combinatorics of Dickson's Lemma
论文作者
论文摘要
我们建设性地研究了迪克森引理的有限病例之间的关系。尽管它们有许多建设性的证据，但我们证明的新颖方面是提取相应的结合。我们提供了一些新的一步不可证实的结果，即“迪克森的引理的有限案例并未在一个步骤中证明是更强大的情况”的结果。此外，我们从建设性反向数学的角度研究了迪克森引理的无限病例。我们在Bishop的非正式建设性数学Bish中工作。
We study constructively the relations between the finite cases of Dickson's lemma. Although there are many constructive proofs of them, the novel aspect of our proofs is the extraction of a corresponding bound. We provide some new one-step unprovability results i.e., results of the form "a finite case of Dickson's lemma does not prove in one step a stronger case of it". Moreover, we study the infinite cases of Dickson's lemma from the point of view of constructive reverse mathematics. We work within Bishop's informal system of constructive mathematics BISH.
