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.
  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.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License