Speaker
Dan Marsden, University of Nottingham School of Computer Science
Title
A Categorical Account of Composition Methods in Logic
Abstract
This talk will present a categorical theory of 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 the composition and transformation of models.
We will present recent results developed by extending the game comonad semantics for model comparison games. This level of abstraction allows 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 positive existential fragment 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.
(Joint work with Tomáš Jakl and Nihil Shah)
Slides
A Categorical Account of Composition Methods in Logic
