Some lesson after the formalization of the ctm approach to forcing

GUNTHER, EMMANUEL; PAGANO, MIGUEL; PEDRO SÁNCHEZ TERRAF; MATÍAS STEINBERG

Congreso; Coloquio Latinoamericano de Matemáticos; 2021

UMALCA

This is a joint work in progress with Emmanuel Gunther, Miguel Pagano,and Matı́as Steinberg.In this talk we?ll discuss some highlights of our computer-verified proof ofthe construction, given a countable transitive set model M of ZFC , of a genericextension M [G] satisfying ZFC + ¬CH . In particular, we isolated a set ∆ of∼40 instances of the axiom schemes of Replacement and afunction F such that such that for any finite fragment Φ ⊆ ZFC , F (Φ) ⊆ ZFCis also finite and if M |= F (Φ) + Separation + ∆ then M [G] |= Φ + Separation + ¬CH.We also obtained the formulas yielded by the Forcing Definability Theorem explicitly.To achieve this, we worked in the proof assistant Isabelle, basing our devel-opment on the theory Isabelle/ZF by L. Paulson and others.The vantage point of the talk will be that of a mathematician but elementsfrom the computer science perspective will be present. Perhaps some mythsregarding what can effectively be done using proof assistants/checkers will bedispelled.We?ll also compare our formalization with the recent one by Jesse M. Hanand Floris van Doorn in the proof assistant Lean.