Sam van Gool

Selected Publications

1. Formalizing and Computing Propositional Quantifiers.

   Hugo Férée and Sam van Gool.

   Certified Proofs and Programs (CPP) 2023

   PDF

   A surprising result of Pitts (1992) says that propositional quantifiers are definable internally in intuitionistic propositional logic (IPC). The main contribution of this paper is to provide a formalization of Pitts’ result in the Coq proof assistant, and thus a verified implementation of Pitts’ construction. We in addition provide an OCaml program, extracted from the Coq formalization, which computes propositional formulas that realize intuitionistic versions of ∃p φ and ∀p φ from p and φ.

2. On duality and model theory for polyadic spaces.

   Sam van Gool and Jérémie Marquès.

   2022

   arXiv

   This paper is a study of first-order coherent logic from the point of view of duality and categorical logic. We start by characterizing the Priestley duals of coherent hyperdoctrines, the algebraization we take for coherent logic, as the open polyadic Priestley spaces. We then prove completeness, omitting types, and Craig interpolation theorems from this order-topological point of view. Our approach emphasizes the role of interpolation and openness properties, and allows for a modular, syntax-free treatment of these model-theoretic results. As further applications of the same method, we prove completeness theorems for constant domain and Gödel-Dummett intuitionistic predicate logics.

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

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

5. 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.

6. 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.

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

8. 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.