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.

翻译：一阶逻辑的半环语义通过允许真值取自交换半环，推广了经典的布尔语义，从而能够对诸如成本或访问限制等信息进行建模。这引发了一个问题：经典模型论性质在多大程度上仍然适用，以及这如何依赖于半环的代数性质。在本文中，我们针对由Hanf和Gaifman提出的经典局部性定理研究了这个问题。我们证明了Hanf局部性定理可以推广到所有具有幂等运算的半环，但在许多非幂等半环中不成立。接着，我们考虑Gaifman范式，并证明对于含有自由变量的公式，Gaifman定理无法推广到布尔半环之外。即使对于句子，它在自然数半环和热带半环中也不成立。然而，我们的主要结果是构造性地证明了min-max半环和格半环中Gaifman范式的存在性。该证明蕴含了布尔语义中Gaifman经典定理的一个更强版本：每个句子都有一个不增加否定词的Gaifman范式。