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	Up tack / Independence atom	x̄ ⊥_z̄ ȳ: conditional independence
=( )	—	Dependence atom	Definable as ȳ ⊥_x̄ ȳ
X	—	Team	Set of assignments
Σ¹₁	—	Sigma-1-1	Existential second-order; the sentence-level strength
⊨	U+22A8	True / Satisfaction	Between a model-team pair and a formula
∈	U+2208	Element of	Assignment belonging to a team
∅	U+2205	Empty set	The unconditional case x̄ ⊥_∅ ȳ; also the empty team
≡	U+2261	Identical to / Equivalent	Interdefinability of atoms
′	U+2032	Prime	Second assignment in the atom's clause
″	U+2033	Double prime	Witness assignment in the atom's clause

Metatheory. Galliani (2012) settled the formula level: a class of teams is definable in independence logic iff it is Σ¹₁-definable and contains the empty team, so the downward-closure clause that Kontinen and Väänänen (2009) had to impose for dependence logic simply drops away. On sentences the two logics coincide at Σ¹₁, hence NP over finite structures by Fagin's theorem, and the data complexity of model checking is NP-complete. Galliani also proved independence logic equivalent to inclusion–exclusion logic. Locality and the empty team property hold; neither downward closure nor union closure does. Validity is inherited from dependence logic and is non-arithmetical, so no recursive axiomatization exists. The sentence-level equivalence alongside the formula-level separation is what makes the family's structure visible: Σ¹₁ is a ceiling on sentences that several atoms reach, while the closure properties separate the logics below it. The 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; adding one lifts the logic to full second-order logic and costs compactness and Löwenheim–Skolem. At the sentence level independence logic gains nothing over dependence logic — both are Σ¹₁ — so the extra strength is invisible wherever theories rather than open formulas are the object, and over finite structures every definable class is in NP, putting co-NP-complete properties out of reach unless NP = co-NP. Validity has no recursive axiomatization. Because the logic is neither downward nor union closed, the proof techniques the rest of the family relies on do not apply to it. 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.