The formal verification of the ctm approach to forcing

被引：0
作者：
Gunther, Emmanuel [1 ]
Pagano, Miguel [1 ]
Terraf, Pedro Sanchez [1 ,2 ]
Steinberg, Matias [1 ]
机构：
[1] Univ Nacl Cordoba, Fac Matemat Astron Fis & Comp, Cordoba, Argentina
[2] Consejo Nacl Invest Cient & Tecn, Ctr Invest & Estudios Matemat CIEM, FAMAF, Cordoba, Argentina
来源：
ANNALS OF PURE AND APPLIED LOGIC | 2024年 / 175卷 / 05期
关键词：
Isabelle/ZF; Countable transitive models; Continuum hypothesis; Proof assistants; Interactive theorem provers; Generic extension; SET-THEORY; CALCULUS;
D O I：
10.1016/j.apal.2024.103413
中图分类号：
O29 [应用数学];
学科分类号：
070104 ;
摘要：
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 + not sign CH and ZFC + CH. Moreover, let R be the set of instances of the Axiom of Replacement. We isolated a 21-element subset 12 C R and defined F : R - R such that for every phi C R and M-generic G, M |= ZC U F"phi U 12 implies M[G] |= ZC U phi U { not sign 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. (c) 2024 Elsevier B.V. All rights reserved.
引用
收藏
页数：28
相关论文
共 59 条
  • [1] Agda Development Team, 2022, Agda, version 2.6.2
  • [2] [Anonymous], 2014, Handbook of the History of Logic, DOI DOI 10.1016/B978-0-444-51624-4.50004-6
  • [3] [Anonymous], 1998, Oxford Logic Guides
  • [4] [Anonymous], 2008, Notices Amer. Math. Soc.
  • [5] [Anonymous], 1984, Intuitionistic Type Theory
  • [6] [Anonymous], 2003, LMS J. Comput. Math., DOI [10.1112/S1461157000000449, DOI 10.1112/S1461157000000449]
  • [7] Bayer J, 2022, Arxiv, DOI arXiv:2207.04779
  • [8] Blanchette Jasmin, 2020, Handbook of Proof Assistants and Their Applications in Mathematics and Computer Science
  • [9] BRUIJN NGD, 1972, P K NED AKAD A MATH, V75, P381
  • [10] Buzzard K., arXiv
123456