Facets of Distribution Identities in Probabilistic Team Semantics

TL;DR

This paper explores the expressive power of probabilistic team semantics, focusing on logical and probabilistic dependencies, and addresses the complexity of the implication problem of conditional independence.

Contribution

It classifies the expressive power of various probabilistic atoms and relates the framework to the first-order theory of the reals, advancing understanding of probabilistic dependencies.

Findings

Classifies expressive power of probabilistic atoms

Relates probabilistic team semantics to the first-order theory of reals

Addresses complexity of the implication problem of conditional independence

Abstract

We study probabilistic team semantics which is a semantical framework allowing the study of logical and probabilistic dependencies simultaneously. We examine and classify the expressive power of logical formalisms arising by different probabilistic atoms such as conditional independence and different variants of marginal distribution equivalences. We also relate the framework to the first-order theory of the reals and apply our methods to the open question on the complexity of the implication problem of conditional independence.

Tables

Table 1. Table 1: Relative expressivity in probabilistic team semantics (PTS) and team semantics (TS)

PTS:
TS:	[12, 13]

Equations

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

$$\mathbb{X}[A/x](s(a/x))=\sum _{\begin{array}{c}t\in X\\ t(a/x)=s(a/x)\end{array}}\mathbb{X}(t)\cdot \frac{1}{|A|},$$

$$\mathbb{X}[F/x](s(a/x))=\sum _{\begin{array}{c}t\in X\\ t(a/x)=s(a/x)\end{array}}\mathbb{X}(t)\cdot F(t)(a),$$

$$\mathfrak{A}{\models }_{\mathbb{X}}\psi \iff \forall s\in X\text{ such that }\mathbb{X}(s)>0:\mathfrak{A}{\models }_s\psi .$$

$$|{\mathbb{X}}_{\vec{x}=\vec{a}}|:=\sum _{\begin{array}{c}s(\vec{x})=\vec{a}\\ s\in X\end{array}}\mathbb{X}(s).$$

$$\mathfrak{A}{\models }_{\mathbb{X}}\vec{x}\approx \vec{y}\iff |{\mathbb{X}}_{\vec{x}=\vec{a}}|=|{\mathbb{X}}_{\vec{y}=\vec{a}}|\text{ for each a∈Ak}.$$

$$\mathfrak{A}{\models }_{\mathbb{X}}\vec{x}{\approx }^{\ast }\vec{y}\iff \{\{|{\mathbb{X}}_{\vec{x}=\vec{a}}|>0\mid \vec{a}\in A^{|\vec{x}|}\}\}=\{\{|{\mathbb{X}}_{\vec{y}=\vec{b}}|>0\mid \vec{b}\in A^{|\vec{y}|}\}\}.$$

$$\mathfrak{A}{\models }_{\mathbb{X}}\vec{y}\perp {\perp }_{\vec{x}}\vec{z}$$

$$|{\mathbb{X}}_{\vec{x}\vec{y}=s(\vec{x}\vec{y})}|\cdot |{\mathbb{X}}_{\vec{x}\vec{z}=s(\vec{x}\vec{z})}|=|{\mathbb{X}}_{\vec{x}\vec{y}\vec{z}=s(\vec{x}\vec{y}\vec{z})}|\cdot |{\mathbb{X}}_{\vec{x}=s(\vec{x})}|.$$

$$\mathfrak{A}{\models }_X=(\vec{x},\vec{y})\iff s(\vec{x})=s^{\prime }(\vec{x})\text{ implies }s(\vec{y})=s^{\prime }(\vec{y})\text{ for all }s,s^{\prime }\in X.$$

$$\exists qr\big{[}x_{1}\ldots x_{n}~{}\!\!\perp\!\!\!\perp\!\!~{}r\wedge\bigvee_{i=1}^{n}r=i\wedge\bigwedge_{i=1}^{n}\exists x^{\prime}r^{\prime}\big{(}x_{i}r\approx x^{\prime}r^{\prime}\wedge[(q=i\vee r^{\prime}=i)\to yq=x^{\prime}r^{\prime}]\big{)}\big{]},$$

$$o_i\perp {\perp }_{\vec{m}}(o_1,\dots ,o_{i-1},o_{i+1},\dots ,o_m)$$

$$P(t,c,g,a)=P(t)\cdot P(c\mid t)\cdot P(g\mid t,c)\cdot P(a\mid t,c)$$

$$t=T\vee (t=F\wedge g\perp \perp c).$$

$$\mathfrak{A}{\models }_{\mathbb{X}}(\psi \vee \theta )\iff \mathfrak{A}{\models }_{\mathbb{Y}}\psi \text{ and }\mathfrak{A}{\models }_{\mathbb{Z}}\theta \text{ for some Y,Z s.t. }\mathbb{Y}\bigsqcup \mathbb{Z}=\mathbb{X},$$

$${\mathbb{X}}_{x=a}=\frac{1}{|S|}\text{ for all }a\in S\text{ and }{X}_{x=a}=0\text{ otherwise}.$$

$$\mathcal{M}{\models }_{\mathbb{X}}\varphi \iff$$

$$d$$

$$(\vec{z}\perp\!\!\!\perp d)\land\forall a\in\{c_{1},c_{2}\}\exists b\in\{c_{1},c_{2}\}\big{[}(a\perp\!\!\!\perp b)\land\big{(}(a=b\land d=c_{1})\lor(a\neq b\land d=c_{2})\big{)}\big{]}.$$

$$\mathfrak{A}{\models }_{\mathbb{X}}\varphi$$

$$\big{[}(a\perp\!\!\!\perp b)\land\big{(}(a=b\land d=c_{1})\lor(a\neq b\land d=c_{2})\big{)}\big{]}$$

$$\phi:=\forall\vec{z}\big{(}(\vec{z}\neq\vec{x}\wedge\vec{z}\neq\vec{y})\vee((\vec{z}=\vec{x}\vee\vec{z}=\vec{y})\wedge\vec{z}\approx^{*}\vec{x}\wedge\vec{z}\approx^{*}\vec{y})\big{)}.$$

$$|{\mathbb{Y}}_{\vec{x}=\vec{i}}|=|{\mathbb{X}}_{\theta \wedge \vec{x}=\vec{i}}^{\prime }|=|{\mathbb{X}}_{\theta \wedge \vec{x}=\vec{i}\wedge \vec{x}\ne \vec{y}}^{\prime }|+|{\mathbb{X}}_{\theta \wedge \vec{x}=\vec{i}\wedge \vec{y}=\vec{i}}^{\prime }|=\frac{2l_{\vec{i}}+c_{\vec{i}}}{n^m}.$$

$$|{\mathbb{Y}}_{\vec{y}=\vec{i}}|=\frac{2r_{\vec{i}}+c_{\vec{i}}}{n^m}\text{ and }|{\mathbb{Y}}_{\vec{z}=\vec{i}}|=\frac{r_{\vec{i}}+l_{\vec{i}}+c_{\vec{i}}}{n^m}.$$

$$W_{\vec{x}}:=\{\{2l_{\vec{1}}+c_{\vec{1}},\dots ,2l_{\vec{n}}+c_{\vec{n}}\}\},$$

$$W_{\vec{y}}:=\{\{2r_{\vec{1}}+c_{\vec{1}},\dots ,2r_{\vec{n}}+c_{\vec{n}}\}\},$$

$$W_{\vec{z}}:=\{\{l_{\vec{1}}+r_{\vec{1}}+c_{\vec{1}},\dots ,l_{\vec{n}}+r_{\vec{n}}+c_{\vec{n}}\}\},$$

$$\text{if }\mathfrak{A}{\models }_{\mathbb{X}}\varphi \text{ and }\mathfrak{A}{\models }_{\mathbb{Y}}\varphi \text{, then }\mathfrak{A}{\models }_{\mathbb{X}{\bigsqcup }_k\mathbb{Y}}\varphi .$$

$$\varphi ::=p\mid \neg p\mid \varphi \vee \varphi \mid \varphi \wedge \varphi \mid \exists p\varphi \mid \forall p\varphi ,$$

$$\psi:=\exists s_{\vec{p}=\vec{0}}\ldots s_{\vec{p}=\vec{1}}\big{(}\bigwedge_{\vec{i}}0\leq s_{\vec{p}=\vec{i}}\ \wedge\neg 0=\sum_{\vec{i}}s_{\vec{p}=\vec{i}}\wedge\phi^{*}(\vec{s})\big{)}$$

