Intuitionistic Dependence Logic

Origin. Samson Abramsky and Jouko Väänänen, "From IF to BI" (Synthese, 2009), which introduced the implication and named the connection it exposes; Fan Yang, "Expressing second-order sentences in intuitionistic dependence logic" (2010), proved the expressive power. The second of the two routes from dependence logic to full second-order logic, and the one nobody expected.

Models. Dependence logic has no implication — the splitting disjunction and the dual negation give no way to say "if φ then ψ" of a team. The natural definition quantifies over subteams: φ → ψ holds of X when every subteam satisfying φ satisfies ψ. That clause is intuitionistic implication's, transposed from Kripke's worlds to teams, and the resemblance is not superficial: subteams ordered by inclusion are a Kripke frame, and downward closure is persistence.

Formalism.

The intuitionistic implication: X ⊨ φ → ψ iff for all Y ⊆ X: if Y ⊨ φ then Y ⊨ ψ Quantifies over subteams, as Kripke's clause quantifies over accessible worlds. The subteam order is the accessibility relation; downward closure is persistence.

Why it is not classical: φ → ψ is not ∼φ ∨ ψ — there is no contradictory negation available. The clause is intuitionistic because the team order is a preorder and the semantics is persistent.

Expressive power (Yang 2010): Dependence logic + → ≡ full second-order logic. The same ceiling team logic reaches with the contradictory negation ∼, reached instead by an implication that adds no negation at all.

Two routes, one destination: dependence + ∼ = SOL (Kontinen–Nurmi 2009) dependence + → = SOL (Yang 2010) Neither addition is definable from the other, and both escape Σ¹₁. So the Σ¹₁ ceiling is fragile in two independent ways.

The BI connection (Abramsky–Väänänen): The splitting disjunction is a multiplicative connective; the intuitionistic implication is additive. Team semantics has both, which is the signature of bunched logic — BI's ∗ and its additive → over the same context. The paper's title is the claim: the logic of imperfect information is a bunched logic.

Symbols.

Metatheory. Yang's result and Kontinen–Nurmi's together are the interesting fact: dependence logic sits at Σ¹₁ and two unrelated additions — one a negation, one an implication — each take it to full second-order logic. The Σ¹₁ ceiling is therefore not a robust feature of team semantics but an artifact of the connective set, and the family's careful expressive hierarchy holds only for a language chosen to keep it. Abramsky and Väänänen's identification of the bunched structure is the deeper point: teams carry a multiplicative and an additive connective over the same context, which is what BI is, and it means the logic of imperfect information and the logic of resource separation are instances of one pattern.

Applies to. The expressive analysis of team semantics. Bunched logic, where the structural resemblance is exact and cross-listed. Intuitionistic semantics over orders other than worlds. The question of which connectives team semantics can support without collapse.

Limitations. Full second-order power carries the usual costs — no completeness, no compactness, no Löwenheim–Skolem — and buys nothing dependence logic wanted. The implication is defined and not motivated: it is the clause that works, and the intuitionistic reading is read off the clause rather than argued for. The BI connection is structural and has not produced a transfer of results in either direction, which is what would make it more than a resemblance.

© 2026 Lingenic LLC