Expressive completeness for BSML

[Ant25] [AAY24] [Alo22]

[Ant25] Chapter 3 (= [AK25b]) proves that BSML is expressively complete for the class of convex, union-closed, bounded-bisimulation-invariant modal team properties — solving the BSML expressive-power problem left open in [AAY24]. In the Team/Definability.lean vocabulary this is ExpressivelyCompleteFor (support M) for the cell convexProperties ∩ unionClosedProperties ∩ bisimClosedProperties M.

The theorem splits into two halves:

• Soundness (⟦BSML⟧ ⊆ cell) — every definable property lies in the cell. Fully proved here, assembling the three closure pillars: ordConnected_support (convexity, Proposition 3.3.1), supClosed_support (union closure), and bisimClosed_definedBy (Theorem 3.8 / bisimulation invariance, BSML/Bisimulation.lean).
• Completeness (cell ⊆ ⟦BSML⟧) — the converse: every property in the cell is BSML-definable, proved for finite atom types via the characteristic-formula machinery of BSML/Characteristic.lean (the within-model, finite-atom specialisation of [Ant25] Ch 3, whose cross-model theorem indexes bisimulation by finite atom sets).

Main declarations

• BisimClosed M P, bisimClosedProperties M — bounded-bisimulation closure of a team property within M (the third soundness pillar as a closure cell).
• bisimInvariant_support — Theorem 3.8 specialised to one model.
• bisimClosed_definedBy — every BSML-definable property is bisim-closed.
• expressiveSoundness — ⟦BSML⟧ ⊆ the convex/union-closed/bisim-closed cell.
• expressiveCompleteness_converse — the converse.
• expressivelyComplete — the headline equality.

Bounded-bisimulation closure (the third soundness pillar)

def BSML.BisimClosed {W : Type u_1} {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) (P : Team.TeamProperty W) : Prop

A team property is bounded-bisimulation-closed in M if for some depth k it is closed under k-bisimulation of teams within M. This is the closure invariant — alongside convexity and union closure — that characterises BSML-definability ([Ant25] Ch 3).

Equations

• BSML.BisimClosed M P = ∃ (k : ℕ), ∀ (s s' : Finset W), ModalLogic.StateBisim k M s M s' → (s ∈ P ↔ s' ∈ P)

def BSML.bisimClosedProperties {W : Type u_1} {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) : Set (Team.TeamProperty W)

The class of bounded-bisimulation-closed team properties of M.

Equations

• BSML.bisimClosedProperties M = {P : Team.TeamProperty W | BSML.BisimClosed M P}

theorem BSML.bisimInvariant_support {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) {k : ℕ} (hd : φ.modalDepth ≤ k) {s s' : Finset W} (h : ModalLogic.StateBisim k M s M s') : support M φ s ↔ support M φ s'

BSML support is bounded-bisimulation invariant within a model: if s ⇌_k s' and k ≥ φ.modalDepth, then s and s' agree on φ. Immediate from Theorem 3.8 (bisim_invariant_eval) at M' := M.

theorem BSML.bisimClosed_definedBy {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) (φ : Formula Atom) : BisimClosed M (Team.definedBy (support M) φ)

Every BSML-definable team property is bounded-bisimulation-closed, with witnessing depth the formula's modal depth.

Expressive completeness

theorem BSML.expressiveSoundness {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) : Team.definableClass (support M) ⊆ Team.convexProperties ∩ Team.unionClosedProperties ∩ bisimClosedProperties M

Soundness half ([Ant25] Ch 3): every BSML-definable team property is convex, union-closed, and bounded-bisimulation-closed. Assembles ordConnected_support, supClosed_support, and bisimClosed_definedBy.

theorem BSML.expressiveCompleteness_converse {W : Type u_1} [DecidableEq W] {Atom : Type u_2} [Fintype W] [Fintype Atom] [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) : Team.convexProperties ∩ Team.unionClosedProperties ∩ bisimClosedProperties M ⊆ Team.definableClass (support M)

Completeness half ([Ant25] Ch 3 — the hard direction, the BSML expressive-power problem left open by [AAY24] — in its within-model, finite-atom form): every convex, union-closed, bounded-bisimulation-closed team property is BSML-definable.

The defining formula conjoins an upper bound — the flat disjunction δ_U of the characteristic formulas of the union U of all teams of P — with, for every set T of worlds whose bisimilarity classes meet every team of P, the hitting disjunct (δ_T ∧ NE) ∨ δ_U. A supporting team t lies under U and meets every such transversal; the worlds not bisimilar into t therefore fail to be a transversal, which yields a team s₀ ∈ P whose classes t covers, and s₀ ∪ (U restricted to t's classes) lies in P by convexity between s₀ and U and is bisimilar to t — so t ∈ P by bisimulation closure.

theorem BSML.expressivelyComplete {W : Type u_1} [DecidableEq W] {Atom : Type u_2} [Fintype W] [Fintype Atom] [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) : Team.ExpressivelyCompleteFor (support M) (Team.convexProperties ∩ Team.unionClosedProperties ∩ bisimClosedProperties M)

BSML is expressively complete for the convex, union-closed, bounded-bisimulation-closed team properties ([Ant25] Ch 3, in within-model finite-atom form).