scientific article; zbMATH DE number 7649968
From MaRDI portal
Publication:5875427
DOI10.4230/LIPIcs.ITP.2019.19MaRDI QIDQ5875427
Jesse Michael Han, Floris van Doorn
Publication date: 3 February 2023
Full work available at URL: https://arxiv.org/abs/1904.10570
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
forcingformal verificationset theorycontinuum hypothesisBoolean-valued modelsinteractive theorem provingindependence proofsLean
Related Items (3)
Formalization of Forcing in Isabelle/ZF ⋮ Formalizing Galois Theory ⋮ The formal verification of the ctm approach to forcing
Uses Software
Cites Work
- GitHub
- Delimited control operators prove double-negation shift
- Set theory. An introduction to independence proofs
- Set theory for verification. I: From foundations to functions
- Formalization of the resolution calculus for first-order logic
- Stochastic \(\lambda\)-calculi: an extended abstract
- First steps towards a formalization of forcing
- The Lean Theorem Prover (System Description)
- The Relative Consistency of the Axiom of Choice — Mechanized Using Isabelle/ZF
- Introduction to Boolean Algebras
- Metamathematics, Machines and Gödel's Proof
- The Mathematical Development of Set Theory from Cantor to Cohen
- Boolean-Valued Semantics for the Stochastic λ-Calculus
- Nonexistence of Idempotent Means on Free Binary Systems
- Theorem Proving in Higher Order Logics
- A proof of the independence of the continuum hypothesis
- THE INDEPENDENCE OF THE CONTINUUM HYPOTHESIS
- The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis
- Mechanizing set theory. Cardinal arithmetic and the axiom of choice
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication:
