Finite Axiomatizability by Disjunctive Existential Rules (Extended Abstract)

1 Introduction

Model theory is the study of the interaction between sentences in some logical formalism and their models, that is, structures that satisfy the sentences. There are two directions in this interaction: from syntax to semantics and from semantics to syntax. The first direction aims to identify properties that are satisfied by all models of sentences having common syntactic features, i.e., the syntax of a logical formalism is introduced first and then the properties of the mathematical structures that satisfy sentences of that formalism are explored. The second direction aims to characterize sentences in terms of their model-theoretic properties, i.e., given a set of properties, the goal is to determine whether or not these properties characterize some logical formalism. In general, establishing results in the second direction is much harder than establishing results in the first. In other words, obtaining model-theoretic characterizations of logical formalisms is a far greater challenge than identifying properties enjoyed by all models of sentences from a certain formalism.

In this work, we are concerned with the second direction of the interaction between logical sentences and their models. More precisely, we are interested in model-theoretic results of the following form. For a logical formalism L, given a collection C of structures, the following are equivalent:

1. There exists a finite set Φ of sentences from L such that C is precisely the set of models of Φ, in which case we say that C is finitely axiomatizable by L. 1

∗This short paper is based on a conference paper appeared in the 22nd International Conference on Principles of Knowledge Representation and Reasoning (KR 2025).

1 Note that one can also talk about the notion of axiomatizability by L, where the set of sentences Φ from L might be infinite.

1. C enjoys certain model-theoretic properties.

Such results are welcome as they pinpoint the absolute expressive power of a logical formalism in terms of insightful model-theoretic properties. In other words, they equip uswith model-theoretic tools that allow us to prove or disprove that a set of sentences Φ from some logical formalism can be equivalently rewritten as a finite set of sentences from L. Indeed, by showing that the collection of models of Φ enjoy the properties listed in item (2), then Φ is logically equivalent to a finite set Φ′ of sentences from L; otherwise, we can safely conclude that such Φ′ does not exist.

Characterizations for Rule-based Formalisms. Interesting results of the above form have been established for rulebased formalisms, expressed in suitable fragments of firstorder logic, that have been used in numerous areas of central importance to databases and knowledge representation and reasoning. A prominent such formalism is that of existential rules (a.k.a. tuple-generating dependencies in the database literature) that are first-order sentences

