Compactness in Semiring Semantics

Brinke, Sophie; Dawar, Anuj; Grädel, Erich; Mrkonjić, Lovro; Naaf, Matthias

doi:10.4230/LIPIcs.CSL.2026.13

Compactness in Semiring Semantics

Sophie Brinke

RWTH Aachen University, Germany Anuj Dawar

University of Cambridge, UK Erich Grädel

RWTH Aachen University, Germany Lovro Mrkonjić

RWTH Aachen University, Germany Matthias Naaf

RWTH Aachen University, Germany

Abstract

Semiring provenance was originally introduced in database theory with the aim of explaining why certain tuples are (not) contained in the answer of a query. To this end, logical statements are not just evaluated to true or false but 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. Recently, this approach has been expanded to a systematic study of semiring semantics for first-order logic and other logical systems. This raises the question to what extent model-theoretic results can be generalised to semiring semantics and how this relates to the algebraic properties of the underlying semiring.

Here we investigate the availability of compactness in semiring semantics. The appropriate setting for this is based on absorptive semirings with well-defined infinitary products. Compactness can be stated either in terms of satisfiability or in terms of entailment, and these two variants are trivially equivalent in Boolean semantics. However, this is no longer the case in semiring semantics. Compactness in terms of satisfiability, defined as the existence of non-zero valuations, indeed generalises to every infinitary absorptive semiring. For compactness in terms of entailment the situation is different. The entailment relation naturally extends to semiring semantics (via the natural order on the semiring) but this yields a stronger variant of compactness, which fails for certain important semirings, including the tropical semiring and the Łukasiewicz semiring. Our main positive results show that strong compactness does indeed hold for all finite semirings and all lattice semirings.

Keywords and phrases:

Semiring semantics, compactness

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Logic

DOI:

10.4230/LIPIcs.CSL.2026.13

Event:

34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Editors:

Stefano Guerrini and Barbara König

Series and Publisher:

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

1 Introduction

We assume familiarity with first-order logic (FO) and recall the classical compactness theorem.

Theorem 1 (Compactness).

For every class of sentences $\Phi\subseteq\operatorname{FO}$ and every sentence $\psi\in\operatorname{FO}$ ,

1.

$\Phi$ is satisfiable if, and only if, every finite subset $\Phi_{0}\subseteq\Phi$ is satisfiable;
2.

$\Phi\models\psi$ if, and only if, there exists a finite subset $\Phi_{0}\subseteq\Phi$ such that $\Phi_{0}\models\psi$ .

The compactness theorem is a direct consequence of Gödel’s completeness theorem, but it can also be established directly, actually by simpler arguments than those needed for the completeness theorem (see e.g. [21]). The compactness theorem is a fundamental tool for studying the expressive power and structural properties of first-order theories. Many model-theoretic methods directly rely on the compactness theorem, and fail in contexts where compactness is not available. In particular this is the case in finite model theory, where compactness obviously fails¹¹1Just take the axiom system for infinity, consisting of the sentences saying that there exist $n$ distinct elements, for all $n\geq 1$ . While this axiom system is not satisfiable by finite models, each of its finite subsets is. and so do many of its classical consequences, such as most preservation theorems.

The objective of this paper is to explore the status of compactness in semiring semantics, which evaluates logical statements not just by true or false, but by values in some commutative semiring. This approach has its origins in the provenance analysis of database queries. Semiring provenance was introduced by Green, Karvounarakis, and Tannen in the seminal paper [16], based on the idea of annotating the atomic facts in a database by values of a commutative semiring, and propagating these values through a database query, keeping track whether information is used alternatively or jointly. Depending on the chosen semiring, provenance valuations give practical information about a query, 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. This approach has been successfully applied to many variants of (positive) database queries, including conjunctive queries, positive relational algebra, datalog, nested relations, XML, SQL-aggregates, graph databases (see, e.g., the surveys [17, 9]).

Such detailed information, as provided by semiring provenance, is not only useful in databases, but may be of great interest in many other areas of logic in computer science. In particular, it has been used for the strategy analysis in various forms of finite and infinite games [14, 11, 18]. There thus is ample motivation to extend the approach of semiring provenance beyond (positive) database queries to a general semiring semantics for logical systems, in particular for full first-order logic, but also for modal and temporal logics, and for logics with least and greatest fixed points. This poses a number of mathematical challenges that have been addressed in recent research.

Negation.

While semiring provenance has for a long time been restricted to negation-free queries, a new approach for dealing with negation was proposed in 2017 by Grädel and Tannen [13], based on transformations into negation normal form, quotient semirings of polynomials with dual indeterminates, and a close relationship to semiring valuations of games. This led to a semiring provenance analysis for full first-order logic (over finite domains) and also permitted a reverse provenance analysis, i.e., finding models that satisfy various properties under given provenance tracking assumptions, with applications to explaining missing query answers or failures of integrity constraints and computing repairs. An updated exposition of this approach (with many examples) can be found in [15].

Infinitary operations.

A priori, semirings only provide addition and multiplication operations over finitely many arguments. For the evaluation of infinite collections of sentences (as needed in this paper), and also for the interpretation of quantifiers over infinite domains, semirings need to be expanded by operations over infinite sets of values, with suitable algebraic properties. In some cases this is completely straightforward and unproblematic, for instance for finite min-max semirings or, more generally, for semirings induced by a complete lattice (with suprema and infima as semiring operations). Further there are important semirings, such as the tropical semiring $\mathbb{T}=(\mathbb{R}_{+}^{\infty},\min,+,\infty,0)$ where the definition of the infinitary operations (here infimum and infinitary sum) is obvious, but it is not clear whether all relevant algebraic properties of the semiring operations also hold for their infinitary versions. A systematic study of the algebraic properties of such infinitary operations and, on this basis, a definition of infinitary semirings has recently been proposed in [6].

Logical properties of semiring semantics.

The development of semiring semantics raises the question to what extent classical logical results also hold in this more general context, and how this depends on algebraic properties of the underlying semiring. Research on such questions has included the study of elementary equivalence and the axiomatisability of finite semiring interpretations [12], of the equivalence of the relational calculus with relational algebra (Codd’s Theorem) [3], 0-1 laws [10], Ehrenfeucht–Fraïssé games [5], the locality theorems by Hanf and Gaifman [4], and the interplay between local consistency and global consistency for relations over semirings [1, 2].

The present paper expands this research by a study of compactness in semiring semantics. The appropriate setting for this is provided by infinitary absorptive semirings (see Definition 4 below). Indeed, compactness is concerned with the evaluation of infinite sets of formulae and the properties they entail, compared to the properties entailed by their finite subsets. It is natural to define the valuation of a set of sentences as the product of the valuations of its elements, so we need semirings where infinite products are well-defined. Further, a reasonable notion of entailment requires that we have a partial order on these valuations, with the property that disjunctions increase the values and conjunctions reduce them. This is the case precisely for absorptive semirings; they are naturally ordered by addition in the sense that $s\leq t:\Leftrightarrow\exists r(s+r=t)$ , and the absorption law implies (and is in fact equivalent to) the property that $s\cdot t\leq s$ for all $s, t$ .

Once this setting, and the semiring semantics of first-order logic, is well-defined, it is easy to see that a weak form of compactness, in terms of satisfiability understood as the existence of non-zero valuations, holds for all infinitary absorptive semirings. Yet, this result marks an essential difference to previous studies of compactness in the context of many-valued logics, where such notions of compactness fail due to different semantics of negation and universal quantification [7]. Beyond that, we study a more powerful variant of compactness in terms of entailment, interpreted via the natural order, which avoids fixing a set of “designated truth values” a priori. We shall prove that strong compactness fails in a number of important semirings, including the tropical semiring, the Łukasiewicz semiring, and the semirings of generalised absorptive polynomials. On the other side, we can prove that strong compactness does generalise to semiring semantics in at least two important cases. For finite semirings, we can encode the semiring interpretations via classical Boolean semantics over an expanded signature, and use this to lift compactness to the semiring setting. This also affects applications usually modeled by semirings for which strong compactness fails as they often have finite analogues that suffice for applications. For instance, instead of doing cost computations in the tropical semiring over the positive reals, we can take a variant with finitely many cost levels and have a cost scenario where compactness applies. A more sophisticated result is the generalisation of strong compactness to (possibly infinite) completely distributive lattice semirings. This requires refinements of the reduction technique based on separating homomorphisms, which were originally introduced in [12]. These take into account the natural order and cope with the lacking continuity of homomorphisms from lattices with dense intervals (such as the fuzzy semiring) into the Boolean semiring. In the appendix we briefly discuss Löwenheim–Skolem theorems (a classical consequence of compactness) in the semiring setting.

2 Semiring Semantics

We summarise the foundations of semiring semantics for first-order logic and refer to [15] for further details.

Definition 2.

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 implicitly 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 w.r.t. the natural order. For the questions that we study here, the natural scenario is provided by semirings that are absorptive, which means that $s+st=s$ for all $s,t\in S$ or, equivalently, that multiplication is decreasing in $\mathcal{S}$ . In particular, addition in absorptive semirings is idempotent (i.e., $s+s=s$ for each $s\in S$ ), so sums coincide with suprema. Unless multiplication is also idempotent in $\mathcal{S}$ , this need not be true for products and infima. We say that $\mathcal{S}$ is (multiplicatively) $n$ -idempotent if $s^{n+1}=s^{n}$ for each $s\in S$ . 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)$ . Specific important examples are the Boolean semiring, the fuzzy semiring $\mathbb{F}=([0,1],\max,\min,0,1)$ , and the access control semiring, also called the security semiring [8].
$\blacksquare$

A more general class (than min-max semirings) 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$

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 that is relevant here, the important examples are the semirings $\mathbb{S}^{\infty}(X)$ of generalised absorptive polynomials. The elements of $\mathbb{S}^{\infty}(X)$ are $\preceq$ -antichains of monomials with exponents from $\mathbb{N}\cup\{\infty\}$ where the absorption order $\preceq$ is defined by $m_{1}\preceq m_{2}:\Leftrightarrow\exists m(m_{1}=m\cdot m_{2})$ . Further absorptive provenance semirings arise as quotients from $\mathbb{S}^{\infty}(X)$ . For instance, the lattice semirings $\textrm{PosBool}(X)$ are the quotients induced by $x\cdot x\sim x$ or, more generally, the quotient semirings $\mathbb{S}^{n}(X)$ are obtained via the congruence generated by $x^{n+1}\sim x^{n}$ . See [19] for more details.

To evaluate first-order formulae in these 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 3.

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

We will only consider model-defining interpretations here. To define semiring semantics also for infinite universes $A$ , and to extend it to valuations of infinite collections $\Phi$ of first-order sentences, our 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 [6]. Here, only the absorptive case is relevant.

Definition 4.

An infinitary absorptive semiring is the expansion of an absorptive semiring $\mathcal{S}$ which satisfies the additional properties that

$\blacksquare$

the natural order $(\mathcal{S},\leq)$ is a complete lattice and
$\blacksquare$

$\mathcal{S}$ is (fully) continuous: for every non-empty chain $C\subseteq S$ , the supremum $\bigsqcup C$ and the infimum $\bigsqcap C$ are compatible with addition and multiplication, i.e.

$s\circ\bigsqcup C=\bigsqcup(s\circ C)\quad\text{ and }\quad s\circ\bigsqcap C=% \bigsqcap(s\circ C),$

for every $s\in S$ and $\circ\in\{+,\cdot\}$ , where $(s\circ C)\coloneqq\{s\circ c\mid c\in C\}$ .

As a consequence, we can define natural infinitary addition and multiplication operations in $\mathcal{S}$ by taking suprema of finite subsums and infima of finite subproducts:

\sum_{i\in I}s_{i}\coloneqq\bigsqcup_{\begin{subarray}{c}I_{0}\subseteq I\\ I_{0}\text{ finite}\end{subarray}}\Bigl(\,\sum_{i\in I_{0}}s_{i}\Bigr)\quad% \text{ and }\quad\prod_{i\in I}s_{i}\coloneqq\bigsqcap_{\begin{subarray}{c}I_{% 0}\subseteq I\\ I_{0}\text{ finite}\end{subarray}}\Bigl(\,\prod_{i\in I_{0}}s_{i}\Bigr).

Definition 5.

Let $\mathcal{S}$ and $\mathcal{T}$ be infinitary absorptive semirings. An infinitary homomorphism (or $\infty$ -homomorphism) is a semiring homomorphism $h\colon\mathcal{S}\to\mathcal{T}$ such that for all sequences $(s_{i})_{i\in I}$ in $\mathcal{S}$ , it holds that $h(\sum_{i\in I}s_{i})=\sum_{i\in I}h(s_{i})$ and $h(\prod_{i\in I}s_{i})=\prod_{i\in I}h(s_{i})$ . We denote by $\operatorname{Hom}(\mathcal{S},\mathcal{T})$ the set of semiring homomorphisms $h\colon\mathcal{S}\to\mathcal{T}$ and by $\text{Hom}^{\infty}(\mathcal{S},\mathcal{T})$ the set of infinitary homomorphisms from $\mathcal{S}$ to $\mathcal{T}$ .

All examples of practically relevant semirings we mentioned before are infinitary absorptive semirings, and the natural infinitary sums and products they admit correspond to this definition. Moreover, these operations have similar properties as the finitary ones: infinitary addition is the same as the supremum, i.e. $\sum_{i\in I}s_{i}=\bigsqcup_{i\in I}s_{i}$ , while infinitary multiplication is decreasing but need not coincide with infima.²²2Indeed, we note that there are infinitary absorptive semirings in which the natural order is a completely distributive lattice (i.e. infima and suprema satisfy a strong distributive law [6, definition 13] over infinite index sets), but strong distributivity does not hold for the infinitary semiring operations defined above. Two such examples are the Viterbi semiring $\mathbb{V}$ and the tropical semiring $\mathbb{T}$ , in which the natural order is linear and completely distributive, but the strong distributive law fails for uncountable index sets, as shown in [6].

