Dependence logic is an extension of first-order logic which adds to itdependence atoms, that is, expressions of the form\(\eqord(x_1 \ldots x_n, y)\) which assert that the value of \(y\) isfunctionally dependent on (in other words, determined by) the valuesof \(x_1 \ldots x_n\). These atoms permit the specification ofnon-linearly ordereddependency patterns between variables,much in the same sense of IF-Logicslashed quantifiers; but,differently from IF-logic, dependence logic separates quantificationfrom the specification of such dependence/independence conditions.

The principal semantics of dependence logic, calledteamsemantics, generalizes Tarski’s semantics by lettingexpressions be satisfied or not satisfied with respect tosets of variable assignments rather than with respect tosingle assignments. This semantics pre-dates the development ofdependence logic proper, and it was originally developed by WilfridHodges in the context of IF-logic (Hodges 1997). There also exists agame-theoretic semantics for dependence logic, based on games ofimperfect information and roughly analogous to the game-theoreticsemantics for independence-friendly logic (Väänänen2007a).Sensu stricto, the term “dependencelogic” refers exclusively to the language obtained by adding theabove-mentioned functional dependence atoms to the language offirst-order logic; but the term is also used, in a more general sense,to refer to the area of research that studies the properties of logicsobtained by adding variousnotions of dependence andindependence to first order logic, such asindependencelogic (Grädel & Väänänen 2013),intuitionistic dependence logic (Yang 2013) orinclusionlogic (Galliani 2012, Galliani & Hella 2013), or even thoseof logics extendingother logical frameworks through similaratoms, as in the case ofmodal dependence logic(Väänänen 2008).

In this article, the term “dependence logic” will be usedto refer to dependence logic proper, and the term “logics ofdependence and independence” will instead be used to refer toits variants and generalizations.

• 1. Dependency patterns in first order logic and its extensions
• 2. Team semantics
  • 2.1 Game-theoretic semantics
• 3. Properties
  • 3.1 Expressivity
  • 3.2 Hierarchies in dependence logic
  • 3.3 Negation in dependence logic
  • 3.4 Truth, validity and proof systems in dependence logic
• 4. Variants of dependence logic
  • 4.1 Independence Logic
  • 4.2 Inclusion logic
  • 4.3 Team Logic
  • 4.4 Intuitionistic Dependence Logic
  • 4.5 Generalized Dependencies and Connectives in Team Semantics
  • 4.6 Propositional Dependence Logic
  • 4.7 Modal Dependence Logic
  • 4.8 Linear Temporal Logic with Team Semantics
  • 4.9 Quantitative Variants of Team Semantics and Dependence Logic
• 5. Applications of dependence logic
  • 5.1 Dependence logic and database theory
  • 5.2 Dependence logic and belief representation
  • 5.3 Dependence logic and Arrow’s theorem
  • 5.4 Quantum team logic and Bell’s inequalities
  • 5.5 Team Semantics and Counterfactual Reasoning
• Bibliography
• Academic Tools
• Other Internet Resources
• Related Entries

1. Dependency patterns in first order logic and its extensions

One feature of first order logic which accounts for much of itsexpressivity and applicability is the fact that it allows quantifiersto benested, and, hence, it permits the specification ofdependency patterns between quantified variables. Consider,for example, the (hopefully false) statement that “every boyloves some girl that loves some other boy”. It can bestraightforwardly translated into first order logic as

