Locality Theorems in Semiring Semantics

TL;DR

The paper studies locality properties of first-order logic under semiring semantics, linking locality to the algebraic properties of the underlying semiring $K=(K,+,\cdot,0,1)$. It proves that Hanf locality generalizes to all fully idempotent semirings (where both $+$ and $\cdot$ are idempotent). Gaifman locality exhibits a mixed behavior: Gaifman's normal form fails for formulae with free variables beyond the Boolean semiring, and fails for sentences in the natural semiring and the tropical semiring. Yet it provides a constructive Gaifman normal form for min-max and lattice semirings, and shows that in the Boolean setting every sentence has a Gaifman normal form that does not introduce new negations.

Abstract

Semiring semantics of first-order logic generalises classical Boolean semantics by permitting truth values from a commutative semiring, which can model information such as costs or access restrictions. This raises the question to what extent classical model theoretic properties still apply, and how this depends on the algebraic properties of the semiring. In this paper, we study this question for the classical locality theorems due to Hanf and Gaifman. We prove that Hanf's Locality Theorem generalises to all semirings with idempotent operations, but fails for many non-idempotent semirings. We then consider Gaifman normal forms and show that for formulae with free variables, Gaifman's Theorem does not generalise beyond the Boolean semiring. Also for sentences, it fails in the natural semiring and the tropical semiring. Our main result, however, is a constructive proof of the existence of Gaifman normal forms for min-max and lattice semirings. The proof implies a stronger version of Gaifman's classical theorem in Boolean semantics: every sentence has a Gaifman normal form which does not add negations.