Formalizing ordinal partition relations using Isabelle/HOL

DOI10.1080/10586458.2021.1980464MaRDI QIDQ5094473zbMATH OpenOpenAlexFDO

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

Publication date 3 August 2022

Published in Experimental Mathematics (Search for Journal in Brave)

Copyright license Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International

Full work available at URL https://arxiv.org/abs/2011.13218

zbMATH Keywords

interactive theorem provingIsabelleproof assistantsset theoryordinal partition relations

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) Ordinal and cardinal numbers (03E10) Digital mathematics libraries and repositories (68V35)

Recommendations

• Mechanizing set theory. Cardinal arithmetic and the axiom of choice
• Cardinals in Isabelle/HOL
• Ordinals in HOL: transfinite arithmetic up to (and beyond) \(\omega _{1}\)
• scientific article; zbMATH DE number 7204430
• First steps towards a formalization of forcing

Cites work

• scientific article; zbMATH DE number 4039909 (Why is no real title available?)
• scientific article; zbMATH DE number 956479 (Why is no real title available?)
• scientific article; zbMATH DE number 3548474 (Why is no real title available?)
• scientific article; zbMATH DE number 3210032 (Why is no real title available?)
• scientific article; zbMATH DE number 3289430 (Why is no real title available?)
• A Theorem in the Partition Calculus
• A formal proof of the Kepler conjecture
• A formally verified proof of the central limit theorem
• A formulation of the simple theory of types
• A partition calculus in set theory
• A partition theorem for the complete graph on \(\omega^\omega\)
• A short proof of a partition theorem for the ordinal ωω
• A synthesis of the procedural and declarative styles of interactive theorem proving
• Analyzing Nash-Williams' partition theorem by means of ordinal types
• Borel sets and Ramsey's theorem
• Combinatorial set theory: Partition relations for cardinals
• Countable partition ordinals
• Formalizing an analytic proof of the prime number theorem
• From LCF to Isabelle/HOL
• Introduction to Ramsey space
• Isabelle/HOL. A proof assistant for higher-order logic
• Nitpick: a counterexample generator for higher-order logic based on a relational model finder
• On Fraissé's order type conjecture
• Partition Problems in Topology
• Partitioning pairs of countable ordinals
• Pinning countable ordinals
• Set theory. An introduction to independence proofs
• Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’
• Teilmengen von Mengen mit Relationen
• The Jordan Curve Theorem, Formally and Informally
• The new Quickcheck for Isabelle. Random, exhaustive and symbolic testing under one roof
• Three chapters of measure theory in Isabelle/HOL

Cited in

(9)

• The formal verification of the ctm approach to forcing
• Formalising Ordinal Partition Relations Using Isabelle/HOL
• Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis
• Formalizing calendars with the category of ordinals
• Cardinals in Isabelle/HOL
• Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
• Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL
• Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project
• A formalised theorem in the partition calculus

Describes a project that uses

Uses Software

• Nitpick
• Isabelle/HOL
• PVS
• HOL Light
• Automath
• QuickCheck
• Jordan
• kepler98
• Archive Formal Proofs

This page was built for publication: Formalizing 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 Q5094473)