# The propositional logic of teams

Engström  Fredrik  Lorimer Olsson  Orvar

###### Abstract

Since the introduction by Hodges, and refinement by Väänänen, team semantic
constructions have been used to generate expressively enriched logics
conserving some nice properties, such as compactness or decidability. By
contrast, these logics fail to be substitutional, limiting any algebraic
treatment, and rendering schematic uniform proof systems impossible. This
shortcoming can be attributed to _the flatness principle_ , commonly adhered
to when generating team semantics.

Investigating the formation of team semantics from algebraic semantics, and
disregarding the flatness principle, we present _the logic of teams_ , LT, a
substitutional logic in which important propositional team logics are
axiomatisable as fragments. Starting from classical propositional logic and
Boolean algebras, we give a semantics for LT by considering the algebras that
are powersets of Boolean algebras $B$, i.e., of the form ${\mathcal{P}}B$,
equipped with _internal_ (pointwise) and _external_ (set theoretic)
connectives. Furthermore, we present a well-motivated complete and sound
labelled natural deduction system for LT.

##  1 Introduction

Team semantics was invented by Hodges [Hodges1997] to give the Independence
Friendly logic (IF-logic) of Hintikka and Sandu [Hintikka1989] a compositional
semantics. Team semantics was later used by Väänänen to define Dependence
logic [Vaeaenaenen2007], a formalism extending first-order logic in which
functional dependencies between variables are explicitly expressed by atomic
formulas. The intended meaning of these atomic formulas
$\mathtt{D}(\bar{x},y)$ is that the value of the variable $y$ is functionally
determined by the values of the finitely many variables $\bar{x}$. Even though
Dependence logic uses only first-order quantifiers it can express any
existential second-order property or statement. The reason is that there are
second-order quantifiers hidden in the truth conditions, most interestingly in
the truth conditions for $\lor$ and $\exists$.

Since then many logics based on team semantics have been introduced and
investigated, such as Independence logic, Propositional dependence logics and
Modal dependence logics.

###  1.1 Lifting Tarskian semantics to team semantics

In the classical Tarskian semantics of first-order logic the denotation of a
formula, given a structure, is defined to be the set of all assignments that
satisfies the formula. Similarly, the denotation of a propositional formula is
the set of valuations satisfying the formula, and the denotation of a modal
logic formula, given a Kripke model, is the set of all worlds satisfying the
formula. Thus, the denotation of a formula in this classical setting is an
element of ${\mathcal{P}}X$, the powerset of the set $X$ of all assignments,
all valuations or all worlds, respectively.

Team semantics of first-order, propositional and modal logic lifts the
denotations of formulas to be sets of subsets of $X$, i.e., elements of
${\mathcal{P}}{\mathcal{P}}X$, instead of elements of ${\mathcal{P}}X$. Thus,
instead of asking if a single assignment, valuation or world satisfies a
formula, team semantics asks if a _set_ of assignments, valuations or worlds
satisfies a formula. Such sets are called _teams_. In this sense, the team
semantical denotation is the image of the classical denotation under a
specific function, a lift, from ${\mathcal{P}}X$ to
${\mathcal{P}}{\mathcal{P}}X$.

For most team semanticists the _flatness principle_ has guided the definition
of the semantics. This principle can be formulated as follows:

> A team satisfies a formula iff every individual assignment, valuation, or
> world in the team satisfies the formula in the usual classical sense.

Note that this only applies to formulas in the original language, without any
dependence atoms or other added connectives; for these formulas it make sense
to say that an assignment/valuation/world satisfies a formula. Flatness
directly gives conservativity in the sense that the singleton team of the
empty assignment satisfies a sentence in a model iff the sentence is true in
the classical sense in the model.

In terms of denotations of formulas the flatness principle naturally
translates to the equation

$\llbracket\varphi\rrbracket_{h}={\mathcal{P}}\llbracket\varphi\rrbracket_{c}$
(1)

where $\llbracket\varphi\rrbracket_{h}$ is the team semantical denotation of
$\varphi$ ($h$ for Hodges) and $\llbracket\varphi\rrbracket_{c}$ is the
ordinary Tarskian denotation of $\varphi$ ($c$ for classical). By subscribing
to the flatness principle most team semanticists also subscribe to this
powerset lift of classical semantics to team semantics.

###  1.2 Substitutionality and logics

Dependence logic and its variants have some nice properties such as
compactness, Löwenheim-Skolem properties [Vaeaenaenen2007] and that first-
order consequences of theories can be axiomatized [Kontinen2013] to name a
few. But they are not substitutional; for example

$\forall x\,(P(x)\lor P(x))\vDash\forall x\,P(x)\text{, but }\forall
x\,(\mathtt{D}(x)\lor\mathtt{D}(x))\nvDash\forall x\,\mathtt{D}(x),$

where $\mathtt{D}(x)$ is the dependence atom with only one free variable,
intuitively stating that there is only one value of $x$ in the team, i.e.,
that $x$ is constant.

In general, a logic is substitutional if $\varphi\vDash\psi$ implies
$\varphi[\sigma/p]\vDash\psi[\sigma/p]$, i.e., an entailment does not break by
substituting a formula $\sigma$ for an atom $p$. Substitutionality was already
used by Bolzano to define the concept of validity. In [Bolzano1837] Bolzano
defines _universally valid propositions_ as propositions with all their
variants true. In his terminology a variant is nothing but a substitutional
instance. Bolzano, and many after him, thus took substitutionality not only as
an important property for a logic, but as the basic principle for the concept
of logical validity.

Any attempt to algebraise a logic that is not substitutional will not work in
the strict sense since the elements of the algebraic structure need to be
partitioned, or divided, into different types. Indeed, the examples of
algebraisations of variants of propositional dependence logic that appear in
the literature [Quadrellaro2021, Quadrellaro2020, Bezhanishvili2021] all
introduce additional predicates on the resulting algebras in order to
partition the elements into different types.

The powerset lift of the Tarskian semantics to team semantics, as in (1),
could be blamed for the lack of substitutionality in Dependence logic. In
fact, any specific lift will limit the possible denotations of atoms and the
resulting logics will not, in general, be substitutional.

In this paper we will therefore generalize away from using a specific lift.
Instead we will, in a certain sense, quantify over all possible lifts of the
atoms: Given a function
$\mathcal{L}:{\mathcal{P}}X\to{\mathcal{P}}{\mathcal{P}}X$ that lifts the
denotations of atoms from a Tarskian setting to a team semantical setting, we
extend this compositionally to give team semantical denotations
$\llbracket\varphi\rrbracket_{\mathcal{L}}$ to all formulas $\varphi$ in our
logic. We define the entailment relation by $\varphi\vDash\psi$ if
$\llbracket\varphi\rrbracket_{\mathcal{L}}\subseteq\llbracket\psi\rrbracket_{\mathcal{L}}$
for all functions $\mathcal{L}:{\mathcal{P}}X\to{\mathcal{P}}{\mathcal{P}}X$.

The function $\varphi\mapsto\llbracket\varphi\rrbracket_{\mathcal{L}}$ is
nothing but a homomorphism from the absolutely free term algebra of formulas
to a specific algebraic structure of sets of teams. Describing a logic by
quantifying over all homomorphisms from a term language into an algebraic
structure is exactly the starting point for constructing algebraic semantics.

###  1.3 Lifting algebraic semantics

The semantics of classical propositional logic can be defined in terms of
Boolean algebras. One may even say that classical propositional logic _is_ the
logic of Boolean algebras. The set of propositional formulas is the term
algebra generated by atoms using the Boolean operators $\bot,\lnot,\lor$, and
$\land$; and the semantics of propositional logic can be stated using
homomorphisms from this term algebra to a Boolean algebra. A formula is a
tautology if its image under any such homomorphism is the top element of the
Boolean algebra. This is the starting point when we define the Logic of Teams,
or LT for short: Lifting the algebraic semantics for classical propositional
logic to the setting of teams. A team in this setting is nothing but a set of
elements of the Boolean algebra.

The connectives, and the corresponding operators on the sets of teams, we are
interested in are the ordinary Boolean connectives $\bot,\lnot,\lor,\land$
that correspond to the empty set, the complement, the union and the
intersection. We will call these connectives and the corresponding operators
_external_ Boolean connectives and operators. We will also add the _internal_
connectives and operators that are defined by pointwise application of the
operators of the Boolean algebra, for example

$A\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}B=\set{a\lor
b}{a\in A,b\in B},$

where
$\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}$
is the internal disjunction. We will use blackbord boldface versions of the
Boolean connectives to denote these internal connectives:
$\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}},\mathord{\vphantom{\lnot}\mathchoice{\ooalign{\raisebox{0.86108pt}{$\displaystyle\neg$}\cr\raisebox{-0.86108pt}{$\displaystyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\textstyle\neg$}\cr\raisebox{-0.86108pt}{$\textstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptscriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptscriptstyle\neg$}}}},\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}},\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}$.
When the underlying Boolean algebra is ${\mathcal{P}}2^{\mathbb{N}}$ with the
set-theoretic Boolean operators, the connective
$\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}$
is exactly the “splitjunction” used in Dependence logic, and
$\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}$
is, in Dependence logic, equivalent to conjunction.

###  1.4 Related constructions

An algebraic structure generated by the powerset of a Boolean algebra with
internal connectives is not new to mathematics and logic. Brink [Brink1984,
Brink1986, Brink1993] contributes to these investigations and calls them
_power algebras_ , whereas Goldblatt calls them _complex algebras_
[Goldblatt1989] referring to a subset of an algebraic group as a complex. It
is also worth noting that these algebras are special cases of _Boolean
algebras with operators_ as described by Jónsson and Tarski [Jonsson1993].
These play a notable role in the algebraic treatment of Modal logic, see
[Venema2007].

In other related work, Priest has utilised the powerset lift in order to
investigate resulting families of plurivalent logics [Priest2017], an effort
elaborated on by Humberstone in [Humberstone2014] coining the term power
matrices for the resulting constructions. In these papers, semantics of
multivalued logics is lifted into evaluations on subsets of possible truth
values, and the logical connectives are interpreted in terms of pointwise
operations. They do, however, not include any connectives relating to the set-
theoretic Boolean operations on the powerset algebra.

In particular, in [Goranko99] Goranko and Vakarelov use power sets of Boolean
algebras, referred to as hyperboolean algebras, in order to define what they
call the hyperboolean modal logic, HBML. This construction treats a Boolean
algebra, expressed as a partial order, as a Kripke frame and utilise the
Boolean structure to define modal operators. The algebraic counterpart of the
logic HBML is thus the powerset algebra of the original Boolean algebra, with
the modal operators defined as the internal pointwise operations on the
underlying algebra.

The logic of teams that we define in this paper has different motivation and
origin than that of HBML, but building on the same class of models. It is easy
to see that the connectives of LT and HBML are interdefinable such that the
two logics share validities and can in this sense be viewed as having the same
theorems. However, where Goranko and Vakarelov only defines HBML in terms of
validity with a proof system fundamentally structured around an elaborately
defined difference modality and an only operator, we define LT for a full
entailment notion and present a labelled natural deduction system for which
the rules directly correspond to the basic connectives of the logic. Even so,
the correspondence between the two logics is strong enough for some important
properties of HBML presented in [Goranko99] to also apply to LT, see Section
3.1.

###  1.5 Structure of this paper

In the next section we formally introduce the syntax and semantics of the
Logic of Teams, LT. The semantics is defined in an algebraic manner in terms
of homomorphisms into algebraic structures based on Boolean algebras. In the
same section we also introduce a labelled natural deduction system for LT. The
formulas are decorated by labels and the labels are themselves classical
propositional formulas. By including rules in the deduction system identifying
classically equivalent formulas as equivalent labels we establish the role of
the labels as references to elements in a Boolean algebra, and this paves the
way for the completeness proof via Lindenbaum–Tarski algebras presented in the
next section.

Section 3 is devoted to prove the completeness of the natural deduction system
and the consequences that can be observed by a more careful investigation of
the proof. This section also includes results regarding non-canonicity and
adequacy of sets of Boolean algebras.

