# Propositional Team Logics111Some results in this paper were included in the
dissertation of the first author [32], which was supervised by the second
author.

Fan Yang22footnotemark: 2 Department of Values, Technology and Innovation,
Delft University of Technology, Jaffalaan 5, 2628 BX Delft, The Netherlands
<EMAIL_ADDRESS>Jouko Väänänen333The research was partially supported by
grant 251557 of the Academy of Finland<EMAIL_ADDRESS>Department
of Mathematics and Statistics, Gustaf Hällströmin katu 2b, PL 68, FIN-00014
University of Helsinki, Finland and University of Amsterdam, The Netherlands

###### Abstract

We consider team semantics for propositional logic, continuing [34]. In team
semantics the truth of a propositional formula is considered in a set of
valuations, called a team, rather than in an individual valuation. This offers
the possibility to give meaning to concepts such as dependence, independence
and inclusion. We associate with every formula $\phi$ based on finitely many
propositional variables the set $\llbracket\phi\rrbracket$ of teams that
satisfy $\phi$. We define a full propositional team logic in which every set
of teams is definable as $\llbracket\phi\rrbracket$ for suitable $\phi$. This
requires going beyond the logical operations of classical propositional logic.
We exhibit a hierarchy of logics between the smallest, viz. classical
propositional logic, and the full propositional team logic. We characterize
these different logics in several ways: first syntactically by their logical
operations, and then semantically by the kind of sets of teams they are
capable of defining. In several important cases we are able to find complete
axiomatizations for these logics.

###### keywords:

propositional team logics , team semantics , dependence logic , non-classical
logic

###### MSC:

[2010] 03B60

††journal: arXiv.org

$\mathsf{TIME}$ $\mathsf{NTIME}$ $\mathsf{ATIME}$ $\mathsf{SPACE}$
$\mathsf{NSPACE}$ $\mathsf{ASPACE}$

fnfnfootnotetext: This paper is partially based on research that was carried
out in the Graduate School of Mathematics and Statistics of the University of
Helsinki.

##  1 Introduction

In classical propositional logic the propositional atoms, say
$p_{1},\ldots,p_{n}$, are given a truth value $1$ or $0$ by what is called a
valuation and then any propositional formula $\phi$ can be associated with the
set $|\phi|$ of valuations giving $\phi$ the value $1$. This constitutes a
perfect analysis of the circumstances under which $\phi$ is true. The formula
$\phi$ can be presented in so-called Disjunctive Normal Form based on taking
the disjunction of descriptions of the valuations in $|\phi|$. Two fundamental
results can be proved for classical propositional logic. The first says that
every set of valuations of $p_{1},\ldots,p_{n}$ is equal to $|\phi|$ for some
propositional formula $\phi$. The second fundamental result says that there is
a simple complete axiomatization of those $\phi$ that are valid in the sense
that $|\phi|$ is the full set of all valuations on the propositional atoms
occurring in $\phi$.

In this paper, which continues [34], we consider a richer semantics called
team semantics for propositional logic. In team semantics the truth of a
propositional formula is evaluated in a set of valuations, called a team,
rather than in an individual valuation. This offers the possibility of
considering probabilities of formulas, as in [19], and the meaning of concepts
such as dependence, independence and inclusion, as in [34]. It is the latter
possibility that is our focus in this paper.

Team semantics was introduced by the second author in [27] on the basis of a
new compositional semantics, due to Hodges [17, 18], for independence friendly
logic [16, 25]. The monograph [27] was written in the context of predicate
logic and team semantics was used to give meaning to a variable being totally
determined by a sequence of other variables. In the context of propositional
and modal logic team semantics was introduced in [28]. In propositional logic
team semantics can be used to give meaning to a propositional variable being
totally determined by a sequence of other variables. It took a few years
before this idea was fully exploited in [31, 32]. Meanwhile modal dependence
logic, i.e. team semantics for modal logic, was investigated e.g. in [26, 8,
7, 23, 9, 14, 15].

When propositional formulas are evaluated in a team—i.e. a set—of valuations,
a whole new landscape opens in front of us. The first observation is a
numerical explosion: If we have $n$ propositional atoms, there are $2^{n}$
valuations, $2^{2^{n}}$ teams, and $2^{2^{2^{n}}}$ sets of teams. For $n=3$
the third number is about $10^{77}$. This emphasises the need for mathematical
methods in team semantics. The truth table methods which list all
possibilities is bad enough in ordinary propositional logic, but totally
untenable in team semantics.

In classical propositional logic, we associate with every formula $\phi$ based
on propositional atoms $p_{1},\ldots,p_{n}$ the set $|\phi|$ of valuations
that satisfy $\phi$. Similarly, in team semantics we associate with every
formula $\phi$ based on propositional atoms $p_{1},\ldots,p_{n}$ the set
$\llbracket\phi\rrbracket$ of teams that satisfy (in the sense defined below)
$\phi$. By choosing our formulas carefully we can express every set of teams
in the form $\llbracket\phi\rrbracket$ for suitable $\phi$, but this requires
going beyond the logical operations of classical propositional logic. We can
also axiomatize the propositional formulas that are valid i.e. satisfied by
every team.

The rich structure of teams gives rise to a plethora of new propositional
connectives. Most importantly, disjunction has several versions. To define
when a team $X$ satisfies $\phi\vee\psi$ we can say that this happens if $X$
satisfies $\phi$ or it satisfies $\psi$, or we can say that this happens if
$X$ is the union of two sets $Y$ and $Z$ such that $Y$ satisfies $\phi$ and
$Z$ satisfies $\psi$, or, finally, we can also say that this happens if,
assuming $X\neq\emptyset$, the team $X$ is the union of two sets
$Y\neq\emptyset$ and $Z\neq\emptyset$ such that $Y$ satisfies $\phi$ and $Z$
satisfies $\psi$. If $X$ is a singleton, which corresponds to the classical
case, the first two disjunctions are equivalent, but the third is equivalent
to $\phi\wedge\psi$. But for non-singleton teams there is a big difference in
every respect. These distinctions, leading to different variants of familiar
logical operations, reveal a hierarchy of logics between the smallest, viz.
classical propositional logic, and the maximal one capable of defining every
set of teams. We characterize these different logics in several ways: first
syntactically by their logical operations, and then semantically by the kind
of sets of teams they are capable of defining. In several important cases we
are able to find complete axiomatizations for these logic.

In our previous paper [34] we considered sets of teams that are downward
closed in the sense that if a team is in the set, then every subteam is in the
set, too. Respectively, the logics studied in [34] have the property that the
sets of teams defined by their formulas are downward closed. We isolated five
equivalent logics with this property, all based on some aspect of dependence.
In these logics every downward closed set of teams is definable, and the
logics have complete axiomatizations. The axiomatizations are by no means as
simple as typical axiomatizations of classical propositional logic, but have
still a certain degree of naturality.

In this paper we consider sets of teams, and related propositional logics,
that are not downward closed. A property in a sense opposite to downward
closure is closure under (set-theoretical) unions. In fact, a set of teams
that is both closed downward and closed under unions is definable in classical
propositional logic. So-called inclusion logic, to be defined below, is an
example of a logic in which definable sets of teams are closed under unions.
So-called independence logic, also to be defined below, is neither downward
closed nor closed under unions. Our methods do not seem to apply to
independence logic, we can merely approximate it from below and from above
with logics that we understand better.

We do not rule out the possibility that a team is empty. Accordingly we
distinguish whether a set of teams contains the empty team as an element or
not. The basic dependence, independence and inclusion logics have the Empty
Team Property i.e. every definable set of teams contains the empty team.
However, many of our proofs depend on the ability to express the non-emptiness
of a team. For this purpose we also consider a special atomic formula
$\mathop{\mbox{\small\rm NE}}$ the only role of which is to say that the team
is nonempty. This so-called non-emptiness $\mathop{\mbox{\small\rm NE}}$ was
introduced in [32] and in [29]. We give examples which suggest that
$\mathop{\mbox{\small\rm NE}}$ is not completely alien to common usage of
language although it seems hopelessly abstract. The introduction of
$\mathop{\mbox{\small\rm NE}}$ leads to two versions of each of our
propositional logics: one without $\mathop{\mbox{\small\rm NE}}$ and one with
$\mathop{\mbox{\small\rm NE}}$.

This paper is structured as follows. In Section 2 we define the basic concepts
and make some preliminary observations. We also define the propositional team
logics we study in the paper, including _propositional dependence logic_ ,
_propositional independence logic_ , _propositional union closed logic_ ,
_propositional inclusion logic_ and _propositional team logic_ as well as the
strong version of each. In Section 3 we establish basic normal forms and use
them to obtain semantic characterizations of our logics, whether strong or
not. In Section 4 we prove some metalogical properties of our logics,
including compactness and the closure under classical substitutions of the
logics. In Section 5 we establish complete axiomatizations of the strong
versions of our logics. Several open problems are listed in the concluding
Section 6.

##  2 Preliminaries

Our propositional team logic follows the pattern set forth on first-order
level by dependence logic [27], independence logic [13], as well as inclusion
and exclusion logics [10]. The concepts of dependence and independence were
earlier introduced in database theory, starting with [6]. However, in database
theory the focus is on dependence and independence of attributes per se, while
we take the dependence and independence as atomic formulas and use logical
operations to build complex formulas. The benefit of considering complex
formulas is that we can express very involved types of dependence and
independence. A good example is the fact that first-order inclusion logic can
express in finite models exactly all dependencies expressible in fixed point
logic [11].

We follow here the reasoning of Wilfrid Hodges [17, 18] to the effect that a
set of valuations, rather than a single valuation, permits the delineation of
dependence and independence. We call such sets teams. Let us now give the
formal definition of a team.

######  Definition 2.1.

Throughout the paper we fix an infinite set ${\rm Prop}=\\{p_{i}\mid
i\in\mathbb{N}\\}$ of propositional variables. We sometimes use
$\vec{x},\vec{y},\vec{z},\dots$ to denote arbitrary sequences of propositional
variables. A _valuation_ $s$ on a set $N$ of indices (i.e. a set of natural
numbers) is a function from $N$ to the set $2=\\{0,1\\}$. A _team_ $X$ on $N$
is a set of valuations on $N$. A _team_ $X$ on the set $\mathbb{N}$ of all
natural numbers is called a _team_. If $X$ is a team on $N$ and
$N^{\prime}\subseteq N$, then we write $X\upharpoonright N^{\prime}$ for the
set $\\{s\upharpoonright N^{\prime}\mid s\in X\\}$.

Table 1 shows an example of a team $X$ consisting of six valuations. One
possibility is to view a team as an information state as is done in
inquisitive logic [5]. The idea is that there is one “true” valuation $v$ and
the valuations in the team are approximations of it as far as we know. The
bigger the team the bigger is our uncertainty about $v$. On the other hand, if
the team is as small as a singleton $\\{v\\}$, we know the valuation, and
there is no uncertainty. This is just one intuition behind the team concept. A
different intuition is that the valuations in a team arise from scientific
observations. They may arise also from the organizational structure of a large
company, etc.

We call propositional logics that have semantics based on teams _propositional
team logics_. As the first step, let us examine the usual classical
propositional logic in the setting of team semantics.

######  Definition 2.2.

Well-formed formulas of _classical propositional logic_ ($\mathbf{CPL}$) are
given by the following grammar

$\phi::=\,p_{i}\mid\neg
p_{i}\mid\bot\mid(\phi\wedge\phi)\mid(\phi\otimes\phi).$

Here we use the symbol $\otimes$ to denote the disjunction of $\mathbf{CPL}$.
A well-formed formula of $\mathbf{CPL}$ is said to be a _formula in the
language of $\mathbf{CPL}$_ or a _classical formula_.

| $p_{0}$ | $p_{1}$ | $p_{2}$ | $p_{3}$ | $\dots$
---|---|---|---|---|---
$s_{1}$ | 1 | 1 | 1 | 1 |
$s_{2}$ | 1 | 0 | 0 | 0 |
$s_{3}$ | 0 | 1 | 1 | 1 |
$s_{4}$ | 0 | 0 | 0 | 0 | $\dots$
$s_{5}$ | 1 | 1 | 0 | 0 |
$s_{6}$ | 0 | 1 | 0 | 1 |
Table 1: A team $X=\\{s_{1},\dots,s_{6}\\}$

######  Definition 2.3.

We define inductively the notion of a classical formula $\phi$ being _true_ on
a team $X$, denoted by $X\models\phi$, as follows:

  * 1.

$X\models p_{i}$ iff for all $s\in X$, $s(i)=1$

  * 2.

$X\models\neg p_{i}$ iff for all $s\in X$, $s(i)=0$

  * 3.

$X\models\bot$ iff $X=\emptyset$

  * 4.

$X\models\phi\wedge\psi$ iff $X\models\phi$ and $X\models\psi$

  * 5.

$X\models\phi\otimes\psi$ iff there exist two subteams $Y,Z\subseteq X$ with
$X=Y\cup Z$ such that $Y\models\phi\text{ and }Z\models\psi$

We write $\phi(p_{i_{1}},\dots,p_{i_{n}})$ if the propositional variables
occurring in the formula $\phi$ are among $p_{i_{1}},\dots,p_{i_{n}}$. The
following lemma summarizes the main properties of classical formulas. The
reader is referred to [34] for details on other properties of the team
semantics of classical formulas.

######  Lemma 2.4.

Classical formulas have the _Locality Property_ , the _Flatness Property_ ,
the _Downward Closure Property_ , the _Union Closure Property_ , and the
_Empty Team Property_ defined as follows.

(Locality Property)

Let $X$ and $Y$ be two teams, and $\phi(p_{i_{1}},\dots,p_{i_{n}})$ a formula.
If
$X\upharpoonright\\{{i_{1}},\dots,{i_{n}}\\}=Y\upharpoonright\\{{i_{1}},\dots,{i_{n}}\\}$,
then $X\models\phi\iff Y\models\phi.$

(Flateness Property)

$X\models\phi\iff\forall s\in X(\\{s\\}\models\phi)$

(Downward Closure Property)

If $X\models\phi$ and $Y\subseteq X$, then $Y\models\phi$

(Union Closure Property)

If $X\models\phi$ for all $X\in\mathcal{X}$, then
$\bigcup\mathcal{X}\models\phi$

(Empty Team Property)

$\emptyset\models\phi$ always holds

Under the usual single valuation semantics a classical formula
$\phi(p_{i_{1}},\dots,p_{i_{n}})$ defines a set $|\phi|=\\{s\in
2^{N}:s\models\phi\\}$ of valuations (a team!) on
$N=\\{{i_{1}},\dots,{i_{n}}\\}$; the same formula under the team semantics
defines a set

$\llbracket\phi\rrbracket:=\\{X\subseteq 2^{N}\mid X\models\phi\\}$

of teams on $N$. It is well-know that $\mathbf{CPL}$ is _expressively
complete_ under the usual single valuation semantics in the sense that every
property $X\subseteq 2^{N}$ is definable by a classical formula $\phi$, i.e.,
$X=|\phi|$. We now define a similar notion of _expressive completeness_ for a
set of team properties under the team semantics.

######  Definition 2.5.

Let $\mathbb{P}$ be a set of team properties i.e. a set of sets of teams. We
let $\mathbb{P}_{N}=\\{\mathsf{P}\upharpoonright
N:\mathsf{P}\in\mathbb{P}\\}$, where each $\mathsf{P}\upharpoonright
N=\\{X\upharpoonright N:X\in\mathsf{P}\\}$ is a team property on a finite set
$N$ of indices. We say that a propositional team logic $\mathsf{L}$
_characterizes_ $\mathbb{P}$, if for each index set
$N=\\{i_{1},\dots,i_{n}\\}$,

$\mathbb{P}_{N}=\\{\llbracket\phi\rrbracket:~{}\phi(p_{i_{1}},\dots,p_{i_{n}})\text{
is a formula in the language of $\mathsf{L}$}\\}.$

If a logic characterizes a set $\mathbb{P}$ of team properties, then we also
say that the logic is _expressively complete_ for $\mathbb{P}$.

Below we define some interesting team properties, already inherent in Lemma
2.4:

######  Definition 2.6.

A team property $\mathsf{P}$, i.e., a set of teams, is called

  * 1.

_flat_ if $X\in\mathsf{P}\iff\forall s\in X(\\{s\\}\in\mathsf{P})$;

  * 2.

_downward closed_ if $Y\subseteq X\in\mathsf{P}\Longrightarrow
Y\in\mathsf{P}$;

  * 3.

_union closed_ if
$\mathcal{X}\subseteq\mathsf{P}\Longrightarrow\bigcup\mathcal{X}\in\mathsf{P}$.

It follows from our previous paper [34] that several propositional logics of
dependence ($\mathbf{PD}$) (including propositional dependence logic and
inquisitive logic) are expressively complete for the set of all nonempty
downward closed team properties. In this paper we will study logics that are
expressively complete for each of the team properties defined above. In
particular, we will prove that $\mathbf{CPL}$ is expressively complete for the
set of flat team properties and it is the biggest propositional team logic
that defines both all downward closed team properties and all union closed
team properties (Theorem 3.1).

The empty team is a member of any flat team property and of any nonempty
downward closed team property. The familiar classical formulas and formulas in
the language of $\mathbf{PD}$ that we studied in our previous paper [34] all
have the empty team property. To define team properties that do not contain
the empty team, we introduce a new atom $\mathop{\mbox{\small\rm NE}}$, called
_non-emptiness_ , stating that the team in question is nonempty. To define
also other interesting team properties, we now enrich the language of our
logic.

######  Definition 2.7.

Well-formed formulas of the _full propositional team logic_ ($\mathbf{FPT}$)
are given by the following grammar

$\begin{split}\phi::=&\,p_{i}\mid\neg p_{i}\mid\mathop{\mbox{\small\rm
NE}}\mid\bot\mid p_{i_{1}}\dots p_{i_{k}}\perp p_{j_{1}}\dots
p_{j_{m}}\mid\mathop{=\\!}(p_{i_{1}},\dots,p_{i_{k}},p_{j})\\\ &\mid
p_{i_{1}},\dots,p_{i_{k}}\subseteq p_{j_{1}}\dots
p_{j_{m}}\mid(\phi\wedge\phi)\mid(\phi\otimes\phi)\mid(\phi\varoast\phi)\mid(\phi\vee\phi)\end{split}$

The formulas $p_{i_{1}}\dots p_{i_{k}}\perp p_{j_{1}}\dots p_{j_{m}}$,
$\mathop{=\\!}(p_{i_{1}},\dots,p_{i_{k}},p_{j})$ and
$p_{i_{1}},\dots,p_{i_{k}}\subseteq p_{j_{1}}\dots p_{j_{m}}$ are called the
_independence atom_ , the _dependence atom_ and the _inclusion atom_ ,
respectively. The connectives $\otimes$, $\varoast$ and $\vee$ are called the
_tensor (disjunction)_ , the _nonempty disjunction_ and the _Boolean
disjunction_ , respectively.

######  Definition 2.8.

We define inductively the notion of a formula $\phi$ in the language of
$\mathbf{FPT}$ being _true_ on a team $X$, denoted by $X\models\phi$. All the
cases are identical to those defined in Definition 2.3 and additionally:

  * 1.

$X\models\mathop{\mbox{\small\rm NE}}$ iff $X\neq\emptyset$

  * 2.

$X\models\,p_{i_{1}}\dots p_{i_{k}}\perp p_{j_{1}}\dots p_{j_{m}}$ iff for all
$s,s^{\prime}\in X$, there exists $s^{\prime\prime}\in X$ such that

$\langle s^{\prime\prime}(i_{1}),\dots,s^{\prime\prime}(i_{k})\rangle=\langle
s(i_{1}),\dots,s(i_{k})\rangle$

and

$\langle s^{\prime\prime}(j_{1}),\dots,s^{\prime\prime}(j_{m})\rangle=\langle
s^{\prime}(j_{1}),\dots,s^{\prime}(j_{m})\rangle$

  * 3.

