From: Manuel Eberl <eberlm@in.tum.de>

Ordinal Partitions

by Lawrence C. Paulson

https://www.isa-afp.org/entries/Ordinal_Partitions.html

The theory of partition relations concerns generalisations of Ramsey’s

theorem. For any ordinal α, write α → (α, m)² if for each function f

from unordered pairs of elements of α into {0, 1}, either there is a

subset X ⊆ α order-isomorphic to α such that f {x, y} = 0 for all {x, y}

⊆ X, or there is an m element set Y ⊆ α such that f {x, y} = 1 for all

{x, y} ⊆ Y. (In both cases, with {x, y} we require x ≠ y.)

In particular, the infinite Ramsey theorem can be written in this

notation as ω → (ω, ω)², or if we restrict m to the positive integers as

above, then ω → (ω, m)² for all m.

This entry formalises Larson’s proof of ω^ω → (ω^ω, m)² along with a

similar proof of a result due to Specker: ω² → (ω², m)² . Also proved is

a necessary result by Erdős and Milner: ω^(1+α·n) → (ω^(1+α), 2^n)².

These examples demonstrate the use of Isabelle/HOL to formalise advanced

results that combine ZF set theory with basic concepts like lists and

natural numbers.

It is certainly nice to see more and more set theory in Isabelle,

although I for one don't understand much of it (yet). And someone is

certainly putting the AFP's new LaTeX support to good use!

Enjoy,

Manuel

Last updated: Sep 28 2021 at 19:14 UTC