2 citations · 4 across the 3 of their papers we have counts for
5 papers
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…
Directly Indecomposables in Semidegenerate Varieties of Connected po-Groupoids
Pedro Sánchez Terraf
We study varieties with a term-definable poset structure, "po-groupoids". It is known that connected posets have the "strict refinement property" (SRP). In [arXiv:0808.1860v1 [math…
Boolean Factor Congruences and Property (*)
Pedro Sánchez Terraf
A variety V has Boolean factor congruences (BFC) if the set of factor congruences of every algebra in V is a distributive sublattice of its congruence lattice; this property holds…