Mechanization of Separation in Generic Extensions

Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf

Published 2019-01-10Version 1

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. We also formalize the satisfaction of the axioms of Extensionality, Foundation, Union, and Powerset. The axiom of Infinity is likewise treated, under additional assumptions on the ground model. In order to achieve these goals, we extended Paulson's library on constructibility with renaming of variables for internalized formulas, improved results on definitions by recursion on well-founded relations, and sharpened hypotheses in his development of relativization and absoluteness.