Existential and positive games: a comonadic and axiomatic view
By: Samson Abramsky, Thomas Laure, Luca Reggio
Potential Business Impact:
Helps computers understand logic puzzles better.
A number of model-comparison games central to (finite) model theory, such as pebble and Ehrenfeucht-Fra\"{i}ss\'{e} games, can be captured as comonads on categories of relational structures. In particular, the coalgebras for these comonads encode in a syntax-free way preservation of resource-indexed logic fragments, such as first-order logic with bounded quantifier rank or a finite number of variables. In this paper, we extend this approach to existential and positive fragments (i.e., without universal quantifiers and without negations, respectively) of first-order and modal logic. We show, both concretely and at the axiomatic level of arboreal categories, that the preservation of existential fragments is characterised by the existence of so-called pathwise embeddings, while positive fragments are captured by a newly introduced notion of positive bisimulation. As an application, we offer a new proof of an equi-resource Lyndon positivity theorem for (multi)modal logic.
Similar Papers
Complete First-Order Game Logic
Logic in Computer Science
Makes math logic and computer game logic the same.
First-Order Modal Logic via Logical Categories
Logic in Computer Science
Makes computers understand logic better.
A General (Uniform) Relational Semantics for Sentential Logics
Logic in Computer Science
Makes many different logic systems work the same.