The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF

DOI10.1007/978-3-540-69407-6_52MaRDI QIDQ3507465zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Lawrence C. Paulson

Publication date 19 June 2008

Published in Logic and Theory of Algorithms (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Axiom of choice and related propositions (03E25) Consistency and independence results (03E35)

Abstract: The proof of the relative consistency of the axiom of choice has been mechanized using Isabelle/ZF. The proof builds upon a previous mechanization of the reflection theorem. The heavy reliance on metatheory in the original proof makes the formalization unusually long, and not entirely satisfactory: two parts of the proof do not fit together. It seems impossible to solve these problems without formalizing the metatheory. However, the present development follows a standard textbook, Kunen's Set Theory, and could support the formalization of further material from that book. It also serves as an example of what to expect when deep mathematics is formalized.

Recommendations

• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
• ZF and the axiom of choice in some paraconsistent set theories
• On the computational content of the axiom of choice
• Independence of the induction principle and the axiom of choice in the pure calculus of constructions
• scientific article; zbMATH DE number 3861140
• scientific article; zbMATH DE number 3882419
• A realizability semantics for inductive formal topologies, Church's thesis and axiom of choice
• A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle
• Choice of primitives: A note on axiomatizing intuitionistic logic
• The axiom of choice in computability theory and reverse mathematics with a cameo for the continuum hypothesis

Cites work

• A compendium of continuous lattices in MIZAR
• Automated deduction in von Neumann-Bernays-Gödel set theory
• scientific article; zbMATH DE number 2090314 (Why is no real title available?)
• On computer-assisted proofs in ordinal number theory
• Set theory for verification. I: From foundations to functions
• Set theory for verification. II: Induction and recursion
• Set theory. An introduction to independence proofs
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf

Cited in

(6)

• *ZFC: An axiomatic * approach to nonstandard methods
• An Isomorphism Related to Gödel's Fundamental Operations
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
• scientific article; zbMATH DE number 7649968 (Why is no real title available?)
• Mechanizing set theory. Cardinal arithmetic and the axiom of choice
• Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis

Describes a project that uses

Uses Software

• Isabelle/ZF
• Isabelle

This page was built for publication: The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF

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