Formalizing Ordinal Partition Relations Using Isabelle/HOL

ABSTRACT

This is an overview of a formalization project in the proof assistant Isabelle/HOL of a number of research results in infinitary combinatorics and set theory (more specifically in ordinal partition relations) by Erdős–Milner, Specker, Larson and Nash-Williams, leading to Larson’s proof of the unpublished result by E.C. Milner asserting that for all $m\in \mathbb{N}$, ${\omega }^{\omega }\to ({\omega }^{\omega },m)$. This material has been recently formalised by Paulson and is available on the Archive of Formal Proofs; here we discuss some of the most challenging aspects of the formalization process. This project is also a demonstration of working with Zermelo–Fraenkel set theory in higher-order logic.

KEYWORDS:

• Ordinal partition relations
• set theory
• interactive theorem proving
• Isabelle
• proof assistants

AMS 2020 SUBJECT CLASSESMATHEMATICS SUBJECT CLASSIFICATION:

• 03E02
• 03E05
• 03E10
• 03B35
• 68V20
• 68V35

Correction Statement

This article has been republished with minor changes. These changes do not impact the academic content of the article.

Acknowledgments

All three authors thank the London Mathematical Society for support through their Grant SC7-1920-11. Thanks to Stevo Todorčević for advice and to the anonymous reviewers for their helpful feedback on the first submitted version of this article.

Conflict of Interest

No potential conflict of interest was reported by the author(s).

Notes

1 The word generalization deserves explanation. It is often said, including by Larson [28], that Nash-Williams theorem is a Ramsey-type statement, however this does not appear immediately. Namely, Ramsey’s theorem applies to colorings of pairs of elements of ω, while the Nash-Williams theorem applies to coloring singletons in a thin set, not the pairs of the elements of it. The crude analogue of the theorem applying to pairs of elements of a thin set is easily seen to be false, while however there exists a finer version of Nash-Williams theorem using fronts and the shift-initial segment relation, obtaining a result that does apply to pairs and n-tuples of the elements of a thin set.

2 For readers familiar with forcing: we may see these definitions as coming from a forcing notion consisting of the pairs (s, B) with $\max (s)<\min (B)$ where the extension is given by $(s,B)\le (t,C)$ if $s⊑t,C\subseteq B$ and $t\setminus s\subseteq B$. This resembles Prikry or Mathias forcing. In Hodkinson’s notes such pairs are called Prikry pairs and the idea of using them in combinatorics comes from the Galvin-Prikry partition theorem [15].

3 An undefined value is simply regarded as underspecified. It has the expected type, and we always have $(ϵx.\varphi )=(ϵx.\varphi )$ for example.

4 {Sup S<.} is the set of integers greater than $\max S$

5 Which is even executable, if N is effectively enumerable.

6 Conceptually the same as thin_set, it is a property of sets of lists, not sets of sets.

7 Thus it seems that Larson should have written $l<2(j+1)$. This seems to be the only error in her paper.

Additional information

Funding

Angeliki Koutsoukou-Argyraki and Lawrence C. Paulson thank the ERC for their support through the Advanced Grant ALEXANDRIA (Project GA 742178). Mirna Džamonja’s research was supported by the GAČR project EXPRO 20-31529X and RVO: 67985840 at the Czech Academy of Sciences; she received funding from the European’s Union Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No 1010232.