Polyteam Semantics

Abstract

Team semantics is the mathematical framework of modern logics of dependence and independence in which formulae are interpreted by sets of assignments (teams) instead of single assignments as in first-order logic. In order to deepen the fruitful interplay between team semantics and database dependency theory, we define Polyteam Semantics in which formulae are evaluated over a family of teams. We begin by defining a novel polyteam variant of dependence atoms and give a finite axiomatisation for the associated implication problem. We also characterise the expressive power of poly-dependence logic by properties of polyteams that are downward closed and definable in existential second-order logic ($\mathsf {ESO}$). The analogous result is shown to hold for poly-independence logic and all $\mathsf {ESO}$-definable properties.

This research was supported by a Marsden grant from Government funding, administered by the Royal Society of New Zealand, and grants 292767 and 308712 of the Academy of Finland.

1 Introduction

Team semantics is the mathematical framework of modern logics of dependence and independence. The origin of team semantics goes back to [15] but its development to its current form began with the publication of the monograph [24]. In team semantics formulae are interpreted by sets of assignments (teams) instead of single assignments as in first-order logic. The reason for this change is that statements such as the value of a variable x depends on the value of y do not really make sense for single assignments. Team semantics has interesting connections with database theory and database dependencies [11,12,13, 18]. In order to facilitate the exchange between team semantics and database theory, we introduce a generalisation of team semantics in which formulae are evaluated over a family of teams. We identify a natural notion of poly-dependence that generalises dependence atoms to polyteams and give a finite axiomatisation for its implication problem. We also define polyteam versions of independence, inclusion and exclusion atoms, and characterise the expressive power of poly-dependence and poly-independence logic.

A team X is a set of assignments with a common finite domain $x_1,\ldots , x_{n}$ of variables. Such a team can be viewed as a database table with $x_1,\ldots , x_{n}$ as its attributes. Dependence logic extends the language of first-order logic with atomic formulae $=\!\left( \overline{x}, y\right)$ called dependence atoms expressing that value of the variable y is functionally determined by the values of the variables in $\overline{x}$. On the other hand, independence atoms $\overline{y} \perp _{\overline{x}} \overline{z}$ [9] express that, for any fixed value of $\overline{x}$, knowing the value of $\overline{z}$ does not tell us anything new about the value of $\overline{y}$. By viewing a team as a database, the atoms $=\!\left( \overline{x}, y\right)$ and $\overline{y} \perp _{\overline{x}} \overline{z}$ correspond to the widely studied functional and embedded multivalued dependencies. Furthermore, inclusion atoms $\overline{x} \subseteq \overline{y}$ and exclusion atoms $\overline{x} | \overline{y}$ of [6] inherit their semantics from the corresponding database dependencies.

Independence, inclusion, and exclusion atoms have very interesting properties in the team semantics setting. For example, inclusion atoms give rise to a variant of dependence logic that corresponds to the complexity class PTIME over finite ordered structures [7] whereas all the other atoms above (and their combinations) give rise to logics that are equi-expressive with existential second-order logic and the complexity class NP. The complexity theoretic aspects of logics in team semantics have been studied extensively during the past few years (see [4] for a survey).

A multiset version of team semantics was recently defined in [3]. Multiteam semantics is motivated by the fact that multisets are widely assumed in database theory and occur in applications. Multiteam semantics can be also used to model and study database, probabilistic, and approximate dependencies in a unified framework (see [3, 25]).

The aim of this work is similar to that of [3], i.e., we want to extend the applicability of team semantics. In database theory dependencies are often expressed by so-called embedded dependencies. An embedded dependency is a sentence of first-order logic with equality of the form

$$ \forall x_1\dots \forall x_n \big (\phi (x_1,\dots ,x_n) \rightarrow \exists y_1\dots \exists y_k \psi (x_1,\dots ,x_n,y_1,\dots ,y_k)\big ), $$

where $\phi$ and $\psi$ are conjunctions of relational atoms $R(x_1,\dots ,x_n)$ and equalities $x=y$. In the literature embedded dependencies have been thoroughly classified stemming from real life applications. Examples of well-known subclasses include full, uni-relational, 1-head, tuple-generating, and equality-generating. For example, an embedded dependency is called tuple-generating if it is equality free (for further details see, e.g., [16, Sect. 3]). The uni-relational dependencies can be studied also in the context of team semantics as generalised dependencies [21]. However in many applications, especially in the area of data exchange and data integration, it is essential to be able to express dependencies between different relations.

In the context of data exchange (see e.g. [5]) the relational database is divided into a set of source relations $\mathcal S$ and a set of target relations $\mathcal T$. Dependencies are used to describe what kind of properties should hold when data is transferred from the source schema to the target schema. In this setting a new taxonomy of embedded dependencies rises: An embedded dependency $\forall \overline{x}\big ( \phi (\overline{x}) \rightarrow \exists \overline{y} \psi (\overline{x}, \overline{y}) \big )$ is source-to-target if the relation symbols occurring in $\phi$ and $\psi$ are from $\mathcal S$ and $\mathcal T$, respectively. The embedded dependency is target if the relation symbols occurring in it are from $\mathcal T$. There is no direct way to study these classes of dependencies in the uni-relational setting of team semantics. In this paper we propose a general framework in which these inherently poly-relational dependencies can be studied.

In Sect. 2 we lay the foundations of polyteam semantics. The shift to polyteams is exemplified in Sect. 2.2, by the definition of poly-dependence atoms and an Armstrong type axiomatisation for the associated implication problem. In Sect. 3 polyteam semantics is extended from atoms to complex formulae. Section 4 studies the expressive power of the new logics over polyteams. The main technical results of the section characterises poly-independence (poly-dependence) logic as the maximal logic capable of defining all (downward closed) properties of polyteams definable in existential second-order logic.

2 From Uni-dependencies to Poly-dependencies

We start by defining the familiar dependency notions from the team semantics literature. In Sect. 2.2 we introduce a novel poly-relational version of dependence atoms and establish a finite axiomatisation of its implication problem. We then continue to present poly-relational versions of inclusion, exclusion, and independence atoms, and a general notion of a poly-relational dependency atom. We conclude this section by relating the embedded dependencies studied in database theory to our new setting.

2.1 Dependencies in Team Semantics

Vocabularies $\tau$ are sets of relation symbols with prescribed arities. For each $R\in \tau$, let ${\mathrm {ar}(R)}\in Z_+$ denote the arity of R. A $\tau$-structure is a tuple $\mathfrak {A}= \big (A, (R^\mathfrak {A}_i)_{R_i\in \tau }\big )$, where A is a set and each $R^\mathfrak {A}_i$ is an ${\mathrm {ar}(R_i)}$-ary relation on A (i.e., $R^\mathfrak {A}_i \subseteq A^{{\mathrm {ar}(R_i)}}$). We use $\mathfrak {A}$, $\mathfrak {B}$, etc. to denote $\tau$-structures and A, B, etc. to denote the corresponding domains.

Let D be a finite set of first-order variables and A be a nonempty set. A function $s:D \rightarrow A$ is called an assignment. For a variable x and $a\in A$, the assignment $s(a/x):D\cup \{x\} \rightarrow A$ is obtained from s as follows:

