拉姆齐定理的直觉主义版本（意大利语版本）
摘要
针对数对的 Ramsey 定理 [6] 是直觉主义可证但非经典可证的：它等价于一个次经典原则 [2]。在本文中，我们证明 Ramsey 定理可以重述为一种直觉主义可证的形式，该形式具有信息量（或至少不包含否定），并且在经典逻辑下与原定理等价。与以往同类工作相比，我们既未使用 [1]、[5] 中的“无反例”方法，也未像 [4] 那样向直觉主义添加新原则。我们主张，该直觉主义版本的 Ramsey 定理可用于替换 [3] 中程序收敛性证明里的 Ramsey 定理。[1] Gianluigi Bellin. Ramsey interpreted: a parametric version of Ramsey Theorem. In AMS, editor, Logic and Computation: Proceedings of a Symposium held at Carnegie Mellon University, volume 106. [2] Stefano Berardi, Silvia Steila, Ramsey Theorem for pairs as a classical principle in Intuitionistic Arithmetic, Submitted to the proceedings of Types 2013 in Toulouse. [3] Byron Cook, Abigail See, Florian Zuleger, Ramsey vs. Lexicographic Termination Proving, LNCS 7795, 2013, Springer Berlin Heidelberg. [4] Thierry Coquand. A direct proof of Ramsey Theorem. [5] Paulo Oliva and Thomas Powell. A Constructive Interpretation of Ramsey Theorem via the Product of Selection Functions. CoRR, arXiv:1204.5631, 2012. [6] F. P. Ramsey. On a problem in formal logic. Proc. London Math. Soc., 1930.
引用
@article{arxiv.1401.2515,
title = {An intuitionistic version of Ramsey Theorem (italian version)},
author = {Stefano Berardi},
journal= {arXiv preprint arXiv:1401.2515},
year = {2014}
}
备注
in Italian