$$\underset{\vec{i}\vec{j}\vec{k}}{\bigwedge }($$

$${\varphi }^{\ast }(\vec{s}):=\underset{\vec{i}}{\bigwedge }\sum _{{\vec{j}}^{\prime }{\vec{k}}^{\prime }}{s}_{\vec{a}\vec{b}\vec{c}=\vec{i}{\vec{j}}^{\prime }{\vec{k}}^{\prime }}=\sum _{{\vec{j}}^{\prime }{\vec{k}}^{\prime }}{s}_{\vec{a}\vec{b}\vec{c}={\vec{j}}^{\prime }\vec{i}{\vec{k}}^{\prime }}.$$

Full text

\NewEnviron

reptheorem[1]

\NewEnviron

replemma[1]

11institutetext: University of Helsinki, Finland 11email: {miika.hannula,asa.hirvonen,juha.kontinen}@helsinki.fi 22institutetext: Aalto University, Finland, 22email: vadim.kulikov@iki.fi 33institutetext: Hasselt University, Belgium, 33email: jonni.virtema@uhasselt.be

Facets of Distribution Identities in Probabilistic Team Semantics††thanks: The first and the third author were supported by grant 308712, the fourth by grant 285203 of the Academy of Finland.

Miika Hannula 11 0000-0002-9637-6664

  

Åsa Hirvonen 11 0000-0003-2149-4153

  

Juha Kontinen 11 0000-0003-0115-5154

  

Vadim Kulikov 1122   

Jonni Virtema 33 0000-0002-1582-3718

1 Introduction

Team semantics, introduced by Hodges [20] and popularised by Väänänen [25], shifts the focus of logics away from assignments as the primitive notion connected to satisfaction. In team semantics formulae are evaluated with respect to sets of assignments (i.e., teams) as opposed to single assignments of Tarskian semantics. During the last decade the research on team semantics has flourished, many logical formalisms have been defined, and surprising connections to other fields identified. In particular, several promising application areas of team semantics have been identified recently. Krebs et al. [22] developed a team based approach to linear temporal logic for the verification of information flow properties. In applications to database theory, a team corresponds exactly to a database table (see, e.g., [16]). Hannula et al. [18] introduced a framework that extends the connection of team semantics and database theory to polyrelational databases and data exchange.

The focus of this article is probabilistic team semantics which connects team based logics to probabilistic dependency notions. Probabilistic team semantics is built compositionally upon the notion of a probabilistic team, that is, a probability distribution over variable assignments. While the first ideas of probabilistic teams trace back to the works of Galliani [11] and Hyttinen et al. [21], the systematic study of the topic was initiated and further continued by Durand et al. in [8, 9]. It is worth noting that in [2] so-called causal teams have been introduced to logically model causality and interventions. Probabilistic team semantics has also a close connection to the area of metafinite model theory [14]. In metafinite model theory, finite structures are extended with an another (infinite) domain sort such as the real numbers (often with arithmetic) and with weight functions that work as a bridge between the two sorts. This approach provides an elegant way to model weighted graphs and other structures that refer to infinite structures. The exact relationship between probabilistic team semantics and logics over metafinite models as well as with probabilistic databases of [6] will be a topic of future research.

The starting point of this work comes from [9] in which probabilistic team semantics was defined following the lines of [11]. The main theme in [9] was to characterize logical formalisms in this framework in terms of existential second-order logic. Two main probabilistic dependency atoms were examined. The probabilistic conditional independence atom $\vec{y}~{}\!\!\perp\!\!\!\perp_{\vec{x}}\!\!~{}\vec{z}$ states that the two variable tuples $\vec{y}$ and $\vec{z}$ are independent given the third tuple $\vec{x}$. The marginal identity atom $\vec{x}\approx\vec{y}$ states that the marginal distributions induced from the two tuples $\vec{x}$ and $\vec{y}$ (of the same length) are identical. The extension of first-order logic with these atoms (${\rm FO}(\perp\!\!\!\perp_{\rm c},\approx)$) was then shown to correspond to a two-sorted variant of existential second-order logic that allows a restricted access to arithmetical operations for numerical function terms. What was left unexamined were the relationships between different logical formalisms in probabilistic team semantics. In fact, it was unknown whether there are any meaningful probabilistic dependency notions such that the properties definable with one notion are comparable to those definable with another.

In this article we study the relative expressivity of first-order logic with probabilistic conditional independence atoms (${\rm FO}(\perp\!\!\!\perp_{\rm c})$) and with marginal identity atoms (${\rm FO}(\approx)$). The logic ${\rm FO}(\approx)$ is a probabilistic variant of inclusion logic that is strictly less expressive than independence logic, after which ${\rm FO}(\perp\!\!\!\perp_{\rm c})$ is modelled [12, 15]. In addition, we examine ${\rm FO}(\approx^{*})$ which is another extension defined in terms of so-called marginal distribution equivalence. The marginal distribution equivalence atom $\vec{x}\approx^{*}\vec{y}$ for two variable tuples $\vec{x}$ and $\vec{y}$ (not necessarily of the same length) relaxes the truth condition of the marginal identity atom in that the two distributions induced from $\vec{x}$ and $\vec{y}$ are required to determine the same multisets of probabilities. The aforementioned open question is now answered in the positive. The logics mentioned above are not only comparable, but they form a linear expressivity hierarchy: ${\rm FO}(\approx)<{\rm FO}(\approx^{*})\leq{\rm FO}(\perp\!\!\!\perp_{\rm c})$. We also show that ${\rm FO}(\approx)$ enjoys a union closure property that is a generalization of the union closure property of inclusion logic, and that conditional independence atoms $\vec{y}~{}\!\!\perp\!\!\!\perp_{\vec{x}}\!\!~{}\vec{z}$ can be defined with an access to only marginal independence atoms $\vec{x}~{}\!\!\perp\!\!\!\perp\!\!~{}\vec{y}$ between two variable tuples. Furthermore, we show that, surprisingly, ${\rm FO}(\approx^{*})$ corresponds to ${\rm FO}(\approx,=\!\!(\cdot))$, where $=\!\!(\cdot)$ refers to the dependence atom defined as a declaration of functional dependence over the support of the probabilistic team. The question whether ${\rm FO}(\approx,=\!\!(\cdot))$ is strictly less expressive than ${\rm FO}(\perp\!\!\!\perp_{\rm c})$ is left as an open question; in team semantics the corresponding logics are known to be equivalent. The above findings look outwardly very similar to many results in team semantics. However, it is important to note that, apart perhaps from the union closure property, the results of this paper base on entirely new ideas and do not recycle old arguments from the team semantics context.

We also investigate (quantified) propositional logics with probabilistic team semantics. By connecting these logics to the arithmetic of the reals we show upper bounds for their associated computational problems. Our results suggest that the addition of probabilities to team semantics entails an increase in the complexity. Satisfiability of propositional team logic ($\mathrm{PL}(\sim)$), i.e., propositional logic with classical negation is in team semantics known to be complete for alternating exponential time with polynomially many alternations [19]. Shifting to probabilistic team semantics analogous problems are here shown to enjoy double exponential space upper bound. This is still lower than the complexity of satisfiability for modal team logic ($\mathrm{ML}(\sim)$) in team semantics, known to be complete for the non-elementary complexity class $\mathsf{TOWER}(poly)$ which consists of problems solvable in time restricted by some tower of exponentials of polynomial height [23]. One intriguing consequence of our translation to real arithmetic is that the implication problem of conditional independence statements over binary distributions is decidable in exponential space. The decidability of this problem is open relative to all discrete probability distributions [24].

2 Preliminaries

First-order variables are denoted by $x,y,z$ and tuples of first-order variables by $\vec{x},\vec{y},\vec{z}$. By $\mathrm{Var}(\vec{x})$ we denote the set of variables that appear in the variable sequence $\vec{x}$. The length of the tuple $\vec{x}$ is denoted by $\lvert\vec{x}\rvert$. A vocabulary $\tau$ is a set of relation symbols and function symbols with prescribed arities. We mostly denote relation symbols by $R$ and function symbols by $f$, and the related arities by $\operatorname{ar}(R)$ and $\operatorname{ar}(f)$, respectively. The closed interval of real numbers between [math] and $1$ is denoted by $[0,1]$. Given a finite set $A$, a function $f\colon A\to[0,1]$ is called a (probability) distribution if $\sum_{s\in A}f(s)=1$. In addition, the empty function is a distribution.

The probabilistic logics investigated in this paper are extensions of first-order logic ${\rm FO}$ over a vocabulary $\tau$ given by the grammar rules:

[TABLE]

where $\vec{x}$ is a tuple of first-order variables and $R$ a relation symbol from $\tau$.

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 equal to $s$ with the exception that $s(a/x)(x)=a$. A team $X$ is a finite set of assignments from $D$ to $A$. The set $D$ is called the domain of $X$ (written $\operatorname{Dom}(X)$) and the set $A$ the range of $X$ (written $\operatorname{Ran}(X)$). Let $X$ be a team with range $A$, and let $F\colon X\to\mathcal{P}(A)\setminus\{\emptyset\}$ be 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)\}$. A probabilistic team $\mathbb{X}$ is a distribution $\mathbb{X}\colon X\rightarrow[0,1]$. Let $\mathfrak{A}$ be a $\tau$-structure and $\mathbb{X}:X\to[0,1]$ a probabilistic team such that the domain of $\mathfrak{A}$ is the range of $X$. Then we say that $\mathbb{X}$ is a probabilistic team of $\mathfrak{A}$. In the following, we will define two notations $\mathbb{X}[A/x]$ and $\mathbb{X}[F/x]$. Let $\mathbb{X}\colon X\to[0,1]$ be a probabilistic team, $A$ a finite non-empty set, $p_{A}$ the set of all probability distributions $d\colon A\to[0,1]$, and $F\colon X\to p_{A}$ a function. We denote by $\mathbb{X}[A/x]$ the probabilistic team $X[A/x]\to[0,1]$ such that

