Team Logic

Origin. Jouko Väänänen, Dependence Logic (2007), §8, where it appears as the closure of dependence logic under a genuine negation; Juha Kontinen and Ville Nurmi, "Team logic and second-order logic" (2009), settled its expressive power. The system exists to answer an obvious question: dependence logic's negation is the game-theoretic dual, so what happens if you add the contradictory one?

Models. Dependence logic plus ∼, where ∼φ means simply that φ fails. That single addition breaks the family's ceiling: every other team-semantic logic in this division sits at Σ¹₁, and team logic is full second-order logic. The reason is that a contradictory negation restores the classical duality the team semantics had traded away, and with it the ability to quantify over the whole relational hierarchy.

Formalism.

The two negations: ¬φ — the dual negation of dependence logic: X ⊨ ¬φ iff X negatively satisfies φ. ∼φ — contradictory: X ⊨ ∼φ iff X ⊭ φ. In dependence logic ¬¬φ ≡ φ and φ ∨ ¬φ is not valid. With ∼, φ ∨ ∼φ is valid and ∼ is not definable from ¬.

What the addition costs: Downward closure fails: ∼φ is not downward closed even when φ is. The empty team property fails: ∅ ⊭ ∼φ when ∅ ⊨ φ, which is always. Both properties the family is organized by are gone.

Expressive power (Kontinen–Nurmi 2009): Team logic ≡ full second-order logic, on sentences. Dependence logic = Σ¹₁; adding ∼ climbs the whole hierarchy. The alternation of ∼ with the splitting disjunction generates the second-order quantifier alternation.

Why not just use SOL: Team logic reaches SOL with a first-order syntax and one extra connective. The second-order quantification is in the semantics, not the language — which is the same trade dependence logic makes for Σ¹₁, run to its end.

Relation to the family: dependence ⊊ independence ≡ inclusion–exclusion ⊊ team logic The first three are Σ¹₁ on sentences. Only team logic escapes.

Symbols.

Symbol	Unicode	Name	Meaning
∼	U+223C	Contradictory negation	X ⊨ ∼φ iff X ⊭ φ
¬	U+00AC	Dual negation	Dependence logic's game negation
X	—	Team	Set of assignments
SOL	—	Second-order logic	The expressive ceiling reached
Σ¹₁	U+03A3	Sigma-1-1	Where the rest of the family sits

Metatheory. The Kontinen–Nurmi theorem is the division's sharpest result: one connective moves a logic from NP to the full analytical hierarchy, and it does so by restoring a negation the team semantics had deliberately not had. That makes the family's Σ¹₁ ceiling visible as a choice — it is a consequence of using the dual negation, not of using teams — and it locates dependence logic's tractability precisely. Losing downward closure and the empty team property together shows how load-bearing they were: every proof technique in the rest of the division uses one or the other.

Applies to. The expressive-power analysis of team semantics. Second-order logic, reached from a first-order syntax. The classification of the team family by closure properties, for which team logic is the boundary case.

Limitations. Full second-order expressive power means no completeness theorem, no compactness, and no Löwenheim–Skolem — everything dependence logic keeps, team logic loses. The system has no proof theory and no application: it exists to mark the boundary, and the literature on it is a handful of papers about its strength rather than its use. And two negations in one language is a presentational burden that nothing in the semantics motivates beyond the fact that both are definable.