Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic

Authors Stefano Berardi, Silvia Steila

Thumbnail PDF


  • Filesize: 0.49 MB
  • 20 pages

Document Identifiers

Author Details

Stefano Berardi
Silvia Steila

Cite AsGet BibTex

Stefano Berardi and Silvia Steila. Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic. In 19th International Conference on Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 26, pp. 64-83, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)


We produce a first order proof of a famous combinatorial result, Ramsey Theorem for pairs and in two colors. Our goal is to find the minimal classical principle that implies the "miniature" version of Ramsey we may express in Heyting Arithmetic HA. We are going to prove that Ramsey Theorem for pairs with recursive assignments of two colors is equivalent in HA to the sub-classical principle Sigma-0-3-LLPO. One possible application of our result could be to use classical realization to give constructive proofs of some combinatorial corollaries of Ramsey; another, a formalization of Ramsey in HA, using a proof assistant. In order to compare Ramsey Theorem with first order classical principles, we express it as a schema in the first order language of arithmetic, instead of using quantification over sets and functions as it is more usual: all sets we deal with are explicitly defined as arithmetical predicates. In particular, we formally define the homogeneous set which is the witness of Ramsey theorem as a Delta-0-3-arithmetical predicate.
  • Formalization
  • Constructivism
  • Classical logic
  • Ramsey Theorem


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Yohji Akama, Stefano Berardi, Susumu Hayashi, and Ulrich Kohlenbach. An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles. In LICS, pages 192-201. IEEE Computer Society, 2004. Google Scholar
  2. G. Bellin. Ramsey interpreted: a parametric version of Ramsey’s Theorem. In AMS, editor, Logic and Computation: Proceedings of a Symposium held at Carnegie-Mellon University, volume 106, pages 17-37, 1990. Google Scholar
  3. Stefano Berardi and Ugo de' Liguoro. A Calculus of Realizers for EM1 Arithmetic. In Proceedings of CSL'08, Lecture Notes in Computer Science. Springer-Verlag, 2008. Google Scholar
  4. Giovanni Birolo. Interactive Realizability, Monads and Witness Extraction. PhD thesis, Doctoral School of Sciences and Innovative Technologies, 2012. PhD Thesis, Università di Torino. Google Scholar
  5. Peter A. Cholak, Carl G. Jockusch, and Theodore A. Slaman. On the strength of Ramsey’s theorem for pairs. Journal of Symbolic Logic, pages 1-55, 2001. Google Scholar
  6. C. T. Chong, Theodore A. Slaman, and Yue Yang. The Metamathematics of Stable Ramsey’s Theorem for Pairs. preprint, 2012. Google Scholar
  7. Thierry Coquand. A direct proof of Ramsey’s Theorem. Author’s website, 2011. Google Scholar
  8. Denis R. Hirschfeldt. Slicing the Truth: On the Computability Theoretic and Reverse Mathematical Analysis of Combinatorial Principles. Author’s webpage. Google Scholar
  9. Hajime Ishihara. Reverse mathematics in Bishop’s constructive mathematics. Philosophia Scientiae, Cahier special, 6:43-59, 2006. Google Scholar
  10. Carl G. Jockusch Jr. Ramsey’s Theorem and Recursion Theory. J. Symb. Log., 37(2):268-280, 1972. Google Scholar
  11. Ulrich Kohlenbach and Alexander Kreuzer. Term extraction and Ramsey’s theorem for pairs. J. Symb. Log., 77(3):853-895, 2012. Google Scholar
  12. Jiayi Liu. RT₂² does not imply WKL₀. J. Symb. Log., 77(2):609-620, 2012. Google Scholar
  13. Joseph R. Mileti. Partition theorems and computability theory. Technical Report 3, Department of Mathematics, University of Chicago, 2005. Google Scholar
  14. Paulo Oliva and Thomas Powell. A Constructive Interpretation of Ramsey’s Theorem via the Product of Selection Functions. CoRR, abs/1204.5631, 2012. Google Scholar
  15. F. P. Ramsey. On a problem in formal logic. Proc. London Math. Soc., 30:264-286, 1930. Google Scholar
  16. Stephen George Simpson. Subsystems of second order arithmetic. Perspectives in logic. Association for symbolic logic, New York, 2009. 2nd edition. Google Scholar
  17. Theodore A. Slaman. Σ_n-bounding and Δ_n-induction. Proc. Amer. Math. Soc., 132:2449-2456, 2004. Google Scholar