Locality in Residuated-Lattice Structures
James Carr
TL;DR
The paper investigates whether classical locality results from finite model theory extend to many‑valued first‑order logics defined over residuated lattices. It develops a pair of syntactic and semantic tools—k‑isomorphism types and distance‑based neighborhood encoding—to adapt Hanf and Gaifman locality to this nonclassical setting, highlighting how an order‑defining connective is crucial to connect syntax and semantics. The authors show that Hanf locality fails for natural distances in general residuated lattices but can be recovered under a strict $\bot$‑threshold distance in bounded, well‑connected algebras, and that Gaifman locality can be recovered under restrictions (witnessed models, residuated chains with a co‑atom) using Gaifman‑style distance formulas. They further compare with semiring locality results, discuss definability of queries, and illustrate the approach with locality examples, outlining open questions about relaxing assumptions and extending to infinite models.
Abstract
Many-valued models generalise the structures from classical model theory by defining truth values for a model with an arbitrary algebra. Just as algebraic varieties provide semantics for many non-classical propositional logics, models defined over algebras in a variety provide the semantics for the corresponding non-classical predicate logics. In particular, models defined over varieties of residuated lattices represent the model theory for first-order substructural logics. In this paper we study the extent to which the classical locality theorems from Hanf and Gaifman hold true in the residuated lattice setting. We demonstrate that the answer is sensitive both to how locality is understood in the generalised context and the behaviour of the truth-defining algebra. In the case of Hanf's theorem, we will show that the theorem fails for the natural understanding of local neighbourhoods, but is recoverable with an alternative understanding for well-connected residuated lattices. For Gaifman's theorem, rather than consider Gaifman normal forms directly we focus on the main lemma of the theorem from textbook proofs - that models which satisfy the same basic local sentences are elementarily equivalent. We prove that for a number of different understandings of locality, provided the algebra is well-behaved enough to express locality in its syntax, this main lemma can be recovered. In each case we will see the importance of an order-interpreting connective which creates a link between the modelling relation for models and formulas and the valuation function from formulas into the algebra. This link enables a syntactic encoding of back-and-forth systems providing the main technical ingredient to proofs of the main locality results.