Formalising Ordinal Partition Relations Using Isabelle/HOL

DOI10.1080/10586458.2021.1980464MaRDI QIDQ6354634arXivFDO

Authors Mirna Džamonja, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson

Publication date 26 November 2020

Published in arXiv

Full work available at URL https://doi.org/10.1080/10586458.2021.1980464

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Partition relations (03E02) Other combinatorial set theory (03E05) Formalization of mathematics in connection with theorem provers (68V20)

arXiv classification

math.LO

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 ErdH{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 $minmathbbN$, $omeg{a}^{o}megaarrows(omeg{a}^{o}mega,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.

This page was built for publication: Formalising Ordinal Partition Relations Using Isabelle/HOL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6354634)