Mechanizing set theory. Cardinal arithmetic and the axiom of choice

DOI10.1007/BF00283132zbMATH Open0868.03005OpenAlexW2073127449WikidataQ114018501 ScholiaQ114018501MaRDI QIDQ5961491FDOQ5961491

Krzysztof Grąbczewski, Lawrence C. Paulson

Publication date: 3 August 1997

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00283132

zbMATH Keywords

axiom of choiceproof assistantcardinal arithmeticZermelo-Fraenkel set theoryIsabelle Logical Framework

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Ordinal and cardinal numbers (03E10) Axiom of choice and related propositions (03E25)

Cited In (13)

• First steps towards a formalization of forcing
• Explaining Gabriel-Zisman localization to the computer
• Computer proofs about finite and regular sets: The unifying concept of subvariance.
• The formal verification of the ctm approach to forcing
• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
• Title not available (Why is that?)
• Mathematical Knowledge Management
• Mechanizing Nonstandard Real Analysis
• 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

• Coq
• Isabelle
• IMPS

   Recommendations

• The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf 👍 👎
• The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF 👍 👎
• Set theory for verification. I: From foundations to functions 👍 👎
• Mathematical Knowledge Management 👍 👎

This page was built for publication: Mechanizing set theory. Cardinal arithmetic and the axiom of choice

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