First-Order Modal Logic via Logical Categories
Silvio Ghilardi, Jérémie Marquès
TL;DR
The paper presents a categorical approach to quantified modal logic by defining modal categories: lex categories equipped with a stable factorization system and a modal lattice structure on subobjects, allowing modalities to act directly on subobjects. It proves a Joyal-style representation theorem embedding small modal categories into relational $G$-sets, with saturation conditions yielding conservative representations and enabling quotients and disjoint unions to form modal quasi-pretoposes. It develops a comprehensive theory of saturation (SS, FS, IS) and modal transformations, then extends to quotients and disjoint sums, culminating in a powerful completeness framework for modal first-order theories via syntactic modal categories. The framework aims to unify semantic relational models, syntactic theories, and structural features like quotients and disjoint unions, with potential impact on description logics and higher-order modal reasoning.
Abstract
We extend the logical categories framework to first order modal logic. In our modal categories, modal operators are applied directly to subobjects and interact with the background factorization system. We prove a Joyal-style representation theorem into relational structures formalizing a `counterpart' notion. We investigate saturation conditions related to definability questions and we enrich our framework with quotients and disjoint sums, thus leading to the notion of a modal (quasi) pretopos. We finally show how to build syntactic categories out of first order modal theories.