Polyteam Semantics

TL;DR

This paper introduces Polyteam Semantics, a new framework evaluating formulas over families of teams, advancing the understanding of dependence and independence logics and their relation to database theory.

Contribution

It defines a novel polyteam variant of dependence atoms, provides a finite axiomatisation, and characterizes the expressive power of poly-dependence and poly-independence logics.

Findings

Finite axiomatisation for the implication problem of polyteam dependence atoms

Poly-dependence and poly-independence logics characterize properties downwards closed and ESO-definable

Poly-inclusion logic relates to greatest fixed point logic

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 relate polyteam semantics to team semantics and investigate in which cases logics over the former can be simulated by logics over the latter. We also characterise the expressive power of poly-dependence logic by properties of polyteams that are downwards closed and definable in existential second-order logic (ESO). The analogous result is shown to hold for poly-independence logic and all ESO-definable properties. We also relate poly-inclusion logic to greatest fixed point logic.

Equations

$$\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{)},$$

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

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

$$\mathfrak{A}{\models }_X\overline{x}\subseteq \overline{y}\text{ if for all }s\in X\text{ there exists }{s}^{\prime }\in X\text{ such that }s(\overline{x})=s^{\prime }(\overline{y}).$$

$$\mathfrak{A}{\models }_X\overline{x}\mid \overline{y}\text{ if for all }s,s^{\prime }\in X:s(\overline{x})\ne s^{\prime }(\overline{y}).$$

$$\mathfrak{A}{\models }_X\overline{y}{\perp }_{\overline{x}}\overline{z}\text{ if for all }s,s^{\prime }\in X\text{ such that }s(\overline{x})=s^{\prime }(\overline{x})\text{ there exists }{s}^{\prime \prime }\in X$$

$$\text{ such that }{s}^{\prime \prime }(\overline{x})=s(\overline{x})\text{, }{s}^{\prime \prime }(\overline{y})=s(\overline{y}),\text{ and }{s}^{\prime \prime }(\overline{z})=s^{\prime }(\overline{z}).$$

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

$$\mathfrak{A}{\models }_{\overline{X}}{\overline{x}}^i\subseteq {\overline{y}}^j\iff \forall s\in X_i\exists s^{\prime }\in X_j:s({\overline{x}}^i)=s^{\prime }({\overline{y}}^j).$$

$$\mathfrak{A}{\models }_{\overline{X}}{\overline{x}}^i\mid {\overline{y}}^j\iff \forall s\in X_i,s^{\prime }\in X_j:s({\overline{x}}^i)\ne s^{\prime }({\overline{y}}^j).$$

$$\mathfrak{A}{\models }_{\overline{X}}{\overline{y}}^i/{\overline{v}}^k{\perp }_{{\overline{x}}^i,{\overline{a}}^j/{\overline{u}}^k}{\overline{b}}^j/{\overline{w}}^k\iff \forall s\in X_i,s^{\prime }\in X_j:s({\overline{x}}^i)=s^{\prime }({\overline{a}}^j)\text{ implies }$$

$$\exists s^{\prime \prime }\in X_k:s^{\prime \prime }({\overline{u}}^k{\overline{v}}^k)=s({\overline{x}}^i{\overline{y}}^i)\text{ and }{s}^{\prime \prime }({\overline{w}}^k)=s^{\prime }({\overline{b}}^j).$$

$$\text{textsc}P(rojects)=$$

$$\text{textsc}E(mployees)=$$

$$\text{textsc}P[\text{project}]/\text{textsc}E[\text{project}]{\perp }_{\text{textsc}P[\text{team}],\text{textsc}T[\text{team}]/\text{textsc}E[\text{team}]}\text{textsc}T[\text{employee}]/\text{textsc}E[\text{employee}]$$

$$\mathfrak{A}\models_{\overline{X}}\alpha_{Q}(\overline{x}_{1},\ldots,\overline{x}_{n})\Leftrightarrow\Big{(}{\mathsf{Dom}(\mathfrak{A})},R_{1}:={\mathrm{rel}(X_{l_{1}},\overline{x}_{1})}\ldots,R_{n}:={\mathrm{rel}(X_{l_{n}},\overline{x}_{n})}\Big{)}\in Q.$$

$$\mathcal{C}:=\{{\alpha }_Q({\overline{x}}_1,\dots ,{\overline{x}}_n)\mid$$

$$\text{the class of equality-generating dependencies}\}$$

$$\forall x_{1}\forall x_{2}\forall y_{1}\forall y_{2}\big{(}(R_{1}(x_{1},x_{2})\land R_{2}(y_{1},y_{2})\land x_{1}=y_{1})\rightarrow x_{2}=y_{2}\big{)}.$$

$$\varphi ::=x=y\mid x\ne y\mid R(\overline{x})\mid \neg R(\overline{x})\mid (\varphi \wedge \varphi )\mid (\varphi \vee \varphi )\mid (\varphi {\vee }^j\varphi )\mid \exists x\varphi \mid \forall x\varphi ,$$

$$\mathfrak{A}{\models }_{\overline{X}}\varphi \iff \mathfrak{A}{\models }_{X_i}\varphi \iff \forall s\in X_i:\mathfrak{A}{\models }_s\varphi ,$$

$$\text{textsc}Patient=$$

$$\text{textsc}Case=$$

$$\text{textsc}Test=$$

$$\text{textsc}Results=$$

$${\varphi }_0:=$$

$$\underset{i=1,2}{\bigwedge }(\text{textsc}Case[\text{diagnosis\_id},x_i]\subseteq \text{textsc}Test[\text{diagnosis\_id,test\_id}]\wedge$$

$$\displaystyle\textsc{Case}[\texttt{patient\_id},x_{i},positive]\subseteq\textsc{Results}[\texttt{patient\_id,test\_id,result}])\big{)}$$

$${\varphi }_1:=$$

$$\displaystyle\forall x\big{(}\textsc{Case}[\texttt{diagnosis\_id},x]\mid\textsc{Test}[\texttt{diagnosis\_id,test\_id}]\vee^{\textsc{Case}}$$

$$\displaystyle\hskip 11.38109pt\textsc{Case}[\texttt{patient\_id},x,positive]\mid\textsc{Results}[\texttt{patient\_id,test\_id,result}]\big{)}$$

$$\mathfrak{A}{\models }_{\overline{X}}\varphi \iff \mathfrak{A}{\models }_{\overline{X}\upharpoonright \overline{V}}\varphi .$$

$${\varphi }^{+}:=\underset{i\in I}{\text{vbox}\exists }{x}^i{y}^i({\xi }_l\wedge {\xi }_r),$$

