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$.
  author  = {Lawrence C. Paulson},
  title   = {Ordinal Partitions},
  journal = {Archive of Formal Proofs},
  month   = aug,
  year    = 2020,
  note    = {\url{http://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.