Modal dependence logic

Väänänen's modal dependence logic (MDL) extends classical modal logic with the dependence atom =(p₁, …, pₙ; q), supported by a team when the value of q is a function of the values of p₁, …, pₙ across the team. Like BSML it evaluates formulas bilaterally against teams of worlds of a Kripke model, and negation swaps support and anti-support. A team supports ◇φ when one team supporting φ supplies a successor to each of its worlds, and anti-supports it when the union of the successor sets anti-supports φ. MDL formulas are downward closed and supported by the empty team, but the dependence atom breaks union closure.

Main definitions

• Formula: atoms, dependence atoms, ¬, ∧, split ∨ and ◇.
• eval: bilateral evaluation, with support and antiSupport.
• Formula.modalDepth: the nesting depth of ◇.
• Formula.DepFree, Realize: the fragment without dependence atoms, and classical truth.

Main results

• isLowerSet_support, support_empty: support is downward closed and contains ∅.
• not_supClosed_dep_of_witness: the dependence atom is not union-closed.
• support_iff_forall_realize: without dependence atoms, support is pointwise classical truth.
• invariant_eval: k-bisimilar teams agree on every formula of modal depth at most k.

Implementation notes

eval is a fold over the operations of Team/Operations.lean and the dependence atom Team.dep, with Väänänen's single-witness and image modalities. The disjunction clause is the split t₁ ∪ t₂ = t, which is equivalent to Väänänen's t ⊆ t₁ ∪ t₂ under downward closure.

TODO

• The classical disjunction and the satisfiability complexity results of [LV13].
• Modal independence logic, with the independence atom beside Team.dep.

References

• [Vaa07] Väänänen, Dependence Logic: A New Approach to Independence Friendly Logic
• [Vaa08] Väänänen, Modal Dependence Logic
• [LV13] Lohmann and Vollmer, Complexity Results for Modal Dependence Logic
• [AAY24] Aloni, Anttila and Yang, State-based Modal Logics for Free Choice

Syntax (Definition 1.1)

inductive ModalLogic.Dependence.Formula (Atom : Type u_3) : Type u_3

The formulas of MDL ([Vaa08] Definition 1.1, p. 238) extend classical modal logic with the dependence atom =(p₁,...,pₙ; q). Väänänen defines □A as ¬◇¬A and A ∧ B as ¬(¬A ∨ ¬B); conj is primitive here, with the clauses that abbreviation yields.

• atom {Atom : Type u_3} (p : Atom) : Formula Atom

  Atomic proposition.

• dep {Atom : Type u_3} (xs : List Atom) (y : Atom) : Formula Atom

  The dependence atom =(x⃗; y) says that the values of y in the team are a function of the values of x⃗.

• neg {Atom : Type u_3} (φ : Formula Atom) : Formula Atom

  Negation, which swaps support and anti-support.

• conj {Atom : Type u_3} (φ ψ : Formula Atom) : Formula Atom

  Conjunction.

• disj {Atom : Type u_3} (φ ψ : Formula Atom) : Formula Atom

  Tensor disjunction (team-split form under downward closure).

• poss {Atom : Type u_3} (φ : Formula Atom) : Formula Atom

  Possibility modal ◇.

@[instance_reducible]

instance ModalLogic.Dependence.instReprFormula {Atom✝ : Type u_3} [Repr Atom✝] : Repr (Formula Atom✝)

Equations

• ModalLogic.Dependence.instReprFormula = { reprPrec := ModalLogic.Dependence.instReprFormula.repr }

def ModalLogic.Dependence.instReprFormula.repr {Atom✝ : Type u_3} [Repr Atom✝] : Formula Atom✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

Classical truth

Without dependence atoms MDL is classical modal logic ([Ant21]'s Proposition 2.2.16 for Väänänen's modalities, support_iff_forall_realize below).

def ModalLogic.Dependence.Formula.DepFree {Atom : Type u_2} : Formula Atom → Prop

Formula.DepFree φ holds when φ contains no dependence atom.

Equations

• (ModalLogic.Dependence.Formula.atom p).DepFree = True
• (ModalLogic.Dependence.Formula.dep xs y).DepFree = False
• φ.neg.DepFree = φ.DepFree
• φ.poss.DepFree = φ.DepFree
• (φ.conj ψ).DepFree = (φ.DepFree ∧ ψ.DepFree)
• (φ.disj ψ).DepFree = (φ.DepFree ∧ ψ.DepFree)