[TABLE]

for each $a\in A$ and $s\in X$. Note that if $x$ does not belong to the domain of $X$ then the righthand side of the above equation is simply $\mathbb{X}(s)\cdot\frac{1}{\lvert A\rvert}$. By $\mathbb{X}[F/x]$ we denote the probabilistic team $X[A/x]\to[0,1]$ defined such that

[TABLE]

for each $a\in A$ and $s\in X$. Again if $x$ does not belong to the domain of $X$, $\sum$ can be dropped from the above equation.

If $\mathbb{Y}\colon X\to[0,1]$ and $\mathbb{Z}\colon X\to[0,1]$ are probabilistic teams and $k\in[0,1]$, then we write $\mathbb{Y}\sqcup_{k}\mathbb{Z}$ for the $k$-scaled union of $\mathbb{Y}$ and $\mathbb{Z}$, that is, the probabilistic team $\mathbb{Y}\sqcup_{k}\mathbb{Z}\colon X\to[0,1]$ defined such that $(\mathbb{Y}\sqcup_{k}\mathbb{Z})(s)=k\cdot\mathbb{Y}(s)+(1-k)\cdot\mathbb{Z}(s)$ for each $s\in X$.

We may now define probabilistic team semantics for first-order formulae. The definition is the same as in [9]. The only exception is that it is here applied to probabilistic teams that have real probabilities, whereas in [9] rational probabilities were used.

Definition 1

Let $\mathfrak{A}$ be a probabilistic $\tau$-structure over a finite domain $A$, and $\mathbb{X}\colon X\to[0,1]$ a probabilistic team of $\mathfrak{A}$. The satisfaction relation $\models_{\mathbb{X}}$ for first-order logic is defined as follows:

[TABLE]

Probabilistic team semantics is in line with Tarskian semantics for first-order formulae ($\models_{s}$):

[TABLE]

In particular the non-classical semantics for negation is required for the above equivalence to hold.

In this paper we consider three probabilistic atoms: marginal identity, probabilistic independence, and marginal distribution equivalence atom. The first two were first introduced in the context of multiteam semantics in [8], and they extend the notions of inclusion and independence atoms from team semantics [12].

We define $|\mathbb{X}_{\vec{x}=\vec{a}}|$ where $\vec{x}$ is a tuple of variables and $\vec{a}$ a tuple of values, as

[TABLE]

If $\phi$ is some first-order formula, then $|\mathbb{X}_{\phi}|$ is defined analogously as the total sum of weights of those assignments in $X$ that satisfy $\phi$.

If $\vec{x},\vec{y}$ are variable sequences of length $k$, then $\vec{x}\approx\vec{y}$ is a marginal identity atom with the following semantics:

[TABLE]

Note that the equality $|{\mathbb{X}}_{\vec{x}=\vec{a}}\rvert=\lvert{\mathbb{X}}_{\vec{y}=\vec{a}}\rvert$ in (4) can be equivalently replaced with $\lvert{\mathbb{X}}_{\vec{x}=\vec{a}}\rvert\leq\lvert{\mathbb{X}}_{\vec{y}=\vec{a}}\rvert$ since the tuples $\vec{a}$ range over $A^{k}$ for a finite $A$ (see [8, Definition 7] for details). Due to this alternative formulation, marginal identity atoms were in [8] called probabilistic inclusion atoms. Intuitively, the atom $\vec{x}\approx\vec{y}$ states that the distributions induced from $\vec{x}$ and $\vec{y}$ are identical.

The marginal distribution equivalence atom is defined in terms of multisets of assignment weights. We distinguish multisets from sets by using double wave brackets, e.g., $\{\{a,a,b\}\}$ denotes the multiset $(\{a,b\},m)$ where $a$ and $b$ are given multiplicities $m(a)=2$ and $m(b)=1$. If $\vec{x},\vec{y}$ are variable sequences, then $\vec{x}\approx^{*}\vec{y}$ is a marginal distribution equivalence atom with the following semantics:

[TABLE]

The next example illustrates the relationships between marginal distribution equivalence atoms and marginal identity atoms; the latter implies the former, but not vice versa.

Example 1

Let $\mathbb{X}$ be the probabilistic team depicted in Figure 1. The team $\mathbb{X}$ satisfies the atoms $xy\approx^{*}y$, $x\approx^{*}y$, $y\approx^{*}z$, and $y\approx z$. The team $\mathbb{X}$ falsies the atom $x\approx y$, whereas $xy\approx y$ is not a well formed formula.

If $\vec{x},\vec{y},\vec{z}$ are variable sequences, then $\vec{y}~{}\!\!\perp\!\!\!\perp_{\vec{x}}\!\!~{}\vec{z}$ is a probabilistic conditional independence atom with the satisfaction relation defined as

[TABLE]

if for all $s\colon\mathrm{Var}(\vec{x}\vec{y}\vec{z})\to A$ it holds that

[TABLE]

Furthermore, we define probabilistic marginal independence atom $\vec{x}~{}\!\!\perp\!\!\!\perp\!\!~{}\vec{y}$ as $\vec{x}~{}\!\!\perp\!\!\!\perp_{\emptyset}\!\!~{}\vec{y}$, i.e., probabilistic independence conditioned by the empty tuple.

In addition to atoms based on counting or arithmetic operations, we may also include all dependency atoms from the team semantics literature. Let $\alpha$ be an atom that is interpreted in team semantics, let $\mathfrak{A}$ be a finite structure, and $\mathbb{X}:X\to[0,1]$ a probabilistic team. We define $\mathfrak{A}\models_{\mathbb{X}}\alpha$ if $\mathfrak{A}\models_{X^{+}}\alpha$, where $X^{+}$ consists of those assignments of $X$ that are given positive weight by $\mathbb{X}$. In this paper we will discuss dependence atoms also in the context of probabilistic team semantics. If $\vec{x},\vec{y}$ are two variable sequences, then $=\!\!(\vec{x},\vec{y})$ is a dependence atom with team semantics:

[TABLE]

A dependence atom of the form $=\!\!(\emptyset,\vec{x})$ is called a constancy atom, written $=\!\!(\vec{x})$ in shorthand notation. Dependence atoms can be expressed by using probabilistic independence atoms. This has been shown for multiteams in [8], and the proof applies to probabilistic teams.

Proposition 2 ([8])

Let $\mathfrak{A}$ be a structure, $\mathbb{X}:X\to[0,1]$ a probabilistic team of $\mathfrak{A}$, and $\vec{x}$ and $\vec{y}$ two sequences of variables. Then $\mathfrak{A}\models_{\mathbb{X}}=\!\!(\vec{x},\vec{y})\Leftrightarrow\mathfrak{A}\models_{\mathbb{X}}\vec{y}~{}\!\!\perp\!\!\!\perp_{\vec{x}}\!\!~{}\vec{y}.$

Given a collection $C$ of atoms from $\{\perp\!\!\!\perp_{\rm c},\perp\!\!\!\perp,\approx,\approx^{*},=\!\!(\cdot)\}$, we write ${\rm FO}(C)$ for the logic that extends ${\rm FO}$ with the atoms in $C$.

Example 2

Let $f_{1},\ldots,f_{n},g$ be univariate distributions. Then $g$ is a finite mixture of $f_{1},\ldots,f_{n}$ if it can be expressed as a convex combination of $f_{1},\ldots,f_{n}$, i.e., if there are non-negative real numbers $r_{1},\ldots,r_{n}$ such that $r_{1}+\ldots+r_{n}=1$ and $g(a)=\sum_{i=1}^{n}r_{i}f_{i}(a)$. A probabilistic team $\mathbb{X}:X\to[0,1]$ gives rise to a univariate distribution $f_{x}(a):=|\mathbb{X}_{x=a}|$ for each variable $x$ from the domain of $X$. The next formula expresses that the distribution $f_{y}$ is a finite mixture of the distributions $f_{x_{1}},\ldots,f_{x_{n}}$:

[TABLE]

where the indices $1,\ldots,n$ are also thought of as distinct constants, and $(q=i\vee r^{\prime}=i)\to yq=x^{\prime}r^{\prime}$ stands for $\neg(q\neq i\wedge r^{\prime}\neq i)\vee yq=x^{\prime}r^{\prime}$. The non-negative real numbers $r_{i}$ are represented by the weights of $r=i$ where $r$ is distributed independently of each $x_{i}$. The summand $r_{i}f_{x_{i}}(a)$ is then represented by the weight of $x_{i}r=ai$ and $f_{y}(a)$ by the weight of $y=a$. The quantified subformula expresses that the former weight matches the weight of $yq=ai$, which implies that $f_{y}(a)$ is $r_{1}f_{x_{1}}(a)+\ldots+r_{n}f_{x_{n}}(a)$.

