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 hard converse: every property in the cell is BSML-definable. Stated here as expressiveCompleteness_converse with a sorry; it is the within-model specialisation of [Ant25] Ch 3 and requires the characteristic-formula machinery (see the TODO there).

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 open converse (sorry).
• expressivelyComplete — the headline equality (inherits the converse sorry).

Bounded-bisimulation closure (the third soundness pillar)

def Core.Logic.Modal.BSML.BisimClosed {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel 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

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

def Core.Logic.Modal.BSML.bisimClosedProperties {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) : Set (Team.TeamProperty W)

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

Equations

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

theorem Core.Logic.Modal.BSML.bisimInvariant_support {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ : BSMLFormula Atom) {k : ℕ} (hd : φ.modalDepth ≤ k) {s s' : Finset W} (h : 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 Core.Logic.Modal.BSML.bisimClosed_definedBy {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ : BSMLFormula 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 Core.Logic.Modal.BSML.expressiveSoundness {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel 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 Core.Logic.Modal.BSML.expressiveCompleteness_converse {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel 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] and solved via Knudstorp's convexity machinery): every convex, union-closed, bounded-bisimulation-closed team property is BSML-definable.

TODO: prove via characteristic formulas. The prerequisite is the Hennessy-Milner direction (Theorem 3.3, deferred in BSML/Bisimulation.lean): for [Fintype Atom], build NE-free Hintikka formulas χ_w^k satisfying {v} ⊨ χ_w^k ↔ WorldBisim k M w M v, lift them to characteristic formulas for teams, then assemble P as a split disjunction over the inclusion-minimal teams of P of their characteristic formulas conjoined with NE (the convex + union-closed normal form — the converse of Proposition 3.3.1). This is the within-model specialisation of Anttila's cross-model theorem.

theorem Core.Logic.Modal.BSML.expressivelyComplete {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel 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). Inherits the sorry of expressiveCompleteness_converse.