2022/10/27 by Emmanuel Gunther, Miguel Pagano, Gunther, Emmanuel +5
Computer Science · Psychology · #03E30 (Secondary) #68V20 (Primary) 03E35 #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #I.2.3 #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Philosophy and Theoretical Science
paper · pdf · doi:10.48550/arxiv.2210.15609
openalex publication_date 2022/10/27 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We discuss some highlights of our computer-verified proof of the construction, given a countable transitive set-model M of ZFC, of generic extensions satisfying ZFC+\negCH and ZFC+CH. Moreover, let R be the set of instances of the Axiom of Replacement. We isolated a 21-element subset Ω\subseteqR and defined F:R\toR such that for every Φ\subseteqR and M-generic G, M\models ZC ∪ F``Φ∪ Ω implies M[G]\models ZC ∪ Φ∪ \ ¬ CH \, where ZC is Zermelo set theory with Choice. To achieve this, we worked in the proof assistant Isabelle, basing our development on the Isabelle/ZF library by L. Paulson and others.