Preservation Theorems in Semiring Semantics

Brinke, Sophie; Dawar, Anuj; Grädel, Erich; Pago, Benedikt

doi:10.4230/LIPIcs.ICALP.2026.172

Preservation Theorems in Semiring Semantics

Sophie Brinke

RWTH Aachen University, Germany Anuj Dawar

University of Cambridge, UK Erich Grädel

RWTH Aachen University, Germany Benedikt Pago

University of Cambridge, UK

Abstract

We study the status of classical model-theoretic preservation theorems such as the Łoś-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 but has been extended to a systematic way of evaluating logical statements to values in a commutative semiring. Depending on the underlying semiring, this allows us to track descriptions of the atomic facts that 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 Łukasiewicz semiring, and the natural semirings $\mathbb{N}$ and $\mathbb{N}^{\infty}$ . Surprisingly, the existential preservation theorem does hold for finite interpretations in a number of semirings, including the three-element min-max semiring, which extends the Boolean by just a single additional truth value. Thus, the situation for these semirings is in sharp contrast to the Boolean case, where the Łoś-Tarski theorem holds in general, but not in the finite.

Keywords and phrases:

Semiring semantics, preservation theorems, model theory, algebraic logics

Category:

Track B: Automata, Logic, Semantics, and Theory of Programming

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Finite Model Theory

Editors:

Sayan Bhattacharya, Danupon Nanongkai, Michael Benedikt, and Gabriele Puppis

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Preservation Theorems

In model theory, preservation theorems typically state that the first-order sentences satisfying a specific semantic property are precisely those that are equivalent to sentences of a particular syntactic form. Well-known examples include the Łoś-Tarski theorem saying that a first-order sentence is preserved under extensions of its models if, and only if, it is equivalent to an existential sentence, and the homomorphism preservation theorem which states that the first-order sentences preserved under homomorphisms are precisely those that are equivalent to existential-positive sentences (unions of conjunctive queries). Preservation theorems matter because they tell us which syntactic forms capture which structural invariance properties, and this drives applications in databases, descriptive complexity, the simplification of axiomatisations, quantifier elimination, and the study of expressive power of fragments of first-order logic.

The prominence of preservation theorems in classical model theory has motivated persistent investigations of their status in other model-theoretic contexts, in particular in finite model theory and, more recently, also in many-valued logics. In finite model theory, it has been known for a long time that most of the classical preservation theorems fail when restricted to finite structures. In particular this concerns the Łoś-Tarski theorem for which Tait [28] and Gurevich [22] provide examples of first-order sentences whose finite models are closed under extensions but which are not equivalent, over finite structures, to any existential sentence. This failure has been strengthened by Dawar and Sankaran [11] who construct, for every $n$ , sentences whose finite models are closed under extensions, but which are not equivalent in the finite to any $\Sigma_{n}$ -sentence. Among the few positive results on preservation theorems in finite model theory, the most significant one, due to Rossman [27], establishes that the homomorphism preservation theorem does indeed hold on finite structures. There are many further results on preservation theorems in finite model theory, see [26] for a survey and [23] for a more recent treatment.

In many-valued logics, Badia et al. [3] generalised the Łoś-Tarski theorem and also the Chang-Łoś-Suszko preservation theorem for $\Pi_{2}$ -sentences under unions of chains to the specific setting of fixed finite MTL-chains (linearly ordered algebraic models of monoidal t-norm–based logic). Dellunde and Vidal [12] established a variant of the homomorphism preservation theorem in the same setting and Carr [10] provided a variant of this for finite many-valued structures, based on an extension of Rossman’s proof.

Semiring Semantics

In this paper, we extend the study of preservation theorems to the setting of semiring semantics. This approach, which has its origins in the provenance analysis of database queries [20], is based on the idea of evaluating logical statements not just to true or false, but more generally to values in some commutative semiring $\mathcal{S}=(S,+,\cdot,0,1)$ . Atomic facts are annotated by values from $S$ which are then propagated through a database query or a logical formula, keeping track whether information is used alternatively or jointly. Depending on the chosen semiring, provenance valuations give practical information about a statement, for instance concerning the confidence that we may have in its truth, the cost of its evaluation, the required clearance level for the access to not freely available data, the number of successful evaluation strategies, and so on. Beyond such provenance evaluations in specific application semirings, more precise information is obtained by evaluations in provenance semirings of polynomials or formal power series, which permit us to track which atomic facts are used (and how often) to compute the answer to the query. See [21, 14] for surveys on semiring provenance in databases.

The detailed information on a logical statement, as provided by semiring provenance, is of interest not just for databases, but also in many other areas of logic in computer science. There is thus ample motivation to extend the approach of semiring provenance beyond database queries to a general semiring semantics for logical systems, in particular for full first-order logic. Further, semiring valuations have also been successfully applied to the strategy analysis for various forms of finite and infinite games [18, 16, 24]. This poses a number of mathematical challenges that have been addressed in recent research, and it raises the question to what extent classical logical methods and results also hold in this more general context. Research on such questions has included the study of elementary equivalence and the axiomatisability of finite semiring interpretations [17], of the equivalence of the relational calculus with relational algebra (Codd’s Theorem) [4], 0-1 laws [15], Ehrenfeucht–Fraïssé games [8], the locality theorems by Hanf and Gaifman [5], compactness [6], and the interplay between local consistency and global consistency for relations over semirings [1, 2]. The study of preservation theorems in semiring semantics extends this research to a further important model-theoretic topic.

From the study of model-theoretic methods and results in the setting of semiring semantics, the following general picture has emerged.

$\blacksquare$

For most of the central model-theoretic notions (such as elementary equivalence, homomorphisms, evaluation and comparison games, locality, compactness, random structures etc.), the definitions naturally generalise to the semiring setting. In some cases, the generalisations require that semirings with specific algebraic properties are considered (for instance absorptive semirings, or semirings with infinitary operations).
$\blacksquare$

Sometimes, variants of such definitions which are clearly equivalent in the classical Boolean case can become different, non-equivalent notions in semiring semantics. An important example is compactness, which can be formulated either in terms of satisfiability or in terms of entailment, and in the classical setting either one of the formulations of the compactness theorem obviously implies the other. In semiring semantics this is not the case. There, compactness in terms of entailment is a stronger notion than compactness in terms of satisfiability, and there are important semirings, such as the tropical semiring where the two notions can be separated [6].
$\blacksquare$

While the questions about the status of classical logical theorems in semiring semantics arise very naturally, their answers (and the proofs of these) become much more complicated and often strongly depend on algebraic properties of the underlying semirings. Moreover, they often require the development of new mathematical methods.

Our Contributions

For preservation properties in semiring semantics, we make similar observations. The notions of preservation under extensions, substructures, or homomorphisms generalise very naturally to semiring semantics, and so do the straightforward directions (from syntactic forms to semantic properties) of the preservation theorems that we consider: Existential sentences are preserved under extensions, universal sentences are preserved downwards and existential-positive sentences are preserved under homomorphisms. We study the question for which semirings also the “difficult” direction (from semantic properties to syntactic forms) of the preservation theorems holds, both in the case of semiring interpretations over arbitrary domains and those just over finite domains. More precisely, our questions concerning, say, the Łoś-Tarski theorem can be stated as follows: Fix a semiring $\mathcal{S}$ . Is it the case that for every first-order sentence $\psi$ which is preserved under extensions of (finite) $\mathcal{S}$ -interpretations there exists a purely existential sentence which is equivalent to $\psi$ under all (finite) $\mathcal{S}$ -interpretations? Can we identify algebraic notions that imply positive or negative answers to this question?

The questions for universal preservation and preservation under homomorphisms are analogous. Notice that the classical duality between existential and universal preservation breaks down. While the classical Łoś-Tarski theorem can be equivalently formulated in terms of existential or universal preservation, these are separate issues in semiring semantics. We also note that preservation theorems for semirings neither entail the classical Boolean variants, nor are they entailed by them. This is because on the semantic side, preservation properties for a semiring $\mathcal{S}$ are stronger than their Boolean analogues, but on the syntactic side also $\mathcal{S}$ -equivalence is a stronger notion than classical logical equivalence.

Our main results can be summarised as follows:

$\blacksquare$

The preservation theorems for extensions, subinterpretations and homomorphisms are indeed true for all lattice semirings $(S,\sqcup,\sqcap,0,1)$ . These are semirings induced by a completely distributive complete lattice $(S,\leq)$ (i.e. a partial order closed under suprema and infima in which infima distributive over suprema), with suprema and infima as semiring operations; they encompass in particular all min-max semirings, such as the fuzzy semiring $\mathbb{F}=([0,1],\max,\min,0,1)$ , and the security semiring for reasoning about access control [13]. The proofs combine adaptations of the classical compactness and amalgamation methods to the specific three-element min-max semiring $\mathcal{S}_{3}$ with a reduction method from [6], reducing entailments for arbitrary lattice semirings to $\mathcal{S}_{3}$ -entailments.
$\blacksquare$

Variants of the existential preservation theorem fail for many other semirings, including the tropical semiring, the Viterbi semiring, the Łukasiewicz semiring and the natural semirings $\mathbb{N}$ and $\mathbb{N}^{\infty}$ .
$\blacksquare$

Surprisingly, the existential preservation theorem does, however, hold for finite interpretations in the Viterbi semiring, the tropical semiring, the Łukasiewicz semiring, and every lattice semiring with at least three elements. Thus the situation for these semirings is in sharp contrast to the classical Boolean case, where the Łoś-Tarski theorem holds in general, but not in the finite. To prove this result, we develop a novel technique that allows us to translate evaluation strategies for sentences between models of different finite cardinalities.

In particular, the latter result raises the intriguing question whether the failure of extension preservation in the finite is perhaps merely a sporadic phenomenon that is unique to the Boolean semiring. Thus, our study provides the foundation for a new line of future research: For which other (classes of) semirings does extension preservation survive in the finite?

2 Semiring Semantics for First-order Logic

We briefly describe the foundations of semiring semantics for first-order logic and refer to [19] for further details.

Definition 2.1.

A commutative monoid is an algebraic structure $(M,+,0)$ where $+$ is a binary commutative and associative operation with $0\in M$ as its neutral element. A commutative semiring is a structure $\mathcal{S}=(S,+,\cdot,0,1)$ with $0\neq 1$ such that $(S,+,0)$ and $(S,\cdot,1)$ are commutative monoids, $\cdot$ distributes over $+$ , and $0\cdot s=s\cdot 0=0$ .

In the following, we assume that all semirings are commutative and naturally ordered, that is, $s\leq t\Leftrightarrow\exists r(s+r=t)$ defines a partial order. Addition and multiplication are monotone with respect to the natural order. A semiring is absorptive if $s+st=s$ for all $s,t\in S$ , which is equivalent to the property that multiplication is decreasing with respect to the natural order. Absorptive semirings are particularly important in semiring semantics, because they preserve, to some extent, the common logical dualities. Addition in absorptive semirings is idempotent (i.e., $s+s=s$ for each $s\in S$ ), so sums coincide with suprema. Beyond the Boolean semiring $\mathbb{B}=(\{0,1\},\vee,\wedge,0,1)$ , there are many other absorptive semirings that provide useful information about the evaluation of a formula.

$\blacksquare$

A totally ordered set $(S,\leq)$ with least element $s$ and greatest element $t$ induces the min-max semiring $(S,\max,\min,s,t)$ .
$\blacksquare$

A more general class is the class of lattice semirings $(S,\sqcup,\sqcap,s,t)$ induced by a bounded distributive lattice $(S,\leq)$ . In fact, every absorptive semiring with idempotent multiplication is a lattice semiring.
$\blacksquare$

The tropical semiring $\mathbb{T}=(\mathbb{R}^{\infty}_{+},\min,+,\infty,0)$ is used for cost analysis.
$\blacksquare$

To reason about confidence, we may use the Viterbi semiring $\mathbb{V}=([0,1]_{\mathbb{R}},\max,\cdot,0,1)$ or the Łukasiewicz semiring $\mathbb{L}=([0,1]_{\mathbb{R}},\max,\odot,0,1)$ where $s\odot t\coloneqq\max(s+t-1,0)$ .
$\blacksquare$

The semiring $\mathbb{D}=([0,1]_{\mathbb{R}},\min,\oplus,1,0)$ with $s\oplus t\coloneqq\min(s+t,1)$ models levels of doubt.
$\blacksquare$

The most important non-absorptive semirings are the natural semiring $(\mathbb{N},+,\cdot,0,1)$ and its extension to $\mathbb{N}^{\infty}=\mathbb{N}\cup\{\infty\}$ .
$\blacksquare$

Provenance semirings allow us to track the atomic facts that are responsible for the truth of a formula. In the non-absorptive case, the most general provenance semirings are $\mathbb{N}[X]$ , the semirings of polynomials over a finite set $X$ of indeterminates and coefficients from $\mathbb{N}$ . In the absorptive setting the important examples are the semirings $\mathbb{S}(X)$ and $\mathbb{S}^{\infty}(X)$ of (generalised) absorptive polynomials. See [19, 25] for more details.

To define semiring semantics also for infinite universes, and to extend it to valuations of infinite collections $\Phi$ of first-order sentences, the semirings need to be equipped with infinitary summation and product operators. Algebraic foundations, mathematical properties and provenance valuations of such infinitary semirings have been studied in [9]. We will not go into details here and tacitly assume that infinitary sums and products are available and have the desired associativity and commutativity properties. In the specific semirings that we consider here, the definitions of these operations are straightforward.

To evaluate first-order formulae in semirings, classical structures are generalised to semiring interpretations that map the atomic facts and their negations to semiring values. While $0$ represents falsity, every non-zero element provides an annotation of truth.

Definition 2.2 (Semiring interpretations).

Let $A$ be a (finite or infinite) universe, let $\tau$ be a relational vocabulary, and let $\mathcal{S}$ be a semiring. We denote by $\operatorname{Lit}_{A}(\tau)$ the set of $\tau$ -literals of the form $R\bar{a}$ or $\lnot R\bar{a}$ that are instantiated with tuples from $A$ . Analogously, $\operatorname{Atoms}_{A}(\tau)$ denotes the set of $\tau$ -atoms $R\bar{a}$ over $A$ . An $\mathcal{S}$ -interpretation (for $A$ and $\tau$ ) is a function $\pi\colon\operatorname{Lit}_{A}(\tau)\rightarrow\mathcal{S}$ . We say that $\pi$ is model-defining if for every literal $L\in\operatorname{Lit}_{A}(\tau)$ precisely one of the values $\pi(L)$ and $\pi(\neg L)$ is 0. Every model-defining $\mathcal{S}$ -interpretation defines a $\tau$ -model ${\mathfrak{A}}_{\pi}$ where ${\mathfrak{A}}_{\pi}\models L$ if $\pi(L)\neq 0$ for $L\in\operatorname{Lit}_{A}(\tau)$ .

We only consider model-defining interpretations in this paper. Semiring semantics lifts each $\mathcal{S}$ -interpretation for a universe $A$ and vocabulary $\tau$ to a mapping $\operatorname{FO}_{A}(\tau)\to\mathcal{S}$ where $\operatorname{FO}_{A}(\tau)$ is the set of first-order formulae instantiated with elements from $A$ . We assume that all formulae are written in negation normal form. This has emerged as the standard approach for dealing with negation in semiring semantics, and is explained in detail in [19].

Definition 2.3 (Semiring Semantics).

For every $\varphi\in\operatorname{FO}_{A}(\tau)$ in negation normal form, the semiring valuation $\pi\llbracket\varphi\rrbracket$ is lifted beyond the literals inductively, by

	$\displaystyle\pi\llbracket\psi\vee\vartheta\rrbracket$	$\displaystyle\coloneqq\pi\llbracket\psi\rrbracket+\pi\llbracket\vartheta% \rrbracket,\hskip 28.45274pt$	$\displaystyle\pi\llbracket\forall x\psi(x)\rrbracket$	$\displaystyle\coloneqq\prod_{a\in A}\pi\llbracket\psi(a)\rrbracket,$
	$\displaystyle\pi\llbracket\psi\wedge\vartheta\rrbracket$	$\displaystyle\coloneqq\pi\llbracket\psi\rrbracket\cdot\pi\llbracket\vartheta% \rrbracket,\hskip 28.45274pt$	$\displaystyle\pi\llbracket\exists x\psi(x)\rrbracket$	$\displaystyle\coloneqq\sum_{a\in A}\pi\llbracket\psi(a)\rrbracket.$