Example 3

Probabilistic team semantics can be also used to model properties of data obtained from a quantum experiment (adapting the approach of [1]). Consider a probabilistic team $\mathbb{X}$ over variables $m_{1},\dots,m_{n},o_{1},\dots,o_{n}$. The intended interpretation of $\mathbb{X}(s)=r$ is that the joint probability that $s(m_{i})$ was measured with outcome $s(o_{i})$, for $1\leq i\leq m$, is $r$. In this setting many important properties of the experiment can be expressed using our formalism. For example the formula

[TABLE]

expresses a property called Outcome-Independence; given the measurements $\vec{m}$, the outcome at $i$ is independent of the outcomes at other positions. The dependence atom $=\!\!(\vec{m},\vec{o})$ on the other hand corresponds to a property called Weak-Determinism. Moreover, if $\phi$ describes some property of hidden-variable models (Outcome-Independence, etc.), then the formula $\exists\lambda\phi$ expresses that the experiment can be explained by a hidden-variable model satisfying that property.

The next example relates probabilistic team semantics to Bayesian networks. The example is an adaptation of an example discussed also in [8].

Example 4

Consider the Bayesian network $\mathbb{G}$ in Fig. 2 that models beliefs about house safety using four Boolean random variables thief, cat, guard and alarm. We refer to these variables by $t,c,g,a$. The dependence structure of a Bayesian network is characterized by the so-called local directed Markov property stating that each variable is conditionally independent of its non-descendants given its parents. For our network $\mathbb{G}$ the only non-trivial independence given by this property is $g~{}\!\!\perp\!\!\!\perp_{tc}\!\!~{}a$. Hence a joint distribution $P$ over $t,c,g,a$ factorizes according to $\mathbb{G}$ if $\mathbb{X}$ satisfies $g~{}\!\!\perp\!\!\!\perp_{tc}\!\!~{}a$. In this case $P$ can be factorized by

[TABLE]

where, for instance, $t$ abbreviates either $\texttt{thief}=T$ or $\texttt{thief}=F$, and $P(c\mid t)$ is the probability of $c$ given $t$. The joint probability distribution (i.e., the team $\mathbb{X}$) can hence be stored as in Fig. 2. Note that while $\mathbb{G}$ expresses the independence statement $g~{}\!\!\perp\!\!\!\perp_{tc}\!\!~{}a$, $\mathrm{FO}(\perp\!\!\!\perp_{\rm c},\approx)$-formulas can be used to further refine the joint probability distribution as follows. Assume we have information suggesting that we may safely assume an $\mathrm{FO}(\perp\!\!\!\perp_{\rm c},\approx)$ formula $\phi$ on $\mathbb{X}$:

• •

$\phi:=t=F\to g=F$ indicates that guard never raises alarm in absence of thief. In this case the two bottom rows of the conditional probability distribution for guard become superfluous.

• •

the assumption that $\phi$ is satisfied also exemplifies an interesting form of contex-specific independence (CSI) that cannot be formalized by the usual Bayesian networks (see, e.g., [7]). Namely, $\phi$ implies that guard is independent of cat in the context $\texttt{thief}=F$. Interestingly such CSI statements can be formalized utilizing the disjunction of $\mathrm{FO}(\perp\!\!\!\perp_{\rm c},\approx)$:

[TABLE]

• •

satisfaction of $\phi:=tca\approx tcg$ would imply that alarm and guard have the same reliability for any given value of thief and cat. Consequently, the conditional distributions for alarm and guard are equal and one of the them could be removed.

The following locality property dictates that satisfaction of a formula $\phi$ in probabilistic team semantics depends only on the free variables of $\phi$. For this, we define the restriction of a team $X$ to $V$ as $X\upharpoonright V=\{s\upharpoonright V\mid s\in X\}$ where $s\upharpoonright V$ denotes the restriction of the assignment $s$ to $V$. The restriction of a probabilistic team $\mathbb{X}:X\to[0,1]$ to $V$ is then defined as the probabilistic team $\mathbb{Y}\colon X\upharpoonright V\to[0,1]$ where $\mathbb{Y}(s)=\sum_{s^{\prime}\upharpoonright V=s}\mathbb{X}(s^{\prime}).$ The set of free variables $\operatorname{Fr}(\phi)$ of a formula over probabilistic team semantics is defined recursively as in first-order logic; note that for any atom $\phi$, $\operatorname{Fr}(\phi)$ consists of all variables that appear in $\phi$.

Proposition 3 (Locality, [9])

Let $\phi(\vec{x})\in{\rm FO}(\perp\!\!\!\perp_{\rm c},\approx,\approx^{*},=\!\!(\cdot))$ be a formula with free variables from $\vec{x}=(x_{1},\ldots,x_{n})$. Then for all structures $\mathfrak{A}$ and probabilistic teams $\mathbb{X}:X\to[0,1]$ where $\{x_{1},\ldots,x_{n}\}\subseteq V\subseteq\operatorname{Dom}(X)$, $\mathfrak{A}\models_{\mathbb{X}}\phi\iff\mathfrak{A}\models_{\mathbb{X}\upharpoonright V}\phi.$

Given two logics $\mathcal{L}$ and $\mathcal{L}^{\prime}$ over probabilistic team semantics, we write $\mathcal{L}\leq\mathcal{L}^{\prime}$ if for all open formulae $\phi(\vec{x})\in\mathcal{L}$ there is a formula $\psi(\vec{x})\in\mathcal{L}^{\prime}$ such that $\mathfrak{A}\models_{\mathbb{X}}\phi\Leftrightarrow\mathfrak{A}\models_{\mathbb{X}}\psi$, for all structures $\mathfrak{A}$ and probabilistic teams $\mathbb{X}$. The equality ”$\equiv$” and strict inequality ”$<$” relations between $\mathcal{L}$ and $\mathcal{L}^{\prime}$ are defined from ”$\leq$” in the standard way.

Alternative Definition.

Probabilistic teams can also be defined as mappings $\mathbb{X}:X\to\mathbb{R}_{\geq 0}$ that have no restriction for the total sum of assignment weights, $\mathbb{R}_{\geq 0}$ being the set of all non-negative reals. Probabilistic team semantics with respect to such real weighted teams is then given exactly as in Definition 1, except that we define disjunction without scaling:

[TABLE]

where the union $\mathbb{Y}\sqcup\mathbb{Z}$ is defined such that $(\mathbb{Y}\sqcup\mathbb{Z})(s)=\mathbb{Y}(s)+\mathbb{Z}(s)$ for each $s$. Whether interpreting probabilistic teams as probability distributions or just mappings from assignments to non-negative reals does not make any difference in our framework. Hence we write $\mathbb{X}:X\to[0,1]$ for a probabilistic team that is a distribution such that $\sum_{s\in X}\mathbb{X}(s)=1$, and $\mathbb{X}:X\to\mathbb{R}_{\geq 0}$ for a probabilistic team that is any mapping from assignments to non-negative reals. A probabilistic team of the former type is then a special case of that of the latter. We will use both notions and their associated semantics interchangeably. If we need to distinguish between the two semantics, we write $\models^{[0,1]}$ and $\models^{\geq 0}$ respectively for the scaled (i.e., Definition 1) and non-scaled variants. Given $\mathbb{X}:X\to\mathbb{R}_{\geq 0}$ and $r\in\mathbb{R}_{\geq 0}$, we write $|\mathbb{X}|$ for the total weight $\sum_{s\in X}\mathbb{X}(s)$ of $\mathbb{X}$, and $r\cdot\mathbb{X}$ for the probabilistic team $\mathbb{Y}:X\to\mathbb{R}_{\geq 0}$ such that $\mathbb{Y}(s)=r\cdot\mathbb{X}(s)$ for all $s\in X$. The proposition below follows from a straightforward induction (see Appendix 0.A).

{repproposition}

prop Let $\mathfrak{A}$ be a structure, $\mathbb{X}:X\to\mathbb{R}_{\geq 0}$ a probabilistic team of $\mathfrak{A}$, and $\phi\in{\rm FO}(\perp\!\!\!\perp_{\rm c},\approx,\approx^{*},=\!\!(\cdot))$. Then $\mathfrak{A}\models^{\geq 0}_{\mathbb{X}}\phi\Leftrightarrow\mathfrak{A}\models^{[0,1]}_{\frac{1}{|\mathbb{X}|}\cdot\mathbb{X}}\phi.$

3 Expressiveness of ${\rm FO}(\perp\!\!\!\perp)$

Let $\mathbb{X}\colon X\to[0,1]$ be a probabilistic team where $X$ is a finite set of assignements from a finite set $D$ of variables. A variable $x\in D$ is uniformly distributed in $\mathbb{X}$ over a set of values $S$, if

