Doubly Strongly First Order Dependencies

Abstract

Team Semantics is a generalization of Tarskian Semantics that can be used to add to First Order Logic atoms and connectives expressing dependencies between the possible values of variables. Some of the resulting logics are more expressive than First Order Logic, while others are not. I characterize the (relativizable) atoms and families of atoms that do not increase the expressive power of First Order Logic when they and their complements are added to it, separately or jointly.

1 Introduction

Team Semantics generalizes Tarskian Semantics for First Order Logic by defining satisfaction with respect to sets of assignments (called Teams) rather than with respect to single assignments. This semantics arises naturally from the analysis of the game theoretic semantics of First Order Logic and its extensions: in brief, a team represents a set of possible game states (= variable assignments) that can be played at some subformula, and a team satisfies a subformula if the existential player has a¹ strategy that is winning for the corresponding subgame for every starting assignment in the team. This approach works equally well for extensions of First Order Logic whose game-theoretic semantics yield imperfect information games, as is the case for Independence-Friendly Logic [14, 15, 22] which was the reason for the original development of Team Semantics (then called “Trump Semantics”) in [16].

Jouko Väänänen [25] observed that a logic roughly equivalent to Independence-Friendly Logic, but with more convenient formal properties (for example locality, in the sense that the interpretation of a formula in a team depends only on the restriction of the team to the free variables of the formula), can be obtained by adding to First Order Logic, in place of the so-called slashed quantifiers (“there exists a y, chosen independently from x, such that ...”) of Independence-Friendly Logic, functional dependence atoms $=\!\!(x; y)$ that state that the values of y are determined by those of x. The resulting logic, called Dependence Logic, has been the subject of a considerable amount of research that cannot be summarized here (for an up-to-date introduction, we refer the reader to [9]). It was soon noticed that Team Semantics could also be used to extend First Order Logic via other atoms (see e.g. [3, 12]) or connectives (like the “contradictory negation” of [26], the “intuitionistic implication” of [1], or the generalized quantifiers of [2]) that have no direct analogues in Tarskian Semantics as their definitions likewise involve possible interactions between different assignments. Other Team Semantics-based logics use families of connectives different from the ones arising directly from the Game-Theoretic Semantics of First Order Logic: of particular interest in this context is the FOT logic of [19], that relates to ordinary First Order Logic not through Game Theoretic Semantics but on the level of team definability, in the sense that a family of teams is defined by a FOT formula if and only if the corresponding family of relations is first order definable and every sentence of $\mathbf{FOT}$ is equivalent to some first order sentence.²

Team Semantics – aside from its applications and connections with other areas, which we will not discuss here – can thus be seen as a generalization of Tarskian Semantics that allows for the construction of new kinds of extensions and fragments of First Order Logic; and while some of these extensions have been studied in some depth by now (see e.g. [18, 21] for the contradictory negation, [27] for the intuitionistic implications, or [3, 10, 11, 13, 23] for database-theoretic atoms), not much is yet known regarding the general properties of the extensions of First Order Logic obtainable through Team Semantics.

This work is a partial answer to the following question: which extensions of First Order Logic based on Team Semantics are genuinely more expressive than First Order Logic itself, and which ones instead can only specify properties that were already first order definable? This question is the obvious starting point for a classification of Team Semantics-based extensions of First Order Logic; and yet, at the moment only some very limited answers (see [6, 7]) are known.

The main result of this work is a full characterization – aside from the technical condition of relativizability, that most dependencies of interest satisfy – of the dependencies that are doubly strongly first order in the sense that both they and their complements can be added (jointly or separately) to First Order Logic with Team Semantics without increasing their expressive power. This may be regarded as another step towards the classification of the expressive capabilities – and computational costs – of logics based on Team Semantics, a topic of both practical (especially given the applications of Team Semantics to knowledge representation and database theory, for which we refer the reader to [9]) and theoretical interest.

2 Preliminaries

2.1 Team Semantics

Definition 1 (Team)

Let $\mathfrak M$ be a first order model with domain $\mathbf{Dom} (\mathfrak M) = M$ and let V be a finite set of variables. Then a team X over $\mathfrak M$ with domain $\mathbf{Dom} (X) = V$ is a set of variable assignments $s: V \rightarrow M$. Given such a team and some tuple of variables $\vec v = v_1 \ldots v_k \in V^k$, we will write $X(\vec v)$ for the $|\vec v|$-ary relation $\{s(\vec v) : s \in X\} \subseteq M^{|v|}$, where $s(\vec v)$ is the tuple $s(v_1) \ldots s(v_k)$.

Definition 2 (Team Semantics for First Order Logic)

Let $\mathfrak M$ be a first order model, let $\phi$ be a first order formula in Negation Normal Form³ over the signature of $\mathfrak M$, and let X be a team over $\mathfrak M$ whose domain contains the free variables of $\phi$. Then we say that X satisfies $\phi$ in $\mathfrak M$, and we write $\mathfrak M\models _X \phi$, if this follows from the following rules:

• TS-lit: If $\phi$ is a first order literal, $\mathfrak M\models _X \phi$ if and only if, for all assignments $s \in X$, $\mathfrak M\models _s \phi$ in the usual sense of Tarskian Semantics;

• TS-$\vee$: $\mathfrak M\models _X \phi _1 \vee \phi _2$ if and only if $X = Y \cup Z$ for two $Y, Z \subseteq X$ such that $\mathfrak M\models _Y \phi _1$ and $\mathfrak M\models _Z \phi _2$;

• TS-$\wedge$: $\mathfrak M\models _X \phi _1 \wedge \phi _2$ if and only if $\mathfrak M\models _X \phi _1$ and $\mathfrak M\models _X \phi _2$;

• TS-$\exists$: $\mathfrak M\models _X \exists v \psi$ if and only if there exists some function⁴ $H: X \rightarrow \mathcal P(M) \backslash \{\emptyset \}$ such that $\mathfrak M\models _{X[H/v]} \psi$, where $X[H/v] = \{s[m/v] : s \in X, m \in H(s)\}$;

• TS-$\forall$: $\mathfrak M\models _X \forall v \psi$ if and only if $\mathfrak M\models _{X[M/v]} \psi$, where $X[M/v] = \{s[m/v] : s \in X, m \in M\}$.

A sentence $\phi$ is true in a model $\mathfrak M$ if and only if $\mathfrak M\models _{\{\emptyset \}} \phi$, where $\{\emptyset \}$ is the team containing only the empty assignment. In that case, we write that $\mathfrak M\models \phi$.

Over First Order Logic, Team Semantics reduces to Tarskian Semantics:

Proposition 1

([25], Corollary 3.32) Let $\mathfrak M$ be a first order model, let $\phi$ be a first order formula in Negation Normal Form over the signature of $\mathfrak M$, and let X be a team over $\mathfrak M$ whose domain contains the free variables of $\phi$. Then $\mathfrak M\models _X \phi$ if and only if, for all $s \in X$, $\mathfrak M\models _s \phi$ in the sense of Tarskian Semantics.

In particular, if $\phi$ is a sentence, $\mathfrak M\models \phi$ in the sense of Team Semantics if and only if $\mathfrak M\models \phi$ in the sense of Tarskian Semantics.

Nonetheless, Team Semantics makes it possible to extend First Order Logic via new types of atoms specifying collective properties of (that is to say, dependencies between) the assignments in a team. The earliest and arguably most important atoms studied in this context are the functional dependence atoms [25]

