Mechanization of Separation in Generic Extensions. arXiv:1901.03313
Preprint, arXiv:1901.03313 [cs.LO] (2019).
Summary: 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.
MSC:
03B35 | Mechanization of proofs and logical operations |
03E40 | Other aspects of forcing and Boolean-valued models |
03B70 | Logic in computer science |
68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
arXiv data are taken from the
arXiv OAI-PMH API.
If you found a mistake, please
report it directly to arXiv.