
Ordinal
Partitions
Title: 
Ordinal Partitions 
Author:

Lawrence C. Paulson

Submission date: 
20200803 
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$ orderisomorphic 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_PartitionsAFP,
author = {Lawrence C. Paulson},
title = {Ordinal Partitions},
journal = {Archive of Formal Proofs},
month = aug,
year = 2020,
note = {\url{https://isaafp.org/entries/Ordinal_Partitions.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
Nash_Williams, ZFC_in_HOL 
