Ramsey's theorem, infinitary version

Title:	Ramsey's theorem, infinitary version
Author:	Tom Ridge
Submission date:	2004-09-20
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{Ramsey-Infinite-AFP, author = {Tom Ridge}, title = {Ramsey's theorem, infinitary version}, journal = {Archive of Formal Proofs}, month = sep, year = 2004, note = {\url{http://isa-afp.org/entries/Ramsey-Infinite.html}, Formal proof development}, ISSN = {2150-914x}, }
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.