## Research team

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

## Recent Papers (and latest manuscripts)

1. E. Gunther, M. Pagano, and P. Sánchez Terraf, “First steps towards a formalization of Forcing,” arXiv:1807.05174 (2018).
[ arXiv | 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 = {ArXiv e-prints},
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,
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.}
}

2. M. A. Campercholi and J. G. Raftery, “Relative congruence formulas and decompositions in quasivarieties,” Algebra universalis (2017).

Quasivarietal analogues of uniform congruence schemes are discussed, and their relationship with the equational definability of principal relative congruences (EDPRC) is established, along with their significance for relative congruences on subalgebras of products. Generalizing the situation in varieties, we prove that a quasivariety is relatively ideal iff it has EDPRC; it is relatively filtral iff it is relatively semisimple with EDPRC. As an application, it is shown that a finitary sentential logic, algebraized by a quasivariety K, has a classical inconsistency lemma if and only if K is relatively filtral and the subalgebras of its nontrivial members are nontrivial. A concrete instance of this result is exhibited, in which K is not a variety. Finally, for quasivarieties {\$}{\$}{\{}{\backslash}sf{\{}M{\}} {\backslash}subseteq {\backslash}sf{\{}K{\}}{\}}{\$}{\$} M ⊆ K , we supply some conditions under which M is the restriction to K of a variety, assuming that K has EDPRC.

@article{Campercholi2017,
author = {Campercholi, Miguel A. and Raftery, James G.},
title = {Relative congruence formulas and decompositions in quasivarieties},
journal = {Algebra universalis},
year = {2017},
month = {Sep},
abstract = {Quasivarietal analogues of uniform congruence schemes are discussed, and their relationship with the equational definability of principal relative congruences (EDPRC) is established, along with their significance for relative congruences on subalgebras of products. Generalizing the situation in varieties, we prove that a quasivariety is relatively ideal iff it has EDPRC; it is relatively filtral iff it is relatively semisimple with EDPRC. As an application, it is shown that a finitary sentential logic, algebraized by a quasivariety K, has a classical inconsistency lemma if and only if K is relatively filtral and the subalgebras of its nontrivial members are nontrivial. A concrete instance of this result is exhibited, in which K is not a variety. Finally, for quasivarieties {\$}{\$}{\{}{\backslash}sf{\{}M{\}} {\backslash}subseteq {\backslash}sf{\{}K{\}}{\}}{\$}{\$} M ⊆ K , we supply some conditions under which M is the restriction to K of a variety, assuming that K has EDPRC.},
day = {27},
doi = {10.1007/s00012-017-0455-y},
issn = {1420-8911},
url = {https://doi.org/10.1007/s00012-017-0455-y}
}

3. 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}
}

4. 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},
}