Piecewise Interpretations in Many-Sorted Logic
Abstract
Piecewise interpretations, introduced by Visser, generalize ordinary interpretations between first-order theories by allowing formulae to be interpreted using disjoint unions of definable sets. This makes it possible to capture natural constructions, such as the projective completion of an affine plane, but also leads to a notion of equivalence of theories, namely piecewise bi-interpretability. We develop the theory of piecewise interpretations systematically in the many-sorted setting. Each piecewise interpretation induces a semantic dual, a functor between categories of models. In addition, we introduce a syntactic notion of morphism between piecewise interpretations, which likewise has a semantic dual. Using these semantic duals, we collect theories, piecewise interpretations, and morphisms between them into a bicategory, in particular defining a well-behaved notion of composition of interpretations, associative up to coherent isomorphism. As an application, we consider a familiar idea, championed by Quine, namely that one can replace any many-sorted theory with a corresponding single-sorted one by replacing sorts with sortal predicates. We show that this leads to a biequivalence between the developed bicategories of theories with finitely many sorts and single-sorted theories, thereby providing an argument for the dispensability of sorts.
Related
- Many-Sorted Algebraic Semantics for Dimensional Quantity Calculus
- Higher-order many-sorted categorial algebras via generalized hep-derivors
- How many sorted projections determine n points in k dimensions?
- Sorted Mutability as an Entropic Functional: Theory and Two Applications
- Distribution of the inversion statistic on run-sorted permutations
BibTeX
@misc{zayton2026piecewise,
title = {{Piecewise Interpretations in Many-Sorted Logic}},
author = {Benjamin Zayton},
howpublished = {arXiv},
year = {2026},
month = nov,
doi = {10.48550/arxiv.2611.14552},
eprint = {2611.14552},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2611.14552},
note = {CC BY 4.0},
}
RIS
TY - UNPB
TI - Piecewise Interpretations in Many-Sorted Logic
AU - Benjamin Zayton
PY - 2026
DA - 2026/11/02
PB - arXiv
DO - 10.48550/arxiv.2611.14552
UR - https://arxiv.org/abs/2611.14552
AB - Piecewise interpretations, introduced by Visser, generalize ordinary interpretations between first-order theories by allowing formulae to be interpreted using disjoint unions of definable sets. This makes it possible to capture natural constructions, such as the projective completion of an affine plane, but also leads to a notion of equivalence of theories, namely piecewise bi-interpretability. We develop the theory of piecewise interpretations systematically in the many-sorted setting. Each piecewise interpretation induces a semantic dual, a functor between categories of models. In addition, we introduce a syntactic notion of morphism between piecewise interpretations, which likewise has a semantic dual. Using these semantic duals, we collect theories, piecewise interpretations, and morphisms between them into a bicategory, in particular defining a well-behaved notion of composition of interpretations, associative up to coherent isomorphism. As an application, we consider a familiar idea, championed by Quine, namely that one can replace any many-sorted theory with a corresponding single-sorted one by replacing sorts with sortal predicates. We show that this leads to a biequivalence between the developed bicategories of theories with finitely many sorts and single-sorted theories, thereby providing an argument for the dispensability of sorts.
ER -