In Section 4 we introduce some important definable connectives in LT. In
particular we define the strict negation that, apart from being an interesting
type of negation, will be important in Section 6. We also define a universal
$\Box$-modality, which plays an important role in Section 5, where definable
classes of homomorphisms and axiomatisations of their corresponding logics are
discussed.

In section 6 we finally utilise the strict negation to define classes of
homomorphisms, and give axioms expressing the strong propositional team logic,
PT+ in [Yang2017], as a part of LT. In this way we establish the connection
between LT and the propositional team logics found in the literature with
semantics based on teams of valuations, here referred to as valuational team
semantics. These results establish LT as a well motivated, substitutional, and
expressively rich propositional team logic that is highly relevant for a
better understanding of team semantics for propositional logics.

In the final section of the paper we reflect generally on the construction
that we have presented, and discuss some further topics of investigation that
are implicated by our work.

##  2 The Logic of Teams

Let us now define the Logic of Teams, LT, that is our main object of study in
this paper.

Let $B$ be a Boolean algebra, allowing for $B$ to be the trivial, one element,
Boolean algebra. The powerset ${\mathcal{P}}B$ is the domain of a Boolean
algebra with respect to the usual set-theoretic operators
$(\emptyset,\cdot^{C},\cup,\cap)$, which we from now will denote by $\bot$,
$\lnot$, $\lor$, and $\land$. These structures also have some additional
natural operators; the internal, or pointwise operators:
$\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}$,
$\mathord{\vphantom{\lnot}\mathchoice{\ooalign{\raisebox{0.86108pt}{$\displaystyle\neg$}\cr\raisebox{-0.86108pt}{$\displaystyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\textstyle\neg$}\cr\raisebox{-0.86108pt}{$\textstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptscriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptscriptstyle\neg$}}}}$,
$\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}$,
and
$\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}$.
These operators are defined as follows:

$\displaystyle\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}$ $\displaystyle=\set{\bot},$
$\displaystyle\mathord{\vphantom{\lnot}\mathchoice{\ooalign{\raisebox{0.86108pt}{$\displaystyle\neg$}\cr\raisebox{-0.86108pt}{$\displaystyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\textstyle\neg$}\cr\raisebox{-0.86108pt}{$\textstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptscriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptscriptstyle\neg$}}}}X$
$\displaystyle=\set{\lnot a}{a\in X},$ $\displaystyle
X\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}Y$
$\displaystyle=\set{a\lor b}{a\in X,b\in Y},\text{ and}$ $\displaystyle
X\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}Y$
$\displaystyle=\set{a\land b}{a\in X,b\in Y},$

where $X,Y\subseteq B$ and, for example, $a\lor b\in B$ is the result of the
operator $\lor$ in the Boolean algebra $B$ applied to $a$ and $b$.

Formulas of LT are elements in the term algebra, the absolutely free algebra,
generated by the propositional variables $P_{0}$, $P_{1}$, … using the
external Boolean connectives $\bot$, $\lnot$, $\lor$, $\land$ and the internal
Boolean connectives
$\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}$,
$\mathord{\vphantom{\lnot}\mathchoice{\ooalign{\raisebox{0.86108pt}{$\displaystyle\neg$}\cr\raisebox{-0.86108pt}{$\displaystyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\textstyle\neg$}\cr\raisebox{-0.86108pt}{$\textstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptscriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptscriptstyle\neg$}}}}$,
$\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}$,
$\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}$.
We will denote this term algebra by $\mathtt{Fm}$:111Observe that the symbols
$\bot$, $\lnot$, $\lor$, and $\land$ have different meanings in different
contexts. They denote the connectives in the term algebra, the set-theoretic
operators in ${\mathcal{P}}B$ and the Boolean operators in $B$. Later on will
introduce yet another meaning, as connectives in the labels of the natural
deduction system.

$\varphi::=\bot\mathrel{|}\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}\mathrel{|}P_{i}\mathrel{|}\lnot\varphi\mathrel{|}\mathord{\vphantom{\lnot}\mathchoice{\ooalign{\raisebox{0.86108pt}{$\displaystyle\neg$}\cr\raisebox{-0.86108pt}{$\displaystyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\textstyle\neg$}\cr\raisebox{-0.86108pt}{$\textstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptscriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptscriptstyle\neg$}}}}\varphi\mathrel{|}\varphi\lor\varphi\mathrel{|}\varphi\land\varphi\mathrel{|}\varphi\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\varphi\mathrel{|}\varphi\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}\varphi$

Entailment is defined as the subset relation for the images of the formulas
under arbitrary homomorphisms.

######  Definition 2.1.

Let $\Delta$ be a set of formulas. Then $\Delta\vDash\psi$ iff for all Boolean
algebras $B$ and all homomorphisms $H:\mathtt{Fm}\to{\mathcal{P}}B$:

$\bigcap_{\varphi\in\Delta}H(\varphi)\subseteq H(\psi).$

Note that this definition of entailment does not correspond to the standard
entailment in algebraic logic in which $\varphi$ entails $\psi$ iff whenever
$H$ is a homomorphism with $H(\varphi)=B$ then $H(\psi)=B$. The fact that
$\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}\nvDash\mathord{\vphantom{\lnot}\mathchoice{\ooalign{\raisebox{0.86108pt}{$\displaystyle\neg$}\cr\raisebox{-0.86108pt}{$\displaystyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\textstyle\neg$}\cr\raisebox{-0.86108pt}{$\textstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptscriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptscriptstyle\neg$}}}}\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}$ shows this.222In fact, the definition of
entailment in LT corresponds to what, in the algebraic logic literature, is
called _semilattice based logics_. It follows from some general results on
semilattice based logics (see Section 7.2 in [Font16]) that LT is _not_
algebraisable in the strict sense of the term.

Substitution instances of formulas are nothing but images under homomorphisms:
$\sigma:\mathtt{Fm}\to\mathtt{Fm}$ and thus substitutionality follows directly
from the definition of the entailment relation.

######  Theorem 2.2 (Substitutionality)

If $\Delta\vDash\psi$ then $\sigma(\Delta)\vDash\sigma(\psi)$ for every
algebra homomorphism $\sigma:\mathtt{Fm}\to\mathtt{Fm}$.

###### Proof.

Follows directly from the definitions, and the fact that if
$H:\mathtt{Fm}\to{\mathcal{P}}B$ is a homomorphism then so is $H\circ\sigma$.
∎

###  2.1 Natural deduction

To define a deductive system for LT we will introduce _labels_ and _labelled
formulas_. The labels have their intended reading as elements in a Boolean
algebra and the formulas as subsets of the same Boolean algebra. Formally,
labels are classical propositional formulas:

$a::=\bot\mathrel{|}p_{i}\mathrel{|}\lnot a\mathrel{|}a\lor a\mathrel{|}a\land
a$

The propositional variables $p_{i}$ are called _atomic labels_. The term
algebra of labels is denoted by $\mathtt{Lb}$.

A _labelled formula_ is of the form $a\mathbin{:}\varphi$ where $a$ is a label
and $\varphi$ a formula. The intended meaning of this is that $a$ is an
element of $\varphi$, i.e., that under any homomorphisms $h$ and $H$, $h(a)\in
H(\varphi)$. Thus, we define entailment in the natural way:

######  Definition 2.3.

Let $\Gamma$ be a set of labelled formulas, then $\Gamma\vDash
b\mathbin{:}\psi$ iff for all Boolean algebras $B$ and all homomorphisms
$h:\mathtt{Lb}\to B$, $H:\mathtt{Fm}\to{\mathcal{P}}B$ if $h(a)\in H(\varphi)$
for all $a\mathbin{:}\varphi\in\Gamma$ then $h(b)\in H(\psi)$.

We say that the homomorphisms $H$ and $h$ make $a\mathbin{:}\varphi$ true if
$h(a)\in H(\varphi)$.

###### Proposition 2.4

$\Delta\vDash\psi$ iff $p\mathbin{:}\Delta\vDash p\mathbin{:}\psi$, where $p$
is an atomic label and
$p\mathbin{:}\Delta=\set{p\mathbin{:}\varphi}{\varphi\in\Delta}$.

###### Proof.

Follows directly from the definitions. ∎

We will now present a sound and complete proof system for the relation
$\Gamma\vDash b\mathbin{:}\psi$, where $\Gamma$ is a set of labelled formulas.
For this we will use the usual shorthands $a\leftrightarrow b$ for
$(a\lor\lnot b)\land(\lnot a\lor b)$ and
$\mathord{\vphantom{\top}\mathchoice{\ooalign{$\displaystyle\top$\cr\kern
1.99997pt$\displaystyle\top$}}{\ooalign{$\textstyle\top$\cr\kern
1.99997pt$\textstyle\top$}}{\ooalign{$\scriptstyle\top$\cr\kern
1.99997pt$\scriptstyle\top$}}{\ooalign{$\scriptscriptstyle\top$\cr\kern
1.99997pt$\scriptscriptstyle\top$}}}$ for
$\mathord{\vphantom{\lnot}\mathchoice{\ooalign{\raisebox{0.86108pt}{$\displaystyle\neg$}\cr\raisebox{-0.86108pt}{$\displaystyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\textstyle\neg$}\cr\raisebox{-0.86108pt}{$\textstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptscriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptscriptstyle\neg$}}}}\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}$. Also $a=b$ is a shorthand for the
labelled formula $a\leftrightarrow
b\mathbin{:}\mathord{\vphantom{\top}\mathchoice{\ooalign{$\displaystyle\top$\cr\kern
1.99997pt$\displaystyle\top$}}{\ooalign{$\textstyle\top$\cr\kern
1.99997pt$\textstyle\top$}}{\ooalign{$\scriptstyle\top$\cr\kern
1.99997pt$\scriptstyle\top$}}{\ooalign{$\scriptscriptstyle\top$\cr\kern
1.99997pt$\scriptscriptstyle\top$}}}$. Note that if $H$ and $h$ are
homomorphisms that make $a=b$ true then $h(a)=h(b)$.

####  2.1.1 Rules for external Boolean connectives

The following rules are the standard rules for propositional logic, with
labels added to the formulas.

$a\mathbin{:}\varphi\land\psi\lx@proof@logical@and a\mathbin{:}\varphi
a\mathbin{:}\psi\qquad\qquad a\mathbin{:}\varphi
a\mathbin{:}\varphi\land\psi\qquad\qquad a\mathbin{:}\psi
a\mathbin{:}\varphi\land\psi$

$a\mathbin{:}\varphi\lor\psi a\mathbin{:}\varphi\qquad\qquad
a\mathbin{:}\varphi\lor\psi a\mathbin{:}\psi\qquad\qquad
b\mathbin{:}\sigma\lx@proof@logical@and a\mathbin{:}\varphi\lor\psi
b\mathbin{:}\sigma[a\mathbin{:}\varphi]b\mathbin{:}\sigma[a\mathbin{:}\psi]$

$a\mathbin{:}\lnot\varphi b\mathbin{:}\bot[a\mathbin{:}\varphi]\qquad\qquad
a\mathbin{:}\bot\lx@proof@logical@and a\mathbin{:}\varphi
a\mathbin{:}\lnot\varphi$

$a\mathbin{:}\varphi b\mathbin{:}\bot[a\mathbin{:}\lnot\varphi]\qquad\qquad
b\mathbin{:}\varphi a\mathbin{:}\bot$

####  2.1.2 Rules for internal Boolean connectives

Next we add rules for the internal connectives. The rule
$\mathord{\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}}\mathtt{E}$
is modelled on the fact that $x\in
H(\varphi\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}\psi)$
iff there are $y,z$ such that $x\in H(\varphi)$, $y\in H(\psi)$ and $x=y\land
z$ holds in the Boolean algebra $B$. Similarily for
$\mathord{\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}}\mathtt{E}$.

$a\land
b\mathbin{:}\varphi\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}\psi\lx@proof@logical@and
a\mathbin{:}\varphi b\mathbin{:}\psi\qquad\qquad
b\mathbin{:}\sigma\lx@proof@logical@and
a\mathbin{:}\varphi\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}\psi
b\mathbin{:}\sigma[a=p\land q][q\mathbin{:}\psi][p\mathbin{:}\varphi]$

