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

DOI10.1007/978-3-540-69407-6_52zbMath1142.03332DBLPconf/cie/Paulson08arXiv2104.12674OpenAlexW2154189201WikidataQ57382628 ScholiaQ57382628MaRDI QIDQ3507465

Lawrence Charles 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) Consistency and independence results (03E35) Axiom of choice and related propositions (03E25)

Related Items (1)

Unnamed Item

Uses Software

• Isabelle
• Isabelle/ZF

Cites Work

• Unnamed Item
• Set theory. An introduction to independence proofs
• Automated deduction in von Neumann-Bernays-Gödel set theory
• On computer-assisted proofs in ordinal number theory
• Set theory for verification. I: From foundations to functions
• A compendium of continuous lattices in MIZAR
• Set theory for verification. II: Induction and recursion
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf

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