Modal Dependence Logic

Origin. Jouko Väänänen, "Modal dependence logic" (in New Perspectives on Games and Interaction, 2008), transposing his 2007 first-order dependence logic to the modal setting. Sevenster (2009) settled the complexity; Ebbing, Lohmann, Hella, Kontinen, Müller, and Vollmer mapped the fragments (2011–2013); Yang and Väänänen (2016) gave the propositional theory.

Models. A modal formula is evaluated at a world. A modal dependence formula is evaluated at a set of worlds — and once it is, one can say that the value of p is determined by the value of q across that set, which no formula evaluated at a single world can say. The team is a set of worlds rather than of assignments, and the atoms constrain the team.

Formalism.

Teams of worlds: For a Kripke model M = (W, R, V) and T ⊆ W, satisfaction is M, T ⊨ φ. Classical formulas are lifted pointwise: M, T ⊨ p iff M, w ⊨ p for every w ∈ T.

The dependence atom: M, T ⊨ =(p₁, ..., pₙ, q) iff for all w, w′ ∈ T: if V(w)(pᵢ) = V(w′)(pᵢ) for all i, then V(w)(q) = V(w′)(q). Within the team, the pᵢ determine q. =(q) alone says q is constant across T.

Connectives: M, T ⊨ φ ∧ ψ iff T ⊨ φ and T ⊨ ψ M, T ⊨ φ ∨ ψ iff T = T₁ ∪ T₂ with T₁ ⊨ φ and T₂ ⊨ ψ (splitting, as in dependence logic)

The modality: M, T ⊨ ◇φ iff there is a nonempty S ⊆ ⋃_{w ∈ T} R[w] with S ∩ R[w] ≠ ∅ for every w ∈ T, and M, S ⊨ φ. The diamond chooses successors for the whole team at once. M, T ⊨ □φ iff M, R[T] ⊨ φ.

Closure: Downward closed: T ⊨ φ and S ⊆ T gives S ⊨ φ. Empty team property: ∅ ⊨ φ always. Same closure as first-order dependence logic; the atoms are the same shape.

Complexity (Sevenster 2009): Satisfiability is NEXPTIME-complete — one exponential above K's PSPACE. Model checking is NP-complete. The fragments with restricted ◇ or with a bounded dependence arity drop to lower classes.

Propositional dependence logic (Yang–Väänänen 2016): Teams of valuations rather than of worlds; no modality. Axiomatized completely, unlike the first-order case.

Symbols.

Metatheory. The NEXPTIME-completeness is the result that makes the logic worth having and worth avoiding: adding one atom to K, which is PSPACE, costs an exponential, and the cost comes entirely from the splitting disjunction interacting with the dependence atom. Propositional dependence logic is the tractable and completely axiomatized fragment, which the first-order case is not — the modal setting is where team semantics is best behaved and least expressive. The downward-closure property lines this up with dependence and exclusion logic rather than with inclusion logic, so the family's split by closure property survives the transposition.

Applies to. Multi-agent settings where an agent's knowledge determines another's. Database dependencies over transition systems. The comparative study of team semantics across settings, where the modal case is the tractable specimen. Verification of information-flow properties, where "the output depends only on the low input" is a dependence atom.

Limitations. NEXPTIME satisfiability puts it beyond practical reasoning for anything but small instances, and the fragments that are tractable are expressively thin. There is no natural deduction or sequent system for the full logic — the axiomatization exists only for the propositional fragment. And the team-of-worlds reading strains the intuition that made first-order dependence logic compelling: a team of assignments is a database, and a team of worlds is a set of possibilities that no agent's information state need correspond to.

© 2026 Lingenic LLC