$a\lor
b\mathbin{:}\varphi\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\psi\lx@proof@logical@and
a\mathbin{:}\varphi b\mathbin{:}\psi\qquad\qquad
b\mathbin{:}\sigma\lx@proof@logical@and
a\mathbin{:}\varphi\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\psi
b\mathbin{:}\sigma[a=p\lor q][q\mathbin{:}\psi][p\mathbin{:}\varphi]$

$\lnot
a\mathbin{:}\mathord{\vphantom{\lnot}\mathchoice{\ooalign{\raisebox{0.86108pt}{$\displaystyle\neg$}\cr\raisebox{-0.86108pt}{$\displaystyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\textstyle\neg$}\cr\raisebox{-0.86108pt}{$\textstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptscriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptscriptstyle\neg$}}}}\varphi
a\mathbin{:}\varphi\qquad\qquad\lnot a\mathbin{:}\varphi
a\mathbin{:}\mathord{\vphantom{\lnot}\mathchoice{\ooalign{\raisebox{0.86108pt}{$\displaystyle\neg$}\cr\raisebox{-0.86108pt}{$\displaystyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\textstyle\neg$}\cr\raisebox{-0.86108pt}{$\textstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptscriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptscriptstyle\neg$}}}}\varphi$

Note that vacuous discharges are allowed in the elimination rules for
$\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}$
and
$\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}$.
In
$\mathord{\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}}\mathtt{E}$
and
$\mathord{\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}}\mathtt{E}$
the $p$ and $q$ are distinct propositional variables not occurring in any
uncancelled assumptions, nor in $a$ or $b$.

####  2.1.3 Rules for labels

We add two rules for dealing with labels.

$b\mathbin{:}\mathord{\vphantom{\top}\mathchoice{\ooalign{$\displaystyle\top$\cr\kern
1.99997pt$\displaystyle\top$}}{\ooalign{$\textstyle\top$\cr\kern
1.99997pt$\textstyle\top$}}{\ooalign{$\scriptstyle\top$\cr\kern
1.99997pt$\scriptstyle\top$}}{\ooalign{$\scriptscriptstyle\top$\cr\kern
1.99997pt$\scriptscriptstyle\top$}}}\lx@proof@logical@and
a_{1}\mathbin{:}\mathord{\vphantom{\top}\mathchoice{\ooalign{$\displaystyle\top$\cr\kern
1.99997pt$\displaystyle\top$}}{\ooalign{$\textstyle\top$\cr\kern
1.99997pt$\textstyle\top$}}{\ooalign{$\scriptstyle\top$\cr\kern
1.99997pt$\scriptstyle\top$}}{\ooalign{$\scriptscriptstyle\top$\cr\kern
1.99997pt$\scriptscriptstyle\top$}}}\cdots
a_{k}\mathbin{:}\mathord{\vphantom{\top}\mathchoice{\ooalign{$\displaystyle\top$\cr\kern
1.99997pt$\displaystyle\top$}}{\ooalign{$\textstyle\top$\cr\kern
1.99997pt$\textstyle\top$}}{\ooalign{$\scriptstyle\top$\cr\kern
1.99997pt$\scriptstyle\top$}}{\ooalign{$\scriptscriptstyle\top$\cr\kern
1.99997pt$\scriptscriptstyle\top$}}}\qquad\qquad
a\mathbin{:}\varphi\lx@proof@logical@and a=bb\mathbin{:}\varphi$

The rule $\mathtt{taut}$ is only applicable if $a_{1},\ldots,a_{k}\vdash b$ in
classical propositional logic, i.e., if $a_{1}\land\ldots\land
a_{k}\rightarrow b$ is a tautology. Note that we allow for the special case
when $k=0$ in this rule.

Without the distinctiveness criteria in
$\mathord{\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}}\mathtt{E}$
and
$\mathord{\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}}\mathtt{E}$
the system would not be sound: The following “derivation” would then show that
$a\mathbin{:}P\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}Q\vDash
a\mathbin{:}P\land Q$, but this is false.

$a\mathbin{:}P\land Q\lx@proof@logical@and
a\mathbin{:}P\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}Qa\mathbin{:}P\land
Q\lx@proof@logical@and a=b[a=b\land b]^{1}b\mathbin{:}P\land
Q\lx@proof@logical@and[b\mathbin{:}P]^{1}[b\mathbin{:}Q]^{1}$

For an example of a non-trivial derivation of an entailment, see Figure 1. It
is easy to see that the derivability relation satisfies the following lemma:

###### Lemma 2.5

$\Gamma\vdash a\mathbin{:}\varphi$ iff $\Gamma,a\mathbin{:}\lnot\varphi\vdash
a\mathbin{:}\bot$.

Soundness follows by an easy induction:

######  Theorem 2.6 (Soundness)

If $\Gamma\vdash a\mathbin{:}\varphi$ then $\Gamma\vDash a\mathbin{:}\varphi$.

###### Proof.

Follows from a straight-forward induction on proof trees. For the case of
$\mathord{\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}}\mathtt{E}$,
$\mathord{\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}}\mathtt{E}$,
$\mathtt{taut}$ and $\mathtt{sub}$ note that $h(a)\in
H(\mathord{\vphantom{\top}\mathchoice{\ooalign{$\displaystyle\top$\cr\kern
1.99997pt$\displaystyle\top$}}{\ooalign{$\textstyle\top$\cr\kern
1.99997pt$\textstyle\top$}}{\ooalign{$\scriptstyle\top$\cr\kern
1.99997pt$\scriptstyle\top$}}{\ooalign{$\scriptscriptstyle\top$\cr\kern
1.99997pt$\scriptscriptstyle\top$}}})$ implies that $h(a)$ is $\top$, the top
element of $B$. Thus, if $h(a\leftrightarrow b)\in
H(\mathord{\vphantom{\top}\mathchoice{\ooalign{$\displaystyle\top$\cr\kern
1.99997pt$\displaystyle\top$}}{\ooalign{$\textstyle\top$\cr\kern
1.99997pt$\textstyle\top$}}{\ooalign{$\scriptstyle\top$\cr\kern
1.99997pt$\scriptstyle\top$}}{\ooalign{$\scriptscriptstyle\top$\cr\kern
1.99997pt$\scriptscriptstyle\top$}}})$ then $h(a)=h(b)$. ∎

##  3 Completeness and adequacy

Next we will prove the completeness of the proof system, but first we need
some definitions and a few easy facts.

Observe that if $\Gamma\vdash\bot\mathbin{:}\bot$ then $\Gamma\vdash
a\mathbin{:}\varphi$ for all labels $a$ and all formulas $\varphi$. We say
that $\Gamma$ is _consistent_ if $\Gamma\nvdash\bot\mathbin{:}\bot$ or
equivalently that there are $a$ and $\varphi$ such that $\Gamma\nvdash
a\mathbin{:}\varphi$.

###### Proposition 3.1

If $\Gamma$ is consistent then so is either $\Gamma,a\mathbin{:}\varphi$ or
$\Gamma,a\mathbin{:}\lnot\varphi$.

###### Proof.

Directly by using the $\lnot\mathtt{I}$ and $\lnot\mathtt{E}$ rules. ∎

In the next proposition remember that if $a$ and $b$ are labels then $a=b$
denotes the labelled formula $a\leftrightarrow
b:\mathord{\vphantom{\top}\mathchoice{\ooalign{$\displaystyle\top$\cr\kern
1.99997pt$\displaystyle\top$}}{\ooalign{$\textstyle\top$\cr\kern
1.99997pt$\textstyle\top$}}{\ooalign{$\scriptstyle\top$\cr\kern
1.99997pt$\scriptstyle\top$}}{\ooalign{$\scriptscriptstyle\top$\cr\kern
1.99997pt$\scriptscriptstyle\top$}}}$.

###### Proposition 3.2

If
$\Gamma,a\mathbin{:}\varphi\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\psi$
is consistent and $p$ and $q$ are propositional variables not occurring in
$\Gamma$, nor in $a$, then
$\Gamma,a\mathbin{:}\varphi\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\psi,p\mathbin{:}\varphi,q\mathbin{:}\psi,a=p\lor
q$ is consistent. And similarly for
$\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}$.

###### Proof.

Directly by using the
$\mathord{\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}}\mathtt{E}$
rule and the
$\mathord{\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}}\mathtt{E}$
rule. ∎

######  Definition 3.3.

$\Gamma$ is
_$\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}$
-saturated_ if whenever
$a\mathbin{:}\varphi\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\psi\in\Gamma$
then there are labels $b$ and $c$ such that
$\set{b\mathbin{:}\varphi,c\mathbin{:}\psi,a=b\lor c}\subseteq\Gamma$. The
dual notion of
_$\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}$
-saturation_ is defined similarly. We say that $\Gamma$ is _saturated_ if it
is both
$\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}$-saturated
and
$\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}$-saturated.

###### Lemma 3.4

Let $\Gamma$ be a set of labelled formulas and $\Gamma^{\prime}$ be the result
of renaming the atomic labels $p_{i}$ by $p_{2i}$. Then

  1. 1.

$\Gamma$ is consistent iff $\Gamma^{\prime}$ is, and

  2. 2.

$\Gamma$ is satisfiable iff $\Gamma^{\prime}$ is.

###### Proof.

  1. 1.

If $\Gamma\vdash\bot$ then the same derivation with all atomic labels renamed
shows that $\Gamma^{\prime}\vdash\bot$. On the other hand if
$\Gamma^{\prime}\vdash\bot$, there is a finite subset $\Gamma^{f}$ of
$\Gamma^{\prime}$ such that $\Gamma^{f}\vdash\bot$. By renaming the atoms
$p_{2i}$ by $p_{i}$ and $p_{2i+1}$ by $p_{i+k}$ where $k$ is large enough,
i.e., larger than all indices of atoms occurring in $\Gamma^{f}$, we see that
$\Gamma\vdash\bot$.

  2. 2.

Given a Boolean algebra $B$ and homomorphisms $H$ and $h$ such that $h(a)\in
H(\varphi)$ for all $a:\varphi\in\Gamma$ we can define $h^{\prime}$ by setting
$h^{\prime}(p_{2i})=h(p_{i})$ and $h^{\prime}(p_{2i+1})=\bot\in B$. Then
$B,H,h^{\prime}$ satisfies $\Gamma^{\prime}$. Also, if $B,H,h$ satisfies
$\Gamma^{\prime}$ then clearly for $h^{\prime}$ defined by
$h^{\prime}(p_{i})=h(p_{2i})$ we have that $B,H,h^{\prime}$ satisfies
$\Gamma$.

∎

######  Theorem 3.5 (Completeness)

If $\Gamma\vDash a\mathbin{:}\varphi$ then $\Gamma\vdash a\mathbin{:}\varphi$.

###### Proof.

Assume that $\Gamma\nvdash a\mathbin{:}\varphi$. By Lemma 2.5 the set
$\Gamma_{0}=\Gamma,a\mathbin{:}\lnot\varphi$ is consistent. We will extend it
to a maximal consistent saturated set $\Gamma^{\ast}$. By applying the
previous lemma we may assume that there are an infinite set of atomic labels
that are not mentioned in $\Gamma_{0}$.

We construct $\Gamma^{\ast}$ as the union of $\Gamma_{n}$ where each
$\Gamma_{n}$ is a finite extension of $\Gamma_{0}$. First, we enumerate all
labelled formulas and when constructing $\Gamma_{n+1}$ we pick the $n$:th
labelled formula $b\mathbin{:}\psi$ and add either $b\mathbin{:}\psi$ or
$b\mathbin{:}\lnot\psi$. By Proposition 3.1 one of these is consistent with
$\Gamma_{n}$.

By Proposition 3.2 we can assure that if we add a labelled formula
$b\mathbin{:}\sigma\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\theta$
then we also add $p\mathbin{:}\sigma$, $q\mathbin{:}\theta$ and $b=p\lor q$
for some new propositional variables $p$ and $q$, and keeping $\Gamma_{n+1}$
consistent. This construction assures that $\Gamma^{\ast}$ is maximal
consistent and saturated.

