2 citations · 4 across the 3 of their papers we have counts for
3 papers · 1 filter
Formalization of Forcing in Isabelle/ZF
Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf
We formalize the theory of forcing in the set theory framework of Isabelle/ZF. Under the assumption of the existence of a countable transitive model of ZFC, we construct a proper g…
Mechanization of Separation in Generic Extensions
Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf
We mechanize, in the proof assistant Isabelle, a proof of the axiom-scheme of Separation in generic extensions of models of set theory by using the fundamental theorems of forcing.…
First steps towards a formalization of Forcing
Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf
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…