• TS-dep: If $\vec x$ and $\vec y$ are tuples of variables, $\mathfrak M\models _X =\!\!(\vec x; \vec y)$ if and only if, for all $s, s' \in X$, if $s(\vec x) = s'(\vec x)$ then $s(\vec y) = s'(\vec y)$.

This rule corresponds precisely to the database-theoretic notion of functional dependence; and it was soon recognized that other dependency notions may also be studied in the same context, such as independence atoms [12]

• TS-ind: $\mathfrak M\models _X \vec x \bot _{\vec y} \vec z$ if and only if for any two $s, s' \in X$ with $s(\vec y) = s'(\vec y)$ there exists some $s'' \in X$ with $s''(\vec x \vec y) = s(\vec x \vec y)$ and $s''(\vec y \vec z) = s'(\vec y \vec z)$

which as per [2] have a close connection with database-theoretic embedded multivalued dependencies, inclusion dependencies [3, 11, 13]

• TS-inc: $\mathfrak M\models _X \vec x \subseteq \vec y$ if and only if $X(\vec x) \subseteq X(\vec y)$

and exclusion dependencies [3, 24]

• TS-exc: $\mathfrak M\models _X \vec x | \vec y$ if and only if $X(\vec x) \cap X(\vec y) = \emptyset$.

But what is, in general, a dependency? The following definition is from [20]:

Definition 3 (Generalized Dependency)

A k-ary generalized dependency is a class $\mathbf{D}$, closed under isomorphisms, of models $\mathfrak M= (M, R)$ over the signature $\{R\}$, where R is a k-ary relation symbol. $\mathbf{D}$ corresponds to the rule

• TS-$\mathbf{D}$: $\mathfrak M\models _X \mathbf{D}\vec x$ if and only if $(\mathbf{Dom} (\mathfrak M), R:=X(\vec x)) \in \mathbf{D}$

where $\vec x$ is any tuple of k variables and $(\mathbf{Dom} (\mathfrak M), R:=X(\vec x))$ is the model with the same domain $\mathbf{Dom} (\mathfrak M)$ of $\mathfrak M$ and with signature $\{R\}$, where R is interpreted as $R^{\mathfrak M} = X(\vec x) = \{s(\vec x) : s \in X\}$.

Definition 4

($\mathbf {FO}(\mathcal D)$). Let $\mathcal D = \{\mathbf{D}_1, \mathbf{D}_2, \ldots \}$ be a set of generalized dependencies. Then $\mathbf {FO}(\mathcal D)$ is the logic obtained by taking First Order Logic (with Team Semantics) $\mathbf {FO}$ and adding to it all the generalized dependency atoms $\mathbf{D}\in \mathcal D$.

An important class of generalized dependencies is that of the first order ones:

Definition 5 (First Order Generalized Dependencies)

A k-ary generalized dependency $\mathbf{D}$ is first order if there exists some first order sentence $\mathbf{D}(R)$, over the signature $\{R\}$ where R is a k-ary relation symbol, such that $\mathbf{D}= \{(M, R): (M, R) \models \mathbf{D}(R)\}$.

If $\mathbf{D}$ is a first order generalized dependency, the rule TS-$\mathbf{D}$ is equivalent to

• TS-$\mathbf{D}$-FO: $\mathfrak M\models _X \mathbf{D}\vec x$ if and only if $(\mathbf{Dom} (\mathfrak M), R:=X(\vec x)) \models \mathbf{D}(R)$.

Functional dependence atoms, independence atoms, inclusion atoms, and exclusion atoms are all first order; but the logics obtained by adding them to First Order Logic are more expressive than First Order Logic itself. This differs from the case of generalized quantifiers in Tarskian Semantics, in which if a quantifier $\mathbf{Q}$ is first order definable then adding it to First Order Logic yields nothing new. The intriguing phenomenon of first order dependencies increasing the expressiveness of First Order Logic is a consequence of the higher order character of Team Semantics, and in particular to the existential second order quantification implicit in the rules TS-$\vee$ and TS-$\exists$,⁵ and it raises immediately a natural (and still open) problem: can we identify the dependencies (or the families of dependencies, or even more in general the families of connectives and dependencies) that do not increase the expressive power of First Order Logic?

2.2 Strongly First Order Dependencies

In this section, we will recall some partial results related to the problem of characterizing the dependencies that are “safe” to add to First Order Logic:

Definition 6 (Strongly First Order Dependencies)

A generalized dependency $\mathbf{D}$ is strongly first order if and only if $\mathbf {FO}(\mathbf{D}) \equiv \mathbf {FO}$,⁶ i.e., if and only if every sentence of $\mathbf {FO}(\mathbf{D})$ is equivalent to some first order sentence. Likewise, a family of dependencies $\mathcal D$ is strongly first order if and only if $\mathbf {FO}(\mathcal D) \equiv \mathbf {FO}$.

If $\mathbf{D}$ is strongly first order then it is first order in the sense of Definition 5: indeed, it is definable via the first order sentence equivalent to the $\mathbf {FO}(\mathbf{D})$ sentence $\forall \vec w (\lnot R \vec w \vee (R \vec w \wedge \mathbf{D}\vec w))$. However, as mentioned at the end of the previous section, not all first order dependencies are strongly first order.

A notion closely related to strong first-orderness is that of safety:

Definition 7 (Safe Dependencies)

Let $\mathbf{D}$ be a generalized dependency and let $\mathcal E$ be a family of dependencies. Then $\mathbf{D}$ is safe for $\mathcal E$ if $\mathbf {FO}(\mathbf{D}, \mathcal E) \equiv \mathbf {FO}(\mathcal E)$, that is, if every sentence of $\mathbf {FO}(\mathbf{D}, \mathcal E)$ is equivalent to some sentence of $\mathbf {FO}(\mathcal E)$.

If $\mathcal D$ and $\mathcal E$ are families of dependencies, $\mathcal D$ is safe for $\mathcal E$ if $\mathbf {FO}(\mathcal D, \mathcal E) \equiv \mathbf {FO}(\mathcal E)$.

Clearly, a dependency $\mathbf{D}$ or a family of dependencies $\mathcal D$ is strongly first order if and only if it is safe for $\emptyset$: in this sense, safety is a generalization of strong first-orderness. However, as shown in ([8], Theorem 53), strongly first order dependencies are not necessarily safe for all families of dependencies.

An example of strongly first order dependencies is given by the constancy atoms ([3], Corollary 3.13)

• TS-Const: $\mathfrak M\models _X =\!\!(\vec x)$ if and only if for all $s, s' \in X$ it holds that $s(\vec x) = s'(\vec x)$.

A more general strongly first order family of generalized dependencies is given by first order upwards closed dependencies, that are strongly first order even taken together with each other and with the constancy atom:

Definition 8 (Upwards and Downwards Closed Dependencies)

