Team Semantics

Origin. Hodges (1997), Väänänen (2007). Dependence logic. Sets of assignments. Independence-friendly logic semantics. Foundation for dependence concepts.

Models. Truth relative to teams (sets of assignments). Dependencies expressible in object language. Compositional semantics for IF logic. Captures database-like dependencies.

Formalism.

Teams: Team X = set of assignments. Assignment s: Var → Domain. X satisfies φ: M ⊨ₓ φ. Set-based satisfaction.

Atomic dependence: =(x₁,...,xₙ,y): value of y depends on x₁,...,xₙ. M ⊨ₓ =(x̄,y) iff for all s,s' ∈ X: s(x̄) = s'(x̄) implies s(y) = s'(y). Functional dependency.

Independence: x ⊥_z y: x independent of y given z. No correlation between x, y holding z fixed. Database-style independence. Key notion in dependence logic.

Downward closure: If M ⊨ₓ φ and Y ⊆ X, then M ⊨ᵧ φ. Dependence atoms have this, and so does the whole of dependence logic — a functional dependency that holds across a team still holds across any subteam.

Union closure: If M ⊨ₓ φ and M ⊨ᵧ φ, then M ⊨_{X∪Y} φ. Dependence atoms do not have this. Take X = {s} with s(x)=0, s(y)=0 and Y = {s'} with s'(x)=0, s'(y)=1: each singleton satisfies =(x,y), the union does not. Union closure is inclusion logic's property, not dependence logic's; the two closure conditions are what divide the family, and independence atoms have neither.

Expressive power: Dependence logic = Σ¹₁ (existential SO). Captures NP. More expressive than FO. Maintains compositional semantics.

Extensions: Independence logic. Inclusion logic. Exclusion logic. Team-based modal logic.

Symbols.

Symbol	Unicode	Name	Meaning
X	—	Team	A set of variable assignments
=(x̄,y)	—	Dependence atom	y is functionally determined by x̄ across the team
x ⊥_z y	—	Independence atom	x and y are independent given z
⊨ₓ	—	Team satisfaction	Truth relative to the team X, not a single assignment
s	—	Assignment	A member of the team, Var → Domain
⊆	U+2286	Subteam	Y ⊆ X, the relation downward closure runs along
∪	U+222A	Union	X ∪ Y, the relation union closure runs along
∨	U+2228	Disjunction	Splits the team: X = Y ∪ Z with Y ⊨ φ, Z ⊨ ψ
Σ¹₁	—	Existential second-order	The expressive ceiling of dependence logic

Metatheory. Satisfaction relates a structure to a set of assignments, and first-order formulas are flat — a team satisfies φ iff every assignment in it does — so team semantics conservatively extends Tarskian semantics. The empty team satisfies everything, and satisfaction is local, depending only on the free variables. Dependence logic sentences are equi-expressive with Σ¹₁, so by Fagin's theorem (1974) they capture NP over finite structures, and model checking is NP-complete. Kontinen and Väänänen (2009) settled definability: a team property is expressible in dependence logic exactly when it is Σ¹₁, downward closed, and holds of the empty team. Independence logic reaches all of Σ¹₁ at the formula level (Galliani 2012), while inclusion logic sentences coincide with greatest-fixed-point logic and capture PTIME on ordered finite structures (Galliani and Hella 2013). Since Σ¹₁ is compact and satisfies downward Löwenheim–Skolem, so does dependence logic; validity is not recursively enumerable, but Kontinen and Väänänen (2013) axiomatized its first-order consequences.

Applies to. Database theory. Independence concepts. IF logic. Expressiveness studies.

Limitations. The logic is not closed under contradictory negation. The negation of a dependence atom is satisfied only by the empty team, so =(x,y) ∨ ¬=(x,y) is equivalent to =(x,y) and excluded middle fails. Adding a genuine contradictory negation raises expressive power to full second-order logic, at which point compactness, Löwenheim–Skolem and any effective proof system are lost. That dependence logic is compact and has downward Löwenheim–Skolem without being first-order does not refute Lindström's theorem, since Lindström assumes closure under negation — the escape comes precisely from the missing connective. Validity being non-r.e., there is no complete deduction system for the full logic, only for its first-order consequences. Downward closure and union closure hold in different members of the family, so results transfer between dependence, inclusion and independence logic only where the relevant closure condition is shared.