Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A categorical account of composition methods in logic (extended version)

Tomáš Jakl, Dan Marsden, Nihil Shah

TL;DR

We develop a categorical, parameterised framework for composition methods in finite model theory by deploying game comonads to capture logics and model-comparison games. The approach yields abstract Feferman–Vaught–Mostowski type theorems that hold uniformly across logics, operations, and model classes, covering positive existential, existential, counting, and full fragments, with resource-bounded variants (e.g., quantified by $k$). Central ideas include lifting operations to coalgebras via Kleisli laws, and using open pathwise-embeddings to transfer equivalences through product and coproduct constructions, revealing connections to bilinear maps in monad theory. The results recover classical theorems (e.g., Mostowski, cospectrality refinements) and provide modular, semantically grounded proofs for product theorems and enrichments, with implications for algorithmic meta-theorems and potentially MSO via enrichment in future work.

Abstract

We present a categorical theory of the composition methods in finite model theory -- a key technique enabling modular reasoning about complex structures by building them out of simpler components. The crucial results required by the composition methods are Feferman--Vaught--Mostowski (FVM) type theorems, which characterize how logical equivalence behaves under composition and transformation of models. Our results are developed by extending the recently introduced game comonad semantics for model comparison games. This level of abstraction allow us to give conditions yielding FVM type results in a uniform way. Our theorems are parametric in the classes of models, logics and operations involved. Furthermore, they naturally account for the existential and positive existential fragments, and extensions with counting quantifiers of these logics. We also reveal surprising connections between FVM type theorems, and classical concepts in the theory of monads. We illustrate our methods by recovering many classical theorems of practical interest, including a refinement of a previous result by Dawar, Severini, and Zapata concerning the 3-variable counting logic and cospectrality. To highlight the importance of our techniques being parametric in the logic of interest, we prove a family of FVM theorems for products of structures, uniformly in the logic in question, which cannot be done using specific game arguments. This is an extended version of the LiCS 2023 conference paper of the same name.

A categorical account of composition methods in logic (extended version)

TL;DR

We develop a categorical, parameterised framework for composition methods in finite model theory by deploying game comonads to capture logics and model-comparison games. The approach yields abstract Feferman–Vaught–Mostowski type theorems that hold uniformly across logics, operations, and model classes, covering positive existential, existential, counting, and full fragments, with resource-bounded variants (e.g., quantified by ). Central ideas include lifting operations to coalgebras via Kleisli laws, and using open pathwise-embeddings to transfer equivalences through product and coproduct constructions, revealing connections to bilinear maps in monad theory. The results recover classical theorems (e.g., Mostowski, cospectrality refinements) and provide modular, semantically grounded proofs for product theorems and enrichments, with implications for algorithmic meta-theorems and potentially MSO via enrichment in future work.

Abstract

We present a categorical theory of the composition methods in finite model theory -- a key technique enabling modular reasoning about complex structures by building them out of simpler components. The crucial results required by the composition methods are Feferman--Vaught--Mostowski (FVM) type theorems, which characterize how logical equivalence behaves under composition and transformation of models. Our results are developed by extending the recently introduced game comonad semantics for model comparison games. This level of abstraction allow us to give conditions yielding FVM type results in a uniform way. Our theorems are parametric in the classes of models, logics and operations involved. Furthermore, they naturally account for the existential and positive existential fragments, and extensions with counting quantifiers of these logics. We also reveal surprising connections between FVM type theorems, and classical concepts in the theory of monads. We illustrate our methods by recovering many classical theorems of practical interest, including a refinement of a previous result by Dawar, Severini, and Zapata concerning the 3-variable counting logic and cospectrality. To highlight the importance of our techniques being parametric in the logic of interest, we prove a family of FVM theorems for products of structures, uniformly in the logic in question, which cannot be done using specific game arguments. This is an extended version of the LiCS 2023 conference paper of the same name.
Paper Structure (23 sections, 34 theorems, 104 equations, 1 figure)

This paper contains 23 sections, 34 theorems, 104 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Categories of Relational Structures
  4. Comonads
  5. FVM theorems for positive existential fragments
  6. Examples
  7. FVM theorems for counting logic
  8. Kleisli category
  9. Kleisli laws
  10. Examples
  11. Coalgebras and open pathwise-embeddings
  12. Lifting operations to coalgebras
  13. Open pathwise-embeddings and their preservation
  14. FVM theorems for the full logic
  15. Heteromorphisms
  16. ...and 8 more sections

Key Result

Lemma 2.1

Every comonad in Kleisli form $(\mathbb C, \varepsilon, (-)^*)$ induces a comonad in comonoid form $(\mathbb C, \varepsilon, \delta)$ where $\mathbb C$ is extended to morphisms by setting $\mathbb C(f\colon A \to B) = (f \circ \varepsilon_A)^*$ and $\delta_A$ is the coextension of the identity morph

Figures (1)

  • Figure :

Theorems & Definitions (88)

  • Lemma 2.1
  • Theorem 2.2: AbramskyDW17abramsky2021relating
  • Remark 3.1
  • Theorem 3.2
  • proof
  • Remark 3.3: Infinitary Operations
  • Example 3.4
  • Example 3.5: Counterexample
  • Example 3.6
  • Example 3.7
  • ...and 78 more