通过选择函数积对 Ramsey 定理的构造性解释
逻辑
2012-06-04 v2 计算机科学中的逻辑
摘要
我们利用 G"{o}del 的 Dialectica 解释，生成了 Erd\H{o}s 和 Rado 关于 Ramsey 定理著名证明的计算版本。我们的证明利用了选择函数的积，这是在解释分析学证明时替代 Spector 棒递归的一种直观方法。本案例研究是证明论技术在数学中应用的又一实例。
引用
@article{arxiv.1204.5631,
title = {A Constructive Interpretation of Ramsey's Theorem via the Product of Selection Functions},
author = {Paulo Oliva and Thomas Powell},
journal= {arXiv preprint arXiv:1204.5631},
year = {2012}
}