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 extend 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.

翻译：一阶逻辑的半环语义通过允许来自交换半环的真值（可模拟成本或访问限制等信息），推广了经典的布尔语义。这引发了一个问题：经典模型论性质在多大程度上仍然适用，以及这如何依赖于半环的代数性质。本文针对汉夫和盖夫曼的经典局域性定理研究了该问题。我们证明汉夫局域性定理可推广至所有具有幂等运算的半环，但在许多非幂等半环中失效。随后考虑盖夫曼范式，结果表明对于含自由变量的公式，盖夫曼定理无法推广至布尔半环之外。对于语句，该定理在自然数半环和热带半环中同样失效。然而，我们的主要贡献在于：针对极大-极小半环和格半环，给出了盖夫曼范式存在性的构造性证明。该证明蕴含了布尔语义下盖夫曼经典定理的一个更强版本：每个语句均存在不引入否定运算的盖夫曼范式。