$$ s(a/x)(y) := {\left\{ \begin{array}{ll} a &{} \text {if y=x},\\ s(y) &{}\text {otherwise}. \end{array}\right. } $$

For an assignment s and a tuple of variables $\overline{x}=(x_1,\ldots ,x_n)$, we write $s(\overline{x})$ to denote the sequence $\big (s(x_1),\ldots ,s(x_n)\big )$. A $team$ is a set of assignments with a common domain D and codomain A. Let $\mathfrak {A}$ be a $\tau$-structure and X a team with codomain A, then we say that X is a team of $\mathfrak {A}$.

The following dependency atoms were introduced in [6, 9, 24].

Definition 1

(Dependency atoms). Let $\mathfrak {A}$ be a model and X a team with codomain A. If $\overline{x}, \overline{y}$ are variable sequences, then $=\!\left( \overline{x},\overline{y}\right)$ is a dependence atom with the truth condition:

$$\mathfrak {A}\models _X =\!\left( \overline{x},\overline{y}\right) \text { if for all } s,s'\in X \text { s.t.}\, s(\overline{x}) = s'(\overline{x}), \text { it holds that } s(\overline{y})=s'(\overline{y}).$$

If $\overline{x},\overline{y}$ are variable sequences of the same length, then $\overline{x} \subseteq \overline{y}$ is an inclusion atom and $\overline{x} \mid \overline{y}$ an exclusion atom with satisfaction defined as follows:

$$\begin{aligned}&\mathfrak {A}\models _X \overline{x} \subseteq \overline{y} \text { if for all }s\in X \text { there exists } s'\in X\text { such that } s(\overline{x})=s'(\overline{y}).\\&\mathfrak {A}\models _X \overline{x} \mid \overline{y} \text { if for all }s,s'\in X: s(\overline{x})\ne s'(\overline{y}). \end{aligned}$$

If $\overline{x},\overline{y},\overline{z}$ are variable sequences, then $\overline{y}~\bot _{\overline{x}}~\overline{z}$ is a conditional independence atom with satisfaction defined by

$$\begin{aligned}&\mathfrak {A}\models _{X} \overline{y}~\bot _{\overline{x}}~\overline{z}\text { if for all } s,s'\in X\text { such that }s(\overline{x})=s'(\overline{x})\text { there exists } s''\in X \\&\text { such that }s''(\overline{x})=s(\overline{x})\text {, }s''(\overline{y})=s(\overline{y}), \text { and }s''(\overline{z})=s'( \overline{z}). \end{aligned}$$

Note that in the previous definitions it is allowed that some or all of the vectors of variables have length 0. For example, $\mathfrak {A}\models _X=\!\left( \overline{x}\right)$ holds iff $\forall s\in X: s(\overline{x})=\overline{c}$ holds for some fixed tuple $\overline{c}$, and $\mathfrak {A}\models _X\overline{y}~\bot _{\overline{x}}~\overline{z}$ holds always if either of the vectors $\overline{y}$ or $\overline{z}$ is of length 0.

All the aforementioned dependency atoms have corresponding variants in relational databases. One effect of this relationship is that the axiomatic properties of these dependency atoms trace back to well-known results in database theory. Armstrong’s axioms for functional dependencies constitute a finite axiomatisation for dependence atoms [1, 9], and inclusion atoms can be finitely axiomatised using the axiomatisation for inclusion dependencies [2]. On the other hand, the non-axiomatisability and undecidability of the (finite and unrestricted) implication problem for embedded multivalued dependencies both carry over to conditional independence atoms [14, 22, 23]. Restricting attention to the so-called pure independence atoms, i.e., atoms of the form $\overline{x} ~\bot _{\emptyset }~ \overline{y}$, a finite axiomatisation is obtained by relating to marginal independence in statistics [8, 18].

2.2 The Notion of Poly-dependence

For each $i\in \mathbb {N}$, let $\text {Var}(i)$ denote a distinct countable set of first-order variable symbols. We say that these variables are of sort i. Relating to databases, sorts correspond to table names. Usually we set $\text {Var}(i)=\{x^i_j\mid j\in \mathbb {N}\}$. We write $x^i$, $y^i$, $x^i_j$ to denote variables form $\text {Var}(i)$, and $\overline{x}^i$ to denote tuples of variables from $\text {Var}(i)$. Sometimes we drop the index i and write simply x and $\overline{x}$ instead of $x^i$ and $\overline{x}^i$, respectively. Note that $\overline{x}$ is always a tuple of variables of a single sort. In order to simplify notation, we sometimes write $\overline{x}^i$ and $\overline{x}^j$ to denote arbitrary tuples of variables of sort i and j, respectively. We emphasise that $\overline{x}^i$ and $\overline{x}^j$ might be of different length and may consist of distinct variables. Let $\mathfrak {A}$ be a $\tau$-model and let $D_i\subseteq \text {Var}(i)$ for all $i\in \mathbb {N}$. A tuple $\overline{X}=(X_i)_{i\in \mathbb {N}}$ is a polyteam of $\mathfrak {A}$ with domain $\overline{D} =(D_i)_{i\in \mathbb {N}}$, if $X_i$ is a team with domain $D_i$ and co-domain A for each $i\in \mathbb {N}$. We identify $\overline{X}$ with $(X_0, \ldots ,X_n)$ if $X_i$ is the singleton team consisting with the empty assignment for all i greater than n. Let $\overline{X}=(X_i)_{i\in \mathbb {N}}$ and $\overline{Y}=(Y_i)_{i\in \mathbb {N}}$ be two polyteams. We say that $\overline{X}$ is a subteam of $\overline{Y}$ if $X_i\subseteq Y_i$ for all $i\in \mathbb {N}$. By the union (resp. intersection) of $\overline{X}$ and $\overline{Y}$ we denote the polyteam $(X_i\cup Y_i)_{i\in \mathbb {N}}$ (resp. $(X_i\cap Y_i)_{i\in \mathbb {N}}$). By a slight abuse of notation we write $\overline{X} \cup \overline{Y}$ (resp. $\overline{X} \cap \overline{Y}$) for the union (resp. intersection) of $\overline{X}$ and $\overline{Y}$, and $\overline{X} \subseteq \overline{Y}$ to denote that $\overline{X}$ is a subteam of $\overline{Y}$. For a tuple $\overline{V}=(V_i)_{i\in \mathbb {N}}$ where $V_i\subseteq \text {Var}(i)$, the restriction of $\overline{X}$ to $\overline{V}$, written $\overline{X} \upharpoonright \overline{V}$, is defined as $(X_i\upharpoonright V_i)_{i\in \mathbb {N}}$ where $X_i\upharpoonright V_i$ denotes the restriction of $X_i$ to $V_i$.

Next we generalise dependence atoms to the polyteam setting. In contrast to the standard dependence atoms, poly-dependence atoms declare functional dependence of variables over two teams.

Poly-dependence. Let $\overline{x}^i\overline{y}^i$ and $\overline{u}^j \overline{v}^j$ be sequences of variables such that $\overline{x}^i$ and $\overline{u}^j$, and $\overline{y}^i$ and $\overline{u}^j$ have the same length, respectively. Then $=\!\left( \overline{x}^i,\overline{y}^i/\overline{u}^j,\overline{v}^j\right)$ is a poly-dependence atom whose satisfaction relation $\models _{\overline{X}}$ is defined as follows:

$$ \mathfrak {A}\models _{\overline{X}} =\!\left( \overline{x}^i,\overline{y}^i/\overline{u}^j,\overline{v}^j\right) \Leftrightarrow \forall s\in X_i\forall s'\in X_j: s(\overline{x}^i)=s'(\overline{u}^j)\text { implies }s( \overline{y}^i)=s'( \overline{v}^j). $$

Note that the atom $=\!\left( \overline{x},\overline{y}/\overline{x},\overline{y}\right)$ corresponds to the dependence atom $=\!\left( \overline{x}, \overline{y}\right)$. For empty tuples $\overline{x}^i$ and $\overline{u}^j$ the poly-dependence atom reduces to a “poly-constancy atom” $=\!\left( \overline{y}^i/\overline{v}^j\right)$. We will later show (Remark 13) that poly-dependence atoms of the form $=\!\left( \overline{x}^i,\overline{y}^i/\overline{u}^i,\overline{v}^i\right)$ can be expressed with formulae using only ordinary dependence atoms. Thus poly-dependence atoms of this form are considered as primitive notions only when $\overline{x}^i\overline{y}^i = \overline{u}^i \overline{v}^i$; otherwise $=\!\left( \overline{x}^i,\overline{y}^i/\overline{u}^i,\overline{v}^i\right)$ is considered as a shorthand for the equivalent formula obtained from Remark 13.

The ability to reason about database dependencies can be employed to facilitate many critical data management tasks such as schema design, query optimisation, and integrity maintenance. Keys, inclusion dependencies, and functional dependencies in particular have a crucial role in all of these processes. A traditional way to approach the interaction between dependencies has been the utilisation of proof systems similar to natural deduction systems in logic. The most significant of all these systems is the Armstrong’s axiomatisation for functional dependencies. This inference system consists of only three rules which we depict below using the standard notation for functional dependencies, i.e., $X\rightarrow Y$ denotes that an attribute set X functionally determines another attribute set Y.

Definition 2

(Armstrong’s axiomatisation [1])

• Reflexivity: If $Y\subseteq X$, then $X\rightarrow Y$

• Augmentation: if $X \rightarrow Y$, then $XZ\rightarrow YZ$

• Transitivity: if $X \rightarrow Y$ and $Y\rightarrow Z$, then $X\rightarrow Z$

Our first development is the generalisation of Armstrong’s axiomatisation to the poly-dependence setting. To this end, we assemble the three rules of Armstrong and introduce three auxiliary rules: Union, Symmetry, and Weak Transitivity. Contrary to the Armstrong’s proof system, here Union is not reducible to Transitivity and Augmentation because we operate with sequences instead of sets of variables or attributes. Symmetry in turn is imposed by the sequential notation employed by the poly-dependence atom. Weak Transitivity exhibits transitivity of equalities on the right-hand side of a poly-dependence atom, a phenomenon that arises only in the polyteam setting.

Definition 3

(Axiomatisation for poly-dependence atoms)

• Reflexivity: $=\!\left( \overline{x}^i,\text {pr}_k (\overline{x}^i)/\overline{y}^j,\text {pr}_k(\overline{y}^j)\right)$, where $k=1, \ldots ,|\overline{x}^i|$ and $\text {pr}_k$ takes the kth projection of a sequence.

• Augmentation: if $=\!\left( \overline{x}^i,\overline{y}^i/\overline{u}^j,\overline{v}^j\right)$, then $=\!\left( \overline{x}^i\overline{z}^i,\overline{y}^i\overline{z}^i/\overline{u}^j\overline{w}^j,\overline{v}^j\overline{w}^j\right)$

• Transitivity: if $=\!\left( \overline{x}^i,\overline{y}^i/\overline{u}^j,\overline{v}^j\right)$ and $=\!\left( \overline{y}^i,\overline{z}^i/\overline{v}^j,\overline{w}^j\right)$, then $=\!\left( \overline{x}^i,\overline{z}^i/\overline{u}^j,\overline{w}^j\right)$

• Union: if $=\!\left( \overline{x}^i,\overline{y}^i/\overline{u}^j,\overline{v}^j\right)$ and $=\!\left( \overline{x}^i,\overline{z}^i/\overline{u}^j,\overline{w}^j\right)$ then $=\!\left( \overline{x}^i,\overline{y}^i\overline{z}^i/\overline{u}^j,\overline{v}^j\overline{w}^j\right)$

• Symmetry: if $=\!\left( \overline{x}^i,\overline{y}^i/\overline{u}^j,\overline{v}^j\right)$, then $=\!\left( \overline{u}^j,\overline{v}^j/\overline{x}^i,\overline{y}^i\right)$

• Weak Transitivity: if $=\!\left( \overline{x}^i,\overline{y}^i\overline{z}^i\overline{z}^i/\overline{u}^j,\overline{v}^j\overline{v}^j\overline{w}^j\right)$, then $=\!\left( \overline{x}^i,\overline{y}^i/\overline{u}^j,\overline{w}^j\right)$

This proof system forms a complete characterisation of logical implication for poly-dependence atoms. We use $\models$ to refer to logical implication, i.e., we write $\varSigma \models ~\sigma$ if $\mathcal {A}\models _{\overline{X}} \varSigma$ implies $\mathcal {A}\models _{\overline{X}} \sigma$ for all models $\mathcal {A}$ and polyteams $\overline{X}$. Given an axiomatisation R, that is, a set of axioms and inference rules, we write $\varSigma \vdash _{\mathcal {R}}\sigma$ if $\mathcal {R}$ yields a proof of $\sigma$ from $\varSigma$. Given a class of dependency atoms $\mathcal {C}$, we then say that $\mathcal {R}$ is sound (complete, resp.) for $\mathcal {C}$ if for all finite sets of dependency atoms $\varSigma \cup \{\sigma \}$ from $\mathcal {C}$, $\varSigma \vdash _{\mathcal {R}}\sigma$ implies (is implied by, resp.) $\varSigma \models ~\sigma$.

Theorem 4

The axiomatisation of Definition 3 is sound and complete for poly-dependence atoms.

Proof

The proof of soundness is straightforward and omitted. We show that the axiomatisation is complete, i.e., that $\varSigma \models ~\sigma$ implies $\varSigma \vdash \sigma$ for a set $\varSigma \cup \{\sigma \}$ of poly-dependence atoms. Assume $\sigma$ is $=\!\left( \overline{x}^i,\overline{y}^i/\overline{x}^j,\overline{y}^j\right)$. First we consider the case where $i=j$ in which case $\sigma$ is a standard dependence atom. Let $\varSigma ^*$ be the subset of $\varSigma$ consisting of all standard dependence atoms over $\text {Var}(i)$. Since all teams satisfying $\varSigma ^*$ can be extended to a polyteam satisfying $\varSigma$ by introducing new empty teams, we have that $\varSigma ^*\models ~\sigma$ in the team semantics setting. Since dependence atoms $=\!\left( \overline{x},\overline{y}\right)$ in team semantics correspond to functional dependencies $\{x\in \overline{x}^i\}\rightarrow \{y\in \overline{y}^i\}$ in relational databases (see e.g. [9]), Armstrong’s complete axiomatisation from Definition 2 yields a deduction of $\sigma _0$ from $\varSigma ^*_0$ where $\varSigma ^*_0$ and $\{\sigma _0\}$ are obtained from $\varSigma ^*$ and $\sigma$ by replacing dependence atoms with their corresponding functional dependencies. Since dependence atoms are provably order-independent (i.e. one derives $=\!\left( \overline{x}_0,\overline{x}_1\right)$ from $=\!\left( \overline{y}_0,\overline{y}_1\right)$ by Reflexivity, Union, and Transitivity if $\overline{x}_i$ and $\overline{y}_i$ list the same variables), the deduction in Armstrong’s system can be simulated with the rules in Definition 3. This proves the case $i=j$.

Let us then consider the case $i\ne j$. We will show that $\varSigma \not \vdash \sigma$ implies $\varSigma \not \models ~\sigma$. Assume $\varSigma \not \vdash \sigma$. Define first a binary relation $\sim$ on $\text {Var}(i)\cup \text {Var}(j)$ such that $a^i\sim a^j$ if $\varSigma \vdash =\!\left( \overline{x}^i,a^i/\overline{x}^j,a^j\right)$, $a^j\sim a^i$ if $\varSigma \vdash =\!\left( \overline{x}^j,a^j/\overline{x}^i,a^i\right)$, and $a^i\sim b^i$ ($a^j\sim b^j$, resp.) if $a^i=b^i$ or $\varSigma \vdash =\!\left( \overline{x}^i,a^ib^i/\overline{x}^j,a^ja^j\right)$ for some $a^j$ ($a^j=b^j$ or $\varSigma \vdash =\!\left( \overline{x}^j,a^jb^j/\overline{x}^i,a^ia^i\right)$ for some $a^i$, resp.). We show that $\sim$ is an equivalence relation.

• Reflexivity: Holds by definition.

• Symmetry: First note that $a^i\sim a^j$ and $a^j\sim a^i$ are derivably equivalent by the symmetry rule. Assume that $a^i\sim b^i$ in which case $=\!\left( \overline{x}^i,a^ib^i/\overline{x}^j,a^ja^j\right)$ is derivable for some $a^j$. Then derive $=\!\left( a^ib^i,b^i/a^ja^j,a^j\right)$ and $=\!\left( a^ib^i,a^i/a^ja^j,a^j\right)$ by using the reflexivity rule, and then $=\!\left( \overline{x}^i,b^i/\overline{x}^j,a^j\right)$ and $=\!\left( \overline{x}^i,a^i/\overline{x}^j,a^j\right)$ by using the transitivity rule. Finally derive $=\!\left( \overline{x}^i,b^ia^i/\overline{x}^j,a^ja^j\right)$ by using the union rule.

• Transitivity: Assume first that $a^i\sim b^i\sim c^i$, where $a^i, b^i,c^i$ and are pairwise distinct. Then $=\!\left( \overline{x}^i,a^ib^i/\overline{x}^j,a^ja^j\right)$ and $=\!\left( \overline{x}^i,b^ic^i/\overline{x}^j,b^jb^j\right)$ are derivable for some $a^j$ and $b^j$. Then analogously to the previous case assemble $=\!\left( \overline{x}^i,a^ib^ib^i/\overline{x}^j,a^ja^jb^j\right)$ which admits $=\!\left( \overline{x}^i,a^i/\overline{x}^j,b^j\right)$ by weak transitivity, and detach $=\!\left( \overline{x}^i,c^i/\overline{x}^j,b^j\right)$ from $=\!\left( \overline{x}^i,b^ic^i/\overline{x}^j,b^jb^j\right)$. By the union rule we then obtain $=\!\left( \overline{x}^i,a^ic^i/\overline{x}^j,b^jb^j\right)$ and thus that $a^i\sim c^i$. Since all the other cases are analogous, we observe that $\sim$ is transitive.

Let s be a function that maps each $x\in \text {Var}(i)\cup \text {Var}(j)$ that appears in $\varSigma \cup \{\sigma \}$ to the equivalence class $x/\sim$. We define $\overline{X}=(X_i,X_j)$ where $X_k=\{s\upharpoonright \text {Var}(k)\}$ for $k=i,j$. First notice that $\overline{X}\not \models ~\sigma$ for, by union, it cannot be the case that $\text {pr}_k(\overline{y}^i)\sim \text {pr}_k(\overline{y}^j)$ for all $k=1, \ldots ,|\overline{y}^i|$. It suffices to show that $\overline{X}$ satisfies each $=\!\left( \overline{u}^m,\overline{v}^m/\overline{u}^n,\overline{v}^n\right)$ in $\varSigma$. If $m=n$ or $\{m,n\}\ne \{i,j\}$, the atom is trivially satisfied. Hence, and by symmetry, we may assume that the atom is of the form $=\!\left( \overline{u}^i,\overline{v}^i/\overline{u}^j,\overline{v}^j\right)$. Assume that $s(\overline{u}^i)=s(\overline{u}^j)$, that is, $\text {pr}_k(\overline{u}^i)\sim \text {pr}_k(\overline{u}^j)$ for all $k=1, \ldots ,|\overline{u}^i|$. We obtain by the union rule that $=\!\left( \overline{x}^i,\overline{u}^i/\overline{x}^j,\overline{u}^j\right)$ is derivable, and hence by the transitivity rule that $=\!\left( \overline{x}^i,\overline{v}^i/\overline{x}^j,\overline{v}^j\right)$ is also derivable. Therefore, by using the reflexivity and transitivity rules we conclude that $s(\overline{v}^i)=s(\overline{v}^j)$.   $\square$

2.3 A General Notion of a Poly-dependency

Next we consider suitable polyteam generalisations for the dependencies discussed in Sect. 2.1 and also define a general notion of poly-dependency. This generalisation is immediate for inclusion atoms which are inherently multi-relational; relational database management systems maintain referential integrity by enforcing inclusion dependencies specifically between two distinct tables. With poly-inclusion atoms these multi-relational features can now be captured.

Poly-inclusion. Let $\overline{x}^i$ and $\overline{y}^j$ be sequences of variables of the same length. Then $\overline{x}^i \subseteq \overline{y}^j$ is a poly-inclusion atom whose satisfaction relation $\models _{\overline{X}}$ is defined as follows:

$$\begin{aligned} \mathfrak {A}\models _{\overline{X}} \overline{x}^i \subseteq \overline{y}^j \Leftrightarrow \forall s\in X_i\exists s'\in X_j: s(\overline{x}^i)=s'(\overline{y}^j). \end{aligned}$$

If $i=j$, then the atom is the standard inclusion atom.

Poly-exclusion. Let $\overline{x}^i$ and $\overline{y}^j$ be sequences of variables of the same length. Then $\overline{x}^i \mid \overline{y}^j$ is a poly-exclusion atom whose satisfaction relation $\models _{\overline{X}}$ is defined as follows:

$$\begin{aligned} \mathfrak {A}\models _{\overline{X}} \overline{x}^i \mid \overline{y}^j \Leftrightarrow \forall s\in X_i, s'\in X_j: s(\overline{x}^i)\ne s'(\overline{y}^j). \end{aligned}$$

If $i=j$, then the atom is the standard exclusion atom.

Poly-independence. Let $\overline{x}^i$, $\overline{y}^i$, $\overline{a}^j$,$\overline{b}^j$, $\overline{u}^k$, $\overline{v}^k$, and $\overline{w}^k$ be tuples of variables such that $|\overline{x}^i|=|\overline{a}^j|=|\overline{u}^k|$, $|\overline{y}^i|=|\overline{v}^k|$, $|\overline{b}^j|=|\overline{w}^k|$. Then $\overline{y}^i / \overline{v}^k ~\bot _{\overline{x}^i,\overline{a}^j / \overline{u}^k}~ \overline{b}^j / \overline{w}^k$ is a poly-independence atom whose satisfaction relation $\models _{\overline{X}}$ is defined as follows:

$$\begin{aligned}&\mathfrak {A}\models _{\overline{X}} \overline{y}^i / \overline{v}^k ~\bot _{\overline{x}^i,\overline{a}^j / \overline{u}^k}~ \overline{b}^j / \overline{w}^k \Leftrightarrow \forall s\in X_i, s'\in X_j: s(\overline{x}^i)= s'(\overline{a}^j)\text { implies }\\&\exists s''\in X_k: s''(\overline{u}^k \overline{v}^k)=s(\overline{x}^i \overline{y}^i) \text { and } s''(\overline{w}^k)=s'(\overline{b}^j). \end{aligned}$$

The atom $\overline{y} / \overline{y} ~\bot _{\overline{x},\overline{x} / \overline{x}}~ \overline{z} / \overline{z}$, where all variables are of the same sort, corresponds to the standard independence atom $\overline{y} ~\bot _{\overline{x}}~ \overline{z}$. Furthermore, a pure poly-independence atom is an atom of the form $\overline{y}^i / \overline{v}^k ~\bot _{\emptyset ,\emptyset / \emptyset }~ \overline{b}^j / \overline{w}^k$, written using a shorthand $\overline{y}^i / \overline{v}^k ~\bot _{}~ \overline{b}^j / \overline{w}^k$.

Poly-independence atoms are closely related to equi-join operators of relational databases as the next example exemplifies.

Example 5

A relational database schema

$$\begin{aligned} \textsc {P(rojects)}=\,&\{\texttt {project,team}\}, \quad \textsc {T(eams)}=\{\texttt {team,employee}\},\\ \textsc {E(mployees)}=&\,\{\texttt {employee,team,project}\}, \end{aligned}$$

stores information about distribution of employees for teams and projects in a workplace. The poly-independence atom

$$\begin{aligned} \textsc {P}[\texttt {project}] / \textsc {E}[\texttt {project}] ~\bot _{\textsc {P}[\texttt {team}], \textsc {T}[\texttt {team}] / \textsc {E}[\texttt {team}]}~ \textsc {T}[\texttt {employee}] / \textsc {E}[\texttt {employee}] \end{aligned}$$

(1)

expresses that the relation Employees includes as a subrelation the natural join of Projects and Teams. If furthermore $\textsc {E}[\texttt {project,team}]\subseteq \textsc {P}[\texttt {project,team}]$ and $\textsc {E}[\texttt {team,employee}]\subseteq \textsc {T}[\texttt {team,employee}]$ hold, then Employees is exactly this natural join.

In addition to the poly-atoms described above we define a notion of a generalised poly-atom, similarly to the notion of generalised atom of [21].

Generalised poly-atoms. Let $(j_1, \ldots ,j_n)$ be a sequence of positive integers. A generalised quantifier of type $(j_1, \ldots ,j_n)$ is a collection Q of relational structures $(A,R_1, \ldots ,R_n)$ (where each $R_i$ is $j_i$-ary) that is closed under isomorphisms. Then, for any sequence $(\overline{x}_1, \ldots ,\overline{x}_n)$ where $\overline{x}_i$ is a length $j_i$ tuple of variables from some $\text {Var}(l_i)$, $A_Q(\overline{x}_1,\ldots ,\overline{x}_n)$ is a generalised poly-atom of type $(j_1, \ldots ,j_n)$. For a model $\mathcal {A}$ and polyteam $\overline{X}$ where $\overline{x}_i\subseteq {\mathsf {Dom}(X_{l_i})}$, the satisfaction relation with respect to $A_Q$ is defined as follows:

By ${\mathrm {rel}(X, \overline{x})}$, for $\overline{x} = (x_1, \ldots ,x_m)$, we denote the relation $\{(s(x_1),\ldots ,s(x_m))\mid s\in X\}$. A poly-atom $A_Q(\overline{x}_1,\ldots ,\overline{x}_n)$ is a uni-atom if the variable sequences $\overline{x}_1,\ldots ,\overline{x}_n$ are of a single sort. Uni-atoms correspond exactly to generalised atoms of [21]. We say that the atom $A_Q(\overline{x}_1,\ldots ,\overline{x}_n)$ is definable in a logic $\mathcal {L}$ if the class Q is definable in $\mathcal {L}$. For instance, we notice that a poly-inclusion atom $(x^1,y^1)\subseteq (u^2,v^2)$ is a first-order definable generalised poly-atom of type (2, 2).

2.4 Database Dependencies as Poly-atoms

Embedded dependencies in a multi-relational context can now be studied with the help of generalised poly-atoms and polyteam semantics. Conversely, strong results obtained in the study of database dependencies can be transferred and generalised for stronger results in the polyteam setting. In particular, each embedded dependency can be seen as a defining formula for a generalised poly-atom, and hence the classification of embedded dependencies naturally yield a corresponding classification of generalised poly-atoms. For example, the class

$$\begin{aligned} \mathcal {C}:=\{A_Q(\overline{x}_1,\ldots ,\overline{x}_n) \mid \,&Q \text{ is } \text{ definable } \text{ by } \text{ an } \mathsf {FO}(R_1,\dots ,R_n)\text{-sentence } \text{ in }\\&\text {the class of equality-generating dependencies}\} \end{aligned}$$

is the class of equality-generating poly-atoms. The defining formula of the generalised atom of type (2, 2) that captures the poly-dependence atom of type $=\!\left( x^i,y^i/u^j,v^j\right)$ is

$$ \forall x_1 \forall x_2\forall y_1\forall y_2 \big ((R_1(x_1,x_2) \wedge R_2(y_1,y_2) \wedge x_1=y_1) \rightarrow x_2=y_2\big ). $$

Thus poly-dependence atoms are included in the class of equality-generating poly-atoms.

In order to study data exchange in the polyteam setting, we first need to define the notions of source-to-target and target poly-atoms. This classification of poly-atoms requires some more care as it is not enough to consider the defining formulae of the corresponding atoms, but also the variables that the atom is instantiated with. We will return to this topic briefly after we have given semantics for logics that work on polyteams.

3 Polyteam Semantics for Complex Formulae

We next delineate a version of team semantics suitable for the polyteam context. We note here that it is not a priori clear what sort of modifications for connectives and quantifiers one should entertain when shifting from teams to the polyteam setting.

3.1 Syntax and Semantics

Definition 6

Let $\tau$ be a set of relation symbols. The syntax of poly first-order logic $\mathsf {PFO}(\tau )$ is given by the following grammar rules:

$$ \phi \mathrel {\mathop {{\mathop :}{\mathop :}}}=x= y \mid x \ne y \mid R({\overline{x}}) \mid \lnot R({\overline{x}}) \mid (\phi \wedge \phi ) \mid (\phi \vee \phi ) \mid (\phi \vee ^j\phi ) \mid \exists x \phi \mid \forall x \phi , $$

where $R\in \tau$ is a k-ary relation symbol, $j\in \mathbb {N}$, $\overline{x}\subseteq \text {Var}(i)^k$ and $x,y\in \text {Var}(i)$ for some $i,k\in \mathbb {N}$.

We say that $\vee$ is a global disjunction whereas $\vee ^i$ is a local disjunction. Note that in the definition the scope of negation is restricted to atomic formulae. Note also that the restriction of $\mathsf {PFO}(\tau )$ to formulae without the connective $\vee ^j$ and using only variables of a single fixed sort is $\mathsf {FO}(\tau )$.

For the definition of the polyteam semantics of $\mathsf {PFO}$, recall the definitions of teams and polyteams from Sects. 2.1 and 2.2, respectively. Let X be a team, A a finite set, and $F:X\rightarrow \mathcal {P}(A)\setminus \{\emptyset \}$ a function. We denote by X[A / x] the modified team $\{s(a/x) \mid s\in X, a\in A\}$, and by X[F / x] the team $\{s(a/x)\mid s\in X, a\in F(s)\}$. Again note that if restricted to the above fragment of $\mathsf {PFO}(\tau )$ the polyteam semantics below coincides with traditional team semantics, see e.g. [4] for a definition. Thus for $\mathsf {FO}(\tau )$ formulae we may write $\mathfrak {A}\models _{X_i} \phi$ instead of $\mathfrak {A}\models _{(X_i)} \phi$.

Definition 7

(Lax polyteam semantics). Let $\mathfrak {A}$ be a $\tau$-structure and $\overline{X}$ a polyteam of $\mathfrak {A}$. The satisfaction relation $\models _{\overline{X}}$ for poly first-order logic is defined as follows:

The truth of a sentence $\phi$ (i.e., a formula with no free variables) in a model $\mathfrak {A}$ is defined as: $\mathfrak {A}\models ~\phi \text { if }\mathfrak {A}\models _{(\{\emptyset \})} \phi ,$ where $(\{\emptyset \})$ denotes the polyteam consisting only singleton teams of the empty assignment. We write $\text {Fr}(\phi )$ for the set of free variables in $\phi$, and $\text {Fr}_{i}(\phi )$ for $\text {Fr}(\phi )\cap \text {Var}(i)$.

Polyteam semantics is a conservative extension of team semantics in the same fashion as teams semantics is a conservative extension of Tarski semantics [24].

Proposition 8

Let $\phi \in \mathsf {FO}(\tau )$ whose variables are all of sort $i\in \mathbb {N}$. Let $\mathfrak {A}$ be a $\tau$-structure and $\overline{X}$ a polyteam of $\mathfrak {A}$. Then $\mathfrak {A}\models _{\overline{X}} \phi \,\Leftrightarrow \,\mathfrak {A}\models _{X_i} \phi \,\Leftrightarrow \, \forall s\in X_i: \mathfrak {A}\models _s \phi ,$ where $\models _s$ denotes the ordinary satisfaction relation of first-order logic.

Example 9

A relational database schema

$$\begin{aligned} \textsc {Patient}=&\{\texttt {patient\_id,patient\_name}\},\\ \textsc {Case}=&\{\texttt {case\_id,patient\_id,diagnosis\_id,confirmation}\},\\ \textsc {Test}=&\{\texttt {diagnosis\_id,test\_id}\},\\ \textsc {Results}=&\{\texttt {patient\_id,test\_id,result}\} \end{aligned}$$

stores information about patient cases and their related laboratory tests. In order to maintain consistency of the stored data, database management systems support the use of integrity constraints that are based on functional and inclusion dependencies. For instance, on relation schema $\textsc {Patient}$ the key $\texttt {patient\_id}$ (i.e. the dependence atom $=\!\left( \texttt {patient\_id,patient\_name}\right)$) ensures that no patient id can refer to two different patient names. On $\textsc {Case}$ the foreign key $\texttt {patient\_id}$ referring to $\texttt {patient\_id}$ on $\textsc {Patient}$ (i.e. the inclusion atom $\textsc {Case}[\texttt {patient\_id}]\subseteq \textsc {Patient}[\texttt {patient\_id}]$) enforces that patient ids on $\textsc {Case}$ refer to real patients. The introduction of poly-dependence logics opens up possibilities for more expressive data constraints. The poly-inclusion formula

$$\begin{aligned} \phi _0=&\texttt {confirmation}\ne \textit{positive} \vee _{\textsc {Case}}\exists x_1x_2\big (x_1\ne x_2 \wedge \\&\bigwedge _{i=1,2}(\textsc {Case}[\texttt {diagnosis\_id},x_i]\subseteq \textsc {Test}[\texttt {diagnosis\_id,test\_id}]\wedge \\&\textsc {Case}[\texttt {patient\_id},x_i,positive]\subseteq \textsc {Results}[\texttt {patient\_id,test\_id,result}])\big ) \end{aligned}$$

ensures that a diagnosis may be confirmed only if it has been affirmed by two different appropriate tests. The poly-exclusion formula

$$\begin{aligned}\phi _1=&\texttt {confirmation}\ne \textit{negative} \vee _{\textsc {Case}}\\&\forall x\big (\textsc {Case}[\texttt {diagnosis\_id},x] \mid \textsc {Test}[\texttt {diagnosis\_id,test\_id}]\vee _{\textsc {Case}}\\&\textsc {Case}[\texttt {patient\_id},x,positive] \mid \textsc {Results}[\texttt {patient\_id,test\_id,result}]\big ) \end{aligned}$$

makes sure that a diagnosis may obtain a negative confirmation only if it has no positive indication by any suitable test. Note that both formulae employ local disjunction and quantified variables that refer to $\textsc {Case}$. Interestingly, the illustrated expressive gain is still computationally feasible as both $\phi _0$ and $\phi _1$ can be enforced in polynomial time. For $\phi _0$ note that the data complexity of inclusion logic is in $\mathsf {PTIME}$ [7]; for $\phi _1$ observe that satisfaction of a formula of the form $\overline{x}^1 \mid \overline{y}^2\vee _1 \overline{x}^1 \mid \overline{z}^3$ can be decided in $\mathsf {PTIME}$ as well.

Poly-dependence logics. Poly-dependence, poly-independence, poly-inclusion, and poly-exclusion logics ($\mathsf {PFO}(\mathrm{pdep})$, $\mathsf {PFO}(\mathrm{pind})$, $\mathsf {PFO}(\text {pinc})$, and $\mathsf {PFO}(\mathrm{pexc})$, resp.) are obtained by extending $\mathsf {PFO}$ with poly-dependence, poly-independence, poly-inclusion, and poly-exclusion atoms, respectively. In general, given a set of atoms $\mathcal {C}$ we denote by $\mathsf {PFO}(\mathcal {C})$ the logic obtained by extending $\mathsf {PFO}$ with the atoms of $\mathcal {C}$. We also consider poly-atoms in the team semantics setting; by $\mathsf {FO}(\mathcal {C})$ we denote the extension of first-order logic by the poly-atoms in $\mathcal {C}$. Similarly, it is also possible to consider atoms of Sect. 2.1 in the polyteam setting by requiring that the variables used with each atom are of a single sort.

3.2 Basic Properties

We say that a formula $\phi$ is local in polyteam semantics if for all $\overline{V}=(V_i)_{i\in \mathbb {N}}$ where $\text {Fr}_{i}(\phi )\subseteq V_i$ for $i\in \mathbb {N}$, and all models $\mathfrak {A}$ and polyteams $\overline{X}$, we have

$$\begin{aligned} \mathfrak {A}\models _{\overline{X}} \phi \Leftrightarrow \mathfrak {A}\models _{\overline{X} \upharpoonright \overline{V}}\phi . \end{aligned}$$

In other words, the truth value of a local formula depends only on its free variables. Furthermore, a logic $\mathcal {L}$ is called local if all its formulae are local.

Proposition 10

(Locality). For any set $\mathcal {C}$ of generalised poly-atoms $\mathsf {PFO}(\mathcal {C})$ is local.

Furthermore, the downward closure of dependence logic as well as the union closure of inclusion logic generalise to polyteams.

Proposition 11

(Downward Closure and Union Closure). Let $\phi$ be a formula of $\mathsf {PFO}(\mathrm{pdep})$, $\psi$ a formula of $\mathsf {PFO}(\text {pinc})$, $\mathfrak {A}$ a model, and $\overline{X},\overline{Y}$ two polyteams. Then $\mathfrak {A}\models _{\overline{X}}\phi$ and $\overline{Y} \subseteq \overline{X}$ implies that $\mathfrak {A}\models _{\overline{Y}}\phi$, and $\mathfrak {A}\models _{\overline{X}} \psi$ and $\mathfrak {A}\models _{\overline{Y}}\psi$ implies that $\mathfrak {A}\models _{\overline{X}\cup \overline{Y}}\psi$.

The following proposition shows that the substitution of independence (dependence) atoms for any (downwards closed) class of atoms definable in existential second-order logic ($\mathsf {ESO}$) results in no expressive gain.

Proposition 12

Let $\mathcal {C}$ ($\mathcal {D}$, resp.) be the class of all (all downward closed, resp.) $\mathsf {ESO}$-definable poly-atoms. The following equivalences of logics hold: $\mathsf {FO}(\mathcal {C}) \equiv \mathsf {FO}(\mathrm{ind})$, $\mathsf {FO}(\mathcal D) \equiv \mathsf {FO}(\mathrm{dep})$, and $\mathsf {FO}(\text {pinc}) \equiv \mathsf {FO}(\mathrm{inc})$.

Proof

The claim $\mathsf {FO}(\text {pinc}) \equiv \mathsf {FO}(\mathrm{inc})$ follows directly from the observation that in the team semantics setting poly-inclusion atoms are exactly inclusion atoms. Note that $\mathsf {FO}(\mathrm{ind})$ ($\mathsf {FO}(\mathrm{dep})$, resp.) captures all (all downward closed, resp.) $\mathsf {ESO}$-definable properties of teams (see Theorem 18). It is easy to show (cf. [17, Theorem 6]) that every property of teams definable in $\mathsf {FO}(\mathcal {C})$ ($\mathsf {FO}(\mathcal {D})$, resp.) is $\mathsf {ESO}$-definable ($\mathsf {ESO}$-definable and downward closed, resp.). Thus since $\mathrm{ind}\in \mathcal {C}$ and $\mathrm{dep}\in \mathcal {D}$, we obtain that $\mathsf {FO}(\mathcal {C}) \equiv \mathsf {FO}(\mathrm{ind})$ and $\mathsf {FO}(\mathcal {D}) \equiv \mathsf {FO}(\mathrm{dep})$.   $\square$

Remark 13

In particular it follows from the previous proposition that, in the polyteam setting, each occurrence of any (any downward closed, resp.) $\mathsf {ESO}$-definable poly-atom that takes variables of a single sort as parameters may be equivalently expressed by a formula of $\mathsf {PFO}(\mathrm{ind})$ ($\mathsf {PFO}(\mathrm{dep})$, resp.) that only uses variables of the same single sort.

We end this section by considering the relationship of global and local disjunctions. In particular, we observe that by the introduction of local disjunction its global variant becomes redundant. To facilitate our construction we here allow the use of $\vee ^I$, where I is a set on indices, with obvious semantics. We then show that $\vee$ can be replaced by $\vee ^I$ and $\vee ^I$ by $\vee ^i$.

Proposition 14

For every formula of $\mathsf {PFO}$ there exists an equivalent formula of $\mathsf {PFO}$ that only uses disjunctions of type $\vee ^i$.

Proof

Let $\phi$ be a formula of $\mathsf {PFO}$ and let I list the sorts of all the variables that occur in $\phi$. Let $\phi ^*$ denote the formula obtained from $\phi$ by substituting all occurrences of $\vee$ by $\vee ^I$. It is a direct consequence of the locality property that $\phi$ and $\phi ^*$ are equivalent.

We will next show how to eliminate disjunctions of type $\vee ^I$ from $\phi ^*$. Let $\phi _0 \vee ^I \phi _1$ be a formula of $\mathsf {PFO}$ and let $I=\{i_1,\dots ,i_n\}$. Define

$$ \psi := \exists z^{i_1}_0\exists z^{i_1}_1 \dots \exists z^{i_n}_0\exists z^{i_n}_1 (\theta _0 \wedge \theta _1), $$

where $z^{i_1}_0$, $z^{i_1}_1$, ..., $z^{i_n}_0$, $z^{i_n}_1$ are fresh and distinct variables, and

The idea above is that the variables $z^{i_j}_0$, $z^{i_j}_1$ are used to encode a split of the team $X_j$. Using locality it is easy to see that $(\phi _0 \vee ^I \phi _1)$ and $\psi$ are equivalent over structures of cardinality at least two. From this the claim follows in a straightforward manner.   $\square$

3.3 Data Exchange in the Polyteam Setting

As promised, we now return to the topic of modelling data exchange in our new setting. In this section we restrict our attention to poly-atoms that are embedded dependencies. Our first goal is to define the notions of source-to-target and target poly-atoms. For this purpose we define a normal form for embedded dependencies. We call an embedded dependency $\forall \overline{x} \big (\phi (\overline{x}) \rightarrow \exists \overline{y} \psi (\overline{x},\overline{y})\big )$ separated if the relation symbols that occur in $\phi$ and $\psi$ are distinct. A poly-atom is called separated, if the defining formula is a separated embedded dependency. In the polyteam setting this is just a technical restriction as non-separated poly-atoms can be always simulated by separated ones. Below we use the syntax $A(\overline{x}_1,\dots , \overline{x}_l, \overline{y}_1,\dots , \overline{y}_k)$ for separated poly-atoms. The idea is that $\overline{x}_i$s project extensions for relations used in the antecedent and $\overline{y}_j$s in the consequent of the defining formula.

Let $\mathcal S$ and $\mathcal T$ be a set of source relations and target relations from some data exchange instance, respectively. Let $\overline{X}=(S_1, \dots S_n, T_1,\dots ,T_m)$ be a polyteam that encodes $\mathcal S$ and $\mathcal T$ in the obvious manner. We say that an instance of a separated atom $A(\overline{x}_1,\dots , \overline{x}_l, \overline{y}_1,\dots , \overline{y}_k)$ is source-to-target if each $\overline{x}_i$ is a tuple of variables of the sort of $S_j$, for some j, and each $\overline{y}_i$ is a tuple of variables of the sort of $T_j$, for some j. Analogously the instance $A(\overline{x}_1,\dots , \overline{x}_l, \overline{y}_1,\dots , \overline{y}_k)$ is target if each $\overline{x}_i$ and $\overline{y}_j$ is a tuple of variables of the sort of $T_p$ for some p.

Data exchange problems can now be directly studied in the polyteam setting. For example the existence-of-solution problem can be reduced to a model checking problem by using first-order quantifiers to guess a solution for the problem while the rest of the formula describes the dependences required to be fulfilled in the data exchange problem.

Example 15

A relational database schemas

$$\begin{aligned}&\mathcal S:\quad \textsc {P(rojects)}=\{\texttt {name, employee, employee\_position}\},\\&\mathcal T:\quad \textsc {E(mployees)}=\{\texttt {name, project\_1, project\_2}\} \end{aligned}$$

are used to store information about employees positions in different projects. We wish to check whether for a given instance of the schema $\mathcal S$ there exists an instance of the schema $\mathcal T$ that does not lose any information about for which projects employees are tasked to work and that uses the attribute name as a key. The $\mathsf {PFO}(\text {pinc}, \mathrm{dep})$-formula

when evaluated on a polyteam that encodes an instance of the schema $\mathcal S$, expresses that a solution for the data exchange problem exists. The variables $x_1$, $x_2$ and $x_3$ above are of the sort E and are used to encode attribute names name, project_1 and project_2, respectively. The dependence atom above enforces that the attribute name is a key.

4 Expressiveness

The expressiveness properties of dependence, independence, inclusion, and exclusion logic and their fragments enjoy already comprehensive classifications. Dependence logic and exclusion logic are equi-expressive and capture all downward closed $\mathsf {ESO}$ properties of teams [6, 19]. Independence logic, whose independence atoms violate downward closure, in turn captures all $\mathsf {ESO}$ team properties [6]. On the other hand, the expressivity of inclusion logic has been characterised by the so-called greatest fixed point logic [7]. In this section we turn attention to polyteams and consider the expressivity of the poly-dependence logics introduced in this paper. Section 4.1 deals with logics with only uni-dependencies whereas in Sect. 4.2 poly-dependencies are considered.

4.1 Uni-dependencies in Polyteam Semantics

The following theorem displays how polyteam semantics over logics with only uni-atoms collapses to standard team semantics.

Theorem 16

Let $\mathcal {C}$ be a set of uni-atoms. Each formula $\phi (\overline{x}^1, \ldots ,\overline{x}^n)\in \mathsf {PFO}(\mathcal {C})$ can be associated with a sequence of formulae $\psi _1(\overline{x}^1), \ldots ,\psi _n(\overline{x}^n) \in \mathsf {FO}(\mathcal {C})$ such that for all $\overline{X}=(X_1, \ldots ,X_n)$, where $X_i$ is a team with domain $\overline{x}^i$,

$$\begin{aligned} \mathcal {M}\models _{\overline{X}} \phi (\overline{x}^1, \ldots ,\overline{x}^n) \Leftrightarrow \forall i=1, \ldots ,n: \mathcal {M}\models _{X_i} \psi _i(\overline{x}^i). \end{aligned}$$

Similarly, the statement holds vice versa.

Proof

The latter statement is clear as it suffices to set $\phi (\overline{x}^1, \ldots ,\overline{x}^n):= \psi _1(\overline{x}^1)\wedge \ldots \wedge \psi _n(\overline{x}^n)$. For the other direction, we define recursively functions $f_i$ that map formulae $\phi (\overline{x}^1, \ldots ,\overline{x}^n) \in \mathsf {PFO}(\mathcal {C})$ to formulae $\psi _i(\overline{x}^i) \in \mathsf {FO}(\mathcal {C})$. By Proposition 14 we may assume that only disjunctions of type $\vee ^i$, for some $i\in \mathbb {N}$, may occur in $\phi$. The functions $f_i$ are defined as follows:

• If $\phi (\overline{x}^j)$ is an atom, then $f_i(\phi )={\left\{ \begin{array}{ll}\phi &{}\text {if }i=j,\\ \top &{}\text {otherwise.}\end{array}\right. }$

• $f_i(\psi \vee ^j \theta )={\left\{ \begin{array}{ll}f_i(\psi ) \vee f_i(\theta ) &{}\text {if }i=j,\\ f_i(\psi ) \wedge f_i(\theta ) &{}\text {otherwise.}\end{array}\right. }$

• $f_i(\psi \wedge \theta )=f_i(\psi )\wedge f_i(\theta )$.

• For $Q\in \{\exists ,\forall \}$, if $f_i(Q x^j \psi )={\left\{ \begin{array}{ll}Q x f_i(\psi ) &{}\text {if }i=j,\\ f_i(\psi ) &{}\text {otherwise.}\end{array}\right. }$

We set $\psi _i:=f_i(\phi )$ and show the claim by induction on the structure of the formula. The cases for atoms and conjunctions are trivial. We show the case for $\vee ^i$.

Let $\phi =\psi \vee ^j\theta$ and assume that the claim holds for $\psi$ and $\theta$. Now

$$\begin{aligned} \mathfrak {A}\models _{\overline{X}} \phi \quad \mathrm{iff }\quad&{\mathfrak {A}\models _{\overline{X}[Y_j/X_j]}\psi \, \mathrm{and}\, \mathfrak {A}\models _{\overline{X}[Z_j/X_j]}\theta ,} \\&\mathrm{for\, some\,} Y_j,Z_j\subseteq X_j\, \mathrm{such \,that}\, Y_j\cup Z_j = X_j. \end{aligned}$$

By the induction hypothesis, $\mathfrak {A}\models _{\overline{X}[Y_j/X_j]}\psi$ and $\mathfrak {A}\models _{\overline{X}[Z_j/X_j]}\theta$ iff $\mathfrak {A}\models _{Y_j} f_j(\psi )$, $\mathfrak {A}\models _{Z_j} f_j(\theta )$, and $\mathfrak {A}\models _{X_i} f_i(\psi ), \mathfrak {A}\models _{X_i} f_i(\theta )$ for each $i\ne j$. Thus we obtain that $\mathfrak {A}\models _{\overline{X}} \phi$ holds iff

$$ \mathfrak {A}\models _{X_j} f_j(\psi )\vee f_j(\theta ), \text { and } \mathfrak {A}\models _{X_i} f_i(\psi ) \text { and } \mathfrak {A}\models _{X_i} f_i(\theta ) \text { for each } i\ne j. $$

The above can be rewritten as

$$ \mathfrak {A}\models _{X_j} f_j(\psi )\vee f_j(\theta ), \text { and } \mathfrak {A}\models _{X_i} f_i(\psi ) \wedge f_i(\theta ) \text { for each } i\ne j. $$

The claim now follows, since $f_j(\psi )\vee f_j(\theta )= f_j(\psi \vee ^j \theta )$ and $f_i(\psi )\wedge f_i(\theta )= f_i(\psi \vee ^j \theta )$, for $i\ne j$.

The cases for the quantifiers are similar.

This theorem implies that poly-atoms which describe relations between two teams are beyond the scope of uni-logics. The following proposition illustrates this for $\mathsf {PFO}(\mathrm{dep})$.

Proposition 17

The poly-constancy atom $=\!\left( x^1/x^2\right)$ cannot be expressed in $\mathsf {PFO}(\mathrm{dep})$.

Proof

Assume that $=\!\left( x^1/x^2\right)$ can be defined by some $\phi (x^1,x^2)\in \mathsf {PFO}(\mathrm{dep})$. By Theorem 16 there are $\mathsf {FO}(\mathrm{dep})$-formulae $\psi _1( x^1)$ and $\psi _2( x^2)$ such that for all $\overline{X}=(X_1,X_2)$, where $X_i$ is a team with domain $x^i$, it holds that

$$\begin{aligned} \mathcal {M}\models _{\overline{X}} =\!\left( x^1/x^2\right) \Leftrightarrow \forall i=1,2 : \mathcal {M}\models _{X_i} \psi _i( x^i). \end{aligned}$$

(2)

Define teams $X_1:=\{x^1\mapsto 0\}$, $X_2:=\{x^2\mapsto 0\}$, $Y_1:=\{x^1\mapsto 1\}$, and $Y_2:=\{x^2\mapsto 1\}$. Now clearly $\mathcal {M}\models _{(X_1,X_2)} =\!\left( x^1/x^2\right)$, and $\mathcal {M}\models _{(Y_1,Y_2)} =\!\left( x^1/x^2\right)$. Hence by (2), we obtain first that $\mathcal {M}\models _{X_1} \psi _i( x^1) \text { and } \mathcal {M}\models _{Y_2} \psi _i( x^2)$, and then that $\mathcal {M}\models _{(X_1,Y_2)} =\!\left( x^1/x^2\right)$, which is a contradiction.   $\square$

Using Theorem 16 we may now compare and characterise the expressivity of $\mathsf {PFO}(\mathrm{dep})$ and $\mathsf {PFO}(\mathrm{ind})$ in terms of existential second-order logic. To this end, let us first recall the $\mathsf {ESO}$ characterisations of open dependence and independence logic formulae. Note that ${\mathrm {rel}(X)}$ refers to a relation $\{s(x_1, \ldots , x_n)\mid s\in X\}$ where $x_1, \ldots ,x_n$ is some enumeration of ${\mathsf {Dom}(X)}$.

Theorem 18

([6, 19]). Let $\phi (\overline{x})$ be an independence logic (dependence logic, resp.) formula, and let R be an $|\overline{x}|$-ary relation. Then there is an (downward closed with respect to R, resp.) $\mathsf {ESO}$-sentence $\psi (R)$ such that for all teams $X\ne \emptyset$ where ${\mathsf {Dom}(X)}=\overline{x}$,

$$\begin{aligned} \mathcal {M}\models _X \phi (\overline{x}) \Leftrightarrow (\mathcal {M}, R:={\mathrm {rel}(X)})\models \psi (R) \end{aligned}$$

The same statement holds also vice versa.

It is now easy to see that Theorems 16 and 18 together imply that $\mathsf {PFO}(\mathrm{dep})$ captures all conjunctions of downward closed $\mathsf {ESO}$ properties of teams whereas $\mathsf {PFO}(\mathrm{ind})$ captures all such properties.

Theorem 19

Let $\phi (\overline{x}^1, \ldots ,\overline{x}^n)$ be a $\mathsf {PFO}(\mathrm{ind})$ ($\mathsf {PFO}(\mathrm{dep})$, resp.) formula where $\overline{x}^i$ is a sequence of variables from $\text {Var}(i)$. Let $R_i$ be an $|\overline{x}^i|$-ary relation symbol for $i=1, \ldots ,n$. Then there are (downward closed with respect to $R_i$, resp.) $\mathsf {ESO}$-sentences $\psi _1(R_1), \ldots ,\psi _n(R_n)$ such that for all polyteams $\overline{X}=(X_1, \ldots ,X_n)$ where ${\mathsf {Dom}(X_i)}=\overline{x}^i$ and $X_i\ne \emptyset$

The same statement holds also vice versa.

4.2 Poly-dependencies in Polyteam Semantics

Next we consider poly-dependencies in polyteam semantics.

Lemma 20

The following equivalences hold:

$$\begin{aligned} =\!\left( \overline{x}^1,\overline{y}^1/\overline{u}^2,\overline{v}^2\right) \equiv&\overline{y}^1 / \overline{y}^1 ~\bot _{\overline{x}^1, \overline{u}^2 / \overline{x}^1}~ \overline{v}^2 / \overline{y}^1,\end{aligned}$$

(3)

$$\begin{aligned} =\!\left( \overline{x}^1,y^1/\overline{u}^2,v^2\right) \equiv&\forall z^1(y^1 = z^1 \vee ^1 \overline{x}^1 z^1 \mid \overline{u}^2 v^2),\end{aligned}$$

(4)

$$\begin{aligned} \overline{x}^1\subseteq \overline{u}^2 \equiv& \overline{x}^1 / \overline{u}^2 ~\bot ~ \emptyset / \emptyset ,\end{aligned}$$

(5)

$$\begin{aligned} \overline{x}^1\subseteq \overline{u}^2 \equiv& \forall \overline{v}^2(\overline{x}^1 \mid \overline{v}^2 \vee ^2 \overline{v}^2\subseteq \overline{u}^2),\end{aligned}$$

(6)

$$\begin{aligned} \overline{x}^1 \mid \overline{u}^2 \equiv& \exists y^1 z^1 v^2 w^2 (=\!\left( \overline{x}^1,y^1z^1/\overline{u}^2,v^2w^2\right) \\&\quad \wedge y^1=z^1 \wedge v^2\ne w^2),\nonumber \end{aligned}$$

(7)

$$\begin{aligned} \overline{x}^1 \mid \overline{u}^2 \equiv& \exists \overline{y}^1(\overline{u}^2 \subseteq \overline{y}^1 \wedge \overline{x}^1 \mid \overline{y}^1), \end{aligned}$$

(8)

$$\begin{aligned} \overline{y}^2 / \overline{y}^1 ~\bot _{\overline{x}^2,\overline{x}^3 / \overline{x}^1}~ \overline{z}^3 / \overline{z}^1\equiv&\forall \overline{p}^2\overline{q}^2 \exists u^2 v^2\forall \overline{p}^3\overline{q}^3\overline{r}^3 \exists u^3 v^3 \Big ( \\&=\!\left( \overline{p}^2\overline{q}^2,u^2v^2/\overline{p}^3\overline{q}^3 ,u^3v^3\right) \nonumber \\&\wedge \big (u^2 =v^2\vee ^1(u^2\ne v^2 \wedge \overline{x}^2 \overline{y}^2 \mid \overline{p}^2\overline{q}^2)\big ) \nonumber \\&\wedge \big (u^3 \ne v^3 \vee ^2 \overline{x}^3 \overline{z}^3 \mid \overline{p}^3\overline{r}^3 \vee ^2 \overline{p}^3\overline{q}^3\overline{r}^3 \subseteq \overline{x}^1\overline{y}^1\overline{z}^1\big )\Big ).\nonumber \end{aligned}$$

(9)

Proof

The equivalences (3)–(8) are straightforward and (9) is analogous to the corresponding translation in the team semantics setting (see [6]).   $\square$

The following theorem compares the expressive powers of different polyteam-based logics. Observe that the expressivity of the logics with two poly-dependency atoms remains the same even if either one of the atoms has the standard team semantics interpretation.

Theorem 21

The following equivalences of logic hold:

• (1) $\mathsf {PFO}(\mathrm{pdep}) \equiv \mathsf {PFO}(\mathrm{pexc})$,

• (2) $\mathsf {PFO}(\mathrm{pind}) \equiv \mathsf {PFO}(\mathrm{pexc},\mathrm{inc}) \equiv \mathsf {PFO}(\text {pinc},\mathrm{exc}) \equiv \mathsf {PFO}(\mathrm{pdep},\mathrm{inc})$ $\equiv \mathsf {PFO}(\text {pinc},\mathrm{dep}) \equiv \mathsf {PFO}(\mathrm{pdep},\mathrm{ind}) \equiv \mathsf {PFO}(\mathrm{pexc},\mathrm{ind}) \equiv \mathsf {PFO}(\text {pinc},\mathrm{ind})$.

Proof

Item (1) follows by Eqs. (4) and (7). Item (2) follows from the below list of relationships:

• $\mathsf {PFO}(\mathrm{pind})\subseteq \mathsf {PFO}(\mathrm{pexc},\mathrm{inc})$ by (4), (6), and (9).

• $\mathsf {PFO}(\mathrm{pexc},\mathrm{inc}) \equiv \mathsf {PFO}(\text {pinc},\mathrm{exc})$ by (6) and (8).

• $\mathsf {PFO}(\mathrm{pexc},\mathrm{inc}) \equiv \mathsf {PFO}(\mathrm{pdep},\mathrm{inc})$ by (4) and (7).

• $\mathsf {PFO}(\text {pinc},\mathrm{exc}) \equiv \mathsf {PFO}(\text {pinc},\mathrm{dep})$, since exclusion (dependence, resp.) atoms can be described in $\mathsf {FO}(\mathrm{dep})$ ($\mathsf {FO}(\mathrm{exc})$, resp.) [6].

• $\mathsf {PFO}(\mathrm{pdep},\mathrm{inc})\subseteq \mathsf {PFO}(\mathrm{pdep},\mathrm{ind})$, $\mathsf {PFO}(\mathrm{pexc},\mathrm{inc})\subseteq \mathsf {PFO}(\mathrm{pexc},\mathrm{ind})$, and $\mathsf {PFO}(\text {pinc},\mathrm{dep})\subseteq \mathsf {PFO}(\text {pinc},\mathrm{ind})$ since inclusion atoms can be described in $\mathsf {FO}(\mathrm{ind})$ [6] and dependence atoms by independence atoms [9].

• $\mathsf {PFO}(\mathrm{pdep},\mathrm{ind})\subseteq \mathsf {PFO}(\mathrm{ind})$, $\mathsf {PFO}(\mathrm{pexc},\mathrm{ind})\subseteq \mathsf {PFO}(\mathrm{ind})$, and $\mathsf {PFO}(\text {pinc},\mathrm{ind})$ $\subseteq \mathsf {PFO}(\mathrm{pind})$ by (3), (5), and (7).   $\square$

Next we show the analogue of Theorem 18 for polyteams.

Theorem 22

Let $\phi (R_1, \ldots ,R_n)$ be an $\mathsf {ESO}$-sentence. There is a $\mathsf {PFO}(\mathrm{pdep},\mathrm{inc})$ formula $\phi ^*(\overline{x}^1, \ldots ,\overline{x}^n)$, where $|\overline{x}^i|={\mathrm {ar}(R_i)}$, such that for all polyteams $\overline{X}=(X_1, \ldots ,X_n)$ with ${\mathsf {Dom}(X_i)}=\overline{x}^i$ and $X_i\ne \emptyset$,

$$\begin{aligned} \mathcal {M}\models _{\overline{X}} \phi ^*(\overline{x}^1, \ldots ,\overline{x}^n) \Leftrightarrow (\mathcal {M}, R_1:={\mathrm {rel}(X_1)}, \ldots ,R_n:={\mathrm {rel}(X_n)})\models \phi (R_1, \ldots ,R_n). \end{aligned}$$

The statement holds also vice versa.

Proof

The direction from $\mathsf {PFO}(\mathrm{pdep},\mathrm{inc})$ to $\mathsf {ESO}$ is proven by a translation similar to the one from dependence logic to $\mathsf {ESO}$ in [24]. We show only the opposite direction. Analogously to [6], we can rewrite $\phi (R_1, \ldots ,R_n)$ as

$$\begin{aligned} \exists \overline{f} \forall \overline{u} \big ( \bigwedge _{i=1}^{n} (R_i(\overline{u}_i) \leftrightarrow f_{2i-1}(\overline{u}_i)=f_{2i}(\overline{u}_i))\wedge \psi (\overline{u}, \overline{f})\big ) \end{aligned}$$

where $\overline{f}=f_1, \ldots ,f_{2n}, \ldots ,f_m$ is a list of function variables, $\psi$ is a quantifier-free formula in which no $R_i$ appears, each $\overline{u}_i$ is a subsequence of $\overline{u}$, and each $f_i$ occurs only as $f_i(\overline{u}_{j_i})$ for some fixed tuple $\overline{u}_{j_i}$ of variables. For instance, $j_i= i/2$ for even $i\le 2n$.

Let $\overline{b}^i$ be sequences of variables of sort i such that $|\overline{b}^i|=|\overline{u}_i|$, and let $\overline{u}^1 \overline{y}^1$ be a sequence of variables of sort 1 such that $\overline{u}^1$ is a copy of $\overline{u}$ and $\overline{y}^1=y^1_1, \ldots , y^1_m$. We define $\phi ^*(\overline{x}^1, \ldots ,\overline{x}^n)$ as the formula

$$ \forall \overline{b}^1\exists z^1_0z^1_1\ldots \forall \overline{b}^n\exists z^n_0z^n_1 \forall \overline{u}^1\exists \overline{y}^1\big ( \theta _0 \wedge \theta _1\wedge \psi '(\overline{u}^1, \overline{y}^1) ) $$

where

$$\begin{aligned} \theta _0 :=&\bigwedge _{i=1}^n =\!\left( \overline{b}^i,z^i_0\right) \wedge =\!\left( \overline{b}^i,z^i_1\right) \wedge ((\overline{b}^i \subseteq \overline{x}^i\wedge z^i_0 = z^i_1) \vee ^i (\overline{x}^i \mid \overline{b}^i \wedge z^i_0\ne z^i_1)),\\ \theta _1:=&\bigwedge _{i=1}^n=\!\left( \overline{u}^1_i,y^1_{2i-1}/\overline{b}^i,z^i_0\right) \wedge =\!\left( \overline{u}^1_i,y^1_{2i}/\overline{b}^i,z^i_1\right) \wedge \bigwedge _{i=n+1}^m =\!\left( \overline{u}^1_{j_i},y^1_i\right) , \end{aligned}$$

and $\psi '(\overline{u}^1, \overline{y}^1)$ is obtained from $\psi (\overline{u}, \overline{f})$ by replacing $\overline{u}$ pointwise with $\overline{u}^1$ and each $f_i(\overline{u}_{j_i})$ with $y^1_i$. Above, $\theta _0$ amounts to the description of the characteristic functions $f_{2i-1}$ and $f_{2i}$. We refer the reader to [6] to check that $\mathcal {M}\models _{\overline{X}} \theta _0$ iff for all i the functions $s(\overline{b}^i)\mapsto s(z^i_0)$ and $s(\overline{b}^i)\mapsto s(z^i_1)$ determined by the assignments $s\in X_i$ agree on $s(\overline{b}^i)$ exactly when $s(\overline{b}^i)\in {\mathrm {rel}(X_i)}$. The poly-dependence atoms in $\theta _1$ then transfer these functions over to the first team, and the dependence atoms in $\psi _1$ describe the remaining functions. As in [6], it can now be seen that $\phi ^*$ correctly simulates $\phi$. Since exclusion atoms can be expressed in dependence logic, the claim then follows.   $\square$

By item (2) of Theorem 21 the result of Theorem 22 extends to a number of other logics as well. For instance, we obtain that poly-independence logic captures all $\mathsf {ESO}$ properties of polyteams. The proof of Theorem 22 can be now easily adapted to show that poly-exclusion and poly-dependence logic capture all downward closed $\mathsf {ESO}$ properties of polyteams.

Theorem 23

Let $\phi (R_1, \ldots ,R_n)$ be an $\mathsf {ESO}$-sentence that is downward closed with respect to $R_i$. Then there is a $\mathsf {PFO}(\mathrm{pdep})$-formula $\phi ^*(\overline{x}^1, \ldots ,\overline{x}^n)$, where $|\overline{x}^i|={\mathrm {ar}(R_i)}$, such that for all polyteams $\overline{X}=(X_1, \ldots ,X_n)$ with ${\mathsf {Dom}(X_i)}=\overline{x}^i$ and $X_i\ne \emptyset$,

$$\begin{aligned} \mathcal {M}\models _{\overline{X}} \phi ^*(\overline{x}^1, \ldots ,\overline{x}^n) \Leftrightarrow (\mathcal {M}, R_1:={\mathrm {rel}(X_1)}, \ldots ,R_n:={\mathrm {rel}(X_n)})\models ~\phi (R_1, \ldots ,R_n). \end{aligned}$$

The statement holds also vice versa.

Proof

The direction from $\mathsf {PFO}(\mathrm{pdep})$ to $\mathsf {ESO}$ is again similar to the standard translation of [24]. For the other direction, let $\phi (R_1, \ldots ,R_n)$ be an $\mathsf {ESO}$-sentence in which the relations $R_i$ appear only negatively. As in the proof of Theorem 22 and by downward closure we may transform it to an equivalent form (see [19] for details)

$$\begin{aligned} \exists \overline{f} \forall \overline{u} \big ( \bigwedge _{i=1}^{n} (\lnot R_i(\overline{u}_i) \vee f_{2i-1}(\overline{u}_i)=f_{2i}(\overline{u}_i))\wedge \psi (\overline{u}, \overline{f})\big ) \end{aligned}$$

Now the translation $\phi (\overline{x}^1, \ldots ,\overline{x}^n)$ is defined analogously to the proof of Theorem 22 except for $\theta _0$ which is redefined as

$$\begin{aligned} \theta _0 := \bigwedge _{i=1}^n =\!\left( \overline{b}^i,z^i_0\right) \wedge =\!\left( \overline{b}^i,z^i_1\right) \wedge (\overline{x}^i \mid \overline{b}^i \vee ^i z^i_0= z^i_1). \end{aligned}$$

Finally the claim follows by eliminating the exclusion atoms from $\theta _0$.

5 Conclusion

In this article we have laid the foundations of polyteam semantics in order to facilitate the fruitful exchange of ideas and results between team semantics and database theory. Our results show that many of the familiar properties and results from team semantics carry over to the polyteam setting. In particular, we identified a natural polyteam analogue of dependence atoms and gave a complete axiomatisation for the associated implication problem. It is an interesting task to develop axiomatic characterisations for these new logics (cf. [10, 20]). Another interesting issue is to study the expressive power of various syntactic fragments of logics over polyteams.