$X\models\mathop{=\\!}(p_{i_{1}}\dots p_{i_{k}},p_{j})$ iff for all
$s,s^{\prime}\in X$,

$\text{if }\langle s(i_{1}),\dots,s(i_{k})\rangle=\langle
s^{\prime}(i_{1}),\dots,s^{\prime}(i_{k})\rangle,\text{ then
}s(j)=s^{\prime}(j)$

  * 4.

$X\models p_{i_{1}}\dots p_{i_{k}}\subseteq p_{j_{1}}\dots p_{j_{k}}$ iff for
all $s\in X$, there exists $s^{\prime}\in X$ such that

$\langle s(i_{1}),\dots,s(i_{k})\rangle=\langle
s^{\prime}(j_{1}),\dots,s^{\prime}(j_{k})$

  * 5.

$X\models\phi\varoast\psi$ iff $X=\emptyset$ or there are nonempty $Y$ and $Z$
such that $X=Y\cup Z$, $Y\models\phi$ and $Z\models\psi$

  * 6.

$X\models\phi\vee\psi$ iff $X\models\phi$ or $X\models\psi$

We say that a formula $\phi$ is _valid_ , denoted by $\models\phi$, if
$X\models\phi$ holds for all teams $X$. We say that a formula $\psi$ is a
_logical consequence_ of a set $\Gamma$ of formulas, written
$\Gamma\models\psi$, if for any team $X$ such that $X\models\phi$ for all
$\phi\in\Gamma$, we have $X\models\psi$. We also write $\phi\models\psi$ for
$\\{\phi\\}\models\psi$. If $\phi\models\psi$ and $\psi\models\phi$, then we
say that $\phi$ and $\psi$ are _semantically equivalent_ , in symbols
$\phi\equiv\psi$.

Let $\mathsf{L}_{1}$ and $\mathsf{L}_{2}$ be two propositional team logics. We
write $\mathsf{L}_{1}\leq\mathsf{L}_{2}$ if every formula of $\mathsf{L}_{1}$
is semantically equivalent to a formula of $\mathsf{L}_{2}$. If
$\mathsf{L}_{1}\leq\mathsf{L}_{2}$ and $\mathsf{L}_{2}\leq\mathsf{L}_{1}$,
then we write $\mathsf{L}_{1}\equiv\mathsf{L}_{2}$ and say that
$\mathsf{L}_{1}$ and $\mathsf{L}_{2}$ have the _same expressive power_.

Let us now spend a few moments with the atoms and connectives of
$\mathbf{FPT}$.

### Independence atom

Let us first take a closer look at the independence atoms by considering the
team $X$ of Table 1. It can be verified that the independence atom $p_{0}\perp
p_{3}$ is satisfied by $X$. One may think of the team $X$ as given data about
$p_{0},p_{1},p_{2},p_{3},\dots$. For example, $p_{0},p_{1},p_{2}$ may be
propositional variables which tell whether some valves $V_{0},V_{1},V_{2}$
controlling gas flow in an industrial process are open (1) or closed (0), and
$p_{3}$ is a propositional variable indicating whether a warning lamp is on
(1) or off (0). We can conclude on the basis of the team of Table 1 that the
lamp is independent of the valve $V_{0}$. However, the lamp is not completely
independent of $V_{1}$, because if $V_{1}$ is closed, the lamp is definitely
off. Also, the lamp is not entirely independent of the valve $V_{2}$, because
if $V_{2}$ is closed, the lamp is again definitely off.

One way to describe the truth definition of $X\models p_{i_{1}}\dots
p_{i_{k}}\perp p_{j_{1}}\dots p_{j_{m}}$ is to compare it to Cartesian
product: $X\models\\{p_{i}:i\in I\\}\perp\\{p_{j}:j\in J\\}$ if and only if

$X\upharpoonright I\cup J=(X\upharpoonright I)\times(X\upharpoonright J).$

This manifests the similarity between our concept of independence and the
concept of independence of random variables in statistics.

The implication problem of independence atoms (i.e., the problem of asking
whether an independence atom follows from a set of independence atoms) can be
completely axiomatized by the axioms below, known in database theory as the
Geiger-Paz-Pearl axioms ([12]):

(i)

If $\vec{x}\perp\vec{y}$, then $\vec{y}\perp\vec{x}$.

(ii)

If $\vec{x}\perp\vec{y}$, then $\vec{z}\perp\vec{y}$, where $\vec{z}$ is a
subsequence of $\vec{x}$.

(iii)

If $\vec{x}\perp\vec{y}$, then $\vec{u}\perp\vec{v}$, where $\vec{u}$ and
$\vec{v}$ are permutations of $\vec{x}$ and $\vec{y}$, respectively.

(iv)

If $\vec{x}\perp\vec{y}$ and $\vec{x}\vec{y}\perp\vec{z}$, then
$\vec{x}\perp\vec{y}\vec{z}$.

While the downward closure property has a profound influence on properties of
dependence logic as already mentioned, the independence atoms violate this
property. For example, in Table 1 in the team $X$ the attributes $p_{0}$ and
$p_{3}$ are independent but in the subteam $Y=\\{s_{1},s_{2},s_{3}\\}$ they
are not. We will see in the sequel that propositional independence logic and
other propositional team logics have a completely different flavor than
propositional logics of dependence.

### Non-emptiness atom

Another formula that violates the downward closure property is the very simple
atom $\mathop{\mbox{\small\rm NE}}$ that we call nonemptieness which states
that the team is nonempty. An easy inductive proof shows that the
$\mathop{\mbox{\small\rm NE}}$-free fragment of $\mathbf{FPT}$ has the empty
team property. But often when describing properties of teams, we do want to
distinguish between the empty team and the nonempty teams. The atom
$\mathop{\mbox{\small\rm NE}}$ is introduced exactly for this purpose.

The symbol $\mathop{\mbox{\small\rm NE}}$ is a logical symbol, on a par with
$\bot$, with no internal structure and no proposition symbols occurring in it.
While $\bot$ is generally conceived of as a symbol of contradiction, one may
ask what is the intuitive meaning of $\mathop{\mbox{\small\rm NE}}$? Does this
symbol occur in natural language or in scientific discourse? Let us think of a
natural language sentence that has the modality “might”:

I _might_ come to the party.

Given a nonempty information state (i.e. a team) $X$, this sentence can be
characterized as “there exists a nonempty substate $Y$ in which I indeed come
to the party”. This “might” modality (denoted by $\triangledown$) was
considered by Hella and Stumpf in [15] and its team semantics is given by the
clause

  * 1.

$X\models\triangledown\phi$ iff $X=\emptyset$ or there exists a nonempty team
$Y\subseteq X$ such that $Y\models\phi$

The “might” modality can be expressed in terms of the more basic notion of
non-emptiness of a team:

$\triangledown\phi\equiv\bot\vee\big{(}(\phi\wedge\mathop{\mbox{\small\rm
NE}})\otimes\top\big{)}.$

### Contradictions and linear implication

In the presence of the non-emptiness $\mathop{\mbox{\small\rm NE}}$
_contradiction_ has two variants: the _weak contradiction_ $\bot$ that is
satisfied only by the empty team and the _strong contradiction_
$\bot\wedge\mathop{\mbox{\small\rm NE}}$ that is satisfied by no team at all.

A related logical constant is the _linear implication_ $\multimap$ (introduced
by Abramsky and Väänänen [1]) that has the semantics

  * 1.

$X\models\phi\multimap\psi$ iff for any team $Y$, if $Y\models\phi$, then
$X\cup Y\models\psi$

The strong contradiction is easily definable using the linear implication:

$\bot\wedge\mathop{\mbox{\small\rm NE}}\equiv\top\multimap\bot,$

where $\top=p_{i_{1}}\otimes\neg p_{i_{1}}$. The reader is referred to [1] for
details on linear implication. We only remark that in the presence of the
downward closure property, we have

$\phi\models\psi\iff\emptyset\models\phi\multimap\psi.$

In other words, deciding whether $\psi$ is a logical consequence of $\phi$ is
reduced to deciding whether the linear implication $\phi\multimap\psi$ is
satisfied by the empty team.

### Disjunctions

Due to the way we define semantics there are more propositional operations
than in the case of classical propositional logic. In particular, disjunction
has three different incarnations, namely $\otimes$, $\varoast$ and $\vee$.
These different forms arise from the difference between considering individual
valuations and sets of valuations.

The tensor disjunction $\otimes$ generalizes the disjunction of classical
propositional logic. The semantics of $\otimes$ and other connectives as
defined in Definitions 2.3 and 2.8 is known in the literature (see e.g.,[10])
as the _Lax Semantics_ (in contrast to the _Strict Semantics_). An easy
inductive proof shows that our logic $\mathbf{FPT}$ has the locality property.
By contrast, if we replace the clause for tensor disjunction $\otimes$ in
Definition 2.3 by the corresponding clause under strict semantics (denoted by
$\models^{s}$)

  * 1.

$X\models^{s}\phi\otimes\psi$ iff there exist two _disjoint_ subteams
$Y,Z\subseteq X$ with $X=Y\cup Z$ such that $Y\models^{s}\phi\text{ and
}Z\models^{s}\psi$

the logic does not any more satisfy the local property. This is because, for
instance, for the two valuations $s_{0}$ and $s_{1}$ defined in Table 1, we
have $\\{s_{0},s_{1}\\}\models^{s}(\mathop{\mbox{\small\rm NE}}\wedge
p_{0})\otimes(\mathop{\mbox{\small\rm NE}}\wedge p_{0})$ while
$\\{s_{0}\\}\not\models^{s}(\mathop{\mbox{\small\rm NE}}\wedge
p_{0})\otimes(\mathop{\mbox{\small\rm NE}}\wedge p_{0})$, even though
$\\{s_{0}\upharpoonright\\{0\\},s_{1}\upharpoonright\\{0\\}\\}=\\{(0,1)\\}=\\{s_{0}\upharpoonright\\{0\\}\\}$.
We refer the reader to [10] for further discussions on the difference between
lax and strict semantics.

The nonempty disjunction $\phi\varoast\psi$ was introduced by Raine Rönnholm
(personal communication). One can easily verify that $\varoast$ can be defined
in terms of the other disjunctions and the non-emptiness:

$\phi\varoast\psi\equiv\bot\vee\big{(}(\phi\wedge\mathop{\mbox{\small\rm
NE}})\otimes(\psi\wedge\mathop{\mbox{\small\rm NE}})\big{)}.$

Moreover, it was observed in [15] that in any fragment of $\mathbf{FPT}$ that
has the empty team property the might modality $\triangledown$ and the
nonempty disjunction $\varoast$ as inter-definable:

$\triangledown\phi\equiv\phi\varoast\top\quad\text{ and
}\quad\phi\varoast\psi\equiv(\phi\otimes\psi)\wedge(\triangledown\phi\otimes\triangledown\psi)$
(1)

To understand the meaning of $\varoast$ in natural language, let us think of
the sentence (in the context of chess):

Rook or queen was sacrificed in each play. (2)

It is clear what it means to say that a nonempty set $X$ of plays satisfies
this, and in each play in $X$ either rook or queen was sacrificed. There is a
slight difference in saying

Rook or queen was sacrificed and both cases occurred in some plays. (3)

In our symbolic language, denoting “Rook was sacrificed” by $\phi$ and “queen
was sacrificed” by $\psi$, (2) would be written

$X\models\mbox{$\phi$ $\otimes$ $\psi$}$

while (3) would be written

$X\models\mbox{($\phi\wedge\mathop{\mbox{\small\rm NE}}$) $\otimes$
($\psi\wedge\mathop{\mbox{\small\rm NE}}$)}\text{ or
}X\models\phi\varoast\psi.$

In a sense, $\phi\varoast\psi$ is an “honest” disjunction: if the team has
anything in it at all, then it is divided between $\phi$ and $\psi$ in the
non-trivial way that both get a nonempty subteam. We can think that whoever
says (3), means that if some plays were actually played, then in some of them
a Rook was sacrificed and in some the Queen. To put it in a more general
context, the formula $\phi\varoast\psi$ permits a type of “free choice” by
having each disjunct nonvoid. This way the nonempty disjunction
$\phi\varoast\psi$ provides more information than the tensor disjunction
$\phi\otimes\psi$. In particular, uttering a disjunction with a void disjunct
is actually less informative than simply stating one of the disjuncts.

The Boolean disjunction $\vee$ was called _intuitionistic disjunction_ in our
previous paper [34] in the context of propositional logics of dependence. In
particular, in the presence of the downward closure property the
intuitionistic disjunction has the _disjunction property_ :

$\models\phi\vee\psi\text{ implies }\models\phi\text{ or }\models\psi.$

However, in the absence of the downward closure, this property, reminiscent of
constructive logic, for $\vee$ fails, since, e.g.,
$\models\bot\vee\mathop{\mbox{\small\rm NE}}$ and $\models(p\varoast\neg
p)\vee(p\vee\neg p)$, whereas $\not\models\bot$,
$\not\models\mathop{\mbox{\small\rm NE}}$, $\not\models p\varoast\neg p$ and
$\not\models p\vee\neg p$.

We define the empty disjunction for all three disjunctions as

$\operatorname*{\bigotimes}\emptyset:=\bot,~{}\mathop{\raisebox{-1.9pt}{$\huge\text{$\varoast$}$}}\emptyset:=\bot\text{
and }\operatorname*{\bigvee}\emptyset:=\bot\wedge\mathop{\mbox{\small\rm
NE}}.$

Table 2: Propositional team logics Logic | Atoms | Connectives
---|---|---
Classical propositional logic ($\mathbf{CPL}$) | $p_{i},\neg p_{i},\bot$ | $\wedge,\otimes$
Strong classical propositional logic ($\mathbf{CPL^{+}}$) | $p_{i},\neg p_{i},\bot,\mathop{\mbox{\small\rm NE}}$ | $\wedge,\otimes$
Propositional independence logic ($\mathbf{PI}$) | $p_{i},\neg p_{i},\bot,$ | $\wedge,\otimes$
$p_{i_{1}}\dots p_{i_{k}}\perp p_{j_{1}}\dots p_{j_{m}}$
Strong propositional independence logic ($\mathbf{PI}^{+}$) | $p_{i},\neg p_{i},\bot,\mathop{\mbox{\small\rm NE}},$ | $\wedge,\otimes$
$p_{i_{1}}\dots p_{i_{k}}\perp p_{j_{1}}\dots p_{j_{m}}$
Propositional team logic ($\mathbf{PT}$) | $p_{i},\neg p_{i},\bot$ | $\wedge,\varoast,\vee$
Strong propositional team logic ($\mathbf{PT}^{+}$) | $p_{i},\neg p_{i},\bot,\mathop{\mbox{\small\rm NE}}$ | $\wedge,\otimes,\vee$
Propositional union closed logic ($\mathbf{PU}$) | $p_{i},\neg p_{i},\bot$ | $\wedge,\otimes,\varoast$
Strong propositional union closed logic ($\mathbf{PU}^{+}$) | $p_{i},\neg p_{i},\bot,\mathop{\mbox{\small\rm NE}}$ | $\wedge,\otimes,\varoast$
Propositional inclusion logic ($\mathbf{PInc}$) | $p_{i},\neg p_{i},\bot,$ | $\wedge,\otimes$
$p_{i_{1}}\dots p_{i_{k}}\subseteq p_{j_{1}}\dots p_{j_{k}}$
Strong propositional inclusion logic ($\mathbf{PInc}^{+}$) | $p_{i},\neg p_{i},\bot,\mathop{\mbox{\small\rm NE}},$ | $\wedge,\otimes$
$p_{i_{1}}\dots p_{i_{k}}\subseteq p_{j_{1}}\dots p_{j_{k}}$
Propositional dependence logic ($\mathbf{PD}$) | $p_{i},\neg p_{i},\bot,$ | $\wedge,\otimes,\vee$
$\mathop{=\\!}(p_{i_{1}}\dots p_{i_{k}},p_{j})$
Strong propositional dependence logic ($\mathbf{PD}^{+}$) | $p_{i},\neg p_{i},\bot,$ | $\wedge,\otimes,\vee,\multimap$
$\mathop{=\\!}(p_{i_{1}}\dots p_{i_{k}},p_{j})$
Full propositional team logic ($\mathbf{FPT}$) | $p_{i},\neg p_{i},\bot,\mathop{\mbox{\small\rm NE}},$ | $\wedge,\otimes,\varoast,\vee$
$p_{i_{1}}\dots p_{i_{k}}\perp p_{j_{1}}\dots p_{j_{m}}$
$\mathop{=\\!}(p_{i_{1}}\dots p_{i_{k}},p_{j})$
$p_{i_{1}}\dots p_{i_{k}}\subseteq p_{j_{1}}\dots p_{j_{k}}$

We are interested in fragments of $\mathbf{FPT}$ that are expressively
complete for some nice sets of team properties as defined in Definition 2.6.
The languages of these fragments are determined in terms of which atoms and
connective are allowed. Table 2 defines the sets of atoms and connectives of
the languages of these logics. Apart from $\mathbf{FPT}$, we consider six
other types of propositional logics, namely, classical logic, independence
logic, team logic, union closed logic, inclusion logic and dependence logic,
each of which has two variants, a weak version that has the empty team
property, and a strong version that contains the $\mathop{\mbox{\small\rm
NE}}$ atom or the linear implication $\multimap$ in its language. The
propositional independence logic, propositional inclusion logic and
propositional dependence logic we define here are propositional version of
their first-order counterparts introduced in [13, 10, 27]. The propositional
team logic defined as in Table 2 does not directly correspond to the
propositional fragment of the first-order team logic studied in [27, 21], and
the reader should not confuse the two logics. The propositional union closed
logic is a new logic that was not previously considered in the literature.

$\mathbf{PD}$$\mathbf{PD}^{+}$$\mathbf{PU}^{+}$$\mathbf{PU}$$\mathbf{PInc}^{+}$$\mathbf{PInc}$$\mathbf{CPL^{+}}$$\mathbf{PI}^{+}$$\mathbf{PI}$$\mathbf{CPL}$$\mathbf{PT}^{+}$,
$\mathbf{FPT}$$\mathbf{PT}$flat logicdownwardclosed logicsunion
closedlogics12logic with theempty team property12logic without theempty team
property12expressively completelogic$L_{2}$$L_{1}$

$<$

$L_{2}$$L_{1}$

$\geq$

Figure 1: Expressive power of propositional team logics

##  3 Expressive Power and Normal Forms

In this section, we study the expressive power of the propositional team
logics defined in Table 2 and their normal forms. We will also prove the
interconnections illustrated in Figure 1.

To begin with, recall from [34] that for each team $X$ on a finite set
$N=\\{i_{1},\dots,i_{n}\\}$ of indices, the classical formula

$\Theta_{X}=\operatorname*{\bigotimes}_{s\in
X}(p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge p_{i_{n}}^{s(i_{n})})$

(in disjunctive normal form) defines the team $X$ _modulo subteams_ , where
$p_{i}^{1}:=p_{i}$ and $p_{i}^{0}:=\neg p_{i}$ for any index $i$. That is, for
any team $Y$ on $N$,

$Y\models\Theta_{X}\iff Y\subseteq X.$ (4)

Using this formula, we can prove the expressive completeness of $\mathbf{CPL}$
under the team semantics for the set of all flat team properties, as
illustrated in Figure 1.

######  Theorem 3.1.

$\mathbf{CPL}$ characterizes the set of all flat team properties.

###### Proof.

Recall from Definitions 2.5 and 2.6 that we need to show that for any finite
set $N=\\{i_{1},\dots,i_{n}\\}$ of indices, every classical formula
$\phi(p_{i_{1}},\dots,p_{i_{n}})$ defines a flat team property, i.e.,
$\llbracket\phi\rrbracket$ is flat, and every flat team property
$\mathsf{P}\subseteq\mathcal{P}(2^{N})$ is definable by some classical formula
$\phi(p_{i_{1}},\dots,p_{i_{n}})$, i.e.,
$\llbracket\phi\rrbracket=\mathsf{P}$. The former follows from Lemma 2.4. We
now prove the latter. Let $\mathsf{P}$ be a flat team property and
$\\{s_{1}\\},\dots,\\{s_{k}\\}$ all singleton teams in $\mathsf{P}$. Putting
$X=\\{s_{1},\dots,s_{k}\\}$, we have
$\mathsf{P}=\llbracket\Theta_{X}\rrbracket$, since for any team $Y$ on $N$,