[TABLE]

The following lemma says essentially that if we can express constancy and independence for a uniform distribution, then we can express $\approx$. Note that it may happen that we can express “$\vec{x}$ uniformly distributed and independent of $\vec{y}$” even when we cannot express “$\vec{x}$ is independent of $\vec{y}$” in general. For a proof of the lemma, see Appendix 0.B.

{replemma}

lem Let $\mathfrak{A}$ be structure with at least two elements and $\vec{z}$ an $n$-tuple of variables. Let $\phi(\vec{z},d,c_{1},c_{2})$ be a formula such that for all probabilistic teams $\mathbb{X}$, whose variable domain includes $\vec{z},d,c_{1},c_{2}$ and for which $\mathfrak{A}\models_{\mathbb{X}}c_{1}\neq c_{2}$ and $\mathfrak{A}\models_{\mathbb{X}}=\!\!(c_{1})\land=\!\!(c_{2})$, it holds that

[TABLE]

Then $\vec{x}\approx\vec{y}$ can be expressed for $n$-tuples $\vec{x}$ and $\vec{y}$ using $\phi$ and the constancy atom.

Theorem 3.1

${\rm FO}(\approx)\leq{\rm FO}(\perp\!\!\!\perp)$.

Proof

Proposition 2 established that the constancy atom $=\!\!(x)$ can be equivalently expressed by the independence atom $x\!\perp\!\!\!\perp\!x$. Hence it is enough to show that we can define the formula $\phi$ of Lemma 3 by using $\perp\!\!\!\perp$.

Let $\mathfrak{A}$ and $\mathbb{X}$ be as assumed in Lemma 3. We use below $\exists b\in\{c_{1},c_{2}\}\,\theta$ as an abbreviation for $\exists b(b=c_{1}\lor b=c_{2})\land\theta$, and $\forall b\in\{c_{1},c_{2}\}\,\theta$ for \forall b(b\neq c_{1}\land b\neq c_{2})\lor\big{(}(b=c_{1}\lor b=c_{2})\land\theta\big{)}. Define $\phi(\vec{z},d,c_{1},c_{2})$ as

[TABLE]

It suffices to prove (5). The formula $\phi$ clearly states that $\vec{z}$ and $d$ are independent. The formula also states that the values of $d$ range over the values of $c_{1}$ and $c_{2}$. It remains to be shown, conditioned on that $\vec{z}$ and $d$ are independent, that

[TABLE]

Note that, by assumption of Lemma 3, $c_{1}$ and $c_{2}$ are distinct constants. Let $\mathbb{X}_{1}$ be a team obtained from $\mathbb{X}$ by the quantification of $a$ and $b$. By the definition of universal quantification, in $\mathbb{X}_{1}$ $a$ is uniformly distributed and independent of everything else except maybe $b$. Note that $d$ is uniformly distributed over the values of $c_{1}$ and $c_{2}$ in $X$ if and only if it is in $X_{1}$.

If $d$ is uniformly distributed over the values of $c_{1}$ and $c_{2}$, then picking values of $b$ with a uniform probability such that the right conjunct in

[TABLE]

holds clearly yields a team in which the left conjunct also holds. However, if $d$ is not uniformly distributed over $c_{1}$ and $c_{2}$, then picking values for $b$ such that the right conjunct of (7) holds will yield $b$ that is not independent on $a$. ∎

We also note that conditional independence is definable using marginal independence. The proof applies ideas from [9] and can be found in Appendix 0.C. {reptheorem}thm ${\rm FO}(\perp\!\!\!\perp)\equiv{\rm FO}(\perp\!\!\!\perp_{\rm c})$.

4 Expressiveness of ${\rm FO}(\approx^{*})$ and ${\rm FO}(\approx)$

Initially it may seem that first-order logic with marginal distribution equivalence atoms is less expressive than that with marginal identity atoms, as the former atoms are given a strictly weaker truth condition. Contrary to this intuition, however, we will in this section show that ${\rm FO}(\approx^{*})$ is actually strictly more expressive than ${\rm FO}(\approx)$. The result is proven in two phases. First, in Sect. 4.1 we show that dependence and marginal identity can be defined in ${\rm FO}(\approx^{*})$, the former by a single marginal distribution equivalence atom and the latter by a more complex formula. Second, in Sect. 4.2 we show that the expressiveness of ${\rm FO}(\approx)$ is restricted by a union closure property which is similar to that of inclusion logic in team semantics. Since dependence atoms lack this property, the strict inequality between ${\rm FO}(\approx)$ and ${\rm FO}(\approx^{*})$ follows.

4.1 Translations of Dependence and Marginal Identity to

${\rm FO}(\approx^{*})$

We observe first that dependence atoms can be expressed in terms of marginal distribution equivalence atoms, which in turn are definable using marginal identity and dependence atoms.

Proposition 4

The following equivalences hold:

$=\!\!(\vec{x},y)\equiv\vec{x}y\approx^{*}\vec{x}$, 2. 2.

$\vec{x}\approx^{*}\vec{y}\equiv\exists\vec{z}(=\!\!(\vec{y},\vec{z})\wedge=\!\!(\vec{z},\vec{y})\wedge\vec{x}\approx\vec{z})$.

Defining marginal identity atoms in ${\rm FO}(\approx^{*})$ is more cumbersome. Let $\mathbb{X}:X\to\mathbb{R}_{\geq 0}$ be a probabilistic team, and $\phi$ a quantifier-free first-order formula over the empty vocabulary (i.e., such that its satisfaction depends only on the variable assignment). We define $\mathbb{X}_{\phi}:X\to\mathbb{R}_{\geq 0}$ as the probabilistic team such that $\mathbb{X}_{\phi}(s)=\mathbb{X}(s)$ if $s$ satisfies $\phi$, and $\mathbb{X}_{\phi}(s)=0$ otherwise. Given two sequences of variables $\vec{x}=(x_{1},\ldots,x_{n})$ and $\vec{y}=(y_{1},\ldots,y_{n})$, we write $\vec{x}\neq\vec{y}$ as a shorthand for $\bigvee_{i=1}^{n}\neg x_{i}=y_{i}$.

Theorem 4.1

$\vec{x}\approx\vec{y}$* is equivalent to $\phi\in{\rm FO}(\approx^{*})$ where*

[TABLE]

Proof

Assume that $\vec{x},\vec{y},\vec{z}$ are all $m$-ary. Let $\mathfrak{A}$ be a structure with domain $A=\{1,\ldots,n\}$, and let $\mathbb{X}:X\to\mathbb{R}_{\geq 0}$ a probabilistic team. Assume first that $\mathfrak{A}\models_{\mathbb{X}}\vec{x}\approx\vec{y}$, that is, for all $\vec{i}\in A^{m}$, the weights $|\mathbb{X}_{\vec{x}=\vec{i}}|$ and $|\mathbb{X}_{\vec{y}=\vec{i}}|$ coincide. It suffices to show that $\mathfrak{A}\models_{\mathbb{Y}}\vec{z}\approx^{*}\vec{x}\wedge\vec{z}\approx^{*}\vec{y}$ for $\mathbb{Y}:=\mathbb{X}^{\prime}_{\theta}$ where $\theta$ is $\vec{z}=\vec{x}\vee\vec{z}=\vec{y}$ and $\mathbb{X}^{\prime}=\mathbb{X}[A^{m}/\vec{z}]$ is the probabilistic team obtained from $\mathbb{X}$ by distributing $A^{m}$ to $\vec{z}$ uniformly. For each $\vec{i}\in A^{m}$ we consider three weight measures, obtained by dividing assignments associated with $\vec{i}$ into three parts, $l_{\vec{i}}:=|\mathbb{X}_{\vec{x}=\vec{i}\wedge\vec{x}\neq\vec{y}}|$, $r_{\vec{i}}:=|\mathbb{X}_{\vec{y}=\vec{i}\wedge\vec{x}\neq\vec{y}}|$, and $c_{\vec{i}}:=|\mathbb{X}_{\vec{x}=\vec{i}\wedge\vec{y}=\vec{i}}|$. Then

[TABLE]

Observe that for $\mathbb{X}^{\prime}_{\theta\wedge\vec{x}=\vec{i}\wedge\vec{x}\neq\vec{y}}$ we first partition each assignment in $\mathbb{X}_{\vec{x}=\vec{i}\wedge\vec{x}\neq\vec{y}}$ uniformly to $n^{m}$ parts in terms of the value of $\vec{z}$ and then keep only those parts where $\theta$ holds. Since $\vec{x}$ and $\vec{y}$ disagree for every assignment in $\mathbb{X}^{\prime}_{\vec{x}=\vec{i}\wedge\vec{x}\neq\vec{y}}$, the total weight of $\mathbb{X}^{\prime}_{\theta\wedge\vec{x}=\vec{i}\wedge\vec{x}\neq\vec{y}}$ is obtained by multiplying $l_{\vec{i}}$ with $\frac{2}{n^{m}}$. For $\mathbb{X}^{\prime}_{\theta\wedge\vec{x}=\vec{i}\wedge\vec{y}=\vec{i}}$ we have identical $\vec{x}$ and $\vec{y}$, and hence its weight is obtained by multiplying $c_{\vec{i}}$ with $\frac{1}{n^{m}}$. By analogous reasoning we obtain that

