arXiv subjects

Sam van Gool

Publications and source records attributed to Sam van Gool.

15 recordsLinked to original sources

arXiv2026

The points of canonical extensions of doctrines

We analyse the space of points of the canonical extension of a coherent doctrine. We first give a full characterisation of doctrine morphisms that are extensible, and relate it to the existing notion of p-model of a coherent category. Through this characterisation, the extensible morphisms are shown to be exactly those which are {\omega}-saturated in the sense of coherent first-order logic. Next, we answer the question: when does a presheaf of models fully describe the canonical extension? We prove a characterisation theorem via two conditions, which are again natural from the perspective of coherent logic, namely, homogeneity and the realisation of all prime types in a strict sense. The characterisation theorem allows us to deduce a reconstruction result for any coherent theory with the property that all prime types can be realised in a countable, saturated model. For instance, {\omega}-stable coherent theories always have this property. We conclude by explaining how our results can be interpreted topos-theoretically, by relating them to the classifying topos and to the topos of types.

math.CT↗

arXiv2025

Uniform Interpolation

Uniform interpolation is a strengthening of interpolation that holds for certain propositional logics. The starting point of this chapter is a theorem of A. Pitts, which shows that uniform interpolation holds for intuitionistic propositional logic. We outline how this theorem may be proved semantically via the definability of bisimulation quantifiers, and how it generalizes to an open mapping theorem between Esakia spaces. We also discuss connections between uniform interpolation and research in categorical logic, algebra, and model theory.

math.LO↗

arXiv2025

Toposes with enough points as categories of \'etale spaces

We extend Makkai duality between coherent toposes and ultracategories to a duality between toposes with enough points and ultraconvergence spaces. Our proof generalizes and simplifies Makkai's original proof. Our main result can also be seen as an extension to ionads of Barr's equivalence between topological spaces and relational modules for the ultrafilter monad. In view of the correspondence between toposes and geometric theories, we obtain a strong conceptual completeness theorem, in the sense of Makkai, for geometric theories with enough Set-models. The same result has recently been obtained independently by Saadia (arXiv:2506.23935) and by Hamad (arXiv:2507.07922). Both of their proofs rely on groupoid representations of toposes, which our proof here does not assume.

math.CT↗

arXiv2025

Learning Weighted Automata over Number Rings, Concretely and Categorically

We develop a generic reduction procedure for active learning problems. Our approach is inspired by a recent polynomial-time reduction of the exact learning problem for weighted automata over integers to that for weighted automata over rationals (Buna-Marginean et al. 2024). Our procedure improves the efficiency of a category-theoretic automata learning algorithm, and poses new questions about the complexity of its implementation when instantiated to concrete categories. As our second main contribution, we address these complexity aspects in the concrete setting of learning weighted automata over number rings, that is, rings of integers in an algebraic number field. Assuming a full representation of a number ring OK, we obtain an exact learning algorithm of OK-weighted automata that runs in polynomial time in the size of the target automaton, the logarithm of the length of the longest counterexample, the degree of the number field, and the logarithm of its discriminant. Our algorithm produces an automaton that has at most one more state than the minimal one, and we prove that doing better requires solving the principal ideal problem, for which the best currently known algorithm is in quantum polynomial time.

cs.FL↗

arXiv2024

Mechanised uniform interpolation for modal logics K, GL, and iSL

The uniform interpolation property in a given logic can be understood as the definability of propositional quantifiers. We mechanise the computation of these quantifiers and prove correctness in the Coq proof assistant for three modal logics, namely: (1) the modal logic K, for which a pen-and-paper proof exists; (2) G\"odel-L\"ob logic GL, for which our formalisation clarifies an important point in an existing, but incomplete, sequent-style proof; and (3) intuitionistic strong L\"ob logic iSL, for which this is the first proof-theoretic construction of uniform interpolants. Our work also yields verified programs that allow one to compute the propositional quantifiers on any formula in this logic.

cs.LO↗

arXiv2023

Profinite lambda-terms and parametricity

Combining ideas coming from Stone duality and Reynolds parametricity, we formulate in a clean and principled way a notion of profinite lambda-term which, we show, generalizes at every type the traditional notion of profinite word coming from automata theory. We start by defining the Stone space of profinite lambda-terms as a projective limit of finite sets of usual lambda-terms, considered modulo a notion of equivalence based on the finite standard model. One main contribution of the paper is to establish that, somewhat surprisingly, the resulting notion of profinite lambda-term coming from Stone duality lives in perfect harmony with the principles of Reynolds parametricity. In addition, we show that the notion of profinite lambda-term is compositional by constructing a cartesian closed category of profinite lambda-terms, and we establish that the embedding from lambda-terms modulo beta-eta-conversion to profinite lambda-terms is faithful using Statman's finite completeness theorem. Finally, we prove that the traditional Church encoding of finite words into lambda-terms can be extended to profinite words, and leads to a homeomorphism between the space of profinite words and the space of profinite lambda-terms of the corresponding Church type.

cs.LO↗

arXiv2023

Deciding Equations in the Time Warp Algebra

Join-preserving maps on the discrete time scale $\omega^+$, referred to as time warps, have been proposed as graded modalities that can be used to quantify the growth of information in the course of program execution. The set of time warps forms a simple distributive involutive residuated lattice -- called the time warp algebra -- that is equipped with residual operations relevant to potential applications. In this paper, we show that although the time warp algebra generates a variety that lacks the finite model property, it nevertheless has a decidable equational theory. We also describe an implementation of a procedure for deciding equations in this algebra, written in the OCaml programming language, that makes use of the Z3 theorem prover.

cs.LO↗

arXiv2022

On duality and model theory for polyadic spaces

This paper is a study of first-order coherent logic from the point of view of duality and categorical logic. We prove a duality theorem between coherent hyperdoctrines and open polyadic Priestley spaces, which we subsequently apply to prove completeness, omitting types, and Craig interpolation theorems for coherent or intuitionistic logic. 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\"odel-Dummett intuitionistic predicate logics.

math.LO↗

arXiv2022

Topological Duality for Distributive Lattices: Theory and Applications

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.

math.LO↗

arXiv2022

First-order separation over countable ordinals

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 $\omega$-words. For this, we develop the algebraic concept of monoid (resp. $\omega$-semigroup, resp. ordinal monoid) with aperiodic merge, an extension of monoids (resp. $\omega$-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.

cs.LO↗

arXiv2021

Time Warps, from Algebra to Algorithms

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.

math.LO↗

arXiv2020

Priestley duality for MV-algebras and beyond

We provide a new perspective on extended Priestley duality for a 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.

math.LO↗

arXiv2018

An interpolant in predicate G\"odel logic

A logic satisfies the interpolation property provided that whenever a formula {\Delta} is a consequence of another formula {\Gamma}, then this is witnessed by a formula {\Theta} which only refers to the language common to {\Gamma} and {\Delta}. That is, the relational (and functional) symbols occurring in {\Theta} occur in both {\Gamma} and {\Delta}, {\Gamma} has {\Theta} as a consequence, and {\Theta} has {\Delta} 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\"odel logic does. In this short note, we show that their counterexample for constant domain intuitionistic logic does admit an interpolant in predicate G\"odel logic. While this has no impact on settling the question for predicate G\"odel 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.

math.LO↗

arXiv2012

A non-commutative Priestley duality

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.

math.RA↗

arXiv2010

Duality and canonical extensions for stably compact spaces

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 pi- and sigma-extensions.

math.GN↗