scientific article; zbMATH DE number 7649968

DOI10.4230/LIPICS.ITP.2019.19MaRDI QIDQ5875427zbMATH OpenFDO

Authors Jesse Michael Han, Floris van Doorn

Publication date 3 February 2023

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

zbMATH Keywords

Boolean-valued modelscontinuum hypothesisforcingformal verificationindependence proofsinteractive theorem provingLeanset theory

Mathematics Subject Classification ID

Cites work

• A proof of the independence of the continuum hypothesis
• Boolean-valued semantics for the stochastic \(\lambda \)-calculus
• Delimited control operators prove double-negation shift
• First steps towards a formalization of forcing
• Formalization of the resolution calculus for first-order logic
• GitHub
• scientific article; zbMATH DE number 5910780 (Why is no real title available?)
• scientific article; zbMATH DE number 3839951 (Why is no real title available?)
• scientific article; zbMATH DE number 5295821 (Why is no real title available?)
• scientific article; zbMATH DE number 5539366 (Why is no real title available?)
• scientific article; zbMATH DE number 4012604 (Why is no real title available?)
• scientific article; zbMATH DE number 3754682 (Why is no real title available?)
• scientific article; zbMATH DE number 1301853 (Why is no real title available?)
• scientific article; zbMATH DE number 1062123 (Why is no real title available?)
• scientific article; zbMATH DE number 1088050 (Why is no real title available?)
• scientific article; zbMATH DE number 2090314 (Why is no real title available?)
• scientific article; zbMATH DE number 3387345 (Why is no real title available?)
• Introduction to Boolean Algebras
• Mechanizing set theory. Cardinal arithmetic and the axiom of choice
• Metamathematics, Machines and Gödel's Proof
• Nonexistence of idempotent means on free binary systems
• Set theory for verification. I: From foundations to functions
• Set theory. An introduction to independence proofs
• Stochastic \(\lambda\)-calculi: an extended abstract
• The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis
• The higher infinite. Large cardinals in set theory from their beginnings.
• THE INDEPENDENCE OF THE CONTINUUM HYPOTHESIS
• The Lean theorem prover (system description)
• The Mathematical Development of Set Theory from Cantor to Cohen
• The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF
• Theorem Proving in Higher Order Logics

Cited in

(7)

• Some consequences from proper forcing axiom together with large continuum and the negation of Martin's axiom
• A Note on Shoenfield's Unramified Forcing
• A combinatorial forcing for coding the universe by a real when there are no sharps
• Formalization of Forcing in Isabelle/ZF
• Formalizing Galois theory
• The formal verification of the ctm approach to forcing
• A formalization of forcing and the unprovability of the continuum hypothesis

Describes a project that uses

Uses Software

• Isabelle/ZF
• Lean
• Archive Formal Proofs
• GitHub

This page was built for publication:

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