Mechanization of Separation in Generic Extensions

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 of the hypotheses in his development of relativization and absoluteness.

You can download the paper and the whole Isabelle development. You can also browse the session as generated by Isabelle.

First steps towards a formalization of Forcing

Paper and code for LSFA 2018

Our first report on the formalization of Forcing was presented at LSFA 2018.

You can download the paper accepted for the post-proceedings and the whole Isabelle development. You can also browse the session as generated by Isabelle.