def ModalLogic.Dependence.Realize {W : Type u_1} {Atom : Type u_2} (M : KripkeModel W Atom) : Formula Atom → W → Prop

Classical Kripke truth of an MDL formula at a world, with ◇ the shared ModalLogic.Diamond; a dependence atom is true at every world.

Equations

• ModalLogic.Dependence.Realize M (ModalLogic.Dependence.Formula.atom p) x✝ = M.val p x✝
• ModalLogic.Dependence.Realize M (ModalLogic.Dependence.Formula.dep xs y) x✝ = True
• ModalLogic.Dependence.Realize M ψ.neg x✝ = ¬ModalLogic.Dependence.Realize M ψ x✝
• ModalLogic.Dependence.Realize M (ψ₁.conj ψ₂) x✝ = (ModalLogic.Dependence.Realize M ψ₁ x✝ ∧ ModalLogic.Dependence.Realize M ψ₂ x✝)
• ModalLogic.Dependence.Realize M (ψ₁.disj ψ₂) x✝ = (ModalLogic.Dependence.Realize M ψ₁ x✝ ∨ ModalLogic.Dependence.Realize M ψ₂ x✝)
• ModalLogic.Dependence.Realize M ψ.poss x✝ = ModalLogic.Diamond M.accessible (ModalLogic.Dependence.Realize M ψ) x✝

theorem ModalLogic.Dependence.realize_poss {W : Type u_1} {Atom : Type u_2} {M : KripkeModel W Atom} {ψ : Formula Atom} {w : W} : Realize M ψ.poss w ↔ ∃ v ∈ M.access w, Realize M ψ v

Semantics (Definition 4.1)

def ModalLogic.Dependence.eval {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) : Bool → Formula Atom → Finset W → Prop

Bilateral evaluation for MDL (Definition 4.1 of [Vaa08], p. 245). eval M true φ t is support (Player II); eval M false φ t is anti-support (Player I). Negation flips polarity (clause (T5)).

The ◇ clauses (T8), (T9) use Väänänen's single-witness form, not BSML's per-world form; the two formulations diverge for non-union- closed logics like MDL.

Equations

• ModalLogic.Dependence.eval M true (ModalLogic.Dependence.Formula.atom p) x✝ = (x✝ ∈ Team.flat (M.val p))
• ModalLogic.Dependence.eval M false (ModalLogic.Dependence.Formula.atom p) x✝ = (x✝ ∈ Team.flat fun (w : W) => ¬M.val p w)
• ModalLogic.Dependence.eval M true (ModalLogic.Dependence.Formula.dep xs y) x✝ = (x✝ ∈ Team.dep (fun (w : W) => List.map (fun (x : Atom) => M.val x w) xs) (M.val y))
• ModalLogic.Dependence.eval M false (ModalLogic.Dependence.Formula.dep xs y) x✝ = (x✝ ∈ {∅})
• ModalLogic.Dependence.eval M true ψ.neg x✝ = ModalLogic.Dependence.eval M false ψ x✝
• ModalLogic.Dependence.eval M false ψ.neg x✝ = ModalLogic.Dependence.eval M true ψ x✝
• ModalLogic.Dependence.eval M true (ψ₁.conj ψ₂) x✝ = (ModalLogic.Dependence.eval M true ψ₁ x✝ ∧ ModalLogic.Dependence.eval M true ψ₂ x✝)
• ModalLogic.Dependence.eval M false (ψ₁.conj ψ₂) x✝ = (x✝ ∈ Team.tensor {s : Finset W | ModalLogic.Dependence.eval M false ψ₁ s} {s : Finset W | ModalLogic.Dependence.eval M false ψ₂ s})
• ModalLogic.Dependence.eval M true (ψ₁.disj ψ₂) x✝ = (x✝ ∈ Team.tensor {s : Finset W | ModalLogic.Dependence.eval M true ψ₁ s} {s : Finset W | ModalLogic.Dependence.eval M true ψ₂ s})
• ModalLogic.Dependence.eval M false (ψ₁.disj ψ₂) x✝ = (ModalLogic.Dependence.eval M false ψ₁ x✝ ∧ ModalLogic.Dependence.eval M false ψ₂ x✝)
• ModalLogic.Dependence.eval M true ψ.poss x✝ = (x✝ ∈ Team.possWitness M.access {s : Finset W | ModalLogic.Dependence.eval M true ψ s})
• ModalLogic.Dependence.eval M false ψ.poss x✝ = (x✝ ∈ Team.necImage M.access {s : Finset W | ModalLogic.Dependence.eval M false ψ s})

