Strongly First Order, Domain Independent Dependencies: The Union-Closed Case

Team Semantics generalizes Tarski’s Semantics by defining satisfaction with respect to sets of assignments rather than with respect to single assignments. Because of this, it is possible to use Team Semantics to extend First Order Logic via new kinds of connectives or atoms – most importantly, via dependency atoms that express dependencies between different assignments.

Some of these extensions are more expressive than First Order Logic proper, while others are reducible to it. In this work, I provide necessary and sufficient conditions for a dependency atom that is domain independent (in the sense that its truth or falsity in a relation does not depend on the existence in the model of elements that do not occur in the relation) and union closed (in the sense that whenever it is satisfied by all members of a family of relations it is also satisfied by their union) to be strongly first order, in the sense that the logic obtained by adding them to First Order Logic is no more expressive than First Order Logic itself.

1. 1.

   In this work we will assume that all expressions are in Negation Normal Form. Also, we will use the usual abbreviations of First Order Logic, such as \(\vec x = \vec y\) for \(\bigwedge _i (x_i = y_i)\) where \(\vec x = (x_1 \ldots x_k)\) and \(\vec y = (y_1 \ldots y_k)\) are tuples of variables of the same length.

2. 2.

   \(\mathcal P(M)\) represents the powerset \(\{A : A \subseteq M\}\) of M.

3. 3.

   Anonymity atoms were called “non-dependence atoms” and briefly studied in Sect. 4.6 of [3], in which their equidefinability with inclusion atoms was also proved; but their interpretation and their properties are discussed more in depth in [22, 23].

4. 4.

   In the sense that every sentence of any of these logics is equivalent to some Existential Second Order sentence, and vice versa. As we will see, it is however not the case that every formula of \(\textbf{FO}(\bot )\) is equivalent to some formula of \(\textbf{FO}(|)\).

5. 5.

   The choice of \(\vec v\) in the atom \(\texttt {NE}(\vec v)\) is indifferent as long as it is contained in the domain of X. Thus, one could define \(\texttt {NE}\) as a single 0-ary dependency instead of a family of dependencies of all arities, as we do here for simplicity and uniformity.

6. 6.

   Theorem 1 in this work.

7. 7.

   Of course there is a first order sentence \(\exists \vec x R \vec x\) that says that R is not empty; however, there is no first order formula \(\phi (\vec w)\) such that \(\mathfrak M\models _X \phi (\vec w)\) if and only if \(X(\vec w) \not = \emptyset \).

8. 8.

   In [19], this property is called “Universe Independence”.

9. 9.

   The FOT logic of [20], which is a Team Semantics-based logic with no higher order quantifications in the rules for its connectives, is no stronger than First Order Logic and can define all first order dependencies.

10. 10.

    \(\texttt {NE}\) and \({\textbf {All}}\) are not union closed because the union of the empty family of relations is the empty relation, which does not satisfy these dependencies. If we restricted the definition of union closure to nonempty families I, they would be union closed.

11. 11.

    We could consider only unary constancy atoms, as \(=\!\!(\vec x) \equiv \bigwedge _{x \in \vec x} =\!\!(x)\); but, similarly to the \(\texttt {NE}\) case, for simplicity and uniformity we define constancy atoms for all arities.

12. 12.

    The result of [7] actually requires a weaker condition than domain independence called relativizability. This property is implied by domain independence, and in this work we will focus on domain independent dependencies. Totality \({\textbf {All}}\) is an example of a dependency that is relativizable but not domain independent.

13. 13.

    Again, relativizability suffices for this result.

14. 14.

    Or relativizable.

15. 15.

    Again, or just relativizable.

16. 16.

    Nonetheless, there are dependencies of interest, such as independence atoms \(\bot \), which satisfy none of these closure properties; and thus, the problem of fully characterizing strongly first order dependencies remains not entirely solved yet.

17. 17.

    This is a shorthand for \(X[M/\vec w_1][M/\vec w_2] \ldots [M/\vec w_k]\).

18. 18.

    Instead \((A_3, R_3) \in \textbf{D}\), because \((A_3, R_3) \succeq (A_2, R_2) \in \textbf{D}\) and \(\textbf{D}\) is first order.

19. 19.

    Here \(\chi [v/a_{\lambda }]\) represents the formula obtained from \(\chi \) by replacing the constant \(a_\lambda \) with the variable v.

20. 20.

    This follows from the so-called “Lemma on Constants” (e.g. Lemma 2.3.2. of [17]): if \(T \models \phi (\vec c)\), where \(\vec c\) is a tuple of constants not occurring in T, then \(T \models \forall \vec x \phi (\vec x)\).

21. 21.

    Here \(\top \) can be any literal that is always true, such as \(w = w\) for some \(w \in \vec w\).

22. 22.

    Note that the signature of \(\mathfrak M\) does not necessarily have to include the symbol R, which is instead interpreted as \(X(\vec w)\) when evaluating \(\chi _i(R)\); and accordingly, \(\chi '_i(\vec w)\) is a \(\textbf{FO}(=\!\!(\cdot ), \texttt {NE})\) formula over the empty signature.

23. 23.

    More formally: \(Y = X[H_1/x_1]\ldots [H_k/x_k]\), where each \(H_j\) picks the same singleton \(\{a_j\}\) for all assignments in its domain – indeed, only choice functions of this type can ensure that \(\mathfrak M\models _Y =\!\!(\vec x)\).

24. 24.

    Or non-jumping.

Authors and Affiliations

1. Free University of Bozen-Bolzano, Bolzano, Italy

   Pietro Galliani

Corresponding author

Correspondence to Pietro Galliani .

Editors and Affiliations

1. Technische Universität Wien, Vienna, Austria

   Agata Ciabattoni

2. University College London, London, UK

   Elaine Pimentel

3. Universidade Federal de Pernambuco, Recife, Pernambuco, Brazil

   Ruy J. G. B. de Queiroz

Reprints and permissions

© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG

Policies and ethics