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 ∼, excluded middle returns for the Boolean disjunction ∼(∼φ ∧ ∼ψ) — not for the splitting ∨ — 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.

Metatheory. Kontinen and Nurmi (2009) proved that team logic sentences are expressively equivalent to full second-order logic; over finite structures that is the whole polynomial hierarchy rather than NP alone. One connective does this, 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. The cost is exact: downward closure fails because ∼φ need not be downward closed even when φ is, and the empty team property fails because ∅ ⊨ φ always, so ∅ ⊭ ∼φ always. Losing both together shows how much depended on them, since every proof technique in the rest of the division uses one or the other. Full second-order strength also removes compactness, downward Löwenheim–Skolem, and any recursive axiomatization, all of which dependence logic retains.

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.

© 2026 Lingenic LLC