Bisimulation for modal team logics

This file defines bounded-depth world bisimulation between pointed KripkeModels and its lift to teams, and proves the transport lemmas (image unions, team splits, witness teams) that each team-semantic logic's invariance theorem consumes at its modal and split cases. Nothing here mentions a formula type: each logic states its own bisim_invariant_eval against its own evaluation, recursing through these carrier lemmas.

Main declarations

• WorldBisim k M w M' w': bounded k-bisimulation between pointed worlds.
• StateBisim k M s M' s': its lift to teams, by back/forth partnership.
• StateBisim.biUnionAccess, StateBisim.splitPreserve, StateBisim.possWitness: the transport lemmas.

References

• [AAY24] — Definitions 3.1 and 3.6, Lemma 3.7
• [Vaa08] — modal dependence logic, the (T8)/(T9) modal clauses
• [Ant25] — nonemptiness in team semantics

World bisimulation

def ModalLogic.WorldBisim {W : Type u_1} {W' : Type u_2} {Atom : Type u_3} : ℕ → KripkeModel W Atom → W → KripkeModel W' Atom → W' → Prop

Bounded-depth bisimulation between pointed worlds across two KripkeModels (Definition 3.1 of [AAY24]). At depth 0, requires only that atoms match. At depth k+1, additionally requires the standard back/forth conditions on accessibility relating depth-k bisimilar successors.

Equations

• One or more equations did not get rendered due to their size.
• ModalLogic.WorldBisim 0 x✝³ x✝² x✝¹ x✝ = ∀ (p : Atom), x✝³.val p x✝² = x✝¹.val p x✝

theorem ModalLogic.WorldBisim.refl {W : Type u_1} {Atom : Type u_3} (k : ℕ) (M : KripkeModel W Atom) (w : W) : WorldBisim k M w M w

World bisimulation is reflexive at every depth.

theorem ModalLogic.WorldBisim.symm {W : Type u_1} {W' : Type u_2} {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {w : W} {M' : KripkeModel W' Atom} {w' : W'} : WorldBisim k M w M' w' → WorldBisim k M' w' M w

World bisimulation is symmetric (swap models).

theorem ModalLogic.WorldBisim.mono_succ {W : Type u_1} {W' : Type u_2} {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {w : W} {M' : KripkeModel W' Atom} {w' : W'} : WorldBisim (k + 1) M w M' w' → WorldBisim k M w M' w'

Bisimilarity at depth k+1 implies bisimilarity at depth k: higher depths are stricter.

theorem ModalLogic.WorldBisim.mono_le {W : Type u_1} {W' : Type u_2} {Atom : Type u_3} {m n : ℕ} (hmn : m ≤ n) {M : KripkeModel W Atom} {w : W} {M' : KripkeModel W' Atom} {w' : W'} : WorldBisim n M w M' w' → WorldBisim m M w M' w'

Bisimilarity is monotone in depth: m ≤ n → WorldBisim n → WorldBisim m.

State bisimulation

def ModalLogic.StateBisim {W : Type u_1} {W' : Type u_2} {Atom : Type u_3} (k : ℕ) (M : KripkeModel W Atom) (s : Finset W) (M' : KripkeModel W' Atom) (s' : Finset W') : Prop

State bisimulation (Definition 3.6 of [AAY24]): every world in s is k-bisimilar to some world in s', and every world in s' is k-bisimilar to some world in s. Lifts world bisimulation from points to teams.

Equations

• ModalLogic.StateBisim k M s M' s' = ((∀ w ∈ s, ∃ w' ∈ s', ModalLogic.WorldBisim k M w M' w') ∧ ∀ w' ∈ s', ∃ w ∈ s, ModalLogic.WorldBisim k M w M' w')

theorem ModalLogic.StateBisim.refl {W : Type u_1} {Atom : Type u_3} (k : ℕ) (M : KripkeModel W Atom) (s : Finset W) : StateBisim k M s M s

theorem ModalLogic.StateBisim.symm {W : Type u_1} {W' : Type u_2} {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {s : Finset W} {M' : KripkeModel W' Atom} {s' : Finset W'} : StateBisim k M s M' s' → StateBisim k M' s' M s

theorem ModalLogic.StateBisim.mono_succ {W : Type u_1} {W' : Type u_2} {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {s : Finset W} {M' : KripkeModel W' Atom} {s' : Finset W'} : StateBisim (k + 1) M s M' s' → StateBisim k M s M' s'

theorem ModalLogic.StateBisim.mono_le {W : Type u_1} {W' : Type u_2} {Atom : Type u_3} {m n : ℕ} (hmn : m ≤ n) {M : KripkeModel W Atom} {s : Finset W} {M' : KripkeModel W' Atom} {s' : Finset W'} : StateBisim n M s M' s' → StateBisim m M s M' s'

Helpers for the invariance theorems

theorem ModalLogic.WorldBisim.val_eq {W : Type u_1} {W' : Type u_2} {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {w : W} {M' : KripkeModel W' Atom} {w' : W'} (h : WorldBisim k M w M' w') (p : Atom) : M.val p w = M'.val p w'

World bisimilarity at any depth preserves atom valuations.

theorem ModalLogic.WorldBisim.accessStateBisim {W : Type u_1} {W' : Type u_2} {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {w : W} {M' : KripkeModel W' Atom} {w' : W'} (h : WorldBisim (k + 1) M w M' w') : StateBisim k M (M.access w) M' (M'.access w')

World bisim at depth k+1 yields state bisim of the accessibility images at depth k — the singleton form of Lemma 3.7(i).

theorem ModalLogic.StateBisim.nonempty_iff {W : Type u_1} {W' : Type u_2} {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {s : Finset W} {M' : KripkeModel W' Atom} {s' : Finset W'} (h : StateBisim k M s M' s') : s.Nonempty ↔ s'.Nonempty

State bisim preserves nonemptiness.

theorem ModalLogic.StateBisim.eq_empty_iff {W : Type u_1} {W' : Type u_2} {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {s : Finset W} {M' : KripkeModel W' Atom} {s' : Finset W'} (h : StateBisim k M s M' s') : s = ∅ ↔ s' = ∅

State bisim preserves emptiness.

theorem ModalLogic.StateBisim.exists_image_subset {W : Type u_1} {W' : Type u_2} {Atom : Type u_3} {k : ℕ} {M : KripkeModel W Atom} {s t : Finset W} {M' : KripkeModel W' Atom} {s' : Finset W'} (h : StateBisim k M s M' s') (hsub : t ⊆ s) : ∃ t' ⊆ s', (t.Nonempty → t'.Nonempty) ∧ StateBisim k M t M' t'

Given s ⇌_k s' and a sub-team t ⊆ s, there is a sub-team t' ⊆ s' with t ⇌_k t'; non-emptiness transfers.

Lemma 3.7: state bisimulation preserves modal step and team splits

theorem ModalLogic.StateBisim.biUnionAccess {W : Type u_1} {W' : Type u_2} {Atom : Type u_3} [DecidableEq W] [DecidableEq W'] {k : ℕ} {M : KripkeModel W Atom} {s : Finset W} {M' : KripkeModel W' Atom} {s' : Finset W'} (h : StateBisim (k + 1) M s M' s') : StateBisim k M (s.biUnion M.access) M' (s'.biUnion M'.access)

Lemma 3.7(i): state bisim at depth k+1 yields state bisim of the unions of accessibility images at depth k.

theorem ModalLogic.StateBisim.splitPreserve {W : Type u_1} {W' : Type u_2} {Atom : Type u_3} [DecidableEq W] [DecidableEq W'] {k : ℕ} {M : KripkeModel W Atom} {s t u : Finset W} {M' : KripkeModel W' Atom} {s' : Finset W'} (h : StateBisim k M s M' s') (hsplit : Team.splitsAs s t u) (htsub : t ⊆ s) (husub : u ⊆ s) : ∃ (t' : Finset W') (u' : Finset W'), Team.splitsAs s' t' u' ∧ StateBisim k M t M' t' ∧ StateBisim k M u M' u'

Lemma 3.7(ii): state bisim preserves binary team splits. Given s = t ∪ u and s ⇌_k s', there are t', u' with s' = t' ∪ u', t ⇌_k t', and u ⇌_k u'.

Single-witness modal step (Väänänen-style ◇)

theorem ModalLogic.StateBisim.possWitness {W : Type u_1} {W' : Type u_2} {Atom : Type u_3} [DecidableEq W] [DecidableEq W'] {k : ℕ} {M : KripkeModel W Atom} {s : Finset W} {M' : KripkeModel W' Atom} {s' : Finset W'} (h : StateBisim (k + 1) M s M' s') {Y : Finset W} (hYsub : Y ⊆ s.biUnion M.access) (hwit : ∀ w ∈ s, ∃ y ∈ Y, y ∈ M.access w) : ∃ Y' ⊆ s'.biUnion M'.access, (∀ w' ∈ s', ∃ y' ∈ Y', y' ∈ M'.access w') ∧ StateBisim k M Y M' Y'

Single-witness team transport: given s ⇌_{k+1} s' and a witness team Y inside the image union that every world in s reaches, there is a Y' that every world in s' reaches, with Y ⇌_k Y' — the Lemma 3.7 analogue for the single-witness ◇-support clause.