Research

2022

1. Topological duality for distributive lattices, and applications.

   Mai Gehrke and Sam van Gool.

   Textbook, preprint, 2022

   arXiv

   This book is a course in Stone-Priestley duality theory, with applications to logic and theoretical computer science. Our target audience are graduate students and researchers in mathematics and computer science. Our aim is to get in a fairly full palette of duality tools as directly and quickly as possible, then to illustrate and further elaborate these tools within the setting of three emblematic applications: semantics of propositional logics, domain theory in logical form, and the theory of profinite monoids for the study of regular languages and automata. This preprint version contains the first part of the book, a graduate level ‘crash course’ in duality theory as it is practiced now, and a chapter on applications to domain theory.

2. First-order separation over countable ordinals.

   Thomas Colcombet, Sam van Gool, and Rémi Morvan.

   Foundations of Software Science and Computation Structures (FoSSaCS) 2022

   arXiv PDF

   We show that the existence of a first-order formula separating two monadic second order formulas over countable ordinal words is decidable. This extends the work of Henckell and Almeida on finite words, and of Place and Zeitoun on ω-words. For this, we develop the algebraic concept of monoid (resp. ω-semigroup, resp. ordinal monoid) with aperiodic merge, an extension of monoids (resp. ω-semigroup, resp. ordinal monoid) that explicitly includes a new operation capturing the loss of precision induced by first-order indistinguishability. We also show the computability of FO-pointlike sets, and the decidability of the covering problem for first-order logic on countable ordinal words.

2021

1. Time Warps, from Algebra to Algorithms.

   Sam van Gool, Adrien Guatto, George Metcalfe, and Simon Santschi.

   Relational and Algebraic Methods in Computer Science (RAMiCS) 2021

   arXiv PDF

   Graded modalities have been proposed in recent work on programming languages as a general framework for refining type systems with intensional properties. In particular, continuous endomaps of the discrete time scale, or time warps, can be used to quantify the growth of information in the course of program execution. Time warps form a complete residuated lattice, with the residuals playing an important role in potential programming applications. In this paper, we study the algebraic structure of time warps, and prove that their equational theory is decidable, a necessary condition for their use in real-world compilers. We also describe how our universal-algebraic proof technique lends itself to a constraint-based implementation, establishing a new link between universal algebra and verification technology.

2. Priestley duality for MV algebras and beyond.

   Wesley Fussner, Mai Gehrke, Sam van Gool, and Vincenzo Marra.

   Forum Mathematicum 2021

   arXiv PDF

   We provide a new perspective on extended Priestley duality for large class of distributive lattices equipped with binary double quasioperators. Under this approach, non-lattice binary operations are each presented as a pair of partial binary operations on dual spaces. In this enriched environment, equational conditions on the algebraic side of the duality may more often be rendered as first-order conditions on dual spaces. In particular, we specialize our general results to the variety of MV-algebras, obtaining a duality for these in which the equations axiomatizing MV-algebras are dualized as first-order conditions.

2019

1. Pointlike sets for varieties determined by groups.

   Sam van Gool and Benjamin Steinberg.

   Advances in Mathematics 2019

   arXiv PDF

   For a variety of finite groups H, let H-bar denote the variety of finite semigroups all of whose subgroups lie in H. We give a characterization of the subsets of a finite semigroup that are pointlike with respect to H-bar. Our characterization is effective whenever H has a decidable membership problem. In particular, the separation problem for H-bar-languages is decidable for any decidable variety of finite groups H. This generalizes Henckell’s theorem on decidability of aperiodic pointlikes.

2. Pro-aperiodic monoids via saturated models (journal version).

   Sam van Gool and Benjamin Steinberg.

   Israel Journal of Mathematics 2019

   arXiv PDF

   We apply Stone duality and model theory to study the structure theory of free pro-aperiodic monoids. Stone duality implies that elements of the free pro-aperiodic monoid may be viewed as elementary equivalence classes of pseudofinite words. Model theory provides us with saturated words in each such class, i.e., words in which all possible factorizations are realized. We give several applications of this new approach, including a solution to the word problem for ω-terms that avoids using McCammond’s normal forms, as well as new proofs and extensions of other structural results concerning free pro-aperiodic monoids.

