Expressive completeness for BSML

Anttila, with Knudstorp, proves that BSML is expressively complete for the convex, union-closed, bounded-bisimulation-invariant team properties, a question Aloni, Anttila and Yang left open. In the vocabulary of Team/Definability.lean this is definableClass (support M) = {P | P.OrdConnected ∧ SupClosed P ∧ BisimClosed M P}. One inclusion collects the closure properties of support; the other is proved within one model over finitely many atoms, from the characteristic formulas of Characteristic.lean.

Main results

• bisimClosed_support: support is closed under bounded bisimulation.
• definableClass_support_subset, subset_definableClass_support: the two inclusions.
• definableClass_support_eq: their equality.

References

• [Alo22] Aloni, Logic and Conversation: The Case of Free Choice
• [AAY24] Aloni, Anttila and Yang, State-based Modal Logics for Free Choice
• [Ant25] Anttila, Not Nothing: Nonemptiness in Team Semantics
• [AK25b] Anttila and Knudstorp, Convex Team Logics

Bounded-bisimulation closure

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

The support of a formula is closed under bisimulation at its modal depth.

Expressive completeness

theorem BSML.definableClass_support_subset {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) : Team.definableClass (support M) ⊆ {P : Team.TeamProperty W | Set.OrdConnected P ∧ SupClosed P ∧ ModalLogic.BisimClosed M P}

Every BSML-definable team property is convex, union-closed and bounded-bisimulation-closed ([Ant25] §3.3.2).

theorem BSML.subset_definableClass_support {W : Type u_1} [DecidableEq W] {Atom : Type u_2} [Fintype W] [Fintype Atom] [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) : {P : Set (Finset W) | P.OrdConnected ∧ SupClosed P ∧ ModalLogic.BisimClosed M P} ⊆ Team.definableClass (support M)

Every convex, union-closed, bounded-bisimulation-closed team property is BSML-definable ([Ant25] Theorem 3.3.7 and the remark after it, p. 83, here within one model and over finitely many atoms).

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.definableClass_support_eq {W : Type u_1} [DecidableEq W] {Atom : Type u_2} [Fintype W] [Fintype Atom] [Inhabited Atom] (M : ModalLogic.KripkeModel W Atom) : Team.definableClass (support M) = {P : Set (Finset W) | P.OrdConnected ∧ SupClosed P ∧ ModalLogic.BisimClosed M P}

BSML is expressively complete for the convex, union-closed, bounded-bisimulation-closed team properties ([Ant25] Theorem 3.3.7 and the remark after it, p. 83, in within-model finite-atom form).