[TABLE]

Since our assumption implies $l_{\vec{i}}=r_{\vec{i}}$ for all $\vec{i}$, the claim now follows from the observation that $\{\{|\mathbb{Y}_{\vec{u}=\vec{i}}|\mid\vec{i}\in A^{m}\}\}$ are identical multisets for $\vec{u}\in\{\vec{x},\vec{y},\vec{z}\}$.

Vice versa, assuming $\mathfrak{A}\models_{\mathbb{X}}\phi$ we show $\mathfrak{A}\models_{\mathbb{X}}\vec{x}\approx\vec{y}$. Let the weights $l_{\vec{i}},r_{\vec{i}},c_{\vec{i}}$ and the probabilistic team $\mathbb{Y}$ be as above. By assumption we have $\mathfrak{A}\models_{\mathbb{Y}}\vec{z}\approx^{*}\vec{x}\wedge\vec{z}\approx^{*}\vec{y}$, and thus the following multisets are identical:

[TABLE]

where $\vec{1}=(1,\dots,1)$ and $\vec{n}=(n,\dots,n)$. Assume to the contrary that $\mathfrak{A}\not\models_{\mathbb{X}}\vec{x}\approx\vec{y}$, that is, $l_{\vec{i}}\neq r_{\vec{i}}$ for some $\vec{i}$. Observe that whenever $l_{\vec{j}}=r_{\vec{j}}$ agree, then $\vec{j}$ contributes the same weight to all $W_{\vec{x}}$, $W_{\vec{y}}$, and $W_{\vec{z}}$. Therefore, we may assume without loss of generality that $l_{\vec{i}}\neq r_{\vec{i}}$ for all $\vec{i}$. Assume that $2l_{\vec{j}}+c_{\vec{j}}$ is the smallest element from $W_{\vec{x}}$. Since $W_{\vec{x}}=W_{\vec{z}}$, it follows that $2l_{\vec{j}}+c_{\vec{j}}=l_{\vec{k}}+r_{\vec{k}}+c_{\vec{k}}$ for some $\vec{k}$. If $l_{\vec{k}}<r_{\vec{k}}$, then $2l_{\vec{k}}+c_{\vec{k}}<l_{\vec{k}}+r_{\vec{k}}+c_{\vec{k}}$ which contradicts the assumption that $2l_{\vec{j}}+c_{\vec{j}}$ is smallest. Since $W_{\vec{x}}=W_{\vec{y}}$, similar contradiction follows from $r_{\vec{k}}<l_{\vec{k}}$, too. Hence, $\mathfrak{A}\models_{\mathbb{X}}\vec{x}\approx\vec{y}$ which concludes the proof. ∎

The following theorem now combines the results of this section. Note that the translations to both directions are of linear size.

Theorem 4.2

${\rm FO}(\approx^{*})\equiv{\rm FO}(\approx,=\!\!(\cdot))$.

4.2 Scaled Union Closure of ${\rm FO}(\approx)$

Inclusion logic is known to be union closed over teams. This means that for all structures $\mathfrak{A}$, teams $X$, and inclusion logic formulae $\phi$: if $\mathfrak{A}\models_{X}\phi$ and $\mathfrak{A}\models_{Y}\phi$, then $\mathfrak{A}\models_{X\cup Y}\phi$. The following proposition, proven in Appendix 0.D, demonstrates that ${\rm FO}(\approx)$ is endowed with an analogous closure property, namely, that all formulae of ${\rm FO}(\approx)$ are closed under all $k$-scaled unions of probabilistic teams. {repproposition}prop:ucl Let $\mathfrak{A}$ be a model, $\phi\in{\rm FO}(\approx)$ a formula, and $\mathbb{X}:X\to[0,1]$ and $\mathbb{Y}:X\to[0,1]$ two probabilistic teams. Then for all $k\in[0,1]$:

[TABLE]

As a corollary we observe that ${\rm FO}(\approx)$ is strictly weaker than ${\rm FO}(\approx^{*})$. Recall from Proposition 4 that the constancy atom $=\!\!(x)$ is definable in ${\rm FO}(\approx^{*})$. However, constancy is clearly not preserved under $k$-scaled unions, therefore falling outside the scope of ${\rm FO}(\approx)$. Furthremore, by Theorem 4.1 ${\rm FO}(\approx^{*})$ is at least as expressive as ${\rm FO}(\approx)$.

Corollary 1

${\rm FO}(\approx)<{\rm FO}(\approx^{*})$.

5 Binary Probabilistic Teams

In this section we restrict attention to binary probabilistic teams and propositional logic extended with quantifiers (see [17] for related work). We define the syntax of quantified propositional logic $\mathrm{QPL}$ by the following grammar

[TABLE]

where $p$ is a proposition variable. The probabilistic team semantics of $\mathrm{QPL}$ is defined analogously to that of first-order formulae. We say that a probabilistic team $\mathbb{X}:X\to[0,1]$ is binary if $X$ assigns variables into $\{0,1\}$. For a $\mathrm{QPL}$ formula $\phi$ and a binary probabilistic team $\mathbb{X}:X\to[0,1]$, we write $\mathbb{X}\models\phi$ iff $\mathfrak{A}\models_{\mathbb{X}}\phi^{*}$, where $\phi^{*}$ is the first-order formula obtained from $\phi$ by substituting $P(p)$ for $p$ and $\neg P(p)$ for $\neg p$, and letting $\mathfrak{A}:=(\{0,1\},P^{\mathfrak{A}}:=\{1\})$. Furthermore, we denote classical negation by ”$\sim$”. That is, we write $\mathbb{X}\models\sim\phi$ if $\mathbb{X}\not\models\phi$. We let $\mathrm{QPL}(\sim)$ denote the logic obtained by the grammar (8) extended with $\sim\phi$, and denote by $\mathrm{QPL}(\sim,C)$ the extension of $\mathrm{QPL}(\sim)$ by any collection of dependencies $C$.

We observe that $\mathrm{QPL}(\sim,\perp\!\!\!\perp_{\rm c},\approx)$ can be interpreted as statements of real arithmetic. As truth in real arithmetic is decidable, this gives us some fairly conservative upper bounds with respect to the complexity of satisfiability and validity of $\mathrm{QPL}(\sim,\perp\!\!\!\perp_{\rm c},\approx)$. We say that $\phi\in\mathrm{QPL}(\sim,\perp\!\!\!\perp_{\rm c},\approx)$ is satisfiable if $\phi$ is satisfied by some non-empty binary probabilistic team.111Empty team satisfies every formula without $\sim$; with $\sim$ it is a non-interesting special case [19]. Also, $\phi$ is valid is $\phi$ is satisfied by all binary probabilistic teams. Note that the free variables of a $\mathrm{QPL}(\sim,C)$ formula are defined analogously to the first-order case.

Theorem 5.1

For each $\phi\in\mathrm{QPL}(\sim,\perp\!\!\!\perp_{\rm c})$ ($\phi\in\mathrm{QPL}(\sim,\approx)$, resp.) there exists a first-order sentence $\psi$ over vocabulary $\{+,\times,\leq,0,1\}$ ($\{+,\leq,0\}$, resp.) such that $\phi$ is satisfiable iff $(\mathbb{R},+,\times,\leq,0,1)\models\psi$ ($(\mathbb{R},+,\leq,0)\models\psi$, resp.).

Proof

We show that satisfiability of a formula $\phi\in\mathrm{QPL}(\sim,\perp\!\!\!\perp_{\rm c})$ is definable in real arithmetic in terms of the non-scaled variant of probabililistic team semantics. For a given tuple $\vec{p}=(p_{1},\ldots,p_{n})$ of proposition variables, we introduce fresh first-order variables $s_{\vec{p}=\vec{i}}$ for each propositional assignment $s(\vec{p})=\vec{i}$, where $\vec{i}$ is a binary string of length $n$. We write $\vec{s}$ to denote the complete tuple of these variables. For a $\vec{p}$ listing the free variables of $\phi$, we define

[TABLE]

where the mapping $\phi(\vec{p})\mapsto\phi^{*}(\vec{s})$ is defined recursively as follows:

• •

If $\phi(\vec{p})$ is a propositional literal, then $\phi^{*}(\vec{s}):=\bigwedge_{s\not\models\phi}s=0$.

• •

If $\phi(\vec{p})$ is $\vec{b}~{}\!\!\perp\!\!\!\perp_{\vec{a}}\!\!~{}\vec{c}$, where $\vec{p}=\vec{a}\vec{b}\vec{c}\vec{d}$ for some $\vec{d}$, then $\phi^{*}(\vec{s})$ is defined as

