Enriched concepts of regular logic
Jiří Rosický, Giacomo Tendas
TL;DR
This work develops enriched regular logic by allowing function and relation symbols with arities in the enrichment base $\mathcal{V}$ and interpreting existential quantification via an enriched factorization system $(\mathcal{E},\mathcal{M})$. It defines the $\mathcal{V}$-category of $\mathbb{L}$-structures $\operatorname{\bf Str}({\mathbb L})$, introduces presentation formulas for $\lambda$-presentable structures, and develops a semantics for atomic and regular formulas (including positive-primitive ones). The main result shows that, under suitable hypotheses on $\mathcal{V}$ and $(\mathcal{E},\mathcal{M})$, the enriched $(\lambda,\mathcal{E})$-injectivity classes in $\operatorname{Str}(\mathbb{L})$ coincide with models of regular $\mathbb{L}_{\lambda\lambda}$-theories, yielding equivalent characterizations via injectivity and via logical theories; this extends internal logic from toposes to more general enrichment bases. The paper provides concrete bases (e.g., $\mathbf{Met}$, $\mathbf{Ban}$, $\mathbf{Ab}$, $\mathbf{Cat}$) and discusses limitations (e.g., Frobenius failures when $\mathcal{E}$ is not pullback-stable) and potential generalizations to broader bases, connecting enriched model theory with presentation theory and purity.
Abstract
Building on our previous work on enriched universal algebra, we define a notion of enriched language consisting of function and relation symbols whose arities are objects of the base of enrichment. In this context, we construct atomic formulas and define the regular fragment of enriched logic by taking conjunctions and existential quantifications of those. We then characterize enriched categories of models of regular theories as enriched injectivity classes in the enriched category of structures. These notions rely on the choice of a factorization system on the base of enrichment which will be used to interpret relation symbols and existential quantifications.