Now, let
$T=\set{a}{a\mathbin{:}\mathord{\vphantom{\top}\mathchoice{\ooalign{$\displaystyle\top$\cr\kern
1.99997pt$\displaystyle\top$}}{\ooalign{$\textstyle\top$\cr\kern
1.99997pt$\textstyle\top$}}{\ooalign{$\scriptstyle\top$\cr\kern
1.99997pt$\scriptstyle\top$}}{\ooalign{$\scriptscriptstyle\top$\cr\kern
1.99997pt$\scriptscriptstyle\top$}}}\in\Gamma^{\ast}}$. Let $B$ be the
Lindenbaum–Tarski Boolean algebra of labels over $T$, i.e., its elements are
equivalence classes of labels under the relation of $T$-provable equivalence:

$B=\mathtt{Lb}/\mathord{\sim}_{T}=\set{[a]_{T}}{a\in\mathtt{Lb}},$

where $a\sim_{T}b$ iff $T\vdash a\leftrightarrow b$ (in classical
propositional logic) and $[a]_{T}=\set{b\in\mathtt{Lb}}{a\sim_{T}b}$. Observe
that $B$ is the trivial one-element Boolean algebra iff $T$ is the
inconsistent theory, i.e., iff $\bot\in T$.

Define the homomorphisms $h:\mathtt{Lb}\to B$ and
$H:\mathtt{Fm}\to{\mathcal{P}}B$ by

$\displaystyle h(a)=[a]_{T}\in B\text{ for atoms $a$, and}$ $\displaystyle
H(\varphi)=\set{h(a)}{a\mathbin{:}\varphi\in\Gamma^{\ast}}\text{ for atoms
$\varphi$}.$

Claim. $h(a)\in H(\varphi)$ iff $a\mathbin{:}\varphi\in\Gamma^{\ast}$.

The claim is proved by induction on formulas. The base case follows
immediately from the definition of $H$ and the observation that

$H(\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}})=\\{[\bot]_{T}\\}.$

This is seen by taking $h(b)\in
H(\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}})$ and observing that
$b\mathbin{:}\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}\in\Gamma^{\ast}$ and so $\lnot
b\mathbin{:}\mathord{\vphantom{\top}\mathchoice{\ooalign{$\displaystyle\top$\cr\kern
1.99997pt$\displaystyle\top$}}{\ooalign{$\textstyle\top$\cr\kern
1.99997pt$\textstyle\top$}}{\ooalign{$\scriptstyle\top$\cr\kern
1.99997pt$\scriptstyle\top$}}{\ooalign{$\scriptscriptstyle\top$\cr\kern
1.99997pt$\scriptscriptstyle\top$}}}\in\Gamma^{\ast}$ and, thus, $\lnot b\in
T$ and $b\in[\bot]_{T}$.

  * •

If $\varphi$ is $\psi\lor\sigma$, $\psi\land\sigma$ or $\lnot\psi$ the
induction step is straight-forward, as for example
$a\mathbin{:}\psi\land\sigma\in\Gamma^{\ast}$ iff
$a\mathbin{:}\psi\in\Gamma^{\ast}$ and $a\mathbin{:}\sigma\in\Gamma^{\ast}$
and, by the induction hypothesis, this is equivalent to $h(a)\in H(\psi)$ and
$h(a)\in H(\sigma)$, i.e., $h(a)\in H(\psi)\cap H(\sigma)=H(\psi\land\sigma)$.

  * •

For the case when $\varphi$ is
$\mathord{\vphantom{\lnot}\mathchoice{\ooalign{\raisebox{0.86108pt}{$\displaystyle\neg$}\cr\raisebox{-0.86108pt}{$\displaystyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\textstyle\neg$}\cr\raisebox{-0.86108pt}{$\textstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptscriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptscriptstyle\neg$}}}}\psi$
note that
$a\mathbin{:}\mathord{\vphantom{\lnot}\mathchoice{\ooalign{\raisebox{0.86108pt}{$\displaystyle\neg$}\cr\raisebox{-0.86108pt}{$\displaystyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\textstyle\neg$}\cr\raisebox{-0.86108pt}{$\textstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptscriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptscriptstyle\neg$}}}}\psi\in\Gamma^{\ast}$
iff $\lnot a\mathbin{:}\psi\in\Gamma^{\ast}$ iff $h(\lnot a)\in H(\psi)$ iff
$\lnot h(a)\in H(\psi)$ iff $h(a)\in
H(\mathord{\vphantom{\lnot}\mathchoice{\ooalign{\raisebox{0.86108pt}{$\displaystyle\neg$}\cr\raisebox{-0.86108pt}{$\displaystyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\textstyle\neg$}\cr\raisebox{-0.86108pt}{$\textstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptscriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptscriptstyle\neg$}}}}\psi)$.

  * •

When $\varphi$ is
$\psi\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\sigma$
note that
$a\mathbin{:}\psi\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\sigma\in\Gamma^{\ast}$
iff there are labels $b$ and $c$ such that $b\mathbin{:}\psi\in\Gamma^{\ast}$,
$c\mathbin{:}\sigma\in\Gamma^{\ast}$ and $a=b\lor c\in\Gamma^{\ast}$. By the
induction hypothesis this is equivalent to $h(b)\in H(\psi)$, $h(c)\in
H(\sigma)$ and $h(a)=h(b\lor c)=h(b)\lor h(c)$. Thus this is equivalent to
$h(a)\in
H(\psi\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\sigma)$.

  * •

The case when $\varphi$ is
$\psi\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}\sigma$
is treated similarly, ending the proof of the claim.

It now follows immediately that for these choices of $B$, $H$, and $h$ we have
$h(a)\in H(\varphi)$ for all $a\mathbin{:}\varphi\in\Gamma_{0}$ and thus
$\Gamma\nvDash a\mathbin{:}\varphi$. ∎

###### Corollary 3.6

The logic LT is compact.

###### Proof.

Follows directly from soundness and completeness. ∎

###  3.1 Canonical algebras

The semantics of classical propositional logic can be defined both in terms of
the single two-element Boolean algebra or in terms of all Boolean algebras,
i.e., the two-element Boolean algebra is _canonical_ for propositional logic.
In LT the situation is a bit different as we will see.

We write

$X:\Delta\vDash\varphi\quad\text{and}\quad B:\Delta\vDash\varphi$

for the restricted version of the entailment relation where the quantification
is done over a set $X$ of Boolean algebras or a single Boolean algebra $B$.
For example, $B:\Delta\vDash\varphi$ iff for all homomorphisms
$H:\mathtt{Fm}\to{\mathcal{P}}B$,

$\bigcap_{\psi\in\Delta}H(\psi)\subseteq H(\varphi).$

######  Definition 3.7.

A set $X$ of Boolean algebras is _adequate_ (for LT) if for every $\Delta$ and
$\varphi$ we have

$\Delta\vDash\varphi\text{ iff }X:\Delta\vDash\varphi.$

We omit an empty theory and write $B:{}\vDash\varphi$ instead of
$B:\emptyset\vDash\varphi$. Let us make some observations:

$B:{}\vDash\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}\text{ iff }B=1,$

where $1$ is the trivial one-element Boolean algebra. If $\varphi$ has no
propositional variables then

$B:{}\nvDash\varphi\text{ iff
}B:{}\vDash\lnot\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}\lor(\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}\lnot\varphi).$

Thus, there is a $\psi$ such that

$B:{}\vDash\psi\text{ iff }B\neq 1.$

Therefore, if $X$ is an adequate set of Boolean algebras then $1\in X$.333Note
that, if we add $\psi$ as an axiom we get a (sound and) complete derivation
system for the semantics restricted to non-trivial Boolean algebras We have a
similar result for $B=2$:

$B:{}\vDash\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}\lor\mathord{\vphantom{\top}\mathchoice{\ooalign{$\displaystyle\top$\cr\kern
1.99997pt$\displaystyle\top$}}{\ooalign{$\textstyle\top$\cr\kern
1.99997pt$\textstyle\top$}}{\ooalign{$\scriptstyle\top$\cr\kern
1.99997pt$\scriptstyle\top$}}{\ooalign{$\scriptscriptstyle\top$\cr\kern
1.99997pt$\scriptscriptstyle\top$}}}\text{ iff }B=1,2,$

where
$\mathord{\vphantom{\top}\mathchoice{\ooalign{$\displaystyle\top$\cr\kern
1.99997pt$\displaystyle\top$}}{\ooalign{$\textstyle\top$\cr\kern
1.99997pt$\textstyle\top$}}{\ooalign{$\scriptstyle\top$\cr\kern
1.99997pt$\scriptstyle\top$}}{\ooalign{$\scriptscriptstyle\top$\cr\kern
1.99997pt$\scriptscriptstyle\top$}}}$ is
$\mathord{\vphantom{\lnot}\mathchoice{\ooalign{\raisebox{0.86108pt}{$\displaystyle\neg$}\cr\raisebox{-0.86108pt}{$\displaystyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\textstyle\neg$}\cr\raisebox{-0.86108pt}{$\textstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptscriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptscriptstyle\neg$}}}}\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}$. Thus, if $X$ is adequate then $2\in X$.
And so, if $X$ is adequate then $\\{1,2\\}\subsetneq X$. But, we can say more.
Due to the similarities of LT and HBML we can follow the procedure in
[Goranko99] to observe that no set of finite Boolean algebras is adequate.
Interpreting the models of LT as Kripke frames, the operation
$\mathop{\downarrow}$, defined in LT in section 4.2, directly corresponds to
the ‘diamond’ operation of the partial order $\leq$ of the underlying Boolean
algebra. For the equally definable dual box operation
$\Box\scriptscriptstyle{\leq}$, it then follows by an established result for
any extension of the modal logic S4, that Grzegorczyk’s formula

$\textbf{Grz:
}\Box_{\scriptscriptstyle{\leq}}(\Box_{\scriptscriptstyle{\leq}}(P\to\Box_{\scriptscriptstyle{\leq}}P)\to
P)\to P$

is valid on a partially ordered Kripke frame if and only if it is finite.444It
is fairly straight-forward to see that Grz is falsifiable in a partially
ordered Kripke frame $F$ if and only if it is possible to choose a valuation
$V$ such that there is a $\leq$-sequence of points ${p_{1}\leq
p_{2}\leq\dots}$ such that satisfaction of the member-hood $p_{i}\in V(P)$ is
infinitely alternating. See [Bull1984] for details. Since LT can express this
formula, we can conclude that:

###### Theorem 3.8

The set of finite Boolean algebras is not adequate (for LT).

On the other hand, the completeness theorem gives us a set of Boolean algebras
that is adequate, the set of Lindenbaum–Tarski algebras. These are all
countable Boolean algebras.

###### Theorem 3.9

The set of finite and countable Boolean algebras is adequate.

###### Proof.

The proof of the completeness theorem constructs a Boolean algebra $B$ that is
a Lindenbaum–Tarski algebra over a countably infinite set of propositional
variables. Thus, if $\Gamma\nvdash a\mathbin{:}\varphi$ there is
$H:\mathtt{Fm}\to{\mathcal{P}}B$, where $B$ is a finite or countable Boolean
algebra, such that $\bigcap_{\psi\in\Gamma}H(\psi)\nsubseteq H(\varphi)$. ∎

##  4 Definable connectives

We have defined an algebra based on external and internal Boolean connectives.
Using these connectives, we can define a set of other constants and
connectives; some of the usual suspects, and some that will be useful for the
connection to other propositional team semantics in the literature, see
section 6. It will be clear from the definitions we give that there are plenty
of other definable connectives; in particular, all connectives defined for
HBML in [Goranko99] are definable in LT. In this paper we focus on the
connectives that will be important for expressing propositional team
semantics, and leave further exploration for future work. We name connectives
after their interpretation in the intended semantics.

###  4.1 Constants

We define the following constants with corresponding semantic interpretation
for every Boolean algebra $B$ and every homomorphism
$H:\mathtt{Fm}\to{\mathcal{P}}B$:

  * •

$\top~{}~{}=\lnot\bot$. Then $H(\top)=B$ and is called _the external top_.

  * •

$\mathord{\text{NB}}=\lnot\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}$. Then
$H(\text{NB})=\\{\bot\\}^{C}=\set{x}{x\neq\bot}$ and is called the _not-bottom
constant_.

