### The Relative Consistency of CH in Isabelle/ZF (2021)

We developed relative versions of the Axiom of Dependent
choices in order to formalize κ-closed forcing
notions. Using this we are able to construct, given a
countable transitive model M of ZFC, a generic
extension satisfying ZFC plus the Continuum Hypothesis.

You can look at the development for Isabelle2021 at our
Bitbucket
repository, download
the sources
and generated documents,
and browse the
generated HTML.

### The Unprovability of CH in Isabelle/ZF (2021)

We finished our formalization of the construction, given a
countable transitive model M of ZFC, of a generic
extension satisfying ZFC plus the negation of the
Continuum Hypothesis.

You can look at the development at our
Bitbucket
repository and browse the cross-linked
session as generated by
Isabelle2021. Also slides
from the virtual talk
at the Set Theory and its
Interactions
session at
CLAM2021
are available.

### Formalization of Forcing in Isabelle/ZF (2020)

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 generic extension and show
that the latter also satisfies ZFC. In doing so, we remodularized
Paulson's ZF-Constructibility library.

You can download the
paper
(accepted at IJCAR
2020; arXiv:2001.09715;
video
of the talk)
and
the whole Isabelle 2019 development. You can also browse the
session as generated by
Isabelle. [*New:*
cross-linked session for Isabelle 2020]

### Mechanization of Separation in Generic Extensions
(2019)

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.

The manuscript is available at arXiv:1901.03313.

Previous stages of our project were announced here.

^{1} Universidad Nacional de Córdoba. Facultad de
Matemática, Astronomía, Física y Computación.

^{2} Centro de Investigación y Estudios de
Matemática (CIEM-FaMAF), Conicet. Córdoba. Argentina.