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.

Symbol	Unicode	Name	Meaning
=(x̄,y)	—	Dependence atom	y determined by x̄
⊥	U+22A5	Up tack / Independence atom	x̄ ⊥_z̄ ȳ: conditionally independent
⊆	U+2286	Subset / Inclusion atom	Values of x̄ among values of ȳ
\|	—	Vertical line / Exclusion atom	Value sets disjoint
X	—	Team	Set of assignments
⊨_X	—	Team satisfaction	Truth of a formula in a team
⊗	U+2297	Circled times / Tensor	Alternative notation for the splitting disjunction
∨	U+2228	Logical or	Splitting disjunction: the team divides
∧	U+2227	Logical and	Both conjuncts hold of the whole team
∃	U+2203	Existential quantifier	Supplements the team by a choice function
∀	U+2200	Universal quantifier	Duplicates the team over the domain
∪	U+222A	Union	Recombines the two halves of a split
∈	U+2208	Element of	Assignment belonging to a team
s	—	Assignment	A member of the team

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 — ∃z ∀x₁ ∀x₂ ∃y₁ ∃y₂ (=(x₁,y₁) ∧ =(x₂,y₂) ∧ (x₁ = x₂ ↔ y₁ = y₂) ∧ y₁ ≠ z) is true in a model iff its domain is infinite, which no first-order formula can say. This is Ehrenfeucht's branching-quantifier infinity sentence: the dependence atoms make y₁ and y₂ functions of x₁ and x₂ alone, the biconditional makes that function injective, and z is outside its range. The shorter ∀x∃y (=(y,x) ∧ y ≠ x) will not do — it says only that some injective fixed-point-free function exists, which any domain of even size admits (take {0,1} and y = 1 − x). 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 — Σ⁰₁-complete, so refutations are still recursively enumerable even though validities are not. 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. Validity is not axiomatizable: the set of valid sentences is Π₂-complete in the Lévy hierarchy, so no recursive proof system captures it, and only the fragment φ ⊨ ψ with ψ first-order admits a complete calculus (Kontinen and Väänänen, 2013). Downward closure is a ceiling on expression as well as a proof technique — no formula defines a team property that is not downward closed, which is exactly why the inclusion atom and the independence atom are not definable at the formula level. The empty team satisfies every formula, so nonemptiness of a team is inexpressible. Being Σ¹₁, the logic captures NP over finite structures and therefore no co-NP-complete property unless NP = co-NP: non-3-colourability has no sentence, and well-foundedness, being Π¹₁, has none either. The negation is the game-theoretic dual rather than the contradictory one, so excluded middle fails; restoring the contradictory negation lifts the logic to full second-order logic and destroys compactness and Löwenheim–Skolem.