Dickson 引理的一个界
逻辑
2019-03-14 v2
摘要
我们考虑 Dickson 引理的一个特例：对于自然数上的任意两个函数 ，存在两个数 ，使得 和 在其上均弱递增，即 且 。通过组合论证（由第一作者提出），构建了此类 的一个简单界。该组合学基于有限鸽巢原理，并导出了一个下降引理。从下降引理可以证明 Dickson 引理，进而猜测界的形式，并通过适当的证明进行验证。我们还通过可实现性从下降引理的证明（及其形式化）中提取了一个界。关键词：Dickson 引理，有限鸽巢原理，从证明中提取程序，非计算量词。
引用
@article{arxiv.1503.03325,
title = {A bound for Dickson's lemma},
author = {Josef Berger and Helmut Schwichtenberg},
journal= {arXiv preprint arXiv:1503.03325},
year = {2019}
}