Linglib.Core.Logic.Modal.Dependence

[Vaa08] [Vaa07]

MDL is the modal extension of dependence logic introduced in [Vaa08] ("Modal Dependence Logic", in Apt & van Rooij eds. New Perspectives on Games and Interaction, pp. 237-254). It adds a dependence atom =(p₁,...,pₙ; q) to classical modal logic, meaning "the value of q is functionally determined by the values of p₁,...,pₙ across the team."

The framework is grounded in Väänänen's foundational [Vaa07] (the Dependence Logic book, Cambridge University Press 2007), which develops the first-order team-semantic apparatus that MDL adapts to modal logic. Where the book's quantifiers range over assignments, MDL's modalities range over Kripke worlds — but the team-semantic skeleton (formulas as predicates of teams, downward closure, dependence atoms) transfers directly.

MDL is studied for its computational and model-theoretic properties (satisfiability complexity in [LV13] and Sevenster's earlier expressive-power work; bisimulation invariance), with applications in database theory, knowledge representation, and AI rather than primarily in linguistic semantics — hence the placement in Core/Logic/ rather than Semantics/, alongside the other team-semantic primitives (Core/Logic/Team/, Core/Logic/Bilateral/).

What changes from BSML #

MDL and BSML share a bilateral semantics (Player II = support, Player I = anti-support, negation flips polarity per [Vaa08] clause (T5)) and the same Kripke-model carrier. The structural differences:

Atom: BSML's NE becomes MDL's dep. =(x⃗; y) is supported by a team iff any two worlds agreeing on x⃗ also agree on y.
Modal operator clauses: MDL's ◇-support uses a single witness Y ([Vaa08] clause (T8)) — ∃ Y, (∀ w ∈ s, ∃ y ∈ Y, y ∈ R[w]) ∧ support φ Y — rather than BSML's per-world witnesses. Similarly, ◇-anti-support uses the union of accessibility images (T9) rather than per-world checks. The two formulations are equivalent under union-closure but diverge for MDL since dep atoms break it.

Closure profile #

MDL's closure profile differs from BSML's, placing it in a different cell of the closure-property lattice:

Property	BSML (NE-free)	BSML (with NE)	MDL
`IsLowerSet`	✓	broken by NE	✓ (Lemma 4.2)
`SupClosed`	✓	✓	broken by `dep`
`∅ ∈ support`	✓	✓	✓

The dep atom is downward-closed (subteam of a functionally-dependent team is functionally dependent) but breaks union-closure (two functionally-dependent teams may have conflicting y values at worlds with matching x⃗).

Main declarations #

Formula — MDL syntax (Definition 1.1).
eval — bilateral semantics (Definition 4.1), parametric in polarity.
support / antiSupport — convenience abbreviations.
Formula.modalDepth — depth of nested ◇.
isBilateral — Core.Logic.Bilateral.IsBilateral instance.
isLowerSet_support — Lemma 4.2's downward-closure property.
support_empty — every formula is supported on the empty team.
not_supClosed_dep_of_witness — the witness that dep breaks union-closure: in any model with two worlds sharing a p-value but differing on q, the singleton teams support =(p; q) but their union does not.

Implementation notes #

The MDL eval uses Väänänen's exact clauses, not BSML's. The disjunction clause is the under-DC simplified form X = Y ∪ Z (paper's (T6)' under Lemma 4.2 part 1) rather than the literal X ⊆ Y ∪ Z from (T6); under downward closure they are equivalent.

The KripkeModel carrier from Core/Logic/Modal/Kripke.lean is the shared substrate; BSML, QBSML, and the AAY-2024 extensions (BSMLOr/BSMLEmpty) alias BSMLModel := KripkeModel for literature compatibility.

Sibling logics in `Core/Logic/Modal/` #

This directory houses modal-logic variants that share Kripke-model infrastructure but differ in atom flavor:

Modal/Kripke.lean — the carrier type, shared.
Modal/Dependence.lean (this file) — MDL with dependence atoms.
Modal/Inclusion.lean (future) — modal inclusion logic ML(⊆), introduced by Galliani; axiomatized in [Ant25] Ch 5.
Modal/Independence.lean (future) — modal independence logic (Grädel and Väänänen).
Modal/Bilateral.lean (future, after BSML's eventual Core/ graduation) — BSML's bilateral negation + NE atom.

The bisimulation substrate currently lives at Core/Logic/Modal/BSML/Bisimulation.lean for historical reasons; a future refactor lifts it to Core/Logic/Modal/Bisimulation.lean.

Todo #

[LV13] — adds classical disjunction ⓿ (the BSML∨ analogue) and complete satisfiability complexity classification. Natural second consumer paper, with a Studies file anchored on it.
Bisim invariance for MDL — same shape as BSML/BSMLOr/BSMLEmpty proofs in BSML/Bisimulation.lean and Studies/AloniAnttilaYang2024, but the modal-case argument differs because MDL's ◇ uses single- witness semantics rather than per-world.
Modal independence logic (Grädel and Väänänen's independence atoms) — sibling at Core/Logic/Modal/Independence.lean.

Syntax (Definition 1.1) #

Semantics (Definition 4.1) #

Lemma 4.2: Downward closure #

Empty team property #

Dep breaks union closure (the defining feature) #

Soundness for the closure cell (Definability bridge) #

Bisimulation invariance (Väänänen-style ◇) #

MDL's modality differs from BSML's: anti-◇ uses the union of accessibility images (clause (T9)), and ◇-support a single witness team (clause (T8)), rather than BSML's per-world sub-witnesses. The invariance proof therefore recurses through StateBisim.biUnionAccess and StateBisim.possWitness (the carrier-level Lemma 3.7 analogues in Core/Logic/Modal/Bisimulation.lean) at the modal step, where BSML uses StateBisim.accessImage / exists_image_subset. The dependence-atom case is depth-0 and turns on WorldBisim.val_eq: state bisim preserves the set of atom-valuation profiles realised in a team, and functional dependence is a property of that set.

Modal Dependence Logic (MDL) #