First steps towards a formalization of forcing
From MaRDI portal
Publication:2333671
DOI10.1016/j.entcs.2019.07.008zbMath1434.03029arXiv1807.05174OpenAlexW2969850793WikidataQ113317457 ScholiaQ113317457MaRDI QIDQ2333671
Miguel Pagano, Pedro Sánchez Terraf, Emmanuel Gunther
Publication date: 13 November 2019
Full work available at URL: https://arxiv.org/abs/1807.05174
Mechanization of proofs and logical operations (03B35) Consistency and independence results (03E35) Formalization of mathematics in connection with theorem provers (68V20)
Related Items (3)
Formalization of Forcing in Isabelle/ZF ⋮ The formal verification of the ctm approach to forcing ⋮ Unnamed Item
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Computer theorem proving in mathematics
- Equivalents of the axiom of choice. 2nd ed
- Theorem proving in higher order logics. 12th international conference, TPHOLs '99. Nice, France, September 14--17, 1999. Proceedings
- Set theory for verification. II: Induction and recursion
- Cardinals in Isabelle/HOL
- Partizan Games in Isabelle/HOLZF
- The Isabelle Framework
- The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
- A FORMAL PROOF OF THE KEPLER CONJECTURE
- Homotopy Type Theory: Univalent Foundations of Mathematics
- THE INDEPENDENCE OF THE CONTINUUM HYPOTHESIS
- Consistency of the Continuum Hypothesis. (AM-3)
- Formalization of the fundamental group in untyped set theory using auto2
- Mechanizing set theory. Cardinal arithmetic and the axiom of choice
This page was built for publication: First steps towards a formalization of forcing
