## Research team

- Diego Vaggione (Head of the group and Full Professor)
- Hector Gramaglia (Associate Professor)
- Miguel Campercholi (Adjunct Professor and Conicet Researcher)
- Pedro Sánchez Terraf (Associate Professor and Conicet Researcher)
- Mariana Badano (Assistant Professor and Postdoctoral fellow)

## Current graduate students

- Martín Moroni
- Mauricio Tellechea (Assistant Professor)
- Pablo Ventura

## Recent Papers (and latest manuscripts)

- E. Gunther, M. Pagano, and P. Sánchez Terraf, “Mechanization of Separation in Generic Extensions,” arXiv e-prints p. arXiv:1901.03313 (2019).

[ Abstract | BibTeX ]

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.

`@article{2019arXiv190103313G, author = {Gunther, Emmanuel and Pagano, Miguel and S{\'a}nchez Terraf, Pedro}, title = {{Mechanization of Separation in Generic Extensions}}, journal = {arXiv e-prints}, keywords = {Computer Science - Logic in Computer Science, Mathematics - Logic, 03B35 (Primary) 03E40, 03B70, 68T15 (Secondary), F.4.1}, year = 2019, month = jan, eid = {arXiv:1901.03313}, pages = {arXiv:1901.03313}, archiveprefix = {arXiv}, eprint = {1901.03313}, primaryclass = {cs.LO}, adsurl = {https://ui.adsabs.harvard.edu/\#abs/2019arXiv190103313G}, adsnote = {Provided by the SAO/NASA Astrophysics Data System}, abstract = {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.} }`

- M. Badano and D. Vaggione, “Characterization of context-free languages,” Theor. Comput. Sci. 676 p. 92–96 (2017).

[ BibTeX ]`@article{zbMATH06714282, author = {M. {Badano} and D. {Vaggione}}, title = {{Characterization of context-free languages}}, fjournal = {{Theoretical Computer Science}}, journal = {{Theor. Comput. Sci.}}, issn = {0304-3975}, volume = {676}, pages = {92--96}, year = {2017}, publisher = {Elsevier, Amsterdam}, language = {English}, doi = {10.1016/j.tcs.2017.03.002}, msc2010 = {68Q} }`

- M. Badano and D. Vaggione, “$\mathcal{V}_{SI}$ first order implies $\mathcal{V}_{DI}$ first order,” Acta Math. Hung. 151 (1) p. 47–49 (2017).

[ BibTeX ]`@article{zbMATH06707836, author = {M. {Badano} and D. {Vaggione}}, title = {{$\mathcal{V}_{SI}$ first order implies $\mathcal{V}_{DI}$ first order}}, fjournal = {{Acta Mathematica Hungarica}}, journal = {{Acta Math. Hung.}}, issn = {0236-5294; 1588-2632/e}, volume = {151}, number = {1}, pages = {47--49}, year = {2017}, publisher = {Springer Netherlands, Dordrecht; Akad\'emiai Kiad\'o, Budapest}, language = {English}, doi = {10.1007/s10474-016-0676-0}, msc2010 = {08B10} }`

- M. V. Badano and D. J. Vaggione, “Varieties with equationally definable factor congruences II,” Algebra Univers. (2017).

[ BibTeX ]`@article{edfc2, author = {Mariana V. {Badano} and Diego J. {Vaggione}}, title = {{Varieties with equationally definable factor congruences II}}, fjournal = {{Algebra Universalis}}, journal = {{Algebra Univers.}}, issn = {0002-5240; 1420-8911/e}, year = {2017}, publisher = {Springer (Birkh\"auser), Basel; University of Manitoba, Department of Mathematics, Winnipeg}, language = {English}, note = {In press}, msc2010 = {03C05 08B05 08B10} }`

- E. Gunther, M. Pagano, and P. Sánchez Terraf, “First steps towards a formalization of Forcing,” Electronic Notes in Theoretical Computer Science (2018).

[ Abstract | BibTeX ]

We lay the ground for an Isabelle/ZF formalization of Cohen’s technique of \emph{forcing}. We formalize the definition of forcing notions as preorders with top, dense subsets, and generic filters. We formalize a version of the principle of Dependent Choices and using it we prove the Rasiowa-Sikorski lemma on the existence of generic filters. Given a transitive set $M$, we define its generic extension $M[G]$, the canonical names for elements of $M$, and finally show that if $M$ satisfies the axiom of pairing, then $M[G]$ also does.

`@article{2018arXiv180705174G, author = {Gunther, Emmanuel and Pagano, Miguel and S{\'a}nchez Terraf, Pedro}, title = {{First steps towards a formalization of Forcing}}, journal = {Electronic Notes in Theoretical Computer Science}, archiveprefix = {arXiv}, eprint = {1807.05174}, primaryclass = {cs.LO}, keywords = {Computer Science - Logic in Computer Science, 03B35 (Primary) 03E40, 03B70, 68T15 (Secondary), F.4.1}, year = 2018, month = jul, adsurl = {http://adsabs.harvard.edu/abs/2018arXiv180705174G}, adsnote = {Provided by the SAO/NASA Astrophysics Data System}, abstract = {We lay the ground for an Isabelle/ZF formalization of Cohen's technique of \emph{forcing}. We formalize the definition of forcing notions as preorders with top, dense subsets, and generic filters. We formalize a version of the principle of Dependent Choices and using it we prove the Rasiowa-Sikorski lemma on the existence of generic filters. Given a transitive set $M$, we define its generic extension $M[G]$, the canonical names for elements of $M$, and finally show that if $M$ satisfies the axiom of pairing, then $M[G]$ also does.}, note = {Accepted. Presented at \emph{Logical and Semantic Frameworks, with Applications} (LSFA 2018)} }`