Pedro Sánchez Terraf

CIEM-FaMAFUniversidad Nacional de Córdoba

Publicaciones

Buscáme en arXiv

En revistas (y manuscritos recientes)

[17] Set theory in Córdoba (2024). Extended abstract for invited talk at the 40th anniversary of the Center for Research and Studies in Mathematics (Córdoba). [ bib | .pdf ]
Set Theory is a new research area in Argentina, still with very few practitioners. We present some of the first steps towards its development at the National University of Córdoba. Cantor's continuum problem, that of the determining which place does the cardinality of the reals occupy in the cardinal line, provides an appropriate frame for this exposition (and for the whole of Set Theory indeed).
[16] A classification of bisimilarities for general Markov decision processes (2024). 2401.09273. Junto a M. S. Moroni. [ bib | arXiv ]
We provide a fine classification of bisimilarities between states of possibly different labelled Markov processes (LMP). We show that a bisimilarity relation proposed by Panangaden that uses direct sums coincides with “event bisimilarity” from his joint work with Danos, Desharnais, and Laviolette. We also extend Giorgio Bacci's notions of bisimilarity between two different processes to the case of nondeterministic LMP and generalize the game characterization of state bisimilarity by Clerc et al. for the latter.
[15] The formal verification of the ctm approach to forcing. Annals of Pure and Applied Logic, 175 (2024). 2210.15609. Junto a E. Gunther, M. Pagano, y M. Steinberg. [ bib | DOI | arXiv | http ]
We discuss some highlights of our computer-verified proof of the construction, given a countable transitive set-model M of ZFC, of generic extensions satisfying ZFC + ¬CH and ZFC + CH. Moreover, let R be the set of instances of the Axiom of Replacement. We isolated a 21-element subset Ω⊆R and defined F: RR such that for every Φ⊆R and M -generic G, MZCF“Φ∪Ω implies M[G]⊧ZC ∪Φ∪{¬CH}, where ZC is Zermelo set theory with Choice.

To achieve this, we worked in the proof assistant Isabelle, basing our development on the Isabelle/ZF library by L. Paulson and others.

[14] The Zhou ordinal of labelled Markov processes over separable spaces. The Review of Symbolic Logic, 16 (4): 1011–1032 (diciembre 2023). arXiv:2005.03630. Junto a M. S. Moroni. [ bib | DOI | arXiv | http ]
There exist two notions of equivalence of behavior between states of a Labelled Markov Process (LMP): state bisimilarity and event bisimilarity. The first one can be considered as an appropriate generalization to continuous spaces of Larsen and Skou's probabilistic bisimilarity, while the second one is characterized by a natural logic. C. Zhou expressed state bisimilarity as the greatest fixed point of an operator O, and thus introduced an ordinal measure of the discrepancy between it and event bisimilarity. We call this ordinal the "Zhou ordinal" of S, Z(S). When Z(S)=0, S satisfies the Hennessy-Milner property. The second author proved the existence of an LMP S with Z(S) ≥1 and Zhou showed that there are LMPs having an infinite Zhou ordinal. In this paper we show that there are LMPs S over separable metrizable spaces having arbitrary large countable Z(S) and that it is consistent with the axioms of ZFC that there is such a process with an uncountable Zhou ordinal.
[13] Every minimal dual discriminator variety is minimal as a quasivariety. Algebra universalis, 82 (2): 36 (abril 2021). Junto a X. Caicedo, M. Campercholi, K. A. Kearnes, Á. Szendrei, y D. Vaggione. [ bib | DOI | http ]
Let † denote the following property of a variety V: Every subquasivariety of V is a variety. In this paper, we prove that every idempotent dual discriminator variety has property † . Property † need not hold for nonidempotent dual discriminator varieties, but † does hold for minimal nonidempotent dual discriminator varieties. Combining the results for the idempotent and nonidempotent cases, we obtain that every minimal dual discriminator variety is minimal as a quasivariety
[12] Semipullbacks of labelled Markov processes. Logical Methods in Computer Science, 17 (2) (abril 2021). arXiv:1706.02801. Junto a J. Pachl. [ bib | DOI | arXiv | http ]
A labelled Markov process (LMP) consists of a measurable space S together with an indexed family of Markov kernels from S to itself. This structure has been used to model probabilistic computations in Computer Science, and one of the main problems in the area is to define and decide whether two LMP S and S' “behave the same”. There are two natural categorical definitions of sameness of behavior: S and S' are bisimilar if there exist an LMP T and measure preserving maps forming a diagram of the shape STS'; and they are behaviorally equivalent if there exist some U and maps forming a dual diagram SUS'.

