Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Ordinal Partitions

view this post on Zulip Email Gateway (Aug 18 2020 at 10:31):

From: Manuel Eberl <>
Ordinal Partitions
by Lawrence C. Paulson

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!



Last updated: Jul 15 2022 at 23:21 UTC