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定理不能推广到布尔半环之外。对于句子，它在自然半环和热带半环中也失效。然而，我们的主要结果是关于最小-最大半环和格半环存在Gaifman范式的构造性证明。该证明蕴含了布尔语义中Gaifman经典定理的一个更强版本：每个句子都有一个不添加否定词的Gaifman范式。