Equality atoms are interpreted by their Boolean truth value, that is, $\pi\llbracket a=a\rrbracket\coloneqq 1$ and $\pi\llbracket a=b\rrbracket\coloneqq 0$ for $a\neq b$ (and analogously for inequalities). For finite or infinite sets $\Phi\subseteq\operatorname{FO}_{A}(\tau)$ we set $\pi\llbracket\Phi\rrbracket\coloneqq\prod_{\varphi\in\Phi}\pi\llbracket\varphi\rrbracket$ .

Lemma 2.4 (Fundamental Property).

Let $\mathcal{S},\mathcal{S}^{\prime}$ be semirings, $\pi\colon\operatorname{Lit}_{A}(\tau)\to\mathcal{S}$ be an $\mathcal{S}$ -interpretation, and $h\colon\mathcal{S}\to\mathcal{S}^{\prime}$ be a semiring homomorphism. Then, $(h\circ\pi)$ is a $\mathcal{S}^{\prime}$ -interpretation and it holds that $(h\circ\pi)\llbracket\Phi(\bar{a})\rrbracket=h(\pi\llbracket\Phi(\bar{a})\rrbracket)$ for all $\Phi(\bar{a})\subseteq\operatorname{FO}_{A}(\tau)$ .

Definition 2.5 (Entailment).

Let $\Phi,\Psi\subseteq\operatorname{FO}$ be sets of first-order sentences and let $\mathcal{S}$ be an (absorptive) semiring. We write

(1)

$\Phi\models_{\mathcal{S}}\Psi$ ( $\Phi$ $\mathcal{S}$ -entails $\Psi$ ) if $\pi\llbracket\Phi\rrbracket\leq\pi\llbracket\psi\rrbracket$ for every $\mathcal{S}$ -interpretation $\pi$ , and
(2)

$\Phi\equiv_{\mathcal{S}}\Psi$ ( $\Phi$ is $\mathcal{S}$ -equivalent to $\Psi$ ) if $\pi\llbracket\Phi\rrbracket=\pi\llbracket\Psi\rrbracket$ for every $\mathcal{S}$ -interpretation $\pi$ .

If $\Phi$ or $\Psi$ is a singleton, we replace them with the corresponding formula in these notations.

Notions of Preservation in Semiring Semantics

We next discuss how semantic preservation properties (upwards, downwards, and under homomorphisms) present themselves in the context of semiring semantics, and why they are implied by specific syntactic forms.

Definition 2.6 (Homomorphisms and Subinterpretations).

$\blacksquare$

A homomorphism between $\mathcal{S}$ -interpretations $\pi_{A}$ and $\pi_{B}$ is a mapping $g\colon A\to B$ such that for any $R\bar{a}\in\operatorname{Atoms}_{A}(\tau)$ it holds that $\sum_{\bar{a}^{\prime}:g(\bar{a}^{\prime})=g(\bar{a})}\pi_{A}(R\bar{a}^{\prime% })\leq\pi_{B}(Rg(\bar{a}))$ (note that we only take into account the positive literals here). Further, $g$ is a strong homomorphism if $\pi_{A}(L\bar{a})=\pi_{B}(Lg(\bar{a}))$ for all $L\bar{a}\in\operatorname{Lit}_{A}(\tau)$ . If $g$ , in addition, is injective, we call it an embedding and write $g\colon\pi_{A}\subseteq\pi_{B}$ . Note that for idempotent semirings (where addition is the supremum with respect to the natural order), the inequality above reduces to $\pi_{A}(R\bar{a})\leq\pi_{B}(Rg(\bar{a}))$ for each $R\bar{a}\in\operatorname{Atoms}_{A}(\tau)$ .
$\blacksquare$

$\pi_{A}$ is a subinterpretation of $\pi_{B}$ (and $\pi_{B}$ is an extension of $\pi_{A}$ ), denoted $\pi_{A}\subseteq\pi_{B}$ , if $A\subseteq B$ and $\pi_{A}(L\bar{a})=\pi_{B}(L\bar{a})$ holds for all literals $L\bar{a}\in\operatorname{Lit}_{A}(\tau)$ .
$\blacksquare$

$\pi_{A}$ is an elementary subinterpretation of $\pi_{B}$ (and $\pi_{B}$ is an elementary extension of $\pi_{A}$ ), denoted $\pi_{A}\preceq\pi_{B}$ , if $A\subseteq B$ and $\pi_{A}\llbracket\varphi(\bar{a})\rrbracket=\pi_{B}\llbracket\varphi(\bar{a})\rrbracket$ holds for all $\varphi(\bar{a})\in\operatorname{FO}_{A}(\tau)$ .

Classical preservation properties have the form that sentences which are true in a specific structure remain true when we move to another structure, related to the first one as an extension, a substructure, or by a homomorphism. In the context of semiring interpretations we evaluate formulae not just by true or false, but in a general semiring. The property that the formula remains true is replaced by the stronger relationship that the formula evaluates to a greater or equal value (w.r.t. to the natural order on the semiring) when we move from one interpretation to a new one.

Definition 2.7 (Preservation).

$\blacksquare$

A sentence $\psi\in\operatorname{FO}(\tau)$ is preserved under homomorphisms in $\mathcal{S}$ if for all model-defining $\mathcal{S}$ -interpretations $\pi_{A},\pi_{B}$ with a homomorphism $g\colon A\to B$ , we have that $\pi_{A}\llbracket\psi\rrbracket\leq\pi_{B}\llbracket\psi\rrbracket$ .
$\blacksquare$

A sentence $\varphi\in\operatorname{FO}(\tau)$ is preserved under subinterpretations in $\mathcal{S}$ if for all model-defining $\mathcal{S}$ -interpretations $\pi_{A}\subseteq\pi_{B}$ , we have that $\pi_{A}\llbracket\varphi\rrbracket\geq\pi_{B}\llbracket\varphi\rrbracket$ .
$\blacksquare$

Analogously, $\varphi\in\operatorname{FO}(\tau)$ is preserved under extensions in $\mathcal{S}$ if $\pi_{A}\llbracket\varphi\rrbracket\leq\pi_{B}\llbracket\varphi\rrbracket$ is true for all model-defining $\mathcal{S}$ -interpretations $\pi_{A}\subseteq\pi_{B}$ .

We observe that the directions from the syntactic form to the semantic preservation properties of the classical preservation theorems also hold in this context. Recall that

$\blacksquare$

$\Sigma_{1}^{+}$ denotes the set of existential-positive sentences $\exists\bar{x}\varphi(\bar{x})$ where $\varphi(\bar{x})$ is quantifier- and negation-free,
$\blacksquare$

$\Sigma_{1}$ denotes the set of existential sentences $\exists\bar{x}\varphi(\bar{x})$ where $\varphi(\bar{x})$ is quantifier-free, and
$\blacksquare$

$\Pi_{1}$ is the set of universal sentences $\forall\bar{x}\varphi(\bar{x})$ where $\varphi(\bar{x})$ is quantifier-free.

At this point, it becomes clear why our definition of homomorphism involves summation over the preimages of tuples. This accounts for the possibility that multiple tuples in the left-hand side interpretation $\pi_{A}$ are collapsed onto the same tuple in $\pi_{B}$ . Our definition ensures that existential-positive sentences are indeed preserved under homomorphisms. For example, consider the sentence $\exists x\exists yExy$ . Now take for example $\pi_{A}$ to be a bipartite graph with edge weights from $\mathcal{S}$ , and $\pi_{B}$ an $\mathcal{S}$ -weighted graph that is just a single edge. Since every bipartite graph maps homomorphically to a single edge, $\pi_{A}$ should map homomorphically to $\pi_{B}$ . But we have to insist that the value of the single edge in $\pi_{B}$ is at least the sum of its preimages, or else, we would not have $\pi_{A}\llbracket\exists x\exists yExy\rrbracket\leq\pi_{B}\llbracket\exists x% \exists yExy\rrbracket$ . Moreover, in defining homomorphisms we use the natural order rather than insisting on equalities, so that edges are preserved while non-edges need not be.

Lemma 2.8.

If $\psi$ is a positive Boolean combination of (positive) existential sentences, there is some $\varphi\in\Sigma_{1}$ ( $\varphi\in\Sigma_{1}^{+}$ ) such that $\psi\equiv_{\mathcal{S}}\varphi$ for all additively idempotent semirings $\mathcal{S}$ . If $\psi$ is a positive Boolean combination of universal sentences, there is some $\varphi\in\Pi_{1}$ such that $\psi\equiv_{\mathcal{L}}\varphi$ for all lattice semirings $\mathcal{L}$ .

By monotonicity of the semiring operations and the fact that addition is increasing with respect to the natural order, the implication from syntax to semantics follows readily by induction for $\Sigma_{1}^{+}$ and $\Sigma_{1}$ . We only need to take some care in the case $\Pi_{1}$ , where we need multiplication to be decreasing. This is true exactly for absorptive semirings.

Lemma 2.9.

(1)

$\Sigma_{1}^{+}$ -sentences are preserved under homomorphisms in every semiring.
(2)

$\Sigma_{1}$ -sentences are preserved under extensions in every semiring.
(3)

$\Pi_{1}$ -sentences are preserved under subinterpretations in every absorptive semiring.

3 Failure of Extension Preservation in General Semirings

While the easy direction of the classical preservation theorems from syntax to semantics survives in semiring semantics, there are cases where the converse direction fails. We present two examples where sentences or sets of sentences are preserved under extensions but cannot be written without the use of universal quantifiers. The detailed proofs can be found in Appendix C. We first consider $\mathbb{N}^{\infty}$ , the natural semiring $(\mathbb{N},+,\,\cdot\,,0,1)$ expanded to $\mathbb{N}\cup\{\infty\}$ .

Lemma 3.1.

The sentence $\exists x\forall yRx$ is preserved under extensions in $\mathbb{N}^{\infty}$ but not $\mathbb{N}^{\infty}$ -equivalent to a $\Sigma_{1}$ -sentence.

In this example, the universally quantified variable $y$ does not appear in the formula. Hence, the universal quantifier has the effect of just raising the value of the inner formula to the $n$ -th power if $n$ is the size of the universe, and otherwise to the infinite power. While the formula is clearly extension-closed, one can see that expressing powers that grow with the size of the universe is not possible in $\mathbb{N}^{\infty}$ without the use of a universal quantifier.

Our next counterexamples are the Viterbi semiring $\mathbb{V}=([0,1]_{\mathbb{R}},\max,\cdot,0,1)$ and the semiring of doubt $\mathbb{D}=([0,1]_{\mathbb{R}},\min,\oplus,1,0)$ with $s\oplus t=\min(s+t,1)$ . We establish that extension preservation fails for a set of sentences, or for semiring interpretations over infinite universes. Of course these results translate to the tropical semiring $\mathbb{T}$ and to the Łukasiewicz semiring $\mathbb{L}$ , since $\mathbb{T}$ is isomorphic to $\mathbb{V}$ , and $\mathbb{L}$ is isomorphic to $\mathbb{D}$ .

Lemma 3.2.

For $\mathcal{S}\in\{\mathbb{V},\mathbb{D}\}$ , the set $\Phi\coloneqq\{\exists x_{1}\dots\exists x_{n}\bigwedge_{1\leq i<j\leq n}x_{i}% \neq x_{j}\mid n\in\omega\}\cup\{\exists x\forall yRx\}$ is preserved under extensions in $\mathcal{S}$ , but is not $\mathcal{S}$ -equivalent to a set of $\Sigma_{1}$ -sentences.

The axiom system $\Phi$ forces its models to be infinite. In infinite $\mathbb{V}$ -interpretations, the universal quantifier $\forall y$ raises the value of $R x$ to its infinite power (i.e. the infimum of the finite powers), and the maximum over these values is preserved under extensions. However, one can prove that no set of existential sentences has the same semantics. The key argument is this: The supremum (the evaluation of the existential quantifier) over an infinite sequence tending towards $1$ in the interval $[0,1)$ is always $1$ , but when these values are first raised to $\infty$ – which is the effect of $\forall y$ – then the supremum becomes $0$ . In other words, infinite suprema and powers do not commute in $\mathbb{V}$ . The argument for $\mathbb{D}$ is analogous.

4 Preservation Theorems in Lattice Semirings

Whether we consider single sentences or sets of them, the extension preservation theorem does not generalise to all semirings. This raises the question in which semirings it does survive. We show that both variants hold for the important and fairly general class of lattice semirings, induced by a completely distributive complete lattice (i.e. a partial order closed under suprema and infima in which infima distributive over suprema), with supremum and infimum as semiring operations. Also the homomorphism and subinterpretation preservation theorems generalise to the lattice setting.

Theorem 4.1.

Let $\mathcal{L}$ be a lattice semiring. A sentence $\psi\in\operatorname{FO}$ is preserved under homomorphisms/extensions/subinterpretations in $\mathcal{L}$ if, and only if, there is some $\varphi\in\Sigma_{1}^{+}$ / $\varphi\in\Sigma_{1}$ / $\varphi\in\Pi_{1}$ such that $\psi\equiv_{\mathcal{L}}\varphi$ .

Here we will only treat extension preservation and refer to [7] for the proofs of the homomorphism and subinterpretation preservation theorems. The classical proofs of most model-theoretic preservation theorems rely on compactness and amalgamation. Compactness has recently been studied in the context of semiring semantics in [6] and positive results have been established, in particular, for the lattice case. However, by itself, compactness alone does not suffice to extend the proofs of preservation theorems to lattice semirings. A simple yet important property that the classical proof of the extension preservation theorem is based on is that two Boolean structures satisfy the same $\Sigma_{1}$ -sentences if, and only if, they share the same finite substructures. In this respect, semiring semantics behaves completely differently, and finite non-isomorphic interpretations over $4$ -element min-max semirings may even agree on the evaluation of any $\operatorname{FO}$ -sentence [17]. The intuitive reason for this is that the semiring elements do not occur in the logic’s syntax. While the $\Sigma_{1}$ -sentence $\psi=\exists x(Px\wedge\lnot Qx)$ , for example, describes a substructure of size $1$ in the Boolean, its evaluation in a lattice semiring may not even be witnessed by a single instantiation of $x$ as existential quantifiers are evaluated to a supremum. Even if we fix some instantiation $a$ , by commutativity, the evaluation of $Pa\wedge\lnot Qa$ does not give insights into the contribution of the single literals. This mismatch between $\Sigma_{1}$ -sentences and the notions of subinterpretations and extensions in semiring semantics is what makes it a challenge to show that the extension preservation theorem still holds. We achieve this by combining arguments used in the classical proof with new methods specifically developed for semiring semantics.

Proof Methods from Semiring Semantics

A key ingredient to the proof of Theorem 4.1 is a reduction to the case where we evaluate in the three-element lattice semiring $\mathcal{S}_{3}$ , where an element denoted $\varepsilon$ is sandwiched in between $0$ and $1$ , that is, $\mathcal{S}_{3}=(\{0,\varepsilon,1\},\max,\min,0,1)$ . As it embeds into any lattice semiring except the Boolean one, it can be thought of as the simplest lattice semiring beyond the Boolean. By extending a decomposition method based on homomorphisms from [6], we show that a preservation property or a logical equivalence must hold in all lattice semirings $\mathcal{L}\not\cong\mathbb{B}$ once it holds in a single such semiring.

Proposition 4.2.

Let $\mathcal{L},\mathcal{L}^{\prime}\not\cong\mathbb{B}$ be lattice semirings and $\Phi\subseteq\operatorname{FO}$ be a set of sentences. If $\Phi$ is preserved under homomorphisms/extensions/subinterpretations in $\mathcal{L}$ , then $\Phi$ must also be preserved under homomorphisms/extensions/subinterpretations in $\mathcal{L}^{\prime}$ .

Proposition 4.3.

