
Ramsey's
theorem,
infinitary
version
Title: 
Ramsey's theorem, infinitary version 
Author:

Tom Ridge

Submission date: 
20040920 
Abstract: 
This formalization of Ramsey's theorem (infinitary version) is taken from Boolos and Jeffrey, Computability and Logic, 3rd edition, Chapter 26. It differs slightly from the text by assuming a slightly stronger hypothesis. In particular, the induction hypothesis is stronger, holding for any infinite subset of the naturals. This avoids the rather peculiar mapping argument between kj and aikj on p.263, which is unnecessary and slightly mars this really beautiful result. 
BibTeX: 
@article{RamseyInfiniteAFP,
author = {Tom Ridge},
title = {Ramsey's theorem, infinitary version},
journal = {Archive of Formal Proofs},
month = sep,
year = 2004,
note = {\url{http://isaafp.org/entries/RamseyInfinite.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Status: [ok] 
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.