whose truth condition, according to Tarski’s usual semantics, isprecisely what one would expect: the above expression is true if andonly if for every boy \(b\) it is possible to find a girl \(g\) and aboy \(b'\) such that \(b\) loves \(g\) and \(g\) loves \(b'\) and\(b\) and \(b'\) are not the same. The identity of the girl \(g\) mayof course depend on the identity of the first boy \(b\)—afterall, for this expression to be true we do not require that all boysare in love with all girls—and, furthermore, the identity of thesecond boy \(b'\) may depend onboth the identity of thefirst boy \(b\) (since \(b'\) must be different from \(b\)) and fromthe identity of the girl \(g\) that \(b\) loves. So thedependencypattern between our quantified variables is as follows: \(y\)depends on \(x\), while \(z\) depends on both \(x\) and \(y\). From asyntactic perspective, this is reflected by the fact that \(\existsy\) is in thescope of \(\forall x\) while \(\exists z\) isin the scope of both \(\forall x\) and \(\exists y\).

Differences in the dependency patterns between operators can be usedto formalize important distinctions, such as for example the onebetween the continuity of a function \(f\)

and its uniform continuity

or, in intensional extensions of first order logic, to express thedifference betweenDe Dicto andDe Re readings(e.g., “It is possible for every person to be crazy” maybe understood either as stating that it for every person \(p\), it ispossible for \(p\) to be crazy, \(\forall x (\person (x) \rightarrow\Diamond \crazy (x))\), or as stating that it is possible thateveryone is crazy together, \(\Diamond \forall x (\person (x)\rightarrow \crazy (x))\)).

Dependency patterns between quantified variables in first order logicare necessarilytransitive, as it is made evident by theirconnections with the scopes of the corresponding sub-expressions: if\(\exists y\) is in the scope of \(\forall x\) and \(\exists z\) is inthe scope of \(\exists y\) then necessarily \(\exists z\) will be inthe scope of (and, therefore, dependent from) \(\forall x\).Furthermore, the set of all quantifiers in whose scope some subformula\(\alpha\) lies is linearly ordered: if \(\alpha\) is in the scope of\(Q_1 x_1\) and \(Q_2 x_2\), then either \(Q_1 x_1\) is in the scopeof \(Q_2 x_2\) or vice versa.

This limits the expressive possibilities of first order logic. Forexample, let us suppose that we wish to amend our previous assertionabout boys and girls as follows: every boy loves some girl that lovessome other boy, and this second boy can be chosen independently on thefirst one. What this means, intuitively speaking, is simple enough:for every boy \(b\) we can find a girl \(g\) such that \(b\) loves\(g\), and for every such girl we can find a boy \(b'\) such that\(g\) loves \(b'\) and \(b \not = b'\), and furthermore we can findthe identity of the second boy \(b'\) without knowing that of \(b\),on the basis of the identity of the girl \(g\) alone. This can stillbe the true in some scenarios, such as for example if two boys \(b_1\)and \(b_2\) love respectively two girls \(g_1\) and \(g_2\), whohowever love only \(b_2\) and \(b_1\) respectively. However, it iseasily seen that it is not equivalent to our previous statement: forexample, if our universe consists (as in (b) above) of two boys \(b\)and \(b'\) and a girl \(g\), and \(b\) and \(b'\) both love \(g\) wholoves both of them, then our previous assertion is true but thecurrent one is false.

Two scenarios in which (\(\ref{eq:boygirl1}\)) is true. In (a), \(z\)can be chosen independently from \(x\); in (b), it cannot.

However, it is not clear how to formalize this condition in firstorder logic. In essence, we would need to modify(\(\ref{eq:boygirl1}\)) so that \(z\) is not in the scope of \(x\),and hence it does not depend on it; however, we would still want \(z\)to depend on \(y\) and \(y\) on \(x\). As just discussed, however,such a dependency pattern is not realizable in first-order logic. Wecan sidestep the issue by resorting to higher-order quantification:indeed, one can see that the expression

captures our intended interpretation, but only at the cost of explicitexistential quantification over functions.

A possible alternative would be to expand the syntax of first orderlogic in order to lift the restrictions about dependency patternsbetween quantified variables. This is the route taken bybranchingquantifier logic (Henkin 1961), in which the truth conditions of(\(\ref{boygirl2}\)) correspond to those of

and toindependence-friendly logic, in which(\(\ref{boygirl2}\)) is equivalent to

We will not give here a detailed explanation of the semantics of thesetwo formalisms; suffice to say, in (\(\ref{boygirl3}\)) the value of\(w\) does not depend on the values of \(x\) and \(y\) (although itmay depend on the value of \(z\)), as they belong to different“rows” of the complex quantifier\(\left(\begin{smallmatrix} \forall x &\exists y\\ \forall z&\exists w \end{smallmatrix}\right)\), while in(\(\ref{boygirl4}\)) the value of \(z\) does not depend on the valueof \(x\), because this dependency is explicitly “slashedaway” by the quantifier (\(\exists z / x\)).

One feature common to branching quantifier logic and independencefriendly logic, as we can see, is that they do not separate thequantification of variables from the specification of non-standardpatterns of dependence: as in the case of first order logic, whether aquantified variable \(v_1\) will or will not depend on some otherquantified variable \(v_2\) will be determined by the respectiveposition and form of their quantifiers.

Dependence logic takes a different approach to the problem ofextending first order logic in order to represent(\(\ref{boygirl2}\)). Compared to (\(\ref{eq:boygirl1}\)), the onlynovel condition is the one that states that the value of \(z\) isdetermined by (that is, functionally dependent on) the valueof \(y\); and this corresponds to a new atomic condition \(\eqord(y,z)\), called adependence atom, whose intended meaning isthat (the value of) \(z\) is a function of the value of \(y\).Differently from the cases of branching quantifier logic orindependence-friendly logic, this is a condition over the values that\(y\) and \(z\) can take, not a condition over the behaviour of thequantifier \(\exists z\): indeed, there is in general no reason torequire that \(z\) is a quantified variable at all—it might wellbe a free variable instead, or some complex term involving multiplevariables.

In dependence logic, (\(\ref{boygirl2}\)) can be formalized as

The truth conditions of (\(\ref{boygirl2}\)), (\(\ref{boygirl3}\)),(\(\ref{boygirl4}\)) and (\(\ref{boygirl5}\)) are precisely the same:any model that satisfies one of these expressions (in the respectivelanguages) satisfies all four. More in general, as we will see, theexpressive powers of existential second-order logic,independence-friendly logic and dependence logicwith respect todefinability of classes of models are precisely the same. Thisis, however, not the case for formulas with free variables; andfurthermore, these logics can be extended and modified along markedlydifferent lines.

2. Team semantics

Team semantics, first developed by Wilfrid Hodges in the context ofindependence friendly logic (Hodges 1997), is a generalization ofTarski’s semantics for first order logic to the case of multipleassignments of elements to variables. Sets of such assignments, calledteams for historical reasons, constitute the fundamentalsemantic notion of team semantics, and formulas are satisfied or notsatisfied with respect to them rather than with respect to singleassignments. The connection between team semantics and Tarskisemantics is shown by the following result, which holds in dependencelogic as well as in all its first order variants:

More in general, teams can be understood asbelief sets,representing the set of all states of the world (=assignments) thatsome agent believes possible. Then a team \(X\) will satisfy someformula \(\phi\) if and only if \(\phi\) holds when \(X\) is the setof all possible states; and in this case, we will write \(X \models\phi\) (or \(M, X \models \phi\) if the choice of the model \(M\) isnot clear). In this section, we will examine the rules of teamsemantics and their interpretation in terms of this principle; then,in the next section, we will discuss how it also arises from theimperfect-informationgame-theoretic semantics for dependencelogic.

The condition for the new dependence atoms \(\eqord(x_1 \ldots x_n,y)\), which correspond to the statement that the value of \(y\) is afunction of the values of \(x_1 \ldots x_n\), is easilyunderstood:

For example, suppose that \(X\) is a set of assignments over the threevariables \(x_1\), \(x_2\) and \(y\), where \(x_1\) represents thenationality of a candidate to a position, \(x_2\) represents theirscore (according to a suitable evaluation method) and \(y\) representswhether they were accepted or rejected. Then the atom \(\eqord(x_2,y)\) corresponds to the statement that the offer is determined by thescore alone: if two candidates have the same score they will receiveexactly the same offer, regardless of any other factor. A special caseof dependence atom is given by theconstancy atoms\(\eqord(y)\), which—as per the above semantics—aresatisfied by a team if and only if all of its assignments agree overthe value of \(y\).

Under the same interpretation, the rules for first-order literals andconjunctions (for simplicity, we will assume that our expressions arein negation normal form; and, as is customary, we will assume that thenegations of dependence atoms are never satisfied) are easy toderive:

It is worth pointing out that, as we can already see by these rules,thelaw of the excluded middle does not hold in dependencelogic (just as it does not hold in independence friendly logic): forexample, if a team \(X\) contains both assignments \(s\) with \(s(x) =s(y)\) and assignments \(s'\) with \(s'(x) \not = s'(y)\) then \(X\not \models x=y\) and \(X \not \models x\not = y\). In this section,in any case, we will present the language of dependence logic withoutan explicit negation operator; then, later, we will discuss theconsequences of adding it to its language.

What about universal quantification? In which circumstances should auniversally quantified expression \(\forall v \psi\) hold in a team?Again, we must recall the intuition according to which a teamrepresents a set of possible states of things. If we wish to evaluate\(\forall v \psi\), with respect to which possible states of thingsshould we evaluate \(\psi\)? The natural answer is that we shouldconsider all states of things that differ from ones in \(X\) only withrespect to the value of \(v\). This justifies the following rule:

where \(s' \sim_v s\) means that the two assignments \(s\) and \(s'\)differ from each other at most with respect to the value of thevariable \(v\).

Let us now consider disjunction. When should \(\phi \lor \psi\) hold?To answer this, let us recall—once again—that teams can beunderstood as sets of possible states of things, and that thereforethe union of two teams \(Y\) and \(Z\) represents all states of thingswhich may occur if \(Y\) or \(Z\) is the case. Therefore, if the twoformulas \(\phi\) and \(\psi\) are satisfied by the set of teams\(\{Y_1 \ldots Y_n, \ldots\}\) and \(\{Z_1 \ldots Z_n, \ldots\}\)respectively, their disjunction \(\phi \lor \psi\) should be satisfiedby the set of teams \(\{Y_i \cup Z_j : i,j \in 1, \ldots\}\), or,equivalently,

It is worth pointing out here that we donot require, ingeneral, that \(Y\) and \(Z\) are disjoint. Because of thedownwards closure property, which we will discuss soon, thisadditional condition would make no difference for the semantics ofdependence logic proper; but in the case of certain extensions andvariants of dependence logic, that additional requirement wouldconflict with the principle oflocality according to whichthe satisfaction conditions of an expression depend only on the valuesof the variables which occur free in it (Galliani 2012).

It is also important to note that, in dependence logic, disjunction isnot idempotent: for example, \(\eqord(x,y) \lor \eqord(x,y)\)is not equivalent to \(\eqord(x,y)\), and it is satisfied by a team\(X\) if and only if for everythree assignments in \(X\)which agree on \(x\) at leasttwo agree on \(y\). This mayappear somewhat counter-intuitive; but it is a straightforwardconsequence of the fact that, under our interpretation, \(\eqord(x,y)\lor \eqord(x,y)\) is to be read as “every possible state ofthings comes from one of two sets of states of things, and in both ofthem \(y\) is a function of \(x\)”. Since the union of functionsis not in general a function, it comes to little surprise thatdisjunction in dependence logic is not idempotent.

Finally, we consider the case of existential quantification. When isthe expression \(\exists v \psi\) satisfied by a team? In order toanswer this, we may begin by considering the interpretation of therestriction operator which, given any team \(X\), results inthe team \(X_{\backslash v}\) obtained by removing the variable \(v\)(if present) from all assignments \(s \in X\) (and then, since \(X\)is a set, by collapsing identical assignments). This could beunderstood as aforgetting operation, through which we deleteall information about the value of \(v\)—for example, becausewhat we believed about this value was unreliable, or because thisvalue has been altered. Now suppose that \(X_{\backslash v} =Y_{\backslash v}\): then, in our interpretation, this means that thesets of possible states of things represented by \(X\) and \(Y\)disagree at most with respect to the value of \(v\). Thus, if \(Y\)satisfies the condition \(\phi\), we may say that \(X\) would satisfy\(\phi\)if not for the value of \(y\), or, equivalently,that \(X\) satisfies \(\exists v \psi\). This justifies the followingrule:

It is straightforward to verify that this is the case if and only if\(Y\) is of the form \(X[F/y] = \{s[a/y] : s \in X, a \in F(s)\}\) forsome function \(F\) from assignments in \(X\) to nonempty sets ofelements of our model.

It is worth pointing out here that it is not in general required bythe above definition that \(X\) and \(Y\) contain the same number ofassignments: a single assignment in \(X\) may well correspond tomultiple assignments in \(Y\), and—if \(v\) is already avariable occurring in the assignments of \(X\)—a singleassignment in \(Y\) may also correspond to multiple assignments in\(X\).

We will postpone an in-depth discussion of the properties ofdependence logic to after the specification of its game-theoreticsemantics. However, we conclude this section with the following threeimportant consequences of the above-given rules:

The locality principle, together with the conservativity principlementioned at the beginning of this section, constitutes an important“sanity condition” that any variant and extension ofdependence logic should satisfy. The same cannot be said aboutdownwards closure and the empty set property, which—as we willsee—are violated by variants of dependence logic.

Finally, we need to define thetruth of a dependence logicsentence with respect to a model. Since a sentence has no freevariables, by the locality principle we have at once that either allnonempty teams satisfy it or no nonempty team satisfies it. This isanalogous to the case of Tarski’s semantics, in which a sentenceis either satisfied by all variable assignments or by none of them.Thus, we can define truth in the usual way:

2.1 Game-theoretic semantics

As mentioned, the game-theoretic semantics for dependence logic is avariant of the imperfect-information semantics forindependence-friendly logic, which is itself an adaptation of thegame-theoretic semantics of first-order logic. We refer the reader to(Väänänen 2007a) for a formal, detailed definition ofthis semantics.

In game-theoretic semantics, a sentence \(\phi\) and a model \(M\) aremade to correspond to a (usually two-player) game \(G_M(\phi)\). Thentruth is defined in terms of the existence ofwinningstrategies for one of the players (who, in this work, will becalled simply “Player \(0\)”): in other words, if\(\sigma_0\) is a (possibly non-deterministic) strategy for Player\(0\) and \(\Pi(G_M(\phi), \sigma_0)\) is the set of all plays whichare compatible with \(\sigma_0\) then \(\phi\) is true if and only ifevery play in \(\Pi(G_M(\phi), \sigma_0)\) is winning for Player\(0\). It is possible to think of the game \(G_M(\phi)\) as a debatebetween two players, one of whom (Player \(0\)) wishes to demonstratethat it is the case that \(\phi\) while the other (Player \(1\))wishes to demonstrate that it is not the case that \(\phi\).

As in the case of first-order logic and independence-friendly logic,in the imperfect-information game for dependence logic the positionsof the game are pairs \((\theta, s)\), where \(\theta\) is an instanceof a subformula of \(\phi\) (that is, multiple occurrences of the sameexpression as a subformula of \(\phi\) are to be consideredseparately) and \(s\) is a variable assignment over the model \(M\).^[1] The initial position is \((\phi, \emptyset)\), where \(\emptyset\) isthe empty assignment; and a non-deterministic strategy \(\sigma_0\)for Player \(0\) selects, for every disjunction and existentialquantification, one or moresuccessors of the currentposition according to the following rules:

• If the current position is of the form \((\psi \lor \theta, s)\) thenits successors are \((\psi, s)\) and \((\theta, s)\);

• If the current position is of the form \((\exists v \psi, s)\) thenits successors are all positions \((\psi, s')\) with \(s' \sim_vs\).

Similarly, the successors of \((\psi \land \theta, s)\) are \((\psi,s)\) and \((\theta, s)\), and the successors of \((\forall v \psi,s)\) are all positions of the form \((\psi, s')\) for \(s' \sim_v s\);but a strategy for Player \(0\) cannot specify a successor for thesepositions, as it is assumed that Player \(1\) chooses which positionfollows them.

A sequence of positions \(\overline \rho = \rho_0 \rho_1 \ldots\rho_n\) is aplay of \(G_M(\phi)\) if and only if

1. \(\rho_0 = (\phi, \emptyset)\);

2. For all \(i = 1 \ldots n\), \(\rho_{i}\) is a successor of\(\rho_{i-1}\).

If furthermore \(\rho_{i+1} \in \sigma_0(\rho_i)\) whenever \(\rho_i\)corresponds to a disjunction or an existential quantifier, we say that\(\overline \rho\)respects the strategy \(\sigma_0\); and asmentioned, we write \(\Pi(G_M(\phi), \sigma_0)\) for the set of allplays over \(G_M(\phi)\) which respect \(\sigma_0\).

We say that a strategy \(\sigma_0\) iswinning if every play\(\overline \rho\) which ends in a position \((\alpha, s)\) where\(\alpha\) is a first-order literal is such that the assignment \(s\)satisfies \(\alpha\) in the usual sense of Tarski’s semantics.Dependence atoms—and the plays which ends in dependenceatoms—are of no relevance for deciding whether a given strategyis winning. However, they are used to specify whether a given strategyisuniform:

Then we can define truth in game-theoretic semantics as follows:

It can be shown that this notion is equivalent to the notion of truthin team semantics. In fact, we can show more than this. If, for anyteam \(X\) and formula \(\phi\), the game \(G_{M,X}(\phi)\) is playedas \(G_M(\phi)\) but with the initial position chosen randomly forevery play from \(\{(\phi, s) : s \in X\}\), then the followingholds:

This result, as an aside, makes it clear why the team semantics ofdependence logic satisfies the empty set property and the downwardsclosure property. Indeed, if \(X = \emptyset\) then every strategy forPlayer \(0\) in \(G_{M, X}(\phi)\) is trivially winning and uniform;and if \(X \subseteq Y\) then any uniform winning strategy for Player\(0\) in \(G_{M, X}(\phi)\) is also a uniform winning strategy forPlayer \(0\) in \(G_{M, Y}(\phi)\).

3. Properties

3.1 Expressivity

Sentence-wise, dependence logic is equivalent to the existentialfragment \(\Sigma_1^1\) of second-order logic. More precisely, it canbe proved (Väänänen 2007a) that

Since Fagin’s Theorem (Fagin 1974) shows that a property offinite models is definable in \(\Sigma_1^1\) if and only if it isrecognizable in polynomial time by a nondeterministic Turing machine(that is, if and only if it is in NPTIME), it follows at once that

Another direct consequence of the equivalence between dependence logicand \(\Sigma_1^1\) on the level of sentences is that the compactnesstheorem and the Löwenheim-Skolem theorem both hold for dependencelogic too (Väänänen 2007a):

However, matters are more delicate when it comes to formulas with freevariables. Then it is possible to show (Kontinen &Väänänen 2009) that dependence logic corresponds to thedownwards-closed fragment of existential second orderlogic:

3.2 Hierarchies in dependence logic

In (Durand & Kontinen 2012), the effect of restricting the numberof dependent variables of dependence atoms or the number of universalquantifiers was examined. It was shown that both of these ways ofdefining fragments of dependence logic give rise of hierarchies:

• For all \(k\), let \(\mathcal D(k-\forall)\) be dependence logicrestricted to at most \(k\) universal quantifiers and let \(\mathcalD(k-dep)\) be dependence logic restricted to dependency atoms of theform \(\eqord(\vec x, y)\) for \(|\vec x| \leq k\). Then

  \[ \begin{align*}\mathcal D(k-\forall) &< \mathcal D(k+1-dep),\\ \mathcal D(k-\forall) &\leq \mathcal D(k-dep) \leq \mathcal D(k+1 - dep) \end{align*} \]

  and

  \[ \mathcal D(k-\forall) < \mathcal D(2k + 2 - \forall) \]

  with respect to the expressive power of sentences.

3.3 Negation in dependence logic

So far, we assumed that all dependence logic expressions are innegation normal form, and that dependence atoms are never negated.Adding an explicit negation operator to the language of dependencelogic, on the other hand, is somewhat problematic, owing to the factthat existential second order logic is not closed under negation.Indeed, the “obvious” negation rule

greatly increases the expressive power of dependence logic, extendingit toteam logic (Väänänen 2007a,b), which is,in a very strong sense, equivalent to full second order logic(Kontinen & Nurmi 2009).

A less strong, “dual” negation \(\lnot\) can be defined interms of de Morgan’s rules, \(\lnot(\phi \lor [\land] \psi)\equiv (\lnot \phi) \land [\lor] (\lnot \psi)\) and \(\lnot (\exists v[\forall v] \phi) \equiv \forall v [\exists v] (\lnot \phi)\), plusthe law of double negation \(\lnot \lnot \phi \equiv \psi\) and therule

for negations of dependence atoms (Väänänen 2007a,b).The resulting language is expressively equivalent to negation-freedependence logic, and, in fact, the description of dependence logic of(Väänänen 2007a) considers this negation as part of itslanguage; however, as shown in (Kontinen & Väänänen2011), the satisfaction conditions of a dependence logic formula andthose of its negation have little connection to one another. Moreprecisely:

Thus, nothing in general can be said about the dual negation of\(\phi\) except that it is equivalent to some dependence logicexpression which is not satisfied by any team which satisfies\(\phi\). Since, as already mentioned, the law of the excluded middlefails in dependence logic, this is not a very informative property; inparticular, it is possible to find in dependence logic (with dualnegation) equivalent expressions with non-equivalent negations, likefor example \(x \not = x \land y \not = y\) and\(\lnot\eqord(x,y)\).

3.4 Truth, validity and proof systems in dependence logic

Like independence friendly logic, dependence logic can define its owntruth operator (Väänänen 2007a), that is, if for allformulas \(\phi\) we have that \(\lceil \phi\rceil\) is the Gödelnumber of \(\phi\) then we can find a formula \(\tau(x)\), with \(x\)as its only free variable, such that

for all models \(M\) which satisfy Peano’s axioms for naturalnumbers. This is not in contradiction with Tarski’sundefinability theorem, because dependence logic is not closed undercontradictory negation.

The problem of deciding whether a dependence logic sentence is valid(that is, true in all models) is non-arithmetical, and in factcomplete with respect to the \(\Pi_2\) class of the Levy hierarchy.Nonetheless, the proof theory of dependence logic has been studied. Inparticular, in (Kontinen & Väänänen 2013), a soundand complete proof system has been developed for the problem offinding thefirst order consequences of a dependence logictheory.

4. Variants of dependence logic

In this section, we will briefly summarize the properties of the moststudied variants of dependence logic. Many such variants exist, andmuch work has been done on their classification and comparison. Inthis work, we will only mention those variants which are of specialsignificance because of their relationship with dependence logicproper.

4.1 Independence Logic

Rather than extending first order logic with dependence atoms\(\eqord(\vec x, y)\), independence logic (Grädel &Väänänen 2013) extends it withindependenceatoms \(\vec x \mathop{\bot_{\vec z}} \vec y\), whose intendedinterpretation is “for any possible choice of \(\vec z\), thepossible values of \(\vec x\) and \(\vec y\) areindependent”—in other words, given any fixed choice of\(\vec z\), knowing the value taken by \(\vec x\) would not convey anyinformation about the value taken by \(\vec y\). This is a notion ofsignificant conceptual importance: for example, one may want toexpress that—if one does not know the encryptionkey—seeing the encrypted version of a message carries noinformation about the corresponding clear-text version. If \(x\)represents the encrypted message and \(y\) represents the plain-textone, then this corresponds to the condition \(x \mathop{\bot} y\),where \(\vec z\) in this case is empty. Similarly, if \(k\) representsthe key then \(x \mathop{\bot} k\) represents the claim that the keycannot be inferred from the encrypted message; and the conjunctiondependence atom \(\eqord(k, x, y)\) (which, as we will soon see, canbe represented in independence logic) represents the claim that theplain-text message can be decoded given the encrypted message and thekey.

Formally, the satisfaction rule for independence atoms can be given asfollows:

Independence logic is strictly more expressive than dependence logic:indeed, it lacks the downwards closure property, and the dependenceatom \(\eqord(\vec x, y)\) is equivalent to the independence atom \(y\mathop{\bot_{\vec x}} y\). Furthermore, it can also be shown(Galliani & Väänänen 2014) that conditionedindependence atoms \(\vec x \mathop{\bot_{\vec y}} \vec z\) can bedefined in terms ofunconditional independence atoms \(\vec x\mathop{\bot} \vec y\).

Sentence-wise, independence logic is also equivalent to existentialsecond order logic \(\Sigma_1^1\); but formula-wise, it is moreexpressive, and it was shown in Galliani 2012 that it can capture allnonempty \(\Sigma_1^1\)-definable team properties.

4.2 Inclusion logic

Inclusion logic (Galliani 2012, Galliani & Hella 2013) extendsfirst-order logic withinclusion atoms \(\vec x \subseteq\vec y\), reminiscent of the inclusion dependencies of databasetheory. Its semantics is:

Differently from dependence and independence logic, inclusion logic is(sentence-wise) strictly weaker than existential second order logic.In fact, it can be shown (Galliani & Hella 2013) to be equivalentto the positive fragment ofgreatest fixed point logic, and,therefore, to capture PTIME properties of models over finite orderedmodels. Formula-wise, inclusion logic is strictly weaker thanindependence logic but incomparable with dependence logic: indeed, thesatisfiability conditions of its formulas are not downwards closed,but they areclosed by unions in the sense that

4.3 Team Logic

Team logic (Väänänen 2007a,b; Kontinen & Nurmi2009) extends dependence logic by adding to it acontradictorynegation \(\lnot\). It is equi-expressive with full second orderlogic, both in terms of definability of classes of models(Väänänen 2007b) and with respect to the classes ofteams that team logic expressions can define with respect to a givenmodel (Kontinen & Nurmi 2009). In (Lück 2019), aHilbert-style axiomatization for Team Logic (and for its modal andpropositional equivalents) was found that is complete for itsdependence-free fragment (that is, for the fragment in whichdependence atoms do not appear).

4.4 Intuitionistic Dependence Logic

Intuitionistic dependence logic (Abramsky &Väänänen 2009; Yang 2013) extends dependence logic byadding an implication connective \(\phi \rightarrow \psi\), whosesatisfaction rules are given in team semantics by

This operator is called the “intuitionistic implication”,because of the similarity between its semantics and the one of theimplication operator in Kripke’s semantics for intuitionisticlogic (Kripke 1965). Its interpretation in terms of belief is quitestraightforward: if the assignments in \(X\) represent thestatesof thing that some agent believes possible, then a subset \(Y\)of \(X\) may represent the result of abelief update in whichthe agent rejects some previously believed possible states of thing,and \(\phi \rightarrow \psi\) states than any such update that wouldcause \(\phi\) to hold would also cause \(\psi\) to hold. From thisstandpoint, this is a very natural concept which permits us todescribe predictions about how such an agent’s overall beliefstate would react to belief updates.

However, because of the second order universal quantification implicitin its semantics, this connective suffices to greatly increase theexpressive complexity of the logic: in particular, as shown in (Yang2013), any sentence of second order logic is equivalent to somesentence of intuitionistic dependence logic. Intuitionistic dependencelogic retains the downwards closure property: if a team satisfies anintuitionistic dependence logic formula then so do all of itssubsets.

The connections between (extensions of) Intuitionistic DependenceLogic and formal inquisitive semantics has been analyzed in (Ciardelliet al. 2020).

4.5 Generalized Dependencies and Connectives in Team Semantics

The variants and extensions of Dependence Logic seen above are allgenerated from First Order Logic (with Team Semantics) by introducingnew atoms or connectives. It is possible to considergeneralizeddependence atoms (Kuusisto 2015), much in the same way in whichgeneralized quantifiers are introduced in classical First Order Logic,and ask questions like:

• For which collections \(\mathcal D\) of atoms or connectives is itthe case that \(\mathbf{FO}(\mathcal D)\) (i.e., First Order Logicaugmented by the atoms and connectives in \(\mathcal D\)) isexpressively equivalent to First Order Logic? Such collections\(\mathcal D\) are said to bestrongly first order.
• Given a collection \(\mathcal D\) of atoms and connectives, forwhich other collections \(\mathcal E\) of atoms and connectives is itthe case that \(\mathbf{FO}(\mathcal D, \mathcal E)\) is expressivelyequivalent to \(\mathbf{FO}(\mathcal D)\)? Such \(\mathcal E\) aresaid to besafe for \(\mathcal D\).

No complete answer to these questions is known at the moment. Somepartial results, however, are known:

1. If \(\mathcal D\) is a collection of upwards closed dependencies(that is to say, dependencies that, if true of some team \(X\) in somemodel \(M\), are also true of any superteam \(Y \supseteq X\) in thesame model), plus possibly the constancy atom (that is, thealready-mentioned special case of the dependence atom that states thatsome variable is constant over a team), then \(\mathcal D\) isstrongly first order (Galliani 2015);
2. Not all strongly first order dependencies are safe for alldependencies: in particular, the constancy atom is not safe forunary inclusion dependencies \(x \subseteq y\), where \(x\)and \(y\) are single variables; the possibility operator \(\diamond\phi\), which is satisfied by a team \(X\) in a model \(M\) if andonly if there is a nonempty subset of X that satisfies \(\phi\) in\(M\), is instead safe for all collections of dependencies, as are thetotality atom (that states that some variable, or tuple of variables,takes all possible values) and the non-constancy atom (that statesthat some variable takes at least two different values in a team)(Galliani 2021);
3. If \(\mathcal D\) is a strongly first order collection ofdependencies and \(\mathcal E\) is a collection of downwards closeddependencies (that is, dependencies that whenever true of some teamthey are also true of every subteam), then \(\mathcal D\) is safe for\(\mathcal E\) (Galliani 2019);
4. If \(\mathcal D\) is a collection of dependencies that aredownwards closed andrelativizable (that is to say, addingrelativizations of dependencies in \(\mathcal D\) to unary predicates\(P\) to the language is no more expressive than adding thedependencies themselves), then \(\mathcal D\) is strongly first orderif and only if every dependence in it can be defined in terms ofconstancy atoms (Galliani 2019).
5. (Somewhat more involved) characterizations are available for thedependencies that are relativizable and safe to add to First OrderLogictogether with their contradictory negations (Galliani2024) as well as for the ones that are strongly first order, closed byunions, and domain independent (Galliani 2022).

These are all partial results, however, and the general theory ofdependencies and connectives in Team Semantics is still in itsinfancy.

A related topic is the study of extensions of Dependence Logic viageneralized quantifiers (Engström 2012). An interesting resultalong these lines consists in axiomatization for the extension ofDependence Logic via the quantifier \(Q\) “there existuncountably many…”, which is sound and complete for the\(\textbf{FO}(Q)\) consequences of a theory (Engström, Kontinen& Väänänen 2017).

Also worth pointing out in this context is the work of (Kontinen &Yang 2019), which found a logic based on Team Semantics (withdifferent choices of connectives than the “standard” onesof Dependence Logic) whose formulas capture precisely thefirst-order-definable properties of teams; and (Hella et al. 2024), inwhich definability hierarchies are found for generalizeddependencies.

4.6 Propositional Dependence Logic

The dependence and independence atoms considered so far expressrelationships between the possible values ofvariables in aset of assignments. However, the same notions of dependence andindependence can be equally naturally be applied to propositionthemselves, as it happens in natural language expression such as forinstance “Whether he will or will not pass the course dependsonly on the content of his final exam”.

Propositional Dependence Logic consider such atoms within the contextof propositional logic. Propositional dependence logic teams are setsofvaluations \(v\) from propositional atoms \(p_1 \ldotsp_n\) to \(\{T, F\}\). Its semantic rules – and theirjustifications – mirror very closely the ones of first orderteam semantics, and the rule for dependence atoms is

Many of the variants and generalizations of first order dependencelogic can be lowered to the propositional level without anydifficulty: thus, for example, it is possible to study the propertiesof propositional inclusion logic, propositional team logic,propositional intuitionistic dependence logic and so on.

Whereas (first order) dependence logic is strictly more expressivethan first order logic, propositional dependence logic is not moreexpressive than propositional logic, as it follows immediately fromthe fact that all propositional functions are expressible inpropositional logic. There exists, however, a close relation betweenthe teams of propositional dependence logic and theinformationstates ofinquisitive logic (Groenendijk 2009; Ciardelli& Roelofsen 2011), a semantic framework for the study of thenotion of meaning and information exchange: in particular, theimplication of inquisitive logic is exactly the same as the one ofpropositional intuitionistic dependence logic.

In (Mahmood and Meier 2020) the complexity of Propositional DependenceLogic and its variants was studied with respect to a number ofparametrizations (formula-size, formula-depth, treewidth, team-size,number of variables).

Axiomatizations for propositional dependence logic and many of itsextensions can be found in (Yang & Väänänen 2016);and the analysis of the computational complexity of this formalism(and of related propositional logics based on Team Semantics) can befound in (Virtema 2017; Hannula et al. 2018).

4.7 Modal Dependence Logic

Modal dependence logic (Väänänen 2008) and its variantsextend modal logic by adding to it the same dependence atoms\(\eqord(p_1 \ldots p_n, q)\) already considered in the case ofpropositional dependence logic.

Its satisfaction conditions can be defined through a variant of teamsemantics in which teams are replaced bysets of possibleworlds.

Much research has investigated the complexity-theoretic properties ofthis logic, of its fragments, and its extensions (Ebbing, Lohmann,& Yang 2011; Ebbing & Lohmann 2012; Lohmann & Vollmer2013).

Modal Independence Logic has also been investigated in (Kontinen etal, 2017); and a modal version of Inclusion Logic was axiomatized in(Anttila et al, 2025).

4.8 Linear Temporal Logic with Team Semantics

Linear Temporal Logic may also be given a “Team Semantics”of sorts, in which formulas are evaluated with respect to sets oftraces (that is to say, sets of sequences of states), representingpossible computations of a system. Such a logical framework can beused for the specification and verification ofhyperproperties (Krebs et al. 2017, Other Internet Resources;Lück 2020; Gutsfeld et al 2022), that is to say, properties like“The system terminates within a bounded amount of time”whose truth cannot be ascertained by checking every possible trace ofthe system on its own but only by looking at the set of all possibletraces as a whole.

4.9 Quantitative Variants of Team Semantics and Dependence Logic

As teams correspond to sets of assignments, it is natural to considerthe possibility of extensions of team semantics in which satisfactionis defined instead with respect tomultiteams (i.e.,multisets of assignments) orprobability distributions overassignments.

The first possibility has been studied in (Durand et al. 2018a), whilethe second has been studied in (Durand et al. 2018b). The second work,in particular, has led to interesting connections to problems ofdescriptive complexity over the reals and metafinite model theory(Hannula et al. 2019, Hannula et al. 2020, Hannula and Virtema2022).

A related approach is that of (Grädel and Wilke 2022), in which avariant of Team Semantics over multisets of assignments is studied.

5. Applications of dependence logic

5.1 Dependence logic and database theory

There is a straightforward connection between the teams of teamsemantics and the relations studied in relational database theory:given a team \(X\) and a tuple of variables \(\vec v = v_1 \ldotsv_k\) occurring in its assignments, it is possible to define therelation \(X(\vec v) = \{\langle s(v_1), \ldots, s(v_n)\rangle : s \inX\}\). Furthermore, the dependency atoms studied in dependence logicand its variants are analogous to – and in many cases, derivedfrom – dependencies considered in database theory such asfunctional dependencies (Väänänen 2007a),multivalued dependencies (Engström 2012), andinclusion and exclusion dependencies (Galliani 2012). Therelationship between dependence logic and database theory contributednot only to the further development of dependence logic, but also tothat of database theory: for instance, in Hannula & Kontinen 2016a finite axiomatization of the unrestricted implication problem forinclusion, functional, and embedded multivalued database-theoreticdependencies was found through the study of a similar problem withinthe context of team semantics.

5.2 Dependence logic and belief representation

As discussed in (Yang 2014) and (Yang & Väänänen2016), there exists a close connection between (propositional)intuitionistic dependence logic andinquisitive logic(Ciardelli & Roelofsen, 2011), a framework for the study ofmeaning and information exchange between agents. More in general, thedependency atoms and connectives of studied in team semantics admitnatural interpretations in terms ofbelief states andbelief updates, as discussed in (Galliani 2015). At thistime, the exact nature of the relationship between such logics anddynamic-epistemic logic and its variants (Van Ditmarsch, van Der Hoek,& Kooi 2007) is largely unexplored, but there is ample reason tosuspect further connections between these two areas of mathematicaland philosophical logic.

5.3 Dependence logic and Arrow’s theorem

Arrow’s theorem (Arrow 1950) is a profoundly influential resultof social choice theory that, in brief, shows that no voting system(that is, no system for converting rankings of individual preferencesbetween alternatives into a global, societal-level preference ranking)exists that can satisfy three reasonable-sounding conditions,namely

• If every voter prefers \(A\) to \(B\), the group as a whole prefers\(A\) and \(B\);

• Whether the group as a whole prefers \(A\) to \(B\) or vice versadepends exclusively on every voter’s preferences concerning\(A\) and \(B\), andnot on their preferences concerningother possible alternatives;

• No single voter is adictator, that is, the group’spreferences are not determined by the preferences of any singlevoter.

As the wording itself suggests, the second and third conditions admita natural reading in terms of dependence and independence: in fact, asshown in Pacuit & Yang 2016, Arrow’s theorem can beformalized in independence logic and proved in a suitable naturaldeduction system.

5.4 Quantum team logic and Bell’s inequalities

In (Hyttinen, Paolini, & Väänänen 2015) a variantof propositional team logic, calledquantum team logic, isintroduced. In this formalism, teams are replaced byquantumteams, which differ from the ordinary teams of propositional teamlogic in that they allow for the values of certain variables to beindeterminate with respect to certain valuations and in thatthey allow for multiple instances of the same valuation (thus adding aquantitative aspect to team semantics). A semantics is then definedover quantum teams for a language that allows for the specification ofinequalities concerning the probabilities of events, and asound and complete proof system is developed for it; and finally, itis shown thatBell’s inequalities admit counterexamplesin this systems, as they do according to the predictions of quantummechanics and according to experimental evidence (Einstein, Podolsky,& Rosen 1935; Bell 1964; Aspect, Grangier, & Roger 1981),while they do not so in theclassical version of thisframework.

5.5 Team Semantics and Counterfactual Reasoning

Bibliography

• Abramsky, Samson and Jouko Väänänen, 2009,“From IF to BI: A Tale of Dependence and Separation”,Synthese, 167(2): 207–230.doi:10.1007/s11229-008-9415-6
• Anttila, Aleksi, Matilda Häggblom and Fan Yang, 2025,“Axiomatizing modal inclusion logic and its variants”,Arch. Math. Logic.https://doi.org/10.1007/s00153-024-00957-y
• Arrow, Kenneth J., 1950, “A Difficulty in the Concept ofSocial Welfare”,The Journal of Political Economy,pp.328–346. doi:10.1086/256963
• Aspect, Alain, Philippe Grangier and Gérard Roger, 1981,“Experimental Tests of Realistic Local Theories via Bell’sTheorem”,Physical Review Letters, 47(7):460–463. doi:10.1103/PhysRevLett.47.460
• Barbero, Fausto and Gabriel Sandu, 2021, “Team Semantics forInterventionist Counterfactuals: Observations vs.Interventions”,Journal of Philosophical Logic, 50:471–521. doi:10.1007/s10992-020-09573-6
• Barbero, Fausto and Jonni Virtema, 2023, “Strongly completeaxiomatization for a logic with probabilistic interventionistcounterfactuals”,Logics in Artificial Intelligence.JELIA 2023. doi:10.1007/978-3-031-43619-2_44
• –––, 2024, “Expressivity landscape forlogics with probabilistic interventionist counterfactuals”,32nd EACSL Annual Conference on Computer Science Logic, CSL2024, Vol. 288. doi:10.4230/LIPIcs.CSL.2024.15
• Bell, J.S., 1964, “On the Einstein-Podolsky-RosenParadox”,Physics, 1(3): 195–200.
• Ciardelli, Ivano and Floris Roelofsen, 2011, “InquisitiveLogic”,Journal of Philosophical Logic, 40(1):55–94. doi:10.1007/s10992-010-9142-6
• Ciardelli, Ivano, Iemhoff Rosalie, and Yang, Fan, 2020,“Questions and Dependency in Intuitionistic Logic”,Notre Dame Journal of Formal Logic, 61(1): 75– 115.doi:10.1215/00294527-2019-0033
• van Ditmarsch, Hans, Wiebe van der Hoek, and Barteld Kooi,2007,Dynamic Epistemic Logic, (Synthese Library 337),Dordrecht: Springer. doi:10.1007/978-1-4020-5839-4
• Durand, Arnaud and Juha Kontinen, 2012, “Hierarchies inDependence Logic”,ACM Transactions on Computational Logic(TOCL), 13(4): 1–21. doi:10.1145/2362355.2362359
• Durand, Arnaud, et al., 2018, “Approximation and dependencevia multiteam semantics”,Annals of Mathematics andArtificial Intelligence, 83(3): 297–320.
• Durand, Arnaud, et al., 2018, “Probabilistic teamsemantics”,International Symposium on Foundations ofInformation and Knowledge Systems, Cham: Springer.
• Ebbing, Johannes and Peter Lohmann, 2012, “Complexity ofModel Checking for Modal Dependence Logic”,SOFSEM 2012:International Conference on Current Trends in Theory and Practice ofComputer Science, (Lecture Notes in Computer Science, 7147),Berlin, Heidelberg: Springer, pp. 226–237.doi:10.1007/978-3-642-27660-6_19
• Ebbing, Johannes, Peter Lohmann, and Fan Yang, 2013, “ModelChecking for Modal Intuitionistic Dependence Logic”,International Tbilisi Symposium on Logic, Language, andComputation 2011, (Lecture Notes in Computer Science, 7758),Berlin, Heidelberg: Springer, pp. 231–256.doi:10.1007/978-3-642-36976-6_15
• Einstein, A., B. Podolsky and N. Rosen, 1935, “CanQuantum-Mechanical Description of Physical Reality be ConsideredComplete?”Physical Review, 47(10): 777–780.doi:10.1103/PhysRev.47.777
• Engström, Fredrik, 2012, “Generalized Quantifiers inDependence Logic”,Journal of Logic, Language andInformation, 21(3): 299–324.doi:10.1007/s10849-012-9162-4
• Engström, Fredrik, Juha Kontinen, and JoukoVäänänen, 2017, “Dependence logic withgeneralized quantifiers: Axiomatizations”,Journal ofComputer and System Sciences, 88: 90–102.
• Fagin, Ronald, 1974, “Generalized First-Order Spectra andPolynomial-Time Recognizable Sets”,Complexity ofComputation (SIAM-AMS Proceedings 7), Richard M. Karp (ed.),Providence, RI: American Mathematical Society, pp. 27–41.
• Galliani, Pietro, 2012, “Inclusion and ExclusionDependencies in Team Semantics—On Some Logics of ImperfectInformation”,Annals of Pure and Applied Logic, 163(1):68–84. doi:10.1016/j.apal.2011.08.005
• –––, 2015, “The Doxastic Interpretation ofTeam Semantics”,Logic Without Borders: Essays on SetTheory, Model Theory, Philosophical Logic and Philosophy ofMathematics (Ontos Mathematical Logic, 5), Åsa Hirvonen,Juha Kontinen, Roman Kossak, and Andrés Villaveces (eds),Berlin, Boston: De Gruyter, pp. 167–192.doi:10.1515/9781614516873.167
• –––, 2015, “Upwards closed dependencies inteam semantics”,Information and Computation, 245:124–135.
• –––, 2019, “Characterizing downwardsclosed, strongly first-order, relativizable dependencies”,The Journal of Symbolic Logic, 84(3): 1136–1167
• –––, 2021, “Safe dependency atoms andpossibility operators in team semantics.”Information andComputation, 278: 104593.
• –––, 2022, “Strongly First Order, DomainIndependent Dependencies: The Union-Closed Case.”Logic,Language, Information, and Computation, 263–279.
• –––, 2024, “Doubly strongly first-orderdependencies.”Journal of Logic and Computation,exae056.
• Galliani, Pietro and Lauri Hella, 2013, “Inclusion Logic andFixed Point Logic”,Computer Science Logic 2013(Leibniz International Proceedings in Informatics: LIPIcs 23),Dagstuhl, Germany: Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik,pp. 281–295. doi:10.4230/LIPIcs.CSL.2013.281
• Galliani, Pietro and Jouko Väänänen, 2014,“On Dependence Logic”, inJohan van Benthem on Logicand Information Dynamics (Outstanding contributions to logic, 5),Alexandru Baltag and Sonja Smets (eds), Cham: Springer, pp.101–119. doi:10.1007/978-3-319-06025-5_4
• Grädel, Erich and Jouko Väänänen, 2013,“Dependence and Independence”,Studia Logica,101(2): 399–410. doi:10.1007/s11225-013-9479-2
• Grädel, Erich and Richard Wilke, 2022, “Logics withmultiteam semantics”,ACM Transactions on ComputationalLogic (TOCL), 23(2): 1–30. doi:10.1145/3487579
• Groenendijk, Jeroen, 2009, “Inquisitive Semantics: TwoPossibilities for Disjunction”, in Peter Bosch, David Gabelaia,& Jérôme Lang (eds),Seventh internationalTbilisi Symposium on Language, Logic, and Computation (LectureNotes in Computer Science: Volume 5422), Springer-Verlag, pp.80–94. doi:10.1007/978-3-642-00665-4_8
• Gutsfeld, Jens Oliver, Meier, Arne, Ohrem, Christoph and Virtema,Jonni, 2022, “Temporal Team Semantics Revisited”.LICS‘22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic inComputer Science, 44. doi:10.1145/3531130.3533360
• Hannula, Miika and Juha Kontinen, 2016, “A FiniteAxiomatization of Conditional Independence and InclusionDependencies”.Information and Computation, 249:121–137. doi:10.1016/j.ic.2016.04.001
• Hannula, Miika, et al., 2018, “Complexity of propositionallogics in team semantic”,ACM Transactions on ComputationalLogic, 19(1): 1–14.
• –––, 2019, “Facets of distributionidentities in probabilistic team semantics”, in F. Calimeri, N.Leone, and M. Manna (eds.),Logics in ArtificialIntelligence, Cham: Springer.
• –––, 2020, “Descriptive complexity of realcomputation and probabilistic independence logic”,Proceedings of the 35th Annual ACM/IEEE Symposium on Logic inComputer Science, Association for Computing Machinery, New York:550–563.
• Hannula, Miika and Virtema, Jonni, “Tractability frontiersin probabilistic team semantics and existential second-order logicover the reals”,Annals of Pure and Applied Logic173(1): 103108. doi:10.1016/j.apal.2022.103108.
• Hella, Lauri, Kerkko Luosto and Jouko Väänänen,2024, “Dimension in team semantics”,MathematicalStructures in Computer Science, 34(5): 410–454.doi:10.1017/S0960129524000021
• Henkin, Leon, 1961, “Some Remarks on Infinitely LongFormulas”, inInfinitistic Methods (Proceedings of theSymposium on the Foundations of Mathematics, Warsaw, 1959), Oxford:Pergamon Press, pp. 167–183.
• Hodges, Wilfrid, 1997, “Compositional Semantics for aLanguage of Imperfect Information”,Logic Journal of theIGPL, 5(4): 539–563. doi:10.1093/jigpal/5.4.539
• Hyttinen, Tapani, Gianluca Paolini and JoukoVäänänen, 2015, “Quantum Team Logic andBell’s Inequalities”,The Review of SymbolicLogic, 8(4): 722–742. doi:10.1017/S1755020315000192
• Kontinen, Juha and Ville Nurmi, 2009, “Team Logic andSecond-Order Logic”, inProceedings of the 16thInternational Workshop on Logic, Language, Information, andComputation (Lecture Notes in Computer Science, 5514), Berlin,Heidelberg: Springer, pp. 230–241.doi:10.1007/978-3-642-02261-6_19
• Kontinen, Juha and Jouko Väänänen, 2009, “OnDefinability in Dependence Logic”,Journal of Logic,Language and Information, 18(3):317–332.doi:10.1007/s10849-009-9082-0
• –––, 2011, “A Remark on Negation inDependence Logic”,Notre Dame Journal of Formal Logic,52(1): 55–65. doi:10.1215/00294527-2010-036
• –––, 2013, “Axiomatizing First-OrderConsequences in Dependence Logic”,Annals of Pure andApplied Logic, 164(11): 1101–1117.doi:10.1016/j.apal.2013.05.006
• Kontinen, Juha, et al., 2017, “Modal independencelogic”,Journal of Logic and Computation, 27(5):1333–1352.
• Kontinen, Juha and Fan Yang, 2019, “Logics for first-orderteam properties”,International Workshop on Logic, Language,Information, and Computation, Berlin, Heidelberg: Springer.
• Kripke, Saul A., 1965, “Semantical Analysis ofIntuitionistic Logic I”, inFormal Systems and RecursiveFunctions: Proceedings of the Eighth Logic Colloquium, Oxford July1963 (Studies in Logic and the Foundations of Mathematics, 40),John N. Crossley and Michael A. E. Dummett (eds.), North Holland, pp.92–130. doi:10.1016/S0049–237X(08)71685-9
• Kuusisto, Antti, 2015, “A double team semantics forgeneralized quantifiers”,Journal of Logic, Language andInformation, 24(2): 149–191.
• Lohmann, Peter and Heribert Vollmer, 2013, “ComplexityResults for Modal Dependence Logic”,Studia Logica,101(2): 343–366. doi:10.1007/s11225-013-9483-6
• Lück, Martin, 2018, “Axiomatizations of teamlogics”,Annals of Pure and Applied Logic, 169(9):928–969.
• –––, 2020, “On the complexity of lineartemporal logic with team semantics”,Theoretical ComputerScience, 837: 1–25.
• Pacuit, Eric and Fan Yang, 2016, “Dependence andIndependence in Social Choice: Arrow’S Theorem”, inDependence Logic, Samson Abramsky, Juha Kontinen, JoukoVäänänen, and Heribert Vollmer (eds), Dordrecht:Springer, pp. 235–260. doi:10.1007/978-3-319-31803-5_11
• Väänänen, Jouko, 2007a,Dependence Logic: A NewApproach to Independence Friendly Logic, (London MathematicalSociety student texts, 70), Cambridge: Cambridge University Press.doi:10.1017/CBO9780511611193
• –––, 2007b, “Team Logic”, inInteractive Logic: Selected Papers from the 7th Augustus de MorganWorkshop, (Texts in Logic and Games, 1), Johan van Benthem, DovGabbay, and Benedikt Löwe (eds.), Amsterdam: Amsterdam UniversityPress, pp. 281–302.
• –––, 2008, “Modal Dependence Logic”,New Perspectives on Games and Interaction (Texts in Logic andGames, 4), Krzysztof R. Apt and Robert van Rooij (eds), Amsterdam:Amsterdam University Press, pp.237–254.
• Virtema, Jonni, 2017, “Complexity of validity forpropositional dependence logics”,Information andComputation, 253: 224–236.
• Yang, Fan, 2013, “Expressing Second-Order Sentences inIntuitionistic Dependence Logic”,Studia Logica,101(2): 323–342. doi:10.1007/s11225-013-9476-5
• –––, 2014, “On Extensions and Variants ofDependence Logic: A Study of Intuitionistic Connectives in the TeamSemantics Setting”. PhD Thesis, University of Helsinki.
• Yang, Fan and Jouko Väänänen, 2016,“Propositional Logics of Dependence”,Annals of Pureand Applied Logic, 167(7): 557–589.doi:10.1016/j.apal.2016.03.003

Academic Tools

	How to cite this entry.
	Preview the PDF version of this entry at theFriends of the SEP Society.
	Look up topics and thinkers related to this entry at the Internet Philosophy Ontology Project (InPhO).
	Enhanced bibliography for this entryatPhilPapers, with links to its database.

Other Internet Resources

• Krebs, Andreas, et al., 2017, “Team semantics for the specification and verification of hyperproperties”, manuscript at arXiv.org.
• Dependence Logic on Wikipedia

Related Entries

compositionality | game-theoretic semantics and pragmatics |logic: and games |logic: classical |logic: independence friendly |logic: second-order and higher-order