A k-ary dependency $\mathbf{D}$ is upwards closed if and only if $(M, R) \in \mathbf{D}$ implies $(M, R') \in \mathbf{D}$ for all k-ary relations $R' \supseteq R$ over M. We write $\mathcal {UC}$ for the family of upwards closed, first order dependencies. Likewise, we write $\mathcal {DC}$ for the family of all downwards closed first order dependencies, defined analogously.

$\mathcal {DC}$ is not strongly first order: for example, functional dependencies $=\!\!(\vec x; \vec y)$ are first order and downwards closed, but $\mathbf {FO}(=\!\!(\cdot ;\cdot ))$ is as expressive as Existential Second Order Logic ([25], Corollary 6.3). On the other hand,

Theorem 1

([4], Theorem 21). $\mathcal {UC} \cup \{=\!\!(\cdot )\}$ is strongly first order.

An upwards closed, first order generalized dependency atom that will be of some use is the totality atom $\mathbf{All} (\vec x)$, that says that $\vec x$ takes all possible values:

• TS-All: $\mathfrak M\models _X \mathbf{All} (\vec x)$ if and only if $X(\vec x) = \mathbf{Dom} (\mathfrak M)^{|\vec x|}$.

As shown in [8], totality is safe for any collection of dependencies:

Proposition 2

([8], Theorem 38). $\mathbf {FO}(\mathbf{All} , \mathcal D) \equiv \mathbf {FO}(\mathcal D)$ for any collection of dependencies $\mathcal D$.

Also of interest are the families $\mathcal D_0$ and $\mathcal D_1$ of 0-ary and unary first order dependencies. A 0-ary first order dependency atom $[\psi ] = \{M : M \models \psi \}$ is nothing but a family of models over the empty signature characterized by some first order sentence $\psi$, and $\mathfrak M\models _X [\psi ]$ if and only if $M \models \psi$ (that is to say, 0-ary dependencies do not “look” at the team X but only at the domain $\mathbf{Dom} (\mathfrak M) = M$). A unary dependency atom is instead a family of models (M, P) over the signature $\{P\}$, where P is a unary predicate, characterized by some first order sentence over the signature $\{P\}$. As shown in ([5], Proposition 9 and Theorems 9 and 10), both of these families are strongly first order.

The main result of [6] characterizes the strongly first order dependencies $\mathbf{D}$ that are downwards closed, have the empty team property and are relativizable:

Definition 9 (Empty Team Property)

A dependency $\mathbf{D}$ has the empty team property if $(M, \emptyset ) \in \mathbf{D}$ for all domains M.

Definition 10 (Relativization of a dependency; Relativizable Dependencies)

Let P be a unary predicate and let $\mathbf{D}$ be a k-ary generalized dependency. Then the relativization of $\mathbf{D}$ to P is the k-ary atom $\mathbf{D}^{(P)}$, whose semantics - for models $\mathfrak M$ whose signature contains the predicate P interpreted as $P^{\mathfrak M}$ - is

• TS-$\mathbf{D}^{(P)}$: $\mathfrak M\models _X \mathbf{D}^{(P)} \vec x$ if and only if $(P^{\mathfrak M}, X(\vec x)) \in \mathbf{D}$.

A dependency $\mathbf{D}$ is relativizable if every sentence of $\mathbf {FO}(\mathbf{D}^{(P)})$, i.e. of First Order Logic with Team Semantics augmented with the above rule, is equivalent to some sentence of $\mathbf {FO}(\mathbf{D})$. Likewise, a family of dependencies $\mathcal D$ is relativizable if $\mathbf {FO}(\mathcal D^{(P)}) \equiv \mathbf {FO}(\mathcal D)$, where $\mathcal D^{(P)} = \{\mathbf{D}^{(P)} : \mathbf{D}\in \mathcal D\}$.

As discussed in [6], non-relativizable generalized dependencies exist.⁷ However, the vast majority of the dependencies considered in the context of Team Semantics so far (and all the ones whose corresponding logics have been studied in some depth) are relativizable, and most are even universe-independent in the sense of [17] (in brief, $\mathbf{D}$ is universe-independent if the satisfaction of $\mathbf{D}\vec x$ in a team X and in a model $\mathfrak M$ does not depend on the existence in $\mathfrak M$ of elements that are not in $X(\vec x)$). $\mathbf{All}$ is not universe-independent, but it is still relativizable;⁸ and no strongly first order non-relativizable dependencies are currently known.

Theorem 2

([6], Theorem 4.5). Let $\mathbf{D}$ be a downwards closed, relativizable generalized dependency with the empty team property. Then $\mathbf{D}$ is strongly first order if and only if it is definable in $\mathbf {FO}(=\!\!(\cdot ))$.

The same notions of strong first-orderness and safety can also be applied to connectives. Three connectives of particular interest in Team Semantics are the Global (or Boolean) Disjunction $\phi _1 \sqcup \phi _2$, the Possibility Operator $\diamond \phi$ and the Contradictory Negation $\sim \!\!\phi$, corresponding to the rules

• TS-$\sqcup$: $\mathfrak M\models _X \phi _1 \sqcup \phi _2$ if and only if $\mathfrak M\models _X \phi _1$ or $\mathfrak M\models _X \phi _2$;

• TS-$\diamond$: $\mathfrak M\models _X \diamond \phi$ if and only if $\mathfrak M\models _Y \phi$ for some $Y \subseteq X$, $Y \not = \emptyset$;

• TS-$\sim$: $\mathfrak M\models _X \sim \!\!\phi$ if and only if $\mathfrak M\not \models _X \phi$.

As shown in [7], global disjunction is not safe for arbitrary dependencies, but it is safe for strongly first order dependencies.

Proposition 3

([7], Proposition 14). If $\mathcal D$ is a strongly first order family of dependencies then every sentence of $\mathbf {FO}(\sqcup , \mathcal D)$ (i.e. of First Order Logic with Team Semantics, plus global disjunctions and the atoms in $\mathcal D$) is equivalent to some sentence of $\mathbf {FO}$.

Instead $\diamond$ is safe for any collection of dependencies, in the sense that

Proposition 4

([8], Corollary 42). Let $\mathcal D$ be any family of generalized dependencies, not necessarily strongly first order. Then every sentence of $\mathbf {FO}(\diamond , \mathcal D)$ (i.e. of First Order Logic with Team Semantics, plus the possibility operator $\diamond$ and the atoms in $\mathcal D$) is equivalent to some sentence of $\mathbf {FO}(\mathcal D)$.

Differently from global disjunction and from the possibility operator, contradictory negation is extremely unsafe. Augmenting Dependence Logic $\mathbf {FO}(=\!\!(\cdot ; \cdot ))$ with contradictory negation yields Team Logic $\mathbf {FO}(\sim , =\!\!(\cdot ;\cdot ))$ [26], which is as expressive as Second Order Logic; and as observed in ([5], Corollary 2), even $\mathbf {FO}(\sim , =\!\!(\cdot ))$ is already equivalent to full Second Order Logic. On the other hand, $\sim$ is still “strongly first order”, in the sense that $\mathbf {FO}(\sim ) \equiv \mathbf {FO}$: this is mentioned in [5] as a consequence of ([5], Theorem 4), but it may be verified more simply by observing that if $\phi$ is first order then – as a consequence of Proposition 1 – $\sim \!\!\phi$ is logically equivalent to $\diamond (\lnot \phi )$, and then applying Proposition 4.

We end this section with two simple results that will be of some use:

Proposition 5

Let $\mathcal D$ be a strongly first order, relativizable collection of dependencies. Then every sentence of $\mathbf {FO}(\mathcal D, =\!\!(\cdot ))$ is equivalent to some sentence of $\mathbf {FO}$, and so is every sentence of $\mathbf {FO}(\mathcal D^{(P)}, =\!\!(\cdot ))$.

Proof (Sketch)

Given a sentence $\phi \in \mathbf {FO}(\mathcal D, =\!\!(\cdot ))$ [respectively $\mathbf {FO}(\mathcal D^{(P)}, =\!\!(\cdot ))$], replace every constancy atom $=\!\!(\vec x)$ with $\vec x = \vec d_{\vec x}$, where $\vec d_{\vec x}$ is a tuple of constant symbols (each variable corresponding to a unique distinct constant). The result will be in $\mathbf {FO}(\mathcal D)$ [respectively $\mathbf {FO}(\mathcal D^{(P)})$], and so it will be equivalent to some $\phi '(\vec d) \in \mathbf {FO}$, where $\vec d$ contains all new constants; and then $\phi$ will be equivalent to $\exists \vec w \phi '(\vec w)$ for some new tuple of variables $\vec w$.

Proposition 6

$\mathbf {FO}(\mathcal D_0, \sqcup , =\!\!(\cdot ), \mathbf{All} ) \equiv \mathbf {FO}$.

Proof

By Propositions 3 and 2, it is enough to show that $\mathbf {FO}(\mathcal D_0, =\!\!(\cdot )) \equiv \mathbf {FO}$. This follows from Proposition 5, since 0-ary dependencies are strongly first order.

2.3 Relations Definable over the Empty Signature

Finally, in this work we will need a couple of simple results – whose proofs we omit – about the relations that are definable via First Order Logic formulas:

Definition 11

Let $\mathfrak M$ be a first order model with domain M and let $\theta (\vec x, \vec y)$ be a first order formula. Then a $|\vec x|$-ary relation R over $\mathfrak M$ is defined by $\theta$ if there is a tuple of elements $\vec a \in M^{|\vec y|}$ such that $R = \{\vec m \in M^{|\vec x|} : \mathfrak M\models \theta (\vec m, \vec a)\}$.

Definition 12

A first order formula $\theta (\vec x, \vec y)$ is said to fix the identity type of $\vec y$ if, for every two variables $y_i, y_j \in \vec y$, $\models \forall \vec x \vec y (\theta (\vec x, \vec y) \rightarrow y_i = y_j)$ or $\models \forall \vec x \vec y(\theta (\vec x, \vec y) \rightarrow y_i \not = y_j)$.

Proposition 7

If a relation R over $\mathfrak M$ is defined by a formula $\theta (\vec x, \vec y)$, it is defined by some $\theta '(\vec x, \vec y)$ over the same signature that fixes the identity type of $\vec y$.

Proposition 8

If two nonempty relations R and S over the same model $\mathfrak M$ with domain $\mathbf{Dom} (\mathfrak M) = M$ are defined by the same formula $\theta (\vec x, \vec y)$ over the empty signature and $\theta$ fixes the identity type of $\vec y$ then there is a bijection $\mathfrak h: M \rightarrow M$ such that $\mathfrak h[R] = S$.

3 Doubly Strongly First Order Dependencies

We will now characterize the relativizable dependencies $\mathbf{D}$ such that $\{\mathbf{D}, \sim \!\!\mathbf{D}\}$ is strongly first order, where $\sim \!\!\mathbf{D}$ is the complement of $\mathbf{D}$:

Definition 13 (Complement of a Dependency)

Let $\mathbf{D}$ be any generalized dependency. Then $\sim \!\!\mathbf{D}$ is the generalized dependency $\{(M, R) : (M, R) \not \in \mathbf{D}\}$. If $\mathcal D$ is a family of dependencies, we write $\sim \!\!\mathcal D$ for the family $\{\sim \!\!\mathbf{D}: \mathbf{D}\in \mathcal D\}$.

Definition 14 (Doubly Strongly First Order Dependencies)

Let $\mathbf{D}$ be a generalized dependency. Then $\mathbf{D}$ is doubly strongly first order if and only if $\{\mathbf{D}, \sim \!\!\mathbf{D}\}$ is strongly first order. Likewise, a family $\mathcal D$ of dependencies is doubly strongly first order if and only if $\mathcal D~\cup \sim \!\!\mathcal D$ is strongly first order.

Clearly $\mathfrak M\models _X (\sim \!\!\mathbf{D}) \vec v$ if and only if $\mathfrak M\not \models _X \mathbf{D}\vec v$ if and only if $\mathfrak M\models _X \sim \!\!(\mathbf{D}\vec v)$. Also, if $\alpha$ is a first order literal, $\sim \!\!\alpha$ is equivalent to $\diamond (\lnot \alpha )$:⁹ therefore, via Proposition 4, it can be shown that $\mathcal D$ is doubly strongly first order if and only if $\mathbf {FO}(\sim _0, \mathcal D) \equiv \mathbf {FO}$, where $\mathbf {FO}(\sim _0, \mathcal D)$ is the fragment of $\mathbf {FO}(\sim , \mathcal D)$ in which the contradictory negation $\sim$ only occurs in front of literals or dependency atoms.

Our characterization will be based on the following result about strongly first order, relativizable dependencies from [7]:

Definition 15

($\mathbf{D}_{\max }$). Let $\mathbf{D}$ be any dependency. Then $\mathbf{D}_{\max } = \{(M, R) \in \mathbf{D}: \forall R' \supsetneq R, (M, R') \not \in \mathbf{D}\}$ is the dependency containing the maximal $(M, R) \in \mathbf{D}$.

