2020/01/27 by Gunther, Emmanuel, Pagano, Miguel, Terraf, Pedro Sánchez
#03B35 (Primary) 03E40 #03B70 #68T15 (Secondary) #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2001.09715
We formalize the theory of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of ZFC, we construct a proper generic extension and show that the latter also satisfies ZFC. In doing so, we remodularized Paulson's ZF-Constructibility library.