The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf

DOI10.1112/S1461157000000449zbMath1053.03009OpenAlexW2017971007WikidataQ114008993 ScholiaQ114008993MaRDI QIDQ4827615

Lawrence Charles Paulson

Publication date: 18 November 2004

Published in: LMS Journal of Computation and Mathematics (Search for Journal in Brave)

Full work available at URL: http://www.lms.ac.uk/jcm/6/lms2003-001/

zbMATH Keywords

Isabelle/ZFaxiom of choicerelative consistencymechanization

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

A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle, Formalization of Forcing in Isabelle/ZF, Ordinal arithmetic: Algorithms and mechanization, Computational logic: its origins and applications, A formalised theorem in the partition calculus, The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF, The formal verification of the ctm approach to forcing, Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis, The Isabelle Framework, From LCF to Isabelle/HOL, First steps towards a formalization of forcing

Uses Software

• Isabelle
• Isabelle/ZF

Cites Work

• Unnamed Item
• Unnamed Item
• Set theory. An introduction to independence proofs
• Set theory for verification. I: From foundations to functions
• Isabelle. A generic theorem prover
• Automated deduction - CADE-18. 18th international conference, Copenhagen, Denmark, July 27--30, 2002. Proceedings
• The foundation of a generic theorem prover
• Set theory for verification. II: Induction and recursion
• The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis
• Mechanizing set theory. Cardinal arithmetic and the axiom of choice