$$\begin{gathered} {\xi }_l:=(x^{i_1}=y^{i_1}{\vee }^{i_1}(x^{i_1}\ne y^{i_1}\wedge (x^{i_2}=y^{i_2}{\vee }^{i_2}(x^{i_2}\ne y^{i_2} \\ \wedge (\cdots \wedge (x^{i_n}=y^{i_n}{\vee }^{i_n}(x^{i_n}\ne y^{i_n}\wedge \psi )\dots ), \\ {\xi }_r:=(x^{i_1}\ne y^{i_1}{\vee }^{i_1}(x^{i_1}=y^{i_1}\wedge (x^{i_2}\ne y^{i_2}{\vee }^{i_2}(x^{i_2}=y^{i_2} \\ \wedge (\cdots \wedge (x^{i_n}\ne y^{i_n}{\vee }^{i_n}(x^{i_n}=y^{i_n}\wedge \theta )\dots ). \end{gathered}$$

$$\operatorname*{\vphantom{\sum}\mathchoice{\vbox{\hbox{$\forall$}}}{\vbox{\hbox{$\forall$}}}{\vbox{\hbox{$\forall$}}}{\vbox{\hbox{$\forall$}}}}_{i\in I}x^{i}y^{i}\big{(}(\psi\land\bigwedge_{i\in I}x^{i}=y^{i})\lor(\theta\land\bigwedge_{i\in I}x^{i}\neq y^{i})\big{)},$$

$$\mathcal{S}:\text{textsc}P(rojects)=\{\text{name, employee, employee\_position}\},$$

Full text

1 Introduction

Team semantics is the mathematical framework of modern logics of dependence and independence. The origin of team semantics goes back to [18] but its development to its current form began with the publication of the monograph [27]. 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 [13, 15, 16, 21]. 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 logics using these novel atoms.

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 the 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}$ [11] 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 table, 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 [7] 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 [9] 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 [5] 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 widens the applicability of team semantics for the study of qualitative (e.g., functional dependence) and quantitative (e.g., probabilistic independence) dependencies in a unified framework. Recently multiteam semantics was further generalised to so-called probabilistic team semantics in which information on exact multiplicities are replaced by a (probability) distribution over the assignments [4, 14].

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

[TABLE]

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., [19, Section 3]). The uni-relational dependencies can be studied also in the context of team semantics as generalised dependencies [24]. 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., [6]) 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 Section 2 we lay the foundations of polyteam semantics. The shift to polyteams is exemplified in Section 2.2 by the definition of poly-dependence atoms and an Armstrong type axiomatisation for the associated implication problem. In Section 3 polyteam semantics is extended from atoms to complex formulae. Section 4 studies the relationship between polyteam and team semantics. We show that some polyteam logics can be simulated with team logics. Section 5 examines the expressive power of the new logics over polyteams. We characterise poly-independence (poly-dependence) logic as the maximal logic capable of defining all (downwards closed) properties of polyteams definable in existential second-order logic. Finally we relate poly-inclusion logic to a fragment of greatest fixed point logic.

2 From uni-dependencies to poly-dependencies

We start by defining the familiar dependency notions from the team semantics literature. In Section 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\colon D\to A$ is called an assignment. For a variable $x$ and $a\in A$, the assignment $s(a/x)\colon D\cup\{x\}\rightarrow A$ is obtained from $s$ as follows:

[TABLE]

A team $X$ is a set of assignments with a common domain $D$ and codomain $A$. If $\mathfrak{A}$ is a $\tau$-structure and $X$ a team with codomain $A$, then we say that $X$ is a team of $\mathfrak{A}$. Let $\overline{x}=(x_{1},\ldots,x_{n})$ be a sequence of variables, and $s$ an assignment. We write $s(\overline{x})$ to denote the sequence \big{(}s(x_{1}),\ldots,s(x_{n})\big{)}, and $X(\overline{x})$ for the set of values $\{s(\overline{x})\mid s\in X\}$. For a set (or sequence) of variables $V$, we write $X\upharpoonright V$ for the restriction of $X$ to $V$.

The following dependency atoms were introduced in [27, 7, 11].

Definition 1 (Dependency atoms)

Let $\mathfrak{A}$ be a structure 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:

[TABLE]

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:

[TABLE]

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

[TABLE]

Note that in the previous definitions it is allowed that some or all of the vectors of variables have length [math]. For example, $\mathfrak{A}\models_{X}=\!\left(\overline{y}\right)$ holds iff $\forall s\in X:s(\overline{y})=\overline{c}$ holds for some fixed tuple $\overline{c}$, where $=\!\left(\overline{y}\right)$ denotes the dependence atom $=\!\left(\overline{x},\overline{y}\right)$ such that $\overline{x}$ is of length [math]. Also, $\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 [math].

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, 11], 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 [17, 25, 26]. 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 [10, 21].

2.2 The notion of poly-dependence

For each $i\in\mathbb{N}$, let $\textrm{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 $\textrm{Var}(i)=\{x^{i}_{j}\mid j\in\mathbb{N}\}$. We write $x^{i}$, $y^{i}$, $x^{i}_{j}$ to denote variables from $\textrm{Var}(i)$, and $\overline{x}^{i}$ to denote tuples of variables from $\textrm{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$-structure and let $D_{i}\subseteq\textrm{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 of 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\textrm{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}}$.

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{v}^{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:

[TABLE]

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 2) 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 2.

The ability to reason about database dependencies facilitates many 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 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\to 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\to Y$

• •

Augmentation: if $X\to Y$, then $XZ\to YZ$

• •

Transitivity: if $X\to Y$ and $Y\to Z$, then $X\to Z$

Our first objective is to generalise 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 $k$th 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 $\Sigma\models\sigma$ if $\mathfrak{A}\models_{\overline{X}}\Sigma$ implies $\mathfrak{A}\models_{\overline{X}}\sigma$ for all models $\mathfrak{A}$ and polyteams $\overline{X}$. Given an axiomatisation $\mathcal{R}$, that is, a set of axioms and inference rules, we write $\Sigma\vdash_{\mathcal{R}}\sigma$ if $\mathcal{R}$ yields a proof of $\sigma$ from $\Sigma$. 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 $\Sigma\cup\{\sigma\}$ from $\mathcal{C}$, $\Sigma\vdash_{\mathcal{R}}\sigma$ implies (is implied by, resp.) $\Sigma\models\sigma$.

Theorem 2.1

The axiomatisation of Def. 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 $\Sigma\models\sigma$ implies $\Sigma\vdash\sigma$ for a set $\Sigma\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 $\Sigma^{*}$ be the subset of $\Sigma$ consisting of all standard dependence atoms over $\textrm{Var}(i)$. Since all teams satisfying $\Sigma^{*}$ can be extended to a polyteam satisfying $\Sigma$ by introducing new empty teams, we have that $\Sigma^{*}\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. [11]), Armstrong’s complete axiomatisation from Definition 2 yields a deduction of $\sigma_{0}$ from $\Sigma^{*}_{0}$ where $\Sigma^{*}_{0}$ and $\{\sigma_{0}\}$ are obtained from $\Sigma^{*}$ 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\neq j$. We will show that $\Sigma\not\vdash\sigma$ implies $\Sigma\not\models\sigma$. Assume $\Sigma\not\vdash\sigma$. Define first a binary relation $\sim$ on $\textrm{Var}(i)\cup\textrm{Var}(j)$ such that $a^{i}\sim a^{j}$ if $\Sigma\vdash=\!\left(\overline{x}^{i},a^{i}/\overline{x}^{j},a^{j}\right)$, $a^{j}\sim a^{i}$ if $\Sigma\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 $\Sigma\vdash=\!\left(\overline{x}^{i},a^{i}b^{i}/\overline{x}^{j},a^{j}a^{j}\right)$ for some $a^{j}$ ($a^{j}=b^{j}$ or $\Sigma\vdash=\!\left(\overline{x}^{j},a^{j}b^{j}/\overline{x}^{i},a^{i}a^{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 then that $a^{i}\sim b^{i}$ in which case $=\!\left(\overline{x}^{i},a^{i}b^{i}/\overline{x}^{j},a^{j}a^{j}\right)$ is derivable for some $a^{j}$. Then derive $=\!\left(a^{i}b^{i},b^{i}/a^{j}a^{j},a^{j}\right)$ and $=\!\left(a^{i}b^{i},a^{i}/a^{j}a^{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^{i}a^{i}/\overline{x}^{j},a^{j}a^{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^{i}b^{i}/\overline{x}^{j},a^{j}a^{j}\right)$ and $=\!\left(\overline{x}^{i},b^{i}c^{i}/\overline{x}^{j},b^{j}b^{j}\right)$ are derivable for some $a^{j}$ and $b^{j}$. Then analogously to the previous case assemble $=\!\left(\overline{x}^{i},a^{i}b^{i}b^{i}/\overline{x}^{j},a^{j}a^{j}b^{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^{i}c^{i}/\overline{x}^{j},b^{j}b^{j}\right)$. By the union rule we then obtain $=\!\left(\overline{x}^{i},a^{i}c^{i}/\overline{x}^{j},b^{j}b^{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\textrm{Var}(i)\cup\textrm{Var}(j)$ that appears in $\Sigma\cup\{\sigma\}$ to the equivalence class $x/\sim$. We define $\overline{X}=(X_{i},X_{j})$ where $X_{k}=\{s\upharpoonright\textrm{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 $\Sigma$. If $m=n$ or $\{m,n\}\neq\{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})$. ∎

2.3 A general notion of a poly-dependency

Next we consider suitable polyteam generalisations for the dependencies discussed in Section 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 expressed.

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:

[TABLE]

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:

[TABLE]

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:

[TABLE]

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 1

A relational database schema

[TABLE]

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

[TABLE]

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 the notion of generalised poly-atoms that is analogous to the notion of generalised atoms of [24].

Generalised poly-atoms. Let $n\in\mathbb{N}$, and 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. For every sequence $(\overline{x}_{1},\ldots,\overline{x}_{n})$, where $\overline{x}_{i}$ are length $j_{i}$ tuples of variables from some $\textrm{Var}(l_{i})$, $\alpha_{Q}(\overline{x}_{1},\ldots,\overline{x}_{n})$ is a generalised poly-atom of type $(j_{1},\ldots,j_{n})$ and of sort $\{l_{1},\ldots,l_{n}\}$. For a structure $\mathfrak{A}$ and polyteam $\overline{X}$ where $\overline{x}_{i}\subseteq{\mathsf{Dom}(X_{l_{i}})}$, the satisfaction relation with respect to $\alpha_{Q}(\overline{x}_{1},\ldots,\overline{x}_{n})$ is defined as follows:

[TABLE]

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 generalised poly-atom $\alpha_{Q}(\overline{x}_{1},\ldots,\overline{x}_{n})$ that has a singleton sort is called a uni-atom. When referring to the set of all poly-atoms of the form $\alpha_{Q}(\overline{x}_{1},\ldots,\overline{x}_{n})$, for a fixed $Q$, we omit the tuples $\overline{x}_{1},\ldots,\overline{x}_{n}$ and write simply poly-atom $\alpha_{Q}$. We say that an atom $\alpha_{Q}$ is definable in a logic $\mathcal{L}$ if the class $Q$ is definable in $\mathcal{L}$. For instance, we notice that poly-inclusion atoms of the form $(x^{i},y^{i})\subseteq(u^{j},v^{j})$ are first-order definable generalised poly-atoms 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

[TABLE]

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

[TABLE]

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 4

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:

[TABLE]

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

We say that $\vee$ is a global disjunction whereas $\vee^{i}$ is a local disjunction. A literal is said to be of sort $i$ if its variables are of sort $i$. 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 $\lor^{j}$ and using only variables of a single fixed sort is $\mathsf{FO}(\tau)$.

For the definition of polyteam semantics of $\mathsf{PFO}$, recall the definitions of teams and polyteams from Sections 2.1 and 2.2, respectively. Let $X$ be a team, $A$ a non-empty set, and $F\colon X\to\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)\}$. Moreover let $\overline{X}$ be a polyteam. Then $\overline{X}[X/X_{i}]$ denotes the polyteam $(\dots,X_{i-1},X,X_{i+1},\dots)$.

Note that if restricted to the aforementioned single-sort fragment of $\mathsf{PFO}(\tau)$ the polyteam semantics below coincides with traditional team semantics, see e.g. [5] 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 5 (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:

[TABLE]

Remark 1

Note that whereas the global disjunction is both commutative and associative, the local disjunction is only commutative. In particular $(\phi\lor^{i}\psi)\lor^{j}\theta$ is not, in general, equivalent with $\phi\lor^{i}(\psi\lor^{j}\theta)$. However the local disjunction is associative with respect to local disjunctions of the same sort, i.e., $(\phi\lor^{i}\psi)\lor^{i}\theta$ and $\phi\lor^{i}(\psi\lor^{i}\theta)$ are equivalent.

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

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

Proposition 1

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

[TABLE]

where $\models_{s}$ denotes the ordinary satisfaction relation of first-order logic.

Example 2

A relational database schema

[TABLE]

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 Patient the key 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 Case the foreign key patient_id referring to patient_id on Patient (i.e. the inclusion atom $\textsc{Case}[\texttt{patient\_id}]\subseteq\textsc{Patient}[\texttt{patient\_id}]$) enforces that patient ids on Case refer to real patients. The introduction of poly-dependence logics opens up possibilities for more expressive data constraints. The poly-inclusion formula

[TABLE]

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

[TABLE]

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 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 poly-inclusion logic is in $\mathsf{PTIME}\xspace$ because this logic can be translated to fixed-point logic (see Theorem 5.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}\xspace$ as well.

Poly-dependence logics. Poly-dependence, poly-independence, poly-inclusion, and poly-exclusion logics ($\mathsf{PFO}(\rm pdep)$, $\mathsf{PFO}(\rm pind)$, $\mathsf{PFO}(\rm pinc)$, and $\mathsf{PFO}(\rm 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 Section 2.1 in the polyteam setting by requiring that the variables used with each atom are of a single sort. For two logics $\mathcal{L}$ and $\mathcal{L}^{\prime}$ in polyteam setting, we write $\mathcal{L}\leq\mathcal{L}^{\prime}$ if for all $\phi\in\mathcal{L}$ there is $\phi^{\prime}\in\mathcal{L}^{\prime}$ such that $\mathfrak{A}\models_{\overline{X}}\phi$ if and only if $\mathfrak{A}\models_{\overline{X}}\phi^{\prime}$, for all structures $\mathfrak{A}$ and polyteams $\overline{X}$. We also write $\mathcal{L}\equiv\mathcal{L}^{\prime}$ if $\mathcal{L}\leq\mathcal{L}^{\prime}$ and $\mathcal{L}^{\prime}\leq\mathcal{L}$. We define ``$$\leq$$" and ``$$\equiv$$" analogously for two logics in the team setting.

3.2 Basic properties

A polyteam $\overline{X}$ is called strictly non-empty, if none of the teams $X_{i}$, $i\in\mathbb{N}$, is empty. We say that a formula $\phi$ is local in polyteam semantics if for all $\overline{V}=(V_{i})_{i\in\mathbb{N}}$ where $\textrm{Fr}_{i}(\phi)\subseteq V_{i}$ for $i\in\mathbb{N}$, and all structures $\mathfrak{A}$ and polyteams $\overline{X}$, we have

[TABLE]

The truth value of a local formula depends only on the free variables at each coordinate, including those coordinates where the set of free variables is empty. For instance, the formula $\exists x^{1}(x^{1}\neq x^{1})$ is true if and only if the first coordinate team is empty. The truth value of a local formula on a strictly non-empty polyteam depends only on the values of its free variables. We now call a logic $\mathcal{L}$ local if all its formulae are local.

Proposition 2 (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 3 (Downward Closure and Union Closure)

Let $\phi$ be a formula of $\mathsf{PFO}(\rm pdep)$, $\psi$ a formula of $\mathsf{PFO}(\rm 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 replacement of independence (dependence) atoms with any (downwards closed) class of atoms definable in existential second-order logic ($\mathsf{ESO}$) results in no expressive gain, if the empty team is ignored. Note that dependence and independence logic formulae are always true for the empty team. We say that a formula $\phi$ over team semantics has the empty team property if $\mathfrak{A}\models_{\emptyset}\phi$ for all models $\mathfrak{A}$, and a logic $\mathcal{L}$ has the empty team property is all of its formulae have it.

Proposition 4

Let $\mathcal{C}$ ($\mathcal{D}$, resp.) be the class of all (all downwards closed, resp.) $\mathsf{ESO}$-definable poly-atoms. With respect to non-empty teams, $\mathsf{FO}(\mathcal{C})\equiv\mathsf{FO}(\rm ind)$, $\mathsf{FO}(\mathcal{D})\equiv\mathsf{FO}(\rm dep)$. If the atoms in $\mathcal{C}$ and $\mathcal{D}$ have the empty team property, the restriction to non-empty teams can be lifted. Moreover $\mathsf{FO}(\rm pinc)\equiv\mathsf{FO}(\rm inc)$.

Proof

The claim $\mathsf{FO}(\rm pinc)\equiv\mathsf{FO}(\rm inc)$ follows directly from the observation that in the team semantics setting poly-inclusion atoms are exactly inclusion atoms. Note that $\mathsf{FO}(\rm ind)$ ($\mathsf{FO}(\rm dep)$, resp.) captures all (all downwards closed, resp.) $\mathsf{ESO}$-definable properties of teams which include the empty team (see Theorem 4.2). It is easy to show (cf. [20, Lemma 5]) that every property of teams definable in $\mathsf{FO}(\mathcal{C})$ ($\mathsf{FO}(\mathcal{D})$, resp.) is $\mathsf{ESO}$-definable ($\mathsf{ESO}$-definable and downwards closed, resp.). Thus since $\rm ind\in\mathcal{C}$ and $\rm dep\in\mathcal{D}$, we obtain that $\mathsf{FO}(\mathcal{C})\equiv\mathsf{FO}(\rm ind)$ and $\mathsf{FO}(\mathcal{D})\equiv\mathsf{FO}(\rm dep)$ with respect to non-empty teams. Finally note that if all atoms in $\mathcal{C}$ and $\mathcal{D}$ have the empty team property, the logics $\mathsf{FO}(\mathcal{C})$ and $\mathsf{FO}(\mathcal{D})$ have it as well. ∎

Remark 2

In particular it follows from the previous proposition that, in the polyteam setting, each occurrence of any (any downwards closed, resp.) $\mathsf{ESO}$-definable poly-atom (with the empty team property) that takes variables of a single sort as parameters may be equivalently expressed by a formula of $\mathsf{PFO}(\rm ind)$ ($\mathsf{PFO}(\rm 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 either one of the two disjunctions could be omitted from $\mathsf{PFO}$ without influencing the expressivity of the logic. To facilitate our construction, we here allow the use of disjunctions of type $\vee^{I}$, where $I$ is a set of indices, with the obvious semantics. We then show that $\lor$ can be replaced by $\lor^{I}$ and $\lor^{I}$ by $\lor^{i}$.

Proposition 5

For every formula $\phi$ of $\mathsf{PFO}$ there exists an equivalent formula $\psi_{l}$ ($\psi_{g}$, resp.) of $\mathsf{PFO}$ in which all disjunctions are local (global, resp.).

Proof

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

We will next show how to eliminate disjunctions of type $\lor^{I}$. Without loss of generality, we restrict to models of cardinality at least two. Let $\phi=\psi\lor^{I}\theta$ be a formula of $\mathsf{PFO}$ and let $I=\{i_{1},\dots,i_{n}\}$. Define

[TABLE]

where, for each $i\in I$, the variables $x^{i}$ and $y^{i}$ are fresh and distinct, and

[TABLE]

The idea above is that the variables $x^{i_{j}}$, $y^{i_{j}}$ are used to encode a (possibly overlapping) split of the team $X_{j}$. Using locality it is easy to see that $\phi$ and $\phi^{+}$ are equivalent over structures of cardinality at least two. From this the claim follows in a straightforward manner.

Global case. We show how a single local disjunction is eliminated. From this the result follows. Again, without loss of generality, we restrict to structures of cardinality at least two. Let $\phi=\psi\lor^{j}\theta$ be a formula of $\mathsf{PFO}$ and let $I$ list the sorts of all the variables that occur in $\phi$ except $j$. Define $\phi^{*}$ as

[TABLE]

where, for each $i\in I$, the variables $x^{i}$ and $y^{i}$ are fresh and distinct. The idea in $\phi^{*}$ is that on structures with at least two elements, the evaluation of the universal quantifiers $\forall x^{i}y^{i}$ on a polyteam $\overline{X}$ duplicates each assignment in $X_{i}$ in at least two ways: in some duplicates $x^{i}=y^{i}$ holds and in others $x^{i}\neq y^{i}$ holds. It then follows from locality that $\phi^{*}$ and $\phi$ are equivalent. ∎

We wish to point out that, in contrast to the previous result, it is easy to see that there is no single formula in $\mathsf{PFO}$ without local (global, reps.) disjunction that defines global (local, resp.) disjunction. Moreover it’s worth noticing that the translations produced above are quite involved and rely on the use of quantifiers. It is easy to define natural fragments of $\mathsf{PFO}$ where the disjunctions cannot be expressed with another.

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 3

A relational database schemas

[TABLE]

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}(\rm pinc,\rm dep)$-formula

[TABLE]

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 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 Relationship between polyteam and team semantics

Before embarking on an analysis of the expressive power of polyteam logics, we consider the relationship between polyteam and team semantics. One might ask is polyteam semantics really necessary in order to model the polyrelational case. Is it not possible to embed and interpret polyteams within team semantics? We will next shed some light on this question. Independence logic $\mathsf{FO}(\rm ind)$ is as expressive as existential second-order logic $\mathsf{ESO}$ when the team is encoded as a relation [7]. Moreover it is relatively clear that $\mathsf{PFO}(\rm pind)$ translates to $\mathsf{ESO}$ when the polyteam is encoded as a tuple of relations. Furthermore in $\mathsf{ESO}$ multiple relations can be encoded into a single relation of large enough arity. Theorem 4.3 establishes that, analogously to the case with $\mathsf{ESO}$, $\mathsf{PFO}(\rm pind)$ can also be simulated using $\mathsf{FO}(\rm ind)$. On the other hand, such a result does not seem likely to hold for $\mathsf{PFO}(\rm pdep)$ and $\mathsf{FO}(\rm dep)$. It seems that there is no suitable way to encode multiple relations into a single relation that is also compatible with downward closure; it is known that $\mathsf{FO}(\rm dep)$ characterises downward closed $\mathsf{ESO}$-definable properties of teams [22]. Section 4.1 lays out the groundwork for relating polyteam semantics to team semantics. Our results will be shown in Section 4.2.

4.1 Team representation

First let us formulate precisely how polyteams can be represented by teams. Let $X$ be a non-empty team whose domain takes variables from $\textrm{Var}(1),\ldots,\textrm{Var}(n)$. Then $X$ represents the polyteam $\overline{X}=(X_{1},\ldots,X_{n})$ where $X_{i}=X\upharpoonright\textrm{Var}(i)$. Note that any strictly non-empty polyteam $(X_{1},\ldots,X_{n})$, where $\bigcup{\mathsf{Dom}(X_{i})}$ is finite, can be represented by a team. In order to deal with the situations where some coordinate team $X_{i}$ of $\overline{X}$ is empty, we next introduce the concepts of contraction and emptification.

Definition 6 (Contraction and emptification)

Let $Q$ be a generalised quantifier of type $(j_{1},\dots,j_{n})$. The generalised quantifier $Q^{\prime}$ of type $(j_{1},\dots,j_{i-1},j_{i+1},j_{n})$ is the $i$-contraction of $Q$ if the equivalence

[TABLE]

holds for every $A,R_{1},\dots,R_{n}$. For $I\subseteq\{1,\dots,n\}$, the $I$-contraction of $Q$ is defined analogously. We say that a class of generalised poly-atoms $\mathcal{C}$ is closed under contraction if, for any poly-atom $\alpha_{Q}\in\mathcal{C}$ and any index $i$, $A_{Q^{\prime}}\in\mathcal{C}$, where $Q^{\prime}$ is the $i$-contraction of $Q$.

Let $\phi=\alpha_{Q}(\overline{x}^{j_{1}}_{1},\ldots,\overline{x}^{j_{n}}_{n})$ be a poly-atom, $i\in\mathbb{N}$ a natural number, $I=\{k\mid 1\leq k\leq n,j_{k}=i\}$ a set of indices, and $Q^{\prime}$ the $I$-contraction of $Q$. Furthermore let $\overline{\chi}$ list the variable tuples in $\overline{x}^{j_{1}}_{1},\ldots,\overline{x}^{j_{n}}_{n}$ that are not of sort $i$. We let ${\phi}_{i\mapsto\emptyset}$ denote the poly-atom $\alpha_{Q^{\prime}}(\overline{\chi})$, and call it the $i$-emptification of $\phi$.

For instance, the $1$-emptification of the dependence atom $=\!\left(x^{1},y^{1}\right)$ is equivalent to $\top$. It is easy to see that in polyteam setting, the $i$-emptification of $\alpha(\overline{x})$ can be equivalently expressed with a $\mathsf{PFO}(\alpha)$-formula. However the same is not, in general, true in the team semantics setting.

Next we show how statements on polyteams that have empty coordinate teams can be transformed to equivalent statements over strictly non-empty polyteams.

Definition 7 (Emptification of complex formulae)

Let $\mathcal{C}$ be a set of poly-atoms, $\phi$ a formula of $\mathsf{PFO}(\mathcal{C})$, and $i\in\mathbb{N}$. We denote by ${\phi}_{i\mapsto\emptyset}$ the formula obtained from $\phi$ by simultaneously replacing all first-order literals of sort $i$ with $\top$, all disjunctions $\lor^{i}$ with $\land$, and all poly-atoms $\alpha$ with ${\alpha}_{i\mapsto\emptyset}$, and by eliminating all quantifiers of sort $i$. We call ${\phi}_{i\mapsto\emptyset}$ the $i$-emptification of $\phi$. Note that ${\phi}_{i\mapsto\emptyset}$ is free of variables and local disjuctions of sort $i$.

The following proposition can now be shown by straightforward structural induction.

Proposition 6

Let $\phi\in\mathsf{PFO}(\mathcal{C})$, where $\mathcal{C}$ is any set of poly-atoms. Then for all models $\mathfrak{A}$ and polyteams $\overline{X}$,

[TABLE]

where $\overline{X}_{i=\emptyset}$ is obtained from $\overline{X}$ by substituting the empty team for $X_{i}$.

Next we introduce a trick that enables us to change a representation of a polyteam on the fly.

Lemma 1

Let $\mathcal{C}$ be a set of poly-atoms and $X$ a non-empty team representing $\overline{X}=(X_{1},\dots,X_{n})$. For every $\phi\in\mathsf{FO}(\mathcal{C},\rm inc)$ there exists a formula $\phi^{\exists r}\in\mathsf{FO}(\mathcal{C},\rm inc)$ such that

[TABLE]

Proof

Let $\phi$, $\overline{X}$, and $X$ be as described above. For each $1\leq i\leq n$, let $\overline{x}^{i}=x^{i}_{1},\dots,x^{i}_{k}$ be the variable domain of $X_{i}$ and let $\overline{y}^{i}=y^{i}_{1},\dots,y^{i}_{k}$ be fresh and distinct variables. Let $\overline{x}$ and $\overline{y}$ denote $\overline{x}^{1},\dots,\overline{x}^{n}$ and $\overline{y}^{1},\dots,\overline{y}^{n}$, respectively. Define

[TABLE]

It is easy to check, using locality, that $\phi^{\exists r}$ defined as above satisfies the claim of the lemma.∎

4.2 Translation to team semantics

Using the concepts and results from the previous section we will now move to translations from polyteam semantics to team semantics. The next theorem reveals that polyteam semantics can be simulated with team semantics using inclusion atoms and classical disjunction $\hskip 1.42262pt\varovee\hskip 1.42262pt$:

[TABLE]

Theorem 4.1

Let $\phi$ be a formula in $\mathsf{PFO}(\mathcal{C})$, where $\mathcal{C}$ is a contraction closed set of poly-atoms. Then there is a formula \phi^{*}\in\mathsf{FO}(\mathcal{C},\rm inc,\mbox{\hskip 1.42262pt\varovee\hskip 1.42262pt}) such that for any structure $\mathfrak{A}$, with at least two elements, and any non-empty team $X$ representing $\overline{X}=(X_{1},\ldots,X_{n})$,

[TABLE]

where $\mathfrak{A}^{*}$ is an expansion of $\mathfrak{A}$ with two distinct constants.

Proof

Define a rank $\mathrm{r}$ of a formula $\phi$ as follows. For a poly-atom $\alpha(\overline{x}_{1}^{i_{1}},\ldots,\overline{x}_{n}^{i_{n}})$, $\mathrm{r}(\alpha)\mathrel{\mathop{:}}=n$. For first-order literals $\alpha$, $\mathrm{r}(\alpha)\mathrel{\mathop{:}}=1$. For complex formulae, $\mathrm{r}(Q\psi)\mathrel{\mathop{:}}=\mathrm{r}(\psi)+1$ and $\mathrm{r}(\psi C\theta)\mathrel{\mathop{:}}=\mathrm{r}(\psi)+\mathrm{r}(\theta)+1$, where $Q\in\{\exists,\forall\}$ and $C\in\{\wedge,\vee,\vee^{i}\}$. We prove the claim by induction on $\mathrm{r}(\phi)$ for a mapping $\phi\mapsto\phi^{*}$ defined recursively. This mapping is the identity on literals, and homomorphism on conjunction and universal quantification; proving the induction claim is straightforward for these cases and thus omitted. By Proposition 5 we can also exclude the case of global disjunction. Thus it suffices to consider local disjunction and existential quantification.

Local disjunction. Suppose $\phi=\psi\vee^{i}\theta$. We define

[TABLE]

where ∃r is as defined in Lemma 1 and

[TABLE]

where $z$ is a fresh variable and $\overline{x}$ lists all the free variables of $\phi$ which are not of the sort $i$. Furthermore, [math] and $1$ are the two distinct constants, and $\overline{x}0\subseteq\overline{y}z$ and $\overline{x}0\subseteq\overline{y}z$ are shorthands for $\exists v(v=0\wedge\overline{x}v\subseteq\overline{y}z)$ and $\exists v(v=1\wedge\overline{x}v\subseteq\overline{y}z)$, respectively.

Assume first that $\mathfrak{A}\models_{\overline{X}}\phi$. Then there are $Y_{i}\cup Z_{i}=X_{i}$ such that $\mathfrak{A}\models_{\overline{Y}}\psi$ and $\mathfrak{A}\models_{\overline{Z}}\theta$, where $\overline{Y}$ and $\overline{Z}$ are obtained from $\overline{X}$ by substituting respectively $Y_{i}$ and $Z_{i}$ for $X_{i}$. Suppose $Y_{i}$ is empty. Then by Proposition 6 $\mathfrak{A}\models_{\overline{X}}{\psi}_{i\mapsto\emptyset}$. Thus by induction hypothesis $\mathfrak{A}\models_{X}({\psi}_{i\mapsto\emptyset})^{*}$. Furthermore $\mathfrak{A}\models_{X}\theta^{*}$ follows from $\mathfrak{A}\models_{\overline{Z}}\theta$ by the induction hypothesis, for $\overline{Z}=\overline{X}$ since $Y_{i}=\emptyset$. Thus the first disjunct of $\phi^{*}$ holds. If $Z_{i}$ is empty, we similarly obtain that the second disjunct holds.

Suppose then that both $Y_{i}$ and $Z_{i}$ are non-empty. Let $X^{*}$ be a representation of $\overline{X}$ obtained by taking the Cartesian product of the teams $X_{1},\dots,X_{n}$. For $s\in X^{*}$, define

[TABLE]

Clearly, the two left-most conjuncts in (3) are satisfied by $X^{*}[G/z]$. Recall that $\overline{Y}$ and $\overline{Z}$ were obtained from $\overline{X}$ by substituting respectively $Y_{i}$ and $Z_{i}$ for $X_{i}$. Let $Y^{\prime}$ and $Z^{\prime}$ consist of those assignments of $X^{*}[G/z]$ whose restriction to $\textrm{Var}(i)$ belongs to $Y_{i}$ and $Z_{i}$, respectively. Note that if the variable $z$ is disregarded from $Y^{\prime}$ and $Z^{\prime}$, team representations of $\overline{Y}$ and $\overline{Z}$ are obtained, respectively. Now by induction hypothesis, locality (Proposition 2), and the selection of $G$,

[TABLE]

Similarly we obtain that $\mathfrak{A}\models_{Z^{\prime}}\theta^{*}\land z=1$. Since $Y^{\prime}\cup Z^{\prime}=X^{*}[G/z]$, we conclude that $\mathfrak{A}\models_{X^{*}}\Phi$. Finally, by Lemma 1, we obtain that $\mathfrak{A}\models_{X}\Phi^{\exists r}$ and hence that $\mathfrak{A}\models_{X}\phi^{*}$.

For the converse direction, suppose $\mathfrak{A}\models_{X}\phi^{*}$. Assume first that $\mathfrak{A}\models_{X}({\psi}_{i\mapsto\emptyset})^{*}\wedge\theta^{*}$. By the induction hypothesis, it follows that $\mathfrak{A}\models_{\overline{X}}\theta$ and $\mathfrak{A}\models_{\overline{X}}{\psi}_{i\mapsto\emptyset}$. By Proposition 6 together with the semantics of local disjunctions, it follows that $\mathfrak{A}\models_{\overline{X}}\phi$. Similarly, $\mathfrak{A}\models_{\overline{X}}\phi$ if $\mathfrak{A}\models_{X}({\theta}_{i\mapsto\emptyset})^{*}\wedge\psi^{*}$. Assume then that $\mathfrak{A}\models_{X}\Phi^{\exists r}$. Then $\mathfrak{A}\models_{Y}\Phi$ for some team $Y$ representing $\overline{X}$. Let $F\colon Y\to\mathcal{P}(A)\setminus\{\emptyset\}$ be a mapping such that $Y[F/z]$ satisfies the quantifier-free part of (3), and let $U$ and $V$ consist of those assignments of $Y[F/z]$ that map $z$ to [math] and $1$, respectively. The disjunction in (3) now guarantees that $U\cup V=Y[F/z]$, $\mathfrak{A}\models_{U}\psi^{*}$, and $\mathfrak{A}\models_{V}\theta^{*}$. By the induction hypothesis, $\mathfrak{A}\models_{\overline{U}}\psi$ and $\mathfrak{A}\models_{\overline{V}}\theta$, where $\overline{U}=(U_{1},\ldots,U_{n})$ and $\overline{V}=(V_{1},\ldots,V_{n})$ are the polyteams represented by $U$ and $V$, respectively. Since $X$ and $Y$ represent the same polyteam, and $Y(\overline{x})=U(\overline{x})=V(\overline{x})$ by the inclusion atoms in (3), we obtain that $U_{j}=V_{j}=X_{j}$ for $j\neq i$. Moreover, $U_{i}\cup V_{i}=Y_{i}=X_{i}$, and thus we obtain that $\mathfrak{A}\models_{\overline{X}}\psi\vee^{i}\theta$.

Existential quantification. Suppose $\phi=\exists x\psi$ where $x\in\textrm{Var}(i)$. We define $\phi^{*}\mathrel{\mathop{:}}=\exists x\psi^{*}$. Suppose first $\mathfrak{A}\models_{\overline{X}}\phi$. Then $\mathfrak{A}\models_{\overline{X}[X_{i}[F_{i}/x]/X_{i}]}\psi$ for some $F_{i}\colon X_{i}\to\mathcal{P}(A)\setminus\{\emptyset\}$. If $F\colon X\to\mathcal{P}(A)\setminus\{\emptyset\}$ is defined as $F(s)\mathrel{\mathop{:}}=F_{i}(s\upharpoonright\textrm{Var}(i))$, it follows that the team $X[F/x]$ represents the polyteam $\overline{X}[X_{i}[F_{i}/x]/X_{i}]$.Hence by induction hypothesis $\mathfrak{A}\models_{X[F/x]}\psi^{*}$, and thus $\mathfrak{A}\models_{X}\phi^{*}$.

For the converse direction, suppose $\mathfrak{A}\models_{X}\phi^{*}$. Then we find $F\colon X\to\mathcal{P}(A)\setminus\{\emptyset\}$ such that $\mathfrak{A}\models_{X[F/x]}\psi^{*}$. Setting $F_{i}\colon X_{i}\to\mathcal{P}(A)\setminus\{\emptyset\}$ as $F_{i}(s)\mathrel{\mathop{:}}=\bigcup\{F(s^{\prime})\mid s^{\prime}\in X,s^{\prime}\upharpoonright\textrm{Var}(i)=s\}$, it follows that $\overline{X}[X_{i}[F_{i}/x]/X_{i}]$ is represented by $X[F/x]$. Hence, we obtain by the induction hypothesis, that $\mathfrak{A}\models_{\overline{X}[X_{i}[F_{i}/x]/X_{i}]}\psi$. Thus $\mathfrak{A}\models_{\overline{X}}\phi$. ∎

For poly-inclusion logic, the following corollary now follows immediately.

Corollary 1

Let $\phi$ be a formula in $\mathsf{PFO}(\rm pinc)$. Then there is a formula \phi^{*}\in\mathsf{FO}(\rm inc,\mbox{\hskip 1.42262pt\varovee\hskip 1.42262pt}) such that, for any structure $\mathfrak{A}$ with at least two elements, and any non-empty team $X$ representing $\overline{X}$,

[TABLE]

where $\mathfrak{A}^{*}$ is an expansion of $\mathfrak{A}$ with two distinct constants.

Proof

By the previous theorem $\phi^{*}$ can be found from \mathsf{FO}(\mathcal{C},\rm inc,\mbox{\hskip 1.42262pt\varovee\hskip 1.42262pt}), where $\mathcal{C}$ is the closure of poly-inclusion atoms under contraction. Since poly-inclusion atoms are just inclusion atoms in team semantics, and the closure only adds poly-atoms equivalent to $\top$ or $\bot$, we obtain that \phi^{*}\in\mathsf{FO}(\rm inc,\mbox{\hskip 1.42262pt\varovee\hskip 1.42262pt}). ∎

Next we show that the polyteam logics defined in terms of $\mathsf{ESO}$-definable poly-atoms can be represented in independence logic. First, we observe that $\mathsf{ESO}$-definable poly-atoms are closed under contraction.

Proposition 7

The set of $\mathsf{ESO}$-definable poly-atoms is closed under contraction.

Proof

Let $\alpha_{Q}$ be a generalised $\mathsf{ESO}$-definable poly-atom of type $(j_{1},\ldots,j_{n})$, and let $i\in\{1,\ldots,n\}$. We show that the $i$-contraction of $\alpha_{Q}$ is definable in $\mathsf{ESO}$. Without loss of generality $i=n$, in which case the $i$-contraction of $\alpha_{Q}$, written $\alpha_{Q^{\prime}}$, is of type of $(j_{1},\ldots,j_{n-1})$. Let $\phi(R_{1},\ldots,R_{n})$ be an $\mathsf{ESO}$ formula which defines $\alpha_{Q}$, and let $\phi^{\prime}(R_{1},\ldots,R_{n-1})$ be obtained from $\phi$ by replacing all relational atoms of the form $R_{n}(\overline{t})$ with $\bot$. Then for all models $\mathfrak{A}=(A,R^{\mathfrak{A}}_{1},\ldots,R^{\mathfrak{A}}_{n-1})$,

[TABLE]

∎

Second, we use the fact that $\mathsf{FO}(\rm ind)$ characterises all $\mathsf{ESO}$-definable team properties. 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 4.2 ([7, 22])

Let $\phi(\overline{x})$ be an $\mathsf{FO}(\rm ind)$ ($\mathsf{FO}(\rm dep)$, resp.) formula, and let $R$ be an $|\overline{x}|$-ary relation. Then there is an (downwards closed with respect to $R$, resp.) $\mathsf{ESO}$-sentence $\psi(R)$ such that for all teams $X\neq\emptyset$ where ${\mathsf{Dom}(X)}=\overline{x}$,

[TABLE]

The same statement holds also vice versa.

In fact, in the above theorem we may substitute all $\mathsf{ESO}$-definable poly-atoms and classical disjunction for independence atoms.

Theorem 4.3

Let $\mathcal{C}$ be a set of $\mathsf{ESO}$-definable poly-atoms, and let $\phi$ be a formula in $\mathsf{PFO}(\mathcal{C})$. Then there is a formula $\phi^{*}\in\mathsf{FO}(\rm ind)$ such that for any structure $\mathfrak{A}$ and any non-empty team $X$ representing $\overline{X}$,

[TABLE]

Proof

We may assume that $\mathcal{C}$ is the set of all $\mathsf{ESO}$-definable poly-atoms. Let $\phi$ be an arbitrary formula of $\mathsf{PFO}(\mathcal{C})$. Without loss of generality, it suffices to prove the above equivalence with respect to structures that have at least two elements. By Theorem 4.1 and Proposition 7, we find a formula \phi^{\prime}\in\mathsf{FO}(\mathcal{C},\rm inc,\mbox{\hskip 1.42262pt\varovee\hskip 1.42262pt}) such that, for every structure $\mathfrak{A}$, with at least two elements, and team $X$ that represents some non-empty polyteam $\overline{X}$ of $\phi$, it holds that

[TABLE]

where $\mathfrak{A}^{\prime}$ is an expansion of $\mathfrak{A}$ with two distinct constants [math] and $1$. Define the formula \phi^{\prime\prime}\mathrel{\mathop{:}}=\exists xy\big{(}=\!\left(x\right)\land=\!\left(y\right)\land x\neq y\land\phi^{\prime}(x/0,y/1)\big{)}, where $x$ and $y$ are fresh distinct variables that do not occur in $\phi^{\prime}$, and $\phi^{\prime}(x/0,y/1)$ is obtained from $\phi^{\prime}$ by replacing [math] and $1$ by $x$ and $y$, respectively. Clearly

[TABLE]

Note that \phi^{\prime\prime}\in\mathsf{FO}(\mathcal{C},\mbox{\hskip 1.42262pt\varovee\hskip 1.42262pt}), for $\rm dep$ and $\rm inc$ are $\mathsf{ESO}$-definable poly-atoms. Also, when restricted to non-empty teams, \mathsf{FO}(\mathcal{C},\mbox{\hskip 1.42262pt\varovee\hskip 1.42262pt})\leq\mathsf{FO}(\rm ind), for $\mathsf{FO}(\mathcal{C})\equiv\mathsf{FO}(\rm ind)$ by Proposition 4, and $\mathsf{FO}(\rm ind)$ is closed under classical disjunction because it inherits this property from $\mathsf{ESO}$ by Theorem 4.2. Thus we conclude that, by taking a formula $\phi^{*}$ of $\mathsf{FO}(\rm ind)$ which is equivalent to $\phi^{\prime\prime}$ with respect to non-empty teams, we obtain the required team representation of $\phi$. ∎

As an immediate corollary we obtain that poly-independence logic is representable in independence logic.

Corollary 2

Let $\phi$ be a formula in $\mathsf{PFO}(\rm pind)$. Then there is a formula $\phi^{*}\in\mathsf{FO}(\rm ind)$ such that for any structure $\mathfrak{A}$ and any non-empty team $X$ representing $\overline{X}$,

[TABLE]

5 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 downwards closed $\mathsf{ESO}$ properties of teams [7, 22]. Independence logic, whose independence atoms violate downward closure, in turn captures all $\mathsf{ESO}$ team properties [7]. On the other hand, the expressivity of inclusion logic has been characterised by the so-called greatest fixed point logic [9]. In this section we turn attention to polyteams and consider the expressivity of the poly-dependence logics introduced in this paper. Section 5.1 deals with logics with only uni-dependencies whereas in Section 5.2 poly-dependencies are considered.

5.1 Uni-dependencies in polyteam semantics

First we turn attention to uni-atoms in polyteam semantics. We show that with uni-atoms no interaction between different relations is possible.

Theorem 5.1

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 structures $\mathfrak{A}$ and all $\overline{X}=(X_{1},\ldots,X_{n})$, where $X_{i}$ is a team with domain $\overline{x}^{i}$,

[TABLE]

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 5 we may assume that only disjunctions of type $\lor^{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)\mathrel{\mathop{:}}=\begin{cases}\phi&\textrm{if }i=j,\\ \top&\textrm{otherwise.}\end{cases}$

• •

$f_{i}(\psi\lor^{j}\theta)\mathrel{\mathop{:}}=\begin{cases}f_{i}(\psi)\lor f_{i}(\theta)&\textrm{if }i=j,\\ f_{i}(\psi)\land f_{i}(\theta)&\textrm{otherwise.}\end{cases}$

• •

$f_{i}(\psi\land\theta)\mathrel{\mathop{:}}=f_{i}(\psi)\land f_{i}(\theta)$.

• •

For $Q\in\{\exists,\forall\}$, set $f_{i}(Qx^{j}\psi)\mathrel{\mathop{:}}=\begin{cases}Qxf_{i}(\psi)&\textrm{if }i=j,\\ f_{i}(\psi)&\textrm{otherwise.}\end{cases}$

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 $\lor^{i}$.

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

[TABLE]

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\neq j$. Thus we obtain that $\mathfrak{A}\models_{\overline{X}}\phi$ holds iff

[TABLE]

The above can be rewritten as

[TABLE]

The claim now follows, since $f_{j}(\psi)\lor f_{j}(\theta)=f_{j}(\psi\lor^{j}\theta)$ and $f_{i}(\psi)\land f_{i}(\theta)=f_{i}(\psi\lor^{j}\theta)$, for $i\neq j$.

The cases for the quantifiers are similar. ∎

Theorem 5.1 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}(\rm dep)$.

Proposition 8

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

Proof

Assume that $=\!\left(x^{1}/x^{2}\right)$ can be defined by some $\phi(x^{1},x^{2})\in\mathsf{PFO}(\rm dep)$. By Theorem 5.1 there are $\mathsf{FO}(\rm 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

[TABLE]

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 $\mathfrak{A}\models_{(X_{1},X_{2})}=\!\left(x^{1}/x^{2}\right)$, and $\mathfrak{A}\models_{(Y_{1},Y_{2})}=\!\left(x^{1}/x^{2}\right)$. Hence by (5), we obtain first that $\mathfrak{A}\models_{X_{1}}\psi_{i}(x^{1})\textrm{ and }\mathfrak{A}\models_{Y_{2}}\psi_{i}(x^{2})$, and then that $\mathfrak{A}\models_{(X_{1},Y_{2})}=\!\left(x^{1}/x^{2}\right)$, which is a contradiction.∎

It is now easy to see that Theorems 5.1 and 4.2 together imply that $\mathsf{PFO}(\rm ind)$ ($\mathsf{PFO}(\rm dep)$, resp.) captures all conjunctions of (downward closed, resp.) $\mathsf{ESO}$ properties of teams.

Theorem 5.2

Let $\phi(\overline{x}^{1},\ldots,\overline{x}^{n})$ be a $\mathsf{PFO}(\rm ind)$ ($\mathsf{PFO}(\rm dep)$, resp.) formula where $\overline{x}^{i}$ is a sequence of variables from $\textrm{Var}(i)$. Let $R_{i}$ be an $|\overline{x}^{i}|$-ary relation symbol for $i=1,\ldots,n$. Then there are (downwards 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}\neq\emptyset$

[TABLE]

The same statement holds also vice versa.

5.2 Poly-dependencies in polyteam semantics

Next we consider poly-dependencies in polyteam semantics. We begin by observing that many translations between different team logics carry over to polyteam logics.

Lemma 2

The following equivalences hold:

[TABLE]

[TABLE]

Proof

The equivalences (6)–(11) are straightforward and (12) is analogous to the corresponding translation in the team semantics setting (see [7]).∎

The following theorem compares the expressive powers of different polyteam 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 5.3

The following equivalences of logic hold:

1. (1)

$\mathsf{PFO}(\rm pdep)\equiv\mathsf{PFO}(\rm pexc)$, 2. (2)

$\mathsf{PFO}(\rm pind)\equiv\mathsf{PFO}(\rm pexc,\rm inc)\equiv\mathsf{PFO}(\rm pinc,\rm exc)\equiv\mathsf{PFO}(\rm pdep,\rm inc)$

$\equiv\mathsf{PFO}(\rm pinc,\rm dep)\equiv\mathsf{PFO}(\rm pdep,\rm ind)\equiv\mathsf{PFO}(\rm pexc,\rm ind)\equiv\mathsf{PFO}(\rm pinc,\rm ind)$.

Proof

Item (1) follows by equivalences (7) and (10). Item (2) follows from the following list of relationships:

• •

$\mathsf{PFO}(\rm pind)\subseteq\mathsf{PFO}(\rm pexc,\rm inc)$ by (7), (9), and (12).

• •

$\mathsf{PFO}(\rm pexc,\rm inc)\equiv\mathsf{PFO}(\rm pinc,\rm exc)$ by (9) and (11).

• •

$\mathsf{PFO}(\rm pexc,\rm inc)\equiv\mathsf{PFO}(\rm pdep,\rm inc)$ by (7) and (10).

• •

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

• •

$\mathsf{PFO}(\rm pdep,\rm inc)\subseteq\mathsf{PFO}(\rm pdep,\rm ind)$, $\mathsf{PFO}(\rm pexc,\rm inc)\subseteq\mathsf{PFO}(\rm pexc,\rm ind)$, and $\mathsf{PFO}(\rm pinc,\rm dep)\subseteq\mathsf{PFO}(\rm pinc,\rm ind)$ since inclusion atoms can be described in $\mathsf{FO}(\rm ind)$ [7] and dependence atoms by independence atoms [11].

• •

$\mathsf{PFO}(\rm pdep,\rm ind)\subseteq\mathsf{PFO}(\rm ind)$, $\mathsf{PFO}(\rm pexc,\rm ind)\subseteq\mathsf{PFO}(\rm ind)$, and \mathsf{PFO}(\rm pinc,\rm ind)$$\subseteq\mathsf{PFO}(\rm pind) by (6), (8), and (10).

∎

Next we show the analogue of Theorem 4.2 for polyteams.

Theorem 5.4

Let $\phi(R_{1},\ldots,R_{n})$ be an $\mathsf{ESO}$-sentence. There is a $\mathsf{PFO}(\rm pdep,\rm inc)$-formula $\phi^{*}(\overline{x}^{1},\ldots,\overline{x}^{n})$, where $|\overline{x}^{i}|={\mathrm{ar}(R_{i})}$, such that for all structures $\mathfrak{A}$ and all polyteams $\overline{X}=(X_{1},\ldots,X_{n})$ with ${\mathsf{Dom}(X_{i})}=\overline{x}^{i}$ and $X_{i}\neq\emptyset$,

[TABLE]

The statement holds also vice versa.

Proof

Considering first the direction from $\mathsf{PFO}(\rm pdep,\rm inc)$ to $\mathsf{ESO}$, let $\phi(\overline{x}^{1},\ldots,\overline{x}^{n})$ be a $\mathsf{PFO}(\rm pdep,\rm inc)$-formula. Since poly-dependence and uni-inclusion atoms are $\mathsf{ESO}$-definable, $\phi$ can be represented by some $\mathsf{FO}(\rm ind)$-formula $\phi^{*}$ (Theorem 4.3), which in turn can be expressed as some $\mathsf{ESO}$-formula $\psi(R)$ (Theorem 4.2). Let $R_{1},\ldots,R_{n}$ be fresh relation symbols with respective arities $|\overline{x}^{1}|,\ldots,|\overline{x}^{n}|$. Let $\psi^{\prime}$ be obtained from $\psi$ by replacing each atom $R(\overline{v}_{1},\ldots,\overline{v}_{n})$, where $\overline{v}_{1},\ldots,\overline{v}_{n}$ are tuples of variables respective lengths $|\overline{x}^{1}|,\ldots,|\overline{x}^{n}|$, with the conjunction $R_{1}(\overline{v}_{1})\wedge\ldots\wedge R_{n}(\overline{v}_{n})$. Then we observe that for all models $\mathfrak{A}$ and polyteams $\overline{X}=(X_{1},\ldots,X_{n})$ represented by $X$,

[TABLE]

Consider then the opposite direction. Analogously to [7], we can rewrite $\phi(R_{1},\ldots,R_{n})$ as

[TABLE]

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\leq 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

[TABLE]

where

[TABLE]

and $\psi^{\prime}(\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 [7] to check that $\mathfrak{A}\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 [7], it can now be seen that $\phi^{*}$ correctly simulates $\phi$. Since exclusion atoms can be expressed in dependence logic, the claim then follows.∎

By item (2) of Theorem 5.3 the result of Theorem 5.4 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 5.4 can be now easily adapted to show that poly-exclusion and poly-dependence logic capture all downwards closed $\mathsf{ESO}$ properties of polyteams.

Theorem 5.5

Let $\phi(R_{1},\ldots,R_{n})$ be an $\mathsf{ESO}$-sentence that is downwards closed with respect to $R_{i}$. Then there is a $\mathsf{PFO}(\rm pdep)$-formula $\phi^{*}(\overline{x}^{1},\ldots,\overline{x}^{n})$, where $|\overline{x}^{i}|={\mathrm{ar}(R_{i})}$, such that for all structures $\mathfrak{A}$ and all polyteams $\overline{X}=(X_{1},\ldots,X_{n})$ with ${\mathsf{Dom}(X_{i})}=\overline{x}^{i}$ and $X_{i}\neq\emptyset$,

[TABLE]

The statement holds also vice versa.

Proof

Consider first the direction from $\mathsf{PFO}(\rm pdep)$ to $\mathsf{ESO}$. By Theorem 5.3, $\mathsf{PFO}(\rm pdep)$ is subsumed by $\mathsf{PFO}(\rm pind)$, and thus the previous theorem yields a suitable $\mathsf{ESO}$-sentence $\phi(R_{1},\ldots,R_{n})$. Since $\mathsf{PFO}(\rm pdep)$ is downwards closed (Proposition 7), this sentence is also downwards closed with respect to $R_{i}$.

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 5.4 and by downward closure we may transform it to an equivalent form (see [22] for details)

[TABLE]

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

[TABLE]

Finally the claim follows by eliminating the exclusion atoms from $\theta_{0}$. ∎

Next we turn to poly-inclusion logic. Over sentences, inclusion logic is known to be as expressive as positive greatest fixed point logic ($\mathsf{PosGFP}$), the fragment of greatest fixed point logic in which all fixed point operators occur within the scope of an even number of negations. Moreover, all team properties definable in inclusion logic are also definable in $\mathsf{PosGFP}$, but the converse does not hold due to union closure.

Theorem 5.6 ([9])

Every $\mathsf{FO}(\rm inc)$-sentence is equivalent to some $\mathsf{PosGFP}$-sentence, and vice versa. Moreover, for every $\mathsf{FO}(\rm inc)$-formula $\phi(\overline{x})$ there is a $\mathsf{PosGFP}$-sentence $\psi(R)$, where $|\overline{x}|={\mathrm{ar}(R)}$, such that for all structures $\mathfrak{A}$ and all teams $X$ with ${\mathsf{Dom}(X)}=\overline{x}$,

[TABLE]

To generalise these results to polyteam semantics, we use the fact that all team connectives and quantifiers distribute over classical disjunctions.

Proposition 9 ([8])

Let $\phi$ be an \mathsf{FO}(\mathcal{C},\mbox{\hskip 1.42262pt\varovee\hskip 1.42262pt})-formula, where $\mathcal{C}$ is any set of atoms. Then $\phi$ is equivalent to some formula of the form \psi_{1}\mbox{\hskip 1.42262pt\varovee\hskip 1.42262pt}\ldots\mbox{\hskip 1.42262pt\varovee\hskip 1.42262pt}\psi_{n} where $\psi_{1},\ldots,\psi_{n}$ are $\mathsf{FO}(\mathcal{C})$-formulae.

Theorem 5.7

Every $\mathsf{PFO}(\rm pinc)$-sentence is equivalent to some $\mathsf{PosGFP}$-sentence, and vice versa. Moreover, for every $\mathsf{PFO}(\rm pinc)$-formula $\phi(\overline{x}^{1},\ldots,\overline{x}^{n})$ there is a $\mathsf{PosGFP}$-sentence $\psi(R_{1},\ldots,R_{n})$, where $|\overline{x}^{i}|={\mathrm{ar}(R_{i})}$, such that for all structures $\mathfrak{A}$ and all polyteams $\overline{X}=(X_{1},\ldots,X_{n})$ with ${\mathsf{Dom}(X_{i})}=\overline{x}^{i}$,

[TABLE]

Proof

Let $\phi(\overline{x}^{1},\ldots,\overline{x}^{n})\in\mathsf{PFO}(\rm pinc)$ be a formula, and let \phi^{*}(\overline{x}^{1},\ldots,\overline{x}^{n})\in\mathsf{FO}(\rm inc,\mbox{\hskip 1.42262pt\varovee\hskip 1.42262pt}) be its team representation, obtained by Corollary 1, in which two additional constants [math] and $1$ occur. Without loss of generality, we may restrict our attention to structures with at least two elements. By Proposition 9 $\phi^{*}$ is equivalent to a disjunction \psi_{1}\mbox{\hskip 1.42262pt\varovee\hskip 1.42262pt}\ldots\mbox{\hskip 1.42262pt\varovee\hskip 1.42262pt}\psi_{n}, where $\psi_{i}$ are $\mathsf{FO}(\rm inc)$-formulae. By Theorem 5.6 each $\psi_{i}$ is equivalent to some $\mathsf{PosGFP}$-sentence $\Phi_{i}(R)$. Define

[TABLE]

where $\Phi_{i}(y/0,z/1)$ are obtained from $\Phi_{i}$ by substituting $y$ and $z$ respectively for [math] and $1$. Let $R_{1},\ldots,R_{n}$ be fresh relation symbols with respective arities $|\overline{x}^{1}|,\ldots,|\overline{x}^{n}|$. Let $\Phi^{\prime}$ be the formula obtained from $\Phi$ by replacing each atom $R(\overline{y}_{1},\ldots,\overline{y}_{n})$, where $\overline{y}_{1},\ldots,\overline{y}_{n}$ are tuples of variables with respective lengths $|\overline{x}^{1}|,\ldots,|\overline{x}^{n}|$, with the conjunction $R_{1}(\overline{y}_{1})\wedge\ldots\wedge R_{n}(\overline{y}_{n})$. The following equivalence holds for all structures $\mathfrak{A}$, with at least two elements, and strictly non-empty polyteams $\overline{X}=(X_{1},\ldots,X_{n})$. Let $X$ denote the team representation of $\overline{X}$ obtained by taking the Cartesian product of the teams $X_{i}$, $1\leq i\leq n$.

[TABLE]

where $\mathfrak{A}^{*}$ is an expansion of $\mathfrak{A}$ with two distinct constants [math] and $1$. The converse direction for $\mathsf{PosGFP}$-sentences follows by Theorem 5.6 and since $\mathsf{FO}(\rm inc)$ is a fragment of $\mathsf{PFO}(\rm pinc)$.∎

6 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. We also showed that polyteam semantics can sometimes be reduced to team semantics, although it can be questioned whether such an interpretation is reasonable in the first place. The examples of this paper demonstrate that polyteam semantics is a conceptually more natural framework for capturing properties of sets of relations. Specifications for multiple relations are easier to parse if different relations are explicitly distinguished in formulae. Also, if polyteam logics are interpreted as data constraint languages, as in Example 2, then the reduction from polyteam semantics to team semantics incurs an unnecessary computational overhead. First, a single team to represent the polyteam has to be constructed, e.g., by taking a Cartesian product of all coordinate teams; and second, this team has to be validated against a team logic formula which is much larger in size than the initial polyteam formula.

Our results also open up interesting avenues for further research. One question is to determine whether poly-dependence logic reduces to dependence logic. Our methods only work for poly-independence and poly-inclusion logic, and the proviso in the latter case was to include classical disjunction. As inclusion logic with classical disjunction is not union closed, it would also be interesting to study the team properties definable in this logic. Apart from poly-dependence atoms, we did not consider axioms for any other poly-atoms. Since the axioms of poly-inclusion atoms are already known from database theory, a natural next step would be to axiomatise marginal poly-independence atoms. It would also be interesting to develop axiomatic methods for more expressive fragments of polyteam logics (cf. [12, 23, 28]).