# Independence Logic

**Origin.** Erich Grädel and Jouko Väänänen, "Dependence and independence" (Studia Logica, 2013). First-order logic with the independence atom, proposed because dependence logic's downward closure was an artifact of the dependence atom rather than of team semantics — independence is the notion that team semantics was reaching for and could not express.

**Models.** Given the values of z̄, knowing x̄ tells you nothing about ȳ. The atom is conditional independence, in the probabilistic shape but with no probability: it is about what the team's value-combinations are, not about how often they occur. It is neither downward closed nor union closed, which distinguishes it from both of its neighbours.

**Formalism.**

*The independence atom:*
M, X ⊨ x̄ ⊥_z̄ ȳ  iff  for all s, s′ ∈ X with s(z̄) = s′(z̄),
  there is s″ ∈ X with s″(z̄) = s(z̄), s″(x̄) = s(x̄), s″(ȳ) = s′(ȳ).
Every combination of x̄- and ȳ-values compatible with a fixed z̄ is realized.

*Pure independence:*
x̄ ⊥ ȳ is x̄ ⊥_∅ ȳ, the unconditional case.

*Dependence is definable:*
=(x̄, ȳ)  ≡  ȳ ⊥_x̄ ȳ
So dependence logic embeds; independence logic is at least as strong.

*Closure — the distinguishing fact:*
Not downward closed (unlike dependence and exclusion).
Not union closed (unlike inclusion).
It sits in neither closure class, which is why it needed its own atom.

*Expressive power:*
Sentences: Σ¹₁, the same as dependence logic.
Formulas: strictly stronger — dependence-logic formulas are downward closed and independence-logic formulas need not be.
Equivalent to inclusion–exclusion logic (Galliani 2012).

**Symbols.**

| Symbol | Unicode | Name | Meaning |
|--------|---------|------|---------|
| ⊥ | U+22A5 | Independence atom | x̄ ⊥_z̄ ȳ: conditional independence |
| =( ) | — | Dependence atom | Definable as ȳ ⊥_x̄ ȳ |
| X | — | Team | Set of assignments |
| Σ¹₁ | — | Sigma-1-1 | The sentence-level strength |

**Metatheory.** The sentence-level equivalence with dependence logic alongside the formula-level separation is the result that makes the family's structure visible: Σ¹₁ is a ceiling on sentences that several atoms reach, while the closure properties separate the logics below it. Independence logic's atom is the database notion of embedded multivalued dependency, and the connection to conditional independence in probability theory and in graphical models is exact in form and empty of measure — which is either the interesting fact about it or the reason it misleads, depending on who is writing.

**Applies to.** Database theory (multivalued and embedded dependencies). Comparative team semantics. The qualitative skeleton of conditional-independence reasoning, where it borders on graphical models without importing probability.

**Limitations.** No compositional contradictory negation. The probabilistic reading of the atom invites a transfer that does not hold: there is no measure here, and independence in a team is a combinatorial completeness condition on value-tuples, not a factorization of a distribution. Whether independence logic is the right base for the family, or merely the strongest of several atoms reaching the same ceiling, is not settled by the equivalences.

© 2026 Lingenic LLC