For all $\Phi,\Psi\subseteq\operatorname{FO}$ , the following are equivalent:

(1)

$\Phi\models_{\mathcal{L}}\Psi$ for all lattice semirings $\mathcal{L}\not\cong\mathbb{B}$ ;
(2)

$\Phi\models_{\mathcal{L}}\Psi$ for some lattice semiring $\mathcal{L}\not\cong\mathbb{B}$ ;
(3)

$\pi\llbracket\Psi\rrbracket=1$ for all $\mathcal{S}_{3}$ -interpretations $\pi$ with $\pi\llbracket\Phi\rrbracket=1$ .

Corollary 4.4.

For all $\Phi,\Psi\subseteq\operatorname{FO}$ , the following are equivalent:

(1)

$\Phi\equiv_{\mathcal{L}}\Psi$ for all lattice semirings $\mathcal{L}\not\cong\mathbb{B}$ ;
(2)

$\Phi\equiv_{\mathcal{L}}\Psi$ for some lattice semiring $\mathcal{L}\not\cong\mathbb{B}$ ;
(3)

$\pi\llbracket\Phi\rrbracket=1$ if, and only if, $\pi\llbracket\Psi\rrbracket=1$ for all $\mathcal{S}_{3}$ -interpretations $\pi$ .

Note that this reduction only works for lattice semirings $\mathcal{L}\not\cong\mathbb{B}$ , but not for the Boolean semiring itself, i.e., classical semantics. Since equalities are evaluated by their Boolean truth value in semiring semantics, some Boolean tautologies can only evaluate to $1$ in lattice semirings, while others may take values different from $1$ . As a consequence, the sentence $\psi=\forall x(Rx\vee\lnot Rx)$ , for example, is clearly extension preserved in the classical sense, but it is not in any lattice semiring $\mathcal{L}\not\cong\mathbb{B}$ , which contains a third truth value $0<s<1$ : Extending an $\mathcal{L}$ -interpretation over a single element $a$ whose valuation with respect to $R$ is $1$ by a second element $b$ such that $R b$ is evaluated to $s$ decreases the valuation of $\psi$ . Similarly, one observes that $\exists x(x=x)\not\equiv_{\mathcal{L}}\exists x(Rx\vee\lnot Rx)$ for all $\mathcal{L}\not\cong\mathbb{B}$ .

An essential part of the proof of Theorem 4.1 will be the third statement of Corollary 4.4, which intuitively says that the $\mathcal{S}_{3}$ -semantics of a sentence is uniquely determined by its $1$ -valuations. This is not to be confused with its classical Boolean semantics, because it is still evaluated on $\mathcal{S}_{3}$ -interpretations that may also annotate literals with $\varepsilon$ . This insight gives us some relationship between $\Sigma_{1}$ and finite subinterpretations again: Two $\mathcal{S}_{3}$ -interpretations $\pi_{A},\pi_{B}$ evaluate the same $\Sigma_{1}$ -sentence to $1$ if, and only if, they have the same finite subinterpretations that only contain valuations of $1$ .

Besides this reduction to $\mathcal{S}_{3}$ , we will need to apply compactness. The semiring setting admits different notions of compactness. Restricting ourselves to the case $\mathcal{S}_{3}$ allows us to apply two different variants, one of them being based on $\mathcal{S}$ -axioms $(\psi,T)$ , where $\psi$ is a sentence and $T$ a set of designated truth values (a modified version of the notion used in [24]), and another one based on entailment (studied in [6]). While we use the first variant to prove an amalgamation theorem and justify its application, the second variant is important to infer a single equivalent $\Sigma_{1}$ -sentence starting from a single extension preserved sentence, just as in the Boolean proof.

Definition 4.5.

An $\mathcal{S}$ -axiom (over a universe $A$ ) is a pair $(\psi,T)$ where $\psi\in\operatorname{FO}_{A}(\tau)$ and $T\subseteq\mathcal{S}$ . An $\mathcal{S}$ -interpretation $\pi$ satisfies $(\psi,T)$ if $\pi\llbracket\psi\rrbracket\in T$ . A set of $\mathcal{S}$ -axioms $\Delta$ is called an axiomatic system, and it is satisfied by $\pi$ if $\pi$ satisfies each $(\psi,T)\in\Delta$ . An axiomatic system $\Delta$ is satisfiable if there is a model-defining interpretation that satisfies it.

Theorem 4.6 ([24]).

Let $\mathcal{S}$ be finite and absorptive, and $\Delta$ be an unsatisfiable set of $\mathcal{S}$ -axioms. Then there is already a finite unsatisfiable $\Delta_{0}\subseteq\Delta$ .

It should be noted that [24] proves Theorem 4.6 only for $\mathcal{S}$ -axioms $(\psi,T)$ where $T$ is a singleton, but the case where $T\subseteq\mathcal{S}$ is any finite set is completely analogous.

Theorem 4.7 ([6]).

Let $\mathcal{L}$ be a lattice semiring. If $\Phi\models_{\mathcal{L}}\psi$ , then there is some finite $\Phi_{0}\subseteq\Phi$ such that $\Phi_{0}\models_{\mathcal{L}}\psi$ .

Extension Preservation

We first consider the case $\mathcal{S}_{3}$ and then generalise it to arbitrary lattice semirings $\mathcal{L}\not\cong\mathbb{B}$ . More precisely, we prove that every set of sentences $\Phi$ which is extension preserved in $\mathcal{S}_{3}$ is $\mathcal{S}_{3}$ -equivalent to some $\Psi\subseteq\Sigma_{1}$ . As in the classical proof, we show that $\Phi\equiv_{\mathcal{S}_{3}}\Phi_{\exists}$ , where $\Phi_{\exists}\coloneqq\{\psi\in\Sigma_{1}\mid\Phi\models_{\mathcal{S}_{3}}\psi\}$ . It holds that $\Phi\models_{\mathcal{S}_{3}}\Phi_{\exists}$ because for any $\mathcal{S}_{3}$ -interpretation $\pi$ , $\pi\llbracket\Phi\rrbracket$ is a lower bound of $\{\pi\llbracket\psi\rrbracket\mid\psi\in\Phi_{\exists}\}$ , which implies $\pi\llbracket\Phi\rrbracket\leq\bigsqcap\{\pi\llbracket\psi\rrbracket\mid\psi% \in\Phi_{\exists}\}=\pi\llbracket\Phi_{\exists}\rrbracket$ . It remains to show that if $\Phi$ is extension preserved in $\mathcal{S}_{3}$ , the converse entailment $\Phi_{\exists}\models_{\mathcal{S}_{3}}\Phi$ holds as well.

Lemma 4.8.

Let $\pi_{A}$ be an $\mathcal{S}_{3}$ -interpretation such that $\pi_{A}\llbracket\psi\rrbracket=1$ for all $\psi\in\Phi_{\exists}$ . Then there is an $\mathcal{S}_{3}$ -interpretation $\pi_{B}$ such that

(1)

$\pi_{B}\llbracket\Phi\rrbracket=1$ , and
(2)

$\pi_{B}\llbracket\psi\rrbracket\leq\varepsilon$ for all $\psi\in\Sigma_{1}$ with $\pi_{A}\llbracket\psi\rrbracket\leq\varepsilon$ .

Lemma 4.9 (Existential Amalgamation).

Let $\pi_{A}$ and $\pi_{B}$ be $\mathcal{S}_{3}$ -interpretations such that $\pi_{B}\llbracket\psi\rrbracket\leq\varepsilon$ for all $\psi\in\Sigma_{1}$ with $\pi_{A}\llbracket\psi\rrbracket\leq\varepsilon$ . Then there is some $\pi_{C}\succeq\pi_{A}$ and an injective mapping $f\colon B\to C$ such that $\pi_{C}(Lf(\bar{b}))=1$ for all $L\bar{b}\in\operatorname{Lit}_{B}(\tau)$ with $\pi_{B}(L\bar{b})=1$ .

Theorem 4.10.

Let $\Phi\subseteq\operatorname{FO}$ . If $\Phi$ is extension preserved in $\mathcal{S}_{3}$ , then $\Phi_{\exists}\models_{\mathcal{S}_{3}}\Phi$ .

Proof.

Let $\pi_{A}\llbracket\Phi_{\exists}\rrbracket=1$ , i.e., $\pi_{A}\llbracket\psi\rrbracket=1$ for all $\psi\in\Phi_{\exists}$ . By Proposition 4.3, it suffices to prove that $\pi_{A}\llbracket\Phi\rrbracket=1$ . Let $\pi_{B}$ be as in Lemma 4.8 and $\pi_{C}$ be the corresponding amalgamated $\mathcal{S}_{3}$ -interpretation according to Lemma 4.9. We know that $\pi_{B}\llbracket\Phi\rrbracket=1$ and want to argue that $\pi_{C}\llbracket\Phi\rrbracket=1$ holds as well. However, there need not be an embedding from $\pi_{B}$ to $\pi_{C}$ , only an injective mapping that preserves valuations of $1$ , which is why we take a detour via another $\mathcal{S}_{3}$ -interpretation $\pi_{B}^{*}$ that still evaluates $\Phi$ to $1$ but embeds into $\pi_{C}$ . Consider the homomorphism $h_{\geq 1}\colon\mathcal{S}_{3}\to\mathcal{S}_{3}$ where $h_{\geq 1}(1)=1$ and $h_{\geq 1}(0)=h_{\geq 1}(\varepsilon)=0$ . By construction, $\pi_{B}\llbracket\Phi\rrbracket=1$ , which implies $(h_{\geq 1}\circ\pi_{B})\llbracket\Phi\rrbracket=h_{\geq 1}(\pi_{B}\llbracket% \Phi\rrbracket)=1$ . Since valuations of $\varepsilon$ do not occur in $(h_{\geq 1}\circ\pi_{B})$ , the mapping $f$ we get from Lemma 4.9 must be a homomorphism from $(h_{\geq 1}\circ\pi_{B})$ to $\pi_{C}$ . However, $(h_{\geq 1}\circ\pi_{B})$ is not necessarily model-defining and we might have that both a literal and its complement are evaluated to $0$ . Hence, to define the $\mathcal{S}_{3}$ -interpretation $\pi_{B}^{*}$ , also on the universe $B$ , we insert the missing valuations by copying them from $\pi_{C}$ , which ensures that $f$ is still an embedding into $\pi_{C}$ .

More precisely, $\pi_{B}^{*}$ is defined as follows: For $L\bar{b}\in\operatorname{Lit}_{B}(\tau)$ we set $\pi_{B}^{*}(L\bar{b})\coloneqq\pi_{B}(L\bar{b})$ if $\pi_{B}(L\bar{b})=1$ or $\pi_{B}(\lnot L\bar{b})=1$ .¹¹1 $\lnot L\bar{b}$ refers to the dual literal, i.e. we identify $\lnot\lnot L\bar{b}$ with $L\bar{b}$ Otherwise, we set $\pi_{B}^{*}(L\bar{b})\coloneqq\pi_{C}(Lf(\bar{b}))$ . Note that $\pi_{B}^{*}$ is model-defining; in the first case this is inherited from $\pi_{B}$ , and in the second case this is inherited from $\pi_{C}$ . It remains to verify that $f$ embeds $\pi_{B}^{*}$ into $\pi_{C}$ . By Lemma 4.9, $f$ is injective. So let $L\bar{b}\in\operatorname{Lit}_{B}(\tau)$ . By definition of $\pi_{B}^{*}$ , we can restrict ourselves to the case $\pi_{B}(L\bar{b})=1$ or $\pi_{B}(\lnot L\bar{b})=1$ . First let $\pi_{B}^{*}(L\bar{b})=\pi_{B}(L\bar{b})=1$ . We have $\pi_{C}(Lf(\bar{b}))=1$ because $f$ preserves valuations of $1$ inside $\pi_{B}$ . If $\pi_{B}(\lnot L\bar{b})=1$ , we must have that $\pi_{C}(\lnot Lf(\bar{b}))=1$ by construction of $f$ , i.e. $\pi_{C}(Lf(\bar{b}))=0$ , and $\pi_{B}^{*}(L\bar{b})=\pi_{B}(L\bar{b})=0=\pi_{C}(Lf(\bar{b}))$ .

We have $\pi_{B}^{*}(L\bar{b})\geq(h_{\geq 1}\circ\pi_{B})(L\bar{b})$ for all $L\bar{b}\in\operatorname{Lit}_{B}(\tau)$ . By monotonicity of $\max$ and $\min$ , this inductively yields $\pi_{B}^{*}\llbracket\Phi\rrbracket\geq(h_{\geq 1}\circ\pi_{B})\llbracket\Phi% \rrbracket=h_{\geq 1}(\pi_{B}\llbracket\Phi\rrbracket)=1$ . Since $\Phi$ is extension preserved by assumption, this implies $\pi_{C}\llbracket\Phi\rrbracket\geq\pi_{B}^{*}\llbracket\Phi\rrbracket=1$ . With $\pi_{C}\succeq\pi_{A}$ , it follows that $\pi_{A}\llbracket\Phi\rrbracket=\pi_{C}\llbracket\Phi\rrbracket=1$ . Hence, we can overall conclude that $\Phi_{\exists}\models_{\mathcal{S}_{3}}\Phi$ . $\hfill\blacktriangleleft$

Theorem 4.11.

Let $\mathcal{L}\not\cong\mathbb{B}$ be a lattice semiring. If $\Phi\subseteq\operatorname{FO}$ is preserved under extensions in $\mathcal{L}$ , then $\Phi\equiv_{\mathcal{L}}\Psi$ for some $\Psi\subseteq\Sigma_{1}$ . In the special case where $\Phi=\{\varphi\}$ is a singleton, there is a single $\Sigma_{1}$ -sentence $\mathcal{L}$ -equivalent to $\varphi$ .

Proof.

Let $\Phi\subseteq\operatorname{FO}$ be extension preserved in $\mathcal{L}$ . By Proposition 4.2, $\Phi$ must be extension preserved in $\mathcal{S}_{3}$ . By Theorem 4.10, we know that $\Phi_{\exists}\models_{\mathcal{S}_{3}}\Phi$ , and thus $\Phi_{\exists}\equiv_{\mathcal{S}_{3}}\Phi$ . With Corollary 4.4 this yields $\Phi_{\exists}\equiv_{\mathcal{L}}\Phi$ . In the case where $\Phi=\{\varphi\}$ only contains a single sentence, we can apply compactness via entailment (Theorem 4.7), and obtain a finite $\Phi_{0}\subseteq\Phi_{\exists}$ such that $\Phi_{0}\models_{\mathcal{L}}\varphi$ . By Lemma 2.8, $\bigwedge\Phi_{0}$ is $\mathcal{L}$ -equivalent to a $\Sigma_{1}$ -sentence. $\hfill\blacktriangleleft$

5 Extension Preservation in the Finite

The classical Łos–Tarski theorem is known to fail in finite model theory, when both preservation and equivalence are restricted to finite structures. However, unlike for other model-theoretic properties, this does not immediately imply the failure of the theorem for other semirings, as sentences that are preserved under extensions in the Boolean sense may not be preserved in other semirings as well. Therefore, we study the question of whether there are semirings in which the extension preservation theorem remains true when restricted to finite universes. It turns out that in semiring semantics, the situation is much more diverse than in the Boolean world. In some cases, e.g. if we consider the natural semiring, we can easily adapt the counterexample used to disprove the extension preservation theorem in the general setting.

Theorem 5.1.

There is a sentence $\psi$ which is finite extension preserved in $\mathbb{N}$ (i.e. extension preserved on finite $\mathbb{N}$ -interpretations), but, on finite $\mathbb{N}$ -interpretations, it is not equivalent to any $\varphi\in\Sigma_{1}$ .

For other semirings, this is different. Despite the failure in the Boolean, the extension preservation theorem holds in the finite for the Viterbi and the Łukasiewicz semiring (and thus the tropical semiring and the semiring of doubt), and every lattice semiring with at least three elements. In this section, we discuss the key concepts and main proof ideas, and refer to the full version of this paper for a formal definition of all notions and proofs [7].

5.1 The Viterbi and Łukasiewicz Semiring

