仅使用一次拉姆齐定理
逻辑
2020-07-24 v5
摘要
我们证明，在 RCA0 到高阶类型的直觉主义扩展中，无法通过一次典型应用 RT(2,2) 来证明 RT(2,4)，但当加入排中律后，这一结论不再成立。该论证使用了 Kohlenbach 的高阶逆数学公理化体系、与修正可归约性相关的结果，以及对 Weihrauch 可归约性的形式化。
引用
@article{arxiv.1611.03134,
title = {Using Ramsey's Theorem Once},
author = {Jeffry L. Hirst and Carl Mummert},
journal= {arXiv preprint arXiv:1611.03134},
year = {2020}
}
备注
Revised June 1, 2017. Added pointer to published article and included a corrigendum correcting Definition 1