where ϕ and ψ are conjunctions of atoms. Existential rules have been originally introduced as a framework for database constraints [Abiteboul et al., 1995]. Later on, they have been deployed in the study of data exchange [Fagin et al., 2005] and data integration [Lenzerini, 2002]. More recently, they have been used for modeling ontologies intended for dataintensive tasks such as ontology-based data access [Cal`ı et al., 2010; Mugnier and Thomazo, 2014].

Early characterizations of axiomatizability and finite axiomatizability by full existential rules (i.e., existential rules without existentially quantified variables) have been established by Makowsky and Vardi in the 1980s [Makowsky and Vardi, 1986]. Moreover, ten Cate and Kolaitis obtained analogous characterizations for source-to-target existential rules, which have been used to formalize data exchange between a source schema and a target schema [ten Cate and Kolaitis, 2009]. More recently, Console, Kolaitis and Pieris characterized finite axiomatizability by arbitrary existential rules [Console et al., 2021].

To the best of our knowledge, the above results are the only known results in the literature concerning characterizations of axiomatizability and finite axiomatizability by rule-based formalisms. Having said that, let us stress that several preservation results can be found in the literature. When the target is a preservation result, one considers two formalisms L and L′ , where L′ is typically a proper fragment of L, and the goal is to obtain characterizations of the following form: a set Φ of sentences from L is logically equivalent to a set of sentences from L′ iff the models of Φ enjoy certain modeltheoretic properties. A prototypical example of such a result is the Łos-Tarski Theorem [Chang and Keisler, 1992], which states that a set Φ of first-order sentences is equivalent to a set of universal first-order sentences iff the collection of models of Φ is closed under substructures. Such results for rule-based formalisms have been obtained in the context of description logics by Lutz et al. [Lutz et al., 2011] and of existential rules by Zhang et al. [Zhang et al., 2020].

Disjunctive Existential Rules. The extension of existential rules with the feature of disjunction in the right-hand side of the implication, originally proposed in [Deutsch and Tannen, 2003], leads to the central rule-based formalism of disjunctive existential rules that are first-order sentences of the form

Disjunctive existential rules have also found numerous applications in several areas such as data exchange [Fagin et al., 2008], expressive database query languages [Eiter et al., 1997], and knowledge representation and reasoning [Alviano et al., 2012], to name a few. Despite the characterizations concerning existential rules discussed above, similar characterizations for disjunctive existential rules have remained largely unexplored so far. The present work changes this state of affairs by focusing on finite axiomatizability.

We establish that a collection of structures C is finitely axiomatizable by disjunctive existential rules with at most n universally quantified variables, at most m existentially quantified variables, and at most ℓ disjuncts iff C is critical, closed under repairable direct products, and diagrammatically (n,m, ℓ)-compatible; in fact, this has been originally shown in [Calautti et al., 2025]. Criticality is a standard property, which has been used in several works (see, e.g., [Console et al., 2021]), and states that, for each κ > 0, C contains a structure Iκ with κ domain elements, and each relation of Iκ contains all the tuples that can be formed using those κ elements. Closure under repairable direct products is obtained by carefully refining the standard property of closure under direct products since it is easy to show that disjunctive existential rules violate closure under direct products. Finally, diagrammatic (n,m, ℓ)-compatibility, which is the main innovation of this work, relies on the method of diagrams.

2 Preliminaries

Let C and V be disjoint countably infinite sets of constants and variables, respectively. For an integer n > 0, we may write [n] for the set of integers {1, . . . , n}.

Relational Structures. A (relational) schema S is a finite set of relation symbols (or predicates) with positive arity; we write ar(R) for the arity of the relation symbol R. A (relational) structure I over a schema S = {R1, . . . ,Rn}, or Sstructure, is a tuple (dom(I),RI1 , . . . ,RIn ), where dom(I) ⊆ C is a (finite or infinite) domain and RI1 , . . . , RIn are relations over dom(I), i.e., RI i ⊆ dom(I)ar(Ri) for each i ∈ [n]. We say that I is a finite structure if dom(I) is finite. A fact of I is an expression of the form Ri(¯ c), where ¯ c ∈ RI i , and we denote by facts(I) the set of facts of I. The active domain of a structure I, denoted adom(I), is the set of elements of dom(I) that occur in at least one fact of I. For an Sstructure J = (dom(J),RJ 1 , . . . ,RJn ), we write J ⊆ I if facts(J) ⊆ facts(I). We say that J is a substrucure of I, denoted J ⪯ I, if dom(J) ⊆ dom(I) and RJ = RI |dom(J) for each R ∈ S with RI |dom(J) being the restriction of RI over dom(J), i.e., the relation {¯ c ∈ RI | ¯ c ∈ dom(J)ar(R)}. Note that J ⪯ I implies J ⊆ I, but the other direction does not necessarily hold. A homomorphism from I to J is a function h : dom(I) → dom(J) such that, for each i ∈ [n], ¯ c = (c1, . . . , cm) ∈ RI i implies h(¯ c) = (h(c1), . . . , h(cm)) ∈ RJ i . We write h : I → J for the fact that h is a homomorphism from I to J. Let h(facts(I)) be the set {R(h(¯ c)) | R(¯ c) ∈ facts(I)}. Finally, we say that I and J are isomorphic, written I ≃ J, if there is a bijective homomorphism from I to J such that h-1 : J → I.

Extended Structures. An extended schema is a pair (S,F), where S = {R1, . . . ,Rn} is a relational schema and F = {f1, . . . , fm} is a set of 0-ary function symbols. A structure I over (S,F) is a tuple (dom(I),RI1 , . . . ,RIn , f I 1 , . . . , f Im), where dom(I) ⊆ C, RI1 , . . . ,RIn are relations over dom(I), and f I 1 , . . . , f Im are constants of dom(I). Given a relational schema S and a finite non-empty set C = {c1, . . . , cm} of constants from C, we denote by S[C] the extended schema (S, {fc1 , . . . , fcm }). Furthermore, given an S-structure I = (dom(I),RI1 , . . . ,RIn ), we denote by I[C] the structure over S[C] defined as (dom(I) ∪ C,RI1 , . . . ,RIn , f I c1 , . . . , f I cm ), where f I cj = cj for each j ∈ [m]. 2

By abuse of notation, we may write down first-order formulas that mention a constant c ∈ C, which is actually the 0ary function symbol fc. For example, ∃x(R(c, x, d) ∧ ¬(x = d)), where c, d ∈ C and x ∈ V, is essentially the sentence ∃x(R(fc, x, fd) ∧ ¬(x = fd)) over the extended schema ({R}, {fc, fd}). Now, by abuse of terminology, given a structure I over a schema S and a first-order sentence Φ that mentions relation symbols of S and constants (not necessarily from dom(I)) of C, we may say that I satisfies Φ, denoted I |= Φ. With C ⊆ C being the set of constants occurring in Φ, I |= Φ essentially denotes the fact that I[C] |= Φ, that is, the structure I[C] over the extended schema S[C] satisfies Φ under the standard first-order semantics.

Disjunctive Existential Rules. An atom over a schema S is an expression of the form R(¯ v), where R ∈ S and ¯ v is an ar(R)-tuple of variables from V. A disjunctive existential rule (dexr) σ over a schema S is a constant-free sentence

2 The additional notions defined above for relational structures (such as subset, substructure, homomorphism, and isomorphism) are not needed in the paper for structures over extended schemas.

where k > 0, ¯x, ¯ y, ¯x1, . . . , ¯xk, ¯ z1, . . . , ¯ zk are tuples of variables of V, the variables of ¯xi occur in ¯x for i ∈ [k], each variable of ¯x occurs in ¯xi for some i ∈ [k], ϕ(¯x, ¯ y) is a (possibly empty) conjunction of atoms over S, and ψi(¯xi, ¯ zi) is a non-empty conjunction of atoms over S for each i ∈ [k]. For brevity, we write σ as ϕ(¯x, ¯ y) → ∨ki=1 ∃¯ zi ψi(¯xi, ¯ zi) and use comma instead of ∧ for joining atoms. When ϕ(¯x, ¯ y) is empty, σ is essentially the sentence ∨ki=1 ∃¯ zi ψi(¯ zi). We refer to ϕ(¯x, ¯ y) and ∨ki=1 ψi(¯xi, ¯ zi) as the body and head of σ, denoted body(σ) and head(σ), respectively. By abuse of notation, we may treat a tuple of variables as a set of variables and a conjunction of atoms as a set of atoms. Assuming that ϕ(¯x, ¯ y) is non-empty, an S-structure I satisfies σ if the following holds: whenever there exists a function h : ¯x ∪ ¯ y → dom(I) such that h(ϕ(¯x, ¯ y)) ⊆ facts(I) (as usual, we write h(ϕ(¯x, ¯ y)) for the set {R(h(¯ v)) | R(¯ v) ∈ ϕ(¯x, ¯ y)}), then there exists an integer i ∈ [k] and an extension h′ of h such that h′ (ψi(¯xi, ¯ zi)) ⊆ facts(I). When ϕ(¯x, ¯ y) is empty, an S-structure I satisfies σ if there exists i ∈ [k] and a function h : ¯ zi → dom(I) such that h(ψi(¯ zi)) ⊆ facts(I). We write I |= σ for the fact that I satisfies σ. The S-structure I satisfies a set Σ of dexrs over S, written I |= Σ, in which case we say that I is a model of Σ, if I |= σ for each σ ∈ Σ

Finite Axiomatizability. Let C be a collection of structures over a schema S. We say that C is finitely axiomatizable by dexrs if there exists a finite set Σ of dexrs over S such that I ∈ C iff I |= Σ, that is, C is precisely the set of models of Σ. Henceforth, since dexrs cannot distinguish isomorphic structures, we implicitly assume that collections C of structures are closed under isomorphisms, i.e., if I ∈ C and J is a structure such that I ≃ J, then J ∈ C.

3 Finite Axiomatizability by Disjunctive Existential Rules

We proceed to characterize when a collection C of structures is finitely axiomatizable by dexrs. To this end, we introduce three model-theoretic properties of collections of structures, that is, criticality, closure under repairable direct products, and diagrammatic compatibility, and then discuss that they suffice for the desired characterization of finitely axiomatizable by dexrs. Fix an arbitrary schema S = {R1, . . . , Rr}.

3.1 Criticality

An S-structure I = (dom(I),RI1 , . . . ,RIr ) is κ-critical, for κ > 0, if |dom(I)| = κ and RI i = dom(I)ar(Ri) for each i ∈ [r]. We can now lift criticality to collections of structures. Definition 1. A collection C of S-structures is κ-critical, for κ > 0, if it contains a κ-critical S-structure. We further say that C is critical if it is κ-critical for each κ > 0.

It is easy to show the following lemma:

Lemma 2. A collection C of structures that is finitely axiomatizable by dexrs is critical.

3.2 Closure Under Repairable Direct Products

Consider two S-structures I = (dom(I),RI1 , . . . ,RIr ) and J = (dom(J),RJ 1 , . . . , RJ r ). Their direct product, denoted I ⊗ J, is the S-structure K = (dom(K),RK 1 , . . . ,RK r ), where dom(K) = dom(I) × dom(J) and

for each i ∈ [r]. A collection of structures C is closed under direct products if, for every I, J ∈ C, the direct product of I and J belongs to C. Closure under direct products is a well-known property that has been extensively used in model theory. However, it is not appropriate towards a characterization of finite axiomatizability by dexrs.

Example 1. Consider the set Σ consisting of the single dexr

and the structures I1 and I2 with facts(I1) = {R(a), S(a)} and facts(I2) = {R(a), T(a)}, and thus, facts(I1 ⊗ I2) = {R((aa))}. Clearly, I1 |= Σ and I2 |= Σ, but I1 ⊗I2 ̸|= Σ.

The above example essentially tells us that a collection of structures that is finitely axiomatizable by dexrs is not necessarily closed under direct products, and thus, we need to revisit the standard notion of direct product. To this end, we define the function πK : dom(K) → dom(I) as follows: for every (aI, aJ) ∈ dom(K), πK((aI, aJ)) = aI. It is clear that πK is a homomorphism from K to I, which we call the projective homomorphism for K. Now, a repairable direct product of the S-structures I and J is an S-structure L such that (1) I ⊗ J ⊆ L, and (2) there exists an extension h of πK that is a homomorphism from L to I. We now define the following novel model-theoretic property:

Definition 3. A collection C of S-structures is closed under repairable direct products if, for every two S-structures I, J ∈ C, there exists an S-structure in C that is a repairable direct product of I and J.

Coming back to Example 1, it is easy to see that the structure L with facts(L) = {R((aa)), S((aa))} is a repairable direct product of I1 and I2; indeed, I1 ⊗ I2 ⊆ L and πI1⊗I2 is a homomorphism from L to I1. We can show the following:

Lemma 4. A collection C of structures that is finitely axiomatizable by dexrs is closed under repairable direct products.

3.3 Diagrammatic Compatibility

We now introduce our new property of collections of structures, which in turn relies on the notion of relative diagram of a finite structure. We first introduce relative diagrams and then define the new model-theoretic property of interest.

Relative Diagrams. Consider a structure I over a schema S and a finite structure K ⊆ I with dom(K) = adom(K). We are interested in the so-called (m, ℓ)-diagrams of K relative to I for integers m, ℓ ≥ 0, which we define below. To this end, let AK,m be the set of all atomic formulas of the form R(¯u) that can be formed using predicates from S, constants from dom(K), and m distinct variables y1, . . . , ym from V, i.e., R ∈ S and ¯u ∈ (dom(K) ∪ {y1, . . . , ym})ar(R) . Furthermore, let CK,m be the set of all conjunctions of atomic formulas from AK,m. Observe that both AK,m and CK,m are finite sets since dom(K) is finite. Let

which is clearly finite since CK,m is finite. For a set of formulas G ⊆ N IK,m, the G-diagram of K relative to I, denoted ∆IK,G, is defined as the first-order sentence

Note that Ψ1 and Ψ2 might be empty (i.e., they have no conjuncts). In particular, Ψ1 is empty if K is empty, whereas Ψ2 is empty if I is 1-critical, which means that |dom(K)| = 1 and I |= ∃¯ y γ(¯ y) for each γ(¯ y) ∈ CK,m, and thus, G = ∅. When Ψ1 and Ψ2 are empty, ∆IK,G is the truth value true, i.e., a tautology. Intuitively, ∆IK,G provides a witness for the fact that a dexr, whose head-disjuncts belong to G, is violated by the structure I due to the structure K ⊆ I.

Definition 5. Consider an S-structure I and a finite structure K ⊆ I with dom(K) = adom(K). An (m, ℓ)-diagram of K relative to I, for m, ℓ ≥ 0, is a G-diagram of K relative to I, where G ⊆ N IK,m and |G| ≤ ℓ.

Let ΦIK,G(¯x) be the formula obtained from ∆IK,G by replacing each constant c ∈ dom(K) with a new variable xc ∈ V \ {y1, . . . , ym}. If ∆IK,G is empty, then ΦIK,G is the truth value true, i.e., a tautology.

The Property. Consider a collection C of structures over a schema S and an S-structure I. For n,m, ℓ ≥ 0, we say that C is diagrammatically (n,m, ℓ)-compatible with I if, for every K ⪯ I with dom(K) = adom(K) and |dom(K)| ≤ n, and every (m, ℓ)-diagram ∆IK,G of K relative to I, where G ⊆ N IK,m, there is J ∈ C such that J |= ∆IK,G. Roughly, this states that no matter how a dexr σ with a bounded number of variables (at most n universally quantified and at most m existentially quantified variables) and a bounded number of disjuncts in its head (at most ℓ disjuncts) is violated by the structure I, there is always a structure J ∈ C that violates σ for the same reason. The new property of interest follows.

Definition 6. A collection C of S-structures is diagrammatically (n,m, ℓ)-compatible, for n,m, ℓ ≥ 0, if, for every S-structure I, the following holds: C is diagrammatically (n,m, ℓ)-compatible with I implies I ∈ C.

The next lemma establishes that collections of structures that are finitely axiomatizable by dexrs are diagrammatically compatible. Actually, it shows a stronger claim since it relates the integers n,m and ℓ that witness diagrammatic (n, m, ℓ)-compatibility with the number of universally quantified variables, existentially quantified variables, and headdisjuncts, respectively, occurring in the dexrs. A dexr is called (n,m, ℓ)-dexr, for n,m ≥ 0, with n +m > 0, and ℓ > 0, if it mentions at most n universally quantified variables in its body, at most m existentially quantified variables in each disjunct of its head, and at most ℓ disjuncts in its head. Note that we require n+m > 0 since, by definition, a dexr has at least one variable that is either universally or existentially quantified. Furthermore, we require ℓ > 0 since, by definition, a dexr has at least one disjunct in its head.

Lemma 7. For n,m ≥ 0, with n + m > 0, and ℓ > 0, every collection C of structures that is finitely axiomatizable by (n,m, ℓ)-dexrs is diagrammatically (n,m, ℓ)-compatible.

3.4 The Characterization

We are now ready to present the characterization of finite axiomatizability by dexrs.

Theorem 8. For a collection C of structures and n,m ≥ 0, with n +m > 0, and ℓ > 0, the following are equivalent:

1. C is finitely axiomatizable by (n,m, ℓ)-dexrs.
2. C is critical, closed under repairable direct products, and diagrammatically (n, m, ℓ)-compatible.

The direction (1) ⇒ (2) follows from Lemmas 2, 4 and 7. For (2) ⇒ (1), consider a collection C of structures over a schema S that is critical, closed under repairable direct products, and diagrammatically (n,m, ℓ)-compatible for integers n,m ≥ 0, with n +m > 0, and ℓ > 0. We show that C is finitely axiomatizable by (n,m, ℓ)-dexrs in three steps:

1. We first define a finite set Σ∨ of disjunctive dependencies over S, which extend dexrs by allowing equality formulas over the universally quantified variables as disjuncts, with at most n universally quantified variables, at most m existentially quantified variables, and at most ℓ disjuncts that are a conjunction of atoms (i.e., not an equality formula), such that, for every S-structure I, I ∈ C iff I |= Σ∨. This exploits the fact that C is 1critical (this follows from the fact that C is critical) and diagrammatically (n, m, ℓ)-compatible.
2. We then show that there is a finite set Σ∃,= of (n,m, ℓ)- dexrs and disjunctive equality rules (i.e., disjunctive dependencies with only equality formulas as disjuncts) with at most n universally quantified variables over S such that Σ∨ ≡ Σ∃,=; in fact, Σ∃,= is the set of dexrs and disjunctive equality rules occurring in Σ∨. This exploits closure under repairable direct products.
3. We finally argue that Σ∃,= consists only of dexrs, which implies that C is finitely axiomatizable by (n,m, ℓ)- dexrs. This exploits the fact that C is critical.

4 Further Results

Results analogous to Theorem 8 have been also established for the two main members of the guarded family of dexrs:

• A dexr is linear if it has at most one atom in its body.
• A dexr is guarded if its body is empty or has an atom that mentions all the universally quantified variables.

To achieve the desired characterizations for the above classes of dexrs, we simply need to replace the diagrammatic compatibility property in Theorem 8 with a refined version of it that takes into account the syntactic property underlying linear and guarded dexrs.