Remember also that we previously defined
$\mathord{\vphantom{\top}\mathchoice{\ooalign{$\displaystyle\top$\cr\kern
1.99997pt$\displaystyle\top$}}{\ooalign{$\textstyle\top$\cr\kern
1.99997pt$\textstyle\top$}}{\ooalign{$\scriptstyle\top$\cr\kern
1.99997pt$\scriptstyle\top$}}{\ooalign{$\scriptscriptstyle\top$\cr\kern
1.99997pt$\scriptscriptstyle\top$}}}=\mathord{\vphantom{\lnot}\mathchoice{\ooalign{\raisebox{0.86108pt}{$\displaystyle\neg$}\cr\raisebox{-0.86108pt}{$\displaystyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\textstyle\neg$}\cr\raisebox{-0.86108pt}{$\textstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptstyle\neg$}}}{\ooalign{\raisebox{0.86108pt}{$\scriptscriptstyle\neg$}\cr\raisebox{-0.86108pt}{$\scriptscriptstyle\neg$}}}}\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}$, _the internal top_ , so
$H(\mathord{\vphantom{\top}\mathchoice{\ooalign{$\displaystyle\top$\cr\kern
1.99997pt$\displaystyle\top$}}{\ooalign{$\textstyle\top$\cr\kern
1.99997pt$\textstyle\top$}}{\ooalign{$\scriptstyle\top$\cr\kern
1.99997pt$\scriptstyle\top$}}{\ooalign{$\scriptscriptstyle\top$\cr\kern
1.99997pt$\scriptscriptstyle\top$}}})=\\{\top\\}$.

Note however that the interpretations of some of these constants may coincide
for some algebras ${\mathcal{P}}B$. This observation underlies the failure of
canonicity for single algebras explored in section 3.1.

###  4.2 Closures

We define two useful closure operators with corresponding semantic
interpretation for every Boolean algebra $B$ and every homomorphism
$H:\mathtt{Fm}\to{\mathcal{P}}B$:

  * •

$\mathop{\downarrow}\varphi=\varphi\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}\top$.
Then $H(\mathop{\downarrow}\varphi)=\set{b\in B}{\text{there exists }a\in
H(\varphi),\text{ s.t. }b\leq a}$, called the downwards closure operator.

  * •

$\mathop{\uparrow}\varphi=\varphi\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\top$.
Then $H(\mathop{\uparrow}\varphi)=\set{b\in B}{\text{there exists }a\in
H(\varphi),\text{ s.t. }b\geq a}$, called the upwards closure operator.

For elements of a Boolean algebra we use the standard understanding of $a\leq
b$, as $a\land b=a$.

Note that the closure operators are projections in the sense that
$H(\mathop{\downarrow}\mathop{\downarrow}\varphi)=H(\mathop{\downarrow}\varphi)$.
Furthermore, $\top$ and $\bot$ are their only common fix-points:
$H(\mathop{\downarrow}\bot)=H(\bot)=H(\mathop{\uparrow}\bot)$. We also have
the following properties:

$\displaystyle H(\mathop{\downarrow}\varphi)=\emptyset\text{ iff
}H(\varphi)=\emptyset,\text{ and otherwise }\bot\in
H(\mathop{\downarrow}\varphi),$ $\displaystyle
H(\mathop{\uparrow}\varphi)=\emptyset\text{ iff }H(\varphi)=\emptyset,\text{
and otherwise }\top\in H(\mathop{\uparrow}\varphi),$ $\displaystyle
H(\mathop{\downarrow}\varphi)=B\text{ iff }\top\in H(\varphi),\text{ and}$
$\displaystyle H(\mathop{\uparrow}\varphi)=B\text{ iff }\bot\in H(\varphi).$

We will now use these properties to define modal operators.

###  4.3 Modal operators

We define a possibility operator $\Diamond$ such that for all formulas
$\varphi$, algebras ${\mathcal{P}}B$, and all homomorphisms $H$,

$H(\Diamond\varphi)=\begin{cases}B&\text{if there exists }x\in
H(\varphi)\text{, and}\\\ \emptyset&\text{otherwise.}\end{cases}$

Similarly, we consider a necessity operator $\Box$, such that

$H(\Box\varphi)=\begin{cases}B&\text{if for all }x,x\in H(\varphi)\text{,
and}\\\ \emptyset&\text{otherwise.}\end{cases}$

Inspecting the described properties of the closure operators
$\mathop{\downarrow}$ and $\mathop{\uparrow}$ it is clear that these
connectives can be defined in the following manner.

######  Definition 4.1.

For any algebra ${\mathcal{P}}B$ we define the universal and existential
operators $\Box$ and $\Diamond$ as follows:

$\displaystyle\Diamond\varphi$
$\displaystyle=\mathop{\uparrow}\mathop{\downarrow}\varphi=(\varphi\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}\top)\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\top$
$\displaystyle\Box A$ $\displaystyle=\lnot\Diamond\lnot A$

As a sidenote we can observe that viewing a Boolean algebra $B$ as a Kripke
frame, we have defined the universal modal operators, we can therefore
conclude:

###### Proposition 4.2

The fragment $(\bot,\lnot,\lor,\land,\Box,\Diamond)$ of LT is exactly the
modal logic S5.

###### Proof.

Note that the interpretations of the connectives mentioned in the above
proposition do not depend on the underlying, or internal, structure of
${\mathcal{P}}B$, and the underlying Boolean algebra $B$ functions merely as
‘a set of worlds’ with $\Box$ and $\Diamond$ interpreted using the universal
accessibility relation, and is logically equivalent to any other universal
Kripke frame of the same cardinality. Furthermore, every universal Kripke
model is logically equivalent to a Kripke model generated from it by
duplicating some worlds to an arbitrary degree. We can therefore always find a
logically equivalent model with the same cardinality as some Boolean algebra.
∎

The $\Box$ operation however plays a more important role in this paper in that
it facilitates internalisation into formulas of classifications of important
global properties of homomorphism, see section 5.

###  4.4 Implication

Not surprisingly we define external implication as

$\varphi\to\psi=\lnot\varphi\lor\psi.$

With standard Boolean considerations it is then easy to see that the deduction
theorem holds in LT for this external implication.

######  Theorem 4.3 (Deduction theorem for LT)

For all $\Delta\cup\set{\varphi,\psi}\subseteq\mathtt{Fm}$

$\Delta,\varphi\vDash\psi\quad\text{iff}\quad\Delta\vDash\varphi\to\psi.$

###  4.5 Strict negation

When we in Section 6 relate LT to other team semantics described in the
literature, we will consider a third type of negation. We will denote this
negation by $\mathord{{\sim}}$ and start by introducing the operation on an
algebra ${\mathcal{P}}B$.

######  Definition 4.4.

For subset $A$ and an element $b$ of a Boolean algebra $B$ we say that $b$ is
_separate_ from $A$ if for all $a\in A$, $b\land a=\bot$. We define
$\mathord{{\sim}}A$ as the set of all elements separate from $A$, i.e.,

$\mathord{{\sim}}A=\set{b\in B}{\text{for all }a\in A,b\land a=\bot}.$

This operation is definable as an operation in LT, and we call it strict
negation:

######  Definition 4.5.

In LT we define the unary operation $\mathord{{\sim}}$ by

$\mathord{{\sim}}\varphi=\lnot\mathop{\uparrow}(\mathop{\downarrow}\varphi\land\mathord{\text{NB}}).$

###### Theorem 4.6

For every Boolean algebra $B$, every homomorphism
$H:\mathtt{Fm}\to{\mathcal{P}}B$, and every formula $\varphi\in\mathtt{Fm}$ we
have

$H(\mathord{{\sim}}\varphi)=\mathord{{\sim}}H(\varphi).$

###### Proof.

We first convince ourselves that for any algebra, homomorphism and formula as
prescribed we have

$H(\mathop{\downarrow}\varphi\land\mathord{\text{NB}})=\set{a\in
B}{a\neq\bot\text{ and }a\leq b\text{ for some }b\in H(\varphi)}.$

Therefore
$H(\mathop{\uparrow}(\mathop{\downarrow}\varphi\land\mathord{\text{NB}}))$ is
the set of elements of $B$ that have non-trivial intersection with some
element in $H(\varphi)$, i.e

$H(\mathop{\uparrow}(\mathop{\downarrow}\varphi\land\mathord{\text{NB}}))=\set{a\in
B}{a\land b\neq\bot\text{ for some }b\in H(\varphi)}.$

This is exactly the complement of $\mathord{{\sim}}H(\varphi)$, and thus

$H(\mathord{{\sim}}\varphi)=H(\lnot\mathop{\uparrow}(\mathop{\downarrow}\varphi\land\mathord{\text{NB}}))=\mathord{{\sim}}H(\varphi).$

∎

The purpose of defining strict negation in this paper is to identify the
relation between LT and more traditional propositional team semantics defined
by teams of valuations. However, we also want to acknowledge the following
properties of $\mathord{{\sim}}$ in LT.

###### Theorem 4.7

  1. 1.

$\vDash P\to\mathord{{\sim}}\mathord{{\sim}}P$

  2. 2.

$\nvDash\mathord{{\sim}}\mathord{{\sim}}P\to P$

  3. 3.

$\vDash\mathord{{\sim}}\mathord{{\sim}}\mathord{{\sim}}P\rightarrow\mathord{{\sim}}P$

  4. 4.

$\nvDash
P\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\mathord{{\sim}}P$

  5. 5.

$\nvDash\mathord{{\sim}}P\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\mathord{{\sim}}\mathord{{\sim}}P$

###### Proof of statements (1)-(3).

For a semantic proof of (1) we need to show that for any Boolean algebra $B$
and any $A\subset B$ we have that
$A\subseteq\mathord{{\sim}}\mathord{{\sim}}A$. In other words, if $a\in A$
then for all $b\in\mathord{{\sim}}A$ we have that $a\land b=\bot$, which is
guaranteed by definition of $\mathord{{\sim}}A$.

As a simple proof of statement (2), consider for any Boolean algebra a
homomorphism $H$ such that $H(P)=\emptyset$. Then
$H(\mathord{{\sim}}\mathord{{\sim}}P)=\set{\bot}$. Clearly then
$H(\mathord{{\sim}}\mathord{{\sim}}P)\nsubseteq H(P)$ and the statement is
asserted.

For (3) assume for some $A\subseteq B$ that
$b\in\mathord{{\sim}}\mathord{{\sim}}\mathord{{\sim}}A$. Then for all $a\in
A$, by the semantic proof of (1) we have that
$a\in\mathord{{\sim}}\mathord{{\sim}}A$, and thus $b\land a=\bot$, and thus
$b\in\mathord{{\sim}}A$. Hence
$\mathord{{\sim}}\mathord{{\sim}}\mathord{{\sim}}A\subseteq\mathord{{\sim}}A$.
This proves statement (3).

Statement (4) is a direct consequence of Theorem 6.3 below.

For (5) let $B$ be a non-complete Boolean algebra $B$ and $H(P)$ such that
$\bigvee H(P)\notin B$. Then by the proof of Theorem 6.3 it is clear that
$\top\notin
H(\mathord{{\sim}}P\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\mathord{{\sim}}\mathord{{\sim}}P)$.
∎

That $\nvDash
P\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\mathord{{\sim}}P$
will be important when axiomatising proposiitonal dependence logic,
$\text{PT}^{+}$, in LT. Statement (5) indicates that $\mathord{{\sim}}$ is not
an intuitionistic negation, at least not together with
$\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}$.

Statement (1) can also be proven using the natural deduction system given in
Section 2.1, but since the statement includes many defined connectives the
proof trees become fairly large. The statement is written directly without
defined connectives as

$\vDash\neg
P\lor\lnot((([\lnot(((P\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}\lnot\bot)\land\lnot\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}})\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\lnot\bot)]\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}\lnot\bot)\land\lnot\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}})\mathrel{\vphantom{\land}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\leqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\leqslant$}}}}}\lnot\bot).$

Figure 1 gives a derivation in the proof system showing the related proof-
theoretic statement

$a\mathbin{:}P\vdash a\mathbin{:}\mathord{{\sim}}\mathord{{\sim}}P,$

using defined connectives as notational abbreviations.

