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

DOI10.1112/S1461157000000449zbMATH Open1053.03009OpenAlexW2017971007WikidataQ114008993 ScholiaQ114008993MaRDI QIDQ4827615FDOQ4827615

Authors: Lawrence C. 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/

Recommendations

• The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF
• Mechanizing set theory. Cardinal arithmetic and the axiom of choice
• Mathematical Knowledge Management
• First steps towards a formalization of forcing
• Experimenting with Isabelle in ZF set theory

zbMATH Keywords

axiom of choicerelative consistencymechanizationIsabelle/ZF

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (12)

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

Uses Software

• Isabelle
• Isabelle/ZF

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 Q4827615)