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. Despite being reducible to Tarskian semantics over First Order Logic, Team Semantics 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 reasoning. I will argue that Team Semantics is a highly appropriate framework for reasoning 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.
Team Semantics [
With Va¨a¨na¨nen’s development of Dependence Logic [
Semantics [
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 [
In contrast to this interest in the use of variants of Team Semantics for the specification and verification of temporal dependencies, to my knowledge there has been surprisingly little research on the use of Team Semantics for the specification of spatial dependencies. Yet, those dependencies certainly do exist and are of considerable practical interest: to mention one possible example, the results of geological surveys within a certain 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. [
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-9 for disjunction 2In 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.
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 XjV is the team fsjV : s 2 X g of the restrictions of its assignments to V , where for each s 2 X we have that sjV is the assignment with domain V such that sjV (v) = s(v) for all s 2 V .
Definition 4 (Team Update). Let X be a team over a model M with domain Dom(X ), let v 2 Var be any variable, and let Y be a team over the same M with domain Dom(X ) [ fvg. 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 XjDom(X)nfvg = YjDom(X)nfvg.
Proposition 1. Let X be a team over a model M with domain Dom(X ), let v 2 Var be any variable and let Y be a team over the same M with domain Dom(X ) [ fvg. Then Y is an update of X along v if and only if there exists a function F , sending each assignment s 2 X into a nonempty set of elements F (s) M, F (s) 6= 0/ , such that
Y = X [F =v] = fs[m=v] : s 2 X ; m 2 F (s)g where s[m=v] agrees with s on Dom(s)nfvg 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 ) [ fvg. Then Y is the most general update of X along v if
Y .
3This is related to the distinction between lax and strict semantics [
M j=s a in the sense of the usual Tarskian Semantics; TS-_: For all NNF formulas f and y, M j=X f _ y if and only if X = Y [ Z for two subteams Y and Z such that M j=Y f and M j=Z y; TS-^: For all NNF formulas f and y, M j=X f ^ y if and only if M j=X f and M j=X y; TS-9: For all NNF formulas f and all variables v 2 Var, M j=X 9vf if and only if there exists some update X [F=v] of X along v such that M j=X[F=v] f ; TS-8: For all NNF formulas f and all variables v 2 Var, M j=X 8vf if and only if
M j=X[M=v] f for the most general update X [M=v] of X along v.
If f has no free variables, we say that f is true in M according to Team Semantics if and only if M j=feg f where e : 0/ ! M is the empty assignment.
As mentioned before, over First Order Logic proper Team Semantics is reducible to Tarskian Semantics. More precisely, the following result holds:
order formula in Negation Normal Form over the signature of M and with free variables in Dom(X ). Then M j=X f if and only if, for all s 2 X , M j=s f according to the usual rules of Tarski’s semantics. In particular, if f is a sentence, f is true in M according to
Does this result imply that Team Semantics is an unnecessarily complicated, but fundamentally 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 semantics. 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 j=X =(~x;~y) if any two s; s0 2 X which agree on ~x also agree on ~y; TS-inc: M j=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 j=X ~xj~y if the tuples ~x and ~y have the same length and, furthermore, no possible value of ~x in X is also a possible value for ~y in X ; TS-ind: M j=X ~x?~y if for any s; s0 2 X there exists some s00 2 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
(nonconditional) Independence Logic5 respectively, and they are formalisms deserving of
investigation in their own right. Here we mention briefly that every sentence of
functional dependence, exclusion, or independence logic is equivalent to some sentence of
existential second order logic S11, and that conversely every S11 sentence is equivalent to
some sentence of any of these logics [
Team Semantics allows also to extend First Order Logic in new ways via extra
connectives, such as the contradictory negation (such that M j=X f if and only if
M 6j=X f – note, this is not equivalent to the usual “dual negation”) or various types of
generalized quantifier [
4Or, more in general, terms; but for simplicity we will only consider dependence atoms applied to variables.
5There are also conditional independence atoms ~x?~z~y, which state that the possible values of ~x and ~y in X
are informationally independent for any fixed value of~z; but as pointed out in [
6Or, to be more precise, every S11-definable property of the relations corresponding to teams.
As briefly shown above, Team Semantics is a natural generalization of Tarskian Semantics which is of significant theoretical interest, as it makes it possible to extend First Order 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 semantics 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 [
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 j=X f t y iff M j=X f or M j=X y which would instead assert that, knowing that the true state is in X , the agent can conclude that f is true or that y is true. In other words, the difference between f _ y and f t y is the same as that between K(f _ y) (“the agent knows that f or y is true”) and K(f ) _ K(y) (“the agent knows that f is true or the agent knows that y 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 = f(x : 0; y : 0); (x : 0; y : 1)g) which do not satisfy x = y t x 6= y. By combining splitting and dependency atoms we can obtain interesting 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 j=X 9vf 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 f 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 f 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 j=X 8vf if this agent – after disregarding anything about the value of v – believes that f .
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
extended much further, and we refer to [
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 ` 62 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 Hlocated assignment over M with domain V is a function s : V [ f`g ! M [ H, where s(`) 2 H and s(v) 2 M for all v 2 V .
Definition 9 (Located Teams, Location Range). Let M be a first order model with domain 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 fs(`) : s 2 X g 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 j=X =(`;~x) iff, for any two s; s0 2 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 disjunction operator. As before, the interpretation is clear: M j=X f _ y if we can split the set of located observations X into two (possibly overlapping) subsets Y and Z that satisfy 7For 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.
X = y 0 0 s0, s1 the conditions described by f and y 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. However, the fact that each assignment has a location permits us to think about how this location 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 obvious 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 f ; y over the signature of M and with free variables in Dom(X ), TS- un: M j=X f un y if and only if there exist two H-located teams Y; Z X such that Y (`) = Z(`) = X (`), Y [ Z = X , M j=Y f and M j=Z y ;8 TS- lin: M j=X f lin y if and only if there exists a linear operator h : H ! R such that, for Y = fs 2 X : h(s(`)) 0g and Z = fs 2 X : h(s(`)) < 0g, it holds that M j=Y f and M j=Z y .
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:
8As an aside, it is not difficult to see that this is essentially a spatial version of the value-preserving
disjunctions of [
X =
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 2 X be a located assignment of X . Furthermore, let d 2 (0; ¥) be a positive real number, and let V Dom(X ) be a set of variables in the domain of X . Then the (V; d )-local restriction of X around s is the located team XjV;d ;s = fs0jV [s0(`) s(`)=`] : s0 2 X ; d(s0(`); s(`)) d g where, as usual, s0V is the restriction of s to the variables of V (as well as `); d(p; q) = j kp qk = php 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 XjV;d ;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 2 X . Furthermore, let d 2 (0; ¥) and let V Dom(X ). Then we say that s and s0 are (V; d )-locally similar in X , and we write s (X;V;d ) s0, if and only if there exist an orthogonal operator10 o : XjV;d ;s(`) ! XjV;d ;s0 (`) and a function h from XjV;d ;s onto XjV;d ;s0 such that h(s) = s0 and such that, for all s00 2 XjV;d ;s. 1. s00(v) = h(s00)(v) for all v 2 V (h preserves the values of the variables in V ); 2. o(s00(`)) = h(s00)(`) (h transforms the locations according to o).
for s (X;Var(~x);d ) s0, where Var(~x) = fv 2 Var : v occurs in ~xg. (X;~x;d ) s0 as a shorthand
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 d 2 (0; ¥):
10Very 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. X = TS-locdep: M j=X =(~x : d ;~y) if, for any two s; s0 2 X , if s (X;~x;d ) s0 then s(~y) = s0(~y).
According to the above definition, M j=X =(~x : d ;~y) if and only if any two local assignments whose d -neighbourhoods are the same (up to orthogonal transformations, e.g. rotations 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 d1 : : : dn, 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.
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 [
Another idea worth investigating would be the combination of such an approach with
weighted variants of Team Semantics such as the ones discussed in [