Theorem 3

([7], Theorem 23 and Proposition 22). Let $\mathbf{D}$ be a strongly first order, relativizable dependency. Then there exists some first order sentence

$$\begin{aligned} \mathbf{D}^m(R) = \bigvee _{i = 1}^n \exists \vec y \forall \vec x(R \vec x \leftrightarrow \theta _i(\vec x, \vec y)), \end{aligned}$$

(1)

where each $\theta _i$ is a first order formula over the empty signature, such that, for all (M, R), if $(M, R) \in \mathbf{D}_{\max }$ then $(M, R) \models \mathbf{D}^m(R)$. Also, for all $(M, R) \in \mathbf{D}$, R is contained in some $R'$ such that $(M, R') \in \mathbf{D}_{\max }$.

We will now see that if $\mathbf{D}$ and $\sim \!\!\mathbf{D}$ are both strongly first order, there can be no infinite ascending “stair” of relations satisfying alternatively $\mathbf{D}$ and $\sim \!\!\mathbf{D}$:

Fig. 1.

If both $\mathbf{D}$ and $\sim \!\!\mathbf{D}$ are (separately) strongly first order, this configuration of k-ary relations $P_i$ and $Q_i$ over some domain M is forbidden by Lemma 1.

Lemma 1

Let $\mathbf{D}$ be a k-ary dependency, and let $(P_i)_{i \in \mathbb N}$ and $(Q_i)_{i \in \mathbb N}$ be k-ary relations over the same domain M such that

• 1. For all $i \in \mathbb N$, $(M, P_i) \in \mathbf{D}$;

• 2. For all $i \in \mathbb N$, $(M, Q_i) \in \sim \!\!\mathbf{D}$;

• 3. For all $i \in \mathbb N$, $P_i \subseteq Q_i \subseteq P_{i+1}$.

Then at least one between $\mathbf{D}$ and $\sim \!\!\mathbf{D}$ is not strongly first order.

Proof

Let $\mathbf{D}$ and $\sim \!\!\mathbf{D}$ be strongly first order and suppose that relations $P_i, Q_i$ as per our hypothesis exist over some domain M.

M is clearly infinite, since $P_0 \subsetneq P_{1} \subsetneq P_2 \subsetneq \ldots$; so by the Löwenheim-Skolem Theorem we can assume that M is countable and we can identify it with $\mathbb N$. Now let P and Q be the $(k+1)$-ary relations over $\mathbb N$ whose interpretations are $\{(\vec m, i) \in \mathbb N^{k+1}: \vec m \in P_i\}$ and $\{(\vec m, j) \in \mathbb N^{k+1}: \vec m \in Q_j\}$ respectively. Now consider the model $\mathfrak M= (\mathbb N, <, P, Q)$ where < is the usual ordering over $\mathbb N$. I state that, if $\mathbf {FO}(\mathbf{D}) \equiv \mathbf {FO}(\sim \!\!\mathbf{D}) \equiv \mathbf {FO}$, $\mathfrak M$ has no uncountable elementary extensions; but this is impossible due to the Löwenheim-Skolem Theorem.