Recall the counterexample from Section 3. It relied on the fact that on $\mathbb{V}$ -interpretations of infinite universe, the sentence $\psi=\exists x\forall yRx$ is preserved under extensions. If we restrict ourselves to finite $\mathbb{V}$ -interpretations, this is no longer true as the universal quantifier generates a power to the size of the universe, and multiplication is strictly decreasing in $\mathbb{V}\setminus\{0,1\}$ . Consider, for example, the $\mathbb{V}$ -interpretation $\pi_{A}$ over the universe $\{a\}$ with $\pi_{A}(Ra)=1/2$ and its extension $\pi_{B}$ over $\{a,b\}$ with $\pi_{B}(Rb)=1/2$ , where we have $\pi_{A}\llbracket\psi\rrbracket=1/2>1/4=\pi_{B}\llbracket\psi\rrbracket$ . We will show that universal quantifiers, not just in this example, but always, make it impossible for a sentence to be extension preserved in the finite, except when: On sufficiently large $\mathbb{V}$ -interpretations, either the universal quantifier always evaluates to 1 (such as $\forall x(x=x)$ ) and can be replaced by $\top$ , or it does not actually contribute anything to the semantics of the formula and we can replace it with $\bot$ . As an example for the latter case, consider the sentence $\exists xRx\vee\forall xRx$ . While addition is increasing, multiplication is decreasing in $\mathbb{V}$ , so we have $\pi\llbracket\exists xRx\rrbracket\geq\pi\llbracket\forall xRx\rrbracket$ for all $\mathbb{V}$ -interpretations $\pi$ , and replacing the universal subformula with $\bot$ yields a $\mathbb{V}$ -equivalent sentence. Based on this idea, we show that the extension preservation theorem holds not just for $\mathbb{V}$ in the finite, but also for $\mathbb{T}\cong\mathbb{V}$ and $\mathbb{L}\cong\mathbb{D}$ .

Theorem 5.2.

Let $\mathcal{S}\in\{\mathbb{V},\mathbb{T},\mathbb{L},\mathbb{D}\}$ . A sentence $\psi\in\operatorname{FO}$ is finite extension preserved in $\mathcal{S}$ if, and only if, there is some $\varphi\in\Sigma_{1}$ which is equivalent to $\psi$ on finite $\mathcal{S}$ -interpretations.

The implication from syntax to semantics is covered by Lemma 2.9. It remains to prove the converse. The main steps of the proof are as follows.

(1)

Reduce the problem of equivalence to a $\Sigma_{1}$ -sentence to sufficiently large $\mathcal{S}$ -interpretations.
(2)

Track the contribution of subformulae to the semantics of a formula by means of so-called evaluation strategies – these are equivalent to strategies of the Verifier in the classical model checking game for FO.
(3)

Show that for extension preserved sentences and large $\mathcal{S}$ -interpretations, evaluation strategies that use a subformula $\forall y\varphi(\bar{a},y)$ are always dominated by ones that avoid universal quantifiers.
(4)

Remove all strategies using a subformula $\forall y\varphi(\bar{a},y)$ and rewrite the formula without universal quantifiers.

Equivalence on Large $\mathcal{S}$ -interpretations

Given a finite extension preserved sentence $\psi$ , our goal is to construct a finitely equivalent existential sentence. The first step is to argue that it suffices to find an existential sentence $\varphi$ which is equivalent on $\mathcal{S}$ -interpretations whose universe has at least a certain cardinality $n$ (denoted $\psi\equiv_{\mathcal{S}}^{\geq n}\varphi$ ). By replacing each universal quantifier of $\psi$ with an $n$ -ary conjunction, we can always find an existential sentence that is equivalent to $\varphi$ on $\mathcal{S}$ -interpretations of fixed size $n$ . Using extension preservation of $\psi$ and the fact that addition is the maximum with respect to the natural order²²2This is also true for $\mathbb{T}$ and $\mathbb{D}$ , where the natural order is the reverse of the usual order on $\mathbb{R}$ ., we can combine such formulae with $\varphi$ to obtain an existential sentence that is equivalent to $\psi$ on all finite $\mathcal{S}$ -interpretations (denoted by $\equiv_{\mathcal{S}}^{\omega}$ ).

Lemma 5.3.

Let $\mathcal{S}$ be additively idempotent. If $\psi$ is finite extension preserved in $\mathcal{S}$ and there is some $\varphi\in\Sigma_{1}$ and $n\in\omega$ such that $\varphi\equiv^{\geq n}_{\mathcal{S}}\psi$ , then there must be some $\varphi^{*}\in\Sigma_{1}$ such that $\varphi^{*}\equiv^{\omega}_{\mathcal{S}}\psi$ .

Strategies and their Valuation

The semiring semantics of a sentence can be defined via the notion of evaluation strategies. In order to avoid having to consider different equality types of instantiations, we use the variant $\operatorname{FO}^{\neq}$ of $\operatorname{FO}$ where we no longer have equality atoms and the quantifiers $\exists^{\neq},\forall^{\neq}$ only range over elements that do not occur in the instantiations of the free variables. Since formulae can be translated back and forth between $\operatorname{FO}$ and $\operatorname{FO}^{\neq}$ all results for $\operatorname{FO}^{\neq}$ readily translate to $\operatorname{FO}$ . We give a formal definition of $\operatorname{FO}^{\neq}$ and evaluation strategies in Appendix C. Intuitively, an evaluation strategy $\mathcal{T}$ for a sentence $\psi$ and an $\mathcal{S}$ -interpretation $\pi$ is given by specifying for each subformula $\varphi_{1}\lor\varphi_{2}$ of $\psi$ , whether we would like to evaluate $\varphi_{1}$ or $\varphi_{2}$ , and for each instantiated subformula $\exists^{\neq}x\varphi(\bar{a},x)$ , an instantiation of $x$ with an element of the universe that does not occur in $\bar{a}$ . Then the value of the strategy $\pi\llbracket\mathcal{T}\rrbracket$ is the product over all $\pi(L\bar{a})$ such that $L\bar{a}$ is an instantiated literal in $\psi$ that can be reached in the classical FO model-checking game in a play consistent with the (Verifier) strategy $\mathcal{T}$ . Essentially, these are all literals in subformulae of the disjuncts chosen by $\mathcal{T}$ with all variable instantiations consistent with the existential ones chosen by $\mathcal{T}$ .

Theorem 5.4 (Sum-of-Strategies [19]).

For every semiring $\mathcal{S}$ and every $\mathcal{S}$ -interpretation $\pi$ and $\psi\in\operatorname{FO}^{\neq}$ we have $\pi\llbracket\psi\rrbracket=\sum\{\pi\llbracket\mathcal{T}\rrbracket\mid% \mathcal{T}\text{ is an evaluation strategy for $\psi$ and $\pi$}\}$ .

Because addition is the maximum operation in $\mathbb{V}$ and $\mathbb{L}$ , by the above theorem, the valuation $\pi\llbracket\psi\rrbracket$ coincides with the maximum valuation of any evaluation strategy. We refer to such a strategy as optimal for $\pi$ and $\psi$ . We call a strategy existential if it does not use any subformula $\forall^{\neq}y\varphi(\bar{a},y)$ . The central claim we prove is that finite extension preservation implies redundancy of $\forall$ in $\psi$ , which means that for any sufficiently large $\mathcal{S}$ -interpretations $\pi$ there must always be an existential strategy which is optimal for $\pi$ and $\psi$ .

Existence of Existential Optimal Strategies

To prove this claim, we suppose that $\forall$ was not redundant in a finite extension preserved sentence $\psi$ . Starting from a non-existential strategy $\mathcal{T}$ optimal for an $\mathcal{S}$ -interpretation $\pi$ , we aim to infer a contradiction by disproving finite extension preservation of $\psi$ . Essentially, we make use of the fact that multiplication is strictly decreasing on $\mathcal{S}\setminus\{0,1\}$ to construct a strategy $\mathcal{T}^{*}$ for a subinterpretation $\pi^{*}$ of $\pi$ such that $\pi^{*}\llbracket\mathcal{T}^{*}\rrbracket>\pi\llbracket\mathcal{T}\rrbracket$ . By Theorem 5.4 and the optimality of $\mathcal{T}$ , this shows that $\psi$ is not finite extension preserved because $\pi^{*}\subseteq\pi$ , but $\pi^{*}\llbracket\psi\rrbracket\geq\pi^{*}\llbracket\mathcal{T}^{*}\rrbracket>% \pi\llbracket\mathcal{T}\rrbracket=\pi\llbracket\psi\rrbracket$ . Let $A$ denote the universe of $\pi$ and $A^{*}=A\setminus\{a\}$ the universe of $\pi^{*}$ . The idea is to construct the strategy $\mathcal{T}^{*}$ from $\mathcal{T}$ by restricting the instantiations of all universally quantified variables to elements of $A^{*}$ . Because $\mathcal{T}$ uses at least one subformula $\forall^{\neq}y\varphi(\bar{x},y)$ , this will remove at least one substrategy (where we instantiate $y$ with $a$ ). So if we can make sure that $\pi$ neither evaluates this substrategy to $1$ , nor the entire strategy $\mathcal{T}$ to $0$ , we obtain $\pi^{*}\llbracket\mathcal{T}^{*}\rrbracket>\pi\llbracket\mathcal{T}\rrbracket$ as desired. However, there are some technical intricacies to this: The strategy $\mathcal{T}$ may choose to instantiate existentially quantified variables with $a$ , so we have to show that we can find alternative choices without changing the valuation of the strategy too much. We show that this is always possible as long as sufficiently many elements from $A$ do not occur in any relational atom used in $\mathcal{T}$ . This construction of $\mathcal{T}^{*}$ from $\mathcal{T}$ , that we refer to as strategy translation, is the key new technique that we develop for this proof.

Lemma 5.5 (Strategy translation).

If there is an $\mathcal{S}$ -interpretation $\pi$ on a sufficiently large universe $A$ and a strategy $\mathcal{T}$ optimal for $\pi$ and $\psi$ such that (1) $\pi\llbracket\mathcal{T}\rrbracket>0$ , (2) $\mathcal{T}$ uses a subformula $\forall^{\neq}y\varphi(\bar{a},y)$ such that no substrategy for some $\varphi(\bar{a},b)$ is evaluated to $1$ , and (3) at least $\operatorname{qr}(\psi)+1$ elements of $A$ do not occur in any relational atom used in $\mathcal{T}$ , then $\psi$ cannot be finite extension preserved.

To finally argue that finite extension preservation implies redundancy of $\forall$ , we assume that $\forall$ was not redundant in a finite extension preserved sentence $\psi$ , and show that we can always find an $\mathcal{S}$ -interpretation that meets the conditions in Lemma 5.5, which yields the desired contradiction. Just from irredundancy of $\forall$ in $\psi$ , we only know the existence of arbitrarily large $\mathcal{S}$ -interpretations $\pi$ such that every strategy optimal for $\pi$ and $\psi$ is non-existential (that is, uses a subformula $\forall^{\neq}y\varphi(\bar{x},y)$ ). We call such $\mathcal{S}$ -interpretations counterexamples to redundancy of $\forall$ in $\psi$ . It remains to prove that we can find a sufficiently large such counterexample to redundancy that additionally satisfy condition (1)-(3) in Lemma 5.5. This will follow from three main lemmas.

Lemma 5.6.

Let $\psi\not\equiv^{\geq m}_{\mathcal{S}}\bot$ for each $m\in\mathbb{N}$ be finite extension preserved in $\mathcal{S}$ . If $\forall$ is not redundant in $\psi$ , then there are arbitrarily large counterexamples $\pi$ to redundancy of $\forall$ in $\psi$ such that $\pi\llbracket\psi\rrbracket>0$ and at least $\operatorname{qr}(\psi)+1$ elements of the universe are not used in any relational atom in any optimal strategy for $\psi$ .

Using the fact that there is no unique minimal positive element in $\mathcal{S}\in\{\mathbb{V},\mathbb{T},\mathbb{L},\mathbb{D}\}$ , Lemma 5.6 justifies that condition (1) and (3) from Lemma 5.5 can be met. The main idea in the proof of Lemma 5.6 is to extend a counterexample to redundancy of $\forall$ by $\operatorname{qr}(\psi)+1$ elements and to annotate all new literals with a sufficiently small value. Finite extension preservation then makes sure that no strategy optimal for this extension uses any of the newly added relational atoms.

What remains is to exclude the case that only substrategies with a $1$ -valuation are removed during the strategy translation (condition (2) in Lemma 5.5). To this end, we prove that one of the following two cases must occur: On sufficiently large $\mathcal{S}$ -interpretations $\pi$ , a subformula $\forall^{\neq}y\varphi(\bar{x},y)$ must either always be evaluated to $1$ , in which case we call it trivial and can simply rewrite it, or its strategies never evaluate to $1$ unless $1$ occurs as the annotation of a relational atom in $\pi$ . We show in Lemma 5.8 that occurrences of $1$ in $\operatorname{\mathsf{img}}(\pi)$ can be eliminated by replacing them by sufficiently large values $<1$ .

Lemma 5.7.

Let $\mathcal{S}\in\{\mathbb{V},\mathbb{T},\mathbb{L},\mathbb{D}\}$ . For every non-trivial formula $\varphi(\bar{x})$ there is some $n_{0}$ such that for all $n\geq n_{0}$ and $\mathcal{S}$ -interpretations $\pi$ of size $n$ with $1\not\in\operatorname{\mathsf{img}}(\pi)$ , it holds that $\pi\llbracket\mathcal{T}\rrbracket\neq 1$ for all strategies $\mathcal{T}$ for $\varphi(\bar{a})$ and all tuples $\bar{a}$ .

Lemma 5.8.

Let $\mathcal{S}\in\{\mathbb{V},\mathbb{T},\mathbb{L},\mathbb{D}\}$ . For every $\mathcal{S}$ -interpretation $\pi$ with $\pi\llbracket\psi\rrbracket>0$ there is an $\mathcal{S}$ -interpretation $\pi^{*}$ such that $\pi^{*}\llbracket\psi\rrbracket>0$ , $1\not\in\operatorname{\mathsf{img}}(\pi^{*})$ , and every strategy optimal for $\pi^{*}$ and $\psi$ is optimal for $\pi$ and $\psi$ , too.

Combining Lemma 5.6, Lemma 5.7, and Lemma 5.8 allows us to apply Lemma 5.5 and infer that finite extension preservation ensures redundancy of $\forall$ in the following way.

Theorem 5.9.

Let $\mathcal{S}\in\{\mathbb{V},\mathbb{T},\mathbb{L},\mathbb{D}\}$ and $\psi\in\operatorname{FO}$ be finite extension preserved in $\mathcal{S}$ such that $\psi\not\equiv^{\geq m}_{\mathcal{S}}\bot$ for all $m\in\mathbb{N}$ and such that every subformula $\forall^{\neq}y\varphi(\bar{x},y)$ of $\psi$ is non-trivial. Then $\forall$ must be redundant in $\psi$ .

Omitting Universal Quantifiers

The final argument is to show that we can syntactically remove universal subformulae from $\psi$ , provided that $\forall$ is redundant in $\psi$ . More precisely, we replace every non-trivial subformula $\forall^{\neq}y\varphi(\bar{a},y)$ with $\bot$ . Due to the existence of existential optimal strategies, this will maintain the valuation of at least one optimal strategy and thus the semantics of $\psi$ .

Theorem 5.10.

Let $\mathcal{S}\in\{\mathbb{V},\mathbb{T},\mathbb{L},\mathbb{D}\}$ and $\psi\in\operatorname{FO}$ be finite extension preserved in $\mathcal{S}$ such that every subformula $\forall^{\neq}y\varphi(\bar{x},y)$ of $\psi$ is non-trivial and $\psi\not\equiv^{\geq m}_{\mathcal{S}}\bot$ for all $m\in\mathbb{N}$ . Then $\psi\equiv^{\geq n}_{\mathcal{S}}\vartheta$ for some $n\in\mathbb{N}$ where $\vartheta$ arises from $\psi$ by substituting each non-trivial subformula $\forall^{\neq}y\varphi(\bar{a},y)$ with $\bot$ .

The harder direction of Theorem 5.2 now follows: With Theorem 5.10, we can rewrite the given finite extension preserved sentence $\psi$ (on large enough universes) to an existential sentence $\vartheta$ . By Lemma 5.3, this is sufficient to obtain an equivalent existential sentence on all universe sizes. Technically, there is a small gap between the assumptions of Theorem 5.2 and Theorem 5.10: The latter requires all universal subformulae to be non-trivial. This can be achieved by first suitably rewriting $\psi$ , but we defer the details to [7].

5.2 Lattice Semirings

The central ingredient to the proof of Theorem 5.2 is the existence of existential optimal strategies in the presence of finite extension preservation. Note that this argument really relied on the specific algebraic properties of the Viterbi and Łukasiewicz semiring and does not apply to the Boolean semiring. In fact, this argument does not work for any lattice semiring $\mathcal{L}$ , in which multiplication is idempotent. It is not just that the existence of any optimal strategy is not guaranteed in the case where $\mathcal{L}$ is not linearly ordered, even for min-max semirings it may be that all optimal strategies are non-existential. The sentence $\psi=\forall y\exists zRz\equiv_{\mathcal{L}}\exists zRz$ , for example, is finite extension preserved in $\mathcal{L}$ . However, it clearly does not admit any existential strategy, so in particular not an optimal one.

Surprisingly, by combining the techniques from Section 4 and Section 5, we can prove that the finite extension preservation theorem also holds for every lattice semiring apart from the Boolean one.

Theorem 5.11.

Let $\mathcal{L}\not\cong\mathbb{B}$ be a lattice semiring. A sentence $\psi\in\operatorname{FO}$ is finite extension preserved in $\mathcal{L}$ if, and only if, on finite $\mathcal{L}$ -interpretations, it is equivalent to an existential sentence.

To prove Theorem 5.11, we reuse the reduction method from Section 4 and restrict ourselves to the case where we evaluate in the fuzzy semiring $\mathbb{F}=([0,1],\max,\min,0,1)$ . The structure of the proof is similar to the one from Section 5: The first two steps are just the same. Due to its linear order, the notion of optimal strategies also applies to $\mathbb{F}$ . The existence of existential optimal strategies in step 3, however, has to be replaced by a weaker statement. Intuitively, the reason why finite extension preservation in $\mathbb{F}$ might still hold in the presence of universal quantifiers is that strategies might use subformulae $\forall y\varphi(\bar{x},y)$ , however, without actually relying on a literal that contains the universally quantified variable $y$ . In the example above, it is easy to rewrite $\psi$ as an existential sentence: Because no strategy uses a literal containing $y$ , we can simply delete the universal quantifier. A more complicated case occurs when strategies use a literal that contains $y$ for some instantiations, but not for all of them, which might happen if we consider $\psi=\forall y(\exists zRz\vee\exists z(Rz\wedge Qy))$ , for example. Therefore, we consider almost existential strategies, where whenever a subformula $\forall y\varphi(\bar{a},y)$ is used, at least one substrategy for some $\varphi(\bar{a},b)$ does not use any relational literal that contains $b$ . Using density of $\mathbb{F}$ , the main claim we prove is the following.

Lemma 5.12.

Let $\psi$ be finite extension preserved in $\mathbb{F}$ . For every sufficiently large $\mathbb{F}$ -interpretation $\pi$ , there must be an almost existential strategy optimal for $\pi$ and $\psi$ .

The proof requires a strategy translation lemma similar to the one we applied to $\mathbb{V}$ and $\mathbb{L}$ . Knowing just the existence of almost, but not necessarily fully, existential optimal strategies, we cannot replace all universal subformulae by $\bot$ right away as done in the Viterbi and Łukasiewicz case. Instead, in step 4 of the proof, we will first manipulate a given extension preserved sentence by basic logical equivalences to make sure that universal subformulae only occur at places where they do not admit almost existential strategies. This will allow us in the end to argue that such universal subformulae must be redundant and can be removed from the formula without changing its semantics. In the example above, we first transform $\psi={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall y% (}\exists zRz\vee\exists z(Rz\wedge Qy){\color[rgb]{0,0,1}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,1})}$ into $\exists zRz\vee{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0,1}\forall y}\exists z(Rz\wedge Qy)$ , which is $\mathbb{F}$ -equivalent by continuity, and then argue that $\psi\equiv_{\mathbb{F}}^{\omega}\exists zRz\vee\bot\equiv_{\mathbb{F}}\exists zRz$ as $\forall y\exists z(Rz\wedge Qy))$ can never be used in an almost existential strategy.

6 Conclusion

In this paper, we have provided a framework for studying the interplay between syntactic forms and semantic properties of first-order formulae evaluated in semirings beyond the classical Boolean case. As a first result, we have seen that preservation theorems do not always generalise to the semiring setting as, for instance, the extension preservation theorem fails for the tropical semiring, the Viterbi semiring, the Łukasiewicz semiring, and the natural semirings $\mathbb{N}$ and $\mathbb{N}^{\infty}$ . However, on the fairly broad class of lattice semirings we manage to recover the classical preservation theorems for homomorphisms, extensions and subinterpretations. The proof combines adaptations of classical methods from model theory, based on compactness and amalgamation, with a reduction technique specifically designed for semiring semantics. Results with a somewhat similar flavour have been studied in the context of certain many-valued logics [3, 10]. However, our framework differs from these studies in multiple ways: Our notions of preservation and logical equivalence are much more fine-grained as they do not just distinguish valuations of $1$ from those taking different values. Moreover, in our setting, elements of the algebraic structure in which we evaluate the formulae do not appear as constants in the logic (which has several relevant consequences as existential sentences can no longer describe the finite subinterpretations of a given interpretation), and we obtained positive results for arbitrary lattice semirings rather than just the finite linearly ordered ones. Surprisingly, the extension preservation theorem, which fails in finite model theory under Boolean semantics, does hold for a number of semirings including the tropical semiring, the Viterbi semiring, the Łukasiewicz semiring, and every non-Boolean lattice semiring, which is the second main contribution of this paper.

The results presented here suggest two main directions for future research: towards other semirings, and other preservation theorems (both in the finite and general case). More specifically, the approach employed for lattices might be applicable to other preservation theorems, for example concerning chain preservation. Moreover, we believe that the curious phenomenon of extension preservation in the finite deserves further investigation. We suspect that a similar proof technique could be used to establish extension preservation in the finite also for other semirings. For all we know, it is possible that the Boolean lattice is the only one which does not satisfy extension preservation in the finite. Exploring this question further would shed a new light on preservation theorems in finite model theory.

References

[1] A. Atserias and P. Kolaitis. Acyclicity, consistency, and positive semirings. In A. Palmigiano and M. Sadrzadeh, editors, Samson Abramsky on Logic and Structure in Computer Science and Beyond, volume 25 of Outstanding Contributions to Logic, pages 623–668. Springer, 2023. doi:10.1007/978-3-031-24117-8_17.
[2] A. Atserias and P. Kolaitis. Consistency of relations over monoids. Proc. ACM Manag. Data, 2(2):107, 2024. doi:10.1145/3651608.
[3] G. Badia, V. Costa, P. Dellunde, and C. Noguera. Syntactic characterizations of classes of first-order structures in mathematical fuzzy logic. Soft Comput., 23(7):2177–2186, 2019. doi:10.1007/S00500-019-03850-6.
[4] G. Badia, P. Kolaitis, and C. Noguera. Codd’s theorem for databases over semirings. Proc. ACM Manag. Data, 3(5):277:1–277:26, 2025. doi:10.1145/3767713.
[5] C. Bizière, E. Grädel, and M. Naaf. Locality Theorems in Semiring Semantics. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023), volume 272 of Leibniz International Proceedings in Informatics (LIPIcs), pages 20:1–20:15, 2023. doi:10.4230/LIPIcs.MFCS.2023.20.
[6] S. Brinke, A. Dawar, E. Grädel, L. Mrkonjić, and M. Naaf. Compactness in Semiring Semantics. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026), volume 363 of Leibniz International Proceedings in Informatics (LIPIcs), pages 13:1–13:21, 2026. doi:10.4230/LIPIcs.CSL.2026.13.
[7] S. Brinke, A. Dawar, E. Grädel, and B. Pago. Preservation Theorems in Semiring Semantics, 2026. arXiv:2605.10829.
[8] S. Brinke, E. Grädel, and L. Mrkonjić. Ehrenfeucht-Fraïssé Games in Semiring Semantics. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024), volume 288 of Leibniz International Proceedings in Informatics (LIPIcs), pages 19:1–19:22, 2024. doi:10.4230/LIPIcs.CSL.2024.19.
[9] S. Brinke, E. Grädel, L. Mrkonjić, and M. Naaf. Semiring Provenance in the Infinite. In The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen, volume 119 of Open Access Series in Informatics (OASIcs), pages 3:1–3:26, Dagstuhl, Germany, 2024. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/OASIcs.Tannen.3.
[10] J. Carr. Homomorphism preservation theorems for many-valued structures. ACM Transactions on Computational Logic, 2026. doi:10.1145/3793665.
[11] A. Dawar and A. Sankaran. Extension preservation in the finite and prefix classes of first order logic. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), pages 18:1–18:13, 2021. doi:10.4230/LIPIcs.CSL.2021.18.
[12] P. Dellunde and A. Vidal. Truth-preservartion under fuzzy pp-formulas. International Journal of Uncertainty, Fuzzyness, and Knowledge-Based Systems, 27:89–105, 2019. doi:10.1142/S0218488519400051.
[13] J. Nathan Foster, Todd J. Green, and Val Tannen. Annotated xml: queries and provenance. In Proceedings of the Twenty-Seventh ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS ’08, pages 271–280, 2008. doi:10.1145/1376916.1376954.
[14] B. Glavic. Data provenance. Foundations and Trends in Databases, 9(3-4):209–441, 2021. doi:10.1561/1900000068.
[15] E. Grädel, H. Helal, M. Naaf, and R. Wilke. Zero-One Laws and Almost Sure Valuations of First-Order Logic in Semiring Semantics. In LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, pages 41:1–41:12. ACM, 2022. doi:10.1145/3531130.3533358.
[16] E. Grädel, N. Lücking, and M. Naaf. Semiring provenance for Büchi games: Strategy analysis with absorptive polynomials. In P. Ganty and D. Bresolin, editors, Proceedings 12th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2021), volume 346 of EPTCS, pages 67–82, 2021. doi:10.4204/EPTCS.346.5.
[17] E. Grädel and L. Mrkonjić. Elementary equivalence versus isomorphism in semiring semantics. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021), volume 198, pages 133:1–133:20, Dagstuhl, Germany, 2021. doi:10.4230/LIPIcs.ICALP.2021.133.
[18] E. Grädel and V. Tannen. Provenance analysis for logic and games. Moscow Journal of Combinatorics and Number Theory, 9(3):203–228, 2020. Preprint available at https://arxiv.org/abs/1907.08470. doi:10.2140/moscow.2020.9.203.
[19] E. Grädel and V. Tannen. Provenance analysis and semiring semantics for first-order logic. In Model Theory, Computer Science and Graph Polynomials. Festschrift for Johann A. Makowsky. Birkhäuser, 2025. See also arXiv:2412.07986. doi:10.48550/arXiv.2412.07986.
[20] T. Green, G. Karvounarakis, and V. Tannen. Provenance semirings. In Proceedings of the Twenty-Sixth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS ’07, pages 31–40. Association for Computing Machinery, 2007. doi:10.1145/1265530.1265535.
[21] T. Green and V. Tannen. The Semiring Framework for Database Provenance. In Proceedings of the 36th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS ’17, pages 93–99. Association for Computing Machinery, 2017. doi:10.1145/3034786.3056125.
[22] Y. Gurevich. Towards logic tailored for computational complexity. In Computation and Proof Theory, pages 175–216. Springer Lecture Notes in Mathematics, 1984.
[23] A. Lopez. First Order Preservation Theorems in Finite Model Theory : Locality, Topology, and Limit Constructions. PhD thesis, University of Paris-Saclay, France, 2023. URL: https://tel.archives-ouvertes.fr/tel-04534568.
[24] L. Mrkonjić. Semiring Semantics: Algebraic Foundations, Model Theory, and Strategy Analysis. PhD thesis, RWTH Aachen University, 2025. URL: https://publications.rwth-aachen.de/record/1010223.
[25] M. Naaf. Logic, Semirings, and Fixed Points. PhD thesis, RWTH Aachen University, 2024. URL: https://publications.rwth-aachen.de/record/996756.
[26] E. Rosen. Some aspects of model theory on finite structures. Bulletin of Symbolic Logic, 8:380–403, 2002. doi:10.2178/BSL/1182353894.
[27] Benjamin Rossman. Homomorphism preservation theorems. J. ACM, 55(3), 2008. doi:10.1145/1379759.1379763.
[28] W. Tait. A counterexample to a conjecture of Scott and Suppes. Journal of Symbolic Logic, 24:15–16, 1959. doi:10.2307/2964569.

Appendix A Proofs from Section 2 and Section 3

Lemma 2.8. [Restated, see original statement.]

If $\psi$ is a positive Boolean combination of (positive) existential sentences, there is some $\varphi\in\Sigma_{1}$ ( $\varphi\in\Sigma_{1}^{+}$ ) such that $\psi\equiv_{\mathcal{S}}\varphi$ for all additively idempotent semirings $\mathcal{S}$ . If $\psi$ is a positive Boolean combination of universal sentences, there is some $\varphi\in\Pi_{1}$ such that $\psi\equiv_{\mathcal{L}}\varphi$ for all lattice semirings $\mathcal{L}$ .

Proof.

Let $\mathcal{S}$ be a semiring and $\exists\bar{x}\vartheta(\bar{x}),\exists\bar{y}\vartheta^{*}(\bar{y})\in% \operatorname{FO}_{A}(\tau)$ where $\bar{x}$ and $\bar{y}$ are disjoint tuples of variables. By (1) commutativity, associativity, and idempotence of addition, and (2) distributivity, we have the logical equivalences $\exists\bar{x}\vartheta(\bar{x})\circ\exists\bar{y}\vartheta^{*}(\bar{y})% \equiv_{\mathcal{S}}\exists\bar{x}\exists\bar{y}(\vartheta(\bar{x})\circ% \vartheta^{*}(\bar{y}))$ for $\circ\in\{\vee,\wedge\}$ in any semiring $\mathcal{S}$ since for any $\mathcal{S}$ -interpretation $\pi$ of universe $A$ ,

	$\displaystyle\pi\llbracket\exists\bar{x}\vartheta(\bar{x})\vee\exists\bar{y}% \vartheta^{*}(\bar{y})\rrbracket$	$\displaystyle=\sum_{\bar{a}\subseteq A}\pi\llbracket\vartheta(\bar{a})% \rrbracket+\sum_{\bar{a}\subseteq A}\pi\llbracket\vartheta^{*}(\bar{a})\rrbracket$
		$\displaystyle\overset{(1)}{=}\sum_{\bar{a}\subseteq A}\sum_{\bar{b}\subseteq A% }\pi\llbracket\vartheta(\bar{a})\rrbracket+\pi\llbracket\vartheta^{}(\bar{b})% \rrbracket=\pi\llbracket\exists\bar{x}\exists\bar{y}(\vartheta(\bar{x})\vee% \vartheta^{}(\bar{y}))\rrbracket\text{ and }$
	$\displaystyle\pi\llbracket\exists\bar{x}\vartheta(\bar{x})\wedge\exists\bar{y}% \vartheta^{*}(\bar{y})\rrbracket$	$\displaystyle=\sum_{\bar{a}\subseteq A}\pi\llbracket\vartheta(\bar{a})% \rrbracket\cdot\sum_{\bar{a}\subseteq A}\pi\llbracket\vartheta^{*}(\bar{a})\rrbracket$
		$\displaystyle\overset{(2)}{=}\sum_{\bar{a}\subseteq A}\sum_{\bar{b}\subseteq A% }\pi\llbracket\vartheta(\bar{a})\rrbracket\cdot\pi\llbracket\vartheta^{}(\bar% {b})\rrbracket=\pi\llbracket\exists\bar{x}\exists\bar{y}(\vartheta(\bar{x})% \wedge\vartheta^{}(\bar{y}))\rrbracket.$

