License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2013.64
URN: urn:nbn:de:0030-drops-46269
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2014/4626/
Go to the corresponding LIPIcs Volume Portal

Berardi, Stefano ; Steila, Silvia

Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic

pdf-format:
5.pdf (0.5 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{berardi_et_al:LIPIcs:2014:4626,
  author =	{Stefano Berardi and Silvia Steila},
  title =	{{Ramsey Theorem for Pairs As a Classical Principle in Intuitionistic Arithmetic}},
  booktitle =	{19th International Conference on Types for Proofs and Programs (TYPES 2013)},
  pages =	{64--83},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-72-9},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{26},
  editor =	{Ralph Matthes and Aleksy Schubert},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2014/4626},
  URN =		{urn:nbn:de:0030-drops-46269},
  doi =		{10.4230/LIPIcs.TYPES.2013.64},
  annote =	{Keywords: Formalization, Constructivism, Classical logic, Ramsey Theorem}
}

Keywords: Formalization, Constructivism, Classical logic, Ramsey Theorem
Collection: 19th International Conference on Types for Proofs and Programs (TYPES 2013)
Issue Date: 2014
Date of publication: 25.07.2014

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI