First steps towards a formalization of Forcing

TL;DR

This paper formalizes Cohen's forcing technique within Isabelle/ZF, defining forcing notions, generic filters, and proving key properties like the Rasiowa-Sikorski lemma and transitivity of generic extensions.

Contribution

It introduces a formalization of forcing in Isabelle/ZF, including definitions, the Rasiowa-Sikorski lemma, and properties of generic extensions, advancing mechanized set theory.

Findings

Formalization of forcing notions as preorders with top and dense subsets

Proof of the Rasiowa-Sikorski lemma within Isabelle/ZF

Demonstration that generic extensions preserve the axiom of pairing and transitivity

Abstract

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 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 $M[G]$ is transitive.