Hence, the first claim follows by induction. In order to prove the second statement in an analogous way, we do not just need commutativity, associativity, and idempotence of multiplication, but also the dual distributivity law $\prod_{i\in I}s_{i}+\prod_{j\in J}t_{j}=\prod_{i\in I}\prod_{j\in J}(s_{i}+t_{% j})$ , where $(s_{i})_{i\in I},(t_{j})_{j\in J}\subseteq\mathcal{S}$ , which only holds in lattice semirings. In any lattice semiring $\mathcal{L}$ , however, we have the logical equivalences $\forall\bar{x}\vartheta(\bar{x})\vee\forall\bar{y}\vartheta^{*}(\bar{y})\equiv% _{\mathcal{L}}\forall\bar{x}\forall\bar{y}(\vartheta(\bar{x})\vee\vartheta^{*}% (\bar{y}))$ and $\forall\bar{x}\vartheta(\bar{x})\wedge\forall\bar{y}\vartheta^{*}(\bar{y})% \equiv_{\mathcal{L}}\forall\bar{x}\forall\bar{y}(\vartheta(\bar{x})\wedge% \vartheta^{*}(\bar{y}))$ , which inductively imply the second claim. $\hfill\blacktriangleleft$

Lemma 3.1. [Restated, see original statement.]

The sentence $\exists x\forall yRx$ is preserved under extensions in $\mathbb{N}^{\infty}$ but not $\mathbb{N}^{\infty}$ -equivalent to a $\Sigma_{1}$ -sentence.

Proof.

For $\mathbb{N}^{\infty}$ -interpretations $\pi_{A}\subseteq\pi_{B}$ we have that

\displaystyle\hskip-14.22636pt\pi_{A}\llbracket\psi\rrbracket=\sum_{a\in A}\pi% _{A}(Ra)^{|A|}\leq\sum_{a\in A}\pi_{A}(Ra)^{|B|}+\sum_{b\in B\setminus A}\pi_{% B}(Rb)^{|B|}=\sum_{b\in B}\pi_{B}(Rb)^{|B|}=\pi_{B}\llbracket\psi\rrbracket

because addition and exponentiation are increasing. Hence, $\psi$ is preserved under extensions in $\mathbb{N}^{\infty}$ . It remains to show that $\psi$ is not $\mathbb{N}^{\infty}$ -equivalent to a $\Sigma_{1}$ -sentence. For $n\in\omega$ , let $\pi_{n}$ be the $\mathbb{N}[\{x\}]$ -interpretation with universe $A_{n}\coloneqq\{a_{i}\mid i\in[n]\}$ and valuations $\pi_{n}(Ra_{i})=x$ and $\pi_{n}(\lnot Ra_{i})=0$ for all $a_{i}\in A_{n}$ . For $\varphi\in\Sigma_{1}$ , the valuation $\pi_{n}\llbracket\varphi\rrbracket$ is a polynomial whose degree is bounded by the length of $\varphi$ (and does not depend on $n$ ). However, $\pi_{n}\llbracket\psi\rrbracket=n\cdot x^{n}$ . So there must be some $n,m\in\omega$ such that for the homomorphism $h_{m}\colon\mathbb{N}[\{x\}]\to\mathbb{N}^{\infty}$ induced by $h_{m}(x)=m$ we have that $(h_{m}\circ\pi_{n})\llbracket\psi\rrbracket=h_{m}(\pi_{n}\llbracket\psi% \rrbracket)>h_{m}(\pi_{n}\llbracket\varphi\rrbracket)=(h_{m}\circ\pi_{n})% \llbracket\varphi\rrbracket$ . Hence, $\psi\not\equiv_{\mathbb{N}^{\infty}}\varphi$ . $\hfill\blacktriangleleft$

Lemma 3.2. [Restated, see original statement.]

For $\mathcal{S}\in\{\mathbb{V},\mathbb{D}\}$ , the set $\Phi\coloneqq\{\exists x_{1}\dots\exists x_{n}\bigwedge_{1\leq i<j\leq n}x_{i}% \neq x_{j}\mid n\in\omega\}\cup\{\exists x\forall yRx\}$ is preserved under extensions in $\mathcal{S}$ , but is not $\mathcal{S}$ -equivalent to a set of $\Sigma_{1}$ -sentences.

Proof.

Consider first the case $\mathcal{S}=\mathbb{V}$ . Let $\pi_{A}\subseteq\pi_{B}$ be $\mathbb{V}$ -interpretations. If $A$ is finite, we have that $\pi_{A}\llbracket\Phi\rrbracket=0\leq\pi_{B}\llbracket\Phi\rrbracket$ . So let $A$ (and thus $B$ , as $\pi_{A}\subseteq\pi_{B}$ ) be infinite. Then

\pi_{A}\llbracket\Phi\rrbracket=\bigsqcup_{a\in A}\prod_{a^{\prime}\in A}\pi_{% A}(Ra)=\bigsqcup_{a\in A}\pi_{A}(Ra)^{\infty}=\bigsqcup_{a\in A}\pi_{B}(Ra)^{% \infty}\leq\bigsqcup_{b\in B}\pi_{B}(Rb)^{\infty}=\pi_{B}\llbracket\Phi\rrbracket.

Hence, $\Phi$ is preserved under extensions in $\mathbb{V}$ .

Fix some chain $(r_{i})_{i\in\omega}\subseteq[0,1)_{\mathbb{R}}$ such that $\bigsqcup_{i\in\omega}r_{i}=1$ . Let $\pi_{A}$ be the $\mathbb{V}$ -interpretation over universe $A=\{a_{i}\mid i\in\omega\}$ where $\pi_{A}(Ra_{i})=r_{i}$ , and let $\pi_{B}$ be the extension of $\pi_{A}$ with universe $B\coloneqq A\uplus\{b\}$ with $\pi_{B}(Rb)=1$ . We have that $\pi_{A}\llbracket\Phi\rrbracket=0\neq 1=\pi_{B}\llbracket\Phi\rrbracket$ . We show that $\Phi$ cannot be $\mathbb{V}$ -equivalent to a set of $\Sigma_{1}$ -sentences by proving that for every $\varphi=\exists x_{1}\dots\exists x_{k}\psi(x_{1},\dots,x_{k})\in\Sigma_{1}$ with $\pi_{B}\llbracket\varphi\rrbracket=1$ , we also have $\pi_{A}\llbracket\varphi\rrbracket=1$ . So fix such a $\varphi\in\Sigma_{1}$ . Let $\varepsilon>0$ be arbitrary and consider a tuple $\bar{b}\in B^{k}$ .

Since $\pi_{B}\llbracket\psi(\bar{b})\rrbracket$ is a product of the valuations of literals $R(\bar{b})$ and $\lnot R(\bar{b})$ , we can replace each occurrence of the unique element $b\in B\setminus A$ in $\bar{b}$ by some sufficiently large $a_{i}\in A$ such that for the resulting tuple $\bar{a}$ we get $\pi_{A}\llbracket\psi(\bar{a})\rrbracket\geq\pi_{B}\llbracket\psi(\bar{b})% \rrbracket-\varepsilon$ . Since $\varepsilon>0$ and $\bar{b}\in B^{k}$ were arbitrary, this shows that

\pi_{A}\llbracket\varphi\rrbracket=\bigsqcup_{\bar{a}\in A^{k}}\pi_{A}% \llbracket\psi(\bar{a})\rrbracket=\bigsqcup_{\bar{b}\in B^{k}}\pi_{B}% \llbracket\psi(\bar{b})\rrbracket=1.

This finishes the case that $\mathcal{S}=\mathbb{V}$ . If $\mathcal{S}=\mathbb{D}$ , then the reasoning is analogous, with the difference that in $\mathbb{D}$ , the natural order is reversed: To be clear, let $\leq_{\mathbb{R}}$ denote the standard order on the interval $[0,1]_{\mathbb{R}}$ , and let $\leq_{\mathbb{D}}$ denote the order on $\mathbb{D}$ induced by the semiring addition operation, which is $\min$ in this case. Then $a\leq_{\mathbb{R}}b$ if and only if $b\leq_{\mathbb{D}}a$ . Let $\pi_{A}\subseteq\pi_{B}$ be $\mathbb{D}$ -interpretations. We can again assume that both $A$ and $B$ are infinite. Let $t_{>0}\colon\mathbb{D}\to\mathbb{D}$ be the function that maps $0$ to $0$ and every other element of $\mathbb{D}$ to $1$ . Also in $\mathbb{D}$ , $\Phi$ is preserved under extensions:

\pi_{A}\llbracket\Phi\rrbracket=\bigsqcap_{a\in A}\bigoplus_{a^{\prime}\in A}% \pi_{A}(Ra)=\bigsqcap_{a\in A}t_{>0}(\pi_{A}(Ra))\leq_{\mathbb{D}}\bigsqcap_{a% \in B}t_{>0}(\pi_{B}(Ra)).

The inequality is due to the fact that $B\supseteq A$ , so the right-hand side can only be less than the left-hand side with respect to $\leq_{\mathbb{R}}$ . To show that $\Phi$ is not $\mathbb{D}$ -equivalent to a set of $\Sigma_{1}$ -sentences, we use a dual construction to the previous one for $\pi_{A}$ and $\pi_{B}$ . That is, we fix a chain $(r_{i})_{i\in\omega}\subseteq(0,1]_{\mathbb{R}}$ such that $\bigsqcap_{i\in\omega}r_{i}=0$ . Let $\pi_{A}$ be the $\mathbb{V}$ -interpretation over universe $A=\{a_{i}\mid i\in\omega\}$ where $\pi_{A}(Ra_{i})=r_{i}$ , and let $\pi_{B}$ be the extension of $\pi_{A}$ by an additional element $b$ with $\pi_{B}(Rb)=0$ . We have that $\pi_{A}\llbracket\Phi\rrbracket=1\neq 0=\pi_{B}\llbracket\Phi\rrbracket$ . It remains to argue that for every $\varphi=\exists x_{1}\dots\exists x_{k}\psi(x_{1},\dots,x_{k})\in\Sigma_{1}$ , it is the case that $\pi_{B}\llbracket\varphi\rrbracket=0$ also implies $\pi_{A}\llbracket\varphi\rrbracket=0$ . This follows analogously as before by considering an arbitrary $\varepsilon>0$ and $\bar{b}\in B^{k}$ , and observing that by replacing each occurrence of the special element $b$ in $\bar{b}$ with a sufficiently small $a_{i}$ , we obtain a tuple $\bar{a}$ such that $\pi_{A}\llbracket\psi(\bar{a})\rrbracket\leq_{\mathbb{R}}\pi_{B}\llbracket\psi% (\bar{b})\rrbracket+\varepsilon$ . Hence, taking the infimum over all $\bar{a}\in A^{k}$ , we conclude that $\pi_{A}\llbracket\varphi\rrbracket=0$ and so, $\Phi$ cannot be $\mathbb{D}$ -equivalent to a set of $\Sigma_{1}$ -sentences. $\hfill\blacktriangleleft$

Appendix B Proofs from Section 4

Lemma 4.8. [Restated, see original statement.]

Let $\pi_{A}$ be an $\mathcal{S}_{3}$ -interpretation such that $\pi_{A}\llbracket\psi\rrbracket=1$ for all $\psi\in\Phi_{\exists}$ . Then there is an $\mathcal{S}_{3}$ -interpretation $\pi_{B}$ such that

(1)

$\pi_{B}\llbracket\Phi\rrbracket=1$ , and
(2)

$\pi_{B}\llbracket\psi\rrbracket\leq\varepsilon$ for all $\psi\in\Sigma_{1}$ with $\pi_{A}\llbracket\psi\rrbracket\leq\varepsilon$ .

Proof.

Let $\Psi\coloneqq\{\psi\in\Sigma_{1}\mid\pi_{A}\llbracket\psi\rrbracket\leq\varepsilon\}$ and suppose towards a contradiction that the set $\{(\varphi,\{1\})\mid\varphi\in\Phi\}\cup\{(\psi,\{0,\varepsilon\})\mid\psi\in\Psi\}$ was unsatisfiable. By compactness (Theorem 4.6), there must be a finite unsatisfiable subset. Let $\Psi_{0}\subseteq\Psi$ be such that $\{(\varphi,{1})\mid\varphi\in\Phi\}\cup\{(\psi,\{0,\varepsilon\})\mid\psi\in% \Psi_{0}\}$ is unsatisfiable. That means that every model-defining $\mathcal{S}_{3}$ -interpretation $\pi$ with $\pi\llbracket\Phi\rrbracket=1$ also satisfies $\pi\llbracket\bigvee\Psi_{0}\rrbracket=1$ . By Proposition 4.3, this implies $\Phi\models_{\mathcal{S}_{3}}\bigvee\Psi_{0}$ and since $\bigvee\Psi_{0}\equiv_{\mathcal{S}_{3}}\psi$ for some $\psi\in\Sigma_{1}$ (by Lemma 2.8), $\bigvee\Psi_{0}$ is $\mathcal{S}_{3}$ -equivalent to a formula in $\Phi_{\exists}$ . By assumption, $\pi_{A}\llbracket\bigvee\Psi_{0}\rrbracket=1$ , but we defined $\Psi$ such that $\pi_{A}\llbracket\psi\rrbracket\leq\varepsilon$ for all $\psi\in\Psi$ , a contradiction. $\hfill\blacktriangleleft$

Lemma 4.9 (Existential Amalgamation). [Restated, see original statement.]

Let $\pi_{A}$ and $\pi_{B}$ be $\mathcal{S}_{3}$ -interpretations such that $\pi_{B}\llbracket\psi\rrbracket\leq\varepsilon$ for all $\psi\in\Sigma_{1}$ with $\pi_{A}\llbracket\psi\rrbracket\leq\varepsilon$ . Then there is some $\pi_{C}\succeq\pi_{A}$ and an injective mapping $f\colon B\to C$ such that $\pi_{C}(Lf(\bar{b}))=1$ for all $L\bar{b}\in\operatorname{Lit}_{B}(\tau)$ with $\pi_{B}(L\bar{b})=1$ .

Proof.

Suppose that such a $\pi_{C}$ does not exist, i.e., that $\{(\varphi,\{\pi_{A}\llbracket\varphi\rrbracket\})\mid\varphi\in\operatorname{% FO}_{A}(\tau)\}\cup\{(\psi,\{1\})\mid\psi\in\Psi\}$ where $\Psi\coloneqq\{L\bar{b}\in\operatorname{Lit}_{B}(\tau)\mid\pi_{B}(L\bar{b})=1% \}\cup\{(b\neq b^{\prime},\{1\})\mid b\neq b^{\prime}\in B\}$ , is unsatisfiable. Let $\Psi_{0}\subseteq\Psi$ be finite such that $\{(\varphi,\{\pi_{A}\llbracket\varphi\rrbracket\})\mid\varphi\in\operatorname{% FO}\}\cup\{(\psi,\{1\})\mid\psi\in\Psi_{0}\}$ is unsatisfiable; this exists by Theorem 4.6. Consider the set $\Psi_{0}^{*}$ that is obtained from $\Psi_{0}$ by replacing each constant $b_{i}\in B$ with a variable $x_{i}$ . Since $\Psi_{0}$ is finite, only a fixed number $k$ of variables is needed. We claim that $\pi_{A}\llbracket\vartheta\rrbracket\leq\varepsilon$ where $\exists x_{1}\dots\exists x_{k}(\bigwedge_{1\leq i<j\leq k}x_{j}\neq x_{j}% \wedge\bigwedge\Psi_{0}^{*})$ . By assumption, this would imply $\pi_{B}\llbracket\vartheta\rrbracket\leq\varepsilon$ , which is in contradiction with the definition of $\Psi$ . Suppose that $\pi_{A}\llbracket\vartheta\rrbracket=1$ . Then there would be pairwise distinct $a_{1},\dots,a_{k}\in A$ such that $\pi_{A}(L\bar{a})=1$ for all $L(x_{1},\dots,x_{k})\in\Psi_{0}^{*}$ , and the expansion of $\pi_{A}$ where each constant $b_{i}\in B$ occurring in $\Psi_{0}$ is interpreted with $a_{i}$ would satisfy $\{(\varphi,\{\pi_{A}\llbracket\varphi\rrbracket\})\mid\varphi\in\operatorname{% FO}\}\cup\{(\psi,\{1\})\mid\psi\in\Psi_{0}\}$ , a contradiction. $\hfill\blacktriangleleft$

