Formalizing Ordinal Partition Relations Using Isabelle/HOL


Type
Article
Change log
Abstract

This is an overview of a formalisation 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\H{o}s--Milner, Specker, Larson and Nash-Williams, leading to Larson's proof of the unpublished result by E.C. Milner asserting that for all mN, ωω\arrows(ωω,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 formalisation process. This project is also a demonstration of working with Zermelo-Fraenkel set theory in higher-order logic.

Description
Keywords
Ordinal partition relations, set theory, interactive theorem proving, Isabelle, proof assistants
Journal Title
Experimental Mathematics
Conference Name
Journal ISSN
1058-6458
1944-950X
Volume Title
Publisher
Informa UK Limited
Sponsorship
European Research Council (742178)