$a\mathbin{:}\mathord{{\sim}}\mathord{{\sim}}Pa\mathbin{:}\bot\lx@proof@logical@and[a\mathbin{:}\mathop{\uparrow}(\mathop{\downarrow}\mathord{{\sim}}P\land\mathord{\text{NB}})]^{1}a\mathbin{:}\bot\lx@proof@logical@and[p\mathbin{:}\mathop{\downarrow}\mathord{{\sim}}P\land\mathord{\text{NB}}]^{2}a\mathbin{:}\bot
s\mathbin{:}\bot\lx@proof@logical@and[s\mathbin{:}\mathord{{\sim}}P]^{3}s\mathbin{:}\mathop{\uparrow}(\mathop{\downarrow}P\land\mathord{\text{NB}})(s\land
r)\lor(s\land q)\lor(s\land\lnot(r\lor
q))\mathbin{:}\mathop{\uparrow}(\mathop{\downarrow}P\land\mathord{\text{NB}})\lx@proof@logical@and(s\land
r)\lor(s\land
q)\mathbin{:}\mathop{\downarrow}P\land\mathord{\text{NB}}\lx@proof@logical@and(s\land
r)\lor(s\land q)\mathbin{:}\mathop{\downarrow}P((s\land r)\lor q)\land
s\mathbin{:}\mathop{\downarrow}P\lx@proof@logical@and(s\land r)\lor
q\mathbin{:}P\lx@proof@logical@and a=(s\land r)\lor
q\lx@proof@logical@and[a=p\lor q]^{2}[p=s\land
r]^{3}a\mathbin{:}Ps\mathbin{:}\top[s\mathbin{:}\bot](s\land r)\lor(s\land
q)\mathbin{:}\mathord{\text{NB}}(s\land r)\mathbin{:}\bot\lx@proof@logical@and
s\land r\mathbin{:}\mathord{\text{NB}}\lx@proof@logical@and[p=s\land
r]^{3}p\mathbin{:}\mathord{\text{NB}}[p\mathbin{:}\mathop{\downarrow}\mathord{{\sim}}P\land\mathord{\text{NB}}]^{2}(s\land
r)\mathbin{:}\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}\lnot\lnot(s\land
r)\mathbin{:}\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}\lnot(s\land
r)\mathbin{:}\mathord{\vphantom{\top}\mathchoice{\ooalign{$\displaystyle\top$\cr\kern
1.99997pt$\displaystyle\top$}}{\ooalign{$\textstyle\top$\cr\kern
1.99997pt$\textstyle\top$}}{\ooalign{$\scriptstyle\top$\cr\kern
1.99997pt$\scriptstyle\top$}}{\ooalign{$\scriptscriptstyle\top$\cr\kern
1.99997pt$\scriptscriptstyle\top$}}}\lnot((s\land r)\lor(s\land
q))\mathbin{:}\mathord{\vphantom{\top}\mathchoice{\ooalign{$\displaystyle\top$\cr\kern
1.99997pt$\displaystyle\top$}}{\ooalign{$\textstyle\top$\cr\kern
1.99997pt$\textstyle\top$}}{\ooalign{$\scriptstyle\top$\cr\kern
1.99997pt$\scriptstyle\top$}}{\ooalign{$\scriptscriptstyle\top$\cr\kern
1.99997pt$\scriptscriptstyle\top$}}}[(s\land r)\lor(s\land
q)\mathbin{:}\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}]s\land\lnot(r\lor
q)\mathbin{:}\top[s\land\lnot(r\lor q)\mathbin{:}\bot]$

Figure 1: Derivation showing that $a:P\vdash
a:\mathord{{\sim}}\mathord{{\sim}}P$. Here $\mathtt{taut}/\mathtt{sub}$ is a
shorthand for a combination of $\mathtt{taut}$ and $\mathtt{sub}$.

##  5 Definable classes of homomorphisms

The semantic definition of entailment in LT is given as a universal
satisfaction of a property evaluated independently for all homomorphisms for
all Boolean algebras. Just like how, in terms of Kripke models, semantics for
intuitionistic logic is given by a restriction on valuations to those
satisfying a persistence criteria, we are interested in logics that can be
defined by a restriction on the class of homomorphisms that are considered. We
also describe a notion of definability in LT of such classes, and by using the
$\Box$ operator obtain axiomatisations in LT of the logics of definable
classes of homomorphisms, defined by restricting quantification over a class
of homomorphisms.

######  Definition 5.1.

Let $H$ be a homomorphism $\mathtt{Fm}\to{\mathcal{P}}B$. We define the _local
entailment_ of $H$ denoted $H:\Delta\vDash\varphi$ in the expected way:

$H:\Delta\vDash\varphi\quad\text{ iff
}\quad\bigcap_{\delta\in\Delta}H(\delta)\subseteq H(\varphi).$

Given a class of homomorphisms $\mathcal{H}$ (not necessarily all to the same
algebra), we define the logic of the class-entailment

$\mathcal{H}:\Delta\vDash\varphi\text{ iff for all
}H\in\mathcal{H},H:\Delta\vDash\varphi.$

A class of homomorphisms is definable if there is a set of formulas that are
valid precisely for the homomorphisms of that class.

######  Definition 5.2.

A class of homomorphisms $\mathcal{H}$ is definable in LT if there exists a
set of formulas $\Pi$ such that for all homomorphisms
$H:\mathtt{Fm}\to{\mathcal{P}}B$,

$H\in\mathcal{H}\quad\text{iff }\quad H:~{}\vDash\pi\text{ for all
}\pi\in\Pi.$

Note that to axiomatise the logic of a class of homomorphisms it is not enough
to take a defining set of formulas $\Pi$ as axioms. The reason is that
definability imposes a global condition on homomorphism, whereas the
entailment is a local condition. As a simple example, consider the class
$\mathcal{H}_{\text{tr}}$ of homomorphisms onto the powerset of the trivial
Boolean algebra ${\mathcal{P}}B=\set{1}$. It is clear that this class is
defined by the formula:
$\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}$

$H\in\mathcal{H}_{\text{tr}}\quad\text{iff}\quad
H:~{}\vDash\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}.$

On the other hand we have that

$\mathcal{H}_{\text{tr}}:~{}\vDash\mathord{\vphantom{\top}\mathchoice{\ooalign{$\displaystyle\top$\cr\kern
1.99997pt$\displaystyle\top$}}{\ooalign{$\textstyle\top$\cr\kern
1.99997pt$\textstyle\top$}}{\ooalign{$\scriptstyle\top$\cr\kern
1.99997pt$\scriptstyle\top$}}{\ooalign{$\scriptscriptstyle\top$\cr\kern
1.99997pt$\scriptscriptstyle\top$}}}\quad\text{but}\quad\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}\nvDash\mathord{\vphantom{\top}\mathchoice{\ooalign{$\displaystyle\top$\cr\kern
1.99997pt$\displaystyle\top$}}{\ooalign{$\textstyle\top$\cr\kern
1.99997pt$\textstyle\top$}}{\ooalign{$\scriptstyle\top$\cr\kern
1.99997pt$\scriptstyle\top$}}{\ooalign{$\scriptscriptstyle\top$\cr\kern
1.99997pt$\scriptscriptstyle\top$}}}.$

However, by using the universal modality $\Box$, we can internalise global
conditions and ensure that

$x\in H(\Box\eta)\quad\text{ iff}\quad H(\eta)=B.$

That is, for all $x\in B$,

$x\in H(\Box\eta)\quad\text{iff}\quad H:~{}\vDash\eta.$

We can then conclude the following theorem:

###### Theorem 5.3

Assume a class of homomorphisms $\mathcal{H}$ is defined by a set of formulas
$\Pi$ and let $\Box\Pi=\set{\Box\pi}{\pi\in\Pi}$. Then

$\Box\Pi,\Delta\vDash\varphi\quad\text{ iff
}\quad\mathcal{H}:\Delta\vDash\varphi,$

so that $\Box\Pi$ serves as an axiomatization in LT of the logic defined by
the restriction to homomorphisms of the class $\mathcal{H}$.

This usage of $\Box$ also serves the purpose to relate the semantics of LT to
standardly considered algebraic semantics (see for example [Font16]), in which
$H(\top)$ is the special designated value corresponding to truth:

###### Theorem 5.4

$\Box\varphi\vDash\psi$ iff for all homomorphisms $H$, $H(\varphi)=H(\top)$
implies $H(\psi)=H(\top)$.

##  6 Axiomatising valuational team semantics

In this section we show how standard team semantics based on valuations relate
to the logic LT. This construction follows in essence the construction
presented in [LorimerOlsson2022] with some refinements and generalisations.
The construction and proof will be developed through the following steps,
enumerated by the corresponding subsection.

  1. 6.1.

We start by defining the propositional team logic $\text{PT}^{+}$ in terms of
its standard semantics, here referred to as valuational team semantics, by
defining its denotations in terms of collections of teams of valuations. This
is an expressive logic with many interesting logics as syntactic fragments.

  2. 6.2.

Then we show how to formulate this semantics in terms of the algebra
${\mathcal{P}}{\mathcal{P}}2^{\mathbb{N}}$ with a specific homomorphism
$H_{V}$ in the style of the semantics we have given for LT. We can then prove
that LT is in a sense a conservative extension of a logic weaker than
$\text{PT}^{+}$.

  3. 6.3.

Next we observe that the homomorphism $H_{V}$ belongs to a special class of
homomorphisms $\mathcal{H}_{\text{PV}}$ that are nicely definable and
axiomatisable in LT using defined connectives from Section 4.

  4. 6.4.

We can then show that the axiomatisation of this class axiomatises
$\mathrm{PT}^{+}$ as a fragment of LT. This is done by essentially showing
that for the restricted language of $\mathrm{PT}^{+}$ the homomorphism $H_{V}$
is canonical for the logic of the whole class $\mathcal{H}_{\mathrm{PV}}$. The
proof includes two main steps expressed in two separate lemmas:

     * •

Lemma 6.8 states that for embeddings of Boolean algebras all homomorphism in
$\mathcal{H}_{\text{PV}}$ to the domain of the embedding, can be paired with
homomorphism in $\mathcal{H}_{\text{PV}}$ to the co-domain such that
memberhood in interpretations of formulas of $\text{PT}^{+}$ are preserved by
the embedding. This together with Stone’s theorem establishes that the
complete atomic Boolean algebras are adequate for the logic of the class
$\mathcal{H}_{\text{PV}}$.

     * •

Lemma 6.11 then establishes that every homomorphism in
$\mathcal{H}_{\mathrm{PV}}$ with a complete atomic Boolean algebra as co-
domain can be represented by the homomorphism
$H_{V}:\mathtt{Fm}\to{\mathcal{P}}2^{\mathbb{N}}$ in such a way that $H_{V}$
expresses the memberhood of the original homomorphism by the mapping for
interpretations of formulas in $\text{PT}^{+}$.

With these lemmas together we conclude that $\text{PT}^{+}$ is axiomatised as
a fragment of LT by the axioms of the class of homomorphisms.

In this section we will treat several logics defined for different sets of
connectives, and thus with different sets of formulas. For a logic L we denote
by $\mathtt{Fm}_{\text{L}}$ the formulas of the logic and
$\text{L}:\Delta\vDash\varphi$ for the entailment of the logic. In particular,
the formulas of LT will be referred to as $\mathtt{Fm}_{\text{LT}}$, and its
entailment will be denoted by $\text{LT}:\Delta\vDash\varphi$ in contrast to
other sections of this paper.

###  6.1 Valuational team semantics

We are interested in formulating a logic in a sense generalising some
propositional team logics given in team semantics where the notion of team
refers to sets of valuations being the basic semantic object. We call this
valuational team semantics. We represent the valuational team semantics by
recursively defining the denotation of formulas on the set of teams of
valuations ${\mathcal{P}}2^{\mathbb{N}}$. In order to cover a majority of the
more interesting logics we focus our attention on strong propositional team
logic, $\text{PT}^{+}$, one of the strongest logics presented in [Yang2017].

######  Definition 6.1.

The set of formulas $\mathtt{Fm}_{\text{PT}^{+}}$ of _Strong propositional
team logic_ , $\text{PT}^{+}$, is generated by the following grammar