In order to show that $\mathfrak M$ has no uncountable (in fact, no non-standard) elementary extensions, consider the $\mathbf {FO}(\sim \!\!\mathbf{D})$ sentence

$$\begin{aligned} \exists i (i < d \wedge \forall \vec w(\lnot P \vec w i \vee (P \vec w i \wedge (\sim \!\!\mathbf{D}) \vec w))) \end{aligned}$$

(2)

in the signature of $\mathfrak M$ augmented by some new constant symbol d. Since $\sim \!\!\mathbf{D}$ is strongly first order, this sentence is equivalent to some first order sentence $\phi (d)$. I state that $\phi (d)$ is true if and only if there exists a nonempty set of indexes $I \subseteq M$ such that $i < d$ for all $i \in I$ and such that $\left( M, \bigcup _{i \in I}P_i)\right) \not \in \mathbf{D}$, where $P_i$ is the relation $\{\vec m: (\vec m, i) \in P\}$. Indeed, if such a family of indexes exists, we can satisfy (2) by choosing the values of I as the values of the variable i,¹⁰ then taking all possible values of $\vec w$ for all chosen i, and then splitting the team by putting in the right disjunct all the assignments s for which $P \vec w i$ (that is, for which $s(\vec w) \in P_{s(i)}$); and conversely, if (2) can be satisfied, the values that the variable i can take will form a set I of indexes $< d$ such that $\bigcup _{i \in I} P_i$ does not satisfy $\mathbf{D}$.

Now, for the model $\mathfrak M$ with domain $\mathbb N$ described above no such family I may be found no matter the choice of d. Indeed, there will be only finitely many indexes less than d, and so if all elements of I are less than d then $\bigcup _{i \in I} P_i = P_{\max (I)}$, which satisfies $\mathbf{D}$. Hence, $\mathfrak M\models \lnot \exists n \phi (n)$.

Similarly, the $\mathbf {FO}(\mathbf{D})$ sentence $\exists j (j < d \wedge \forall \vec w (\lnot Q \vec w j \vee (Q \vec w j \wedge \mathbf{D}\vec w)))$ is true if and only there exists a nonempty set J of indexes $< d$ such that $\bigcup _{j \in J} Q_j$ satisfies $\mathbf{D}$; and as above, this sentence must be equivalent to some first order $\psi (d)$, because $\mathbf{D}$ is strongly first order, and $\mathfrak M\models \lnot \exists n \psi (n)$.

Now let $\mathfrak M'$ be any elementary extension of $\mathfrak M$, and let d be any nonstandard element of it (that is, any element greater than all $n \in \mathbb N$). Then at least one between $\phi (d)$ and $\psi (d)$ will hold in $\mathfrak M'$. Indeed, in $\mathfrak M'$ – like in $\mathfrak M$ – we will have that $P_i \subseteq Q_i \subseteq P_{i+1}$ for all indexes $i \in \mathbb N$; and therefore, $\bigcup _{i \in \mathbb N} P_i = \bigcup _{i \in \mathbb N}Q_i$ and all indexes in $\mathbb N$ are less than our element d. If this union satisfies $\mathbf{D}$, $\psi (d)$ holds; and if if instead it does not satisfy $\mathbf{D}$, $\phi (d)$ holds. So $\mathfrak M' \models (\exists n \phi (n)) \vee (\exists n \psi (n))$ and $\mathfrak M'$ is not an elementary extension of $\mathfrak M$, contradicting our premise. Thus, $\mathfrak M$ cannot have elementary extensions with non-standard elements (and in particular it cannot have uncountable elementary extensions).

The next lemma can be verified by applying the rules of Team Semantics:

Lemma 2

For all models $\mathfrak M$ with domain M, teams X over M, and formulas $\theta (\vec v, \vec y)$ over the empty signature with $\vec v$ contained in the variables of X,¹¹

$$\begin{aligned} (M, R:= X(\vec v)) \models \exists \vec y \forall \vec x(R \vec x \rightarrow \theta (\vec x, \vec y))&\Leftrightarrow \mathfrak M\models _X \exists \vec y (=\!\!(\vec y) \wedge \theta (\vec v, \vec y));\\ (M, R:=X(\vec v)) \not \models \exists \vec y \forall \vec x (R \vec x \rightarrow \theta (\vec x, \vec y))&\Leftrightarrow \mathfrak M\models _X \top \vee \exists \vec y (\mathbf{All} (\vec y) \wedge \lnot \theta (\vec v, \vec y)). \end{aligned}$$

Lemma 3