$Y\models\Theta_{X}\iff Y\subseteq X\in\mathsf{P}\iff Y\in\mathsf{P}.$

∎

Clearly, from the above theorem it follows that the standard disjunctive
normal form of $\mathbf{CPL}$ under the usual single valuation semantics is
also a normal form of $\mathbf{CPL}$ under the team semantics. Another
immediate corollary of the expressive completeness of $\mathbf{CPL}$ for the
set of all flat properties is that flatness is equivalent to being logically
equivalent to a classical formula in propositional team logics, as stated in
the theorem below. Flatness was originally introduced by Hodges [18] in the
first-order context, and further studied in [27]. In the first-order
dependence logic case all classical first-order formulas have the flatness
property (see, e.g., [27]) but the converse is not true. For example, all
first-order sentences (i.e., formulas without free variables) have the
flatness property for the trivial reason that their truth in any model is
decided by the truth in the singleton team $\\{\emptyset\\}$ of the empty
assignment $\emptyset$ alone (see Lemma 1.1.14 in [32]).

######  Theorem 3.2.

Let $\phi$ be a formula in the language of $\mathbf{FPT}$. The following are
equivalent.

(i)

$\phi$ has the flatness property.

(ii)

$\phi$ is semantically equivalent to a classical formula.

(iii)

$\phi$ has the downward closure property and the union closure property.

###### Proof.

The equivalence of (i) and (ii) follows from Theorem 3.1 and the equivalence
of (i) and (iii) is easy to verify. ∎

Our characterization of classical propositional logic can be equivalently
formulated as follows: The classical propositional logic cannot be extended in
the context of team semantics to a propositional logic which satisfies both
the downward closure and the union closure property. This is remotely
reminiscent of the characterization of classical first-order logic, known as
Lindström’s Theorem [22], to the effect that classical first-order logic
cannot be extended in the context of abstract logics to a logic which
satisfies both the Downward Löwenheim-Skolem Theorem and the Compactness
Theorem.

Recall from [34] that $\mathbf{PD}$ is expressively complete for the set of
all downward closed team properties which contain the empty team. Having
established also the expressive completeness of $\mathbf{CPL}$ for the set of
all flat team properties, we now proceed towards the proof of the other
expressive completeness results illustrated in Figure 1.

The set of subteams of a fixed team $X$ on a finite set $N$ is characterized
by the classical formula $\Theta_{X}$ (in the sense of (4)). We now show that
with the non-emptiness or the nonempty disjunction, a team can be
characterized precisely.

######  Lemma 3.3.

Let $X$ be a team on a finite set $N=\\{i_{1},\dots,i_{n}\\}$ of indices.
Define

$\Theta^{\ast}_{X}:=\operatorname*{\bigotimes}_{s\in
X}(p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge
p_{i_{n}}^{s(i_{n})}\wedge\mathop{\mbox{\small\rm
NE}})\quad\text{and}\quad\Theta^{\ast\ast}_{X}:=\mathop{\raisebox{-1.9pt}{$\huge\text{$\varoast$}$}}_{s\in
X}(p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge p_{i_{n}}^{s(i_{n})}).$

For any team $Y$ on $N$, we have

(i)

$Y\models\Theta^{\ast}_{X}\iff Y=X.$

(ii)

$Y\models\Theta^{\ast\ast}_{X}\iff Y=X$ or $Y=\emptyset$.

###### Proof.

The direction “$\Longleftarrow$” for both items is obvious. For the direction
“$\Longrightarrow$” of item (i), suppose $Y\models\Theta^{\ast}_{X}$. If
$X=\emptyset$, then $\Theta^{\ast}_{X}=\bot$, hence $Y=\emptyset=X$.
Otherwise, for each $s\in X$ there exists a set $Y_{s}$ such that

$Y=\bigcup_{s\in X}Y_{s}\text{ and }Y_{s}\models
p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge
p_{i_{n}}^{s(i_{n})}\wedge\mathop{\mbox{\small\rm NE}}.$

Clearly, $Y_{s}=\\{s\\}$ for each $s\in X$, implying $Y=X$.

For the direction “$\Longrightarrow$” of item (ii), suppose
$Y\models\Theta^{\ast\ast}_{X}$. If $Y=\emptyset$, then we are done.
Otherwise, $Y=X$ is proved by a similar argument to that of item (i). ∎

Next, we prove that many of the logics we defined in Section 2 (see Table 2)
are expressively complete for certain sets of team properties (see Definitions
2.5 and 2.6 for definitions of the relevant notions).

######  Theorem 3.4.

(i)

Both $\mathbf{PT}^{+}$ and $\mathbf{FPT}$ characterize the set of all team
properties, i.e., every team property is definable in the logics. In
particular, $\mathbf{PT}^{+}\equiv\mathbf{FPT}$.

(ii)

$\mathbf{PT}$ characterizes the set of all team properties which contain the
empty team.

(iii)

$\mathbf{PU}$ characterizes the set of all union closed team properties which
contain the empty team.

(iv)

$\mathbf{PU}^{+}$ characterizes the set of all union closed team properties.

(v)

$\mathbf{PD}$ characterizes the set of all downward closed team properties
which contain the empty team.

(vi)

$\mathbf{PD}^{+}$ characterizes the set of all downward closed team
properties.

###### Proof.

Let $N=\\{i_{1},\dots,i_{n}\\}$ be an arbitrary finite set of indices.

(i) Obviously every formula $\phi(p_{i_{1}},\dots,p_{i_{n}})$ in the language
of $\mathbf{PT}^{+}$ or $\mathbf{FPT}$ defines a team property on $N$, i.e.,
$\llbracket\phi\rrbracket\subseteq\mathcal{P}(2^{N})$. Conversely, for any
team property $\mathsf{P}\subseteq\mathcal{P}(2^{N})$, we shall show
$\mathsf{P}=\llbracket\operatorname*{\bigvee}_{X\in\mathsf{P}}\Theta^{\ast}_{X}\rrbracket$.

By Lemma 3.3(i), for any team $Y$ on $N$,

$Y\models\operatorname*{\bigvee}_{X\in\mathsf{P}}\Theta^{\ast}_{X}\iff\exists
X\in\mathsf{P}(Y=X)\iff Y\in\mathsf{P}.$

In particular, if $\mathsf{P}=\emptyset$, then
$\llbracket\operatorname*{\bigvee}_{X\in\emptyset}\Theta^{\ast}_{X}\rrbracket=\llbracket\bot\wedge\mathop{\mbox{\small\rm
NE}}\rrbracket=\emptyset$.

(ii) Since formulas $\phi(p_{i_{1}},\dots,p_{i_{n}})$ in the language of
$\mathbf{PT}$ have the empty team property, we have
$\emptyset\in\llbracket\phi\rrbracket\subseteq\mathcal{P}(2^{N})$. Conversely,
for any team property $\mathsf{P}\subseteq\mathcal{P}(2^{N})$ with
$\emptyset\in\mathsf{P}$, we show
$\mathsf{P}=\llbracket\operatorname*{\bigvee}_{X\in\mathsf{P}}\Theta^{\ast\ast}_{X}\rrbracket$.

By Lemma 3.3(ii), for any team $Y$ on $N$,

$Y\models\operatorname*{\bigvee}_{X\in\mathsf{P}}\Theta^{\ast\ast}_{X}\iff\exists
X\in\mathsf{P}(Y=X)\text{ or }Y=\emptyset\iff Y\in\mathsf{P}.$

(iii) It is easy to show by induction that every formula $\phi$ in the
language of $\mathbf{PU}$ has the union closure property and the empty team
property, which imply that $\llbracket\phi\rrbracket$ is a union closed team
property that contains the empty team. Conversely, for any union closed team
property $\mathsf{P}\subseteq\mathcal{P}(2^{N})$ with
$\emptyset\in\mathsf{P}$, we show that
$\mathsf{P}=\llbracket\operatorname*{\bigotimes}_{X\in\mathsf{P}}\Theta^{\ast\ast}_{X}\rrbracket$.

If $Y\in\mathsf{P}$, then, by Lemma 3.3(ii) we have
$Y\models\Theta^{\ast\ast}_{Y}$ and
$Y\models\operatorname*{\bigotimes}_{X\in\mathsf{P}}\Theta^{\ast\ast}_{X}$.
Conversely, if
$Y\models\operatorname*{\bigotimes}_{X\in\mathsf{P}}\Theta^{\ast\ast}_{X}$,
then for each $X\in\mathsf{P}$ there is $Y_{X}\subseteq Y$ such that
$Y=\bigcup_{X\in\mathsf{P}}Y_{X}$ and $Y_{X}\models\Theta^{\ast\ast}_{X}$. By
Lemma 3.3(ii), we have $Y_{X}=\emptyset$ or $Y_{X}=X$ for each
$X\in\mathsf{P}$. Since $\emptyset\in\mathsf{P}$ and $\mathsf{P}$ is a union
closed team property, we conclude that $Y\in\mathsf{P}$.

(iv) Obviously $\llbracket\mathop{\mbox{\small\rm NE}}\rrbracket$ is a union
closed team property. Thus, by item (iii), for every formula $\phi$ in the
language of $\mathbf{PU}^{+}$, $\llbracket\phi\rrbracket$ is a union closed
team property. Conversely, for any union closed team property
$\mathsf{P}\subseteq\mathcal{P}(2^{N})$, we show that $\mathsf{P}$ is
definable by some formula $\phi$ in the language of $\mathbf{PU}^{+}$.

If $\mathsf{P}$ contains the empty team, then
$\mathsf{P}=\llbracket\operatorname*{\bigotimes}_{X\in\mathsf{P}}\Theta^{\ast\ast}_{X}\rrbracket$
by item (iii). If $\emptyset\notin\mathsf{P}$, then it is easy to verify that
$\mathsf{P}=\llbracket\mathop{\mbox{\small\rm
NE}}\wedge\operatorname*{\bigotimes}_{X\in\mathsf{P}}\Theta^{\ast\ast}_{X}\rrbracket$.

(v) This item is a consequence of results in [34]. Note that in [34],
propositional dependence logic and some of its variants (including
propositional inquisitive logic) are all shown to be expressively complete for
the set of all downward closed team properties which contain the empty team.
With a slight abuse of notation, we denote in this paper by $\mathbf{PD}$ any
of these equivalent logics.

(vi) It is easy to show, by induction, that every formula $\phi$ in the
language of $\mathbf{PD}^{+}$ has the downward closure property, which implies
that $\llbracket\phi\rrbracket$ is a downward closed team property.
Conversely, for any downward closed team property
$\mathsf{P}\subseteq\mathcal{P}(2^{N})$, we show that $\mathsf{P}$ is
definable by some formula in the language of $\mathbf{PU}^{+}$.

If $\mathsf{P}$ is a downward closed team property that contains the empty
set, then by item (v), we know that $\mathsf{P}$ is definable by some formula
in the language of $\mathbf{PD}$ (thus also in the language of
$\mathbf{PD}^{+}$). If $\emptyset\notin\mathsf{P}$, then since $\mathsf{P}$ is
a downward closed team property, we must have $\mathsf{P}=\emptyset$. Clearly,
$\mathsf{P}=\emptyset=\llbracket\top\multimap\bot\rrbracket$.∎

Results in Theorems 3.4 and 3.1 are illustrated in Figure 1, where all those
expressively complete logics are represented in shaded rectangles labeled with
their corresponding characteristic team properties. The logics $\mathbf{FPT}$,
$\mathbf{PT}^{+}$ and $\mathbf{PT}$ do not have a label in Figure 1, as they
characterize the set of arbitrary team properties (with or without the empty
team). Except for the flat team property, each characteristic team property we
study here has two variants. One with the empty team in the property and the
other one without this constraint. We have an expressively complete logic for
certain set of team properties that has the empty team property (indicated by
a solid rectangle) and an expressively complete logic for the same set of team
properties without the empty team property (indicated by a dashed rectangle).

We remarked in Section 2 that in any propositional team logic with the empty
team property, the nonempty disjunction $\varoast$ and the might modality
$\triangledown$ are inter-definable (Equation (1)). Consequently, classical
propositional logic extended with the might modality $\triangledown$ has the
same expressive power as $\mathbf{PU}$ and thereby is also expressively
complete for the set of all union closed team properties which contain the
empty team.

Propositional independence logic $\mathbf{PI}$ is expressively properly
included in the expressively strongest logic $\mathbf{PT}^{+}$. In particular,
the independence atoms are definable in $\mathbf{PT}^{+}$:

$p_{i_{1}}\dots p_{i_{k}}\perp p_{j_{1}}\dots
p_{j_{m}}\equiv\bigvee_{X\in\mathcal{X}_{I,J}}\Theta_{X}^{\ast},$ (5)

where $I=\\{i_{1},\dots,i_{k}\\}$, $J=\\{j_{1},\dots,j_{m}\\}$ and

$\mathcal{X}_{I,J}=\\{X\subseteq\\{0,1\\}^{I\cup J}\mid X=(X\upharpoonright
I)\times(X\upharpoonright J)\\}.$

The expressive power of $\mathbf{PI}$ is an open problem.

Another immediate consequence of the expressive completeness of
$\mathbf{PT}^{+}$ for the set of all team properties is that all the possible
atoms and all the instances of all the possible connectives are expressible in
the expressively strongest logic $\mathbf{PT}^{+}$. Consider the _Boolean
negation_ $\sim$ defined as

  * 1.

$X\models\sim\\!\phi$ iff $X\not\models\phi$

Clearly $\mathop{\mbox{\small\rm NE}}\equiv\sim\\!\bot$ and
$\phi\vee\psi\equiv\sim(\sim\phi\wedge\sim\psi)$. Thus $\mathbf{CPL^{+}}$
extended with the Boolean negation $\sim$ has the same expressive power as
$\mathbf{PT}^{+}$. See [24] for other properties of the Boolean negation
$\sim$ and a complete axiomatization for propositional dependence logic
extended with $\sim$. In this paper we will restrict our attention to the
considerably simpler logical constant $\mathop{\mbox{\small\rm NE}}$ instead
of $\sim$. Note that from the equivalence of the two logics, we only derive
that _every instance_ of $\sim\phi$ is expressible in $\mathbf{PT}^{+}$, but
Boolean negation turns out to be not _uniformly definable_ in
$\mathbf{PT}^{+}$ (see [33]).

From the proofs of Theorem 3.1 and Theorem 3.4 we obtain interesting
disjunctive normal forms for the logics, as listed in (the self-explanatory)
Table 3. It is worth taking note of the many similarities and at the same time
the subtle differences of these normal forms.

Logic | Normal Form
---|---
$\mathbf{PT}^{+}$ | $\displaystyle\operatorname*{\bigvee}_{f\in F}\operatorname*{\bigotimes}_{s\in X_{f}}(p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge p_{i_{n}}^{s(i_{n})}\wedge\mathop{\mbox{\small\rm NE}})$
$\mathbf{FPT}$
$\mathbf{PT}$ | $\displaystyle\operatorname*{\bigvee}_{f\in F}\mathop{\raisebox{-1.9pt}{$\huge\text{$\varoast$}$}}_{s\in X_{f}}(p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge p_{i_{n}}^{s(i_{n})})$
$\mathbf{PU}^{+}$ | either $\displaystyle\mathop{\mbox{\small\rm NE}}\wedge\operatorname*{\bigotimes}_{f\in F}\mathop{\raisebox{-1.9pt}{$\huge\text{$\varoast$}$}}_{s\in X_{f}}(p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge p_{i_{n}}^{s(i_{n})})$ or $\displaystyle\operatorname*{\bigotimes}_{f\in F}\mathop{\raisebox{-1.9pt}{$\huge\text{$\varoast$}$}}_{s\in X_{f}}(p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge p_{i_{n}}^{s(i_{n})})$
$\mathbf{PU}$ | $\displaystyle\operatorname*{\bigotimes}_{f\in F}\mathop{\raisebox{-1.9pt}{$\huge\text{$\varoast$}$}}_{s\in X_{f}}(p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge p_{i_{n}}^{s(i_{n})})$
$\mathbf{PD}$ | $\displaystyle\operatorname*{\bigvee}_{f\in F}\operatorname*{\bigotimes}_{s\in X_{f}}(p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge p_{i_{n}}^{s(i_{n})})$
$\mathbf{PD}^{+}$ | either $\displaystyle\operatorname*{\bigvee}_{f\in F}\operatorname*{\bigotimes}_{s\in X_{f}}(p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge p_{i_{n}}^{s(i_{n})})$ or $\top\multimap\bot$
$\mathbf{CPL}$ | $\displaystyle\operatorname*{\bigotimes}_{s\in X_{f}}(p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge p_{i_{n}}^{s(i_{n})})$
Table 3: Normal forms of propositional team logics

We now prove the results in Figure 1 concerning the comparison of the logics
in terms of their expressive powers. In Figure 1, the logics placed in the
same rectangle have the same expressive power. If a line connects two sets of
logics, then the logics $\mathsf{L}_{2}$ positioned above are expressively
strictly stronger than the logics $\mathsf{L}_{1}$ positioned below, i.e.,
$\mathsf{L}_{1}<\mathsf{L}_{2}$. If instead, $\mathsf{L}_{1}$ and
$\mathsf{L}_{2}$ are connected by a double line, then only
$\mathsf{L}_{1}\leq\mathsf{L}_{2}$ is known. As discussed already, the logic
$\mathbf{PT}^{+}$ and $\mathbf{FPT}$ are expressively complete for the set of
all team properties, thus they are both the expressively strongest logics. The
logic $\mathbf{PT}$ is expressively complete for the set of all team
properties which contain the empty set, therefore it has stronger expressive
power than the two logics $\mathbf{PU}$ and $\mathbf{PI}$ that characterize
certain team properties which contain the empty set. For any other pair of
logics that are linked by a solid line or a double line in Figure 1, if the
one that is positioned above is an extension of the other, then it obviously
has stronger expressive power. The logics $\mathbf{CPL}$, $\mathbf{PU}$,
$\mathbf{PD}$, $\mathbf{PI}$ and $\mathbf{PT}$ that have the empty team
property are strictly weaker than their corresponding logics
$\mathbf{CPL^{+}}$, $\mathbf{PU}^{+}$, $\mathbf{PD}^{+}$, $\mathbf{PI}^{+}$
and $\mathbf{PT}^{+}$ that do not have the empty team property, respectively.
$\mathbf{PD}$ is strictly stronger than $\mathbf{CPL}$ because classical
formulas have the flatness property, while $\mathbf{PD}$ has formulas that
lack the flatness property (see [34] for detail). The union closed logics
$\mathbf{CPL^{+}}$, $\mathbf{PU}$ and $\mathbf{PU}^{+}$ are expressively
different from the non-union closed logics $\mathbf{PI}^{+}$, $\mathbf{PT}$
and $\mathbf{PT}^{+}$, respectively. For instance, the formulas $p_{0}\perp
p_{1}$ and $p_{0}\vee p_{1}$ are not closed under unions. Similarly, the
downward closed logics $\mathbf{PD}$ and $\mathbf{PD}^{+}$ are expressively
different from the non-downward closed logics $\mathbf{PI}$ and
$\mathbf{PI}^{+}$, respectively. For instance, the formula $p_{0}\perp p_{1}$
is not closed downward.

It now remains to prove that $\mathbf{PD}$ and $\mathbf{PD}^{+}$ are
expressively weaker than $\mathbf{PI}$ and $\mathbf{PI}^{+}$, respectively.
This reduces to showing that dependence atoms are expressible in $\mathbf{PI}$
and in $\mathbf{PI}^{+}$. First, note that the independence atoms
$\vec{x}\perp\vec{y}$ are known as _unconditional_ independence atoms in the
literature of independence logic. A _conditional_ independence atom [13] is
written as $\vec{x}\perp_{\vec{z}}\vec{y}$ and its semantics is defined by the
clause

  * 1.