$\varphi::=P_{i}\mathrel{|}\mathord{{\sim}}P_{i}\mathrel{|}\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}\mathrel{|}\mathord{\text{NB}}\mathrel{|}\varphi\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\varphi\mathrel{|}\varphi\land\varphi\mathrel{|}\varphi\lor\varphi$

and its valuational team semantics can be described by defining the
denotations for formulas
$\llbracket\varphi\rrbracket\subseteq{\mathcal{P}}2^{\mathbb{N}}$ recursively
for cases of the main connective as follows:

$\displaystyle\llbracket P_{i}\rrbracket$ $\displaystyle=\set{X}{\text{for all
}s\in X,s(i)=1}$ $\displaystyle\llbracket\mathord{{\sim}}P_{i}\rrbracket$
$\displaystyle=\set{X}{\text{for all }s\in X,s(i)=0}$
$\displaystyle\llbracket\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}\rrbracket$
$\displaystyle=\set{\emptyset}$
$\displaystyle\llbracket\mathord{\text{NB}}\rrbracket$
$\displaystyle=\set{X}{X\neq\emptyset}$
$\displaystyle\llbracket\varphi\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\psi\rrbracket$
$\displaystyle=\set{X\cup
Y}{X\in\llbracket\varphi\rrbracket,Y\in\llbracket\psi\rrbracket}$
$\displaystyle\llbracket\varphi\land\psi\rrbracket$
$\displaystyle=\llbracket\varphi\rrbracket\cap\llbracket\psi\rrbracket$
$\displaystyle\llbracket\varphi\lor\psi\rrbracket$
$\displaystyle=\llbracket\varphi\rrbracket\cup\llbracket\psi\rrbracket$

The logical entailment of $\text{PT}^{+}$ is then defined as follows:

$\text{PT}^{+}:\Delta\vDash\varphi\quad\text{iff}\quad\bigcap_{\delta\in\Delta}\llbracket\delta\rrbracket\subseteq\llbracket\varphi\rrbracket.$

Elements $s\in 2^{\mathbb{N}}$ are viewed as valuations for the set of
propositional variables, and sets of valuations
$X\in{\mathcal{P}}2^{\mathbb{N}}$ are referred to as teams (of valuations).

There is no standard notation for the connectives in the literature, and we
have chosen notation that corresponds best to the notation for LT. Table 1
indicates the correspondence between our notation and notation elsewhere.

[Yang2017] | [Lueck2020] | [Yang2022] | This paper
---|---|---|---
$p_{i}$ | $p_{i}$ | $p_{i}$ | $P_{i}$
$\neg$ | $\neg$ | $\neg$ | $\mathord{{\sim}}$
$\bot$ | $\bot$ | $\bot$ | $\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern 1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern 1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern 1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern 1.99997pt$\scriptscriptstyle\bot$}}}$
$\otimes$ | $\vee$ | $\vee$ | $\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}$
$\wedge$ | $\wedge$ | $\wedge$ | $\land$
$\vee$ | $\ovee$ | $\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}$ | $\lor$
NE |  |  | $\mathord{\text{NB}}$
Table 1: Correspondence between notations in the current paper and other
relevant papers on propositional team logics.

As defined, it is clear that for the set of formulas, including defined
connectives, we have that
$\mathtt{Fm}_{\text{PT}^{+}}\subset\mathtt{Fm}_{\text{LT}}$ even though the
logics are described using different semantics. In this section we will find
axioms in the language of LT that axiomatises $\text{PT}^{+}$ in LT. In the
literature there are multiple weaker propositional team logics described and
studied, in particular propositional logics of dependence [Yang2016]. Many
important logics, however, are given as, or is expressively equivalent to,
logics that can be given as fragments of $\text{PT}^{+}$. This means that our
result regarding the axiomatisation of $\text{PT}^{+}$ in LT will be directly
applicable to these logics too. Table 2 gives an overview of these weaker
logics that can be found in the literature. The logic $\text{PD}^{\vee}$ is
described in [Yang2016], and the others are described in [Yang2017].

Propositional team logics. | Connectives
---|---
Classical propositional logic (CPL) | $\mathord{{\sim}}P_{i},\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern 1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern 1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern 1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern 1.99997pt$\scriptscriptstyle\bot$}}},\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}},\land$
Strong classical propositional logic ($\text{CPL}^{+}$) | $\mathord{{\sim}}P_{i},\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern 1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern 1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern 1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern 1.99997pt$\scriptscriptstyle\bot$}}},\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}},\land,\mathord{\text{NB}}$
Propositional union closed logic (PU) | $\mathord{{\sim}}P_{i},\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern 1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern 1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern 1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern 1.99997pt$\scriptscriptstyle\bot$}}},\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}},\land,\circledast$
Strong propositional union closed logic ($\text{PU}^{+}$) | $\mathord{{\sim}}P_{i},\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern 1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern 1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern 1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern 1.99997pt$\scriptscriptstyle\bot$}}},\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}},\land,\circledast,\mathord{\text{NB}}$
Propositional dependence logic w. int. disj. ($\text{PD}^{\vee}$) | $\mathord{{\sim}}P_{i},\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern 1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern 1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern 1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern 1.99997pt$\scriptscriptstyle\bot$}}},\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}},\land,\lor$
Propositional team logic (PT) | $\mathord{{\sim}}P_{i},\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern 1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern 1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern 1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern 1.99997pt$\scriptscriptstyle\bot$}}},\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}},\land,\lor,\circledast$
Strong propositional team logic ($\text{PT}^{+}$) | $\mathord{{\sim}}P_{i},\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern 1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern 1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern 1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern 1.99997pt$\scriptscriptstyle\bot$}}},\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}},\land,\lor,\mathord{\text{NB}}$
Table 2: Names and included connectives of logics described in [Yang2016] and
[Yang2017] as fragments of $\text{PT}^{+}$. The connective $\circledast$ can
be defined in $\text{PT}^{+}$ as
$\varphi\circledast\psi:=(\varphi\land\mathord{\text{NB}})\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}(\psi\land\mathord{\text{NB}})$.
By $\mathord{{\sim}}P_{i}$ we mean that $\mathord{{\sim}}$ is only allowed to
be applied to propositional variables.

###  6.2 $\text{PT}^{+}$ as a model of LT

Observe that the denotations of valuational team semantics are elements of the
set ${\mathcal{P}}{\mathcal{P}}2^{\mathbb{N}}$, which can be interpreted as a
model of LT by interpreting ${\mathcal{P}}2^{\mathbb{N}}$ as a Boolean algebra
using the standard set operations. We will refer to this as the valuation
model. With this reading we can see that the interpretation of atomic formulas
imposes a specific homomorphism that maps every atomic formula to the set of
teams for which every member evaluates it to true.

Define the valuation homomorphism
$H_{V}:\mathtt{Fm}_{\text{LT}}\to{\mathcal{P}}{\mathcal{P}}2^{\mathbb{N}}$ as
the unique homomorphism such that

$H_{V}(P_{i})=\set{X\in{\mathcal{P}}2^{\mathbb{N}}}{\text{ for all }s\in
X,s(i)=1}={\mathcal{P}}\set{s\in 2^{\mathbb{N}}}{s(i)=1}.$

Thus,

$H_{V}:\Delta\vDash\varphi\quad\text{iff}\quad\bigcap_{\delta\in\Delta}H_{V}(\delta)\subseteq
H_{V}(\varphi).$

Let us formulate this in the following theorem.

###### Theorem 6.2

For all formulas
$\Delta\cup\\{\varphi\\}\subseteq\mathtt{Fm}_{\mathrm{PT}^{+}}$:

$\mathrm{PT}^{+}:\Delta\vDash\varphi\quad\text{ iff }\quad
H_{V}:\Delta\vDash\varphi.$

Hence, if $\text{LT}:\Delta\vDash\varphi$, then
$\mathrm{PT}^{+}:\Delta\vDash\varphi$.

###  6.3 Axiomatising a specific class of homomorphisms

We observe that the valuation homomorphism $H_{V}$ has the following special
property.

$H_{V}(P_{i})={\mathcal{P}}X\text{ for some }X\in{\mathcal{P}}2^{\mathbb{N}}$

Algebraically speaking, every propositional variable is mapped to a non-empty
principal ideal of the Boolean algebra on ${\mathcal{P}}(2^{\mathbb{N}})$,
that is, a subset $A$ of the Boolean algebra $B$ such that there is a maximal
element $a\in A$ generating $A$, i.e., such that

$A=\set{b\in B}{b\leq a}.$

In other words, $A$ is downwards closed and $\bigvee A\in A$.

We can in fact express the property of being a principal ideal in LT in the
following formula akin to the excluded middle:

###### Theorem 6.3

For all Boolean algebras $B$, all homomorphism
$H:\mathtt{Fm}\to{\mathcal{P}}B$, and all formulas $\varphi\in\mathtt{Fm}$ we
have

$H:~{}\vDash\varphi\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\mathord{{\sim}}\varphi\quad\text{
if and only if }H(\varphi)\text{ is a principal ideal}$

As part of proving this statement we will use a small result that will be
useful to refer to multiple times in upcoming proofs. We therefore state it as
a separate lemma.

###### Lemma 6.4

For a Boolean algebra $B$, if $A\subseteq{\mathcal{P}}B$ is a principal ideal
with maximal element $a\in B$, then $\mathord{{\sim}}A$ is a principal ideal
with maximal element $\lnot a$.

###### Proof of lemma.

First note that for all $A\subseteq B$ we have that $\mathord{{\sim}}A$ is
downwards closed, since if $c\leq c^{\prime}\in\mathord{{\sim}}A$ then for all
$b\in A$, $b\land c\leq b\land c^{\prime}=\bot$. What is left to show is that,
if $a=\bigvee A$, then $\neg a=\bigvee\mathord{{\sim}}A$. Clearly, for all
$a^{\prime}\in A$ we have $a^{\prime}\land a=a^{\prime}$ and thus $\lnot
a\land a^{\prime}=\bot$, and thus $\lnot a\in\mathord{{\sim}}A$. Furthermore,
if $b\in\mathord{{\sim}}A$, then $a\land b=\bot$ and therefore $\lnot a=\lnot
a\lor(a\land b)=\lnot a\lor b$. i.e $b\leq\lnot a$. thus $\lnot a$ is an upper
bound of $\mathord{{\sim}}A$ included in the set, and thus the set is a
principal ideal, and $\lnot a=\bigvee\mathord{{\sim}}A$. ∎

###### Proof of Theorem 6.3.

For one direction, assume
$H(\varphi\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\mathord{{\sim}}\varphi)=B$,
we then need to prove that $H(\varphi)$ is a principal ideal. First we
establish that it is downwards closed. In search of a contradiction, assume
that for some $a\in H(\varphi)$ we can find $b\in B$ such that $b\leq a$ and
$b\notin H(\varphi)$. We want to show that then $b\notin
H(\varphi\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\mathord{{\sim}}\varphi)$.
If $b\in
H(\varphi\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\mathord{{\sim}}\varphi)$,
then there exists $c\in H(\varphi)$ and $d\in\mathord{{\sim}}H(\varphi)$ such
that $c\lor d=b$. Since $b\leq a\in H(\varphi)$ we have that

$b\land d\leq a\land d=\bot$

since $d\in\mathord{{\sim}}H(\varphi)$. But then, since clearly $c\leq b$, we
have

$b=b\land b=(c\lor d)\land b=(c\land b)\lor(b\land d)=c\in H(\varphi)$

This is a contradiction. We can therefore conclude, under the main assumption,
that $H(\varphi)$ is downwards closed. Next we show that $\bigvee
H(\varphi)\in H(\varphi)$. By assumption we have that

$\top\in
H(\varphi\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\mathord{{\sim}}\varphi)$

Then there exists $c\in H(\varphi)$ and $d\in H(\mathord{{\sim}}\varphi)$ such
that $c\lor d=\top$. Furthermore, for all $a\in H(\varphi)$ we have that

$a=\top\land a=(c\lor d)\land a=c\land a,$

since $d\land a=\bot$ for all $a\in H(\varphi)$. Consequently $a\leq c$ for
all $a\in H(\varphi)$ and thus $c$ is an upper bound for $H(\varphi)$ included
in the set, i.e. $c=\bigvee H(\varphi)$. With downwards closure established,
this also means that $H(\varphi)$ is a principal ideal.