@[reducible, inline]

abbrev ModalLogic.Dependence.support {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) : Prop

Support is evaluation in the positive polarity.

Equations

• ModalLogic.Dependence.support M φ t = ModalLogic.Dependence.eval M true φ t

@[reducible, inline]

abbrev ModalLogic.Dependence.antiSupport {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) : Prop

Anti-support is evaluation in the negative polarity.

Equations

• ModalLogic.Dependence.antiSupport M φ t = ModalLogic.Dependence.eval M false φ t

@[simp]

theorem ModalLogic.Dependence.support_atom {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (p : Atom) (t : Finset W) : support M (Formula.atom p) t ↔ ∀ w ∈ t, M.val p w

@[simp]

theorem ModalLogic.Dependence.antiSupport_atom {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (p : Atom) (t : Finset W) : antiSupport M (Formula.atom p) t ↔ ∀ w ∈ t, ¬M.val p w

@[simp]

theorem ModalLogic.Dependence.support_dep {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (xs : List Atom) (y : Atom) (t : Finset W) : support M (Formula.dep xs y) t ↔ ∀ w₁ ∈ t, ∀ w₂ ∈ t, (∀ x ∈ xs, M.val x w₁ ↔ M.val x w₂) → (M.val y w₁ ↔ M.val y w₂)

@[simp]

theorem ModalLogic.Dependence.antiSupport_dep {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (xs : List Atom) (y : Atom) (t : Finset W) : antiSupport M (Formula.dep xs y) t ↔ t = ∅

@[simp]

theorem ModalLogic.Dependence.support_neg {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) : support M φ.neg t ↔ antiSupport M φ t

@[simp]

theorem ModalLogic.Dependence.antiSupport_neg {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) : antiSupport M φ.neg t ↔ support M φ t

@[simp]

theorem ModalLogic.Dependence.support_conj {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (φ ψ : Formula Atom) (t : Finset W) : support M (φ.conj ψ) t ↔ support M φ t ∧ support M ψ t

@[simp]

theorem ModalLogic.Dependence.antiSupport_conj {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (φ ψ : Formula Atom) (t : Finset W) : antiSupport M (φ.conj ψ) t ↔ ∃ (t₁ : Finset W), antiSupport M φ t₁ ∧ ∃ (t₂ : Finset W), antiSupport M ψ t₂ ∧ t₁ ∪ t₂ = t

@[simp]

theorem ModalLogic.Dependence.support_disj {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (φ ψ : Formula Atom) (t : Finset W) : support M (φ.disj ψ) t ↔ ∃ (t₁ : Finset W), support M φ t₁ ∧ ∃ (t₂ : Finset W), support M ψ t₂ ∧ t₁ ∪ t₂ = t

@[simp]

theorem ModalLogic.Dependence.antiSupport_disj {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (φ ψ : Formula Atom) (t : Finset W) : antiSupport M (φ.disj ψ) t ↔ antiSupport M φ t ∧ antiSupport M ψ t

@[simp]

theorem ModalLogic.Dependence.support_poss {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) : support M φ.poss t ↔ ∃ (Y : Finset W), (∀ w ∈ t, ∃ y ∈ Y, y ∈ M.access w) ∧ support M φ Y

@[simp]

theorem ModalLogic.Dependence.antiSupport_poss {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (φ : Formula Atom) (t : Finset W) : antiSupport M φ.poss t ↔ antiSupport M φ (t.biUnion M.access)

Modal depth

def ModalLogic.Dependence.Formula.modalDepth {Atom : Type u_2} : Formula Atom → ℕ

The modal depth of a formula is the greatest number of nested ◇s in it.

Equations

• (ModalLogic.Dependence.Formula.atom p).modalDepth = 0
• (ModalLogic.Dependence.Formula.dep xs y).modalDepth = 0
• ψ.neg.modalDepth = ψ.modalDepth
• (ψ₁.conj ψ₂).modalDepth = max ψ₁.modalDepth ψ₂.modalDepth
• (ψ₁.disj ψ₂).modalDepth = max ψ₁.modalDepth ψ₂.modalDepth
• ψ.poss.modalDepth = ψ.modalDepth + 1

Lemma 4.2: Downward closure

theorem ModalLogic.Dependence.isLowerSet_support {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (φ : Formula Atom) : IsLowerSet {t : Finset W | support M φ t}

The support of every MDL formula is downward closed ([Vaa08] Lemma 4.2, p. 245).

Empty team property

theorem ModalLogic.Dependence.support_empty {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) (φ : Formula Atom) : support M φ ∅

Every MDL formula is supported on the empty team.

Dep breaks union closure (the defining feature)

theorem ModalLogic.Dependence.not_supClosed_dep_of_witness {W : Type u_1} {Atom : Type u_2} [DecidableEq W] {p q : Atom} {w₁ w₂ : W} {M : KripkeModel W Atom} (hp : M.val p w₁ ↔ M.val p w₂) (hq : ¬(M.val q w₁ ↔ M.val q w₂)) : ¬SupClosed {t : Finset W | support M (Formula.dep [p] q) t}

The dependence atom is not union-closed. When two worlds agree on p but not on q, each of their singleton teams supports =(p; q) but the team of both does not.

Soundness for the closure cell (Definability bridge)

theorem ModalLogic.Dependence.definableClass_support_subset {W : Type u_1} {Atom : Type u_2} [DecidableEq W] (M : KripkeModel W Atom) : Team.definableClass (support M) ⊆ {P : Team.TeamProperty W | IsLowerSet P ∧ ∅ ∈ P}

Every MDL-definable team property is downward closed and contains the empty team. The converse, that every such property is MDL-definable, is not proved here.

Bisimulation invariance

theorem ModalLogic.Dependence.invariant_eval {W : Type u_1} {Atom : Type u_2} [DecidableEq W] {W' : Type u_3} [DecidableEq W'] {M : KripkeModel W Atom} {M' : KripkeModel W' Atom} {k : ℕ} (φ : Formula Atom) (hd : φ.modalDepth ≤ k) (b : Bool) : Team.Invariant (fun (x1 : W) (x2 : W') => WorldBisim k M x1 M' x2) {t : Finset W | eval M b φ t} {t : Finset W' | eval M' b φ t}

Teams that are k-bisimilar agree on every MDL formula of modal depth at most k, in both polarities, by the argument of [AAY24] Theorem 3.8.

The classical fragment

On dep-free formulas support is pointwise classical truth and anti-support pointwise classical falsity: Väänänen's single-witness and image modalities agree with the flat ones on flat properties (Team.possWitness_flat, Team.necImage_flat).

theorem ModalLogic.Dependence.eval_iff_forall_realize {W : Type u_1} {Atom : Type u_2} [DecidableEq W] {M : KripkeModel W Atom} {φ : Formula Atom} (hD : φ.DepFree) (b : Bool) (t : Finset W) : eval M b φ t ↔ ∀ w ∈ t, Realize M φ w ↔ b = true

On dep-free formulas, support is pointwise classical truth and anti-support pointwise classical falsity.

theorem ModalLogic.Dependence.support_iff_forall_realize {W : Type u_1} {Atom : Type u_2} [DecidableEq W] {M : KripkeModel W Atom} {φ : Formula Atom} {t : Finset W} (hD : φ.DepFree) : support M φ t ↔ ∀ w ∈ t, Realize M φ w

theorem ModalLogic.Dependence.antiSupport_iff_forall_not_realize {W : Type u_1} {Atom : Type u_2} [DecidableEq W] {M : KripkeModel W Atom} {φ : Formula Atom} {t : Finset W} (hD : φ.DepFree) : antiSupport M φ t ↔ ∀ w ∈ t, ¬Realize M φ w

theorem ModalLogic.Dependence.support_singleton_iff_realize {W : Type u_1} {Atom : Type u_2} [DecidableEq W] {M : KripkeModel W Atom} {φ : Formula Atom} {w : W} (hD : φ.DepFree) : support M φ {w} ↔ Realize M φ w