Formalization of Forcing in Isabelle/ZF

Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf

Type: Book-Chapter

Publication Date: 2020-01-01

Citations: 3

DOI: https://doi.org/10.1007/978-3-030-51054-1_13

View Publication

Locations

Lecture notes in computer science - View

Similar Works

Action	Title	Year	Authors
+	Formalization of Forcing in Isabelle/ZF	2020	Emmanuel Gunther Miguel Pagano Pedro Sánchez Terraf
+	Formalization of Forcing in Isabelle/ZF	2020	Emmanuel Gunther Miguel Pagano Pedro Sánchez Terraf
+	The formal verification of the ctm approach to forcing	2022	Emmanuel Gunther Miguel Pagano Pedro Sánchez Terraf Matías Steinberg
+	First steps towards a formalization of Forcing	2018	Emmanuel Gunther Miguel Pagano Pedro Sánchez Terraf
+	First steps towards a formalization of Forcing	2018	Emmanuel Gunther Miguel Pagano Pedro Sánchez Terraf
+	First Steps Towards a Formalization of Forcing	2019	Emmanuel Gunther Miguel Pagano Pedro Sánchez Terraf
+	The Notion of Forcing	2011	Lorenz Halbeısen
+	Mechanization of Separation in Generic Extensions.	2019	Emmanuel Gunther Miguel Pagano Pedro Sánchez Terraf
+	Mechanization of Separation in Generic Extensions	2019	Emmanuel Gunther Miguel Pagano Pedro Sánchez Terraf
+	The Notion of Forcing	2017	Lorenz Halbeısen
+	Forcing revisited	2023	Toby Meadows
+	Fundamentos do forcing	2022	Pedro Galvão Schoueri
+	Constructibility and Class Forcing	2009	Sy D. Friedman
+ PDF Chat	Adding an Abstraction Barrier to ZF Set Theory	2020	Ciarán Dunne J. B. Wells Fairouz Kamareddine
+ PDF Chat	$\Sigma_n$-correct Forcing Axioms	2024	Ben Goodman
+ PDF Chat	A Characterization of Permutation Models in Terms of Forcing	2002	Eric Hall
+	The method of forcing	2019	Justin Tatch Moore
+	The method of forcing	2019	Justin Tatch Moore
+	PFA and guessing models	2016	Nam Trang
+	Extensional realizability for intuitionistic set theory	2020	Emanuele Frittaion Michael Rathjen

Works That Cite This (2)

Action	Title	Year	Authors
+	A formalised theorem in the partition calculus	2023	Lawrence C. Paulson
+ PDF Chat	Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis	2022	Lawrence C. Paulson

Works Cited by This (8)

Action	Title	Year	Authors
+	Mechanization of Separation in Generic Extensions.	2019	Emmanuel Gunther Miguel Pagano Pedro Sánchez Terraf
+ PDF Chat	A formal proof of the independence of the continuum hypothesis	2020	Jesse Michael Han Floris van Doorn
+	Studies in Logic and the Foundations of Mathematics	2008
+ PDF Chat	The foundation of a generic theorem prover	1989	Lawrence C. Paulson
+ PDF Chat	The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf	2003	Lawrence C. Paulson
+	A formalization of forcing and the unprovability of the continuum hypothesis	2019	Jesse Michael Han Floris van Doorn
+	First Steps Towards a Formalization of Forcing	2019	Emmanuel Gunther Miguel Pagano Pedro Sánchez Terraf
+	STUDIES IN LOGIC AND THE FOUNDATIONS OF MATHEMATICS	2014