Preservation Theorems in Semiring Semantics

TL;DR

This paper investigates how classical preservation theorems from model theory extend to semiring semantics, revealing that some hold for lattice semirings while others fail for many common semirings.

Contribution

It establishes which preservation theorems are valid in semiring semantics, especially for lattice semirings, and highlights differences from classical Boolean logic.

Findings

Preservation theorems hold for all lattice semirings.

Existential preservation fails for many semirings like tropical and Viterbi.

Existential preservation holds for finite interpretations in several semirings.

Abstract

We study the status of preservation theorems such as the {\L}o\'s-Tarski theorem and the homomorphism preservation theorem in the context of semiring semantics. Semiring semantics has its origins in the provenance analysis of database queries. Depending on the underlying semiring, it allows us to track which atomic facts are responsible for the truth of a statement or practical information about the evaluation such as costs or confidence. The systematic development of semiring semantics for first-order logic and other logical systems raises the question to what extent classical model-theoretic results can be generalised to this setting and how such results depend on the underlying semiring. The definitions of semantic properties such as preservation under extensions, substructures, or homomorphisms naturally generalise to the setting of semiring semantics. However, the status of the corresponding preservation theorem strongly depends on the algebraic properties of the particular semirings. We prove that these preservation theorems do indeed hold for all lattice semirings (a quite large class, encompassing practically relevant semirings and in particular all min-max semirings). The proofs combine adaptations of the classical compactness and amalgamation methods with specific reduction methods for logical entailment that have been developed in semiring semantics. On the other side, variants of the existential preservation theorem fail for many other semirings, including the tropical semiring, the Viterbi semiring, the {\L}ukasiewicz semiring, and the natural semiring. Surprisingly, the existential preservation theorem does hold for finite interpretations in a number of semirings, including all lattice semirings. Thus, the situation for these semirings is in sharp contrast to the Boolean case, where the {\L}o\'s-Tarski theorem holds in general, but not in the finite.