These two notions differ for general measurable spaces but Edalat proved that they coincide for analytic Borel spaces, showing that from every diagram SUS' one can obtain a bisimilarity diagram as above. Moreover, the resulting square of measure preserving maps is commutative (a semipullback).

In this paper, we extend Edalat's result to measurable spaces S isomorphic to a universally measurable subset of a Polish space with the trace of the Borel σ-algebra, using a version of Strassen's theorem on common extensions of finitely additive measures.

[11] Bisimilarity is not Borel. Mathematical Structures in Computer Science, 27 (7): 1265–1284 (octubre 2017). [ bib | DOI | http ]
We prove that the relation of bisimilarity between countable labelled transition systems is Σ11-complete (hence not Borel), by reducing the set of non-wellorders over the natural numbers continuously to it. This has an impact on the theory of probabilistic and nondeterministic processes over uncountable spaces, since logical characterizations of bisimilarity (as, for instance, those based on the unique structure theorem for analytic spaces) require a countable logic whose formulas have measurable semantics. Our reduction shows that such a logic does not exist in the case of image-infinite processes.
[10] The Lattice of Congruences of a Finite Linear Frame. Journal of Logic and Computation, 27: 2653–2688 (abril 2017). 1504.01789. Junto a C. Areces, M. Campercholi, y D. Penazzi. [ bib | DOI | arXiv ]
Let F=⟨F,R⟩ be a finite Kripke frame. A congruence of F is a bisimulation of F that is also an equivalence relation on F. The set of all congruences of F is a lattice under the inclusion ordering. In this article we investigate this lattice in the case that F is a finite linear frame. We give concrete descriptions of the join and meet of two congruences with a nontrivial upper bound. Through these descriptions we show that for every nontrivial congruence ρ, the interval [IdF,ρ] embeds into the lattice of divisors of a suitable positive integer. We also prove that any two congruences with a nontrivial upper bound permute.
[9] Stochastic nondeterminism and effectivity functions. Journal of Logic and Computation, 27 (1): 357–394 (2017). 1405.7141. Junto a E.-E. Doberkat. [ bib | DOI | arXiv ]
This paper investigates stochastic nondeterminism on continuous state spaces by relating nondeterministic kernels and stochastic effectivity functions to each other. Nondeterministic kernels are functions assigning each state a set o subprobability measures, and effectivity functions assign to each state an upper-closed set of subsets of measures. Both concepts are generalizations of Markov kernels used for defining two different models: Nondeterministic labelled Markov processes and stochastic game models, respectively. We show that an effectivity function that maps into principal filters is given by an image-countable nondeterministic kernel, and that image-finite kernels give rise to effectivity functions. We define state bisimilarity for the latter, considering its connection to morphisms. We provide a logical characterization of bisimilarity in the finitary case. A generalization of congruences (event bisimulations) to effectivity functions and its relation to the categorical presentation of bisimulation are also studied.
[8] Bisimulations for non-deterministic labelled Markov processes. Mathematical Structures in Comp. Sci., 22 (1): 43–68 (febrero 2012). Junto a P. R. D'Argenio y N. Wolovick. [ bib | DOI | http ]
We extend the theory of labeled Markov processes with internal nondeterminism, a fundamental concept for the further development of a process theory with abstraction on nondeterministic continuous probabilistic systems. We define nondeterministic labeled Markov processes (NLMP) and provide three definition of bisimulations: a bisimulation following a traditional characterization, a state based bisimulation tailored to our “measurable” non-determinism, and an event based bisimulation. We show the relation between them, including that the largest state bisimulation is also an event bisimulation. We also introduce a variation of the Hennessy-Milner logic that characterizes event bisimulation and that is sound w.r.t. the other bisimulations for arbitrary NLMP. This logic, however, is infinitary as it contains a denumerable . We then introduce a finitary sublogic that characterize all bisimulations for image finite NLMP whose underlying measure space is also analytic. Hence, in this setting, all notions of bisimulation we deal with turn out to be equal. Finally, we show that all notions of bisimulations are different in the general case. The counterexamples that separate them turn to be non-probabilistic NLMP.
[7] Factor congruences in semilattices. Revista de la Unión Matemática Argentina, 52 (1): 1–10 (2011). 0809.3822. [ bib | arXiv | .pdf ]
We characterize factor congruences in semilattices by using generalized notions of order ideal and of direct sum of ideals. When the semilattice has a minimum (maximum) element, these generalized ideals turn into ordinary (dual) ideals.
[6] Boolean factor congruences and property (*). Int. J. Algebra Comput., 21 (6): 931–950 (2011). [ bib | DOI ]
A variety V has Boolean factor congruences (BFC) if the set of factor congruences of any algebra in V is a distributive sublattice of its congruence lattice; this property holds in rings with unit and in every variety which has a semilattice operation. BFC has a prominent role in the study of uniqueness of direct product representations of algebras, since it is a strengthening of the refinement property. We provide an explicit Mal'tsev condition for BFC. With the aid of this condition, it is shown that BFC is equivalent to a variant of the definability property (*), an open problem in R. Willard's work [J. Algebra 132, No. 1, 130–153 (1990; Zbl 0737.08006)].
[5] Unprovability of the logical characterization of bisimulation. Information and Computation, 209 (7): 1048–1056 (2011). [ bib | DOI | http ]
We quickly review labelled Markov processes (LMP) and provide a counterexample showing that in general measurable spaces, event bisimilarity and state bisimilarity differ in LMP. This shows that the logic in the work by Desharnais does not characterize state bisimulation in non-analytic measurable spaces. Furthermore we show that, under current foundations of Mathematics, such logical characterization is unprovable for spaces that are projections of a coanalytic set. Underlying this construction there is a proof that stationary Markov processes over general measurable spaces do not have semi-pullbacks.
[4] Existentially definable factor congruences. Acta Scientiarum Mathematicarum (Szeged), 76 (1–2): 49–53 (2010). 0906.4722. [ bib | arXiv | http ]
A variety V has definable factor congruences if and only if factor congruences can be defined by a first-order formula Φ having central elements as parameters. We prove that if Φ can be chosen to be existential, factor congruences in every algebra of V are compact.
[3] Varieties with definable factor congruences. Trans. Amer. Math. Soc., 361: 5061–5088 (2009). Junto a D. Vaggione. [ bib | DOI ]
We study direct product representations of algebras in varieties. We collect several conditions expressing that these representations are definable in a first-order-logic sense, among them the concept of Definable Factor Congruences (DFC). The main results are that DFC is a Mal'cev property and that it is equivalent to all other conditions formulated; in particular we prove that V has DFC if and only if V has 0⃗ & 1⃗ and Boolean Factor Congruences. We also obtain an explicit first order definition Φ of the kernel of the canonical projections via the terms associated to the Mal'cev condition for DFC, in such a manner it is preserved by taking direct products and direct factors. The main tool is the use of central elements, which are a generalization of both central idempotent elements in rings with identity and neutral complemented elements in a bounded lattice.
[2] Directly indecomposables in semidegenerate varieties of connected po-groupoids. Order, 25 (4): 377–386 (2008). [ bib | DOI ]
We study varieties with a term-definable poset structure, po-groupoids. It is known that connected posets have the strict refinement property (SRP). In a previous work by Vaggione and the author it is proved that semidegenerate varieties with the SRP have definable factor congruences and if the similarity type is finite, directly indecomposables are axiomatizable by a set of first-order sentences. We obtain such a set for semidegenerate varieties of connected po-groupoids and show its quantifier complexity is bounded in general.
[1] Compact factor congruences imply Boolean factor congruences. Algebra univers., 51: 207–213 (2004). Junto a D. Vaggione. [ bib | DOI ]
We prove that any variety V in which every factor congruence is compact has Boolean factor congruences, i.e., for all A in V the set of factor congruences of A is a distributive sublattice of the congruence lattice of A.

