Centrala begrepp
Semiring semantics of first-order logic generalizes classical Boolean semantics by allowing truth values from a commutative semiring. This raises the question of how classical model-theoretic properties, such as locality theorems, extend to semiring semantics. The paper studies the generalization of Hanf's and Gaifman's locality theorems, showing that Hanf's theorem holds for all semirings, but Gaifman's theorem only holds for certain semirings like min-max and lattice semirings.
Sammanfattning
The paper investigates the extent to which classical locality theorems in first-order logic, such as Hanf's and Gaifman's theorems, generalize to semiring semantics. Semiring semantics extends classical Boolean semantics by allowing truth values from a commutative semiring, which can model additional information like costs or access restrictions.
The key findings are:
Hanf's locality theorem generalizes to all fully idempotent semirings, where both addition and multiplication are idempotent. However, it fails for many non-idempotent semirings.
For formulae with free variables, Gaifman's normal form theorem does not generalize beyond the Boolean semiring. The paper provides counterexamples showing that Gaifman normal forms may not exist in the natural semiring and the tropical semiring.
The main positive result is a constructive proof of the existence of Gaifman normal forms for first-order sentences in min-max and lattice semirings. This proof also leads to a stronger version of Gaifman's theorem in classical Boolean semantics, where every sentence has a Gaifman normal form without introducing new negations.
The paper provides a detailed analysis of how the algebraic properties of the underlying semiring affect the generalization of classical locality theorems. The results highlight the challenges in extending fundamental model-theoretic concepts from Boolean to semiring semantics, and identify the specific semirings where locality properties can be preserved.