[TABLE]

• •

If $\phi(\vec{p})$ is $\vec{a}\approx\vec{b}$, where $\vec{p}=\vec{a}\vec{b}\vec{c}$ for some $\vec{c}$, then

[TABLE]

• •

If $\phi(\vec{p})$ is $\sim\eta(\vec{p})$, then $\phi^{*}(\vec{s}):=\neg\eta^{*}(\vec{s})$.

• •

If $\phi(\vec{p})$ is $\eta(\vec{p})\wedge\chi(\vec{p})$, then $\phi^{*}(\vec{s}):=\eta^{*}(\vec{s})\wedge\chi^{*}(\vec{s})$.

• •

If $\phi(\vec{p})$ is $\eta(\vec{p})\vee\chi(\vec{p})$, then

[TABLE]

• •

If $\phi(\vec{p})$ is $\exists q\eta(\vec{p},q)$, then

[TABLE]

• •

If $\phi(\vec{p})$ is $\forall y\eta(\vec{p},q)$, then

[TABLE]

It is straightforward to check that the claim follows. ∎

From the translation above we immediately obtain some complexity bounds for the satisfiability and validity problems of quantified propositional logics over probabilistic team semantics. We write $\mathsf{2\text{-}EXPSPACE}$ for the class of problems solvable in space $O(2^{2^{p(n)}})$, and $\mathsf{AEXPTIME}(f(n))$ ($\mathsf{2\text{-}AEXPTIME}(f(n))$, resp.) for the class of problems solvable by alternating Turing machine in time $O(2^{p(n)})$ ($O(2^{2^{p(n)}})$, resp.) with $f(n)$ many alternations, where $p$ is a polynomial.

Theorem 5.2

The satisfiability/validity problems of the logics $\mathrm{QPL}(\perp\!\!\!\perp_{\rm c},\sim)$ and $\mathrm{QPL}(\approx,\sim)$ are in $\mathsf{2\text{-}EXPSPACE}$ and $\mathsf{2\text{-}AEXPTIME}(2^{O(n)})$, respectively.

Proof

By the proof of Theorem 5.1, satisfiability and validity of quantified propositional formulae can be reduced to truth of a real arithmetic sentence of size $2^{O(n)}$. The stated upper bounds for $\mathrm{QPL}(\sim,\perp\!\!\!\perp_{\rm c})$ and $\mathrm{QPL}(\sim,\approx)$ then follow because the theory of real-closed fields, $\mathsf{Th}(\mathbb{R},+,\times,\leq,0,1)$, is in $\mathsf{EXPSPACE}$ [3], and the theory of real addition, $\mathsf{Th}(\mathbb{R},+,\leq,0)$, is in $\mathsf{AEXPTIME}(n)$ [4, 10]. ∎

We also obtain an upper bound for the implication problem of conditional independence over binary probability distributions. The implication problem for conditional independence is given as a finite set $\Sigma\cup\{\sigma\}$ of conditional independence statements, and the problem is to decide whether all probability distributions that satisfy $\Sigma$ satisfy also $\sigma$. It is a famous open problem to determine whether implication of conditional independence is decidable over discrete distributions. Since binary probabilistic teams can be interpreted as discrete distributions of binary random variables, we obtain that the implication problem for conditional independence statements is decidable in exponential space over binary distributions. The result follows since any instance of such an implication problem can be expressed as an existential formula of exponential size (Theorem 5.1), and since the existential theory of real-closed fields is in $\mathsf{PSPACE}$ [5].

Corollary 2

The implication problem for conditional independence over binary probability distributions is in $\mathsf{EXPSPACE}$.

It may be conjectured that the obtained complexity bounds are not optimal. The first-order translations provide only access to a very restricted type of arithmetic expressions. For instance, real multiplication is only available between sums of reals from the unit interval. We leave it as an open problem to determine whether the results of this section can be optimized using more refined arguments.

6 Conclusions and further directions

We have studied probabilistic team semantics in association with three notions of dependency atoms: probabilistic independence, marginal identity, and marginal distribution equivalence atoms. Our investigations give rise to an overall classification that is already familiar from the team semantics context (see Table 1). Similar to inclusion logic (${\rm FO}(\subseteq)$) in team semantics, we observed that ${\rm FO}(\approx)$ enjoys a union closure property which renders it strictly less expressive than ${\rm FO}(\approx,=\!\!(\cdot))$. A further analogous fact is that both dependence and marginal identity are definable with conditional independence, which in turn is definable using only marginal independence. An interesting open question is to determine the relationship between ${\rm FO}(\approx,=\!\!(\cdot))$ (or equivalently ${\rm FO}(\approx^{*})$) and ${\rm FO}(\perp\!\!\!\perp_{\rm c})$. Contrary to the picture arising from team semantics, we conjecture that the latter is strictly more expressive.

One motivation behind our marginal distribution equivalence atom was that it seemed to be weaker than marginal identity but still enough to guarantee the same entropy of two distributions. A natural next step would be to consider some form of entropy atom/atoms and study the expressive power of the resulting logics. The exact formulation of such atoms will make all the difference, as one can detect both functional dependencies and marginal independence if one has full access to the conditional entropy as a function.

We also studied (quantified) propositional logics with probabilistic team semantics. By connecting real-valued probabilistic teams to real arithmetic we showed upper bounds for computational problems associated with these logics. As a consequence of our translation to real arithmetic we also obtained an $\mathsf{EXPSPACE}$ upper bound for the implication problem of conditional independence statements over binary distributions.

Appendix 0.A Proof of Proposition 2

Proposition LABEL:prop

Proof

The cases for first-order literals, $\approx$, $\approx^{*}$, $=\!\!(\cdot)$ and the conjunction are immediate. The claim for the independence atom $\vec{y}~{}\!\!\perp\!\!\!\perp_{\vec{x}}\!\!~{}\vec{z}$ follows from the equivalence below together with the observation that the former is the definition of the atom in the unscaled team $\mathbb{X}$ whereas the latter is equivalent to that of the scaled team $\frac{1}{|\mathbb{X}|}\cdot\mathbb{X}$.

[TABLE]

The case for disjuction follows from the following chain of equivalences

[TABLE]

where the last equivalence follows form the definition of the disjunction for $k=\frac{\lvert\mathbb{Y}\rvert}{\lvert\mathbb{X}\rvert}$ and $1-k=\frac{\lvert\mathbb{Z}\rvert}{\lvert\mathbb{X}\rvert}$, since

[TABLE]

The cases for the quantifiers are similar; we show the case for the universal quantifier

[TABLE]

where the second last equivalence follows, since $|\mathbb{X}[A/x]\rvert=\lvert\mathbb{X}\rvert$ and $(\frac{1}{|\mathbb{X}\rvert}\cdot\mathbb{X})[A/x]=\frac{1}{|\mathbb{X}\rvert}\cdot\mathbb{X}[A/x]$.∎

Appendix 0.B Proof of Lemma 3

Lemma LABEL:lem

Proof

We will write a formula $\psi(\vec{x},\vec{y})$ which is to be equivalent with $\vec{x}\approx\vec{y}$. But first we need to define an auxiliary formula $\theta$. Define

[TABLE]

This formula says that $\vec{z}$ always equals either $\vec{x}$ or $\vec{y}$ and $d$ is a “detector” for which one it is. We use the abbreviation $\exists^{c}c_{1}c_{2}$ below to denote $\exists c_{1}\exists c_{2}(=\!\!(c_{1})\land=\!\!(c_{2})\land c_{1}\neq c_{2})$. Now define

[TABLE]

Suppose $\vec{x}\approx\vec{y}$ holds in a team $\mathbb{X}$ over variables $\vec{x}$ and $\vec{y}$. We want to show that $\psi(\vec{x},\vec{y})$ is satisfied by $\mathbb{X}$. Let $\mathbb{X}_{1}$ be the expansion of $\mathbb{X}$ obtained by the quantification of $c_{1}$, $c_{2}$, and $\vec{z}$. We may assume that $c_{1}$, $c_{2}$ were picked such that they attain constant but distinct values. Also note that $\vec{z}$ is independent of all other variables and uniformly distributed over the domain of $\mathfrak{A}$. Now let $d$ be a variable that takes its values from the values of $c_{1}$ and $c_{2}$ such that it “detects” whether $\vec{z}$ equals $\vec{x}$ or not (value of $d$ is the value of $c_{1}$ iff $\vec{z}$ and $\vec{x}$ have the same value). Let $\mathbb{X}_{2}$ be the expansion of $\mathbb{X}_{1}$ by this $d$. We need to check that $\mathbb{X}_{2}$ satisfies

[TABLE]

Let $\mathbb{X}_{3}$ be the maximal subteam of $\mathbb{X}_{2}$ where $\vec{x}\neq\vec{y}$. So now we have to check that

[TABLE]

