{
  "id": "2011.13218",
  "version": "v1",
  "published": "2020-11-26T10:33:51.000Z",
  "updated": "2020-11-26T10:33:51.000Z",
  "title": "Formalising Ordinal Partition Relations Using Isabelle/HOL",
  "authors": [
    "Mirna Džamonja",
    "Angeliki Koutsoukou-Argyraki",
    "Lawrence C. Paulson FR"
  ],
  "categories": [
    "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 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 $m \\in \\mathbb{N}$, $\\omega^\\omega\\arrows(\\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 formalisation process. This project is also a demonstration of working with Zermelo-Fraenkel set theory in higher-order logic.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2020-11-26T10:33:51.000Z"
    }
  ],
  "analyses": {
    "subjects": [
      "03E05",
      "03B35",
      "68V20",
      "68V35"
    ],
    "keywords": [
      "formalising ordinal partition relations",
      "proof assistant isabelle/hol",
      "zermelo-fraenkel set theory",
      "research results",
      "infinitary combinatorics"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 0,
      "language": "en",
      "license": "arXiv",
      "status": "editable"
    }
  }
}