Semiring semantics: algebraic foundations, model theory, and strategy analysis

Semiring semantics generalizes classical semantics by replacing the classical domain of Boolean truth values with a commutative semiring $\mathcal{S}$. A logical formula $\psi$ is not evaluated to true or false, but instead to an element $[\![ \psi ]\!]$ from the semiring $\mathcal{S}$. A valuation of zero is usually interpreted as “false”, whereas a nonzero element represents “true” and carries additional information depending on the semiring $\mathcal{S}$ in question. For example, polynomial semirings $\mathbb{N}[X]$ may be used to perform provenance analysis, where the polynomial $[\![ \psi ]\!]$ provides a detailed overview of the facts that contribute to the truth of $\psi$ in a certain model. In first-order logic, semiring addition is used to evaluate disjunctions and existential quantifiers, while multiplication is used for conjunctions and universal quantifiers. Classical models are replaced with semiring interpretations which assign a semiring element to each literal of a model. This prompts the introduction of model theory to the semiring setting. Since model-theoretic properties of semiring semantics vary significantly depending on the semiring $\mathcal{S}$, we first provide an overview of semiring algebra, focusing in particular on semirings with infinitary operations and polynomial semirings. We further introduce separating homomorphisms as an important algebraic tool in semiring model theory, which can be applied to gain insights on semiring semantics by reduction to classical Boolean semantics. In contrast to classical model theory, we show that elementary equivalence on finite semiring interpretations does not coincide with isomorphism on large classes of semirings, such as the class of fully idempotent semirings with at least three elements, but first-order axiomatization of finite semiring interpretations is still possible on some specific semirings such as $\mathbb{N}$. Additionally, we generalize the classical compactness theorem to the semiring setting and prove that it holds on finite semirings with suitable algebraic properties. We also study semiring semantics in the field of game theory. The underlying idea is that positions $v$ in a game $\mathcal{G}$ are evaluated to some semiring element $\mathcal{G} [\![ v ]\!] \in \mathcal{S}$, based on “initial” semiring valuations $\ell$ of the positions and actions in $\mathcal{G}$. It is known that the sum of strategies theorem holds in this setting: The final valuation $\mathcal{G} [\![ v ]\!]$ corresponds to the sum of the valuations of all strategies starting from $v$. We extend semiring semantics to games with imperfect information and show that an adapted version of the sum of strategies theorem still holds in these games.