Ordinal Partitions

Title:	Ordinal Partitions
Author:	Lawrence C. Paulson
Submission date:	2020-08-03
Abstract:	The theory of partition relations concerns generalisations of Ramsey's theorem. For any ordinal $\alpha$, write $\alpha \to (\alpha, m)^2$ if for each function $f$ from unordered pairs of elements of $\alpha$ into $\{0,1\}$, either there is a subset $X\subseteq \alpha$ order-isomorphic to $\alpha$ such that $f\{x,y\}=0$ for all $\{x,y\}\subseteq X$, or there is an $m$ element set $Y\subseteq \alpha$ such that $f\{x,y\}=1$ for all $\{x,y\}\subseteq Y$. (In both cases, with $\{x,y\}$ we require $x\not=y$.) In particular, the infinite Ramsey theorem can be written in this notation as $\omega \to (\omega, \omega)^2$, or if we restrict $m$ to the positive integers as above, then $\omega \to (\omega, m)^2$ for all $m$. This entry formalises Larson's proof of $\omega^\omega \to (\omega^\omega, m)^2$ along with a similar proof of a result due to Specker: $\omega^2 \to (\omega^2, m)^2$. Also proved is a necessary result by Erdős and Milner: $\omega^{1+\alpha\cdot n} \to (\omega^{1+\alpha}, 2^n)^2$.
BibTeX:	@article{Ordinal_Partitions-AFP, author = {Lawrence C. Paulson}, title = {Ordinal Partitions}, journal = {Archive of Formal Proofs}, month = aug, year = 2020, note = {\url{https://isa-afp.org/entries/Ordinal_Partitions.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Nash_Williams, ZFC_in_HOL
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.

Proof outline
Proof document

Browse theories

Download this entry