Using the (infinitary) semiring operations, semiring semantics lifts each $\mathcal{S}$ -interpretation 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 the universe $A$ . Our treatment of negation is based on negation normal form (nnf). This has emerged as a standard approach in semiring semantics, and is explained in detail in [15].

Definition 6 (Semiring Semantics).

For every $\varphi\in\operatorname{FO}_{A}(\tau)$ , the semiring valuation $\pi\llbracket\varphi\rrbracket$ is inductively defined as follows. Equalities are interpreted by their 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). Further, we set $\pi\llbracket\varphi\rrbracket\coloneqq\pi(\varphi)$ for literals $L\in\operatorname{Lit}_{A}(\tau)$ , $\pi\llbracket\lnot\psi\rrbracket\coloneqq\pi\llbracket\operatorname{nnf}(\lnot% \psi)\rrbracket$ , and

	$\displaystyle\pi\llbracket\psi\vee\vartheta\rrbracket$	$\displaystyle\coloneqq\pi\llbracket\psi\rrbracket+\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=\;\bigsqcup_% {\mathclap{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\forall x\psi(x)\rrbracket$	$\displaystyle\coloneqq\prod_{a\in A}\pi\llbracket\psi(a)\rrbracket=\;\bigsqcap% _{\mathclap{\begin{subarray}{c}A_{0}\subseteq^{\text{fin}}A\end{subarray}}}% \quad\Bigl(\prod_{a\in A_{0}}\pi\llbracket\psi(a)\rrbracket\Bigr).$

Note that we can omit the finite subsums in the definition of the existential quantifier due to the fact that addition and suprema coincide. 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=\bigsqcap_{\Phi_{0}\subseteq^{\text{fin}}\Phi}\Bigl(\prod_{\varphi% \in\Phi_{0}}\pi\llbracket\varphi\rrbracket\Bigr)$ .

Lemma 7 (Fundamental Property).

Let $\pi\colon\operatorname{Lit}_{A}(\tau)\to\mathcal{S}$ be an $\mathcal{S}$ -interpretation and $h\colon\mathcal{S}\to\mathcal{T}$ be an infinitary homomorphism. Then $(h\circ\pi)$ is a $\mathcal{T}$ -interpretation and it holds that $h(\pi\llbracket\varphi\rrbracket)=(h\circ\pi)\llbracket\varphi\rrbracket$ for all $\varphi\in\operatorname{FO}_{A}(\tau)$ .

Definition 8.

Let $\Phi\subseteq\operatorname{FO}$ be a set of first-order sentences, $\psi\in\operatorname{FO}$ , and let $\mathcal{S}$ be an infinitary absorptive semiring. We write

(1)

$\Phi\equiv_{\mathcal{S}}0$ if $\pi\llbracket\Phi\rrbracket=0$ for every model-defining $\mathcal{S}$ -interpretation $\pi$ ;
(2)

$\Phi\models_{\mathcal{S}}\psi$ if $\pi\llbracket\Phi\rrbracket\leq\pi\llbracket\psi\rrbracket$ for every model-defining $\mathcal{S}$ -interpretation $\pi$ .

We shall see that entailments that hold in the Boolean sense need not be preserved when moving to more complex semirings. Conversely, all entailments that hold in an infinitary absorptive semiring $\mathcal{S}$ are preserved in subsemirings $\mathcal{S}^{\prime}\subseteq\mathcal{S}$ (i.e. in the restriction of $\mathcal{S}$ to any subset $S^{\prime}\subseteq S$ that contains 0 and 1 and which is closed under finite and infinitary addition and multiplication). This is immediate from the fact that every $\mathcal{S}^{\prime}$ -interpretation $\pi$ can also be considered as an $\mathcal{S}$ -interpretation, which gives to every sentence, and every set of sentences, the same value in $\mathcal{S}$ and $\mathcal{S}^{\prime}$ .

Lemma 9.

If $\Phi\models_{\mathcal{S}}\psi$ then also $\Phi\models_{\mathcal{S}^{\prime}}\psi$ for every subsemiring $\mathcal{S}^{\prime}\subseteq\mathcal{S}$ .

We are now ready to define two notions of compactness in semiring semantics.

Definition 10.

Let $\mathcal{S}$ be an infinitary absorptive semiring.

(1)

$\mathcal{S}$ has weak compactness if for every set $\Phi\subseteq\operatorname{FO}$ such that $\Phi\equiv_{\mathcal{S}}0$ there exists a finite subset $\Phi_{0}\subseteq\Phi$ such that $\Phi_{0}\equiv_{\mathcal{S}}0$ .
(2)

$\mathcal{S}$ has strong compactness if for every set $\Phi\subseteq\operatorname{FO}$ and every $\psi\in\operatorname{FO}$ such that $\Phi\models_{\mathcal{S}}\psi$ there exists a finite subset $\Phi_{0}\subseteq\Phi$ such that $\Phi_{0}\models_{\mathcal{S}}\psi$ .

3 Separating Weak from Strong Compactness

Clearly, strong compactness implies weak compactness (we can choose an unsatisfiable formula for $\psi$ ). We shall see that the converse is in general not true. Notice that in the classical compactness theorem for Boolean semantics, the two statements imply each other due to the fact that $\Phi\models\psi$ if, and only if, $\Phi\cup\{\neg\psi\}$ is unsatisfiable. In semiring semantics we only have that $\Phi\models_{\mathcal{S}}\psi$ implies that $\Phi\cup\{\neg\psi\}\equiv_{\mathcal{S}}0$ . The converse implication fails in general (see Example 12).

Lemma 11.

$\Phi\models_{\mathcal{S}}\psi$ implies $\Phi\cup\{\neg\psi\}\equiv_{\mathcal{S}}0$ .

Proof.

Let $\pi$ be model-defining. If $\pi\llbracket\Phi\rrbracket\leq\pi\llbracket\psi\rrbracket$ then

\pi\llbracket\Phi\cup\{\neg\psi\}\rrbracket=\pi\llbracket\Phi\rrbracket\cdot% \pi\llbracket\neg\psi\rrbracket\overset{(1)}{\leq}\pi\llbracket\psi\rrbracket% \cdot\pi\llbracket\neg\psi\rrbracket\overset{(2)}{=}0,

where $(1)$ is due to monotonicity and $(2)$ follows inductively from the fact that $\pi(L)\cdot\pi(\lnot L)=0$ for all literals $L\in\operatorname{Lit}_{A}(\tau)$ as $\pi$ is model-defining. $\hfill\blacktriangleleft$

Example 12.

The converse does not hold in general. For instance, consider $\varphi=\exists x(x=x)$ and $\psi=\exists x(Px\lor\neg Px)$ . Since $\pi\llbracket\neg\psi\rrbracket=\pi\llbracket\forall x(Px\land\neg Px)% \rrbracket=0$ for all model-defining semiring interpretations $\pi$ , we have $\varphi\cup\{\neg\psi\}\equiv_{\mathcal{S}}0$ .

Any infinitary absorptive semiring $\mathcal{S}$ with $|\mathcal{S}|\geq 3$ has an element $0<\varepsilon<1$ . The $\mathcal{S}$ -interpretation $\pi^{\prime}(Pa)=\varepsilon$ , $\pi^{\prime}(\neg Pa)=0$ (for all $a\in A$ , with arbitrary universe $A$ ) is a counterexample for $\varphi\models_{\mathcal{S}}\psi$ , since $\pi^{\prime}\llbracket\varphi\rrbracket=1$ but $\pi^{\prime}\llbracket\psi\rrbracket=\varepsilon$ . $\lrcorner$

By the classical compactness theorem, the Boolean semiring $\mathbb{B}$ has strong compactness. The question we want to answer is which other semirings have strong (or just weak) compactness.

With every $\mathcal{S}$ -interpretation $\pi\colon\operatorname{Lit}_{A}(\tau)\to\mathcal{S}$ we associate its flattening $\pi^{\mathbb{B}}$ such that for every literal $L\in\operatorname{Lit}_{A}(\tau)$ we have that $\pi^{\mathbb{B}}(L)=0$ if $\pi(L)=0$ and $\pi^{\mathbb{B}}(L)=1$ otherwise. Notice that $\pi^{\mathbb{B}}$ can be viewed as a $\mathbb{B}$ -interpretation (i.e. a classical $\tau$ -structure) but also as an $\mathcal{S}$ -interpretation that only takes the values 0 and 1. Further, by the monotonicity of (infinitary) addition and multiplication and the fact that $1$ is maximal in absorptive semirings, it follows that $\pi\llbracket\psi\rrbracket\leq\pi^{\mathbb{B}}\llbracket\psi\rrbracket$ for all $\psi\in\operatorname{FO}$ .

Proposition 13.

Every infinitary absorptive semiring has weak compactness.

Proof.

Let $\Phi\equiv_{\mathcal{S}}0$ . Then $\Phi\equiv_{\mathbb{B}}0$ . To see this, consider any model-defining $\mathbb{B}$ -interpretation $\pi$ . We can view $\pi$ as an $\mathcal{S}$ -interpretation, which we denote as $\pi^{\mathcal{S}}$ (so that $(\pi^{\mathcal{S}})^{\mathbb{B}}=\pi$ ). Since addition in $\mathcal{S}$ is idempotent (we need $1+1=1$ ), $\mathbb{B}$ is a subsemiring of $\mathcal{S}$ , and we have $\pi^{\mathcal{S}}\llbracket\varphi\rrbracket=\pi\llbracket\varphi\rrbracket$ for all $\varphi\in\operatorname{FO}$ . Hence $\pi^{\mathcal{S}}\llbracket\Phi\rrbracket=0$ implies $\pi\llbracket\Phi\rrbracket=0$ . By the classical compactness theorem, there exists a finite subset $\Phi_{0}\subseteq\Phi$ such that $\Phi_{0}\equiv_{\mathbb{B}}0$ . But, then we have, for every $\mathcal{S}$ -interpretation $\pi$ that

\pi\llbracket\Phi_{0}\rrbracket=\prod_{\varphi\in\Phi_{0}}\pi\llbracket\varphi% \rrbracket\leq\prod_{\varphi\in\Phi_{0}}\pi^{\mathbb{B}}\llbracket\varphi% \rrbracket=\pi^{\mathbb{B}}\llbracket\Phi_{0}\rrbracket=0.\

$\hfill\blacktriangleleft$

However, for strong compactness, the situation is different.

Proposition 14.

Let $\mathcal{S}$ be any infinitary absorptive semiring such that for every $n\in\mathbb{N}$ there is some element $s_{n}\in\mathcal{S}$ such that $(s_{n})^{\infty}\coloneqq\bigsqcap\{(s_{n})^{m}\mid m<\omega\}<(s_{n})^{n}$ (i.e., that is not multiplicatively $n$ -idempotent for any $n$ ). Then $\mathcal{S}$ does not have strong compactness.

Proof.

Let $P$ be a unary predicate and let $\psi\coloneqq\forall x\exists yPy$ . Further let $\Phi\coloneqq\{\varphi_{n}\mid n\geq 1\}$ where $\varphi_{n}$ is the $n$ -fold conjunction of the same formula $\exists yPy$ .

We first claim that $\Phi\models_{\mathcal{S}}\psi$ . Let $\pi$ be an arbitrary $\mathcal{S}$ -interpretation over a universe $A$ with $r\coloneqq\pi\llbracket\exists yPy\rrbracket$ . It follows that $\pi\llbracket\Phi\rrbracket=\prod\{r^{n}\mid n>0\}=r^{\infty}$ while $\pi\llbracket\psi\rrbracket=r^{n}$ if $A$ is finite with $n$ elements and $\pi\llbracket\psi\rrbracket=r^{\infty}$ if $A$ is infinite. In both cases $\pi\llbracket\Phi\rrbracket\leq\pi\llbracket\psi\rrbracket$ .

For every finite subset $\Phi_{0}\subseteq\Phi$ and every $\mathcal{S}$ -interpretation $\pi$ over an infinite universe, we have that $\pi\llbracket\psi\rrbracket=r^{\infty}$ , where $r=\pi\llbracket\exists yPy\rrbracket$ , but $\pi\llbracket\Phi_{0}\rrbracket=r^{n}$ for some $n$ (that depends on $\Phi_{0}$ ). If we choose $\pi_{n}$ in such a way that $\pi_{n}\llbracket\exists yPy\rrbracket=s_{n}$ we have $\pi_{n}\llbracket\Phi_{0}\rrbracket=(s_{n})^{n}>(s_{n})^{\infty}=\pi_{n}% \llbracket\psi\rrbracket$ so $\Phi_{0}\not\models_{\mathcal{S}}\psi$ . Thus, strong compactness is violated. $\hfill\blacktriangleleft$

Corollary 15.

The tropical semiring $\mathbb{T}$ , the Viterbi semiring $\mathbb{V}$ , the semirings of generalised absorptive polynomials $\mathbb{S}^{\infty}(X)$ , the Łukasiewicz semiring $\mathbb{L}$ and the semiring of doubt $\mathbb{D}$ are not multiplicatively $n$ -idempotent for any $n$ and therefore do not have strong compactness.

4 Finite Semirings

Let $\mathcal{S}$ be a finite absorptive semiring with infinitary operations in the sense of Definition 4. Finiteness of $\mathcal{S}$ trivially implies that there is some $n\in\mathbb{N}_{>0}$ such that multiplication in $\mathcal{S}$ is $n$ -idempotent, that is, we have $s^{n}=s^{n+1}=\ldots=s^{\infty}$ .

With every $\mathcal{S}$ -interpretation $\pi\colon\operatorname{Lit}_{A}(\tau)\to\mathcal{S}$ we associate a classical structure $\mathfrak{C}(\pi)$ over the same universe $A$ and with vocabulary $\tau_{\mathcal{S}}\coloneqq\{R_{s}\mid R\in\tau,s\in\mathcal{S}\}\cup\{R^{\neg% }_{s}\mid R\in\tau,s\in\mathcal{S}\}$ such that $\bar{a}\in R_{s}$ if $\pi(R\bar{a})=s$ and $\bar{a}\in R^{\neg}_{s}$ if $\pi(\neg R\bar{a})=s$ . We can axiomatise structures of this form by the set of formulae

	$\displaystyle\Theta_{\tau}$	$\displaystyle\coloneqq\{\alpha_{L}\mid L=R\text{ or }L=R^{\neg}\text{ for }R% \in\tau\}\cup\{\beta_{R}\mid R\in\tau\}\quad\text{with}$
	$\displaystyle\alpha_{L}$	$\displaystyle\coloneqq\forall\bar{x}\Bigl(\bigvee_{s\in\mathcal{S}}L_{s}\bar{x% }\land\bigwedge_{s\neq t}\neg(L_{s}\bar{x}\land L_{t}\bar{x})\Bigr)\quad\text{% and }\quad\beta_{R}\coloneqq\forall\bar{x}(R_{0}\bar{x}\oplus R^{\neg}_{0}% \bar{x}).$

Lemma 16.

For every $\tau_{\mathcal{S}}$ -structure ${\mathfrak{B}}$ we have that ${\mathfrak{B}}\models\Theta_{\tau}$ if, and only if, ${\mathfrak{B}}=\mathfrak{C}(\pi)$ for some model-defining $\mathcal{S}$ -interpretation $\pi$ .

Proposition 17.

For every formula $\psi(\bar{x})\in\operatorname{FO}(\tau)$ there exists a family of formulae $(\psi_{=s}(\bar{x}))_{s\in S}$ in $\operatorname{FO}(\tau_{\mathcal{S}})$ such that for every $\mathcal{S}$ -interpretation $\pi\colon\operatorname{Lit}_{A}(\tau)\to\mathcal{S}$ , every tuple $\bar{a}$ , and every value $s\in S$ we have that $\pi\llbracket\psi(\bar{a})\rrbracket=s$ , if, and only if, $\mathfrak{C}(\pi)\models\psi_{=s}(\bar{a})$ .

Proof.

Literals $R\bar{x}$ and $\neg R\bar{x}$ are translated to $R_{s}\bar{x}$ and $R^{\neg}_{s}\bar{x}$ , respectively. For $\star\in\{\lor,\land\}$ , choose $\circ\in\{+,\cdot\}$ , respectively, and translate $\psi=\varphi\star\vartheta$ to $\psi_{=s}\coloneqq\bigvee_{r\circ t=s}\varphi_{=r}\land\vartheta_{=t}$ , going through all combinations $r, t$ of semiring values that yield $s$ .

For $\psi=\forall y\,\varphi$ , the construction relies on the fact that multiplication in $\mathcal{S}$ is $n$ -idempotent for some $n$ . For every $s\in\mathcal{S}$ , let $F_{s}$ be the set of those functions $f\colon\mathcal{S}\to\{0,\dots,n\}$ such that $\prod_{t\in\mathcal{S}}t^{f(t)}=s$ , that is, each $f\in F_{s}$ represents a factorisation of $s$ . For any $\mathcal{S}$ -interpretation $\pi\colon\operatorname{Lit}_{A}(\tau)\to\mathcal{S}$ , we have that

\pi\llbracket\forall y\varphi\rrbracket=\prod_{a\in A}\pi\llbracket\varphi(a)% \rrbracket=\prod_{t\in\mathcal{S}}t^{|\{a\mid\pi\llbracket\varphi(a)\rrbracket% =t\}|},

with the convention that $0^{0}=1$ . Thus the formula

\displaystyle\psi_{=s}

\displaystyle\coloneqq\bigvee_{f\in F_{s}}\bigwedge_{t\in\mathcal{S}}\vartheta% _{f,t}\qquad\text{ with }\qquad\vartheta_{f,t}=\begin{cases}\exists^{=f(t)}y\,% \varphi_{=t}(y)&\text{ if }f(t)<n\text{ and}\\ \exists^{\geq f(t)}y\,\varphi_{=t}(y)&\text{ if }f(t)=n\end{cases}

expresses that for one of the functions $f\in F_{s}$ there are indeed precisely $f(t)$ values $a$ such that $\varphi(a)$ evaluates to $t$ in case that $f(t)$ is smaller than $n$ , and at least $n$ such values if $f(t)=n$ (so that $t^{|\{a\mid\pi\llbracket\varphi(a)\rrbracket=t\}|}=t^{n}=t^{f(t)}$ ). This implies that $\mathfrak{C}(\pi)\models\psi_{=s}$ if, and only if, $\pi\llbracket\psi\rrbracket=s$ . For $\psi=\exists y\,\varphi$ , we can use an analogous construction with $n\coloneqq 1$ , since addition in $\mathcal{S}$ is idempotent. $\hfill\blacktriangleleft$

Theorem 18.

Every finite absorptive semiring $\mathcal{S}$ has strong compactness.

Proof.

Suppose that $\Phi\models_{\mathcal{S}}\psi$ . We observe that for every $\mathcal{S}$ -interpretation $\pi$ , there is a finite subset $\Phi(\pi)\subseteq\Phi$ , such that $\pi\llbracket\Phi(\pi)\rrbracket\leq\pi\llbracket\Psi\rrbracket$ for any finite $\Psi\subseteq\Phi$ . Suppose for a contradiction that this is not the case. Since $\mathcal{S}$ is finite, there are only finitely many values $\pi\llbracket\Psi\rrbracket$ for finite subsets $\Psi\subseteq\Phi$ . If there is no minimum value, then there must be finitely many incomparable minimal values $\pi\llbracket\Phi_{1}\rrbracket,\dots,\pi\llbracket\Phi_{m}\rrbracket$ with $m>1$ . Let $\Phi(\pi)\coloneqq\bigcup_{1\leq i\leq m}\Phi_{i}$ . Then $\pi\llbracket\Phi(\pi)\rrbracket\leq\pi\llbracket\Phi_{i}\rrbracket$ for all $1\leq i\leq m$ , in particular, $\pi\llbracket\Phi(\pi)\rrbracket$ is the minimum value with respect to $\leq$ , a contradiction.

Moreover, $\pi\llbracket\Phi(\pi)\rrbracket=\pi\llbracket\Phi\rrbracket$ , since we can write $\pi\llbracket\Phi\rrbracket=\prod_{s\in\mathcal{S}}s^{|\{\varphi\in\Phi\mid\pi% \llbracket\varphi\rrbracket=s\}|}$ , but since the multiplicative order of each $s$ is finite, a finite subset of $\{\varphi\in\Phi\mid\pi\llbracket\varphi\rrbracket=s\}$ suffices. Thus $\pi\llbracket\Phi\rrbracket=\pi\llbracket\Psi\rrbracket$ for some finite subset $\Psi\subseteq\Phi$ , which implies $\pi\llbracket\Phi(\pi)\rrbracket\leq\pi\llbracket\Phi\rrbracket$ .

For every finite subset $\Phi_{0}\subseteq\Phi$ , let $\eta(\Phi_{0})\coloneqq\bigvee_{s\leq t}(\bigwedge\Phi_{0})_{=s}\land\psi_{=t}% \in\operatorname{FO}(\tau_{\mathcal{S}})$ . Clearly, we have $\mathfrak{C}(\pi)\models\eta(\Phi_{0})$ if, and only if, $\pi\llbracket\Phi_{0}\rrbracket\leq\pi\llbracket\psi\rrbracket$ .

Claim.

$\Psi\coloneqq\Theta_{\tau}\cup\{\neg\eta(\Phi_{0})\mid\Phi_{0}\text{ is a % finite subset of }\Phi\}$ is unsatisfiable.

Indeed, suppose that ${\mathfrak{B}}\models\Psi$ . Since ${\mathfrak{B}}\models\Theta_{\tau}$ we have that ${\mathfrak{B}}=\mathfrak{C}(\pi)$ for some model-defining $\mathcal{S}$ -interpretation $\pi$ . Moreover, $\pi\llbracket\Phi_{0}\rrbracket\not\leq\pi\llbracket\psi\rrbracket$ for every finite subset $\Phi_{0}\subseteq\Phi$ , in particular for $\Phi_{0}=\Phi(\pi)$ . But since $\pi\llbracket\Phi(\pi)\rrbracket=\pi\llbracket\Phi\rrbracket$ this would imply that $\Phi\not\models_{\mathcal{S}}\psi$ , a contradiction.

It follows, by compactness, that there exists a finite unsatisfiable subset $\Psi_{0}\subseteq\Psi$ . Let

\Phi^{*}\coloneqq\bigcup\{\Phi_{0}\mid\neg\eta(\Phi_{0})\in\Psi_{0}\}.

Clearly, $\Phi^{*}$ is a finite subset of $\Phi$ . It remains to prove that $\Phi^{*}\models_{\mathcal{S}}\psi$ . If not, then there exists an $\mathcal{S}$ -interpretation $\pi$ with $\pi\llbracket\Phi^{*}\rrbracket\not\leq\pi\llbracket\psi\rrbracket$ . The associated $\tau_{\mathcal{S}}$ -structure $\mathfrak{C}(\pi)$ would clearly satisfy $\Theta_{\tau}$ as well as all formulae $\neg\eta(\Phi_{0})\in\Psi_{0}$ since otherwise $\pi\llbracket\Phi_{0}\rrbracket\leq\pi\llbracket\psi\rrbracket$ . Thus, we would have that $\mathfrak{C}(\pi)\models\Psi_{0}$ , contradicting the unsatisfiability of $\Psi_{0}$ . $\hfill\blacktriangleleft$

5 Lattice Semirings

Based on a reduction to the $3$ -element min-max semiring $\mathcal{S}_{3}=(\{0<\varepsilon<1\},\max,\min,0,1)$ , we show that every completely distributive lattice semiring $\mathcal{L}=(L,\sqcup,\sqcap,0,1)$ has strong compactness. To this end, we make use of the lattice semiring $\mathcal{L}^{*}=(L\cup\{0^{*}\},\sqcup,\sqcap,0^{*},1)$ which adds a new zero $0^{*}$ to $\mathcal{L}$ and prove for all $\Phi\subseteq\operatorname{FO}$ and $\varphi,\psi\in\operatorname{FO}$ that

(1)

$\Phi\models_{\mathcal{L}}\psi$ implies $\Phi\models_{\mathcal{S}_{3}}\psi$ ,
(2)

$\{\varphi\}\models_{\mathcal{S}_{3}}\psi$ implies $\{\varphi\}\models_{\mathcal{L}^{*}}\psi$ , and
(3)

$\{\varphi\}\models_{\mathcal{L}^{*}}\psi$ implies $\{\varphi\}\models_{\mathcal{L}}\psi$ .

Starting from $\Phi\models_{\mathcal{L}}\psi$ we can then infer $\Phi\models_{\mathcal{S}_{3}}\psi$ and apply strong compactness of $\mathcal{S}_{3}$ due to its finiteness, which yields some finite $\Phi_{0}\subseteq\Phi$ with $\{\bigwedge\Phi_{0}\}\equiv\Phi_{0}\models_{\mathcal{S}_{3}}\psi$ and, in turn, implies $\Phi_{0}\models_{\mathcal{L}^{*}}\psi$ and thus $\Phi_{0}\models_{\mathcal{L}}\psi$ . The first implication follows immediately from the fact that $\mathcal{S}_{3}$ can be considered a sublattice of $\mathcal{L}$ (see Lemma 9). To prove the third implication, we note that we obtain an $\infty$ -homomorphism $h\colon\mathcal{L}^{*}\to\mathcal{L}$ by mapping every element to itself except for $0^{*}$ , which is mapped to $0$ .

Lemma 19.

If $\{\varphi\}\models_{\mathcal{L}^{*}}\psi$ , then also $\{\varphi\}\models_{\mathcal{L}}\psi$ .

Proof.

With each model-defining $\mathcal{L}$ -interpretation $\pi$ , we associate an $\mathcal{L}^{*}$ -interpretation $\pi^{*}$ with $\pi^{*}(L)=0^{*}$ if $\pi(L)=0$ and $\pi^{*}(L)=\pi(L)$ otherwise. Clearly, $\pi^{*}$ is also model-defining, and, by hypothesis, we have that $\pi^{*}\llbracket\varphi\rrbracket\leq\pi^{*}\llbracket\psi\rrbracket$ . Since $h$ preserves the order on $\mathcal{L}^{*}$ , this implies $\pi\llbracket\varphi\rrbracket=(h\circ\pi^{*})\llbracket\varphi\rrbracket=h(% \pi^{*}\llbracket\varphi\rrbracket)\leq h(\pi^{*}\llbracket\psi\rrbracket)=(h% \circ\pi^{*})\llbracket\psi\rrbracket=\pi\llbracket\psi\rrbracket$ . $\hfill\blacktriangleleft$

Thus, it remains to prove the second implication, which, for lattices without dense intervals, can be proved using separating $\infty$ -homomorphisms and the fundamental property.

5.1 Reduction via Separating Homomorphisms

Separating sets of homomorphisms contain for each $s\neq t$ some $h$ with $h(s)\neq h(t)$ and were introduced in [12] for the purpose of reducing elementary equivalence from one semiring to another. The main idea behind this condition is to transfer counterexamples against elementary equivalence to the target semiring by applying one of the homomorphisms. By additionally demanding that the homomorphism for $s$ and $t$ should not introduce new inequalities between $s$ and $t$ , we can extend this reduction technique to the entailment relation.

Definition 20.

A set $H\subseteq\operatorname{Hom}^{\infty}(\mathcal{S},\mathcal{T})$ is $\leq$ -separating if for every $s\not\leq t\in\mathcal{S}$ , there is some infinitary homomorphism $h\in H$ such that $h(s)\not\leq h(t)$ and $h^{-1}(0)=\{0\}$ .

Proposition 21.

If there is a $\leq$ -separating set $H\subseteq\operatorname{Hom}^{\infty}(\mathcal{S},\mathcal{T})$ and $\Phi\models_{\mathcal{T}}\psi$ , then we also have that $\Phi\models_{\mathcal{S}}\psi$ .

Proof.

We prove the contraposition. Let $\pi$ be a model-defining $\mathcal{S}$ -interpretation such that $s\coloneqq\pi\llbracket\Phi\rrbracket\not\leq\pi\llbracket\psi\rrbracket\eqqcolon t$ and $h\in H$ be a homomorphism which $\leq$ -separates $s$ from $t$ . Since $h^{-1}(0)=\{0\}$ , $(h\circ\pi)$ is also model-defining. By the fundamental property, we conclude $(h\circ\pi)\llbracket\Phi\rrbracket=h(\pi\llbracket\Phi\rrbracket)\not\leq h(% \pi\llbracket\psi\rrbracket)=(h\circ\pi)\llbracket\psi\rrbracket$ . Hence, $\Phi\not\models_{\mathcal{T}}\psi$ . $\hfill\blacktriangleleft$

Note that the additional condition $h^{-1}(0)=\{0\}$ is the reason why we reduce entailment in $\mathcal{L}$ to $\mathcal{S}_{3}$ by taking a detour via $\mathcal{L}^{*}$ . Homomorphisms into $\mathcal{S}_{3}$ with $h^{-1}(0)=\{0\}$ can only exist if $0$ does not have non-trivial divisors $s,t\neq 0$ , which is not necessarily true for $\mathcal{L}$ , but always true in $\mathcal{L}^{*}$ . Indeed, $s\sqcap t=0$ implies $h(s)\sqcap h(t)=h(s\sqcap t)=h(0)=0$ , i.e. $h(s)=0$ or $h(t)=0$ .

It can be shown that $\leq$ -separating sets of finitary homomorphisms $H\subseteq\operatorname{Hom}(\mathcal{L}^{*},\mathcal{S}_{3})$ exist for every lattice semiring $\mathcal{L}$ [5], but in order to apply the fundamental property, we additionally need that the homomorphisms in $H$ respect the infinitary operations. The existence of some $\leq$ -separating $H\subseteq\operatorname{Hom}^{\infty}(\mathcal{L}^{*},\mathcal{S}_{3})$ , however, is not ensured, not even if $\mathcal{L}$ is induced by a linear order, which is due to the possible presence of dense intervals. Suppose that $\mathcal{L}$ is linearly ordered and $[s,t]$ with $s<t$ is dense. For each homomorphism which $\leq$ -separates $s$ from $t$ there must be some threshold $u\in[s,t]$ such that either $h^{-1}(\varepsilon)=(0^{*},u)$ or $h^{-1}(\varepsilon)=(0^{*},u]$ . In the first case, we observe that $h(\bigsqcup[s,u))=1\neq\varepsilon=\bigsqcup\{h(v)\mid s\leq v<u\}$ while in the second case $h(\bigsqcap(u,t])=\varepsilon\neq 1=\bigsqcap\{h(v)\mid u<v\leq t\}$ , so $h$ cannot be infinitary. As a consequence, we might have that $h(\pi\llbracket\exists xRx\rrbracket)>(h\circ\pi)\llbracket\exists xRx\rrbracket$ or $h(\pi\llbracket\forall xRx\rrbracket)<(h\circ\pi)\llbracket\forall xRx\rrbracket$ if $\{\pi(Ra)\mid a\in A\}$ converges to $u$ , so the fundamental property fails.

Lemma 22.

There is a $\leq$ -separating set of $\infty$ -homomorphisms from $\mathcal{L}^{*}$ to $\mathcal{S}_{3}$ if, and only if, $\mathcal{L}$ is a completely distributive lattice without dense intervals.

Corollary 23.

Each completely distributive lattice without dense intervals has strong compactness.

5.2 Workaround for Dense Lattices

In order to generalise the reduction technique to lattices that contain dense intervals, we develop a weaker condition which relies on homomorphisms that are not necessarily infinitary. Without compatibility with the infinitary operations we cannot apply the fundamental property as before. However, making use of the fact that we consider homomorphisms into a min-max semiring, we can prove a weaker relationship between $h(\pi\llbracket\varphi\rrbracket)$ and $(h\circ\pi)\llbracket\varphi\rrbracket$ . The main idea here is to exclude the suprema and infima that $h$ might not commute with. In the special case discussed in the previous section where $\mathcal{L}$ is a min-max semiring, the fact that $h$ is not infinitary affects just one threshold value $u$ in $\mathcal{L}$ . Whenever $\pi\llbracket\varphi\rrbracket\neq u$ , we still have $h(\pi\llbracket\varphi\rrbracket)=(h\circ\pi)\llbracket\varphi\rrbracket$ although $h$ is not infinitary.

Proposition 24.

Let $h\colon\mathcal{S}\to\mathcal{T}$ be a homomorphism (which does not necessarily respect the infinitary operations) into a min-max semiring $\mathcal{T}$ , and let $t\in\mathcal{T}$ .

(1)

If $h(\pi\llbracket\varphi(\bar{a})\rrbracket)\geq t$ and if for all $X\subseteq\mathcal{S}$ with $\pi\llbracket\varphi(\bar{a})\rrbracket=\bigsqcup X$ there is some $x\in X$ such that $h(x)\geq t$ , then also $(h\circ\pi)\llbracket\varphi(\bar{a})\rrbracket\geq t$ .
(2)

If $h(\pi\llbracket\varphi(\bar{a})\rrbracket)\leq t$ and if for all $X\subseteq\mathcal{S}$ with $\pi\llbracket\varphi(\bar{a})\rrbracket=\bigsqcap X$ there is some $x\in X$ such that $h(x)\leq t$ , then also $(h\circ\pi)\llbracket\varphi(\bar{a})\rrbracket\leq t$ .

Based on the idea that the homomorphism separating $s$ from $t$ need not be infinitary in general, but the parts where it is not should neither match $s$ nor $t$ , we can formulate a weaker condition which we want to use to infer $\{\varphi\}\models_{\mathcal{L}^{*}}\psi$ from $\{\varphi\}\models_{\mathcal{S}_{3}}\psi$ .

Definition 25.

A set $H\subseteq\operatorname{Hom}(\mathcal{S},\mathcal{T})$ of homomorphisms (that are not necessarily infinitary) is weakly $\leq$ -separating if for each $s\not\leq t$ , there is some $h\in H$ with $h^{-1}(0)=\{0\}$ such that

(1)

$h(s)\not\leq h(t)$ ;
(2)

if $s=\bigsqcup X$ , then $h(s)=h(x)$ for some $x\in X$ ;
(3)

if $t=\bigsqcap X$ , then $h(t)=h(x)$ for some $x\in X$ .

Proposition 26.

If there is a weakly $\leq$ -separating set $H\subseteq\operatorname{Hom}(\mathcal{S},\mathcal{T})$ where $\mathcal{T}$ is a min-max semiring and $\{\varphi\}\models_{\mathcal{T}}\psi$ , then it also holds that $\{\varphi\}\models_{\mathcal{S}}\psi$ .

Proof.

Let $\pi$ be an $\mathcal{S}$ -interpretation violating $\{\varphi\}\models_{\mathcal{S}}\psi$ and $h\in H$ be a homomorphism which weakly $\leq$ -separates $\pi\llbracket\varphi\rrbracket$ from $\pi\llbracket\psi\rrbracket$ . Making use of Proposition 24 we obtain that $(h\circ\pi)\llbracket\varphi\rrbracket\geq h(\pi\llbracket\varphi\rrbracket)>h% (\pi\llbracket\psi\rrbracket)\geq(h\circ\pi)\llbracket\psi\rrbracket$ , i.e. $\{\varphi\}\not\models_{\mathcal{T}}\psi$ . $\hfill\blacktriangleleft$

It remains to prove that there is a weakly $\leq$ -separating set of homomorphisms $h\colon\mathcal{L}^{*}\to\mathcal{S}_{3}$ for every completely distributive lattice $\mathcal{L}$ . For min-max semirings, this is straightforward: If there is some $s>u>t$ , we can weakly $\leq$ -separate $s$ from $t$ via $h$ with $h^{-1}(\varepsilon)=(0^{*},u]$ , and if otherwise $t$ is direct predecessor of $s$ , we choose $h^{-1}(\varepsilon)=(0^{*},t]$ . For general lattices, on the contrary, this procedure does not necessarily yield a homomorphism as it might be the case that $u$ is an infimum of greater elements. Instead, homomorphisms from $\mathcal{L}$ to $\mathbb{B}$ correspond to the prime ideals in $\mathcal{L}$ .

Definition 27.

A prime ideal of $\mathcal{L}$ is a non-empty proper subset $P\subsetneq\mathcal{L}$ which is downward-closed, closed under finite suprema, and satisfies $x\sqcap y\in P\Rightarrow\{x,y\}\cap P\neq\varnothing$ for $x,y\in\mathcal{L}$ .

If $P$ is a prime ideal of $\mathcal{L}$ , it induces the homomorphism $h_{P}\colon\mathcal{L}^{*}\to\mathcal{S}_{3}$ with $h_{P}(0^{*})=0$ , $h_{P}(u)=\varepsilon$ if $u\in P$ and $h_{P}(u)=1$ otherwise. While $h_{P}$ only violates the fundamental property at a single “boundary” element $u$ if $\mathcal{L}$ is a min-max semiring, multiple boundary elements may exist in the general case. Thus, we want to construct a prime ideal $P$ such that neither $s$ nor $t$ lie on the boundary of $P$ . More precisely, $P$ has to satisfy the following conditions, which ensure that the induced homomorphism $h_{P}$ weakly $\leq$ -separates $s$ from $t$ .

(1)

$t\in P$ and $s\not\in P$ ,
(2)

$t\neq\bigsqcap X$ for all $X\subseteq\mathcal{S}\setminus P$ and
(3)

$s\neq\bigsqcup X$ for all $X\subseteq P$ .

5.3 Construction of the Prime Ideals

In order to construct for each $s\not\leq t$ a prime ideal with the required properties, we make use of the lattice-theoretic notions from [20] and analyze the minimum semi-ideals with a particular supremum.

Definition 28.

A semi-ideal of $\mathcal{L}$ is a downward-closed subset $I\subseteq\mathcal{L}$ . For $s\in\mathcal{L}$ let $K(s)\coloneqq\bigcap\{I\mid I\text{ semi-ideal s.t. }\bigsqcup I\geq s\}$ .

Lemma 29 ([20]).

The following holds for all $s,t\in\mathcal{L}$ and $X\subseteq\mathcal{L}$ :

(1)

If $s\leq t$ , then $K(s)\subseteq K(t)$ ;
(2)

$K(\bigsqcup X)=\bigcup\{K(x)\mid x\in X\}$ ;
(3)

$\bigsqcup K(s)=s$ ;
(4)

$s\in K(t)$ if, and only if, there is some $u\in\mathcal{L}$ such that $s\in K(u)$ and $u\in K(t)$ .

The idea now is to fix an appropriate chain $C$ depending on the elements $s\not\leq t$ we want to separate and track for each $x\in\mathcal{L}$ which elements of $C$ must be contained in every semi-ideal with supremum $x$ . This induces a partial order on $\mathcal{L}$ (that might be different from the lattice order), which we can use to construct a homomorphism $h\colon\mathcal{L}\to\mathbb{B}$ based on a threshold, analogously to the special case where the lattice order was linear.

For $s\not\leq t$ we have that $K(s)\not\subseteq K(t)$ (since otherwise $s=\bigsqcup K(s)\leq\bigsqcup K(t)=t$ ). In order to construct $C$ , fix some $u\in K(s)\setminus K(t)$ and choose $v,w\in\mathcal{L}$ such that $u\in K(v),v\in K(w)$ , and $w\in K(s)$ , which exist by Lemma 29(4). While $u$ and $v$ will make sure that $s\not\in P$ and $t\in P$ , we use $w$ to argue that $s$ cannot be the supremum of elements inside $P$ . To ensure the dual property w.r.t. $t$ and that the induced homomorphism $h_{P}$ commutes with infima, we inductively extend $\{u,v,w\}$ to $C=\{c_{i}\mid i\in\omega\}\cup\{v,w\}$ by setting $c_{0}=u$ and choosing $c_{i+1}$ arbitrarily such that $c_{i}\in K(c_{i+1})$ and $c_{i+1}\in K(v)$ . Note that $a\in K(b)$ implies $a\leq b$ as $\{c\mid c\leq b\}$ is a semi-ideal with supremum $b$ . Thus, $C$ is a chain.

We claim that $P\coloneqq\{x\mid K(x)\cap C\subsetneq K(v)\cap C\}=\{x\mid K(x)\cap C\not% \supseteq K(v)\cap C\}$ has the desired properties w.r.t. $s$ and $t$ . First, we prove that $P$ induces a homomorphism $h_{P}\colon\mathcal{L}\to\mathbb{B}$ (and thus a homomorphism $h_{P}\colon\mathcal{L}^{*}\to\mathcal{S}_{3}$ ) which even commutes with arbitrary infima (while this is in general not true for suprema).

Figure 1: Construction of the prime ideal weakly

\leq

-separating

s

from

t

, where

x\not\in P

in the case on the left and

x\in P

on the right.

Theorem 30.

$P$ is a prime ideal and for each $X\subseteq\mathcal{L}$ with $\bigsqcap X\in P$ , it holds that $X\cap P\neq\varnothing$ .

Proof.

Let $x_{0},x_{1}\in P$ , i.e. $K(x_{i})\cap C\subsetneq K(v)\cap C$ for $i\in\{0,1\}$ . By downward-closedness, there must be an $i\in\{0,1\}$ such that $K(x_{i})\cap C\subseteq K(x_{1-i})\cap C$ . With Lemma 29(2) this yields $K(x_{0}\sqcup x_{1})\cap C=(K(x_{0})\cup K(x_{1}))\cap C=(K(x_{0})\cap C)\cup(% K(x_{1})\cap C)=K(x_{1-i})\cap C\subsetneq K(v)\cap C$ and thus $x_{0}\sqcup x_{1}\in P$ . Now let $x\leq y\in P$ . Since $K(x)\cap C\subseteq K(y)\cap C\subsetneq K(v)\cap C$ , we also have that $x\in P$ .

It remains to prove that $\bigsqcap X\in P$ implies $X\cap P\neq\varnothing$ . We prove the contraposition, so let $X\subseteq\mathcal{L}$ such that $K(v)\cap C\subseteq K(x)\cap C$ for each $x\in X$ . We claim that $K(v)\cap C\subseteq K(\bigsqcap X)\cap C$ . Let $y\in K(v)\cap C$ . By definition of $C$ , there must be some $z$ such that $y\in K(z)$ and $z\in K(v)\cap C\subseteq\bigcap\{K(x)\cap C\mid x\in X\}$ (if $y\in\{v,w\}$ , we can choose $z\coloneqq v$ , and for $y=c_{i}$ , we pick $z\coloneqq c_{i+1}$ ). Hence, $z\leq x$ for each $x\in X$ , implying $z\leq\bigsqcap X$ . With $y\in K(z)$ this yields $y\in K(\bigsqcap X)$ as required. $\hfill\blacktriangleleft$

By choice of $C$ , we can finally argue that the induced homomorphism $h_{P}\colon\mathcal{L}^{*}\to\mathcal{S}_{3}$ weakly $\leq$ -separates $s$ from $t$ .

Theorem 31.

We have that $t\in P$ and $s\not\in P$ while $t\neq\bigsqcap X$ for all $X\subseteq\mathcal{L}\setminus P$ and $s\neq\bigsqcup X$ for all $X\subseteq P$ .

Proof.

By definition, $u\in K(v)\cap C$ while $u\not\in K(t)$ . Hence, $K(t)\cap C\not\supseteq K(v)\cap C$ , i.e. $t\in P$ . Further, $s\not\in P$ as $v\in K(s)$ and thus $v\leq s$ , which implies $K(s)\cap C\supseteq K(v)\cap C$ . For $X\subseteq\mathcal{L}\setminus P$ we have that $\bigsqcap X\not\in P$ by Theorem 30, hence $\bigsqcap X\neq t\in P$ . Finally, let $X\subseteq P$ . Then $K(\bigsqcup X)\cap C=\bigcup\{K(x)\mid x\in X\}\cap C=\bigcup\{K(x)\cap C\mid x% \in X\}\subseteq K(v)\cap C$ . Now suppose that $s=\bigsqcup X$ , i.e. $K(s)\cap C\subseteq K(v)\cap C$ . By construction, $w\in K(s)$ and thus $w\leq s$ , which implies $K(w)\cap C\subseteq K(s)\cap C$ and yields with $v\in K(w)$ that $v\in K(s)\cap C\subseteq K(v)$ . But $I=\bigcup\{\{y\mid y\leq x\}\mid x\in X\}$ is a semi-ideal with $\bigsqcup I=\bigsqcup X=s\geq v$ . Further, we have that $v\not\in I$ since $v\not\in P$ while $I\subseteq P$ due to $X\subseteq P$ and downward-closure of $P$ . This is a contradiction to $v\in K(v)$ . $\hfill\blacktriangleleft$

Corollary 32.

There is a weakly $\leq$ -separating set $H\subseteq\operatorname{Hom}(\mathcal{L}^{*},\mathcal{S}_{3})$ for every completely distributive lattice $\mathcal{L}$ . Hence, every completely distributive lattice has strong compactness.

Note that we lose implications when moving from the Boolean semiring to a lattice $\mathcal{L}\not\cong\mathbb{B}$ . For instance, we have that $\forall x(x=x)\models_{\mathbb{B}}\forall x(Rx\vee\lnot Rx)$ while $\forall x(x=x)\not\models_{\mathcal{L}}\forall x(Rx\vee\lnot Rx)$ , so even for lattices the entailment relation actually becomes more fine-grained. However, the proof of strong compactness for lattices implies that as soon as $\mathcal{L}$ contains at least three elements, so is not isomorphic to $\mathbb{B}$ , then the same implications $\Phi\models_{\mathcal{L}}\psi$ will hold, no matter which specific lattice we consider.

Example 33.

Consider the fuzzy semiring $\mathbb{F}$ and an $\mathbb{F}$ -interpretation $\pi$ with universe $A$ . For $\varphi_{n}\coloneqq\exists x_{1}\dots\exists x_{n}(\bigwedge_{i<j\leq n}x_{i}% \neq x_{j}\wedge\bigwedge_{i\leq n}Ra_{i})$ and $\Phi=\{\varphi_{n}\mid n\in\omega\}$ we have that

\pi\llbracket\Phi\rrbracket=\bigsqcap_{n\in\omega}\bigsqcup_{\begin{subarray}{% c}A^{\prime}\subseteq A,\\ |A^{\prime}|=n\end{subarray}}\bigsqcap_{a\in A^{\prime}}\pi(Ra)=\bigsqcup_{% \begin{subarray}{c}A^{\prime}\subseteq A,\\ |A^{\prime}|=\omega\end{subarray}}\bigsqcap\{\pi(Ra)\mid a\in A^{\prime}\}% \eqqcolon s_{\pi}

due to complete distributivity. However, we can use strong compactness to prove that $\Phi$ cannot be collapsed to a single axiom $\psi$ with $\psi\equiv_{\mathbb{F}}\Phi$ on $\mathbb{F}$ . Towards a contradiction, suppose that there was some $\psi\in\operatorname{FO}$ with $\pi\llbracket\psi\rrbracket=s_{\pi}$ for each $\mathbb{F}$ -interpretation $\pi$ . By definition, we have that $\Phi\models_{\mathbb{F}}\psi$ and, since $\mathbb{F}$ has strong compactness, there must be some $n_{0}\in\omega$ such that $\{\varphi_{n}\mid n\leq n_{0}\}\models_{\mathbb{F}}\psi$ . But for the $\mathbb{F}$ -interpretation $\pi$ over universe $A=\{a_{i}\mid i\in\omega\}$ with $\pi(Ra_{i})=0.5^{i}$ we have $\pi\llbracket\{\varphi_{n}\mid n\leq n_{0}\}\rrbracket=0.5^{n_{0}}>0=s_{\pi}$ , a contradiction. $\lrcorner$

6 Compactness up to Powers

The counterexamples against strong compactness from Section 3 rely on the following idea: By using the $n$ -fold conjunction of the same formula, $\Phi$ was constructed such that it must be evaluated to some infinite power while every finite $\Phi_{0}\subseteq\Phi$ evaluates to a finite power. This raises the question whether this is the only reason why strong compactness fails for semirings such as $\mathbb{V},\mathbb{L}$ , or $\mathbb{S}^{\infty}(X)$ and whether these semirings still satisfy a weaker variant of compactness which takes finite conjunctions of formulae into account.

Definition 34.

We say that an infinitary absorptive semiring $\mathcal{S}$ has strong compactness up to powers if for every $\Phi\subseteq\operatorname{FO}$ and every $\psi\in\operatorname{FO}$ such that $\Phi\models_{\mathcal{S}}\psi$ there exists a finite subset $\Phi_{0}\subseteq\Phi$ such that $\{\varphi^{n}\mid\varphi\in\Phi_{0},n\in\omega\}\models_{\mathcal{S}}\psi$ where $\varphi^{n}$ denotes the $n$ -fold conjunction of $\varphi$ .

We show that, even in this weakened variant, strong compactness does not generalise to the semiring setting. To see this, consider the Viterbi semiring and suppose that $\pi$ is an infinite $\mathbb{V}$ -interpretation. Evaluating $\psi\coloneqq\forall x\exists y\forall zExy$ on $\pi$ yields $\pi\llbracket\psi\rrbracket=\prod_{a\in A}\bigsqcup_{b\in A}\pi(Eab)^{|A|}$ , i.e. $\pi\llbracket\psi\rrbracket=1$ if for each $a\in A$ there is some $b\in A$ s.t. $\pi(Eab)=1$ , and $\pi\llbracket\psi\rrbracket=0$ otherwise. Now assume that there is a Boolean linear order available on $\pi$ (in $\mathbb{V}$ we can even use $\forall x\forall y\forall z(x<y\vee x\not<y)$ to express that $<$ is Boolean) and compare $\pi\llbracket\psi\rrbracket$ to the relativised formula $\vartheta\coloneqq\forall x\exists y\forall z(z\not<x\vee Exy)$ . Analogously to the previous case, we can only have that $\pi\llbracket\vartheta\rrbracket>0$ if for every $a\in A$ with infinitely many $<$ -predecessors, there is some $b\in A$ s.t. $\pi(Eab)=1$ because $\pi\llbracket\vartheta\rrbracket=\prod_{a\in A}\bigsqcup_{b\in A}\pi(Eab)^{|\{% c\mid c<a\}|}$ . Based on this observation, we can construct a counterexample against strong compactness up to powers for $\mathbb{V}$ . By adding formulae $\varphi_{n}$ for each $n$ to $\vartheta$ which make sure that the $n$ -th minimal element in $\pi$ also has an outgoing edge valuated with $1$ , we obtain a set $\Phi$ with $\Phi\models_{\mathbb{V}}\psi$ . However, a finite subset $\Phi_{0}\subseteq\{\vartheta\}\cup\{\varphi_{n}\mid n<n_{0}\}$ cannot make sure that the $n_{0}$ -th element $a_{n_{0}}$ has an outgoing edge labelled $1$ . Instead, we might still have that $\pi\llbracket\Phi_{0}\rrbracket=\pi\llbracket\Phi_{0}\rrbracket^{\infty}=1$ if $\{\pi(Ea_{n_{0}}b)\mid b\in A\}$ converges to $1$ . The main property we use here is that even if $(s_{i})_{i\in I}\subseteq\mathbb{V}$ converges to $1$ , it might be that $\bigsqcup_{i\in I}s_{i}^{\infty}\neq 1=(\bigsqcup_{i\in I}s_{i})^{\infty}$ while $\bigsqcup_{i\in I}s_{i}^{n}=1$ for each $n$ or, more generally, that $h\colon x\mapsto x^{\infty}$ does not commute with suprema. We show in Appendix A that this condition causes strong compactness up to powers to fail.

Theorem 35.

If $h\colon x\mapsto x^{\infty}$ does not commute with suprema, then $\mathcal{S}$ does not have strong compactness up to powers. In particular, the semirings $\mathbb{V},\mathbb{T},\mathbb{L}$ , and $\mathbb{D}$ do not have strong compactness up to powers.

However, there are also semirings violating strong compactness that do satisfy strong compactness up to powers. We show that, under the assumption that the natural order of $\mathcal{S}$ is completely distributive, it is not only necessary but also sufficient for strong compactness up to powers that $h\colon x\mapsto x^{\infty}$ commutes with suprema as this makes $h$ an $\infty$ -homomorphism.

Theorem 36.

Let $\mathcal{S}$ be an infinitary absorptive semiring in which the natural order is completely distributive and where $h\colon x\mapsto x^{\infty}$ commutes with suprema, i.e. $h$ is an $\infty$ -homomorphism. Then $\mathcal{S}$ has strong compactness up to powers.

Proof.

If $h\colon x\mapsto x^{\infty}$ is an $\infty$ -homomorphism, $\{s^{\infty}\mid s\in\mathcal{S}\}$ induces a subsemiring of $\mathcal{S}$ , which we denote by $\mathcal{S}^{\infty}$ . Clearly, $\mathcal{S}^{\infty}$ is multiplicatively idempotent, so a distributive lattice. As we assume that the natural order in $\mathcal{S}$ is completely distributive, so is $\mathcal{S}^{\infty}$ , which is why $\mathcal{S}^{\infty}$ has strong compactness. Because $\mathcal{S}^{\infty}$ is a subsemiring of $\mathcal{S}$ , $\Phi\models_{\mathcal{S}}\psi$ clearly implies $\Phi\models_{\mathcal{S}^{\infty}}\psi$ . Thus, it suffices to prove that $\{\bigwedge\Phi_{0}\}\equiv_{\mathcal{S}}\Phi_{0}\models_{\mathcal{S}^{\infty}}\psi$ implies $\{\varphi^{n}\mid\varphi\in\Phi_{0},n\in\omega\}\equiv_{\mathcal{S}}\{(% \bigwedge\Phi_{0})^{n}\mid n\in\omega\}\models_{\mathcal{S}}\psi$ . So let $\{\varphi\}\models_{\mathcal{S}^{\infty}}\psi$ and $\pi$ be a model-defining $\mathcal{S}$ -interpretation. For the distributive lattice $\mathcal{S}^{\infty}_{0}$ which extends $\mathcal{S}^{\infty}$ by an additional zero denoted $0^{*}$ , we also have that $\{\varphi\}\models_{\mathcal{S}^{\infty}_{0}}\psi$ , as shown in Section 5, because $\mathcal{S}^{\infty}$ and $\mathcal{S}^{\infty}_{0}$ both are completely distributive lattices. Let $h^{*}\colon\mathcal{S}\to\mathcal{S}^{\infty}_{0}$ with $h^{*}\colon s\mapsto s^{\infty}$ if $s>0$ and $h^{*}\colon 0\mapsto 0^{*}$ . Because $h$ is an $\infty$ -homomorphism, so is $h^{*}$ . Note that, as opposed to $h\circ\pi$ , $h^{*}\circ\pi$ must be model-defining. For $\pi\llbracket\varphi\rrbracket>0$ we can conclude

\pi\llbracket\varphi\rrbracket^{\infty}=h^{*}(\pi\llbracket\varphi\rrbracket)=% (h^{*}\circ\pi)\llbracket\varphi\rrbracket\leq(h^{*}\circ\pi)\llbracket\psi% \rrbracket\overset{\star}{\leq}(h\circ\pi)\llbracket\psi\rrbracket=h(\pi% \llbracket\psi\rrbracket)=\pi\llbracket\psi\rrbracket^{\infty}\leq\pi% \llbracket\psi\rrbracket,

where $(\star)$ uses that $(h^{*}\circ\pi)(L)\leq(h\circ\pi)(L)$ for each literal $L$ if $(h\circ\pi)$ is considered an $\mathcal{S}^{\infty}_{0}$ -interpretation. Hence, $\{\varphi^{n}\mid n\in\omega\}\models_{\mathcal{S}}\psi$ , which proves the claim. $\hfill\blacktriangleleft$

Corollary 37.

If $\mathcal{S}$ is strongly distributive (i.e., infinitary multiplication distributes over infinitary addition in $\mathcal{S}$ ) or $n$ -idempotent for some $n$ , then $\mathcal{S}$ has strong compactness up to powers. In particular, the semirings $\mathbb{S}^{\infty}(X)$ and $\mathbb{S}^{n}(X)$ have strong compactness up to powers.

Notice that for $n$ -idempotent $\mathcal{S}$ , Theorem 36 implies that for each $\Phi\models_{\mathcal{S}}\psi$ , there must be some finite set $\Psi$ with the property that $\Psi\models_{\mathcal{S}}\psi$ due to the logical equivalence $\{\varphi^{m}\mid\varphi\in\Phi_{0},m\in\omega\}\equiv_{\mathcal{S}}\{\varphi^% {n}\mid\varphi\in\Phi_{0}\}$ .

7 Summary and Conclusion

Figure 2: Relationship between variants of compactness and algebraic properties of the underlying semiring. While

X_{\text{fin}}

is a finite set of variables and

X_{\text{inf}}

an infinite set,

X

is of arbitrary cardinality.

In this paper, we have studied the relationship between compactness properties of semiring semantics with algebraic properties of the underlying (infinitary absorptive) semiring. This does not only provide a basis for the generalisation of further model-theoretic properties that rely on compactness, such as Löwenheim–Skolem or preservation theorems, but also yields insights into the logical equivalences which admit the transfer of classical compactness to more general settings. Within the semiring semantics framework, algebraic and model-theoretic properties are closely linked since algebraic equalities (such as multiplicative idempotence) correspond to logical equivalences (e.g. $\varphi\wedge\varphi\equiv\varphi$ ), which might not be preserved when moving from the Boolean to a more complex semiring. Yet, it is not clear how this affects non-trivial model-theoretic results such as compactness.

While a weak form of compactness in terms of satisfiability holds for all infinitary absorptive semirings, this is not the case for stronger versions in terms of entailment. We proved that compactness generalises to finite semirings by simulating semiring semantics in classical Boolean semantics over an extended signature which allows the encoding of semiring valuations. Our main result, however, is the generalisation to (possibly infinite) completely distributive lattice semirings, from which we can infer that the logical equivalence $\varphi\equiv\varphi\wedge\varphi$ ensures strong compactness. We expanded the reduction technique of separating homomorphisms introduced in [12], on the one hand, to take the natural order into account and, more interestingly, to cope with the failure of continuity of homomorphisms from lattices with dense intervals, such as the fuzzy semiring. We believe that this generalised proof technique has applications beyond compactness. Several other model-theoretic results for semiring semantics are based on separating homomorphism and are thus affected by missing continuity. Future work will include the application of weakly separating homomorphism sets to model-theoretic tools such as Ehrenfeucht–Fraïssé games, which, up to now, could only be applied to finite lattice semirings [5].

On the other hand, we discussed counterexamples against strong compactness in semirings that are not $n$ -idempotent for any $n$ , that is, that do not admit logical equivalences of the form $\varphi^{n}\equiv\varphi^{n}\wedge\varphi$ where $\varphi^{n}$ denotes the $n$ -fold conjunction of $\varphi$ . In some cases, such as for the tropical or the Łukasiewicz semiring, strong compactness fails in an even stronger sense. We showed that in these semirings, the lack of idempotence cannot be circumvented by moving to strong compactness up to powers, where the entailment relation is no longer based on finite subsets $\Phi_{0}\subseteq\Phi$ but on their closures under finite conjunctions of the same formula. Figure 2 summarises the connection between algebraic properties of the semiring and variants of compactness established by our results. It remains open for future work to close the gap between multiplicative $n$ -idempotence and multiplicative idempotence (lattices). We conjecture that $n$ -idempotence might already suffice for strong compactness. Possible approaches for proving this include a two-sorted approach discussed in [18] or a generalisation of the homomorphism technique from Section 5. Towards the generalisation of further model-theoretic properties that rely on compactness, we formulate (in the appendix) a variant of the upward Löwenheim–Skolem theorem for semirings that have strong compactness. The analysis of further consequences of compactness, for instance concerning preservation theorems, will be studied in future work.

References

[1] A. Atserias and P. Kolaitis. Consistency, acyclicity, 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, Cham, 2023. doi:10.1007/978-3-031-24117-8_17.
[2] A. Atserias and P. Kolaitis. Consistency of relations over monoids. J. ACM, 72(3), May 2025. doi:10.1145/3721855.
[3] G. Badia, P. Kolaitis, and C. Noguera. Codd’s theorem for databases over semirings. Proc. ACM Manag. Data, 3(5), November 2025. doi:10.1145/3767713.
[4] C. Bizière, E. Grädel, and M. Naaf. Locality theorems in semiring semantics. In Proceedings of MFCS 2023, 2023. doi:10.4230/LIPIcs.MFCS.2023.20.
[5] S. Brinke, E. Grädel, and L. Mrkonjić. Ehrenfeucht–Fraïssé games in semiring semantics. In Proceedings of CSL 2024, 2024. doi:10.4230/LIPIcs.CSL.2024.19.
[6] 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. doi:10.4230/OASIcs.Tannen.3.
[7] P. Cintula and M. Navara. Compactness of fuzzy logics. Fuzzy Sets Syst., 143(1):59–73, 2004. doi:10.1016/J.FSS.2003.06.002.
[8] J. Foster, T. Green, and V. Tannen. Annotated XML: queries and provenance. In Proceedings of PODS 2008, pages 271–280, 2008. doi:10.1145/1376916.1376954.
[9] B. Glavic. Data provenance. Foundations and Trends in Databases, 9(3-4):209–441, 2021. doi:10.1561/1900000068.
[10] 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 Proceedings of LICS 2022, pages 41:1–41:12. ACM, 2022. doi:10.1145/3531130.3533358.
[11] E. Grädel, N. Lücking, and M. Naaf. Semiring provenance for Büchi games: Strategy analysis with absorptive polynomials. Logical Methods in Computer Science, 20(1), 2024. doi:10.46298/lmcs-20(1:21)2024.
[12] E. Grädel and L. Mrkonjić. Elementary equivalence versus isomorphism in semiring semantics. In Proceedings of ICALP 2021, volume 198, pages 133:1–133:20, Dagstuhl, Germany, 2021. doi:10.4230/LIPIcs.ICALP.2021.133.
[13] E. Grädel and V. Tannen. Semiring provenance for first-order model checking, 2017. arXiv:1712.01980.
[14] 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.
[15] 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. doi:10.1007/978-3-031-86319-6_21.
[16] T. Green, G. Karvounarakis, and V. Tannen. Provenance semirings. In Proceedings of PODS 2007, pages 31–40. ACM, 2007. doi:10.1145/1265530.1265535.
[17] T. Green and V. Tannen. The semiring framework for database provenance. In Proceedings of PODS 2017, pages 93–99. ACM, 2017. doi:10.1145/3034786.3056125.
[18] L. Mrkonjić. Semiring Semantics: Algebraic Foundations, Model Theory, and Strategy Analysis. PhD thesis, RWTH Aachen University, 2025. doi:10.18154/RWTH-2025-03940.
[19] M. Naaf. Logic, Semirings, and Fixed Points. PhD thesis, RWTH Aachen University, 2024. doi:10.18154/RWTH-2024-10804.
[20] George N. Raney. A subdirect-union representation for completely distributive complete lattices. Proceedings of the American Mathematical Society, 4(4):518–522, 1953. doi:10.1090/S0002-9939-1953-0058568-4.
[21] P. Rothmaler. Introduction to Model Theory. CRC Press, 2018. doi:10.1201/9781315273822.

Appendix A Omitted Proofs

The proofs of Lemma 22 and Proposition 24 from Section 5 are provided in the following.

Lemma 22. [Restated, see original statement.]

There is a $\leq$ -separating set of $\infty$ -homomorphisms from $\mathcal{L}^{*}$ to $\mathcal{S}_{3}$ if, and only if, $\mathcal{L}$ is a completely distributive lattice without dense intervals.

Proof.

As shown in [18], $\mathcal{L}$ is completely distributive and does not contain dense intervals if, and only if, there is a separating set $H\subseteq\operatorname{Hom}^{\infty}(\mathcal{L},\mathbb{B})$ (recall that $H$ is separating if for each $s\neq t$ there is some $h\in H$ such that $h(s)\neq h(t)$ ). We show that this is equivalent to the existence of a $\leq$ -separating set $H^{*}\subseteq\text{Hom}^{\infty}(\mathcal{L}^{*},\mathcal{S}_{3})$ . So suppose that there is some separating $H\subseteq\text{Hom}^{\infty}(\mathcal{L},\mathbb{B})$ . If $t=0^{*}$ we can $\leq$ -separate $s$ and $t$ by mapping $0^{*}$ to $0\in\mathcal{S}_{3}$ and every other element in $\mathcal{L}^{*}$ to $1$ . Otherwise, we have $t,s\sqcup t\in\mathcal{L}$ and there must be some $h\in H$ with $h(s\sqcup t)\neq h(t)$ , i.e. $h(s\sqcup t)=h(s)\vee h(t)=1$ and $h(t)=0$ , which implies $h(s)\not\leq h(t)$ . Hence, we can $\leq$ -separate $s$ from $t$ via $h^{*}\colon\mathcal{L}^{*}\to\mathcal{S}_{3}$ with $h^{*}(0^{*})=0$ , $h^{*}(u)=\varepsilon$ if $h(u)=0$ and $h^{*}(u)=1$ otherwise. To prove the converse, let $H^{*}\subseteq\text{Hom}^{\infty}(\mathcal{L}^{*},\mathcal{S}_{3})$ be $\leq$ -separating and $s\neq t\in\mathcal{L}$ . As $s\not\leq t$ or $t\not\leq s$ , there must be some $h^{*}\in H^{*}$ with $h^{*}(s)\neq h^{*}(t)$ and $(h^{*})^{-1}(0)=\{0^{*}\}$ , and we can separate $s$ and $t$ via $h\colon\mathcal{S}\to\mathcal{T}$ with $h(u)=0$ if $h^{*}(u)\leq\varepsilon$ and $h(u)=1$ otherwise. $\hfill\blacktriangleleft$

Proposition 24. [Restated, see original statement.]

Let $h\colon\mathcal{S}\to\mathcal{T}$ be a homomorphism (which does not necessarily respect the infinitary operations) into a min-max semiring $\mathcal{T}$ , and let $t\in\mathcal{T}$ .

(1)

If $h(\pi\llbracket\varphi(\bar{a})\rrbracket)\geq t$ and if for all $X\subseteq\mathcal{S}$ with $\pi\llbracket\varphi(\bar{a})\rrbracket=\bigsqcup X$ there is some $x\in X$ such that $h(x)\geq t$ , then also $(h\circ\pi)\llbracket\varphi(\bar{a})\rrbracket\geq t$ .
(2)

If $h(\pi\llbracket\varphi(\bar{a})\rrbracket)\leq t$ and if for all $X\subseteq\mathcal{S}$ with $\pi\llbracket\varphi(\bar{a})\rrbracket=\bigsqcap X$ there is some $x\in X$ such that $h(x)\leq t$ , then also $(h\circ\pi)\llbracket\varphi(\bar{a})\rrbracket\leq t$ .

Proof.

We proceed by induction on $\varphi(\bar{a})$ and only prove the first implication as the reasoning for $(2)$ is analogous. The base case, where $\varphi(\bar{a})$ is a literal, is satisfied by definition.

Let $\varphi=\varphi_{0}\wedge\varphi_{1}$ . If $t\leq h(\pi\llbracket\varphi\rrbracket)=\min(h(\pi\llbracket\varphi_{0}% \rrbracket),h(\pi\llbracket\varphi_{1}\rrbracket))$ , then $t\leq h(\pi\llbracket\varphi_{i}\rrbracket)$ is true for $i\in\{0,1\}$ . Towards a contradiction, suppose that $\pi\llbracket\varphi_{i}\rrbracket=\bigsqcup X$ with $h(x)<t$ for each $x\in X$ . Then $\pi\llbracket\varphi\rrbracket=\pi\llbracket\varphi_{1-i}\rrbracket\cdot% \bigsqcup X=\bigsqcup\{\pi\llbracket\varphi_{1-i}\rrbracket\cdot x\mid x\in X\}$ violates the assumption on $\pi\llbracket\varphi\rrbracket$ as $h(\pi\llbracket\varphi_{1-i}\rrbracket\cdot x)\leq h(x)<t$ . Hence, the induction hypothesis can be applied to $\varphi_{0}$ and $\varphi_{1}$ and we obtain $(h\circ\pi)\llbracket\varphi(\bar{a})\rrbracket=\min((h\circ\pi)\llbracket% \varphi_{0}\rrbracket,(h\circ\pi)\llbracket\varphi_{1}\rrbracket)\geq t$ .

For $\varphi=\varphi_{0}\vee\varphi_{1}$ we get $t\leq\max(h(\pi\llbracket\varphi_{0}\rrbracket),h(\pi\llbracket\varphi_{1}% \rrbracket))$ , i.e. $t\leq h(\pi\llbracket\varphi_{i}\rrbracket)$ for some $i\in\{0,1\}$ . Suppose that $\pi\llbracket\varphi_{i}\rrbracket=\bigsqcup X$ with $h(x)<t$ for each $x\in X$ . We cannot have that $h(\pi\llbracket\varphi_{1-i}\rrbracket)<t$ as $\pi\llbracket\varphi\rrbracket=\pi\llbracket\varphi_{1-i}\rrbracket\sqcup% \bigsqcup X=\bigsqcup\{\pi\llbracket\varphi_{1-i}\rrbracket\}\cup X$ would yield a contradiction. If $\pi\llbracket\varphi_{1-i}\rrbracket=\bigsqcup Y$ where $h(y)<t$ for $y\in Y$ , we obtain a contradiction by $\pi\llbracket\varphi\rrbracket=\bigsqcup X\sqcup\bigsqcup Y=\bigsqcup X\cup Y$ , so the IH must either be applicable to $\varphi_{0}$ or to $\varphi_{1}$ . Both cases yield $\max((h\circ\pi)\llbracket\varphi_{0}\rrbracket,(h\circ\pi)\llbracket\varphi_{% 1}\rrbracket)\geq t$ .

Now let $\varphi(\bar{a})=\exists x\psi(\bar{a},x)$ and $A^{\prime}\coloneqq\{a\in A\mid h(\pi\llbracket\psi(\bar{a},a)\rrbracket)\geq t\}$ . By assumption, ${A^{\prime}\neq\varnothing}$ . Suppose that for each $a\in A^{\prime}$ , there is some $X_{a}$ such that $\pi\llbracket\psi(\bar{a},a)\rrbracket)=\bigsqcup X_{a}$ and $h(x)<t$ for $x\in X_{a}$ . Then we would have $\pi\llbracket\varphi(\bar{a})\rrbracket=\bigsqcup\bigcup_{a\in A^{\prime}}X_{a% }\cup\{\pi\llbracket\psi(\bar{a},a)\rrbracket\mid a\in A\setminus A^{\prime}\}$ , a contradiction. Hence there must be some $a\in A^{\prime}$ the IH can be applied to and we obtain $(h\circ\pi)\llbracket\varphi(\bar{a})\rrbracket\geq(h\circ\pi)\llbracket\psi(% \bar{a},a)\rrbracket\geq t$ .

It remains to prove the claim for $\varphi(\bar{a})=\forall x\psi(\bar{a},x)$ . By monotonicity of $h$ , we have that $h(\pi\llbracket\psi(\bar{a},a)\rrbracket)\geq h(\pi\llbracket\varphi(\bar{a})% \rrbracket)\geq t$ for each $a\in A$ . Suppose that there is some $a\in A$ such that $\pi\llbracket\psi(\bar{a},a)\rrbracket=\bigsqcup X$ with $h(x)<t$ for $x\in X$ . To infer a contradiction, we observe that $\pi\llbracket\varphi(\bar{a})\rrbracket=\bigsqcup X\cdot\prod_{b\in A\setminus% \{a\}}\pi\llbracket\psi(\bar{a},b)\rrbracket=\bigsqcup\{x\cdot\prod_{b\in A% \setminus\{a\}}\pi\llbracket\psi(\bar{a},b)\rrbracket\mid x\in X\}$ with $h(x\cdot\prod_{b\in A\setminus\{a\}}\pi\llbracket\psi(\bar{a},b)\rrbracket)% \leq h(x)<t$ for $x\in X$ . Hence we have that $(h\circ\pi)\llbracket\psi(\bar{a},a)\rrbracket\geq t$ for each $a\in A$ and thus $(h\circ\pi)\llbracket\varphi(\bar{a})\rrbracket=\bigsqcap_{a\in A}(h\circ\pi)% \llbracket\psi(\bar{a},a)\rrbracket\geq t$ . $\hfill\blacktriangleleft$

We also provide proofs for Theorem 35 and Corollary 37 from Section 6. The following additional lemma is required to prove Theorem 35.

Lemma 38.

If $h\colon x\mapsto x^{\infty}$ does not commute with suprema, then there is some $X\subseteq\mathcal{S}$ with $\bigsqcup\{x^{\infty}\mid x\in X\}<(\bigsqcup X)^{\infty}$ while $\bigsqcup\{x^{n}\mid x\in X\}=(\bigsqcup X)^{n}$ for each $n\in\omega$ .

Proof.

By monotonicity, we have $\bigsqcup\{x^{\infty}\mid x\in X\}\leq(\bigsqcup X)^{\infty}$ for each $X\subseteq\mathcal{S}$ , so if $h$ does not respect suprema, there must be some $X_{0}\subseteq\mathcal{S}$ such that $\bigsqcup\{x^{\infty}\mid x\in X_{0}\}<(\bigsqcup X_{0})^{\infty}$ . Note that $X_{0}$ must be infinite as $s^{\infty}\sqcup t^{\infty}=(s\sqcup t)^{\infty}$ is true for every $s,t\in\mathcal{S}$ (we obtain $(s\sqcup t)^{2n}\leq s^{n}\sqcup t^{n}$ by observing that every term in $(s\sqcup t)^{2n}$ contains $s$ or $t$ at least $n$ times). We construct a chain $(X_{i})_{i\in\omega}$ according to $X_{i+1}\coloneqq\{x\sqcup y\mid x,y\in X_{i}\}$ . It follows by induction that $\bigsqcup\{x^{\infty}\mid x\in X_{0}\}=\bigsqcup\{x^{\infty}\mid x\in X_{i}\}$ for each $i\in\omega$ as $\bigsqcup\{x^{\infty}\mid x\in X_{i+1}\}=\bigsqcup\{(x\sqcup y)^{\infty}\mid x% ,y\in X_{i}\}=\bigsqcup\{x^{\infty}\sqcup y^{\infty}\mid x,y\in X_{i}\}=% \bigsqcup\{x^{\infty}\mid x\in X_{i}\}$ . We claim that $X\coloneqq\bigcup\{X_{i}\mid i\in\omega\}$ has the desired properties. On the one hand, we have that $\bigsqcup\{x^{\infty}\mid x\in X\}=\bigsqcup\{\bigsqcup\{x^{\infty}\mid x\in X% _{i}\}\mid i\in\omega\}=\bigsqcup\{x^{\infty}\mid x\in X_{0}\}<(\bigsqcup X_{0% })^{\infty}\leq(\bigsqcup X)^{\infty}$ . Moreover, $\bigsqcup\{x^{n}\mid x\in X\}\leq(\bigsqcup X)^{n}$ for each $n\in\omega$ due to monotonicity. By construction, $X$ is closed under finite suprema and hence

	$\displaystyle(\,\bigsqcup X)^{n}$	$\displaystyle=\bigsqcup\{x_{1}\cdots x_{n}\mid x_{1},\dots,x_{n}\in X\}$
		$\displaystyle\leq\bigsqcup\{(x_{1}\sqcup\dots\sqcup x_{n})^{n}\mid x_{1},\dots% ,x_{n}\in X\}=\bigsqcup\{x^{n}\mid x\in X\}.\$

$\hfill\blacktriangleleft$

Theorem 35. [Restated, see original statement.]

If $h\colon x\mapsto x^{\infty}$ does not commute with suprema, then $\mathcal{S}$ does not have strong compactness up to powers. In particular, the semirings $\mathbb{V},\mathbb{T},\mathbb{L}$ , and $\mathbb{D}$ do not have strong compactness up to powers.

Proof.

We claim that $\Phi\coloneqq\{\varphi_{n}\mid n\in\omega\}\cup\{\vartheta,\varphi_{\text{LO}}% \}\models_{\mathcal{S}}\forall x\exists y\forall zExy\eqqcolon\psi$ where

	$\displaystyle\varphi_{n}$	$\displaystyle\coloneqq\exists x_{1}\dots\exists x_{n}\left(\varphi_{\text{pre}% }(x_{1},\dots,x_{n})\wedge\bigwedge_{i\leq n}\forall yEx_{i}y\right)\text{ with}$
	$\displaystyle\varphi_{\text{pre}}(x_{1},\dots,x_{n})$	$\displaystyle\coloneqq\forall y(y\not<x_{1}\wedge\bigwedge_{i<n}x_{i}<x_{i+1}% \wedge(x_{i}\not<y\vee y\not<x_{i+1})),$
	$\displaystyle\vartheta$	$\displaystyle\coloneqq\forall x\exists y\forall z(z\not<x\vee Exy)$

and $\varphi_{\text{LO}}$ states (in Boolean semantics) that $<$ is a linear order. Let $\pi$ be a model-defining $\mathcal{S}$ -interpretation with $\pi\llbracket\Phi\rrbracket>0$ and recall the flattening $\pi^{\mathbb{B}}$ of $\pi$ , where $\pi^{\mathbb{B}}(L)=1$ if, and only if, $\pi(L)>0$ . Since $1$ is maximal in $\mathcal{S}$ , we have that $\pi^{\mathbb{B}}(L)\geq\pi(L)$ for all $L\in\text{Lit}_{A}(\tau)$ . By monotonicity, this inequality can be lifted to formulae, and for each $\varphi\in\Phi$ , we get $\pi^{\mathbb{B}}\llbracket\varphi\rrbracket\geq\pi\llbracket\varphi\rrbracket>0$ , i.e. $\pi^{\mathbb{B}}\llbracket\varphi\rrbracket=1$ . Due to $\pi^{\mathbb{B}}\llbracket\varphi_{\text{LO}}\rrbracket=1$ , $\pi^{\mathbb{B}}$ is linearly ordered by $<$ . Moreover, $\pi^{\mathbb{B}}\llbracket\varphi_{\text{pre}}(a_{1},\dots,a_{n})\rrbracket=1$ if, and only if, $a_{1},\dots,a_{n}$ is a prefix of $<$ . Hence, $\pi^{\mathbb{B}}\llbracket\varphi_{n}\rrbracket=1$ for each $n$ implies there is an infinite discrete prefix $(a_{i})_{i\in\omega}\subseteq A$ w.r.t. $<$ .

For each $n$ , $(a_{1},\dots,a_{n})$ is the unique tuple such that $\pi^{\mathbb{B}}\llbracket\varphi_{\text{pre}}(a_{1},\dots,a_{n})\rrbracket=1$ and thus the unique tuple with $\pi\llbracket\varphi_{\text{pre}}(a_{1},\dots,a_{n})\rrbracket>0$ . Therefore, $\pi\llbracket\varphi_{n}\rrbracket\leq\prod_{i\leq n}\prod_{b\in A}\pi(Ea_{i}b)$ and thus $\pi\llbracket\{\varphi_{n}\mid n\in\mathbb{N}\}\rrbracket\leq\prod_{i\in\omega% }\prod_{b\in A}\pi(Ea_{i}b)^{\infty}\leq\prod_{i\in\omega}\bigsqcup_{b\in A}% \pi(Ea_{i}b)^{\infty}$ . For every $a\in A\setminus\{a_{i}\mid i\in\omega\}\eqqcolon A^{\prime}$ it holds that

	$\displaystyle\pi\llbracket\exists y\forall z(z\not<a\vee Eay)\rrbracket$	$\displaystyle=\underset{b\in A}{\bigsqcup}\prod_{c\in A}(\pi(c\not<a)\sqcup\pi% (Eab))$
		$\displaystyle\leq\underset{b\in A}{\bigsqcup}\prod_{i\in\omega}(\underbrace{% \pi(a_{i}\not<a)}_{=0}\sqcup\pi(Eab))$
		$\displaystyle=\underset{b\in A}{\bigsqcup}\pi(Eab)^{\infty}.$

Hence, $\pi\llbracket\vartheta\rrbracket\leq\prod_{a\in A^{\prime}}\bigsqcup_{b\in A}% \pi(Eab)^{\infty}$ and overall $\pi\llbracket\Phi\rrbracket\leq\prod_{a\in A}\bigsqcup_{b\in A}\pi(Eab)^{% \infty}=\pi\llbracket\psi\rrbracket$ .

Now let $\Phi_{0}\subseteq\Phi$ be finite and $n_{0}$ be maximal such that $\varphi_{n_{0}}\in\Phi_{0}$ . By assumption, $h$ does not commute with suprema, so we can fix a set $X=\{s_{\beta}\mid\beta\in\mathrm{On},\beta<|X|\}$ as in Lemma 38. In order to disprove $\{\varphi^{n}\mid\varphi\in\Phi_{0},n\in\omega\}\models_{\mathcal{S}}\psi$ , we construct an $\mathcal{S}$ -interpretation $\pi$ such that $\pi\llbracket\{\varphi_{n}\mid n\leq n_{0}\}\cup\{\vartheta,\varphi_{\text{LO}% }\}\rrbracket^{\infty}=(\bigsqcup_{\beta<|X|}s_{\beta})^{\infty}>\bigsqcup_{% \beta<|X|}s_{\beta}^{\infty}=\pi\llbracket\psi\rrbracket$ . The universe of $\pi$ consists of elements $\{a_{\beta}\mid\beta<|X|\}$ and we set $\pi(a_{\beta}<a_{\gamma})=1$ if, and only if, $\beta<\gamma$ , implying $\pi\llbracket\varphi_{\text{LO}}\rrbracket=1$ . Further, we define $\pi(Ea_{i}b)=1$ for each $i\in\omega\setminus\{n_{0}+1\}$ and $b\in A$ , which yields $\pi\llbracket\varphi_{n}\rrbracket=1$ for $n\leq n_{0}$ , while setting $\pi(Ea_{n_{0}+1}a_{\beta})=s_{\beta}$ . Since $\pi\llbracket\exists y\forall z(z\not<a\vee Eay)\rrbracket=1$ for all $a\neq a_{n_{0}+1}$ , we obtain $\pi\llbracket\vartheta\rrbracket=\bigsqcup_{\beta<|X|}s_{\beta}^{n_{0}}=(% \bigsqcup_{\beta<|X|}s_{\beta})^{n_{0}}$ and overall $\pi\llbracket\{\varphi_{n}\mid n\leq n_{0}\}\cup\{\vartheta,\varphi_{\text{LO}% }\}\rrbracket^{\infty}=(\bigsqcup_{\beta<|X|}s_{\beta})^{\infty}$ as desired. On the other hand, $\pi\llbracket\forall x\exists y\forall zExy\rrbracket=\pi\llbracket\exists y% \forall zE{a_{n_{0}+1}}y\rrbracket=\bigsqcup_{b\in A}\pi(Ea_{n_{0}+1}b)^{% \infty}=\bigsqcup_{\beta<|X|}s_{\beta}^{\infty}$ . $\hfill\blacktriangleleft$

Corollary 37. [Restated, see original statement.]

If $\mathcal{S}$ is strongly distributive (i.e., infinitary multiplication distributes over infinitary addition in $\mathcal{S}$ ) or $n$ -idempotent for some $n$ , then $\mathcal{S}$ has strong compactness up to powers. In particular, the semirings $\mathbb{S}^{\infty}(X)$ and $\mathbb{S}^{n}(X)$ have strong compactness up to powers.

Proof.

By Theorem 36, it suffices to verify that $(\bigsqcup_{i\in I}s_{i})^{\infty}\leq\bigsqcup_{i\in I}s_{i}^{\infty}$ whenever $\mathcal{S}$ meets one of the above conditions. First suppose that $\mathcal{S}$ is strongly distributive (such as $\mathbb{S}^{\infty}(X)$ ). W.l.o.g. we can assume that $I$ is infinite since the finite case holds in every infinitary absorptive semiring (see the proof of Lemma 38). Because every $f\colon|I|^{+}\to I$ must hit some $i\in I$ infinitely often, we obtain $(\bigsqcup_{i\in I}s_{i})^{\infty}=(\bigsqcup_{i\in I}s_{i})^{|I|^{+}}=% \bigsqcup\{\prod_{\alpha<|I|^{+}}s_{f(\alpha)}\mid f\colon|I|^{+}\to I\}\leq% \bigsqcup_{i\in I}s_{i}^{\infty}$ .

Now let $\mathcal{S}$ be $n$ -idempotent for some $n$ , which, by finitary distributivity, implies that $(\bigsqcup_{i\in I}s_{i})^{\infty}=(\bigsqcup_{i\in I}s_{i})^{n}=\bigsqcup{\{% \prod_{i\leq n}s_{f(i)}^{n}\mid f\colon[1,n]\to I\}}$ . We fix some $f\colon[1,n]\to I$ and observe that

\prod_{i\leq n}s_{f(i)}\leq(s_{f(1)}\sqcup\dots\sqcup s_{f(n)})^{n}=(s_{f(1)}% \sqcup\dots\sqcup s_{f(n)})^{n\cdot n}\overset{\star}{\leq}s_{f(1)}^{n}\sqcup% \dots\sqcup s_{f(n)}^{n}\leq\bigsqcup_{i\in I}s_{i}^{\infty},

where $(\star)$ is due to the fact that each summand in $(s_{f(1)}\sqcup\dots\sqcup s_{f(n)})^{n\cdot n}$ must contain some $s_{f(i)}$ at least $n$ times. Hence, $\bigsqcup_{i\in I}s_{i}^{\infty}$ is an upper bound of $\{\prod_{i\leq n}s_{f(i)}^{n}\mid f\colon[1,n]\to I\}$ , which proves the claim. $\hfill\blacktriangleleft$

Appendix B The Löwenheim–Skolem Theorems

As an immediate consequence of strong compactness, we obtain a generalisation of the upward Löwenheim–Skolem theorem, which classically implies that sets of first-order formulae with finite models of unbounded size also admit infinite models with unbounded transfinite cardinalities. We generalise this to the semiring setting via entailment: For $\Phi\subseteq\operatorname{FO}$ and $\psi\in\operatorname{FO}$ , if there are arbitrarily large finite witnesses that disprove $\Phi\models_{\mathcal{S}}\psi$ , then there are witnesses of arbitrarily large transfinite sizes.

Theorem 39 (Upward Löwenheim–Skolem).

Let $\mathcal{S}$ have strong compactness (e.g. let $\mathcal{S}$ be finite or a completely distributive lattice) and $\Phi\cup\{\psi\}\subseteq\operatorname{FO}$ .

(1)

If $\pi\llbracket\Phi\rrbracket\not\leq\pi\llbracket\psi\rrbracket$ for arbitrarily large finite $\mathcal{S}$ -interpretations $\pi$ , then $\pi\llbracket\Phi\rrbracket\not\leq\pi\llbracket\psi\rrbracket$ also holds for some infinite $\pi$ .
(2)

If $\pi\llbracket\Phi\rrbracket\not\leq\pi\llbracket\psi\rrbracket$ for some infinite $\mathcal{S}$ -interpretation $\pi$ , then there is some $\pi_{\kappa}$ for each $\kappa\in\operatorname{Cn}$ with $|\pi|\geq\kappa$ such that $\pi_{\kappa}\llbracket\Phi\rrbracket\not\leq\pi_{\kappa}\llbracket\psi\rrbracket$ .

Example 40.

Let $\mathcal{S}$ be a completely distributive lattice. We show there is no $\Phi\subseteq\operatorname{FO}$ such that $\pi\llbracket\Phi\rrbracket=\bigsqcap\{s\mid\pi(Ra)=s\text{ for infinitely % many }a\in A\}$ for each $\mathcal{S}$ -interpretation $\pi$ . Towards a contradiction, suppose that $\Phi$ exists. For finite $\pi$ , we have that $\pi\llbracket\Phi\rrbracket=\bigsqcap\varnothing=1$ . Hence, we can find for each $n$ some $\pi_{n}$ with $|\pi_{n}|=n$ such that $\pi\llbracket\Phi\rrbracket\not\leq\pi\llbracket\exists xRx\rrbracket$ . For $\pi$ with $|\pi|>|\mathcal{S}|$ , however, we have that $\{\pi(Ra)\mid\pi(Ra)\text{ occurs infinitely often in }\pi\}\neq\varnothing$ , which implies $\pi\llbracket\Phi\rrbracket\leq\pi\llbracket\exists xRx\rrbracket$ , a contradiction. $\lrcorner$

In an even stronger sense, the proof of the classical downward Löwenheim–Skolem Theorem can be adapted without major difficulties to semiring interpretations, with a rather liberal condition on the underlying semiring.

Definition 41.

We say that the infinitary sum and product operations on a semiring $\mathcal{S}$ are countably tame if for every sequence $(s_{i})_{i\in I}$ there exist countable subsequences indexed by $J,K\subseteq I$ such that $\sum_{i\in I}s_{i}=\sum_{j\in J}s_{j}$ and $\prod_{i\in I}s_{i}=\prod_{k\in K}s_{k}$ . A semiring is countably tame if its infinitary sum and product operations are.

Clearly, the min-max semiring over $[0,1]$ is countably tame.

Definition 42.

Let $\pi_{A}\colon\operatorname{Lit}_{A}(\tau)\rightarrow\mathcal{S}$ be a semiring interpretation. A subinterpretation $\pi_{B}\subseteq\pi_{A}$ is the restriction of $\pi_{A}$ to $\operatorname{Lit}_{B}(\tau)$ for some subset $B\subseteq A$ . An elementary subinterpretation, denoted $\pi_{B}\preceq\pi_{A}$ , satisfies in addition that $\pi_{B}\llbracket\varphi(\bar{b})\rrbracket=\pi_{A}\llbracket\varphi(\bar{b})\rrbracket$ for every formula $\varphi(\bar{x})\in\operatorname{FO}(\tau)$ and every tuple $\bar{b}$ in $B$ .

Theorem 43 (Downward Löwenheim–Skolem).

Every $\mathcal{S}$ -interpretation $\pi_{A}\colon\operatorname{Lit}_{A}(\tau)\rightarrow\mathcal{S}$ with countable vocabulary $\tau$ into a countably tame semiring $\mathcal{S}$ has a countable elementary subinterpretation $\pi_{B}\preceq\pi_{A}$ .

Proof.

We construct a countable chain $B_{0}\subseteq B_{1}\subseteq\cdots$ of countable subsets $B_{n}\subseteq A$ as follows. Let $B_{0}\coloneqq\varnothing$ . Construct $B_{n+1}$ by adding to $B_{n}$ , for every formula $\varphi(x)\in\operatorname{FO}(\tau\cup B_{n})$ , countable collections $(b_{\varphi,i})_{i<\omega}$ and $(c_{\varphi,i})_{i<\omega}$ of elements from $A$ such that $\pi_{A}\llbracket\exists x\varphi(x)\rrbracket=\sum\{\pi_{A}\llbracket\varphi(% b_{\varphi},i)\rrbracket\mid i<\omega\}$ and $\pi_{A}\llbracket\forall x\varphi(x)\rrbracket=\prod\{\pi_{A}\llbracket\varphi% (c_{\varphi},i)\rrbracket\mid i<\omega\}$ , which is possible since the semiring is countably tame. Finally, let $B\coloneqq\bigcup_{n<\omega}B_{n}$ , which is clearly countable. We claim that $B$ induces an elementary subinterpretation $\pi_{B}\preceq\pi_{A}$ . Consider any formula $\psi(\bar{y})\in\operatorname{FO}(\tau)$ and any tuple $\bar{b}$ over $B$ . We have to prove that $\pi_{B}\llbracket\psi(\bar{b})\rrbracket=\pi_{A}\llbracket\psi(\bar{b})\rrbracket$ . This is proved by induction on $\psi$ . The only non-trivial cases are $\psi(\bar{y})=\exists x\varphi(x,\bar{y})$ and $\psi(\bar{y})=\forall x\varphi(x,\bar{y})$ . Obviously there is some $n<\omega$ such that all components of $\bar{b}$ are in $B_{n}$ which means that $\varphi(x,\bar{b})\in\operatorname{FO}(\tau\cup B_{n})$ . The construction makes sure that $B_{n+1}$ and hence $B$ , contains witnesses $(b_{\varphi,i})_{i<\omega}$ and $(c_{\varphi,i})_{i<\omega}$ to make sure that

\pi_{A}\llbracket\exists x\varphi(x,\bar{b})\rrbracket=\sum\{\pi_{A}\llbracket% \varphi(b_{\varphi,i},\bar{b})\rrbracket\mid i<\omega\}=\sum\{\pi_{B}% \llbracket\varphi(b_{\varphi,i},\bar{b})\rrbracket\mid i<\omega\}=\pi_{B}% \llbracket\exists x\varphi(x,\bar{b})\rrbracket,

and similarly for $\psi(\bar{y})=\forall x\varphi(x,\bar{y})$ using the witnesses $(c_{\varphi,i})_{i<\omega}$ . $\hfill\blacktriangleleft$

[bib.bib1] [1] A. Atserias and P. Kolaitis. Consistency, acyclicity, 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, Cham, 2023. doi:10.1007/978-3-031-24117-8_17.

[bib.bib2] [2] A. Atserias and P. Kolaitis. Consistency of relations over monoids. J. ACM, 72(3), May 2025. doi:10.1145/3721855.

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

[bib.bib4] [4] C. Bizière, E. Grädel, and M. Naaf. Locality theorems in semiring semantics. In Proceedings of MFCS 2023, 2023. doi:10.4230/LIPIcs.MFCS.2023.20.

[bib.bib5] [5] S. Brinke, E. Grädel, and L. Mrkonjić. Ehrenfeucht–Fraïssé games in semiring semantics. In Proceedings of CSL 2024, 2024. doi:10.4230/LIPIcs.CSL.2024.19.

[bib.bib6] [6] 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. doi:10.4230/OASIcs.Tannen.3.

[bib.bib7] [7] P. Cintula and M. Navara. Compactness of fuzzy logics. Fuzzy Sets Syst., 143(1):59–73, 2004. doi:10.1016/J.FSS.2003.06.002.

[bib.bib8] [8] J. Foster, T. Green, and V. Tannen. Annotated XML: queries and provenance. In Proceedings of PODS 2008, pages 271–280, 2008. doi:10.1145/1376916.1376954.

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

[bib.bib10] [10] 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 Proceedings of LICS 2022, pages 41:1–41:12. ACM, 2022. doi:10.1145/3531130.3533358.

[bib.bib11] [11] E. Grädel, N. Lücking, and M. Naaf. Semiring provenance for Büchi games: Strategy analysis with absorptive polynomials. Logical Methods in Computer Science, 20(1), 2024. doi:10.46298/lmcs-20(1:21)2024.

[bib.bib12] [12] E. Grädel and L. Mrkonjić. Elementary equivalence versus isomorphism in semiring semantics. In Proceedings of ICALP 2021, volume 198, pages 133:1–133:20, Dagstuhl, Germany, 2021. doi:10.4230/LIPIcs.ICALP.2021.133.

[bib.bib13] [13] E. Grädel and V. Tannen. Semiring provenance for first-order model checking, 2017. arXiv:1712.01980.

[bib.bib14] [14] 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.bib15] [15] 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. doi:10.1007/978-3-031-86319-6_21.

[bib.bib16] [16] T. Green, G. Karvounarakis, and V. Tannen. Provenance semirings. In Proceedings of PODS 2007, pages 31–40. ACM, 2007. doi:10.1145/1265530.1265535.

[bib.bib17] [17] T. Green and V. Tannen. The semiring framework for database provenance. In Proceedings of PODS 2017, pages 93–99. ACM, 2017. doi:10.1145/3034786.3056125.

[bib.bib18] [18] L. Mrkonjić. Semiring Semantics: Algebraic Foundations, Model Theory, and Strategy Analysis. PhD thesis, RWTH Aachen University, 2025. doi:10.18154/RWTH-2025-03940.

[bib.bib19] [19] M. Naaf. Logic, Semirings, and Fixed Points. PhD thesis, RWTH Aachen University, 2024. doi:10.18154/RWTH-2024-10804.

[bib.bib20] [20] George N. Raney. A subdirect-union representation for completely distributive complete lattices. Proceedings of the American Mathematical Society, 4(4):518–522, 1953. doi:10.1090/S0002-9939-1953-0058568-4.

[bib.bib21] [21] P. Rothmaler. Introduction to Model Theory. CRC Press, 2018. doi:10.1201/9781315273822.