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
相关论文
共 50 条
  • [1] The PERF Approach for Formal Verification
    Benaissa, Nazim
    Bonvoisin, David
    Feliachi, Abderrahmane
    Ordioni, Julien
    [J]. RELIABILITY, SAFETY, AND SECURITY OF RAILWAY SYSTEMS: MODELLING, ANALYSIS, VERIFICATION, AND CERTIFICATION, RSSRAIL 2016, 2016, 9707 : 203 - 214
  • [2] The MODUS Approach to Formal Verification
    Brewka, Lukasz
    Soler, Jose
    Berger, Michael
    [J]. BUSINESS SYSTEMS RESEARCH JOURNAL, 2014, 5 (01): : 21 - 33
  • [3] An easy approach to formal verification
    Schlipf, T
    Buchner, T
    Fritz, R
    Helms, M
    [J]. TENTH ANNUAL IEEE INTERNATIONAL ASIC CONFERENCE AND EXHIBIT, PROCEEDINGS, 1997, : 120 - 124
  • [4] A Formal Approach to the Verification of Networks on Chip
    Borrione, Dominique
    Helmy, Amr
    Pierre, Laurence
    Schmaltz, Julien
    [J]. EURASIP JOURNAL ON EMBEDDED SYSTEMS, 2009, (01)
  • [5] A Formal Verification Approach for Robotic Workflows
    Rathmair, Michael
    Haspl, Thomas
    Komenda, Titanilla
    Reiterer, Bernhard
    Hofbaur, Michael
    [J]. 2021 20TH INTERNATIONAL CONFERENCE ON ADVANCED ROBOTICS (ICAR), 2021, : 670 - 675
  • [6] An Approach for Formal Verification of Authentication Protocols
    A. M. Mironov
    [J]. Lobachevskii Journal of Mathematics, 2022, 43 : 443 - 454
  • [7] An Approach for Formal Verification of Authentication Protocols
    Mironov, A. M.
    [J]. LOBACHEVSKII JOURNAL OF MATHEMATICS, 2022, 43 (02) : 443 - 454
  • [8] An algebraic approach to formal verification of microprocessors
    Hirabayashi, K
    [J]. JOURNAL OF ELECTRONIC TESTING-THEORY AND APPLICATIONS, 2001, 17 (06): : 543 - 544
  • [9] Equational approach to formal verification of SET
    Ogata, K
    Futatsugi, K
    [J]. QSIC 2004: PROCEEDINGS OF THE FOURTH INTERNATIONAL CONFERENCE ON QUALITY SOFTWARE, 2004, : 50 - 59
  • [10] An Algebraic Approach to Formal Verification of Microprocessors
    Kanji Hirabayashi
    [J]. Journal of Electronic Testing, 2001, 17 : 543 - 544
12345