Appendix C Proofs from Section 5

In the proof of Theorem 5.2, we make use of the variant $\operatorname{FO}^{\neq}$ of $\operatorname{FO}$ . Formulae from $\operatorname{FO}^{\neq}$ only contain relational atoms, but no equality atoms, and rather than the usual quantifiers, they may contain quantifiers $\exists^{\neq},\forall^{\neq}$ with the semantics $\pi\llbracket\exists^{\neq}y\varphi(\bar{a},y)\rrbracket\coloneqq\sum_{b\in A% \setminus\bar{a}}\pi\llbracket\varphi(\bar{a},b)\rrbracket$ and $\pi\llbracket\forall^{\neq}y\varphi(\bar{a},y)\rrbracket\coloneqq\prod_{b\in A% \setminus\bar{a}}\pi\llbracket\varphi(\bar{a},b)\rrbracket.$ We also assume that all universes are of the form $[n]$ for some $n\in\mathbb{N}$ .

Definition C.1.

The model checking game graph for $\psi\in\operatorname{FO}^{\neq}$ and $n\geq\operatorname{qr}(\psi)$ is a labelled tree $C_{n}(\psi)=(V,E,\lambda)$ where each node $v$ is labelled by a subformula $\lambda(v)=\varphi(\bar{a})$ of $\psi$ which is instantiated with elements from $[n]$ . We inductively define $C_{n}(\varphi(\bar{a}))$ for $\varphi(\bar{a})\in\operatorname{FO}^{\neq}_{[n]}(\tau)$ and $n\geq\operatorname{qr}(\psi)$ in negation normal form as follows. In any case, the root of $C_{n}(\varphi(\bar{a}))$ is labelled $\varphi(\bar{a})$ . If $\varphi(\bar{a})$ is a literal or a Boolean constant, $C_{n}(\varphi(\bar{a}))$ consists of a single node. For $\varphi(\bar{a})=\varphi_{0}(\bar{a})\star\varphi_{1}(\bar{a})$ where $\star\in\{\vee,\wedge\}$ , in $C_{n}(\varphi(\bar{a}))$ we append $C_{n}(\varphi_{i}(\bar{a}))$ for $i\in\{0,1\}$ as subtrees to the root. Finally, if $\varphi(\bar{a})$ has the form $Qx\vartheta(\bar{a},x)$ where $Q\in\{\exists,\forall\}$ we now append the trees $C_{n}(\vartheta(\bar{a},b))$ for each $b\in[n]\setminus\bar{a}$ to the root.

Definition C.2.

An evaluation strategy (or just strategy) $\mathcal{T}$ for $\psi$ and $n\geq\operatorname{qr}(\psi)$ is a subtree of $C_{n}(\psi)$ where each node labelled with $\varphi_{0}(\bar{a})\vee\varphi_{1}(\bar{a})$ or $\exists x\vartheta(\bar{a},x)$ has exactly one successor and each node labelled with $\varphi_{0}(\bar{a})\wedge\varphi_{1}(\bar{a})$ or $\forall x\vartheta(\bar{a},x)$ contains all successors in $C_{n}(\psi)$ . We write $\mathcal{T}\in C_{n}(\psi)$ and define the valuation $\pi\llbracket\mathcal{T}\rrbracket$ in an $\mathcal{S}$ -interpretation $\pi$ of universe $[n]$ as the products of all valuations $\pi(L(\bar{a}))$ of the leaves in $\mathcal{T}$ .

Lemma 5.6. [Restated, see original statement.]

Let $\psi\not\equiv^{\geq m}_{\mathcal{S}}\bot$ for each $m\in\mathbb{N}$ be finite extension preserved in $\mathcal{S}$ . If $\forall$ is not redundant in $\psi$ , then there are arbitrarily large counterexamples $\pi$ to redundancy of $\forall$ in $\psi$ such that $\pi\llbracket\psi\rrbracket>0$ and at least $\operatorname{qr}(\psi)+1$ elements of the universe are not used in any relational atom in any optimal strategy for $\psi$ .

Proof.

First note that $\psi\not\equiv^{\geq m}_{\mathcal{S}}\bot$ for each $m\in\mathbb{N}$ , together with the fact that $\psi$ is finite extension preserved in $\mathcal{S}$ , implies that there must be some $m_{0}$ such that $\psi\not\equiv^{m}_{\mathcal{S}}\bot$ for all $m\geq m_{0}$ . Thereby, $\equiv^{m}_{\mathcal{S}}$ denotes equivalence on $\mathcal{S}$ -interpretations of size exactly $m$ . Fix some $n_{0}\in\mathbb{N}$ . Because $\forall$ is not redundant in $\psi$ , there must be a counterexample $\pi$ to redundancy of $\forall$ of universe $[n]$ where $n>\max(n_{0},m_{0},2^{|\psi|+1}+\operatorname{qr}(\psi))$ . We first justify that we can assume without loss of generality that $\pi\llbracket\psi\rrbracket>0$ : Suppose that $\pi\llbracket\psi\rrbracket=0$ . Then we must have $\pi\llbracket\mathcal{T}\rrbracket=0$ for all strategies $\mathcal{T}\in C_{n}(\psi)$ , but this means that every such $\mathcal{T}$ is optimal for $\pi$ and can thus not be existential. In this case, every $\mathcal{S}$ -interpretation of universe $[n]$ is a counterexample to redundancy in $\forall$ , and we can replace $\pi$ with some arbitrary $\mathcal{S}$ -interpretation which does not evaluate $\psi$ to $0$ . Such an $\mathcal{S}$ -interpretation must exist by $\psi\not\equiv^{n}_{\mathcal{S}}\bot$ (this is why we insisted on $n\geq m_{0}$ ).

Hence, we can fix some $0<v<\pi\llbracket\psi\rrbracket$ and define an extension $\pi_{\text{ext}}\supseteq\pi$ of universe $[n+r+1]$ such that $\pi_{\text{ext}}(\alpha)=v$ and $\pi_{\text{ext}}(\lnot\alpha)=0$ for $\alpha\in\text{Atoms}_{[n+r+1]\setminus[n]}(\tau)$ . We claim that $\pi_{\text{ext}}$ has the required properties. By finite extension preservation in $\mathcal{S}$ and the fact that $\pi\llbracket\psi\rrbracket>0$ , we have $\pi_{\text{ext}}\llbracket\psi\rrbracket>0$ . Let $\mathcal{T}_{\text{ext}}$ be a strategy optimal for $\pi_{\text{ext}}$ and $\psi$ . $\mathcal{T}_{\text{ext}}$ cannot use any literal $L\in\operatorname{Lit}_{[n+r+1]\setminus[n]}(\tau)$ , otherwise extension preservation would be violated due to $\pi\llbracket\psi\rrbracket>v\geq\pi_{\text{ext}}\llbracket\mathcal{T}_{\text{% ext}}\rrbracket=\pi_{\text{ext}}\llbracket\psi\rrbracket$ . It remains to argue that $\mathcal{T}_{\text{ext}}$ cannot be existential. So suppose it was. We translate $\mathcal{T}_{\text{ext}}$ into an existential strategy $\mathcal{T}$ with $\pi\llbracket\mathcal{T}\rrbracket=\pi_{\text{ext}}\llbracket\mathcal{T}_{% \text{ext}}\rrbracket$ to infer a contradiction. Note that although the elements $n+1,\dots,n+r+1$ are not used in a relational atom in $\mathcal{T}_{\text{ext}}$ they may still occur in $\mathcal{T}$ , as instantiation of an existential quantifier. The depth of $\mathcal{T}_{\text{ext}}$ is $|\psi|$ and its branching degree is at most $2$ . Hence, $\mathcal{T}$ has less than $2^{|\psi|+1}<n-r$ nodes, and there must be elements $i_{1},\dots,i_{r}\in[n]$ which do not occur at all in $\mathcal{T}_{\text{ext}}$ . Hence, swapping each occurrence of $n+j$ in $\mathcal{T}_{\text{ext}}$ with $i_{j}$ respects all inequalities between instantiations in $\mathcal{T}_{\text{ext}}$ (recall that at a position $\exists^{\neq}y\varphi(\bar{a},y)$ , some $b\not\in\bar{a}$ has to be chosen). Further, neither $i_{j}$ nor $n+j$ occurs inside a literal in $\mathcal{T}_{\text{ext}}$ , which ensures $\pi\llbracket\mathcal{T}\rrbracket=\pi_{\text{ext}}\llbracket\mathcal{T}_{% \text{ext}}\rrbracket$ . But, by extension preservation, $\pi\llbracket\mathcal{T}\rrbracket=\pi_{\text{ext}}\llbracket\mathcal{T}_{% \text{ext}}\rrbracket=\pi_{\text{ext}}\llbracket\psi\rrbracket\geq\pi% \llbracket\psi\rrbracket$ , so $\mathcal{T}$ would be an existential strategy optimal for $\pi$ and $\psi$ , a contradiction. $\hfill\blacktriangleleft$

Lemma 5.8. [Restated, see original statement.]

Let $\mathcal{S}\in\{\mathbb{V},\mathbb{T},\mathbb{L},\mathbb{D}\}$ . For every $\mathcal{S}$ -interpretation $\pi$ with $\pi\llbracket\psi\rrbracket>0$ there is an $\mathcal{S}$ -interpretation $\pi^{*}$ such that $\pi^{*}\llbracket\psi\rrbracket>0$ , $1\not\in\operatorname{\mathsf{img}}(\pi^{*})$ , and every strategy optimal for $\pi^{*}$ and $\psi$ is optimal for $\pi$ and $\psi$ , too.

Proof.

In what follows, we extend the set of evaluation strategies $C_{n}(\psi)$ by a dummy element $\mathcal{T}_{\bot}$ whose evaluation is fixed to be $0$ (note that $\mathcal{T}_{\bot}$ is not a strategy in the sense of ˜C.2). Each $\mathcal{S}$ -interpretation of universe $[n]$ induces a preorder on $C_{n}(\psi)\cup\{\mathcal{T}_{\bot}\}$ in the following way: We set $\mathcal{T}\preceq_{\pi}\mathcal{T}^{\prime}$ whenever $\pi\llbracket\mathcal{T}\rrbracket\leq\pi\llbracket\mathcal{T}^{\prime}\rrbracket$ . From $\pi$ we construct an $\mathcal{S}$ -interpretation $\pi^{*}$ such that $1\not\in\operatorname{\mathsf{img}}(\pi^{*})$ and claim that $\preceq_{\pi^{*}}\subseteq\preceq_{\pi}$ . Because $C_{n}(\psi)\cup\{\mathcal{T}_{\bot}\}$ is finite, there exist $\delta,e$ such that $\delta\coloneqq\min\{\pi\llbracket\mathcal{T}\rrbracket-\pi\llbracket\mathcal{% T}^{\prime}\rrbracket\mid\mathcal{T}^{\prime}\prec_{\pi}\mathcal{T}\}$ and $e$ is the maximum number of leaves of strategies in $C_{n}(\psi)$ .

\blacksquare

First consider the case $\mathcal{S}=\mathbb{V}$ . Fix some $s$ with $\sqrt[e]{1-\frac{\delta}{\pi\llbracket\psi\rrbracket}}<s<1$ and set $\pi^{*}(L)=\pi(L)$ if $\pi(L)\neq 1$ and otherwise $\pi^{*}(L)=s$ . Now let $\mathcal{T}\succ_{\pi}\mathcal{T}^{\prime}$ , i.e. $\pi\llbracket\mathcal{T}\rrbracket-\pi\llbracket\mathcal{T}^{\prime}\rrbracket\geq\delta$ . We claim that $\mathcal{T}\succ_{\pi^{*}}\mathcal{T}^{\prime}$ . Using $\pi\llbracket\mathcal{T}\rrbracket\leq\pi\llbracket\psi\rrbracket$ $(*)$ by the Sum-Of-Strategy Theorem, we obtain

	$\displaystyle\pi^{}\llbracket\mathcal{T}\rrbracket-\pi^{}\llbracket\mathcal{% T}^{\prime}\rrbracket$	$\displaystyle\geq\pi^{*}\llbracket\mathcal{T}\rrbracket-\pi\llbracket\mathcal{% T}^{\prime}\rrbracket$
		$\displaystyle\geq s^{e}\cdot\pi\llbracket\mathcal{T}\rrbracket-\pi\llbracket% \mathcal{T}^{\prime}\rrbracket$
		$\displaystyle>(1-\delta/\pi\llbracket\psi\rrbracket)\cdot\pi\llbracket\mathcal% {T}\rrbracket-\pi\llbracket\mathcal{T}^{\prime}\rrbracket$
		$\displaystyle\geq\pi\llbracket\mathcal{T}\rrbracket-(\delta\cdot\pi\llbracket% \mathcal{T}\rrbracket)/\pi\llbracket\psi\rrbracket-\pi\llbracket\mathcal{T}^{% \prime}\rrbracket$
		$\displaystyle\overset{(*)}{\geq}\pi\llbracket\mathcal{T}\rrbracket-\delta-\pi% \llbracket\mathcal{T}^{\prime}\rrbracket\geq 0.$

Hence, $\mathcal{T}\succ_{\pi^{*}}\mathcal{T}^{\prime}$ and we overall obtain $\preceq_{\pi^{*}}\subseteq\preceq_{\pi}$ .

$\blacksquare$

Now let $\mathcal{S}=\mathbb{D}$ . Due to $+^{\mathbb{D}}=\min$ , the natural order of $\mathbb{D}$ is inverted, and $0^{\mathbb{D}}=1$ and $1^{\mathbb{D}}=0$ . We denote by $\leq_{\mathbb{R}}$ the usual order on $[0,1]_{\mathbb{R}}$ . Now fix some $1^{\mathbb{D}}=0<_{\mathbb{R}}s<_{\mathbb{R}}\delta/e$ and, as before, set $\pi^{*}(L)=\pi(L)$ if $\pi(L)\neq 0=1^{\mathbb{D}}$ and $\pi^{*}(L)=s$ otherwise. Let $\mathcal{T}\succ_{\pi}\mathcal{T}^{\prime}$ , i.e. $\pi\llbracket\mathcal{T}\rrbracket<_{\mathbb{R}}\pi\llbracket\mathcal{T}^{% \prime}\rrbracket$ and thus $\pi\llbracket\mathcal{T}^{\prime}\rrbracket-\pi\llbracket\mathcal{T}^{\prime}% \rrbracket\geq_{\mathbb{R}}\delta$ . We have

$\displaystyle\pi^{*}\llbracket\mathcal{T}^{\prime}\rrbracket-\pi^{*}\llbracket% \mathcal{T}\rrbracket$ $\displaystyle\geq_{\mathbb{R}}\pi\llbracket\mathcal{T}^{\prime}\rrbracket-\pi^% {*}\llbracket\mathcal{T}\rrbracket$

$\displaystyle\overset{(*)}{\geq}_{\mathbb{R}}\pi\llbracket\mathcal{T}^{\prime}% \rrbracket-(e\cdot s+\pi\llbracket\mathcal{T}\rrbracket)$

$\displaystyle>\pi\llbracket\mathcal{T}^{\prime}\rrbracket-\delta-\pi\llbracket% \mathcal{T}\rrbracket\geq 0$

Note in $(*)$ that $e\cdot s+\pi\llbracket\mathcal{T}\rrbracket$ cannot exceed $1$ because we take into account the dummy strategy $\mathcal{T}_{\bot}$ , which always evaluates to $1=0^{\mathbb{D}}$ , when defining $\delta$ . As before, it follows that $\mathcal{T}\succ_{\pi^{*}}\mathcal{T}^{\prime}$ , proving $\preceq_{\pi^{*}}\subseteq\preceq_{\pi}$ .

