Dependence Logic

Origin. Jouko Väänänen introduced dependence logic (2007), building on Hintikka's IF logic. Uses team semantics: formulas evaluated on sets of assignments, not single assignments. The dependence atom =(x,y) expresses "y is functionally determined by x." Clean semantics while capturing IF logic's expressiveness. Foundation for a family of logics: independence, inclusion, exclusion.

Models. Functional dependence between variables. In a database: =(SSN, Name) means social security number determines name. In logic: across all assignments in a team, the value of y depends only on x. Team semantics: truth is about patterns across multiple possibilities, not single states.

Formalism.

Team semantics: A team X is a set of assignments s: Var → Domain. Formulas evaluated as: M ⊨_X φ (model M, team X satisfies φ).

Dependence atom: =(x₁,...,xₙ,y) — y is functionally determined by x₁,...,xₙ. M ⊨_X =(x̄,y) iff for all s, s' ∈ X: if s(x̄) = s'(x̄) then s(y) = s'(y).

First-order fragment: On singleton teams {s}, dependence logic = first-order logic. Dependence only matters with multiple assignments.

Connectives and quantifiers:

• Disjunction splits teams: M ⊨_X φ∨ψ iff X = Y ∪ Z and M ⊨_Y φ and M ⊨_Z ψ
• Conjunction: M ⊨_X φ∧ψ iff M ⊨_X φ and M ⊨_X ψ
• Existential: M ⊨X ∃xφ iff M ⊨{X[x/A]} φ for some function choosing witnesses
• Universal: M ⊨X ∀xφ iff M ⊨{X[x/M]} φ where all domain elements added

Extensions:

• Independence: x ⊥_z y (x independent of y given z)
• Inclusion: x ⊆ y (values of x are among values of y)
• Exclusion: x | y (values of x and y are disjoint)

Database connection: Dependence atoms = functional dependencies. Teams = relations (tables). Formulas = constraints on relations.

Symbols.

Metatheory. Conservative extension of first-order logic: on sentences and on singleton teams it is FOL exactly, so nothing classical is lost. Strictly stronger, and the demonstration is one sentence — ∀x∃y (=(y,x) ∧ y ≠ x) is true in a model iff its domain is infinite, which no first-order formula can say. At the sentence level dependence logic = Σ¹₁, hence NP over finite structures by Fagin's theorem; at the formula level it is the downward monotone fragment of Σ¹₁, which is what separates it from independence logic. Downward closed: X ⊨ φ and Y ⊆ X gives Y ⊨ φ. Not union closed — that is inclusion logic's property, and the two closure conditions are what divide the family. The empty team satisfies everything, positively and negatively. Excluded middle fails: φ ∨ ¬φ is neither positively nor negatively satisfied by some teams; disjunction is not idempotent and does not distribute over conjunction. Compactness and Löwenheim–Skolem both hold. Craig interpolation holds in a modified form: if φ and ψ are contradictory, a first-order interpolant exists in the shared language — the modification is forced because the negation is not contradictory. For the same reason dependence logic defines its own truth predicate without contradicting Tarski's undefinability theorem. The decision problem is non-arithmetical, Σ₂-complete in the Lévy hierarchy, while the inconsistency problem is only as hard as FOL's. Locality: satisfaction depends only on the variables occurring free.

Applies to. Database theory (dependencies, normal forms). Social choice (independence of irrelevant alternatives). Quantum mechanics (contextuality). Information theory. Philosophy (supervenience, determination).

Limitations. Team semantics is non-classical; intuitions from FOL may fail. Negation requires care (game negation vs contradictory). Complexity high (Σ₁¹). Practical tools are limited. The family of logics (dependence, independence, inclusion) is still developing. Less mature than classical alternatives.

© 2026 Lingenic LLC