Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice.

TL;DR

This paper details the mechanization of advanced set theory results, including cardinal arithmetic and the Axiom of Choice, within the Isabelle proof assistant, ensuring faithful mathematical representation.

Contribution

It introduces formal proofs of deep set theory results, such as cardinal multiplication and equivalences of AC, covering extensive theories and technical formulations.

Findings

Proved K*K = K for infinite cardinals.

Established equivalence of 7 formulations of Well-ordering Theorem.

Demonstrated 20 formulations of the Axiom of Choice.

Abstract

Fairly deep results of Zermelo-Frenkel (ZF) set theory have been mechanized using the proof assistant Isabelle. The results concern cardinal arithmetic and the Axiom of Choice (AC). A key result about cardinal multiplication is K*K = K, where K is any infinite cardinal. Proving this result required developing theories of orders, order-isomorphisms, order types, ordinal arithmetic, cardinals, etc.; this covers most of Kunen, Set Theory, Chapter I. Furthermore, we have proved the equivalence of 7 formulations of the Well-ordering Theorem and 20 formulations of AC; this covers the first two chapters of Rubin and Rubin, Equivalents of the Axiom of Choice, and involves highly technical material. The definitions used in the proofs are largely faithful in style to the original mathematics.