The formal verification of the ctm approach to forcing
| Autor: | Gunther, Emmanuel, Pagano, Miguel, Terraf, Pedro Sánchez, Steinberg, Matías |
|---|---|
| Rok vydání: | 2022 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| Popis: | We discuss some highlights of our computer-verified proof of the construction, given a countable transitive set-model $M$ of $\mathit{ZFC}$, of generic extensions satisfying $\mathit{ZFC}+\neg\mathit{CH}$ and $\mathit{ZFC}+\mathit{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 \mathit{ZC} \cup \mathcal{F}\text{``}\Phi \cup \Omega$ implies $M[G]\models \mathit{ZC} \cup \Phi \cup \{ \neg \mathit{CH} \}$, where $\mathit{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. Comment: 20pp + 14pp in bibliography & appendices, 2 tables. v2: Added details to Delta System Lemma appendix, updated acknowledgments |
| Databáze: | arXiv |
| Externí odkaz: |
|