Now note that we must have $\pi^{*}\llbracket\psi\rrbracket>0$ . Otherwise we would have $\pi^{*}\llbracket\mathcal{T}\rrbracket=0$ , i.e. $\mathcal{T}\preceq_{\pi^{*}}\mathcal{T}_{\bot}$ , for all $\mathcal{T}\in C_{n}(\psi)$ while $\pi\llbracket\mathcal{T}\rrbracket>0$ , i.e. $\mathcal{T}\not\preceq_{\pi}\mathcal{T}_{\bot}$ , for some $\mathcal{T}\in C_{n}(\psi)$ according to the Sum-Of-Strategies Theorem. Let $\mathcal{T}$ be a strategy optimal for $\pi^{*}$ and $\psi$ . This means that $\mathcal{T}\succeq_{\pi^{*}}\mathcal{T}^{\prime}$ for all $\mathcal{T}^{\prime}\in C_{n}(\psi)$ and thus $\mathcal{T}\succeq_{\pi}\mathcal{T}^{\prime}$ for all $\mathcal{T}^{\prime}\in C_{n}(\psi)$ , implying that $\mathcal{T}$ must be optimal for $\pi$ and $\psi$ too. $\hfill\blacktriangleleft$

Theorem 5.9. [Restated, see original statement.]

Let $\mathcal{S}\in\{\mathbb{V},\mathbb{T},\mathbb{L},\mathbb{D}\}$ and $\psi\in\operatorname{FO}$ be finite extension preserved in $\mathcal{S}$ such that $\psi\not\equiv^{\geq m}_{\mathcal{S}}\bot$ for all $m\in\mathbb{N}$ and such that every subformula $\forall^{\neq}y\varphi(\bar{x},y)$ of $\psi$ is non-trivial. Then $\forall$ must be redundant in $\psi$ .

Proof.

Suppose that $\forall$ was not redundant in $\psi$ , and let $n_{0}$ be sufficiently large to apply Lemma 5.5 and Lemma 5.7 to every subformula $\forall^{\neq}y\varphi(\bar{x},y)$ of $\psi$ . By Lemma 5.6, there must be a counterexample $\pi$ to redundancy of $\forall$ of size $n\geq n_{0}$ such that $\pi\llbracket\psi\rrbracket>0$ and such that at least $\operatorname{qr}(\psi)+1$ elements do not occur inside the literals used in any optimal strategy. Transform $\pi$ into an $\mathcal{S}$ -interpretation $\pi^{*}$ such that $1\not\in\operatorname{\mathsf{img}}(\pi^{*})$ according to Lemma 5.8. Every strategy optimal for $\pi^{*}$ and $\psi$ must be optimal for $\pi$ and $\psi$ and thus non-existential such that at least $\operatorname{qr}(\psi)+1$ elements do not occur inside the literals of the strategy. Further, $\pi^{*}\llbracket\psi\rrbracket>0$ because $\pi\llbracket\psi\rrbracket>0$ . Fix some strategy $\mathcal{T}$ optimal for $\pi^{*}$ and $\psi$ and a subformula $\forall^{\neq}y\varphi(\bar{x},y)$ used in $\mathcal{T}$ . Because $\forall^{\neq}y\varphi(\bar{x},y)$ is non-trivial, $\varphi(\bar{x},y)$ must be non-trivial too, and as $1\not\in\operatorname{\mathsf{img}}(\pi^{*})$ , we know by Lemma 5.7 that $\pi^{*}\llbracket\mathcal{T}\rrbracket\neq 1$ for all strategies $\mathcal{T}$ for $\varphi(\bar{a},b)$ and all $b\not\in\bar{a}$ . Hence, we can invoke Lemma 5.5 and obtain a contradiction to finite extension preservation of $\psi$ . $\hfill\blacktriangleleft$

Theorem 5.10. [Restated, see original statement.]

Let $\mathcal{S}\in\{\mathbb{V},\mathbb{T},\mathbb{L},\mathbb{D}\}$ and $\psi\in\operatorname{FO}$ be finite extension preserved in $\mathcal{S}$ such that every subformula $\forall^{\neq}y\varphi(\bar{x},y)$ of $\psi$ is non-trivial and $\psi\not\equiv^{\geq m}_{\mathcal{S}}\bot$ for all $m\in\mathbb{N}$ . Then $\psi\equiv^{\geq n}_{\mathcal{S}}\vartheta$ for some $n\in\mathbb{N}$ where $\vartheta$ arises from $\psi$ by substituting each non-trivial subformula $\forall^{\neq}y\varphi(\bar{a},y)$ with $\bot$ .

Proof.

Apply Theorem 5.9 to $\psi$ and infer that $\forall$ is redundant in $\psi$ . Let $n\in\mathbb{N}$ be such that for every $\mathcal{S}$ -interpretation $\pi$ of size at least $n$ there exists an existential strategy optimal for $\pi$ and $\psi$ . Now note that for every existential strategy for $\psi$ there is a strategy for $\vartheta$ with the same valuation and vice versa unless it uses $\bot$ and evaluates to $0$ . For any $\mathcal{S}$ -interpretation of universe $[m]$ where $m\geq n$ we have

	$\displaystyle\pi\llbracket\psi\rrbracket$	$\displaystyle=\max\{\pi\llbracket\mathcal{T}\rrbracket\mid\mathcal{T}\in C_{m}% (\psi)\}$
		$\displaystyle=\max\{\pi\llbracket\mathcal{T}\rrbracket\mid\mathcal{T}\in C_{m}% (\psi)\text{ existential}\}$
		$\displaystyle=\max\{\pi\llbracket\mathcal{T}\rrbracket\mid\mathcal{T}\in C_{m}% (\vartheta)\}=\pi\llbracket\vartheta\rrbracket.$

So overall we obtain $\psi\equiv_{\mathcal{S}}^{\geq n}\vartheta$ . $\hfill\blacktriangleleft$

[bib.bib1] [1] A. Atserias and P. Kolaitis. Acyclicity, consistency, and positive semirings. In A. Palmigiano and M. Sadrzadeh, editors, Samson Abramsky on Logic and Structure in Computer Science and Beyond, volume 25 of Outstanding Contributions to Logic, pages 623–668. Springer, 2023. doi:10.1007/978-3-031-24117-8_17.

[bib.bib2] [2] A. Atserias and P. Kolaitis. Consistency of relations over monoids. Proc. ACM Manag. Data, 2(2):107, 2024. doi:10.1145/3651608.

[bib.bib3] [3] G. Badia, V. Costa, P. Dellunde, and C. Noguera. Syntactic characterizations of classes of first-order structures in mathematical fuzzy logic. Soft Comput., 23(7):2177–2186, 2019. doi:10.1007/S00500-019-03850-6.

[bib.bib4] [4] G. Badia, P. Kolaitis, and C. Noguera. Codd’s theorem for databases over semirings. Proc. ACM Manag. Data, 3(5):277:1–277:26, 2025. doi:10.1145/3767713.

[bib.bib5] [5] C. Bizière, E. Grädel, and M. Naaf. Locality Theorems in Semiring Semantics. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023), volume 272 of Leibniz International Proceedings in Informatics (LIPIcs), pages 20:1–20:15, 2023. doi:10.4230/LIPIcs.MFCS.2023.20.

[bib.bib6] [6] S. Brinke, A. Dawar, E. Grädel, L. Mrkonjić, and M. Naaf. Compactness in Semiring Semantics. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026), volume 363 of Leibniz International Proceedings in Informatics (LIPIcs), pages 13:1–13:21, 2026. doi:10.4230/LIPIcs.CSL.2026.13.

[bib.bib7] [7] S. Brinke, A. Dawar, E. Grädel, and B. Pago. Preservation Theorems in Semiring Semantics, 2026. arXiv:2605.10829.

[bib.bib8] [8] S. Brinke, E. Grädel, and L. Mrkonjić. Ehrenfeucht-Fraïssé Games in Semiring Semantics. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024), volume 288 of Leibniz International Proceedings in Informatics (LIPIcs), pages 19:1–19:22, 2024. doi:10.4230/LIPIcs.CSL.2024.19.

[bib.bib9] [9] S. Brinke, E. Grädel, L. Mrkonjić, and M. Naaf. Semiring Provenance in the Infinite. In The Provenance of Elegance in Computation - Essays Dedicated to Val Tannen, volume 119 of Open Access Series in Informatics (OASIcs), pages 3:1–3:26, Dagstuhl, Germany, 2024. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi:10.4230/OASIcs.Tannen.3.

[bib.bib10] [10] J. Carr. Homomorphism preservation theorems for many-valued structures. ACM Transactions on Computational Logic, 2026. doi:10.1145/3793665.

[bib.bib11] [11] A. Dawar and A. Sankaran. Extension preservation in the finite and prefix classes of first order logic. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), pages 18:1–18:13, 2021. doi:10.4230/LIPIcs.CSL.2021.18.

[bib.bib12] [12] P. Dellunde and A. Vidal. Truth-preservartion under fuzzy pp-formulas. International Journal of Uncertainty, Fuzzyness, and Knowledge-Based Systems, 27:89–105, 2019. doi:10.1142/S0218488519400051.

[bib.bib13] [13] J. Nathan Foster, Todd J. Green, and Val Tannen. Annotated xml: queries and provenance. In Proceedings of the Twenty-Seventh ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS ’08, pages 271–280, 2008. doi:10.1145/1376916.1376954.

[bib.bib14] [14] B. Glavic. Data provenance. Foundations and Trends in Databases, 9(3-4):209–441, 2021. doi:10.1561/1900000068.

[bib.bib15] [15] E. Grädel, H. Helal, M. Naaf, and R. Wilke. Zero-One Laws and Almost Sure Valuations of First-Order Logic in Semiring Semantics. In LICS ’22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, pages 41:1–41:12. ACM, 2022. doi:10.1145/3531130.3533358.

[bib.bib16] [16] E. Grädel, N. Lücking, and M. Naaf. Semiring provenance for Büchi games: Strategy analysis with absorptive polynomials. In P. Ganty and D. Bresolin, editors, Proceedings 12th International Symposium on Games, Automata, Logics, and Formal Verification (GandALF 2021), volume 346 of EPTCS, pages 67–82, 2021. doi:10.4204/EPTCS.346.5.

[bib.bib17] [17] E. Grädel and L. Mrkonjić. Elementary equivalence versus isomorphism in semiring semantics. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021), volume 198, pages 133:1–133:20, Dagstuhl, Germany, 2021. doi:10.4230/LIPIcs.ICALP.2021.133.

[bib.bib18] [18] E. Grädel and V. Tannen. Provenance analysis for logic and games. Moscow Journal of Combinatorics and Number Theory, 9(3):203–228, 2020. Preprint available at https://arxiv.org/abs/1907.08470. doi:10.2140/moscow.2020.9.203.

[bib.bib19] [19] E. Grädel and V. Tannen. Provenance analysis and semiring semantics for first-order logic. In Model Theory, Computer Science and Graph Polynomials. Festschrift for Johann A. Makowsky. Birkhäuser, 2025. See also arXiv:2412.07986. doi:10.48550/arXiv.2412.07986.

[bib.bib20] [20] T. Green, G. Karvounarakis, and V. Tannen. Provenance semirings. In Proceedings of the Twenty-Sixth ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS ’07, pages 31–40. Association for Computing Machinery, 2007. doi:10.1145/1265530.1265535.

[bib.bib21] [21] T. Green and V. Tannen. The Semiring Framework for Database Provenance. In Proceedings of the 36th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, PODS ’17, pages 93–99. Association for Computing Machinery, 2017. doi:10.1145/3034786.3056125.

[bib.bib22] [22] Y. Gurevich. Towards logic tailored for computational complexity. In Computation and Proof Theory, pages 175–216. Springer Lecture Notes in Mathematics, 1984.

[bib.bib23] [23] A. Lopez. First Order Preservation Theorems in Finite Model Theory : Locality, Topology, and Limit Constructions. PhD thesis, University of Paris-Saclay, France, 2023. URL: https://tel.archives-ouvertes.fr/tel-04534568.

[bib.bib24] [24] L. Mrkonjić. Semiring Semantics: Algebraic Foundations, Model Theory, and Strategy Analysis. PhD thesis, RWTH Aachen University, 2025. URL: https://publications.rwth-aachen.de/record/1010223.

[bib.bib25] [25] M. Naaf. Logic, Semirings, and Fixed Points. PhD thesis, RWTH Aachen University, 2024. URL: https://publications.rwth-aachen.de/record/996756.

[bib.bib26] [26] E. Rosen. Some aspects of model theory on finite structures. Bulletin of Symbolic Logic, 8:380–403, 2002. doi:10.2178/BSL/1182353894.

[bib.bib27] [27] Benjamin Rossman. Homomorphism preservation theorems. J. ACM, 55(3), 2008. doi:10.1145/1379759.1379763.

[bib.bib28] [28] W. Tait. A counterexample to a conjecture of Scott and Suppes. Journal of Symbolic Logic, 24:15–16, 1959. doi:10.2307/2964569.

	$\displaystyle\pi^{}\llbracket\mathcal{T}^{\prime}\rrbracket-\pi^{}\llbracket% \mathcal{T}\rrbracket$	$\displaystyle\geq_{\mathbb{R}}\pi\llbracket\mathcal{T}^{\prime}\rrbracket-\pi^% {*}\llbracket\mathcal{T}\rrbracket$
		$\displaystyle\overset{(*)}{\geq}_{\mathbb{R}}\pi\llbracket\mathcal{T}^{\prime}% \rrbracket-(e\cdot s+\pi\llbracket\mathcal{T}\rrbracket)$
		$\displaystyle>\pi\llbracket\mathcal{T}^{\prime}\rrbracket-\delta-\pi\llbracket% \mathcal{T}\rrbracket\geq 0$

Preservation Theorems in Semiring Semantics

Abstract

Keywords and phrases:

Category:

Copyright and License:

2012 ACM Subject Classification:

Related Version:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Preservation Theorems

Semiring Semantics

Our Contributions

2 Semiring Semantics for First-order Logic

Definition 2.1.

Definition 2.2 (Semiring interpretations).

Definition 2.3 (Semiring Semantics).

Lemma 2.4 (Fundamental Property).

Definition 2.5 (Entailment).

Notions of Preservation in Semiring Semantics

Definition 2.6 (Homomorphisms and Subinterpretations).

Definition 2.7 (Preservation).

Lemma 2.8.

Lemma 2.9.

3 Failure of Extension Preservation in General Semirings

Lemma 3.1.

Lemma 3.2.

4 Preservation Theorems in Lattice Semirings

Theorem 4.1.

Proof Methods from Semiring Semantics

Proposition 4.2.

Proposition 4.3.

Corollary 4.4.

Definition 4.5.

Theorem 4.6 ([24]).

Theorem 4.7 ([6]).

Extension Preservation

Lemma 4.8.

Lemma 4.9 (Existential Amalgamation).

Theorem 4.10.

Proof.

Theorem 4.11.

Proof.

5 Extension Preservation in the Finite

Theorem 5.1.

5.1 The Viterbi and Łukasiewicz Semiring

Theorem 5.2.

Equivalence on Large 𝓢-interpretations

Lemma 5.3.

Strategies and their Valuation

Theorem 5.4 (Sum-of-Strategies [19]).

Existence of Existential Optimal Strategies

Lemma 5.5 (Strategy translation).

Lemma 5.6.

Lemma 5.7.

Lemma 5.8.

Theorem 5.9.

Omitting Universal Quantifiers

Theorem 5.10.

5.2 Lattice Semirings

Theorem 5.11.

Lemma 5.12.

6 Conclusion

References

Appendix A Proofs from Section 2 and Section 3

Lemma 2.8. [Restated, see original statement.]

Proof.

Lemma 3.1. [Restated, see original statement.]

Proof.

Lemma 3.2. [Restated, see original statement.]

Proof.

Appendix B Proofs from Section 4

Lemma 4.8. [Restated, see original statement.]

Proof.

Lemma 4.9 (Existential Amalgamation). [Restated, see original statement.]

Proof.

Appendix C Proofs from Section 5

Definition C.1.

Equivalence on Large $\mathcal{S}$ -interpretations