=Paper=
{{Paper
|id=Vol-2347/paper4
|storemode=property
|title=Team Semantics for Spatial Reasoning: Locality and Separability
|pdfUrl=https://ceur-ws.org/Vol-2347/paper4.pdf
|volume=Vol-2347
|authors=Pietro Galliani
|dblpUrl=https://dblp.org/rec/conf/c3gi/Galliani18
}}
==Team Semantics for Spatial Reasoning: Locality and Separability==
https://ceur-ws.org/Vol-2347/paper4.pdf
Team Semantics for Spatial Reasoning:
Locality and Separability
Pietro GALLIANI a,1 ,
a Free University of Bozen-Bolzano, Italy
Abstract. Team Semantics is a generalization of Tarski’s semantics for First Order
Logic in which formulas are satisfied or not satisfied by sets of assignments. De-
spite being reducible to Tarskian semantics over First Order Logic, Team Seman-
tics permits to extend it in novel ways, like for instance by means of new types of
atoms that express dependencies between different assignments.
In this work I will discuss the applicability of Team Semantics to spatial reason-
ing. I will argue that Team Semantics is a highly appropriate framework for rea-
soning about notions such as locality, in which the value of some variable at some
point is affected only by the values of other variables in a certain neighbourhood of
that point, and separability of spaces into regions with different properties.
Keywords. Team Semantics, Dependence Logic, Spatial Logic, Locality
1. Introduction
Team Semantics [30] generalizes Tarski’s usual semantics for First Order Logic by let-
ting formulas be satisfied or not satisfied by sets of assignments (called Teams for histori-
cal reasons), rather than by single assignments. This semantics was originally introduced
in order to find a compositional semantics that is equivalent to the game-theoretical se-
mantics for Independence-Friendly Logic [28,29,41], an extension of First Order Logic
– roughly equivalent to Branching Quantifier Logic [27] – which allows for more general
patterns of dependence and independence between quantifiers.
With Väänänen’s development of Dependence Logic [44], however, it became clear
that Team Semantics is a powerful and valuable generalization of Tarskian semantics
in its own right, independently from its original application to Independence-Friendly
Logic. Within the framework of Team Semantics it is possible to extend the language
of First Order Logic by adding operators or atoms that express dependencies between
multiple assignments, which is of course impossible in Tarskian Semantics. In partic-
ular, in terms of Team Semantics Independence-Friendly Logic – the original motiva-
tion for its development – is in very close correspondence with the logic obtained by
adding to First Order Logic functional dependence atoms, whose semantics correspond
precisely to database-theoretic functional dependencies [1]. It was soon recognized that
other database-theoretic notions can be similarly added to the First Order Logic via Team
1 E-mail: pietro.galliani@unibz.it.
Semantics [23,11,19], and the study and classification of the logics obtained in this way
has blossomed into one of the central topics of research in the area.
The same type of “lifting” operation that leads from Tarskian First Order semantics
to Team Semantics can be also applied to other forms of compositional semantics, such as
those of Propositional Logic [47,48], Modal Logic [45,9,7,33], Computation Tree Logic
(CTL) [36] and more recently Linear Temporal Logic (LTL) [37]. This later work, in
particular, showed that by generalizing the semantics of LTL to sets of traces it is possible
to obtain an effective framework for the specification of hyperproperties (i.e. system
properties – such as “the system terminates within a bounded amount of time” – that
cannot be verified by considering each possible trace in isolation but only by considering
the set of all possible traces as a whole). This framework is incomparable with HyperLTL
[4], the most common extension of LTL for the specification of hyperproperties; it can
express properties of practical importance, such as uniform termination, which cannot be
expressed in it; and it has better computational properties (in particular, the satisfiability
problem for HyperLTL is undecidable [13] whereas the one for Team LTL is in PSPACE).
In contrast to this interest in the use of variants of Team Semantics for the specifi-
cation and verification of temporal dependencies, to my knowledge there has been sur-
prisingly little research on the use of Team Semantics for the specification of spatial de-
pendencies. Yet, those dependencies certainly do exist and are of considerable practical
interest: to mention one possible example, the results of geological surveys within a cer-
tain radius from some site of potential interest in Central Asia may be useful to predict
the existence or non-existence of oil in it, but the results of surveys in New Zealand or in
Argentina likely are of no immediate relevance for that.
This work constitutes an exploration of the possibilities of Team Semantics as a
framework for the specification and verification of spatial dependencies. Rather than
starting from a spatial logic and ”teamifying” it in the usual way (i.e. by lifting the
semantics to sets of the relevant meaning-carrying entities), here we will begin from
the usual – and well-studied – Team Semantics of First Order Logic and add spatial
information to it. In this way, we will obtain a formalism that is capable of expressing
sophisticated spatial dependencies but is still very close to the usual first order Team
Semantics.2 This has clear advantages, as this semantics has been the object of intense
research in the last few years, in particular insofar as the study and classification of
computationally treatable fragments (see e.g. [32,8,16,17,26,18,40]) and proof systems
(see e.g. [35,25,39]) are concerned; and it is the hope of the author that the present work
will showcase the possibilities of Team Semantics in this context.
2. Preliminaries: Team Semantics
In this section, we will briefly recall the definition of (first order) Team Semantics, as well
as some basic results regarding its properties. As we will see, for First Order Logic proper
Team Semantics is reducible, in a very strong sense, to the usual Tarskian semantics;
however, the greater richness of the meaning-carrying entities (which will be sets of
assignments, called Teams for historical reasons, rather than single assignments), as well
as the higher order quantification implicit in the rules TS-∨ and TS-∃ for disjunction
2 In fact, it will not be difficult to see that it will be reducible to two-sorted first order Team Semantics.
and existential quantification, make it possible to make use of Team Semantics to extend
First Order Logic in novel and interesting ways.
2.1. Definitions
Definition 1 (Team). Let M be a first order model with domain M, and let V ⊆ Var be a
finite set of variables. A Team over M with domain V is a set of assignments s : V → M.
Definition 2 (Splitting). Let X, Y and Z be teams over a model M with the same domain
Dom(X) = Dom(Y ) = Dom(Z) = V . Then we say that X splits into Y and Z if X = Y ∪ Z.
In general, in the above definition we do not require Y and Z to be disjoint.3 We will
also need to be able to talk about updates of a team along one variable:
Definition 3 (Restriction). Let X be a team over a model M with domain Dom(X), and let
V ⊆ Dom(X) be a subset of its variables. Then its restriction X|V is the team {s|V : s ∈ X}
of the restrictions of its assignments to V , where for each s ∈ X we have that s|V is the
assignment with domain V such that s|V (v) = s(v) for all s ∈ V .
Definition 4 (Team Update). Let X be a team over a model M with domain Dom(X), let
v ∈ Var be any variable, and let Y be a team over the same M with domain Dom(X) ∪ {v}.
Then we say that Y is an update (or supplementation) of X along v if X and Y agree on
all variables aside from v, that is, if and only if X|Dom(X)\{v} = Y|Dom(X)\{v} .
The following result is trivial:
Proposition 1. Let X be a team over a model M with domain Dom(X), let v ∈ Var be
any variable and let Y be a team over the same M with domain Dom(X) ∪ {v}. Then Y is
an update of X along v if and only if there exists a function F, sending each assignment
s ∈ X into a nonempty set of elements F(s) ⊆ M, F(s) 6= 0, / such that
Y = X[F/v] = {s[m/v] : s ∈ X, m ∈ F(s)}
where s[m/v] agrees with s on Dom(s)\{v} and sends v to m.
A particular type of team update that will be useful to consider is the most general
update of a team along a variable, also called the duplication of a team along a variable:
Definition 5 (Most General Update). Let X be a team over a model M with domain
Dom(X), let v be a variable (not necessarily in Dom(X)) and let Y be a team over the same
M with domain Dom(X) ∪ {v}. Then Y is the most general update of X along v if
1. Y is an update of X along v;
2. For all updates Y 0 of X along v we have that Y 0 ⊆ Y .
3 This is related to the distinction between lax and strict semantics [14], or - in game theoretical terms - to
the distinction between nondeterministic and deterministic properties. Much of the recent work in the area has
focused on the lax (not-necessarily-disjoint) case, essentially because in the other the value of a formula may
be affected by the values of variables that do not appear in it.
xy
xy xy
s0 a b
= s0 a b ∪ s1 a c
s1 a c
s1 a c s2 b c
s2 b c
xy
s000 a a
xy
x x" , # s001 a b
" , #
s00 7→ {b, c} s0 a b
s00 a y = s00 a M y = s002 a c
s01 7→ {c} s1 a c
s01 b s01 b s003 b a
s2 b c
s004 b b
s005 b c
Figure 1. Splitting, Update and Most General Update over a model M with domain M = {a, b, c}.
Proposition 2. Let X be a team over a model M with domain Dom(X) and let v a vari-
able. Then the most general update of X along v exists, is unique, and is given by
X[M/v] = {s[m/v] : s ∈ X, m ∈ M}.
We now have all ingredients to define the Team Semantics over First Order Logic.
We will assume, for simplicity, that all expressions are in Negation Normal Form:
Definition 6 (Team Semantics for First Order Logic). Let M be a first order model with
domain M, let X be a team over it, and let φ (~x) be a first order formula in Negation
Normal Form over the signature of M and with free variables in Dom(X). Then we say
that X satisfies φ in M, and we write M |=X φ , if and only if this follows from the rules
TS-lit: For all first order literals α, M |=X α if and only if, for all assignments s ∈ X,
M |=s α in the sense of the usual Tarskian Semantics;
TS-∨: For all NNF formulas φ and ψ, M |=X φ ∨ ψ if and only if X = Y ∪ Z for two
subteams Y and Z such that M |=Y φ and M |=Z ψ;
TS-∧: For all NNF formulas φ and ψ, M |=X φ ∧ψ if and only if M |=X φ and M |=X ψ;
TS-∃: For all NNF formulas φ and all variables v ∈ Var, M |=X ∃vφ if and only if there
exists some update X[F/v] of X along v such that M |=X[F/v] φ ;
TS-∀: For all NNF formulas φ and all variables v ∈ Var, M |=X ∀vφ if and only if
M |=X[M/v] φ for the most general update X[M/v] of X along v.
If φ has no free variables, we say that φ is true in M according to Team Semantics
if and only if M |={ε} φ where ε : 0/ → M is the empty assignment.
2.2. Some Results
As mentioned before, over First Order Logic proper Team Semantics is reducible to
Tarskian Semantics. More precisely, the following result holds:
Proposition 3. Let M be a first order model, let X be a team over it, and let φ be a first
order formula in Negation Normal Form over the signature of M and with free variables
in Dom(X). Then M |=X φ if and only if, for all s ∈ X, M |=s φ according to the usual
rules of Tarski’s semantics. In particular, if φ is a sentence, φ is true in M according to
Team Semantics if and only if it is true in M according to Tarskian Semantics.
Does this result imply that Team Semantics is an unnecessarily complicated, but fun-
damentally equivalent, variant of Tarskian Semantics? Well, no: as already mentioned,
the richer structure of teams over assignments allows one to extend First Order Logic
with Team Semantics in novel ways that have no obvious analogue in Tarskian seman-
tics. Perhaps the easiest – and certainly the most studied – way to do so is to add to the
language of First Order Logic new dependency atoms, expressing dependencies between
the values that variables take in different assignments, like the following ones:
Definition 7 (Functional Dependence, Inclusion, Exclusion, and Independence Atoms).
For all models M, all teams X and all tuples of variables4 ~x and ~y,
TS-fdep: M |=X =(~x;~y) if any two s, s0 ∈ X which agree on ~x also agree on ~y;
TS-inc: M |=X ~x ⊆ ~y if the tuples ~x and ~y have the same length and, furthermore, every
possible value of ~x in X is also a possible value for ~y in X;
TS-exc: M |=X ~x|~y if the tuples ~x and ~y have the same length and, furthermore, no pos-
sible value of ~x in X is also a possible value for ~y in X;
TS-ind: M |=X ~x⊥~y if for any s, s0 ∈ X there exists some s00 ∈ X with s00 (~x) = s(~x) and
s00 (~y) = s0 (~y) (that is, all possible values for ~x and ~y in X may occur together in it).
The logics obtained by adding these atoms to the language of First Order Logic
are called (functional) Dependence Logic, Inclusion Logic, Exclusion Logic and (non-
conditional) Independence Logic5 respectively, and they are formalisms deserving of
investigation in their own right. Here we mention briefly that every sentence of func-
tional dependence, exclusion, or independence logic is equivalent to some sentence of
existential second order logic Σ11 , and that conversely every Σ11 sentence is equivalent to
some sentence of any of these logics [44,24,14]; but that, on the other hand, Inclusion
Logic corresponds to the positive fragment of Greatest Fixed Point Logic [20], and hence
captures PTIME over finite ordered models by [31,46]. On the level of formulas, how-
ever, independence logic differs from functional and exclusion logic (which are however
equivalent): very briefly, it was proved that every Σ11 -definable property of teams6 that is
true of the empty team corresponds to the satisfaction conditions to some Independence
Logic formula, and vice versa [14], whereas for functional and exclusion logic the above
is true only if we further require that these relations are additionally downwards closed
(i.e., whenever they hold of a team they also hold of all its subteams [34]).
Team Semantics allows also to extend First Order Logic in new ways via extra
connectives, such as the contradictory negation ∼ (such that M |=X ∼ φ if and only if
M 6|=X φ – note, this is not equivalent to the usual “dual negation”) or various types of
generalized quantifier [10,12,38,2]; and furthermore, “weighted” or probabilistic vari-
ants of Team Semantics have been also considered [43,21,5,6].
4 Or, more in general, terms; but for simplicity we will only consider dependence atoms applied to variables.
5 There are also conditional independence atoms ~x⊥ ~y, which state that the possible values of ~x and ~y in X
~z
are informationally independent for any fixed value of~z; but as pointed out in [22], these atoms can be defined
in terms of non-conditional independence atoms.
6 Or, to be more precise, every Σ1 -definable property of the relations corresponding to teams.
1
2.3. The Doxastic Interpretation of Team Semantics
As briefly shown above, Team Semantics is a natural generalization of Tarskian Seman-
tics which is of significant theoretical interest, as it makes it possible to extend First Or-
der Logic in novel ways (the classification of which is still largely incomplete). However,
some uncertainty would be understandable at this point regarding the meaning of Team
Semantics. What are teams, exactly? The rules of Definition 6 may well arise naturally
from the analysis of non-deterministic strategies in the Game-Theoretic Semantics of
First Order Logic, and they may well be appropriate for providing a compositional se-
mantics for logics such as Branching Quantifier Logic or Independence-Friendly Logic;
but do they have an actual and understandable meaning, or are they mere technical tricks
of a semantics that – regardless of its nice formal features – does not admit much of an
interpretation? This is a question that is of central importance for this work, since we
intend to discuss the applicability of Team Semantics to spatial reasoning.
As it was discussed at length in [15], and as we will now briefly see, Team Semantics
admits a natural interpretation in terms of doxastic states. If an assignment represents a
potential state of things, a team can easily represent the belief set of an agent – that is, the
set of all states of things that an agent believes possible. Then Proposition 3, for instance,
can be interpreted as showing that, for all first order φ , M |=X φ if and only if an agent
that believes that the true state of things lies in X can be sure that φ will be true of this
true state; a functional dependence atom =(~x;~y) states that the agent could infer the true
value of ~y from the true value of ~x; inclusion and exclusion atoms ~x ⊆ ~y and ~x|~y assert
respectively that the agent considers every possible value of~x a possible/impossible value
for ~y; and an independence atom ~x⊥~y asserts that learning the true value of ~x would
provide the agent with no new information whatsoever regarding the value of ~y.
Splitting a team into two as per rule TS-∨ can be seen as a form of case-based
reasoning: if the agent believes that the true state is in X = Y ∪ Z, they can conclude that
the true state is in Y or in Z (or possibly in both). Note that this would not be the case for
the “Boolean disjunction”
TS-t: M |=X φ t ψ iff M |=X φ or M |=X ψ
which would instead assert that, knowing that the true state is in X, the agent can con-
clude that φ is true or that ψ is true. In other words, the difference between φ ∨ ψ and
φ t ψ is the same as that between K(φ ∨ ψ) (“the agent knows that φ or ψ is true”) and
K(φ ) ∨ K(ψ) (“the agent knows that φ is true or the agent knows that ψ is true”). Thus,
for instance, x = y ∨ x 6= y is satisfied by any team whose domain contains the variables
x and y, but there are teams (for instance, X = {(x : 0, y : 0), (x : 0, y : 1)}) which do not
satisfy x = y t x 6= y. By combining splitting and dependency atoms we can obtain inter-
esting effects: for example, =(x; y)∨ =(x; y) is not equivalent to =(x; y), and it asserts
that any value of x corresponds to at most two values of y – or, to put the matter into more
explicitly doxastic terms, that the agent believes that two scenarios are possible, and that
in either scenario they could learn y given x.
What about quantifiers and variable updates? By definition, M |=X ∃vφ if and only
if there exists some possible belief state Y , which disagrees from X at most with respect
to the variable v, in which φ holds. In other words, the agent could learn something about
the possible values of the variable v – but about that variable alone – after which they
would agree that φ holds. The most general update X[M/v], on the other hand, represents
an “agnostic update” after which the agent believes that the variable v could take any
value at all regardless of the values of the other variables; and thus, M |=X ∀vφ if this
agent – after disregarding anything about the value of v – believes that φ .
Conjunctions and first order literals pose no difficulties; and, thus, we obtained a
doxastic interpretation for all expressions of our language. This interpretation can be ex-
tended much further, and we refer to [15] for more details. We now have enough back-
ground to begin exploring the application of Team Semantics to spatial reasoning.
3. Spatial Team Semantics
As we just discussed, the assignments in a team can be understood as possible states of
things, or equivalently as possible (and not necessarily consistent) observations. It is thus
entirely natural to think of these observations as located into space. This can be done
easily by adding a special location variable ` 6∈ Var to all assignments:
Definition 8 (Located Assignments). Let M be a first order model with domain M, let
V ⊆ Var be a finite set of variables and let H be an arbitrary real Hilbert Space7 . A H-
located assignment over M with domain V is a function s : V ∪ {`} → M ∪ H, where
s(`) ∈ H and s(v) ∈ M for all v ∈ V .
Definition 9 (Located Teams, Location Range). Let M be a first order model with do-
main M, let V ⊆ Var and let H be a real Hilbert Space. Then a H-located team over M
with domain V is a set X of H-located assignments over M with domain V . Its location
range X(`) is the set {s(`) : s ∈ X} ⊆ H of the positions of all its assignments.
The doxastic interpretation of Section 2.3 can be extended to located teams in the
obvious way: in brief, a located team still represent a set of possible observations, but
now each observation is also situated in a particular point of the space H (see e.g. Figure
2). The semantics of Definition 6, as well as the dependency atoms of Definition 7 and
all the other operators and connectives studied in the context of Team Semantics, can
be applied to located teams without any change whatsoever; however, the fact that every
assignment is now made to correspond to a particular point of H allows us to consider
new kinds of operators and dependencies over located teams. For example, one may note
that we did not require that distinct assignments have different positions (this can be used
to represent e.g. ambiguous data about a location). However, a simple dependence atom
can be added to state that the values of certain variables are spatially determined:
TS-sdet: M |=X =(`;~x) iff, for any two s, s0 ∈ X, if s(`) = s0 (`) then s(~x) = s0 (~x).
This spatial determination operator is obviously just a minor variant of the functional
dependency atom of Definition 7; and we may likewise add an “independence atom” `⊥x
to state that the range of the possible values for x is the same for any possible location `.
Can we do anything else with locations? Well, to begin with, let us consider the dis-
junction operator. As before, the interpretation is clear: M |=X φ ∨ ψ if we can split the
set of located observations X into two (possibly overlapping) subsets Y and Z that satisfy
7 For most intended applications, we can assume that H = R2 or H = R3 , but the definitions of this work
apply equally well to the case of a general Hilbert space over R.
1
ℓ v1 v2 v3 s3 , s4
s0 (0.2, 0.4) 1 0 1
s1 (0.2, 0.4) 1 1 0
X = s2 (0.6, 0.2) 2 1 0 y s5
s3 (0.5, 0.9) 3 0 1
s0 , s1
s4 (0.5, 0.9) 3 1 0
s5 (0.7, 0.6) 3 1 0 s2
0 x
0 1
Figure 2. A R2 -located team with domain {v1 , v2 , v3 } over a model M with four elements 0, 1, 2 and 3. Note
that M |=X =(`; v1 ), because any two assignments that are in the same position agree about v1 ; M 6|=X =(`; v2 ),
because for example s0 and s1 have the same position but disagree about v2 ; M |=X =(`; v2 ) ⊗un v3 = 0, because
we can split X into Y = {s0 , s2 , s3 , s5 } and Z = {s1 , s2 , s4 , s5 } and we have that X(`) = Y (`) = Z(`) (no location
is lost in any subteam), M |=Y =(`; v2 ) (in Y , the value of v2 is a function of the position) and M |=Z v3 = 0
(v3 is 0 for all assignments of Z); and M |=X `⊥v2 ⊗lin v1 6= v2 , because the linear operator h : R2 → R given
by h(x, y) = y + 0.5 − 2x separates X into two other regions Y 0 = {s ∈ X : h(s(`)) ≥ 0} = {s0 , s1 , s3 , s4 } and
Z 0 = {s ∈ X : h(s(`)) < 0} = {s2 , s5 } such that M |=Y 0 `⊥v2 (in Y 0 , the set of all the possible values of v2 is the
same – that is, {0,1} – in all positions) and M |=Z 0 v1 6= v2 .
the conditions described by φ and ψ respectively. This remains a perfectly legitimate
connective, with obvious uses – for example, an expression of the form =(`; x)∨ =(`; x)
will say that every location corresponds to at most two values for the variable x. How-
ever, the fact that each assignment has a location permits us to think about how this lo-
cation affects which “sides” of a split an assignment would be put into. Many possible
choices can be considered here, and we will just mention two simple ones that are of ob-
vious interest: on one hand, we might want to require that the split is independent on the
location, so that both Y and Z contain assignments in all locations in which X contains
assignments, and on the other we might want instead to require that Y and Z are linearly
separable on the basis of location. This justifies the two following new connectives (see
Figure 2 and its caption for examples):
Definition 10 (Location-Uniform and Linear Splits). For any model M, real Hilbert
space H, H-located team X over M, and formulas φ , ψ over the signature of M and with
free variables in Dom(X),
TS-⊗un : M |=X φ ⊗un ψ if and only if there exist two H-located teams Y, Z ⊆ X such
that Y (`) = Z(`) = X(`), Y ∪ Z = X, M |=Y φ and M |=Z ψ;8
TS-⊗lin : M |=X φ ⊗lin ψ if and only if there exists a linear operator h : H → R such that,
for Y = {s ∈ X : h(s(`)) ≥ 0} and Z = {s ∈ X : h(s(`)) < 0}, it holds that M |=Y φ
and M |=Z ψ.
What else? Quite a bit. For example, we might want to say that the value of a variable
in a location is determined by the values of certain other variables inside some range:
8 As an aside, it is not difficult to see that this is essentially a spatial version of the value-preserving disjunc-
tions of [42], and as such it can be defined in terms of independence atoms.
ℓ v1 v2 1
s0 (0.20, 0.40) 0 1 s7
s1 (0.35, 0.45) 1 1 s8
s2 (0.30, 0.30) 2 1 s6
s (0.55, 0.20) 0 0 s5 s4
X= 3 y
s4 (0.70, 0.60) 2 1
s1
s5 (0.56, 0.60) 0 0 s0
s6 (0.63, 0.74) 1 1 s2
s7 (0.70, 0.90) 2 2 s3
s8 (0.90, 0.80) 3 3 0
0 x 1
Figure 3. Local similarity. The locations of the table on the left are approximated to two decimals.
s2 ∼(X,v1 ,0.2) s4 : indeed, there exists an orthogonal transformation (a rotation by −π/4) that corresponds to
sending s4 to s2 , s5 to s0 and s6 to s1 , and each of these pairs agree on v1 . The values and locations of s3 , s7
and s8 are irrelevant, because their distances from s2 and s4 is more than 0.2. Note, furthermore, that it is not
true that s2 ∼(X,v1 v2 ,0.2) s4 , because s0 and s5 disagree about the value of v2 .
Definition 11 (Local Restriction). Let H be a real Hilbert space and let X be a H-located
team over some model M, and let s ∈ X be a located assignment of X. Furthermore, let
δ ∈ (0, ∞) be a positive real number, and let V ⊆ Dom(X) be a set of variables in the
domain of X. Then the (V, δ )-local restriction of X around s is the located team
X|V,δ ,s = {s0|V [s0 (`) − s(`)/`] : s0 ∈ X, d(s0 (`), s(`)) ≤ δ }
where, as usual, s0|V is the restriction of s to the variables of V (as well as `); d(p, q) =
p
kp − qk = hp − q, p − qi is the distance associated to H via its inner product h·, ·i; and
we subtracted the location of s from the coordinates of all points so that s lies at the
origin of X|V,δ ,s .9
Definition 12 (Local Similarity). Let H be a real Hilbert space, let X be a H-located
team over some M and let s, s0 ∈ X. Furthermore, let δ ∈ (0, ∞) and let V ⊆ Dom(X).
Then we say that s and s0 are (V, δ )-locally similar in X, and we write s ∼(X,V,δ ) s0 , if
and only if there exist an orthogonal operator10 o : X|V,δ ,s (`) → X|V,δ ,s0 (`) and a function
h from X|V,δ ,s onto X|V,δ ,s0 such that h(s) = s0 and such that, for all s00 ∈ X|V,δ ,s .
1. s00 (v) = h(s00 )(v) for all v ∈ V (h preserves the values of the variables in V );
2. o(s00 (`)) = h(s00 )(`) (h transforms the locations according to o).
If ~x is a tuple of (possibly repeating) variables, we will write s ∼(X,~x,δ ) s0 as a shorthand
for s ∼(X,Var(~x),δ ) s0 , where Var(~x) = {v ∈ Var : v occurs in ~x}.
See Figure 3 for a simple example of local similarity in a R2 -located team. Now we
can define the following local dependency atom, having range δ ∈ (0, ∞):
9 This is so that in Definition 12 we will not need to worry about translations.
10 Very briefly, this means that o preserves inner products (and, consequently, also norms and distances). An
example of such an operator in Rn would be a rotation or a reflection; some non-examples would be a scaling
operation, a translation, or any non-continuous transformation. If we wanted to exclude reflections, it would
suffice to require that o belongs in the group SO(H) of the orientation-preserving orthogonal operators for H.
ℓ m t r
s0 0 0.5 2.5 L r=H t>6
s1 1 0.8 4.5 M
s2 2 1.2 5.5 M r=M 4 6), medium (M, if 4 < t ≤ 6), or low (L, if t ≤ 4). The local depen-
dency =(o : 2.0; r) holds by construction, since s(r) does not depend on the values of s0 (m) for |s(`)−s0 (`)| > 2.
However, =(o : 1.0; r) fails: for instance, s1 ∼(X,m,1) s7 (pick h(s0 ) = s8 , h(s1 ) = s7 and h(s2 ) = s6 – note, this
corresponds to a reflection o : X|o,1.0,s1 (`) → X|o,1.0,s7 (`)), but s1 and s7 do not agree on r.
TS-locdep: M |=X =(~x : δ ;~y) if, for any two s, s0 ∈ X, if s ∼(X,~x,δ ) s0 then s(~y) = s0 (~y).
According to the above definition, M |=X =(~x : δ ;~y) if and only if any two local assign-
ments whose δ -neighbourhoods are the same (up to orthogonal transformations, e.g. ro-
tations or reflections) insofar as the values of the variables in ~x are concerned must also
agree about the value of ~y. Figure 4 shows a toy example of such a dependency in the
case of risk assessment via seismographic data analysis.
All of this could be generalized in several ways: for instance, it would not be difficult
to let tuples of variables ~x1 . . .~xn influence the value of ~y within different radii δ1 . . . δn ,
or we could weaken the similarity condition by allowing a certain degree of “error”
in the mappings of the locations. However, the above should suffice to exemplify the
possibilities of team semantics insofar as spatial reasoning is concerned. We leave a
more detailed examination of the possibilities – and, most importantly, of the limitations
and the computational costs of various choices of connectives, atoms and operators – to
future work.
4. Conclusions
In this work, we explored some of the possible ways in which the formalism of Team
Semantics could be used to model spatial reasoning. Of course, this is a very preliminary
sort of work, intended essentially to showcase the possibilities of such an approach and
– hopefully – to convince the reader that this is a research direction that is worthy of
being investigated further. The obvious next steps would be to compare the expressive
properties of this type of approach to those of other formalisms for spatial reasoning and
investigate the expressive properties of particular selections of connectives of operators.
It could be also interesting to add a temporal dimension to this framework, either by
replacing assignments with traces as it was done in [37] or by adding an a special tempo-
ral parameter τ 6∈ Var ∪ {`} to each assignment, much as we added the spatial parameter
`. This second approach could perhaps be argued to be more in keeping with the original
intuitions of Team Semantics and with its doxastic interpretation, as assignments are in-
tended to represent single observations or possible states of things and the relationships
between them should be expressed in terms of dependencies; and, once again, keeping as
close as standard First Order Team Semantics as possible has the considerable advantage
of letting us make use of the not insubstantial amount of work already done in the area.
Another idea worth investigating would be the combination of such an approach with
weighted variants of Team Semantics such as the ones discussed in [5,6]. The resulting
framework would be an extremely powerful one, integrating spatial, probabilistic, and
possibly also temporal reasoning into a single package. Aside from applications in spa-
tial reasoning, such a framework could also be used for the representation and modelling
of statistical learning, for instance by using the linear split connective (and/or more so-
phisticated variants thereof) for representing concepts such as the learnability of certain
properties under certain conditions. This could also have intriguing connections with the
recent work on causal reasoning via Team Semantics by Barbero and Sandu [3].
References
[1] William W. Armstrong. Dependency Structures of Data Base Relationships. In Proc. of IFIP World
Computer Congress, pages 580–583, 1974.
[2] Fausto Barbero. Some observations about generalized quantifiers in logics of imperfect information.
arXiv preprint arXiv:1709.07301, 2017.
[3] Fausto Barbero and Gabriel Sandu. Team semantics for interventionist counterfactuals and causal de-
pendence. arXiv preprint arXiv:1712.08661, 2017.
[4] Michael R Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K Micinski, Markus N Rabe, and
César Sánchez. Temporal logics for hyperproperties. In International Conference on Principles of
Security and Trust, pages 265–284. Springer, 2014.
[5] Arnaud Durand, Miika Hannula, Juha Kontinen, Arne Meier, and Jonni Virtema. Approximation and
dependence via multiteam semantics. Annals of Mathematics and Artificial Intelligence, 83(3-4):297–
320, 2018.
[6] Arnaud Durand, Miika Hannula, Juha Kontinen, Arne Meier, and Jonni Virtema. Probabilistic team
semantics. In International Symposium on Foundations of Information and Knowledge Systems, pages
186–206. Springer, 2018.
[7] Johannes Ebbing, Lauri Hella, Arne Meier, Julian-Steffen Müller, Jonni Virtema, and Heribert Vollmer.
Extended modal dependence logic. In International Workshop on Logic, Language, Information, and
Computation, pages 126–137. Springer, 2013.
[8] Johannes Ebbing, Juha Kontinen, Julian-Steffen Mueller, and Heribert Vollmer. A fragment of depen-
dence logic capturing polynomial time. Logical Methods in Computer Science 10 (2014), Nr. 3, 10(3):3,
2014.
[9] Johannes Ebbing and Peter Lohmann. Complexity of model checking for modal dependence logic.
In Mria Bielikov, Gerhard Friedrich, Georg Gottlob, Stefan Katzenbeisser, and Gyrgy Turn, editors,
SOFSEM 2012: Theory and Practice of Computer Science, volume 7147 of Lecture Notes in Computer
Science, pages 226–237. Springer Berlin / Heidelberg, 2012.
[10] Fredrik Engström. Generalized quantifiers in dependence logic. Journal of Logic, Language and Infor-
mation, 21(3):299–324, 2012.
[11] Fredrik Engström and Juha Kontinen. Characterizing quantifier extensions of dependence logic. The
Journal of Symbolic Logic, 78(1):307–316, 2013.
[12] Fredrik Engström, Juha Kontinen, and Jouko Väänänen. Dependence logic with generalized quantifiers:
Axiomatizations. In International Workshop on Logic, Language, Information, and Computation, pages
138–152. Springer, 2013.
[13] Bernd Finkbeiner and Christopher Hahn. Deciding hyperproperties. In LIPIcs-Leibniz International
Proceedings in Informatics, volume 59. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2016.
[14] Pietro Galliani. Inclusion and exclusion dependencies in team semantics: On some logics of imperfect
information. Annals of Pure and Applied Logic, 163(1):68 – 84, 2012.
[15] Pietro Galliani. The doxastic interpretation of team semantics. In Åsa Hirvonen, Juha Kontinen, Ro-
man Kossak, and Andrés Villaveces, editors, Logic Without Borders: Essays on Set Theory, Model The-
ory, Philosophical Logic and Philosophy of Mathematics, volume 5, pages 167–191. Walter de Gruyter
GmbH & Co KG, 2015.
[16] Pietro Galliani. Upwards closed dependencies in team semantics. Information and Computation,
245:124–135, 2015.
[17] Pietro Galliani. On strongly first-order dependencies. In Dependence Logic, pages 53–71. Springer,
2016.
[18] Pietro Galliani. Safe dependency atoms and possibility operators in team semantics. In Proceedings
Ninth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2018,
Saarbrücken, Germany, 26-28th September 2018., pages 58–72, 2018.
[19] Pietro Galliani, Miika Hannula, and Juha Kontinen. Hierarchies in independence logic. In Simona
Ronchi Della Rocca, editor, Computer Science Logic 2013 (CSL 2013), volume 23 of Leibniz In-
ternational Proceedings in Informatics (LIPIcs), pages 263–280, Dagstuhl, Germany, 2013. Schloss
Dagstuhl–Leibniz-Zentrum fuer Informatik.
[20] Pietro Galliani and Lauri Hella. Inclusion Logic and Fixed Point Logic. In Simona Ronchi Della Rocca,
editor, Computer Science Logic 2013 (CSL 2013), volume 23 of Leibniz International Proceedings in
Informatics (LIPIcs), pages 281–295, Dagstuhl, Germany, 2013. Schloss Dagstuhl–Leibniz-Zentrum
fuer Informatik.
[21] Pietro Galliani and Allen L. Mann. Lottery semantics: A compositional semantics for probabilistic
first-order logic with imperfect information. Studia Logica, 101(2):293–322, 2013.
[22] Pietro Galliani and Jouko Väänänen. On dependence logic. In Johan van Benthem on Logic and Infor-
mation Dynamics, pages 101–119. Springer, 2014.
[23] Erich Grädel and Jouko Väänänen. Dependence and independence. Studia Logica, pages 1–12, 2010.
[24] Erich Grädel and Jouko Väänänen. Dependence and independence. Studia Logica, 101(2):399–410,
2013.
[25] Miika Hannula. Axiomatizing first-order consequences in independence logic. Annals of Pure and
Applied Logic, 166(1):61–91, 2015.
[26] Miika Hannula. Hierarchies in inclusion logic with lax semantics. ACM Transactions on Computational
Logic (TOCL), 19(3):16, 2018.
[27] Leon Henkin. Some Remarks on Infinitely Long Formulas. In Infinitistic Methods. Proc. Symposium on
Foundations of Mathematics, pages 167–183. Pergamon Press, 1961.
[28] Jaakko Hintikka and Gabriel Sandu. Informational independence as a semantic phenomenon. In J.E
Fenstad, I.T Frolov, and R. Hilpinen, editors, Logic, methodology and philosophy of science, pages
571–589. Elsevier, 1989.
[29] Jaakko Hintikka and Gabriel Sandu. Game-Theoretical Semantics. In Johan van Benthem and Alice T.
Meulen, editors, Handbook of Logic and Language, pages 361–410. Elsevier, 1997.
[30] Wilfrid Hodges. Compositional Semantics for a Language of Imperfect Information. Journal of the
Interest Group in Pure and Applied Logics, 5 (4):539–563, 1997.
[31] Neil Immerman. Relational queries computable in polynomial time. In Proceedings of the fourteenth
annual ACM symposium on Theory of computing, pages 147–152. ACM, 1982.
[32] Juha Kontinen, Antti Kuusisto, and Jonni Virtema. Decidable fragments of logics based on team seman-
tics. CoRR, abs/1410.5037, 2014.
[33] Juha Kontinen, Julian-Steffen Müller, Henning Schnoor, and Heribert Vollmer. Modal independence
logic. Journal of Logic and Computation, 27(5):1333–1352, 2016.
[34] Juha Kontinen and Jouko Väänänen. On definability in dependence logic. Journal of Logic, Language
and Information, 3(18):317–332, 2009.
[35] Juha Kontinen and Jouko Väänänen. Axiomatizing first-order consequences in dependence logic. Annals
of Pure and Applied Logic, 164(11):1101–1117, 2013.
[36] Andreas Krebs, Arne Meier, and Jonni Virtema. A team based variant of CTL. In Temporal Represen-
tation and Reasoning (TIME), 2015 22nd International Symposium on, pages 140–149. IEEE, 2015.
[37] Andreas Krebs, Arne Meier, Jonni Virtema, and Martin Zimmermann. Team semantics for the specifi-
cation and verification of hyperproperties. In LIPIcs-Leibniz International Proceedings in Informatics,
volume 117. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2018.
[38] Antti Kuusisto. A double team semantics for generalized quantifiers. Journal of Logic, Language and
Information, 24(2):149–191, Jun 2015.
[39] Martin Lück. Axiomatizations of team logics. Annals of Pure and Applied Logic, 169(9):928–969,
2018.
[40] Martin Lück. On the Complexity of Team Logic and Its Two-Variable Fragment. In Igor Potapov,
Paul Spirakis, and James Worrell, editors, 43rd International Symposium on Mathematical Foundations
of Computer Science (MFCS 2018), volume 117 of Leibniz International Proceedings in Informatics
(LIPIcs), pages 27:1–27:22, Dagstuhl, Germany, 2018. Schloss Dagstuhl–Leibniz-Zentrum fuer Infor-
matik.
[41] Allen L. Mann, Gabriel Sandu, and Merlijn Sevenster. Independence-Friendly Logic: A Game-Theoretic
Approach. Cambridge University Press, 2011.
[42] Raine Rnnholm. Capturing k-ary existential second order logic with k-ary inclusionexclusion logic.
Annals of Pure and Applied Logic, 169(3):177 – 215, 2018.
[43] Merlijn Sevenster and Gabriel Sandu. Equilibrium semantics of languages of imperfect information.
Annals of Pure and Applied Logic, 161(5):618–631, 2010. The Third workshop on Games for Logic
and Programming Languages (GaLoP), Galop 2008.
[44] Jouko Väänänen. Dependence Logic. Cambridge University Press, 2007.
[45] Jouko Väänänen. Modal Dependence Logic. In Krzysztof R. Apt and Robert van Rooij, editors, New
Perspectives on Games and Interaction. Amsterdam University Press, Amsterdam, 2008.
[46] Moshe Y Vardi. The complexity of relational query languages. In Proceedings of the fourteenth annual
ACM symposium on Theory of computing, pages 137–146. ACM, 1982.
[47] Fan Yang and Jouko Väänänen. Propositional logics of dependence. Annals of Pure and Applied Logic,
167(7):557–589, 2016.
[48] Fan Yang and Jouko Väänänen. Propositional team logics. Annals of Pure and Applied Logic,
168(7):1406–1441, 2017.