$X\models\,p_{j_{1}}\dots p_{j_{b}}\perp_{p_{i_{1}}\dots
p_{i_{a}}}p_{k_{1}}\dots p_{k_{c}}$ iff for all $s,s^{\prime}\in X$ with
$s(\vec{i})=s^{\prime}(\vec{i})$, there exists $s^{\prime\prime}\in X$ such
that

$s^{\prime\prime}(\vec{i})=s(\vec{i})=s^{\prime}(\vec{i}),\quad
s^{\prime\prime}(\vec{j})=s(\vec{j})\quad\text{and}\quad
s^{\prime\prime}(\vec{k})=s^{\prime}(\vec{k}),$

where $\vec{i}=i_{1}\dots i_{a}$, $\vec{j}=j_{1}\dots j_{b}$ and
$\vec{k}=k_{1}\dots k_{c}$.

In our setting conditional independence atoms are expressible in terms of
unconditional ones:

$\displaystyle\vec{x}\perp_{p_{i_{1}}\dots
p_{i_{a}}}\vec{y}\equiv\operatorname*{\bigotimes}_{s\in
2^{I}}\big{(}p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge
p_{i_{a}}^{s(i_{a})}\wedge(\vec{x}\perp\vec{y})\big{)},$

where $I=\\{i_{1},\dots,i_{a}\\}$. As observed already in [13] in the context
of first-order logic, dependence atoms are definable in terms of conditional
independence atoms:

$\mathop{=\\!}(\vec{x},p_{i})\equiv p_{i}\perp_{\vec{x}}p_{i}.$

Putting these altogether, we conclude that dependence atoms are expressible in
$\mathbf{PI}$ and in $\mathbf{PI}^{+}$. This completes the proof of the inter-
relationships shown in Figure 1.

##  4 Metalogical properties

In this section, we study metalogical properties of propositional team logics.
We will prove that propositional team logics are compact, and closed under
classical substitutions.

###  4.1 Compactness

Propositional inquisitive logic was shown to be compact in [5]. As a
consequence, propositional logics of dependence are all compact (see Theorem
3.3 in [34]). Moreover, from the same argument as given in [3] the compactness
of all the other propositional team logics follows as well. Below we present a
sketch of this proof (which makes essential use of König’s Lemma) using the
terminologies of this paper for the benefit of the reader.

######  Theorem 4.1 (Compactness Theorem).

For any set $\Gamma\cup\\{\phi\\}$ of formulas in the language of an arbitrary
propositional team logic, if $\Gamma\models\phi$, then there exists a finite
set $\Gamma_{0}\subseteq\Gamma$ such that $\Gamma_{0}\models\phi$.

###### Proof.

Let $\Gamma=\\{\theta_{k}\mid k\in\mathbb{N}\\}$. For each $k\in\mathbb{N}$,
define $\gamma_{k}=\theta_{1}\wedge\dots\wedge\theta_{k}$. It is sufficient to
show that $\gamma_{k}\models\phi$ for some $k\in\mathbb{N}$. Towards a
contradiction, assume otherwise. Then for each $k\in\mathbb{N}$, there exists
a team $X\subseteq 2^{\mathbb{N}}$ such that $X\models\gamma_{k}$ and
$X\not\models\phi$. Let $N_{k}$ be the set of all indices of all propositional
variables occurring in $\gamma_{k}$ and $\phi$. By the locality property of
propositional team logics, the finite set

$\mathcal{X}_{k}=\\{X\subseteq 2^{N_{k}}:X\models\gamma_{k}\text{ and
}X\not\models\phi\\}$

is nonempty. Put
$T=\\{\emptyset\\}\cup\bigcup_{k\in\mathbb{N}}\mathcal{X}_{k}$. Define a
relation $\leq$ on $T$ by putting

  * 1.

$\emptyset\leq X$ for all $X\in T$;

  * 2.

$X\leq Y$ iff $Y\upharpoonright\rm{dom}(X)=X$.

It is not hard to see that $(T,\leq)$ is a finitely branching infinite tree.
By König’s Lemma, the tree has an infinite branch $\langle X_{k}\mid
k\in\mathbb{N}\rangle$, where $X_{k}\in\mathcal{X}_{k}$ for each
$k\in\mathbb{N}$. Putting $N=\bigcup_{k\in\mathbb{N}}N_{k}$, this infinite
branch determines a team $X\subseteq 2^{N}$ in such a way that
$X\upharpoonright N_{k}=X_{k}$ for each $k\in\mathbb{N}$. Clearly,
$X\not\models\phi$ and $X\models\gamma_{k}$ for each $k\in\mathbb{N}$. These
contradict $\Gamma\models\phi$. ∎

###  4.2 Closure under classical substitutions

A _substitution_ of a propositional team logic $\mathsf{L}$ is a mapping
$\sigma$ from the set ${\rm Form}_{\mathsf{L}}$ of all well-formed formulas of
$\mathsf{L}$ into the set ${\rm Form}_{\mathsf{L}}$ itself that commutes with
the connectives and atoms of $\mathsf{L}$. We say that $\mathsf{L}$ is _closed
under_ the substitution $\sigma$, if for any set $\Gamma\cup\\{\phi\\}$ of
formulas of $\mathsf{L}$,

$\Gamma\models\phi\Longrightarrow\\{\sigma(\gamma)\mid\gamma\in\Gamma\\}\models\sigma(\phi).$

If $\mathsf{L}$ is closed under all substitutions, then we say that
$\mathsf{L}$ is _closed under uniform substitution_. The logics
$\mathbf{FPT}$, $\mathbf{PT}$, $\mathbf{PT}^{+}$, $\mathbf{PD}$,
$\mathbf{PD}^{+}$, $\mathbf{PI}$ and $\mathbf{PI}^{+}$ are not closed under
uniform substitution, because, for instance, we have

$p_{i}\otimes p_{i}\models p_{i}\text{ and }p_{i}\varoast p_{i}\models p_{i},$

whereas

$\mathop{=\\!}(p_{i})\otimes\mathop{=\\!}(p_{i})\not\models\mathop{=\\!}(p_{i}),\quad(p_{i}\perp
p_{i})\otimes(p_{i}\perp p_{i})\not\models p_{i}\perp p_{i},$ $(p_{i}\vee\neg
p_{i})\otimes(p_{i}\vee\neg p_{i})\not\models(p_{i}\vee\neg p_{i})\text{ and
}(p_{i}\vee\neg p_{i})\varoast(p_{i}\vee\neg p_{i})\not\models(p_{i}\vee\neg
p_{i}).$

The logics $\mathbf{PU}^{+}$ and $\mathbf{PU}$ are not closed under uniform
substitution either (for at least the trivial reason that strings of the form
$\neg(\phi\varoast\psi)$ are not well-formed formulas), but nontrivial
counter-examples of the above kind for the two logics are yet to be found. It
was shown in [3] and [20] that propositional logics of dependence are,
nevertheless, closed under _flat substitutions_ , i.e., substitutions $\sigma$
such that $\sigma(p)$ has the flatness property for any propositional variable
$p$. Using the method in [20], we will prove in this section that
propositional team logics are closed under _classical substitutions_ , i.e.,
substitutions $\sigma$ such that $\sigma(p)$ is a classical formula (i.e., a
formula in the language of $\mathbf{CPL}$) for any propositional variable $p$.

Let us start by examining in detail the notion of substitution in our logics.
The well-formed formulas of the propositional team logics we consider in this
paper are assumed to be in _negation normal form_ and we do not allow
arbitrary formulas to occur in a dependence or independence atom. Strings of
the form $\neg\phi$, $\vec{\phi}\perp\vec{\psi}$,
$\mathop{=\\!}(\vec{\phi},\psi)$ and $\vec{\phi}\subseteq\vec{\psi}$ are not
necessarily well-formed formulas of our logics. As such, the notion of
substitution is actually not well-defined in our logics. To derive our
intended closure under substitution result we will then first need to seek for
ways to make sense of the notion of substitution in our logics. In general,
there are two possible solutions: either to expand the languages of the logics
so as to allow more well-formed formulas, or to restrict the range of a
substitution to a subset of the full set ${\rm Form}_{\mathsf{L}}$ of well-
formed formulas. We will take both approaches at the same time. We will
confine ourselves to classical substitutions only and will also expand the
language of our logics to include every substitution instance $\sigma(\phi)$
of a classical substitution $\sigma$ to be a well-formed formula. Our reason
for restricting attention to classical substitutions only is twofold.
Conceptually, we do not have a good intuition of the intended semantics of the
formulas $\neg(\phi\varoast\psi)$ and $\neg(\phi\vee\psi)$ or of the
dependence and independence atoms $\vec{\phi}\perp\vec{\psi}$,
$\mathop{=\\!}(\vec{\phi},\psi)$ and $\vec{\phi}\subseteq\vec{\psi}$ with
arbitrary arguments. Technically, arbitrary substitutions are not very
interesting, as the logics are not closed under uniform substitution.

For simplicity, in what follows we will only work with $\mathbf{FPT}$ which
has the maximal set of atoms and connectives among the propositional team
logics we consider in this paper. Similar results for the other logics can be
easily obtained as corollaries of those for $\mathbf{FPT}$. Let us now expand
the language of $\mathbf{FPT}$ and include strings of the forms $\neg\alpha$,
$\top$, $\vec{\alpha}\perp\vec{\beta}$, $\mathop{=\\!}(\vec{\alpha},\beta)$
and $\vec{\alpha}\subseteq\vec{\beta}$ as well-formed formulas, where
$\alpha,\beta,\vec{\alpha}$ and $\vec{\beta}$ are classical formulas or
sequences of classical formulas. Denote the extended logic by $\mathbb{MPT}$.
Observe that $\mathbb{MPT}$ will, clearly, have the same expressive power as
$\mathbf{FPT}$, since the latter is already expressively complete for the set
of all team properties (Theorem 3.4(i)).

We now define the semantics of $\mathbb{MPT}$. Given sequences
$\vec{\alpha}=\alpha_{1}\dots\alpha_{k}$ and
$\vec{\beta}=\beta_{1}\dots\beta_{k}$ of classical formulas, we define an
equivalence relation $\sim_{(\vec{\alpha},\vec{\beta})}$ on the set of all
valuations as follows:

$s\sim_{(\vec{\alpha},\vec{\beta})}s^{\prime}\quad\text{ iff }\quad\forall
i\in\\{1,\dots,k\\}\,(\\{s\\}\models\alpha_{i}\iff\\{s^{\prime}\\}\models\beta_{i}).$

We write $\sim_{\vec{\alpha}}$ for $\sim_{(\vec{\alpha},\vec{\alpha})}$.

######  Definition 4.2.

The team semantics of well-formed formulas of $\mathbb{MPT}$ is defined
inductively in the same way as in Definitions 2.3 and 2.8 and additionally we
have the following extra clauses:

  * 1.

$X\models\neg\alpha$ iff $s\not\models\alpha$ in the usual sense for all $s\in
X$.

  * 2.

$X\models\top$ always holds.

  * 3.

$X\models\vec{\alpha}\perp\vec{\beta}$ iff for all $s,s^{\prime}\in X$, there
exists $s^{\prime\prime}\in X$ such that
$s\sim_{\vec{\alpha}}s^{\prime\prime}\text{ and
}\mathop{s^{\prime}\sim_{\vec{\beta}}s^{\prime\prime}}.$

  * 4.

$X\models\mathop{=\\!}(\vec{\alpha},\beta)$ iff for all $s,s^{\prime}\in X$,
$\text{if }s\sim_{\vec{\alpha}}s^{\prime}\text{ then
}s\sim_{\beta}s^{\prime}.$

  * 5.

$X\models\vec{\alpha}\subseteq\vec{\beta}$ iff for all $s\in X$, there exists
$s^{\prime}\in X$ such that $s\sim_{(\vec{\alpha},\vec{\beta})}s^{\prime}.$

The above definition deserves some comments. In the literature of logics of
dependence and independence, negation is usually treated only _syntactically_.
That is, a negated classical formula $\neg\phi$ is defined to have the same
semantics as the unique formula $\phi^{\sim}$ in _negation normal form_
obtained by exhaustively applying the De Morgan’s laws and the following
syntactic rewrite rules:

$\begin{array}[]{rclcrclcrcl}p^{\sim}&\mapsto&\neg
p&{}{}{}{}{}{}{}{}\hfil&\top^{\sim}&\mapsto&\bot&{}{}{}{}{}{}{}{}\hfil&(\phi\wedge\psi)^{\sim}&\mapsto&\phi^{\sim}\otimes\psi^{\sim}\\\
(\neg
p)^{\sim}&\mapsto&p&&\bot^{\sim}&\mapsto&\top&&(\phi\otimes\psi)^{\sim}&\mapsto&\phi^{\sim}\wedge\psi^{\sim}\\\
\end{array}$ (6)

A routine inductive proof shows that $\neg\alpha\equiv\alpha^{\sim}$ for all
classical formulas $\alpha$ (or see [20] for the proof), i.e., our negation as
defined in Definition 4.2 coincides with the above syntactic negation when
applied to classical formulas. It is also worth noting that our negation
corresponds to the defined connective $\sim\downarrow$ in Hodges [17, 18].

The extended inclusion atom $\vec{\alpha}\subseteq\vec{\beta}$ is also studied
in [15] in the context of modal inclusion logic. There it is shown that the
usual modal logic extended with the extended inclusion atoms has the same
expressive power as the usual modal logic extended with the might modality
$\triangledown$ (see Section 2, under the heading “non-emptiness atom”). Given
this result, it is natural to conjecture that classical propositional logic
extended with the extended inclusion atoms has the same expressive power as
classical propositional logic extended with the might modality
$\triangledown$, and it is also expressively complete for the set of union
closed team properties which contain the empty team (see the remark after
Theorem 3.4).

If $\alpha$ is a classical formula and $\sigma$ is a classical substitution,
then $\sigma(\alpha)$ is still a classical formula. In particular, given any
classical substitution, the substitution instance of an extended dependence
and independence atom is a well-formed formula of the extended logic
$\mathbb{MPT}$. Having the notion of classical substitution well-defined in
$\mathbb{MPT}$, we will now prove that $\mathbb{MPT}$ is closed under
classical substitutions, namely the following theorem holds.

######  Theorem 4.3.

Let $\Gamma\cup\\{\phi\\}$ be a set of formulas in the language of
$\mathbb{MPT}$, and $\sigma$ a classical substitution. If $\Gamma\models\phi$,
then $\\{\sigma(\gamma)\mid\gamma\in\Gamma\\}\models\sigma(\phi)$.

Note that this theorem also implies that the original logic $\mathbf{FPT}$ is
closed under those classical substitutions $\sigma$ such that $\sigma(\phi)$
is a well-formed formula of $\mathbf{FPT}$, whenever $\phi$ is. In this sense,
Theorem 4.3 also characterizes the behavior of substitutions in the original
logic $\mathbf{FPT}$.

For the proof of Theorem 4.3, we first establish the following lemma, which
generalizes Lemma 3.5 in [20] concerning flat substitutions (note that
classical substitutions are also flat substitutions). For any valuation $s$
and any substitution $\sigma$, define a valuation $s_{\sigma}$ as

