The formal verification of the ctm approach to forcing

Abstract

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+\neg CH$ and $ZFC+CH$. Moreover, let $\mathcal{R}$ be the set of instances of the Axiom of Replacement. We isolated a 21-element subset $\Omega \subseteq \mathcal{R}$ and defined $\mathcal{F}:\mathcal{R}\to \mathcal{R}$ such that for every $\Phi \subseteq \mathcal{R}$ and $M$-generic $G$, $M\models ZC\cup \mathcal{F}\text{“}\Phi \cup \Omega$ implies $M[G]\models ZC\cup \Phi \cup \{\neg 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.

arXiv comment20pp + 14pp in bibliography & appendices, 2 tables. v2: Added details to Delta System Lemma appendix, updated acknowledgments