For the other direction, assume $H(\varphi)$ is a principal ideal. Then there
exists $a\in B$ such that $a$ is the top element of $H(\varphi)$. Then by
Lemma 6.4 we see that $\lnot a$ is the top element of the principal ideal
$H(\mathord{{\sim}}\varphi)$. Therefore, since $a\lor\neg a=\top$ we have for
every $b\in B$ that

$b=b\land(a\lor\neg a)=(b\land a)\lor(b\land\neg a).$

Being the top elements of the respective principal ideals we observe that

$b\land a\in H(\varphi)\quad\text{and}\quad b\land\neg a\in
H(\mathord{{\sim}}\varphi)$

and conclude that
$H(\varphi\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\mathord{{\sim}}\varphi)=B$,
in other words
$H\vDash\varphi\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\mathord{{\sim}}\varphi$.
∎

From this theorem we can directly conclude for the valuation homomorphism
$H_{V}$ that

$H_{V}:{}\vDash
P_{i}\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\mathord{{\sim}}P_{i}\quad\text{for
all }i\in\mathbb{N}.$

We will see that this is the crucial categorisation of the homomorphisms that
relate to valuational team logics. We therefore identify the class defined by
these formulas, and the corresponding axiomatisation as discussed in Section
5.

######  Definition 6.5.

Let $\mathcal{H}_{\text{PV}}$ denote the class of homomorphisms defined by
$\set{P_{i}\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\mathord{{\sim}}P_{i}}{i\in\mathbb{N}}$.
We say that a homomorphism $H$ has principal variables iff
$H\in\mathcal{H}_{\text{PV}}$. Furthermore, let _the principal variable
axioms_ be the set

$\text{PVA}=\set{\Box(P_{i}\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}P_{i})}{i\in\mathbb{N}}.$

It follows directly from Theorem 5.3 that, for all
$\Delta,\set{\varphi}\subseteq\mathtt{Fm}_{\text{LT}}$,

$\mathcal{H}_{\text{PV}}:\Delta\vDash\varphi\quad\text{if and only
if}\quad\text{LT}:\text{PVA},\Delta\vDash\varphi.$

It is evident that $H_{V}\in\mathcal{H}_{\text{PV}}$.

###  6.4 Axiomatisation of $\text{PT}^{+}$ as a fragment

In this section we prove that the axioms PVA axiomatise $\text{PT}^{+}$ in the
sense of the following theorem.

###### Theorem 6.6

For all $\Delta\cup\\{\varphi\\}\subseteq\mathtt{Fm}_{\mathrm{PT}^{+}}$

$\mathrm{PT}^{+}:\Delta\vDash\varphi\quad\text{iff}\quad\mathrm{LT}:\mathrm{PVA},\Delta\vDash\varphi.$

One direction is already proved by Theorem 5.3 and 6.2. To prove the other
direction we first recall the fundamental result by Stone in the theory of
Boolean algebras.

######  Theorem 6.7 ([Halmos2009])

Every Boolean algebra can be embedded into a complete atomic Boolean algebra
of the form $({\mathcal{P}}S,\emptyset,\cdot^{C},\cup,\cap)$ for some set $S$.

Using this theorem we can establish Theorem 6.6 in a two step process. First
showing that any homomorphism $H\in\mathcal{H}_{PV}$ can be faithfully
represented by a homomorphism in a Boolean algebra of subsets, and then that
any such homomorphism can be represented by the specific valuational
homomorphism $H_{V}:\mathtt{Fm}\to{\mathcal{P}}{\mathcal{P}}2^{\mathbb{N}}$.
These steps are established below in Lemma 6.8 and Lemma 6.11 respectively.
Both proofs are similar in structure, where the statement is proven by
induction over the complexity of formulas in $\mathrm{PT}^{+}$ for which
particular care is needed to handle the internal connective
$\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}$.
In the first case this invokes the formulation of an additional sub-lemma, and
in the second case it suffices with a simpler result expressed as a claim.

###### Lemma 6.8

Let $B,B^{\prime}$ be Boolean algebras, and $e:B\hookrightarrow B^{\prime}$ an
embedding of Boolean algebras. Then for each homomorphism
$H:\mathtt{Fm}_{\text{LT}}\to{\mathcal{P}}B$ with principal variables there is
a homomorphism $H^{\prime}:\mathtt{Fm}_{\text{LT}}\to{\mathcal{P}}B^{\prime}$
with principal variables such that for all formulas
$\varphi\in\mathtt{Fm}_{\text{PT}^{+}}$

$b\in H(\varphi)\quad\text{ if and only if }\quad e(b)\in
H^{\prime}(\varphi).$

###### Proof.

Assume $H:\mathtt{Fm}\to{\mathcal{P}}B$ has principal variables. Thus, for all
$i$ there exists $b_{i}\in B$ such that

$H(P_{i})=\set{a\in B}{a\leq b_{i}}.$

We then define $H^{\prime}:\mathtt{Fm}\to{\mathcal{P}}B^{\prime}$ as the
homomorphism that maps each propositional variable $P_{i}$ to the principal
ideal of $e(b_{i})$, i.e.,

$H^{\prime}(P_{i})=\set{a^{\prime}\in B^{\prime}}{a^{\prime}\leq e(b_{i})}.$

Clearly, $H^{\prime}$ has principal variables, so what is left to show is that
the equivalence in the theorem holds for all $b\in B$ and all formulas
$\varphi$ of PT+. In order to do so, we need an additional lemma best
described using the notation of Boolean intervals.555The introduction of
Boolean intervals in this context is inspired by their usage in [Hella2023] in
which minimal covers of Boolean intervals are used to define complexity
measures for expressions in first-order team semantics. Even if our usage is
noticeably different, the proof construction we present for forming included
covering intervals is strongly related to the constructive methods of
generating minimal interval covers for collections of teams satisfying a
formula presented in that paper.

######  Definition 6.9.

In a Boolean algebra $B$, if $a,b\in B$ and $a\leq b$, then let
$[a,b]\subseteq B$ denote the set of elements between $a$ and $b$, that is

$[a,b]=\set{c\in B}{a\leq c\text{ and }c\leq b}.$

We call this the closed interval of $a$ and $b$, and if $a=b$ we may write
$[a]$ instead of $[a,a]$.

######  Lemma 6.10 (Interval lemma)

For all Boolean algebras $B,B^{\prime}$, Boolean embedding $e:B\hookrightarrow
B^{\prime}$, homomorphisms $H:Fm\to{\mathcal{P}}B$ and the generated
homomorphism $H^{\prime}:\mathtt{Fm}\to{\mathcal{P}}B^{\prime}$ as described
above, we have that for all $\varphi\in\mathtt{Fm}_{\text{PT}^{+}}$ and all
$b^{\prime}\in B^{\prime}$, if $b^{\prime}\in H^{\prime}(\varphi)$, then there
is a $b\in B$ such that $b^{\prime}\leq e(b)$ and $[b^{\prime},e(b)]\subseteq
H^{\prime}(\varphi)$.

###### Proof.

We prove this statement for all $b\in B$ by induction over the complexity of
formulas. Let $b_{i}$ denote the generating element of the principal ideal
$H(P_{i})$.

  * •

Assume
$\varphi=\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}$. Then $b^{\prime}\in
H^{\prime}(\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}})$ only if $b^{\prime}=\bot=e(\bot)$, and
thus $[b^{\prime},e(\bot)]=[\bot]\subseteq
H^{\prime}(\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}})$.

  * •

Assume $\varphi=\mathord{\text{NB}}$. Then if $b^{\prime}\in
H^{\prime}(\mathord{\text{NB}})$ clearly $[b^{\prime},e(\top)]\subseteq
H^{\prime}(\mathord{\text{NB}})$.

  * •

Assume $\varphi=P_{i}$. If $b^{\prime}\in H^{\prime}(P_{i})$, then
$b^{\prime}\leq e(b_{i})$ and, since $H^{\prime}(P_{i})$ is a principal ideal,
clearly $[b^{\prime},e(b_{i})]\subseteq H^{\prime}(P_{i})$.

  * •

Assume $\varphi=\mathord{{\sim}}P_{i}$. By Lemma 6.4 and a similar argument as
for the previous case we can conclude that if $b^{\prime}\in
H^{\prime}(\mathord{{\sim}}P_{i})$ then $[b^{\prime},e(\lnot b_{i})]\subseteq
H^{\prime}(\mathord{{\sim}}P_{i})$.

  * •

Assume $\varphi=\psi\land\chi$. If $b^{\prime}\in H^{\prime}(\varphi)$, then
$b^{\prime}\in H^{\prime}(\psi)$ and $b^{\prime}\in H^{\prime}(\chi)$. by
induction, we may find $b_{\psi},b_{\chi}\in B$ such that
$[b^{\prime},e(b_{\psi})]\subseteq H^{\prime}(\psi)$ and
$[b^{\prime},e(b_{\chi})]\subseteq H^{\prime}(\chi)$. Since $e$ is a
homomorphism

$[b^{\prime},e(b_{\psi}\land b_{\chi})]\subseteq H^{\prime}(\varphi).$

  * •

$\varphi=\psi\lor\chi$. If $b^{\prime}\in H^{\prime}(\varphi)$, then
$b^{\prime}\in H^{\prime}(\psi)$ or $b^{\prime}\in H^{\prime}(\chi)$, and
without loss of generality we may assume the former. By induction hypothesis
there is some $b_{\psi}\in B$ such that $[b^{\prime},e(b_{\psi})]\subseteq
H^{\prime}(\psi)$, and thus $[b^{\prime},e(b_{\psi})]\subseteq
H^{\prime}(\varphi)$.

  * •

$\varphi=\psi\mathrel{\vphantom{\lor}\mathchoice{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\displaystyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\textstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptstyle\geqslant$}}}}{\ooalign{\raisebox{0.6458pt}{\rotatebox[origin={c}]{-90.0}{$\scriptscriptstyle\geqslant$}}}}}\chi$.
If $b^{\prime}\in H^{\prime}(\varphi)$, then there is $c^{\prime}\lor
d^{\prime}=b^{\prime}$ such that $c^{\prime}\in H^{\prime}(\psi)$ and
$d^{\prime}\in H^{\prime}(\chi)$. By induction hypothesis, we can then find
$b_{\psi},b_{\chi}\in B$ such that $[c^{\prime},e(b_{\psi})]\subseteq
H^{\prime}(\psi)$ and $[d^{\prime},e(b_{\chi})]\subseteq H^{\prime}(\chi)$.
Then since $b^{\prime}=c^{\prime}\lor d^{\prime}$ and $e$ is a homomorphism,
it is easy to see that

$H^{\prime}(\varphi)\supseteq\set{p\lor
q}{p\in[c^{\prime},e(b_{\psi})],q\in[d^{\prime},e(b_{\chi})]}=[b^{\prime},e(b_{\psi}\lor
b_{\chi})].$

This concludes the proof of the interval lemma. ∎

Now we are ready to finish the proof of Lemma 6.8. Again this is achieved for
all $b\in B$ by induction over the complexity of formulas.

  * •

Assume
$\varphi=\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}}$. First note that $b\in
H(\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}})$ if and only if $b=\bot\in B$ and
$b^{\prime}\in
H^{\prime}(\mathord{\vphantom{\bot}\mathchoice{\ooalign{$\displaystyle\bot$\cr\kern
1.99997pt$\displaystyle\bot$}}{\ooalign{$\textstyle\bot$\cr\kern
1.99997pt$\textstyle\bot$}}{\ooalign{$\scriptstyle\bot$\cr\kern
1.99997pt$\scriptstyle\bot$}}{\ooalign{$\scriptscriptstyle\bot$\cr\kern
1.99997pt$\scriptscriptstyle\bot$}}})$ if and only if $b^{\prime}=\bot\in
B^{\prime}$. Then note that $e(\bot)=\bot\in B^{\prime}$ by $e$ being a
homomorphism, and by $e$ being injective $e(b)=\bot$ if and only if $b=\bot\in
B$. These observations suffice to prove the statement.

  * •

Assume $\varphi=\mathord{\text{NB}}$. Since regardless of homomorphism and