3. Merge decompositions, two-sided Krohn-Rhodes, and aperiodic pointlikes.

   Sam van Gool and Benjamin Steinberg.

   Canadian Mathematical Bulletin 2019

   arXiv PDF

   This paper provides short proofs of two fundamental theorems of finite semigroup theory whose previous proofs were significantly longer, namely the two-sided Krohn-Rhodes decomposition theorem and Henckell’s aperiodic pointlike theorem. We use a new algebraic technique that we call the merge decomposition. A prototypical application of this technique decomposes a semigroup T into a two-sided semidirect product whose components are built from two subsemigroups T₁, T₂, which together generate T, and the subsemigroup generated by their setwise product T₁T₂. In this sense we decompose T by merging the subsemigroups T₁ and T₂. More generally, our technique merges semigroup homomorphisms from free semigroups.

4. Proaperiodic monoids via prime models.

   Sam van Gool and Benjamin Steinberg.

   Research note, 2019

   PDF

   An unpublished note (work in progress) on extending our work on saturated models to prime models.

2018

1. An interpolant in predicate Gödel logic.

   Mattias Baaz, Mai Gehrke, and Sam van Gool.

   Research note, 2018

   arXiv

   A logic satisfies the interpolation property provided that whenever a formula Δ is a consequence of another formula Γ, then this is witnessed by a formula Θ which only refers to the language common to Γ and Δ. That is, the relational (and functional) symbols occurring in Θ occur in both Γ and Δ, Γ has Θ as a consequence, and Θ has Δ as a consequence. Both classical and intuitionistic predicate logic have the interpolation property, but it is a long open problem which intermediate predicate logics enjoy it. In 2013 Mints, Olkhovikov, and Urquhart showed that constant domain intuitionistic logic does not have the interpolation property, while leaving open whether predicate Gödel logic does. In this short note, we show that their counterexample for constant domain intuitionistic logic does admit an interpolant in predicate Gödel logic. While this has no impact on settling the question for predicate Gödel logic, it lends some credence to a common belief that it does satisfy interpolation. Also, our method is based on an analysis of the semantic tools of Olkhovikov and it is our hope that this might eventually be useful in settling this question.

2. An open mapping theorem for finitely copresented Esakia spaces.

   Sam van Gool and Luca Reggio.

   Topology and its Applications 2018

   arXiv PDF

   We prove an open mapping theorem for the topological spaces dual to finitely presented Heyting algebras. This yields in particular a short, self-contained semantic proof of the uniform interpolation theorem for intuitionistic propositional logic, first proved by Pitts in 1992. Our proof is based on the methods of Ghilardi & Zawadowski. However, our proof does not require sheaves nor games, only basic duality theory for Heyting algebras.

3. Sheaves and Duality.

   Mai Gehrke and Sam van Gool.

   Journal of Pure and Applied Algebra 2018

   PDF

   It has long been known in universal algebra that any distributive sublattice of congruences of an algebra which consists entirely of commuting congruences yields a sheaf representation of the algebra. In this paper we provide a generalization of this fact and prove a converse of the generalization. To be precise, we exhibit a one-to-one correspondence (up to isomorphism) between soft sheaf representations of universal algebras over stably compact spaces and frame homomorphisms from the dual frames of such spaces into subframes of pairwise commuting congruences of the congruence lattices of the universal algebras. For distributive-lattice-ordered algebras this allows us to dualize such sheaf representations.

2017

1. A model-theoretic characterization of monadic second-order logic on infinite words.

   Silvio Ghilardi and Sam van Gool.

   Journal of Symbolic Logic 2017

   PDF

   Monadic second order logic and linear temporal logic are two logical formalisms that can be used to describe classes of infinite words, i.e., first-order models based on the natural numbers with order, successor, and finitely many unary predicate symbols. Monadic second order logic over infinite words (S1S) can alternatively be described as a first-order logic interpreted in 𝒫(ω), the power set Boolean algebra of the natural numbers, equipped with modal operators for ’initial’, ’next’ and ’future’ states. We prove that the first-order theory of this structure is the model companion of a class of algebras corresponding to a version of linear temporal logic (LTL) without until. The proof makes crucial use of two classical, non-trivial results from the literature, namely the completeness of LTL with respect to the natural numbers, and the correspondence between S1S-formulas and Büchi automata.