En conferencias con referato

[4] Formalization of Forcing in Isabelle/ZF. En N. Peltier, V. Sofronie-Stokkermans, editores, Automated Reasoning. 10th International Joint Conference, IJCAR 2020, Paris, France, July 1–4, 2020, Proceedings, Part II, tomo 12167 de Lecture Notes in Artificial Intelligence, págs. 221–235. Springer International Publishing (2020). 2001.09715. Junto a E. Gunther y M. Pagano. [ bib | DOI | arXiv ]
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.
[3] First steps towards a formalization of Forcing. Electronic Notes in Theoretical Computer Science, 344: 119 – 136 (julio 2019). 1807.05174. The proceedings of LSFA 2018, the 13th Workshop on Logical and Semantic Frameworks with Applications (LSFA’18). Junto a E. Gunther y M. Pagano. [ bib | DOI | arXiv | http ]
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 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] A theory for the semantics of stochastic and non-deterministic continuous systems. En A. Remke, M. Stoelinga, editores, Stochastic Model Checking. Rigorous Dependability Analysis Using Model Checking Techniques for Stochastic Systems, tomo 8453 de Lecture Notes in Computer Science, págs. 67–86. Springer Berlin Heidelberg (2014). Junto a C. E. Budde, P. R. D'Argenio, y N. Wolovick. [ bib | DOI | http ]
The description of complex systems involving physical or biological components usually requires to model involved continuous behavior induced by variables such as time, distances, speed, temperature, alkalinity of a solution, etc. Often, such variables can be quantified probabilistically to better understand the behavior of the complex systems. For example, the arrival time of events may be considered a Poisson process or the weight of an individual may be assumed to be distributed according to a log-normal distribution. However, it is also common that the uncertainty on how these variables behave make us prefer to leave out the choice of a particular probability and rather model it as a purely non-deterministic decision, as it is the case when a system is intended to be deployed in a variety of very different computer or network architectures. Therefore, the semantics of these systems needs to be represented by a variant of probabilistic automata that involves continuous domains on the state space and the transition relation. In this paper, we provide a survey to the theory of such kind of models. We present the theory of the so called labeled Markov processes (LMP) and its extension with internal non-determinism (NLMP). We show that in these complex domains, the bisimulation relation can be understood in different manners. We show the relation among these different definitions and try to understand the boundaries among them through examples. We also study variants of Hennessy-Milner logic that provides logical characterizations of some of these bisimulations.
[1] Nondeterministic labeled Markov processes: Bisimulations and logical characterization. En QEST, Sixth International Conference on the Quantitative Evaluation of Systems, págs. 11–20. IEEE Computer Society (2009). Junto a P. R. D'Argenio, N. Wolovick, y P. Celayes. [ bib | DOI ]

No publicados

[4] Transitive models of fragments of ZFC. Archive of Formal Proofs (marzo 2022). https://isa-afp.org/entries/Transitive_Models.html, Formal proof development. Junto a E. Gunther, M. Pagano, y M. Steinberg. [ bib ]
[3] The independence of the continuum hypothesis in Isabelle/ZF. Archive of Formal Proofs (marzo 2022). https://isa-afp.org/entries/Independence_CH.html, Formal proof development. Junto a E. Gunther, M. Pagano, y M. Steinberg. [ bib ]
[2] Cofinality and the delta system lemma. Archive of Formal Proofs (diciembre 2020). https://isa-afp.org/entries/Delta_System_Lemma.html, Formal proof development. [ bib ]
[1] Mechanization of Separation in Generic Extensions. arXiv e-prints (enero 2019). arXiv:1901.03313. Junto a E. Gunther y M. Pagano. [ bib | arXiv ]
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.

Ir arriba