Let $\mathbf{D}$ be a k-ary strongly first order, relativizable dependency and let $\theta (\vec x, \vec y)$ be a first order formula over the empty signature, where $\vec x$ is a tuple of k distinct variables. Then $\mathbf{D}_\theta = \{(M', R') : (M', R') \in \mathbf{D}, (M', R') \models \exists \vec y \forall \vec x(R' \vec x \rightarrow \theta (\vec x, \vec y))\}$ is also strongly first order and relativizable.

Proof

Observe that by Lemma 2, $\mathbf{D}_\theta \vec x$ is logically equivalent to the $\mathbf {FO}(\mathbf{D}, =\!\!(\cdot ))$ formula $\mathbf{D}\vec x \wedge \exists \vec a (=\!\!(\vec a) \wedge \theta (\vec x, \vec a))$. Therefore, every $\mathbf {FO}(\mathbf{D}_\theta )$ sentence is equivalent to some $\mathbf {FO}(\mathbf{D}, =\!\!(\cdot ))$ sentence and hence – by Proposition 5 – to some $\mathbf {FO}$ sentence. Therefore, $\mathbf{D}_\theta$ is strongly first order. To show that $\mathbf{D}_\theta$ is also relativizable, observe that its relativization to some unary predicate P can be defined in terms of constancy atoms and of the relativization of $\mathbf{D}$ to P, since $\mathbf{D}_\theta ^{(P)} \vec x \equiv \mathbf{D}^{(P)} \vec x \wedge \exists \vec a \left( =\!\!(\vec a) \wedge \bigwedge _{a \in \vec a} P a \wedge \theta ^{(P)} (\vec x, \vec a)\right)$, where $\theta ^{(P)}$ is the relativization (in the usual First Order Logic sense) of $\theta$ to the unary predicate P. Therefore, every $\mathbf {FO}(\mathbf{D}_\theta ^{(P)})$ sentence is equivalent to some $\mathbf {FO}(\mathbf{D}^{P}, =\!\!(\cdot ))$ sentence, and hence – again by Proposition 5 – to some first order sentence.

Proposition 9

Let $\mathbf{D}$ be a first order, relativizable dependency such that both $\mathbf{D}$ and $\sim \!\!\mathbf{D}$ are strongly first order and let $\mathfrak M= (M, R) \in \mathbf{D}$ for M countable. Then there exists a first order sentence $\eta _\mathfrak M$ of the form

$$\begin{aligned} \eta _\mathfrak M= \psi \wedge \bigwedge _{i=1}^{n} \exists \vec y_i (\forall \vec x (R \vec x \rightarrow \theta _i(\vec x, \vec y_i))) \wedge \bigwedge _{j=1}^{n'} \lnot \exists \vec z_{j} (\forall \vec x(R \vec x \rightarrow \xi _j(\vec x, \vec z_j))) \end{aligned}$$

(3)

where $\psi$ is a first order sentence over the empty signature and all the $\theta _i$ and the $\xi _j$ are first order formulas over the empty signature, such that $\mathfrak M\models \eta _\mathfrak M$ and $\eta _\mathfrak M\models \mathbf{D}(R)$.¹²

Proof

Let T be the theory

$$\begin{aligned} T =&\, \{\psi : M \models \psi \} ~ \cup \{\exists \vec y \forall \vec x (R \vec x \rightarrow \theta (\vec x, \vec y)) : (M, R) \models \exists \vec y \forall \vec x (R \vec x \rightarrow \theta (\vec x, \vec y))\} ~\cup \\&\{\lnot \exists \vec z \forall \vec x (R \vec x \rightarrow \xi (\vec x, \vec z)) : (M, R) \not \models \exists \vec z \forall \vec x (R \vec x \rightarrow \xi (\vec x, \vec z))\} \end{aligned}$$

where $\vec x$ is a tuple of distinct variables such that $|\vec x|$ is the arity of $\mathbf{D}$, $\psi$ ranges over all first order sentences over the empty signature, $\vec y$ and $\vec z$ range over tuples of distinct variables disjoint from $\vec x$ of all finite lengths (including the empty tuple of variables, in which case their existential quantification is vacuous), and $\theta (\vec x, \vec y)$ and $\xi (\vec x, \vec z)$ range over first order formulas with free variables in $\vec x \vec y$ (respectively $\vec x \vec z$) over the empty signature. If we can show that $T \models \mathbf{D}(R)$, the conclusion follows: indeed, by compactness we can then find a finite theory $T_f \subseteq T$ such that $T_f \models \mathbf{D}(R)$, and then $\bigwedge T_f$ has the required form.

Suppose that this is not true, and let $\mathfrak A=(A, S)$ be some model such that $\mathfrak A\models T$ but $\mathfrak A\not \in \mathbf{D}$. Since $\mathfrak A$ and $\mathfrak M$ satisfy the same sentences over the empty signature, we can assume that $\mathfrak A$ and $\mathfrak M$ have the same cardinality (finite or – via Löwenheim-Skolem – countably infinite) and therefore that, up to isomorphism, the domain A of $\mathfrak A$ is the same as that M of $\mathfrak M$, i.e., $\mathfrak A= (M, S)$. Also, $R \not = \emptyset$: indeed, if R were empty then $\forall \vec x (R \vec x \rightarrow \bot )$ would be in T, and so since $(M, S) \models T$ the relation S would also be $\emptyset$, which is impossible since $(M, R) \in \mathbf{D}$ but $(M, S) \not \in \mathbf{D}$. Therefore $\lnot \forall \vec x (R \vec x \rightarrow \bot )$ is in T and $S \not = \emptyset$ too.

I aim to prove, by induction on n, that for every $n \in \mathbb N$ there exists in M a descending chain of relations $S^n_0 \supseteq R^n_0 \supseteq S^n_1 \supseteq R^n_1 \ldots S^n_n \supseteq R^n_n \supseteq R$ such that

• 1. $(M, S^n_i) \in \sim \!\!\mathbf{D}$ and $(M, R^n_i) \in \mathbf{D}$ for all $i = 1 \ldots n$;

• 2. Every $R^n_i$, for $0 \le i \le n$, is defined by some formula $\theta _i(\vec x, \vec y)$ over the empty signature that fixes the identity type of $\vec y$ and by some tuple of elements $\vec a_i^n$, in the sense that $R^n_i = \{\vec m: M \models \theta _i(\vec m, \vec a_i^n)\}$;

• 3. Every $S^n_i$, for $0 \le i \le n$, is defined by some formula $\xi _i(\vec x, \vec z)$ over the empty signature that fixes the identity type of $\vec z$ and by some tuple of elements $\vec b^n_i$, in the sense that $S^n_i = \{\vec m : M \models \xi _i(\vec m, \vec b_i^n)\}$.

• Base Case: See Fig. 2. Since $(M, S) \not \in \mathbf{D}$, $(M, S) \in \sim \!\!\mathbf{D}$; and therefore, by Theorem 3, there exists some $S' \supseteq S$ such that $(M, S') \in (\sim \!\!\mathbf{D})_{\max }$. Also by Theorem 3, $S'$ is first order definable over the empty signature: $(M, S') \models \exists \vec z \forall \vec x(S' \vec x \leftrightarrow \xi _0(\vec x, \vec z))$, where by Proposition 7 we can assume that $\xi _0$ fixes the identity type of $\vec z$. Since $S \subseteq S'$, $(M, S) \models \exists \vec z \forall \vec x(S \vec x \rightarrow \xi _0(\vec x, \vec z))$; and since $(M, S) \models T$, $(M, R) \models \exists \vec z \forall \vec x(R \vec x \rightarrow \xi _0(\vec x, \vec z))$ too.

  Now consider the dependency $\mathbf{E}_0 = \{(M', R') \in \mathbf{D}: (M', R') \models \exists \vec z \forall \vec x (R' \vec x \rightarrow \xi _0(\vec x, \vec z))\}$. By Lemma 3, $\mathbf{E}_0$ is strongly first order and relativizable, and $(M, R) \in \mathbf{E}_0$; therefore, by Theorem 3, there exists some $R_0^0 \supseteq R$ such that $(M, R_0^0) \in (\mathbf{E}_0)_{\max }$, and this $R_0^0$ is definable by some $\theta _0(\vec x, \vec y)$ that fixes the identity type of $\vec y$ and by some tuple $\vec a_0^0 \in M^{|y|}$, in the sense that $R_0^0 = \{\vec m : M \models \theta _0^0(\vec m, \vec a_0^0)\}$.

  Since $(M, R^0_0) \in (\mathbf{E}_0)_{\max }$, $(M, R^0_0) \in \mathbf{E}_0$. Therefore, $(M, R_0^0) \in \mathbf{D}$, and there exists some tuple $\vec b_0^0$ in M such that $R_0^0 \subseteq S_0^0 = \{\vec m : M \models \xi _0(\vec m, \vec b_0^0)\}$. Now $S^0_0$ is nonempty, as it contains $R^0_0$ and hence R, and $S'$ is nonempty, as it contains S, and they are both defined by the same formula $\xi _0(\vec x, \vec z)$ that fixes the identity type of $\vec z$. Therefore, by Proposition 8, there exists a bijection $\mathfrak h: M \rightarrow M$ that maps $S'$ into $S_0^0$. This implies that $(M, S_0^0)$ is isomorphic to $(M, S')$, and thus that $(M, S_0^0) \in \sim \!\!\mathbf{D}$ as required.

• Induction Case: See Fig. 3. Suppose that a chain $S^n_0 \supseteq R^n_0 \ldots S^n_n \supseteq R^n_n \supseteq R$ exists as per our hypothesis. Then, in particular, $R^n_n$ is defined by some $\theta _n(\vec x, \vec y)$ that fixes the identity type of $\vec y$; and since $R \subseteq R^n_n$, $(M, R) \models \exists \vec y \forall \vec x(R \vec x \rightarrow \theta _n(\vec x, \vec y))$. But then, since $(M, S) \models T$, $(M, S) \models \exists \vec y \forall \vec x(S \vec x \rightarrow \theta _n(\vec x, \vec y))$ too. Now consider the dependency $\mathbf{F}_n = \{(M', R')\, {\in }\, {\sim \!\!}\,\, \mathbf{D}: (M', R') \models \exists \vec y \forall \vec x(R' \vec x \rightarrow \theta _n(\vec x, \vec y))\}$. By Lemma 3, $\mathbf{F}_n$ is strongly first order and relativizable, and $(M, S) \in \mathbf{F}_n$; therefore, there exists some $S' \supseteq S$ such that $(M, S') \in (\mathbf{F}_n)_{\max }$, and this $S'$ is defined by some $\xi _{n+1}(\vec x, \vec z)$ over the empty signature that (by Proposition 7) fixes the identity type of $\vec z$. Therefore, since $S \subseteq S'$, $(M, S) \models \exists \vec z \forall \vec x(S \vec x \rightarrow \xi _{n+1}(\vec x, \vec z))$; and since $(M, S) \models T$, this implies that $(M, R) \models \exists \vec z \forall \vec x(R \vec x \rightarrow \xi _{n+1}(\vec x, \vec z))$ as well.

  Consider the dependency $\mathbf{E}_{n+1} = \{(M', R') \in \mathbf{D}: (M', R') \models \exists \vec z \forall \vec x(R' \vec x \rightarrow \xi _{n+1}(\vec x, \vec z))\}$. Again, by Lemma 3, $\mathbf{E}_{n+1}$ is strongly first order and relativizable, and $(M, R) \in \mathbf{E}_{n+1}$; therefore, there exists some $R^{n+1}_{n+1} \supseteq R$ such that $(M, R^{n+1}_{n+1}) \in (\mathbf{E}_{n+1})_{\max }$. This $R^{n+1}_{n+1}$ will, again, be first order definable over the empty signature by some $\theta _{n+1}(\vec x, \vec y)$ that fixes the identity type of $\vec y$ and by some tuple $\vec a^{n+1}_{n+1}$. Furthermore, since $(M, R^{n+1}_{n+1}) \in \mathbf{E}_{n+1}$, it will be the case that $(M, R^{n+1}_{n+1}) \in \mathbf{D}$ and that there exists some $\vec b^{n+1}_{n+1}$ such that $R^{n+1}_{n+1} \subseteq S^{n+1}_{n+1} = \{\vec m : M \models \xi _{n+1}(\vec m, \vec b^{n+1}_{n+1})\}$. Now since $S^{n+1}_{n+1}$ and $S'$ are defined by the same $\xi _{n+1}(\vec x, \vec z)$ and are both nonempty, by Proposition 8 there exists some bijection $\mathfrak g: M \rightarrow M$ such that $\mathfrak g[S'] = S^{n+1}_{n+1}$. Therefore, $(M, S^{n+1}_{n+1}) \in \mathbf{F}_n$: thus, $(M, S^{n+1}_{n+1}) \in \sim \!\!\mathbf{D}$, and there exists some $\vec a^{n+1}_n$ for which $S^{n+1}_{n+1} \subseteq R^{n+1}_n = \{\vec m : \theta _n(\vec m, \vec a^{n+1}_n)\}$.

  $R^{n+1}_{n}$ and $R^n_n$ are defined by the same formula $\theta _n(\vec x, \vec y)$, which fixes the identity type of $\vec y$, and they are both nonempty since they both contain R. Thus by Proposition 8 there exists some bijection $\mathfrak h: M \rightarrow M$ that maps $R^n_n$ into $R^{n+1}_{n}$. Then, for all $i = 0 \ldots n$, let $R^{n+1}_i = \mathfrak h[R^n_i]$ and $S^{n+1}_i = \mathfrak h[S^n_i]$.

  Then $S^{n+1}_0 \supseteq R^{n+1}_0 \supseteq S^{n+1}_1 \supseteq \ldots S^{n+1}_n \supseteq R^{n+1}_n \supseteq S^{n+1}_{n+1} \supseteq R^{n+1}_{n+1} \supseteq R$, because $\mathfrak h$ preserves inclusions. Additionally, $(M, S^{n+1}_i) \,{\in } \,{\sim \!\!}\,\, \mathbf{D}$ and $(M, R^{n+1}_i) \in \mathbf{D}$ for all $i = 0 \ldots n+1$, as required, since $\mathbf{D}$ and $\sim \!\!\mathbf{D}$ are closed under isomorphisms, and for all $i \in 0 \ldots n$ the $S^{n+1}_i$ and $R^{n+1}_i$ are still defined respectively by $\xi _i$ and $\theta _i$ and by $\vec a^{n+1}_i = \mathfrak h(\vec a^n_i)$, $\vec b^{n+1}_i = \mathfrak h(\vec b^n_i)$, since $S^{n+1}_i = \mathfrak h[S^n_i] = \{\mathfrak h(\vec m) : M \models \xi _i(\vec m, \vec b^n_i)\} = \{\vec m' : M \models \xi _i(\vec m', \mathfrak h(\vec b^n_i))\}$ and $R^{n+1}_i = \mathfrak h[R^n_i] = \{\mathfrak h(\vec m) : M \models \theta _i(\vec m, \vec a^n_i)\} = \{\vec m' : M \models \theta _i(\vec m', \mathfrak h(\vec a^n_i))\}$.

Finally, consider the theory

$$ U = \{\forall \vec x (P_i \vec x \rightarrow Q_i \vec x) \wedge (Q_i \vec x \rightarrow P_{i+1} \vec x) : i \in \mathbb N\} \cup \{\mathbf{D}(P_i), \lnot \mathbf{D}(Q_i)\} : i \in \mathbb N\} $$

that states that there is an infinite ascending chain $P_0 \subseteq Q_0 \subseteq P_1 \subseteq Q_1 \subseteq \ldots$ of relations satisfying alternatively $\mathbf{D}$ and $\lnot \mathbf{D}$ as per Fig. 1. U is finitely satisfiable: indeed, for any finite subset $U_f$ of U, if n is the highest index for which $P_n$ or $Q_n$ appear in $U_f$, the model with domain M in which $P_0 \ldots P_n$ are interpreted as $R^n_n \ldots R^n_0$ (note the inverse order) and $Q_0 \ldots Q_n$ are interpreted as $S^n_n \ldots S^n_0$ (likewise in inverse order) satisfies $U_f$, since $P_i = R^n_{n-i} \subseteq S^n_{n-i} = Q_i$ and $Q_i = S_{n-i} \subseteq R_{n-i-1} = P_{i+1}$. Therefore, by compactness, U is satisfiable; and by Lemma 1, at least one between $\mathbf{D}$ and $\sim \!\!\mathbf{D}$ is not strongly first order.

Fig. 2.

The base case.

Fig. 3.

The induction case. M is showed twice to avoid cluttering the figure too much.

We can now prove the main result of this work:

Theorem 4

Let $\mathbf{D}$ be a relativizable first order dependency. Then the following are equivalent:

• i) $\mathbf{D}(R)$ is equivalent to some sentence of the form

  $$\begin{aligned} \bigvee _{k=1}^l \left( \psi _k \wedge \bigwedge _{i=1}^{n_k} \exists \vec y^k_i (\forall \vec x (R \vec x \rightarrow \theta ^k_i(\vec x, \vec y^k_i))) \wedge \bigwedge _{j=1}^{n'_k} \lnot \exists \vec z^k_{j} (\forall \vec x(R \vec x \rightarrow \xi ^k_j(\vec x, \vec z^k_j))) \right) \end{aligned}$$

  (4)

  where all the $\psi _k$ are first order sentences over the empty vocabulary and all the $\theta _i^k$ and the $\xi _j^k$ are first order formulas over the empty vocabulary;

• ii) Both $\mathbf{D}$ and $\sim \!\!\mathbf{D}$ are definable in $\mathbf {FO}(\mathcal D_0, \sqcup , =\!\!(\cdot ), \mathbf{All} )$;

• iii) $\mathbf{D}$ is doubly strongly first order.

• iv) Both $\mathbf{D}$ and $\sim \!\!\mathbf{D}$ are (separately) strongly first order.

Proof

• i) $\Rightarrow$ ii): Suppose that $\mathbf{D}(R)$ is in the form of Eq. (4) and, for each first order sentence $\psi$ over the empty signature $\psi$, let $[\psi ] \in \mathcal D_0$ be the 0-ary first order dependency defined as $[\psi ] = \{M : M \models \psi \}$. Then $\mathbf{D}\vec v$ is equivalent to the $\mathbf {FO}(\mathcal D_0, \sqcup , =\!\!(\cdot ), \mathbf{All} )$ formula

  $$ \bigsqcup _{k=1}^l \left( [\psi _k] \wedge \bigwedge _{i=1}^{n_k} \exists \vec y^k_i (=\!\!(\vec y^k_i) \wedge \theta ^k_i (\vec v, \vec y^k_i)) \wedge \bigwedge _{j=1}^{n'_k} (\top \vee \exists \vec z^k_j (\mathbf{All} (\vec z^k_j) \wedge \lnot \xi ^k_j(\vec v, \vec z^k_j))) \right) $$

  where, up to renaming, we can assume that $\vec v$ is disjoint from all the $\vec y^k_i$ and $\vec z^k_j$ and where each $\lnot \xi ^k_j$ stands for the corresponding expression in Negation Normal Form. Indeed, by Lemma 2 – as well as the rules TS-$\wedge$ and TS-$\sqcup$ for conjunction and global disjunction – the above expression is satisfied by a team X in a model $\mathfrak M$ if and only if there exists some $k \in 1 \ldots l$ such that

  • 1. $M \models \psi _k$;

  • 2. For all $i \in 1 \ldots n_k$, $(M, X(\vec v)) \models \exists \vec y^k_i \forall \vec x(R \vec x \rightarrow \theta ^k_i(\vec x, \vec y^k_i))$;

  • 3. For all $j \in 1 \ldots n'_k$, $(M, X(\vec v)) \not \models \exists \vec z^k_j \forall \vec x(R \vec x \rightarrow \xi ^k_j(\vec x, \vec z^k_j))$.

  These are precisely the conditions for Eq. (4) to be true in $(M, X(\vec v))$, that is, for it to be the case that $\mathfrak M\models _X \mathbf{D}\vec v$. Likewise, $\sim \!\!\mathbf{D}\vec v$ is equivalent to

  $$ \bigwedge _{k=1}^l \left( [\lnot \psi _k] \sqcup \bigsqcup _{i=1}^{n_k} (\top \vee \exists \vec y^k_i (\mathbf{All} (\vec y^k_i) \wedge \lnot \theta ^k_i(\vec v, \vec y^k_i))) \sqcup \bigsqcup _{j=1}^{n'_k} \exists \vec z^k_j (=\!\!(\vec z^k_j) \wedge \xi ^k_j(\vec v, \vec z^k_j)) \right) . $$

  Therefore, both $\mathbf{D}$ and $\sim \!\!\mathbf{D}$ are indeed definable in $\mathbf {FO}(\mathcal D_0, \sqcup , =\!\!(\cdot ), \mathbf{All} )$.

• ii) $\Rightarrow$ iii) Since both $\mathbf{D}$ and $\sim \!\!\mathbf{D}$ are definable in $\mathbf {FO}(\mathcal D_0, \sqcup , =\!\!(\cdot ), \mathbf{All} )$, every sentence of $\mathbf {FO}(\mathbf{D}, \sim \!\!\mathbf{D})$ is equivalent to some sentence of $\mathbf {FO}(\mathcal D_0, \sqcup , =\!\!(\cdot ), \mathbf{All} )$ and therefore – by Proposition 6 – to some sentence of $\mathbf {FO}$. Therefore, $\mathbf{D}$ is doubly strongly first order.

• iii) $\Rightarrow$ iv) Obvious, because $\mathbf {FO}(\mathbf{D}),\mathbf {FO}(\sim \!\!\mathbf{D}) \subseteq \mathbf {FO}(\mathbf{D}, \sim \!\!\mathbf{D}) \equiv \mathbf {FO}$.

• iv) $\Rightarrow$i) Suppose that both $\mathbf{D}$ and $\sim \!\!\mathbf{D}$ are strongly first order. Then, by Proposition 9, for every countable $\mathfrak M= (M, R) \in \mathbf{D}$ there exists some first order sentence $\eta _\mathfrak M$ of the form of Eq. (3) such that $\mathfrak M\models \eta _\mathfrak M$ and that $\eta _\mathfrak M\models \mathbf{D}(R)$. Now consider the first order theory

  $$ T = \{\lnot \eta _\mathfrak M: \mathfrak M\in \mathbf{D}, \mathfrak M \text{ is } \text{ countable }\} \cup \{\mathbf{D}(R)\} $$

  T is unsatisfiable: indeed, if it had a model then by the Löwenheim-Skolem Theorem it would have a countable model $\mathfrak M= (M, R)$, but this is impossible because we would have that $\mathfrak M\in \mathbf{D}$ (since $\mathbf{D}(R) \in T$) and thus $\mathfrak M\models \eta _\mathfrak M$, despite the fact that $\lnot \eta _\mathfrak M\in T$. Therefore, T is finitely unsatisfiable and $\mathbf{D}(R) \models \bigvee _{k=1}^l \eta _{\mathfrak M_k}$ for some finite set $\mathfrak M_1 \ldots \mathfrak M_l$ of countable models of $\mathbf{D}$. But each such $\eta _{\mathfrak M_k}$ entails $\mathbf{D}(R)$, and therefore $\mathbf{D}(R)$ is equivalent to $\bigvee _{k=1}^l \eta _{\mathfrak M_k}$ which is in the form of Eq. (4).

Corollary 1

Let $\mathcal D$ be a family of relativizable dependencies. Then $\mathcal D$ is doubly strongly first order if and only if every $\mathbf{D}\in \mathcal D$ is doubly strongly first order.

Proof

If $\mathcal D$ is doubly strongly first order and $\mathbf{D}\in \mathcal D$, every sentence of $\mathbf {FO}(\mathbf{D}, \sim \!\!\mathbf{D})$ is a sentence of $\mathbf {FO}(\mathcal D, \sim \!\!\mathcal D) \equiv \mathbf {FO}$, and so $\mathbf{D}$ is doubly strongly first order.

Conversely, suppose that every $\mathbf{D}\in \mathcal D$ is doubly strongly first order and relativizable. Then by Theorem 4, for every $\mathbf{D}\in \mathcal D$ both $\mathbf{D}$ and $\sim \!\!\mathbf{D}$ are definable in $\mathbf {FO}(\mathcal D_0, \sqcup , =\!\!(\cdot ), \mathbf{All} )$. Therefore, every sentence of $\mathbf {FO}(\mathcal D, \sim \!\!\mathcal D)$ is equivalent to some sentence of $\mathbf {FO}(\mathcal D_0, \sqcup , =\!\!(\cdot ), \mathbf{All} )$, and thus – because of Proposition 6 – to some first order sentence. Therefore, $\mathcal D$ is doubly strongly first order.