holds in $\mathbb{X}_{3}$. Recall that $\theta$ says in particular that $\vec{z}$ equals either $\vec{x}$ or $\vec{y}$, so (9) holds in $\mathbb{X}_{3}$ if and only if $\theta\land\phi$ holds in the maximal subteam $\mathbb{X}_{4}$ of $\mathbb{X}_{3}$ in which this is the case. We also just defined $d$ to attain the value $c_{1}$ if and only if $\vec{z}=\vec{x}$ and the only other option is that $\vec{z}=\vec{y}$ in which case $d=c_{2}$, so $\theta$ is satisfied. What about $\phi$; note that $\mathbb{X}_{4}$ is such that (6) holds. Now fix any value $\vec{v}$ of $\vec{z}$ in $\mathbb{X}_{4}$. Since $\vec{x}\approx\vec{y}$ holds, we have $|\mathbb{X}_{\vec{x}=\vec{v}}|=|\mathbb{X}_{\vec{y}=\vec{v}}|$. When we expand $\mathbb{X}$ to $\mathbb{X}_{1}$ and further to $\mathbb{X}_{2}$ this property is (clearly) preserved. It is also preserved when we take the subteam $\mathbb{X}_{3}$, because when we move from $\mathbb{X}_{2}$ to $\mathbb{X}_{3}$, we only remove assignments $s$ where $s(\vec{x})=s(\vec{y})$, so if an assignment with $\vec{x}=\vec{v}$ is deleted, then also an assignment with $\vec{y}=\vec{v}$ is deleted (the same assignment). When we move to $\mathbb{X}_{4}$ we still have $|(\mathbb{X}_{4})_{\vec{x}=\vec{v}}|=|(\mathbb{X}_{4})_{\vec{y}=\vec{v}}|$ which follows from the fact that $\vec{z}$ is independent of $\vec{x},\vec{y},c_{1},c_{2}$. Therefore

[TABLE]

But this means that conditioned on $\vec{z}=\vec{v}$, $d$ is uniformly distributed in $\mathbb{X}_{4}$. Since this holds for any $\vec{v}$, $d$ is uniformly distributed and independent of $\vec{z}$ as desired and $\psi(\vec{x},\vec{y})$ is satisfied by $\mathbb{X}$.

Suppose now that a team $\mathbb{X}$ satisfies $\psi(\vec{x},\vec{y})$. We want to show that $\vec{x}\approx\vec{y}$. But the chain of reasoning above also works “backwards”. Fix a value $\vec{v}$ of $\vec{x}$. We want to show that $|\mathbb{X}_{\vec{x}=\vec{v}}|=|\mathbb{X}_{\vec{y}=\vec{v}}|$. It is clear that it is sufficient to look at $\mathbb{X}_{3}$ as defined above. But because $\theta$ says that $d$ is a “detector” of whether $\vec{z}=\vec{x}$ or not, it is in fact sufficient to check $\vec{x}\approx\vec{y}$ for the subteam $\mathbb{X}_{4}$ (also as defined above). But in $\mathbb{X}_{4}$, this follows from $\phi$.∎

Appendix 0.C Proof of Theorem 3

Theorem 3 follows from Lemma 3 presented below. Lemma 3 can be proven following the proof of Theorem 2 in [9]. We omit the details and instead delineate intuition behind the translation. The idea is to simulate the semantics of the probabilistic conditional independence atom using only marginal independence and marginal identity atoms. First, the universally quantified $\vec{y}$ in the translation represents all possible variable assignments $s$ of $\vec{x}$. Second, $\psi_{0}$ and $\psi_{1}$ indicate that the marginal distributions of $\vec{x}_{0}$, $\vec{x}_{0}\vec{x}_{1}$, $\vec{x}_{0}\vec{x}_{2}$, and $\vec{x}_{0}\vec{x}_{1}\vec{x}_{2}$ are distributed respectively to $\vec{z}_{0},\vec{z}_{1},\vec{z}_{2},\vec{z}_{3}$ independently of $\vec{y}$ and of each other. Third, $\psi_{2}$ encodes the product of the weights of $s(\vec{x}_{0})$ and $s(\vec{x}_{0}\vec{x}_{1}\vec{x}_{2})$ by $\alpha=0$, and $\psi_{3}$ similarly the product of the weights of $s(\vec{x}_{0}\vec{x}_{1})$ and $s(\vec{x}_{0}\vec{x}_{2})$ by $\beta=0$. Finally, conditional independence between $\vec{x}_{1}$ and $\vec{x}_{2}$ given $\vec{x}_{0}$ follows iff these products are equal relative to all assignments of $\vec{y}$. Theorem 3 then follows from this lemma since the constant [math] and the marginal identity atom are both definable in ${\rm FO}(\perp\!\!\!\perp)$.

Lemma 3

Let $\vec{x}_{0},\vec{x}_{1},\vec{x}_{2}$ be three sequences of variables from $\vec{x}=(x_{1},\ldots,x_{n})$, and let [math] be a constant symbol. Then $\vec{x}_{1}~{}\!\!\perp\!\!\!\perp_{\vec{x}_{0}}\!\!~{}\vec{x}_{2}$ is equivalent to

[TABLE]

where

[TABLE]

Appendix 0.D Proof of Proposition 4.2

Proposition LABEL:prop:ucl

Proof

We may assume that $\mathbb{X}=(X,f)$ and $\mathbb{Y}=(X,g)$. We prove the claim by structural induction on $\phi$. We omit the cases for atomic formulae and conjunction which are straightforward.

• •

Assume that $\phi=\phi_{0}\vee\phi_{1}$. By the semantics of the disjunction, we find $p,q\in[0,1]$ and distributions $f_{0},f_{1},g_{0},g_{1}$ over $X$ such that $\mathfrak{A}\models_{(X,f_{0})}\phi_{0}$, $\mathfrak{A}\models_{(X,f_{1})}\phi_{1}$, $\mathfrak{A}\models_{(X,g_{0})}\phi_{0}$, $\mathfrak{A}\models_{(X,g_{1})}\phi_{1}$, $f=pf_{0}+(1-p)f_{1}$, and $g=qg_{0}+(1-q)g_{1}$. Define $h_{0}:=\frac{kpf_{0}+(1-k)qg_{0}}{kp+(1-k)q}$ and $h_{1}:=\frac{k(1-p)f_{1}+(1-k)(1-q)g_{1}}{k(1-p)+(1-k)(1-q)}$. By the induction hypothesis $\mathfrak{A}\models_{(X,h_{0})}\phi_{0}$ and $\mathfrak{A}\models_{(X,h_{1})}\phi_{1}$, since $(X,h_{0})=(X,f_{0})\sqcup_{a}(X,g_{0})$ for $a:=\frac{kp}{kp+(1-k)q}$, and $(X,h_{1})=(X,f_{1})\sqcup_{b}(X,g_{1})$ for $b:=\frac{k(1-p)}{k(1-p)+(1-k)(1-q)}$. Then $(X,f)\sqcup_{k}(X,g)=(X,h_{0})\sqcup_{c}(X,h_{1})$ for $c:=kp+(1-k)q$ because

[TABLE]

Consequently, $\mathfrak{A}\models_{(X,f)\sqcup_{k}(X,g)}\phi_{0}\vee\phi_{1}$ follows from the semantics of the disjuction which completes the disjunction step of the induction.

• •

Assume that $\phi=\forall x\psi$. Then $\mathfrak{A}\models_{\mathbb{X}[A/x]}\psi$ and $\mathfrak{A}\models_{\mathbb{Y}[A/x]}\psi$, and by induction assumption $\mathfrak{A}\models_{\mathbb{X}[A/x]\sqcup_{k}\mathbb{Y}[A/x]}\psi$. The claim then follows since $\mathbb{X}[A/x]\sqcup_{k}\mathbb{Y}[A/x]=(\mathbb{X}\sqcup_{k}\mathbb{Y})[A/x]$.

• •

Assume that $\phi=\exists x\psi$. Then $\mathfrak{A}\models_{\mathbb{X}[F/x]}\psi$ and $\mathfrak{A}\models_{\mathbb{Y}[G/x]}\psi$ where $F$ and $G$ are functions that map each $s\in X$ to a probability distribution $F_{s}$ over $A=\operatorname{Dom}(\mathfrak{A})$. We let $H$ be a function that maps $s\in X$ to a probability distribution $H_{s}$ over $A$ such that

[TABLE]

Note that $\sum_{a\in A}H_{s}(a)=1$ follows from $\sum_{a\in A}F_{s}(a)=\sum_{a\in A}G_{s}(a)=1$. By induction assumption $\mathfrak{A}\models_{\mathbb{X}[F/x]\sqcup_{k}\mathbb{Y}[F/x]}\psi$. The claim now follows from $\mathbb{X}[F/x]\sqcup_{k}\mathbb{Y}[F/x]=(\mathbb{X}\sqcup_{k}\mathbb{Y})[H/x]$, which holds since for all $a\in A$:

[TABLE]

This concludes the case of existential quantification and the proof.∎