$s_{\sigma}(i)=\left\\{\begin{array}[]{ll}1&\text{if
$\\{s\\}\models\sigma(p_{i})$;}\\\ 0&\text{if
$\\{s\\}\not\models\sigma(p_{i})$.}\\\ \end{array}\right.$

For any team $X$, we write $X_{\sigma}=\\{s_{\sigma}\mid s\in X\\}.$

######  Lemma 4.4.

For any formula $\phi$ in the language of $\mathbb{MPT}$ and any classical
substitution $\sigma$, we have

$X\models\sigma(\phi)\iff X_{\sigma}\models\phi.$

###### Proof.

We prove the lemma by induction on $\phi$. The case
$\phi=\\{\mathop{\mbox{\small\rm NE}},\bot,\top\\}$ is trivial. Case
$\phi=p_{i}$. Since $\sigma(p_{i})$ has the flatness property, we have

$X\models\sigma(p_{i})\iff\forall s\in
X(\\{s\\}\models\sigma(p_{i}))\iff\forall s_{\sigma}\in
X_{\sigma}(\\{s_{\sigma}\\}\models p_{i})\iff X_{\sigma}\models p_{i}.$

Case $\phi=\vec{\alpha}\perp\vec{\beta}$, where $\vec{\alpha}$ and
$\vec{\beta}$ are sequences of classical formulas. To show the direction
“$\Longrightarrow$”, assume
$X\models\sigma(\vec{\alpha})\perp\sigma(\vec{\beta})$. For any
$s_{\sigma},s^{\prime}_{\sigma}\in X_{\sigma}$, we have $s,s^{\prime}\in X$
and there is $s^{\prime\prime}\in X$ such that
$s\sim_{\sigma(\vec{\alpha})}s^{\prime\prime}$ and
$s^{\prime}\sim_{\sigma(\vec{\beta})}s^{\prime\prime}$. By the induction
hypothesis, we have $s_{\sigma}\sim_{\vec{\alpha}}s^{\prime\prime}_{\sigma}$
and $s^{\prime}_{\sigma}\sim_{\vec{\beta}}s^{\prime\prime}_{\sigma}$, as
required. The other direction “$\Longleftarrow$” is proved analogously.

The cases $\phi=\mathop{=\\!}(\vec{\alpha},\beta)$ and
$\phi=\vec{\alpha}\subseteq\vec{\beta}$, where
$\vec{\alpha},\vec{\beta},\beta$ are (sequences of) classical formulas, are
proved analogously.

Case $\phi=\psi\varoast\chi$. For the direction “$\Longrightarrow$”, assuming
$X\models\sigma(\psi)\varoast\sigma(\chi)$, if $X=\emptyset$, then
$X_{\sigma}=\emptyset\models\psi\varoast\chi$. If $X\neq\emptyset$, then there
are nonempty sets $Y,Z\subseteq X$ such that $X=Y\cup Z$ and
$Y\models\sigma(\psi)$ and $Z\models\sigma(\chi)$. Since $Y_{\sigma}\cup
Z_{\sigma}=X_{\sigma}$ and $Y_{\sigma},Z_{\sigma}\neq\emptyset$, we obtain
$X_{\sigma}\models\psi\varoast\chi$ by the induction hypothesis. The other
direction “$\Longleftarrow$” is proved analogously.

The case $\phi=\psi\otimes\chi$ is proved analogously. The cases
$\phi=\neg\alpha$ for $\alpha$ classical, $\phi=\psi\wedge\chi$ and
$\phi=\psi\vee\chi$ follow readily from the induction hypothesis. ∎

Finally, we give the proof of Theorem 4.3.

###### Proof of Theorem 4.3.

If $\Gamma\models\phi$, then for any team $X$,

$\displaystyle X\models\sigma(\gamma)\text{ for all }\gamma\in\Gamma$
$\displaystyle\Longrightarrow X_{\sigma}\models\gamma\text{ for all
}\gamma\in\Gamma~{}~{}\text{ (by
\lx@cref{creftypecap~refnum}{lemsigmaoperation})}$
$\displaystyle\Longrightarrow X_{\sigma}\models\phi~{}~{}\text{ (by the
assumption)}$ $\displaystyle\Longrightarrow X\models\sigma(\phi)~{}~{}\text{
(by \lx@cref{creftypecap~refnum}{lemsigmaoperation})}$

Hence $\\{\sigma(\gamma)\mid\gamma\in\Gamma\\}\models\sigma(\phi)$. ∎

##  5 Axiomatizations

In this section, we study the axiomatization problem of propositional team
logics. For a set of $n$ propositional variables, there are in total
$2^{2^{n}}$ teams. Therefore propositional team logics are clearly
_decidable_. Concrete axiomatizations for propositional logics of dependence
can be found in [34]. In this section, we give natural deduction systems and
prove the Completeness Theorem for the logics $\mathbf{PT}^{+}$,
$\mathbf{CPL^{+}}$, $\mathbf{PI}^{+}$ and $\mathbf{PInc}^{+}$. Among the
propositional team logics we have defined, these are the logics that have the
non-emptiness $\mathop{\mbox{\small\rm NE}}$ but not the nonempty disjunction
$\varoast$ in their languages. The problem of finding (nontrivial)
axiomatizations for the other logics, especially for propositional
independence logic $\mathbf{PI}$, is open.

###  5.1 $\mathbf{PT}^{+}$

In this subsection, we define a natural deduction system of strong
propositional team logic ($\mathbf{PT}^{+}$), an expressively strongest logic,
and prove the Soundness and Completeness Theorems for it.

We first present our natural deduction system. We adopt the standard
conventions of natural deduction systems (readers who are not familiar with
natural deduction systems are referred to, e.g., [30, 2]). For example, the
letter $D$ (with or without subscripts) in the following definition stand for
an arbitrary derivation (with or without extra assumptions). As discussed in
Section 4.2, $\mathbf{PT}^{+}$ (and also the other propositional team logics
to be axiomatized) are _not_ closed under uniform substitution. Therefore, the
(sound and complete) deduction system given by the definition below will _not_
admit the _Substitution Rule_

$\phi(p_{i_{1}},\dots,p_{i_{n}})$ $\mathsf{Sub}$
$\phi(\sigma(p_{i_{1}})/p_{i_{1}},\dots,\sigma(p_{i_{n}})/p_{i_{n}})$

In particular, the axioms and rules of the system presented below using
concrete formulas such as $p_{i}$ should _not_ be read as schemata. Only the
metalanguage symbols $\phi$, $\psi$ and $\chi$ stand for arbitrary formulas.

######  Definition 5.1 (A natural deduction system of $\mathbf{PT}^{+}$).

AXIOMS
---
Atomic excluded middle |  $\mathop{\mbox{\small\rm NE}}$ introduction
$\textsf{EM}_{0}$ $p_{i}\otimes\neg p_{i}$ |  $\mathop{\mbox{\small\rm NE}}\textsf{I}$ $\bot\vee\mathop{\mbox{\small\rm NE}}$

RULES
---
Conjunction introduction |  Conjunction elimination
$D_{1}$ $\phi$ $D_{2}$ $\psi$ $\wedge\textsf{I}$ $\phi\wedge\psi$ |  $D$ $\phi\wedge\psi$ $\wedge\textsf{E}$ $\phi$ $D$ $\phi\wedge\psi$ $\wedge\textsf{E}$ $\psi$

Boolean disjunction introduction |  Boolean disjunction elimination
---|---
$D$ $\phi$ $\vee\textsf{I}$ $\phi\vee\psi$ $D$ $\psi$ $\vee\textsf{I}$ $\phi\vee\psi$ |  $D_{0}$ $\phi\vee\psi$ $[\phi]$ $D_{1}$ $\chi$ $[\psi]$ $D_{2}$ $\chi$ $\vee\textsf{E}$ $\chi$
Tensor disjunction weak introduction |  Tensor disjunction weakening
$D$ $\phi$ ($\ast$) $\otimes\textsf{I}^{-}$ $\phi\otimes\psi$ |  $D$ $\phi$ $\otimes\textsf{W}$ $\phi\otimes\phi$
($\ast$) whenever $\psi$ dose not contain $\mathop{\mbox{\small\rm NE}}$ |
Tensor disjunction weak elimination |  Tensor disjunction weak substitution
$D_{0}$ $\phi\otimes\psi$ $[\phi]$ $D_{1}$ $\alpha$ $[\psi]$ $D_{2}$ $\alpha$ $(\ast)$ $\otimes\textsf{E}^{-}$ $\alpha$ |  $D_{1}$ $\phi\otimes\psi$ $[\psi]$ $D_{2}$ $\chi$ ($\ast$) $\otimes\textsf{Sub}^{-}$ $\phi\otimes\chi$
($\ast$) whenever $\alpha$ is a classical formula and the undischarged assumptions in the derivations $D_{1}$ and $D_{2}$ contain classical formulas only |  ($\ast$) whenever the undischarged assumptions in the derivation $D_{2}$ contain classical formulas only
Commutative and associative laws for tensor disjunction
$D$ $\phi\otimes\psi$ $\textsf{Com}\otimes$ $\psi\otimes\phi$ |  $D$ $\phi\otimes(\psi\otimes\chi)$ $\textsf{Ass}\otimes$ $(\phi\otimes\psi)\otimes\chi$
Contradiction introduction |  Contradiction elimination
$D$ $p_{i}\wedge\neg p_{i}$ $\bot\textsf{I}$ $\bot$ |  $D$ $\phi\otimes\bot$ $\mathbf{\bot}\textsf{E}$ $\phi$
Strong _ex falso_ |  Strong contradiction contraction
$D$ $\bot\wedge\mathop{\mbox{\small\rm NE}}$ $\it{\textsf{ex falso}}^{+}$ $\phi$ |  $D$ $\phi\otimes(\bot\wedge\mathop{\mbox{\small\rm NE}})$ $\mathbf{0}\textsf{Ctr}$ $\bot\wedge\mathop{\mbox{\small\rm NE}}$

Strong contradiction introduction
---
$D$ $\displaystyle\Big{(}\operatorname*{\bigotimes}_{s\in X}(p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge p_{i_{n}}^{s(i_{n})}\wedge\mathop{\mbox{\small\rm NE}})\Big{)}\wedge\Big{(}\operatorname*{\bigotimes}_{s\in Y}(p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge p_{i_{n}}^{s(i_{n})}\wedge\mathop{\mbox{\small\rm NE}})\Big{)}$ ($\ast$) $\mathbf{0}\textsf{I}$ $\bot\wedge\mathop{\mbox{\small\rm NE}}$ |
($\ast$) whenever $X$ and $Y$ are distinct teams on $\\{i_{1},\dots,i_{n}\\}$
Distributive laws
$D$ $\phi\otimes(\psi\vee\chi)$ $\textsf{Dstr}\otimes\vee$ $(\phi\otimes\psi)\vee(\phi\otimes\chi)$ |  $D$ $\displaystyle\mathop{\mbox{\small\rm NE}}\wedge\operatorname*{\bigotimes}_{i\in I}\phi_{i}$ Dstr $\mathop{\mbox{\small\rm NE}}\wedge\otimes$ $\displaystyle\operatorname*{\bigvee}_{\emptyset\neq J\subseteq I}\,\operatorname*{\bigotimes}_{i\in J}(\mathop{\mbox{\small\rm NE}}\wedge\phi_{i})$

The above deduction system consists of two axioms and fifteen sets of rules.
The atomic excluded middle axiom $\textsf{EM}_{0}$ is _not_ an axiom schema.
Especially, as discussed in the previous section, the substitution instances
of $\neg p_{i}$ are not necessarily well-formed formulas of $\mathbf{PT}^{+}$.
The conjunction $\wedge$ and the Boolean disjunction $\vee$ have the usual
introduction and elimination rules. The usual commutative law, associative law
and distributive laws for the two connectives can be derived easily in the
system. Over classical formulas the tensor disjunction admits the usual
Introduction Rule and Elimination Rule. Over non-classical formulas the rules
for the tensor disjunction $\otimes$ are more subtle. The Introduction Rule
$\otimes\textsf{I}^{-}$ is not in general sound in case $\psi$ does not have
the empty team property. For instance, we have
$\bot\not\models\bot\otimes\mathop{\mbox{\small\rm NE}}$. But the weakening
rule $\otimes\textsf{W}$ is sound and we will apply this rule later on in our
completeness proof. The elimination rule $\otimes\textsf{E}^{-}$ is not in
general sound in case $\alpha$ is non-classical. For instance, we have
$p_{i}\otimes\neg p_{i}\not\models p_{i}\vee\neg p_{i}$, even if $p_{i}\models
p_{i}\vee\neg p_{i}$ and $\neg p_{i}\models p_{i}\vee\neg p_{i}$. The rules
$\otimes\textsf{E}^{-}$ and $\otimes\textsf{Sub}^{-}$ have some side
conditions concerning the undischarged assumptions in the sub-derivations. To
see why these restrictions are necessary, note, for example, that for the rule
$\otimes\textsf{E}^{-}$ we have

$(\mathop{\mbox{\small\rm NE}}\wedge p)\otimes(\mathop{\mbox{\small\rm
NE}}\wedge\neg p),p\otimes\neg p\not\models\bot,$ $\text{ even if
}(\mathop{\mbox{\small\rm NE}}\wedge p)\otimes(\mathop{\mbox{\small\rm
NE}}\wedge\neg p),p\models\bot\text{ and }(\mathop{\mbox{\small\rm NE}}\wedge
p)\otimes(\mathop{\mbox{\small\rm NE}}\wedge\neg p),\neg p\models\bot$

and for the rule $\otimes\textsf{Sub}^{-}$ we have

$\mathop{\mbox{\small\rm NE}}\not\models\mathop{\mbox{\small\rm
NE}}\otimes(\mathop{\mbox{\small\rm NE}}\wedge\bot),\text{ even if
}\mathop{\mbox{\small\rm NE}}\models\mathop{\mbox{\small\rm
NE}}\otimes\bot\text{ and }\mathop{\mbox{\small\rm
NE}},\bot\models\mathop{\mbox{\small\rm NE}}\wedge\bot.$

In the absence of the usual (Strong) Introduction Rule and Elimination Rule
for $\otimes$, we added the (weak) substitution, commutative and associative
rules for $\otimes$ to the system. We also include some of the distributive
laws that involve $\otimes$ in our system, and we derive the other sound
distributive laws in the next proposition. The usual distributive laws that
are not listed in Definition 5.1 are not sound in our system, see [34] for
examples of the failure of these laws. The non-emptiness
$\mathop{\mbox{\small\rm NE}}$, the weak and strong negation ($\bot$ and
$\bot\wedge\mathop{\mbox{\small\rm NE}}$) have self-explanatory rules in our
system.

######  Proposition 5.2.

The following are derivable in the natural deduction system of
$\mathbf{PT}^{+}$:

(i)

Weak ex falso ($\it{\textsf{ex falso}}^{-}$): If $\phi$ does not contain
$\mathop{\mbox{\small\rm NE}}$, then $\bot\vdash\phi$.

(ii)

The usual commutative law, associative law and distributive law for
conjunction and Boolean disjunction.

(iii)

Distributive laws:

(a)
$\phi\otimes(\psi\wedge\chi)\vdash(\phi\otimes\psi)\wedge(\phi\otimes\chi)$
($\textsf{Dstr}\otimes\wedge$)
---
(b) $\phi\vee(\psi\otimes\chi)\vdash(\phi\vee\psi)\otimes(\phi\vee\chi)$
($\textsf{Dstr}\vee\otimes$)
(c) $(\phi\otimes\psi)\vee(\phi\otimes\chi)\vdash\phi\otimes(\psi\vee\chi)$
($\textsf{Dstr}\otimes\vee\otimes$)
(d) If $\alpha$ is a classical formula, then
|  \-
$(\alpha\wedge\psi)\otimes(\alpha\wedge\chi)\vdash\alpha\wedge(\psi\otimes\chi)$
($\textsf{Dstr}^{\ast}\\!\wedge\otimes\wedge$)
---
\-
$\alpha\wedge(\psi\otimes\chi)\vdash(\alpha\wedge\psi)\otimes(\alpha\wedge\chi)$
($\textsf{Dstr}^{\ast}\\!\wedge\otimes$)

###### Proof.

The rules in item (ii) are derived as usual. The items (a), (c) and (d) are
not hard to derive (or see the proof of Proposition 4.6 in [34]). We will only
give the derivation for the other rules.

For $\it{\textsf{ex falso}}^{-}$, assuming that $\phi$ does not contain
$\mathop{\mbox{\small\rm NE}}$, we have the following derivation

$\bot$ $\otimes\textsf{I}^{-}$ $\bot\otimes\phi$ $\mathbf{\bot}\textsf{E}$
$\phi$

For $\textsf{Dstr}\vee\otimes$, we have the following derivation

$\phi\vee(\psi\otimes\chi)$ [$\phi$] $\otimes\textsf{W}$ $\phi\otimes\phi$
$\vee\textsf{I}$, $\otimes\textsf{Sub}^{-}$
$(\phi\vee\psi)\otimes(\phi\vee\chi)$ [$\psi\otimes\chi$] $\vee\textsf{I}$,
$\otimes\textsf{Sub}^{-}$ $(\phi\vee\psi)\otimes(\phi\vee\chi)$
$\vee\textsf{E}$ $(\phi\vee\psi)\otimes(\phi\vee\chi)$

∎

Next, we prove the Soundness Theorem for our deduction system.

######  Theorem 5.3 (Soundness Theorem).

For any set $\Gamma\cup\\{\phi\\}$ of formulas in the language of
$\mathbf{PT}^{+}$, we have
$\Gamma\vdash\phi\,\Longrightarrow\,\Gamma\models\phi.$

###### Proof.

We show that $\Gamma\models\phi$ holds for each derivation
$D=\\{\delta_{1},\dots,\delta_{k}\\}$ with the conclusion $\phi$ and the
hypotheses in $\Gamma$.

If $D$ is a singleton, then $\phi\in\Gamma$ or $\phi=p_{i}\otimes\neg p_{i}$
or $\phi=\bot\vee\mathop{\mbox{\small\rm NE}}$. In the first case, obviously
$\\{\phi\\}\models\phi$. The last two cases are also easy because the two
formulas are clearly valid.

The induction steps for the rules 1-4, 6, 9-12, 14 and the distributive rules
$\textsf{Dstr}\otimes\vee$ and $\textsf{Dstr}\otimes\vee\otimes$ are easy to
verify. We only check the induction step for the other rules.

$\otimes\textsf{I}^{-}$: Assume that $D$ is a derivation for $\Pi\vdash\phi$.
We show that $\Pi\models\phi\otimes\psi$ whenever $\psi$ is does not contain
$\mathop{\mbox{\small\rm NE}}$. Suppose $X\models\theta$ for all
$\theta\in\Pi$. By the induction hypothesis, we have $\Pi\models\phi$, thus
$X\models\phi$ follows. Now, since $\psi$ does not contain
$\mathop{\mbox{\small\rm NE}}$, an easy inductive proof shows it has the empty
team property, i.e., $\emptyset\models\psi$. Hence we obtain $\emptyset\cup
X\models\phi\otimes\psi$ as required.

$\otimes\textsf{E}^{-}$: Assume that $D_{0}$, $D_{1}$ and $D_{2}$ are
derivations for $\Pi_{0}\vdash\phi\otimes\psi$, $\Pi_{1},\phi\vdash\alpha$ and
$\Pi_{2},\psi\vdash\alpha$, respectively. Assume that $\alpha$ is a classical
formula and $\Pi_{1}$ and $\Pi_{2}$ contain classical formulas only. We show
that $\Pi_{0},\Pi_{1},\Pi_{2}\models\alpha$ follows from the induction
hypothesis $\Pi_{0}\models\phi\otimes\psi$, $\Pi_{1},\phi\models\alpha$ and
$\Pi_{2},\psi\models\alpha$. Suppose $X\models\theta$ for all
$\theta\in\Pi_{0}\cup\Pi_{1}\cup\Pi_{2}$. Then we have
$X\models\phi\otimes\psi$, which means that there exist $Y,Z\subseteq X$ such
that $X=Y\cup Z$, $Y\models\phi$ and $Z\models\psi$. For all
$\theta\in\Pi_{1}\cup\Pi_{2}$, since $\theta$ is a classical formula, by Lemma
2.4 we know that $\theta$ has the downward closure property. It then follows
that $Y\models\theta_{1}$ for all $\theta_{1}\in\Pi_{1}$ and
$Z\models\theta_{2}$ for all $\theta_{2}\in\Pi_{2}$. Thus $Y\models\alpha$ and
$Z\models\alpha$. Since $\alpha$ is a classical formula, by Lemma 2.4 we know
that $\alpha$ has the union closure property, which yields that
$X\models\alpha$.

$\otimes\textsf{Sub}^{-}$: Assume that $D_{1}$ and $D_{2}$ are derivations for
$\Pi_{1}\vdash\phi\otimes\psi$ and $\Pi_{2},\psi\vdash\chi$, respectively and
$\Pi_{2}$ contains classical formulas only. We show that
$\Pi_{1},\Pi_{2}\models\phi\otimes\chi$ follows from the induction hypothesis
$\Pi_{1}\models\phi\otimes\psi$ and $\Pi_{2},\psi\models\chi$. Suppose
$X\models\theta$ for all $\theta\in\Pi_{1}\cup\Pi_{2}$. By the induction
hypothesis, we have $X\models\phi\otimes\psi$, which means there exist
$Y,Z\subseteq X$ such that $X=Y\cup Z$, $Y\models\phi$ and $Z\models\psi$. For
all $\theta\in\Pi_{2}$, since $\theta$ is a classical formula, by Lemma 2.4 we
know that $\theta$ has the downward closure property. Thus $Z\models\theta$.
It then follows from the induction hypothesis that $Z\models\chi$. Hence we
conclude $Y\cup Z=X\models\phi\otimes\chi$.

$\mathbf{0}\textsf{I}$: It suffices to show that if $X$ and $Y$ are distinct
teams on $\\{i_{1},\dots,i_{n}\\}$, then
$Z\not\models\Theta_{X}^{\ast}\wedge\Theta_{Y}^{\ast}$ for all teams $Z$. In
view of the locality property, we may assume that $Z$ is a team on
$\\{i_{1},\dots,i_{n}\\}$. By Lemma 3.3, if
$Z\models\Theta^{\ast}_{X}\wedge\Theta^{\ast}_{Y}$, then $X=Z=Y$, which
contradicts the assumption.

$\textsf{Dstr}^{\ast}\\!$ $\wedge\otimes$: It suffices to show that
$\phi\wedge(\psi\otimes\chi)\models(\phi\wedge\psi)\otimes(\phi\wedge\chi)$,
whenever $\phi$ does not contain $\mathop{\mbox{\small\rm NE}}$. Suppose
$X\models\phi\wedge(\psi\otimes\chi)$. Then $X\models\phi$, $Y\models\psi$ and
$Z\models\chi$ for some teams $Y,Z\subseteq X$ with $Y\cup Z=X$. Since $\phi$
does not contain $\mathop{\mbox{\small\rm NE}}$, an easy inductive proof shows
that $\phi$ has the downward closure property. Thus $Y\models\phi$ and
$Z\models\phi$. Hence $Y\models\phi\wedge\psi$ and $Z\models\phi\wedge\chi$,
implying $X\models(\phi\wedge\psi)\otimes(\phi\wedge\chi)$.

Dstr $\mathop{\mbox{\small\rm NE}}$ $\wedge\otimes$: It suffices to show that
if $X\models\mathop{\mbox{\small\rm NE}}\wedge\operatorname*{\bigotimes}_{i\in
I}\phi_{i}$ for some team $X$, then $X\models\operatorname*{\bigotimes}_{i\in
J}(\mathop{\mbox{\small\rm NE}}\wedge\phi_{i})$ for some nonempty $J\subseteq
I$. The assumption implies that $X\neq\emptyset$ and there exist teams
$X_{i}\subseteq X$ for each $i\in I$ such that $\bigcup_{i\in I}X_{i}=X$ and
$X_{i}\models\phi_{i}$. Let $J\subseteq I$ be the set of indices $i\in I$ such
that $X_{i}\neq\emptyset$. Since $X\neq\emptyset$, we must have that
$J\neq\emptyset$. Hence $X_{i}\models\mathop{\mbox{\small\rm
NE}}\wedge\phi_{i}$ for each $i\in J$ and
$X\models\operatorname*{\bigotimes}_{i\in J}(\mathop{\mbox{\small\rm
NE}}\wedge\phi_{i})$. ∎

We now proceed to prove the main result of this section, the Completeness
Theorem for our system. Our argument is similar to that of the proof of the
Completeness Theorem for propositional logics of dependence in [34]. The
reader may compare what follows with Section 4.2 in [34]. To begin with, below
we present a crucial lemma that is very similar to Lemma 3.2 in [34].

######  Lemma 5.4.

For any finite nonempty collections of teams $\\{X_{f}\mid f\in F\\}$,
$\\{Y_{g}\mid g\in G\\}$ on some fixed domain, the following are equivalent:

(a)

$\displaystyle\operatorname*{\bigvee}_{f\in
F}\Theta_{X_{f}}^{\ast}\models\operatorname*{\bigvee}_{g\in
G}\Theta_{Y_{g}}^{\ast}$;

(b)

for each $f\in F$, we have $X_{f}=Y_{g_{f}}$ for some $g\in G$.

###### Proof.

Follows easily from Lemma 3.3. ∎

Two formulas $\phi$ and $\psi$ are said to be _provably equivalent_ (written
$\phi\dashv\vdash\psi$) if both $\phi\vdash\psi$ and $\psi\vdash\phi$ hold.
Another crucial step for the completeness proof is to establish that every
formula is provably equivalent in the deduction system to a formula in the
disjunctive normal form shown in Table 3. Let us now state this as a lemma.

######  Lemma 5.5.

Every formula $\phi(p_{i_{1}},\dots,p_{i_{n}})$ in the language of
$\mathbf{PT}^{+}$ is provably equivalent to a formula in the normal form

$\operatorname*{\bigvee}_{f\in F}\Theta_{X_{f}}^{\ast},~{}\text{ where
}~{}\Theta_{X_{f}}^{\ast}=\operatorname*{\bigotimes}_{s\in
X_{f}}(p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge
p_{i_{n}}^{s(i_{n})}\wedge\mathop{\mbox{\small\rm NE}}),$ (7)

$\\{X_{f}\mid f\in F\\}$ a finite set of teams on $N=\\{i_{1},\dots,i_{n}\\}$.

The detailed proof of the above lemma will be postponed. We now give the proof
of the Completeness Theorem for our system.

######  Theorem 5.6 (Completeness Theorem).

For any formulas $\phi$ and $\psi$ in the language of $\mathbf{PT}^{+}$, we
have $\psi\models\phi\Longrightarrow\psi\vdash\phi$. In particular,
$\models\phi\Longrightarrow\,\vdash\phi$.

###### Proof.

Suppose $\psi\models\phi$, where $\phi=\phi(p_{i_{1}},\dots,p_{i_{n}})$ and
$\psi=\psi(p_{i_{1}},\dots,p_{i_{n}})$. By Lemma 5.5, we have

$\phi\dashv\vdash\operatorname*{\bigvee}_{f\in
F}\Theta^{\ast}_{X_{f}}\quad\text{ and
}\quad\psi\dashv\vdash\operatorname*{\bigvee}_{g\in G}\Theta^{\ast}_{Y_{g}}$
(8)

for some finite sets $\\{X_{f}\mid f\in F\\}$ and $\\{Y_{g}\mid g\in G\\}$ of
teams on $\\{i_{1},\dots,i_{n}\\}$. The Soundness Theorem and (8) imply that

$\operatorname*{\bigvee}_{f\in
F}\Theta^{\ast}_{X_{f}}\models\operatorname*{\bigvee}_{g\in
G}\Theta^{\ast}_{Y_{g}}.$ (9)

If $F=\emptyset$, then $\phi\dashv\vdash\bot\wedge\mathop{\mbox{\small\rm
NE}}$. We obtain $\phi\vdash\psi$ by $\it{\textsf{ex falso}}^{+}$. If
$G=\emptyset$, then $\psi\dashv\vdash\bot\wedge\mathop{\mbox{\small\rm NE}}$.
In view of (9), we must have $F=\emptyset$ as well and
$\phi\dashv\vdash\bot\wedge\mathop{\mbox{\small\rm NE}}$. Hence
$\phi\vdash\psi$.

If $F,G\neq\emptyset$, then by Lemma 5.4, for each $f\in F$ we have
$X_{f}=Y_{g_{f}}$ and $\Theta^{\ast}_{X_{f}}=\Theta^{\ast}_{Y_{g_{f}}}$ for
some $g_{f}\in G$, which implies that
$\Theta^{\ast}_{X_{f}}\vdash\operatorname*{\bigvee}_{g\in
G}\Theta^{\ast}_{Y_{g}}$ by $\vee\textsf{I}$. Hence, we obtain
$\operatorname*{\bigvee}_{f\in
F}\Theta^{\ast}_{X_{f}}\vdash\operatorname*{\bigvee}_{g\in
G}\Theta^{\ast}_{Y_{g}}$ by applying $\vee\textsf{E}$. Finally, in view of (8)
we conclude that $\phi\vdash\psi$. ∎

######  Theorem 5.7 (Strong Completeness Theorem).

For any set $\Gamma\cup\\{\phi\\}$ of formulas in the language of
$\mathbf{PT}^{+}$, we have
$\Gamma\models\phi\,\Longrightarrow\,\Gamma\vdash\phi.$

###### Proof.

By Theorem 5.6 and the Compactness Theorem (Theorem 4.1). ∎

We end this section by supplying the proof of Lemma 5.5.

###### Proof of Lemma 5.5.

Note that in the statement of the lemma we have fixed a set
$\\{p_{i_{1}},\dots,p_{i_{n}}\\}$ of variables. These variables all occur in
the formula (7) in normal form, but not necessarily all of them actually occur
in the formula $\phi(p_{i_{1}},\dots,p_{i_{n}})$. In order to take care of
this subtle point we first prove the following claim:

######  Claim.

If $\\{i_{1},\dots,i_{m}\\}\subset\\{j_{1},\dots,j_{k}\\}$, then any formula
$\psi(p_{i_{1}},\dots,p_{i_{m}})$ in the normal form is provably equivalent to
a formula $\theta(p_{j_{1}},\dots,p_{j_{k}})$ in the normal form.

_Proof of the claim._ Without loss of generality we may assume that
$K=\\{j_{1},\dots,j_{k}\\}=\\{i_{1},\dots,i_{m},i_{m+1},\dots,i_{k}\\}$ and
$k>m$. By the assumption, we have

$\psi(p_{i_{1}},\dots,p_{i_{m}})=\operatorname*{\bigvee}_{f\in
F}\operatorname*{\bigotimes}_{s\in
X_{f}}(p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge
p_{i_{m}}^{s(i_{m})}\wedge\mathop{\mbox{\small\rm NE}}),$

where $\\{X_{f}\mid f\in F\\}$ is a finite set of teams on
$M=\\{i_{1},\dots,i_{m}\\}$. Let

$\theta(p_{i_{1}},\dots,p_{i_{k}})=\operatorname*{\bigvee}_{f\in
F}\mathop{\bigvee_{Y\subseteq 2^{K}}}_{Y\upharpoonright
M=X_{f}}\operatorname*{\bigotimes}_{s\in
Y}(p_{i_{1}}^{s(i_{1})}\wedge\dots\dots
p_{i_{k}}^{s(i_{k})}\wedge\mathop{\mbox{\small\rm NE}}).$

The following derivation proves $\theta\vdash\psi$:

$\begin{array}[]{rll}(1)&\displaystyle\operatorname*{\bigvee}_{f\in
F}\mathop{\bigvee_{Y\subseteq 2^{K}}}_{Y\upharpoonright
M=X_{f}}\operatorname*{\bigotimes}_{s\in
Y}(p_{i_{1}}^{s(i_{1})}\wedge\dots\dots
p_{i_{k}}^{s(i_{k})}\wedge\mathop{\mbox{\small\rm NE}})\\\
(2)&\displaystyle\operatorname*{\bigvee}_{f\in F}\mathop{\bigvee_{Y\subseteq
2^{K}}}_{Y\upharpoonright M=X_{f}}\operatorname*{\bigotimes}_{s\in
Y}(p_{i_{1}}^{s(i_{1})}\wedge\dots\dots
p_{i_{m}}^{s(i_{m})}\wedge\mathop{\mbox{\small\rm
NE}})&(\wedge\textsf{E},\otimes\textsf{Sub}^{-})\\\
(3)&\displaystyle\operatorname*{\bigvee}_{f\in
F}\operatorname*{\bigotimes}_{s\in
X_{f}}(p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge
p_{i_{m}}^{s(i_{m})}\wedge\mathop{\mbox{\small\rm
NE}})&(\vee\textsf{E})\end{array}$

Conversely, $\psi\vdash\theta$ is proved by the following derivation:

$\begin{array}[]{rl}(1)&\displaystyle\operatorname*{\bigvee}_{f\in
F}\operatorname*{\bigotimes}_{s\in
X_{f}}(p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge
p_{i_{m}}^{s(i_{m})}\wedge\mathop{\mbox{\small\rm NE}})\\\
(2)&\displaystyle(p_{i_{m+1}}\otimes\neg
p_{i_{m+1}})\wedge\dots\wedge(p_{i_{k}}\otimes\neg
p_{i_{k}})\quad\text{($\textsf{EM}_{0}$, $\wedge\textsf{I}$)}\\\
(3)&\displaystyle\operatorname*{\bigotimes}_{t\in 2^{K\setminus
M}}(p_{i_{m+1}}^{t(i_{m+1})}\wedge\dots\wedge
p_{i_{k}}^{t(i_{k})})\quad((2),\textsf{Dstr}^{\ast}\\!\wedge\otimes)\\\
(4)&\displaystyle\Big{(}\operatorname*{\bigvee}_{f\in
F}\operatorname*{\bigotimes}_{s\in
X_{f}}(p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge
p_{i_{m}}^{s(i_{m})}\wedge\mathop{\mbox{\small\rm
NE}})\Big{)}\wedge\Big{(}\operatorname*{\bigotimes}_{t\in 2^{K\setminus
M}}(p_{i_{m+1}}^{t(i_{m+1})}\wedge\dots\wedge p_{i_{k}}^{t(i_{k})})\Big{)}\\\
&~{}~{}((1),(3),\wedge\textsf{I})\\\
(5)&\displaystyle\operatorname*{\bigvee}_{f\in
F}\operatorname*{\bigotimes}_{s\in
X_{f}}\Big{(}p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge
p_{i_{m}}^{s(i_{m})}\wedge\big{(}\mathop{\mbox{\small\rm
NE}}\wedge\operatorname*{\bigotimes}_{t\in 2^{K\setminus
M}}(p_{i_{m+1}}^{t(i_{m+1})}\wedge\dots\wedge
p_{i_{k}}^{t(i_{k})})\big{)}\Big{)}\\\
&~{}~{}(\textsf{Dstr}^{\ast}\\!\wedge\otimes)\\\
(6)&\displaystyle\operatorname*{\bigvee}_{f\in
F}\operatorname*{\bigotimes}_{s\in
X_{f}}\Big{(}p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge
p_{i_{m}}^{s(i_{m})}\wedge\bigvee_{\emptyset\neq Z\subseteq 2^{K\setminus
M}}\,\operatorname*{\bigotimes}_{t\in
Z}(p_{i_{m+1}}^{t(i_{m+1})}\wedge\dots\wedge
p_{i_{k}}^{t(i_{k})}\wedge\mathop{\mbox{\small\rm NE}})\Big{)}\\\
&~{}~{}(\textsf{Dstr}\mathop{\mbox{\small\rm
NE}}\wedge\otimes,\otimes\textsf{Sub}^{-})\\\
(7)&\displaystyle\operatorname*{\bigvee}_{f\in
F}\operatorname*{\bigotimes}_{s\in X_{f}}\,\bigvee_{\emptyset\neq Z\subseteq
2^{K\setminus M}}\Big{(}p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge
p_{i_{m}}^{s(i_{m})}\wedge\operatorname*{\bigotimes}_{t\in
Z}(p_{i_{m+1}}^{t(i_{m+1})}\wedge\dots\wedge
p_{i_{k}}^{t(i_{k})}\wedge\mathop{\mbox{\small\rm NE}})\Big{)}\\\
(8)&\displaystyle\operatorname*{\bigvee}_{f\in
F}\,\operatorname*{\bigotimes}_{s\in X_{f}}\,\bigvee_{\emptyset\neq Z\subseteq
2^{N\setminus M}}\,\operatorname*{\bigotimes}_{t\in
Z}(p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge p_{i_{m}}^{s(i_{m})}\wedge
p_{i_{m+1}}^{t(i_{m+1})}\wedge\dots\wedge
p_{i_{k}}^{t(i_{k})}\wedge\mathop{\mbox{\small\rm NE}})\\\
&~{}~{}(\textsf{Dstr}^{\ast}\\!\wedge\otimes)\\\ \end{array}$
$\begin{array}[]{rl}(9)&\displaystyle\operatorname*{\bigvee}_{f\in
F}\,\bigvee_{G:X_{f}\to\mathcal{Z}}\operatorname*{\bigotimes}_{s\in
X_{f}}\,\operatorname*{\bigotimes}_{t\in
G(s)}(p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge p_{i_{m}}^{s(i_{m})}\wedge
p_{i_{m+1}}^{t(i_{m+1})}\wedge\dots\wedge
p_{i_{k}}^{t(i_{k})}\wedge\mathop{\mbox{\small\rm NE}})\\\ &~{}~{}\text{where
}\mathcal{Z}=\\{Z\subseteq 2^{K\setminus M}\mid
Z\neq\emptyset\\}\quad(\textsf{Dstr}\otimes\vee)\\\
(10)&\displaystyle\operatorname*{\bigvee}_{f\in F}\mathop{\bigvee_{Y\subseteq
2^{K}}}_{Y\upharpoonright M=X_{f}}\operatorname*{\bigotimes}_{s\in
Y}(p_{i_{1}}^{s(i_{1})}\wedge\dots\dots
p_{i_{k}}^{s(i_{k})}\wedge\mathop{\mbox{\small\rm NE}})\quad(\text{since
dom}(X_{f})=M)\end{array}$

$\dashv$

We now prove Lemma 5.5 by induction on $\phi(p_{i_{1}},\dots,p_{i_{n}})$.

Case $\phi(p_{i_{1}},\dots,p_{i_{n}})=p_{i_{k}}$. We prove that
$p_{i_{k}}\dashv\vdash\bot\vee(p_{i_{k}}\wedge\mathop{\mbox{\small\rm NE}}).$
For $p_{i_{k}}\vdash\bot\vee(p_{i_{k}}\wedge\mathop{\mbox{\small\rm NE}})$, we
have the following derivation:

$\begin{array}[]{rll}(1)&p_{i_{k}}\\\ (2)&\bot\vee\mathop{\mbox{\small\rm
NE}}&\text{($\mathop{\mbox{\small\rm NE}}\textsf{I}$)}\\\
(3)&\big{(}p_{i_{k}}\wedge\bot\big{)}\vee(p_{i_{k}}\wedge\mathop{\mbox{\small\rm
NE}})&\text{((1), (2), $\wedge\textsf{I}$, $\textsf{Dstr}$)}\\\
(4)&\bot\vee(p_{i_{k}}\wedge\mathop{\mbox{\small\rm
NE}})&\text{($\wedge\textsf{E}$)}\end{array}$

Conversely, for $\bot\vee(p_{i_{k}}\wedge\mathop{\mbox{\small\rm NE}})\vdash
p_{i_{k}}$, we have the following derivation

$\begin{array}[]{rll}(1)&\bot\vee(p_{i_{k}}\wedge\mathop{\mbox{\small\rm
NE}})\\\ (2)&p_{i_{k}}\vee p_{i_{k}}&\text{($\it{\textsf{ex falso}}^{-}$,
$\wedge\textsf{E}$)}\\\ (3)&p_{i_{k}}&\text{($\vee\textsf{E}$)}\end{array}$

By the Claim, the formula $p_{i_{k}}$ is provably equivalent to a formula
$\theta(p_{i_{1}},\dots,p_{i_{n}})$ in the normal form.

Case $\phi(p_{i_{1}},\dots,p_{i_{n}})=\neg p_{i_{k}}$. Similar to the above
case.

Case $\phi(p_{i_{1}},\dots,p_{i_{n}})=\mathop{\mbox{\small\rm NE}}$. Note that
$\mathop{\mbox{\small\rm NE}}$ is a formula with no propositional variable,
but for the sake of the inductive proof, we need to prove the theorem for
$\mathop{\mbox{\small\rm NE}}$ viewed as $\mathop{\mbox{\small\rm
NE}}(p_{i_{1}},\dots,p_{i_{n}})$, a formula whose propositional variables are
among $p_{i_{1}},\dots,p_{i_{n}}$. By the claim, it suffices to derive the
normal form for $\mathop{\mbox{\small\rm NE}}$ when it is viewed as
$\mathop{\mbox{\small\rm NE}}(p_{i_{1}})$. We prove that
$\mathop{\mbox{\small\rm NE}}\dashv\vdash\theta$, where

$\theta:=(p_{i_{1}}\wedge\mathop{\mbox{\small\rm NE}})\vee(\neg
p_{i_{1}}\wedge\mathop{\mbox{\small\rm
NE}})\vee\big{(}(p_{i_{1}}\wedge\mathop{\mbox{\small\rm NE}})\otimes(\neg
p_{i_{1}}\wedge\mathop{\mbox{\small\rm NE}})\big{)}.$

For $\mathop{\mbox{\small\rm NE}}\vdash\theta$, we have the following
derivation:

$\begin{array}[]{rll}(1)&\mathop{\mbox{\small\rm NE}}\\\
(2)&\mathop{\mbox{\small\rm NE}}\wedge(p_{i_{1}}\otimes\neg
p_{i_{1}})&\text{($\textsf{EM}_{0}$, $\wedge\textsf{I}$)}\\\
(3)&(p_{i_{1}}\wedge\mathop{\mbox{\small\rm NE}})\vee(\neg
p_{i_{1}}\wedge\mathop{\mbox{\small\rm
NE}})\vee\big{(}(p_{i_{1}}\wedge\mathop{\mbox{\small\rm NE}})\otimes(\neg
p_{i_{1}}\wedge\mathop{\mbox{\small\rm NE}})\big{)}&\text{($\textsf{Dstr}$
\,$\mathop{\mbox{\small\rm NE}}\wedge\otimes$)}\end{array}$

For the other direction $\theta\vdash\mathop{\mbox{\small\rm NE}}$, we have
the following derivation:

$\begin{array}[]{rll}(1)&(p_{i_{1}}\wedge\mathop{\mbox{\small\rm
NE}})\vee(\neg p_{i_{1}}\wedge\mathop{\mbox{\small\rm
NE}})\vee\big{(}(p_{i_{1}}\wedge\mathop{\mbox{\small\rm NE}})\otimes(\neg
p_{i_{1}}\wedge\mathop{\mbox{\small\rm NE}})\big{)}\\\
(2)&(p_{i_{1}}\wedge\mathop{\mbox{\small\rm NE}})\vee(\neg
p_{i_{1}}\wedge\mathop{\mbox{\small\rm NE}})\vee\big{(}(p_{i_{1}}\otimes\neg
p_{i_{1}})\wedge\mathop{\mbox{\small\rm
NE}}\big{)}&\text{($\textsf{Dstr}^{\ast}\\!$ $\wedge\otimes\wedge$)}\\\
(3)&\mathop{\mbox{\small\rm NE}}\vee\mathop{\mbox{\small\rm
NE}}\vee\mathop{\mbox{\small\rm NE}}&\text{($\wedge\textsf{E}$)}\\\
(4)&\mathop{\mbox{\small\rm NE}}&\text{($\vee\textsf{E}$)}\end{array}$

Case $\phi(p_{i_{1}},\dots,p_{i_{n}})=\bot$. Trivially
$\bot\dashv\vdash\Theta^{\ast}_{\emptyset}=\bot$.

Case
$\phi(p_{i_{1}},\dots,p_{i_{n}})=\psi(p_{i_{1}},\dots,p_{i_{n}})\vee\chi(p_{i_{1}},\dots,p_{i_{n}})$.
By the induction hypothesis, we have

$\psi\dashv\vdash\operatorname*{\bigvee}_{f\in F}\Theta^{\ast}_{X_{f}}\text{
and }\chi\dashv\vdash\operatorname*{\bigvee}_{g\in G}\Theta^{\ast}_{X_{g}},$
(10)

where each $X_{f},X_{g}\subseteq 2^{N}$. Then it follows from the rules
$\vee\textsf{E}$ and $\vee\textsf{I}$ that

$\psi\vee\chi\dashv\vdash\operatorname*{\bigvee}_{f\in
F}\Theta_{X_{f}}^{\ast}\vee\operatorname*{\bigvee}_{g\in
G}\Theta_{X_{g}}^{\ast}.$

If $\psi\dashv\vdash\bot\wedge\mathop{\mbox{\small\rm NE}}$ (i.e.,
$F=\emptyset$), then we obtain further by $\it{\textsf{ex falso}}^{+}$,
$\vee\textsf{E}$ and $\vee\textsf{I}$ that
$\psi\vee\chi\dashv\vdash\operatorname*{\bigvee}_{g\in
G}\Theta_{X_{g}}^{\ast}$. Similarly for the case
$\chi\dashv\vdash\bot\wedge\mathop{\mbox{\small\rm NE}}$.

Case
$\phi(p_{i_{1}},\dots,p_{i_{n}})=\psi(p_{i_{1}},\dots,p_{i_{n}})\otimes\chi(p_{i_{1}},\dots,p_{i_{n}})$.
By the induction hypothesis, we have (10). If
$\psi\dashv\vdash\bot\wedge\mathop{\mbox{\small\rm NE}}$ (i.e.,
$F=\emptyset$), then we derive
$\psi\otimes\chi\dashv\vdash\bot\wedge\mathop{\mbox{\small\rm
NE}}=\operatorname*{\bigvee}\emptyset$ by ($\mathbf{0}\textsf{Ctr}$) and
($\it{\textsf{ex falso}}^{+}$). Similarly for the case
$\chi\dashv\vdash\bot\wedge\mathop{\mbox{\small\rm NE}}$ (i.e.,
$G=\emptyset$).

Now, assume $F,G\neq\emptyset$. We show that
$\psi\otimes\chi\dashv\vdash\theta$, where

$\theta:=\operatorname*{\bigvee}_{f\in F}\operatorname*{\bigvee}_{g\in
G}\Theta^{\ast}_{X_{f}\cup X_{g}}.$

For the direction $\psi\otimes\chi\vdash\theta$, we have the following
derivation:

$\begin{array}[]{rll}(1)&\psi\otimes\chi\\\
(2)&\displaystyle\Big{(}\operatorname*{\bigvee}_{f\in
F}\Theta^{\ast}_{X_{f}}\Big{)}\otimes\Big{(}\operatorname*{\bigvee}_{g\in
G}\Theta^{\ast}_{X_{g}}\Big{)}\\\
(3)&\displaystyle\operatorname*{\bigvee}_{f\in F}\operatorname*{\bigvee}_{g\in
G}\left(\Theta^{\ast}_{X_{f}}\otimes\Theta^{\ast}_{X_{g}}\right)&\text{($\textsf{Dstr}$
$\otimes\vee$)}\\\ (4)&\displaystyle\operatorname*{\bigvee}_{f\in
F}\operatorname*{\bigvee}_{g\in G}\Theta^{\ast}_{X_{f}\cup
X_{g}}&(\otimes\textsf{E}^{-},\otimes\textsf{Sub}^{-})\end{array}$

The other direction $\theta\vdash\psi\otimes\chi$ is proved similarly using
$\otimes\textsf{W}$ and $\textsf{Dstr}\otimes\vee\otimes$.

Case
$\phi(p_{i_{1}},\dots,p_{i_{n}})=\psi(p_{i_{1}},\dots,p_{i_{n}})\wedge\chi(p_{i_{1}},\dots,p_{i_{n}})$.
By the induction hypothesis, we have (10). If
$\psi\dashv\vdash\bot\wedge\mathop{\mbox{\small\rm NE}}$ (i.e.,
$F=\emptyset$), then we derive
$\psi\wedge\chi\dashv\vdash\bot\wedge\mathop{\mbox{\small\rm
NE}}=\operatorname*{\bigvee}\emptyset$ by ($\wedge\textsf{E}$) and
($\it{\textsf{ex falso}}^{+}$). Similarly for the case
$\chi\dashv\vdash\bot\wedge\mathop{\mbox{\small\rm NE}}$ (i.e.,
$G=\emptyset$).

Now, assume $F,G\neq\emptyset$. We show that
$\psi\wedge\chi\dashv\vdash\theta$, where

$\theta:=\operatorname*{\bigvee}_{h\in H}\Theta^{\ast}_{X_{h}}\text{ and
}\\{X_{f}\mid f\in F\\}\cap\\{X_{g}\mid g\in G\\}=\\{X_{h}\mid h\in H\\}.$

For $\psi\wedge\chi\vdash\theta$, we have the following derivation:

$\begin{array}[]{rll}(1)&\psi\wedge\chi\\\
(2)&\displaystyle\Big{(}\operatorname*{\bigvee}_{f\in
F}\Theta^{\ast}_{X_{f}}\Big{)}\wedge\Big{(}\operatorname*{\bigvee}_{g\in
G}\Theta^{\ast}_{X_{g}}\Big{)}\\\
(3)&\displaystyle\operatorname*{\bigvee}_{f\in F}\operatorname*{\bigvee}_{g\in
G}\left(\Theta^{\ast}_{X_{f}}\wedge\Theta^{\ast}_{X_{g}}\right)\\\
(4)&\displaystyle\Big{(}\mathop{\operatorname*{\bigvee}_{(f,g)\in F\times
G}}_{X_{f}\neq
X_{g}}\left(\Theta^{\ast}_{X_{f}}\wedge\Theta^{\ast}_{X_{g}}\right)\Big{)}\vee\Big{(}\mathop{\operatorname*{\bigvee}_{(f,g)\in
F\times
G}}_{X_{f}=X_{g}}\left(\Theta^{\ast}_{X_{f}}\wedge\Theta^{\ast}_{X_{g}}\right)\Big{)}\\\
\end{array}$
$\begin{array}[]{rll}(5)&\displaystyle\big{(}\bot\wedge\mathop{\mbox{\small\rm
NE}}\big{)}\vee\mathop{\operatorname*{\bigvee}_{(f,g)\in F\times
G}}_{X_{f}=X_{g}}\left(\Theta^{\ast}_{X_{f}}\wedge\Theta^{\ast}_{X_{g}}\right)&(\mathbf{0}\textsf{I})\\\
(6)&\displaystyle\mathop{\operatorname*{\bigvee}_{(f,g)\in F\times
G}}_{X_{f}=X_{g}}\left(\Theta^{\ast}_{X_{f}}\wedge\Theta^{\ast}_{X_{g}}\right)&(\mathbf{0}\textsf{E})\\\
(7)&\displaystyle\operatorname*{\bigvee}_{h\in
H}\Theta^{\ast}_{X_{h}}&(\wedge\textsf{E},\vee\textsf{E})\end{array}$

For the other direction $\theta\vdash\psi\wedge\chi$, we have the following
derivation:

$\begin{array}[]{rll}(1)&\displaystyle\operatorname*{\bigvee}_{h\in
H}\Theta^{\ast}_{X_{h}}\\\
(2)&\displaystyle\Big{(}\operatorname*{\bigvee}_{h\in
H}\Theta^{\ast}_{X_{h}}\Big{)}\wedge\Big{(}\operatorname*{\bigvee}_{h\in
H}\Theta^{\ast}_{X_{h}}\Big{)}&(\wedge\textsf{I})\\\
(3)&\displaystyle\Big{(}\operatorname*{\bigvee}_{f\in
F}\Theta^{\ast}_{X_{f}}\Big{)}\wedge\Big{(}\operatorname*{\bigvee}_{g\in
G}\Theta^{\ast}_{X_{g}}\Big{)}&(\text{$\vee\textsf{I}$, $H\subseteq F,G$})\\\
(4)&\displaystyle\psi\wedge\chi\end{array}$

∎

###  5.2 $\mathbf{CPL^{+}}$

We will give a complete axiomatization of $\mathbf{CPL^{+}}$ in the style of
natural deduction. For this end, let us review our proof above of the
Completeness Theorem for $\mathbf{PT}^{+}$. In a crucial step of the proof we
transformed a formula into its disjunctive normal form $\bigvee_{f\in
F}\Theta^{\ast}_{X_{f}}$. Each disjunct $\Theta^{\ast}_{X_{f}}$ is a formula
in the language of $\mathbf{CPL^{+}}$, but $\mathbf{CPL^{+}}$ is a fragment of
$\mathbf{PT}^{+}$ that does not have the Boolean disjunction $\vee$ in the
language, so we seem to be in trouble. Our trick is that we view the set
$\\{\Theta^{\ast}_{X_{f}}\mid f\in F\\}$ of formulas, rather than the
disjunction of this set, as a _weak_ normal form for formulas in the language
of $\mathbf{CPL^{+}}$. On the basis of this plan, we can axiomatize
$\mathbf{CPL^{+}}$ and prove the completeness theorem.

We will define a natural deduction system of $\mathbf{CPL^{+}}$ in which every
formula $\phi$ is essentially provably equivalent to its disjunctive normal
form $\bigvee_{f\in F}\Theta^{\ast}_{X_{f}}$. In particular, we will be able
to essentially derive the provable equivalence between the non-emptiness
$\mathop{\mbox{\small\rm NE}}$ and its disjunctive normal form
$\bigvee_{\emptyset\neq Y\subseteq 2^{N}}\Theta^{\ast}_{Y}$. The behavior of
the usual Introduction Rule and Elimination Rule of the Boolean disjunction
$\vee$ ($\vee\textsf{I}$ and $\vee\textsf{E}$) will be simulated by two Strong
Elimination Rules ($\textsf{SE}_{1}$ and $\textsf{SE}_{2}$) that do not
involve $\vee$.

To define the Strong Elimination Rules, we will need to specify a particular
occurrence of a subformula inside a formula. For this purpose, we identify a
formula in the language of $\mathbf{CPL^{+}}$ with a finite string of symbols.
A propositional variable $p_{i}$ and the non-emptiness
$\mathop{\mbox{\small\rm NE}}$ are symbols and the other symbols are
$\wedge,\otimes,\neg$. Starting from the leftmost symbol, we number each
symbol in a formula with a positive integer, as in the following example:

$\mathop{\mbox{\small\rm NE}}$ | $\otimes$ | $($ | $\neg$ | $p_{1}$ | $\wedge$ | $\mathop{\mbox{\small\rm NE}}$ | $)$
---|---|---|---|---|---|---|---
1 | 2 | 3 | 4 | 5 | 6 | 7 | 8

If the $m$th symbol of a formula $\phi$ starts a string $\psi$ which is a
subformula of $\phi$, we denote the subformula $[\psi,m]_{\phi}$, or simply
$[\psi,m]$. We will sometimes refer to an occurrence of a formula $\chi$
inside a subformula $\psi$ of $\phi$. In this case we will use the same
counting for the subformula $\psi$, rather than restart the counting from $1$.
We write $\phi(\beta/[\alpha,m])$ for the formula obtained from $\phi$ by
replacing the occurrence of the subformula $[\alpha,m]$ by $\beta$. For
example, for the formula $\phi=\mathop{\mbox{\small\rm NE}}\otimes(\neg
p_{1}\wedge\mathop{\mbox{\small\rm NE}})$, the second occurrence of the non-
emptiness $\mathop{\mbox{\small\rm NE}}$ is denoted by
$[\mathop{\mbox{\small\rm NE}},7]$, and the same notation also designates the
occurrence of $\mathop{\mbox{\small\rm NE}}$ inside the subformula $\neg
p_{1}\otimes\mathop{\mbox{\small\rm NE}}$. The notation
$\phi(\psi/[\mathop{\mbox{\small\rm NE}},7])$ designates the formula
$\mathop{\mbox{\small\rm NE}}\otimes(\neg p_{1}\wedge\psi)$.

Below we present the natural deduction system of $\mathbf{CPL^{+}}$.

######  Definition 5.8 (A natural deduction system of $\mathbf{CPL^{+}}$).

AXIOM
---
Atomic excluded middle
$\textsf{EM}_{0}$ $p_{i}\otimes\neg p_{i}$

RULES
---
All of the rules in Definition 5.1 that do not involve Boolean disjunction,
i.e., the rules $\wedge\textsf{I}$, $\wedge\textsf{E}$,
$\otimes\textsf{I}^{-}$, $\otimes\textsf{W}$, $\otimes\textsf{E}^{-}$,
$\otimes\textsf{Sub}^{-}$, Com $\otimes$, Ass $\otimes$, $\bot\textsf{I}$,
$\mathbf{\bot}\textsf{E}$, $\it{\textsf{ex falso}}^{+}$,
$\mathbf{0}\textsf{I}$, $\mathbf{0}\textsf{Ctr}$, $\textsf{Dstr}^{\ast}\\!$
$\wedge\otimes$.
Strong elimination rules
$D_{0}$ $\phi$ [$\phi(\Theta^{\ast}_{Y_{1}}/[\mathop{\mbox{\small\rm
NE}},m])$] $D_{1}$ $\theta$ $\ldots$
[$\phi(\Theta^{\ast}_{Y_{k}}/[\mathop{\mbox{\small\rm NE}},m])$] $D_{k}$
$\theta$ $\textsf{SE}_{1}$ $\theta$
where $\\{Y_{1},\dots,Y_{k}\\}$ is the set of all nonempty teams on a set $N$
of indices
$D_{0}$ $\phi$ [$\phi(\psi\wedge\bot/[\psi,m])$] $D_{1}$ $\theta$
[$\phi(\psi\wedge\mathop{\mbox{\small\rm NE}}/[\psi,m])$] $D_{2}$ $\theta$
$\textsf{SE}_{2}$ $\theta$

All rules that do not involve the Boolean disjunction $\vee$ in the natural
deduction system of $\mathbf{PT}^{+}$ (Definition 5.1) are included in the
above system. Thus all clauses in Proposition 5.2 that do not involve $\vee$
are also derivable in the above system.

Let us ponder why we define the Strong Elimination Rules the way they are in
our system in the absence of the Boolean disjunction $\vee$. The idea of the
elimination rules for the conjunction is simply that if we have inferred
$\phi\wedge\psi$, we can infer both $\phi$ and $\psi$. The elimination rule
for disjunction in classical logic is that if we have $\phi\vee\psi$ and we
can derive $\theta$ separately from both $\phi$ and $\psi$ then we have
$\theta$. In both cases the elimination rule builds into the syntax of the
proof the semantics of the logical operation. This is roughly the general idea
of natural deduction, due to Gentzen. We followed the same line of thinking
when we introduce our rules for Boolean disjunction $\vee$ in the system for
$\mathbf{PT}^{+}$. Now, we moved to the weak logic $\mathbf{CPL^{+}}$ which
does not have Boolean disjunction in the language. But still, the non-
emptiness $\mathop{\mbox{\small\rm NE}}$ is semantically equivalent to the
formula $\bigvee_{i=1}^{k}\Theta^{\ast}_{Y_{i}}$ (in the language of
$\mathbf{PT}^{+}$), where $\\{Y_{1},\dots,Y_{k}\\}$ is the set of all nonempty
teams on a set $N$ of indices. To derive a formula $\theta$ from
$\mathop{\mbox{\small\rm NE}}$ given some assumptions, in $\mathbf{PT}^{+}$ in
the presence of the Boolean disjunction we could build up the following
derivation:

$D_{0}$ $\mathop{\mbox{\small\rm NE}}$
$\bigvee_{i=1}^{k}\Theta^{\ast}_{Y_{i}}$ [$\Theta^{\ast}_{Y_{1}}$] $D_{1}$
$\theta$ $\ldots$ [$\Theta^{\ast}_{Y_{k}}$] $D_{k}$ $\theta$ $\theta$

Evidently such a derivation can be simulated in our deduction system of
$\mathbf{CPL^{+}}$ using the rule $\textsf{SE}_{1}$. More generally, a formula
$\phi$ whose $n$th symbol is $\mathop{\mbox{\small\rm NE}}$ is semantically
equivalent to the formula
$\phi(\bigvee_{i=1}^{k}\Theta^{\ast}_{Y_{i}}/[\mathop{\mbox{\small\rm
NE}},m])$ (in the language of $\mathbf{PT}^{+}$), which, as $\vee$ distributes
over all connectives, is semantically equivalent to
$\bigvee_{i=1}^{k}\phi(\Theta^{\ast}_{Y_{i}}/[\mathop{\mbox{\small\rm
NE}},m])$. In the same way, to derive a formula $\theta$ from $\phi$ given
some assumptions, it suffices to derive $\theta$ from each
$\phi(\Theta^{\ast}_{Y_{i}}/[\mathop{\mbox{\small\rm NE}},m])$. This is
exactly what the Strong Elimination Rule $\textsf{SE}_{1}$ characterizes.
Analogously, the rule $\textsf{SE}_{2}$ characterizes the equivalence between
a formula $\phi$ and $\phi(\psi\wedge(\bot\vee\mathop{\mbox{\small\rm
NE}})/[\psi,m])$.

We now prove the Soundness Theorem for the deduction system of
$\mathbf{CPL^{+}}$.

######  Theorem 5.9 (Soundness Theorem).

For any set $\Gamma\cup\\{\phi\\}$ of formulas in the language of
$\mathbf{CPL^{+}}$, we have
$\Gamma\vdash\phi\,\Longrightarrow\,\Gamma\models\phi.$

###### Proof.

We show that for each derivation $D$ with the conclusion $\phi$ and the
hypotheses in $\Gamma$ we have $\Gamma\models\phi$. We only verify the cases
where the Strong Elimination Rules are applied. The other cases follow from
the Soundness Theorem for $\mathbf{PT}^{+}$.

$\textsf{SE}_{1}$: Put
$\phi^{\ast}_{i}=\phi(\Theta^{\ast}_{Y_{i}}/[\mathop{\mbox{\small\rm NE}},m])$
for each $i\in\\{1,\dots,k\\}$. Assume that $D_{0},D_{1},\dots,D_{k}$ are
derivations for $\Pi_{0}\vdash\phi$, $\Pi_{1},\phi^{\ast}_{1}\vdash\theta$, …,
$\Pi_{k},\phi^{\ast}_{k}\vdash\theta$, respectively. We show that
$\Pi_{0},\Pi_{1},\dots,\Pi_{k}\models\theta$ follows from the induction
hypothesis $\Pi_{0}\models\phi$, $\Pi_{1},\phi^{\ast}_{1}\models\theta$, …,
$\Pi_{k},\phi^{\ast}_{k}\models\theta$. This reduces to showing that
$\phi\models\phi^{\ast}_{1}\vee\dots\vee\phi^{\ast}_{k}$ by induction on the
subformulas $\psi$ of $\phi$.

Case $\psi=\mathop{\mbox{\small\rm NE}}$. By the locality property,
$X\models\mathop{\mbox{\small\rm NE}}\iff X\upharpoonright
N\models\mathop{\mbox{\small\rm NE}}$ for any team $X$. Now, since
$\\{Y_{1},\dots,Y_{k}\\}$ is the set of all nonempty teams on $N$, we have
$X\upharpoonright N\models\mathop{\mbox{\small\rm NE}}\iff X\upharpoonright
N\models\Theta^{\ast}_{Y_{i}}$ for some $i\in\\{1,\dots,k\\}$. Hence
$\mathop{\mbox{\small\rm
NE}}\models\Theta^{\ast}_{Y_{1}}\vee\dots\vee\Theta^{\ast}_{Y_{k}}$.

If $\psi$ is $p_{j}$ or $\neg p_{j}$, then $\psi^{\ast}_{i}=\psi$ for each
$i\in\\{1,\dots,k\\}$ and
$\psi\models\psi^{\ast}_{1}\vee\dots\vee\psi^{\ast}_{k}$ holds trivially.

If $\psi=\theta\otimes\chi$ and without loss of generality we assume that the
occurrence of the $\mathop{\mbox{\small\rm NE}}$ is in the subformula
$\theta$. Then by the induction hypothesis we have
$\theta\models\theta^{\ast}_{1}\vee\dots\vee\theta^{\ast}_{k}$. Thus
$\theta\otimes\chi\models(\theta^{\ast}_{1}\vee\dots\vee\theta^{\ast}_{k})\otimes\chi\models(\theta^{\ast}_{1}\otimes\chi)\vee\dots\vee(\theta^{\ast}_{k}\otimes\chi)$.

The case $\psi=\theta\wedge\chi$ is proved similarly.

$\textsf{SE}_{2}$: Put $\phi^{\ast}_{+}=\phi(\psi\wedge\mathop{\mbox{\small\rm
NE}}/[\psi,m])$ and $\phi^{\ast}_{-}=\phi(\psi\wedge\bot/[\psi,m])$. Assume
that $D_{0},D_{1}$ and $D_{2}$ are derivations for $\Pi_{0}\vdash\phi$,
$\Pi_{1},\phi^{\ast}_{+}\vdash\theta$ and
$\Pi_{2},\phi^{\ast}_{-}\vdash\theta$, respectively. We show that
$\Pi_{0},\Pi_{1},\Pi_{2}\models\theta$ follows from the induction hypothesis
$\Pi_{0}\models\phi$, $\Pi_{1},\phi^{\ast}_{+}\models\theta$ and
$\Pi_{2},\phi^{\ast}_{-}\models\theta$. This is reduced to showing that
$\phi\models\phi^{\ast}_{+}\vee\phi^{\ast}_{-}$ by induction on the
subformulas $\delta$ of $\phi$.

If $\delta$ is an atom and $\delta\neq[\psi,m]$, then
$\delta^{\ast}_{+}=\delta=\delta^{\ast}_{-}$ and
$\delta\models\delta^{\ast}_{+}\vee\delta^{\ast}_{-}$ holds trivially.

If $\delta=[\psi,m]$, then
$\delta^{\ast}_{+}=\delta\wedge\mathop{\mbox{\small\rm NE}}$ and
$\delta^{\ast}_{-}=\delta\wedge\bot$. Since $\models\mathop{\mbox{\small\rm
NE}}\vee\bot$, we have $\delta\models\delta\wedge(\mathop{\mbox{\small\rm
NE}}\vee\bot)\models(\delta\wedge\mathop{\mbox{\small\rm
NE}})\vee(\delta\wedge\bot)$.

The induction steps are proved analogously to the $\textsf{SE}_{1}$ case. ∎

In the remainder of this section we prove the Completeness Theorem for our
system. This proof is similar to the completeness proof for $\mathbf{PD}$ that
we gave in [34]. The reader may compare this section with Section 4.3 in [34].
When proving the Completeness Theorem for the deduction system of
$\mathbf{PT}^{+}$, we transformed a formula into its disjunctive normal form.
Here in $\mathbf{CPL^{+}}$ we follow essentially the same idea. But in the
absence of the Boolean disjunction we will not be able to express the relevant
disjunctive normal form in the logic. Instead, we work with the weak normal
form (i.e., the set of all disjuncts of a disjunctive normal form) and the
behavior of the (strong) normal form can be simulated by using the Strong
Elimination Rules $\textsf{SE}_{1}$ and $\textsf{SE}_{2}$. The disjuncts of
the disjunctive normal of a formula (or elements in the weak normal form) can
be obtained from what we call _strong realizations_. Our strong realizations
are analogues of the “resolutions” in [4], and they are more complex than the
“(weak) realizations” we defined in [34]. These strong realizations will play
a crucial role in our argument. Let us now define this notion formally.

Let $\alpha\in\\{p_{i},\neg p_{i},\mathop{\mbox{\small\rm NE}},\bot\\}$ be an
atom and $Y\subseteq 2^{N}$ a team on a set $N$ of indices such that
$Y\models\alpha$. A _strong realization_ $\alpha^{\ast}_{Y}$ of $\alpha$ over
$Y$ is defined as

$\alpha^{\ast}_{Y}:=\Theta^{\ast}_{Y}.$

Let $o=\langle[\alpha_{1},m_{1}],\,\dots,\,[\alpha_{c},m_{c}]\rangle$ be a
sequence of some of the occurrences of atoms in a formula $\phi$ in the
language of $\mathbf{CPL^{+}}$. A _strongly realizing sequence of $\phi$ over
$o$_ is a sequence $\Omega=\langle Y_{1},\dots,Y_{c}\rangle$ such that
$Y_{i}\models\alpha_{i}$ for each $i\in\\{1,\dots,c\\}$. We call the formula
$\phi_{\Omega}^{\ast}$ defined as follows a _strong realization of $\phi$ over
$o$_:

$\phi_{\langle
Y_{1},\dots,Y_{c}\rangle}^{\ast}:=\phi((\alpha_{1})_{Y_{1}}^{\ast}/[\alpha_{1},m_{1}],\dots,(\alpha_{c})_{Y_{c}}^{\ast}/[\alpha_{c},m_{c}]).$

Let $O$ be the sequence of all occurrences of all atoms in $\phi$. A strongly
realizing sequence of $\phi$ over $O$ is called a _maximal strongly realizing
sequence_. A strong realization $\phi^{\ast}_{\Omega}$ over $O$ is called a
_strong realization_ of $\phi$.

For example, consider the formula $\phi=\mathop{\mbox{\small\rm
NE}}\otimes(\neg p_{1}\wedge\mathop{\mbox{\small\rm NE}})$. Let $Y_{1}$ and
$Y_{2}$ be two nonempty teams and $X=\\{\\{(1,0)\\}\\}$ a team on $\\{1\\}$.
Over $o=\langle[\mathop{\mbox{\small\rm NE}},7]\rangle$ the sequence $\langle
Y_{1}\rangle$ is a strongly realizing sequence of $\phi$ and the formula
$\mathop{\mbox{\small\rm NE}}\otimes(\neg p_{1}\wedge\mathop{\mbox{\small\rm
NE}}^{\ast}_{Y_{1}})$ is a strong realization of $\phi$. Both
$\mathop{\mbox{\small\rm NE}}^{\ast}_{Y_{1}}\otimes((\neg
p_{1})^{\ast}_{X}\wedge\mathop{\mbox{\small\rm NE}}^{\ast}_{Y_{2}})$ and
$\mathop{\mbox{\small\rm NE}}^{\ast}_{Y_{2}}\otimes((\neg
p_{1})^{\ast}_{X}\wedge\mathop{\mbox{\small\rm NE}}^{\ast}_{Y_{1}})$ are
strong realizations of $\phi$. Note that a formula always has at least one
atom, so its maximal strongly realizing sequence is always a nonempty
sequence.

In the next lemma we prove that every formula is semantically equivalent to
the Boolean disjunction of all of its strong realizations over an arbitrary
sequence of some occurrences of atoms, particularly of all its maximal
strongly realizing sequences.

######  Lemma 5.10.

Let $\phi$ be a formula in the language of $\mathbf{CPL^{+}}$ and $\Lambda$
the set of its strongly realizing sequences over a sequence $o$. Then
$\displaystyle\phi\equiv\operatorname*{\bigvee}_{\Omega\in\Lambda}\phi^{\ast}_{\Omega}.$

###### Proof.

We prove the lemma by induction on the subformulas $\psi$ of $\phi$. Let $N$
be the set of indices of propositional variables occurring in $\phi$.

Base case: $\psi$ is an atom. If the occurrence of $\psi$ is not listed in
$o$, then $\psi^{\ast}_{\Omega}=\psi$ for all $\Omega\in\Lambda$ and
$\psi\equiv\bigvee_{\Omega\in\Lambda}\psi^{\ast}_{\Omega}$ holds trivially.
Otherwise, the occurrence $\psi=[\psi,m_{i}]$ is in $o$ and the set
$\mathcal{Y}=\\{Y_{i}\mid\langle Y_{1},\dots,Y_{c}\rangle\in\Lambda\\}$
consists of all teams on $N$ that satisfy $\psi$. For any team $X$ on $N$, by
Lemma 5.4 we have $X\models\psi\iff X\in\mathcal{Y}\iff
X\models\bigvee_{Y\in\mathcal{Y}}\Theta^{\ast}_{Y}\iff
X\models\bigvee_{\Omega\in\Lambda}\psi^{\ast}_{\Omega}$.

The induction case $\psi=\theta\otimes\chi$ follows from the induction
hypothesis and the fact that $[\,A\models A^{\prime}\text{ and }B\models
B^{\prime}\,]\Longrightarrow A\otimes B\models A^{\prime}\otimes B^{\prime}$
and that $A\otimes(B\vee C)\models(A\otimes B)\vee(A\otimes C)$ for all
formulas $A,B,C$. Analogously for the case $\psi=\theta\wedge\chi$. ∎

We will show that in our system one derives essentially the equivalence
between a formula $\phi$ and the Boolean disjunction
$\operatorname*{\bigvee}_{\Omega\in\Lambda}\phi^{\ast}_{\Omega}$ of its strong
realizations over some sequence of occurrences of atoms. We first prove the
direction that $\phi$ follows from
$\operatorname*{\bigvee}_{\Omega\in\Lambda}\phi^{\ast}_{\Omega}$, which is
simulated in our system by the derivation that each Boolean disjunct
$\phi^{\ast}_{\Omega}$ implies $\phi$.

######  Lemma 5.11.

If $\Omega$ is a strongly realizing sequence of a formula $\phi$ in the
language of $\mathbf{CPL^{+}}$ over a sequence of some occurrences of atoms in
$\phi$, then $\phi^{\ast}_{\Omega}\vdash\phi$.

###### Proof.

We derive the lemma by induction on the subformulas $\psi$ of $\phi$. Let
$N=\\{i_{1},\dots,i_{n}\\}$ be the set of indices of propositional variables
occurring in $\phi$.

The induction step is left to the reader. We only check the basic case when
$\psi$ is an atom. If the occurrence of $\psi$ is not listed in $o$, then
$\psi^{\ast}_{\Omega}=\psi$ and the statment holds trivially. Now, assume
otherwise. Then $\psi^{\ast}_{\Omega}=\Theta^{\ast}_{X}$ and $X$ is a team on
$N$ that satisfies $\psi$. If $\psi=\bot$, then $X=\emptyset$ and
$\Theta^{\ast}_{\emptyset}=\bot$. Thus $\psi^{\ast}_{\Omega}\vdash\bot$ holds
trivially. If $\psi=p_{i_{k}}$ and $X=\emptyset$, then
$\Theta^{\ast}_{\emptyset}=\bot\vdash p_{i_{k}}$ follows from $\it{\textsf{ex
falso}}^{-}$. If $X\neq\emptyset$, then we have $s(i_{k})=1$ for all $s\in X$
and we derive $\Theta^{\ast}_{X}\vdash p_{i}$ as follows:

$\begin{array}[]{rll}(1)&\displaystyle\operatorname*{\bigotimes}_{s\in
X}(p_{i_{1}}^{s(i_{1})}\wedge\dots\wedge p_{i_{k-1}}^{s(i_{k-1})}\wedge
p_{i_{k}}\wedge p_{i_{k+1}}^{s(i_{k+1})}\wedge\dots\wedge
p_{i_{n}}^{s(i_{n})}\wedge\mathop{\mbox{\small\rm NE}})\\\
(3)&\displaystyle\operatorname*{\bigotimes}_{s\in
X}p_{i_{k}}&(\wedge\textsf{E},\otimes\textsf{Sub}^{-})\\\
(4)&p_{i_{k}}&(\otimes\textsf{E}^{-})\end{array}$

The case $\psi=\neg p_{i_{k}}$ is proved analogously. If
$\psi=\mathop{\mbox{\small\rm NE}}$, then $X\neq\emptyset$ and
$\Theta^{\ast}_{X}\vdash\mathop{\mbox{\small\rm NE}}$ is derived by a similar
argument. ∎

Next, we turn to prove that the Boolean disjunction
$\operatorname*{\bigvee}_{\Omega\in\Lambda}\phi^{\ast}_{\Omega}$ of the strong
realizations of some formula $\phi$ over some sequence $o$ of occurrences of
atoms follows essentially from $\phi$. Following the idea we used when we
defined the Strong Elimination Rules, we simulate the derivation by proving in
our system that a formula $\theta$ follows from $\phi$, given that $\theta$
follows from each $\phi^{\ast}_{\Omega}$. We prove this in steps. First of
all, if $o$ is a sequence of one occurrence of the non-emptiness
$\mathop{\mbox{\small\rm NE}}$, then the statement follows by applying the
$\textsf{SE}_{1}$ rule. We now generalize this result and show that the
statement holds if $o$ is a sequence of one occurrence of any atom.

######  Lemma 5.12.

If $\delta\vdash\theta$, then
$\phi(\delta/[\psi,m])\vdash\phi(\theta/[\psi,m])$.

###### Proof.

We prove the lemma by induction on the subformulas $\chi$ of $\phi$.

If $\chi$ is an atom and $\chi\neq[\psi,m]$, then
$\chi(\delta/[\psi,m])=\chi=\chi(\theta/[\psi,m])$ and trivially
$\chi(\delta/[\psi,m])\vdash\chi(\theta/[\psi,m])$.

If $\chi=[\psi,m]$, then $\chi(\delta/[\psi,m])=\delta$ and
$\chi(\theta/[\psi,m])=\theta$. Thus
$\chi(\delta/[\psi,m])\vdash\chi(\theta/[\psi,m])$ follows directly from the
assumption.

Suppose $\chi=\chi_{0}\otimes\chi_{1}$. Without loss of generality we may
assume that the occurrence of the formula $\psi$ is in the subformula
$\chi_{0}$. By the induction hypothesis we have
$\chi_{0}(\delta/[\psi,m])\vdash\chi_{0}(\theta/[\psi,m])$. An application of
the rule $\otimes\textsf{Sub}^{-}$ yields
$\chi_{0}(\delta/[\psi,m])\otimes\chi_{1}\vdash\chi_{0}(\theta/[\psi,m])\otimes\chi_{1}$.

The case $\chi=\chi_{0}\wedge\chi_{1}$ is proved analogously by applying
$\wedge\textsf{E}$ and $\wedge\textsf{I}$. ∎

######  Lemma 5.13.

Let $[\alpha,m]$ be an occurrence of an atom in a formula $\phi$ and
$\mathcal{Y}$ the set of all teams on $N=\\{i_{1},\dots,i_{n}\\}$ that satisfy
$\alpha$. For any set $\Gamma\cup\\{\theta\\}$ of formulas in the language of
$\mathbf{CPL^{+}}$, if $\Gamma,\phi^{\ast}_{Y}\vdash\theta$ for all
$Y\in\mathcal{Y}$, then $\Gamma,\phi\vdash\theta$.

###### Proof.

If $\alpha$ is the non-emptiness $\mathop{\mbox{\small\rm NE}}$, then the
statement follows from $\textsf{SE}_{1}$. If $\alpha=\bot$, then
$\mathcal{Y}=\\{\emptyset\\}$, $\Theta^{\ast}_{\emptyset}=\bot$ and
$\phi^{\ast}_{\emptyset}=\phi$. Thus the statement holds trivially. The
nontrivial case is when $\alpha$ is $p_{i_{k}}$ or $\neg p_{i_{k}}$. We only
give the proof for the case $\alpha=p_{i_{k}}$. The case $\alpha=\neg
p_{i_{k}}$ is proved similarly.

In view of $\textsf{SE}_{2}$, to show $\Gamma,\phi\vdash\theta$ it suffices to
show that $\Gamma,\phi(p_{i_{k}}\wedge\mathop{\mbox{\small\rm
NE}}/[p_{i_{k}},m])\vdash\theta$ and
$\Gamma,\phi(p_{i_{k}}\wedge\bot/[p_{i_{k}},m])\vdash\theta$. To show the
latter, first note that by the assumption we have
$\Gamma,\phi(\Theta^{\ast}_{\emptyset}/[p_{i_{k}},m])\vdash\theta$, i.e.,
$\Gamma,\phi(\bot/[p_{i_{k}},m])\vdash\theta$. It then suffices to check that
$\phi(p_{i_{k}}\wedge\bot/[p_{i_{k}},m])\vdash\phi(\bot/[p_{i_{k}},m])$. But
this follows from Lemma 5.12, as by $\wedge\textsf{E}$ we have
$p_{i_{k}}\wedge\bot\vdash\bot$.

To show the former, in view of $\textsf{SE}_{1}$ it suffices to derive
$\Gamma,\phi(p_{i_{k}}\wedge\Theta^{\ast}_{X}/[p_{i_{k}},m])\vdash\theta$ for
all nonempty teams $X$ on $N\setminus\\{i_{k}\\}$. By the rule
$\textsf{Dstr}^{\ast}\\!$ $\wedge\otimes$, we have
$p_{i_{k}}\wedge\Theta^{\ast}_{X}\vdash\Theta^{\ast}_{Y}$, where $Y\subseteq
2^{N}$ is defined as

$Y=\\{s:N\to 2\mid s\upharpoonright N\setminus\\{i_{k}\\}\in X\text{ and
}s(i_{k})=1\\}.$

It then follows from Lemma 5.12 that
$\phi(p_{i_{k}}\wedge\Theta^{\ast}_{X}/[p_{i_{k}},m])\vdash\phi(\Theta^{\ast}_{Y}/[p_{i_{k}},m])$.
On the other hand, clearly $Y\in\mathcal{Y}$ and the assumptions implies that
$\Gamma,\phi(\Theta^{\ast}_{Y}/[p_{i_{k}},m])\vdash\theta$. Hence we obtain
$\Gamma,\phi(p_{i_{k}}\wedge\Theta^{\ast}_{X}/[p_{i_{k}},m])\vdash\theta$, as
desired. ∎

Now we are ready to prove the full statement for an arbitrary sequence $o$ of
occurrences of atoms.

######  Lemma 5.14.

Let $\Lambda$ be the set of all strongly realizing sequences of $\phi$ over a
sequence $o$ of some occurrences of atoms in a formula $\phi$. For any set
$\Gamma\cup\\{\theta\\}$ of formulas in the language of $\mathbf{CPL^{+}}$, if
$\Gamma,\phi^{\ast}_{\Omega}\vdash\theta$ for all $\Omega\in\Lambda$, then
$\Gamma,\phi\vdash\theta$.

###### Proof.

Let $o=\langle[\alpha_{1},m_{1}],\,\dots,\,[\alpha_{c},m_{c}]\rangle$. By the
assumption, for any $Y_{1}$ that satisfies $\alpha_{1}$ we have

$\begin{split}\Gamma,\phi((\alpha_{1})^{\ast}_{Y_{1}}/[\alpha_{1},m_{1}],(\alpha_{2})^{\ast}_{X_{2}}/[\alpha_{2},m_{2}],\,&\dots,\,(\alpha_{c})^{\ast}_{X_{c}}/[\alpha_{c},m_{c}])\vdash\theta\\\
&\text{ for all }\langle Y_{1},X_{2},\dots,X_{c}\rangle\in\Lambda\end{split}$

Then we conclude by Lemma 5.13 that $\Gamma,\phi^{\ast}_{\Omega}\vdash\theta$
for all $\Omega\in\Lambda_{1}$, where $\Lambda_{1}$ is the set of all strongly
realizing sequences of $\phi$ over a sequence
$o_{1}=\langle[\alpha_{2},m_{2}],\,\dots,\,[\alpha_{c},m_{c}]\rangle$.

By repeating this argument $c$ times, we obtain $\Gamma,\phi\vdash\theta$ in
the end. ∎

For the sake of the proof of the Completeness Theorem, we need to further
transform each strong realization $\phi^{\ast}_{\Omega}$ into a formula