First Steps Towards a Formalization of Forcing
Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf · Electronic Notes in Theoretical Computer Science · 2019
We lay the ground for an Isabelle/ZF formalization of Cohen's technique of forcing . We formalize the definition of forcing notions as preorders with top, dense subsets, and generic filters. We formalize a version of the principle of Dependent Choices and using it we prove the Rasiowa-Sikorski lemma on the existence of generic filters. Given a transitive set M , we define its generic extension M [ G ], the canonical names for elements of M , and finally show that if M satisfies the axiom of pairing, then M [ G ] also does. We also prove that M [ G ] is transitive.