2. Uniform Interpolation and Compact Congruences.

   Sam van Gool, George Metcalfe, and Constantine Tsinakis.

   Annals of Pure and Applied Logic 2017

   PDF

   Uniform interpolation properties are defined for equational consequence in a variety of algebras and related to properties of compact congruences on first the free and then the finitely presented algebras of the variety. It is also shown, following related results of Ghilardi and Zawadowski, that a combination of these properties provides a sufficient condition for the first-order theory of the variety to admit a model completion.

3. Pro-aperiodic monoids via saturated models.

   Sam van Gool and Benjamin Steinberg.

   Symposium on Theoretical Aspects of Computer Science (STACS) 2017

   PDF

   We apply Stone duality and model theory to study the structure theory of free pro-aperiodic monoids. Stone duality implies that elements of the free pro-aperiodic monoid may be viewed as elementary equivalence classes of pseudofinite words. Model theory provides us with saturated words in each such class, i.e., words in which all possible factorizations are realized. We give several applications of this new approach, including a solution to the word problem for omega-terms that avoids using McCammond’s normal forms, as well as new proofs and extensions of other structural results concerning free pro-aperiodic monoids.

2016

1. Monadic second order logic as the model companion of temporal logic.

   Silvio Ghilardi and Sam van Gool.

   Logic in Computer Science (LICS) 2016

   PDF

   The main focus of this paper is on bisimulation-invariant MSO, and more particularly on giving a novel model-theoretic approach to it. In model theory, a model companion of a theory is a first- order description of the class of models in which all potentially solvable systems of equations and non-equations have solutions. We show that bisimulation-invariant MSO on trees gives the model companion for a new temporal logic, “fair CTL”, an enrichment of CTL with local fairness constraints. To achieve this, we give a completeness proof for the logic fair CTL which combines tableaux and Stone duality, and a fair CTL encoding of the automata for the modal μ-calculus. Moreover, we also show that MSO on binary trees is the model companion of binary deterministic fair CTL.

2015

1. Duality and universal models for the meet-implication fragment of IPC.

   Nick Bezhanishvili, Dion Coumans, Sam van Gool, and Dick de Jongh.

   Tbilisi Symposium on Language, Logic and Computation (TbiLLC) 2015

   arXiv PDF

2014

1. Free algebras for Gödel-Löb provability logic.

   Sam van Gool

   Advances in Modal Logic 2014

   PDF

   We give a construction of finitely generated free algebras for Gödel-Löb provability logic, GL. On the semantic side, this construction yields a notion of canonical graded model for GL and a syntactic definition of those normal forms which are consistent with GL. Our two main techniques are incremental constructions of free algebras and finite duality for partial modal algebras. In order to apply these techniques to GL, we use a rule-based formulation of the logic GL by Avron (which we simplify slightly), and the corresponding semantic characterization that was recently obtained by Bezhanishvili and Ghilardi.

2. Sheaf representations of MV-algebras and lattice-ordered abelian groups via duality.

   Mai Gehrke, Sam van Gool, and Vincenzo Marra.

   Journal of Algebra 2014

   arXiv PDF

   We study representations of MV-algebras — equivalently, unital lattice-ordered abelian groups — through the lens of Stone-Priestley duality, using canonical extensions as an essential tool. Specifically, the theory of canonical extensions implies that the (Stone-Priestley) dual spaces of MV-algebras carry the structure of topological partial commutative ordered semigroups. We use this structure to obtain two different decompositions of such spaces, one indexed over the prime MV-spectrum, the other over the maximal MV-spectrum. These decompositions yield sheaf representations of MV-algebras, using a new and purely duality-theoretic result that relates certain sheaf representations of distributive lattices to decompositions of their dual spaces. Importantly, the proofs of the MV-algebraic representation theorems that we obtain in this way are distinguished from the existing work on this topic by the following features: (1) we use only basic algebraic facts about MV-algebras; (2) we show that the two aforementioned sheaf representations are special cases of a common result, with potential for generalizations; and (3) we show that these results are strongly related to the structure of the Stone-Priestley duals of MV-algebras. In addition, using our analysis of these decompositions, we prove that MV-algebras with isomorphic underlying lattices have homeomorphic maximal MV-spectra. This result is an MV-algebraic generalization of a classical theorem by Kaplansky stating that two compact Hausdorff spaces are homeomorphic if, and only if, the lattices of continuous [0,1]-valued functions on the spaces are isomorphic.

