| Home |
| About |
| Submission Guidelines |
| Search |
| Download |
project summary
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. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|