3. On sheaves and duality.

   Sam van Gool

   PhD thesis, Radboud University Nijmegen 2014

   PDF

2013

1. Distributive envelopes and topological duality for lattices via canonical extensions.

   Mai Gehrke and Sam van Gool.

   Order 2013

   arXiv PDF

   We establish a topological duality for bounded lattices. The two main features of our duality are that it generalizes Stone duality for bounded distributive lattices, and that the morphisms on either side are not the standard ones. A positive consequence of the choice of morphisms is that those on the topological side are functional. Towards obtaining the topological duality, we develop a universal construction which associates to an arbitrary lattice two distributive lattice envelopes with a Galois connection between them. This is a modification of a construction of the injective hull of a semilattice by Bruns and Lakser, adjusting their concept of ‘admissibility’ to the finitary case. Finally, we show that the dual spaces of the distributive envelopes of a lattice coincide with completions of quasi-uniform spaces naturally associated with the lattice, thus giving a precise spatial meaning to the distributive envelopes.

2. A non-commutative Priestley duality.

   Andrej Bauer, Karin Cvetko-Vah, Mai Gehrke, Sam van Gool, and Ganna Kudryavtseva.

   Topology and its Applications 2013

   arXiv PDF

   We prove that the category of left-handed strongly distributive skew lattices with zero and proper homomorphisms is dually equivalent to a category of sheaves over local Priestley spaces. Our result thus provides a non-commutative version of classical Priestley duality for distributive lattices and generalizes the recent development of Stone duality for skew Boolean algebras. From the point of view of skew lattices, Leech showed early on that any strongly distributive skew lattice can be embedded in the skew lattice of partial functions on some set with the operations being given by restriction and so-called override. Our duality shows that there is a canonical choice for this embedding. Conversely, from the point of view of sheaves over Boolean spaces, our results show that skew lattices correspond to Priestley orders on these spaces and that skew lattice structures are naturally appropriate in any setting involving sheaves over Priestley spaces.

3. On generalizing free algebras for a functor.

   Dion Coumans and Sam van Gool.

   Journal of Logic and Computation 2013

   PDF

   In this paper we introduce a new setting, based on partial algebras, for studying con- structions of finitely generated free algebras. We give sufficient conditions under which the finitely generated free algebras for a variety V may be described as the colimit of a chain of finite partial algebras obtained by repeated application of a functor. In particular, our method encompasses the construction of finitely generated free algebras for varieties of algebras for a functor as in [2], Heyting algebras as in [1] and S4 algebras as in [8].

2012

1. Duality and canonical extensions for stably compact spaces.

   Sam van Gool

   Topology and its Applications 2012

   arXiv PDF

   We construct a canonical extension for strong proximity lattices in order to give an algebraic, point-free description of a finitary duality for stably compact spaces. In this setting not only morphisms, but also objects may have distinct π- and σ-extensions.

2010

1. Disjunctive questions, intonation and highlighting.

   Sam van Gool and Floris Roelofsen.

   Logic, Language and Meaning 2010

   arXiv PDF

   This paper examines how intonation affects the interpretation of disjunctive questions. The semantic effect of a question is taken to be three-fold. First, it raises an issue. In the tradition of inquisitive semantics, we model this by assuming that a question proposes several possible updates of the common ground (several possibilities for short) and invites other participants to help establish at least one of these updates. But apart from raising an issue, a question may also highlight and/or suggest certain possibilities, and intonation determines to a large extent which possibilities are highlighted/suggested.