Documentation

Linglib.Logic.Team.BSML.Properties

Closure properties of BSML support #

The teams supporting a BSML formula form a union-closed and order-convex family; when the formula is NE-free they also include the empty team and are closed downward, so they are determined by the singleton teams. Support and anti-support are moreover invariant under bounded bisimulation. Anttila proves the closure properties, and Aloni, Anttila and Yang the invariance. These are the properties for which BSML is expressively complete (BSML/ExpressiveCompleteness.lean).

Main results #

Implementation notes #

Negation swaps support and anti-support, so each property is proved for both polarities at once by induction on the formula; each case is the lemma of its connective in Team/Operations.lean or Team/Bisimulation.lean. Aloni, Anttila and Yang prove bisimulation invariance for support of formulas in negation normal form; the joint induction needs no normal form.

References #

Closure properties by induction over the connectives #

Each case is the closure lemma of its connective from Team/Operations.lean, and negation swaps the two polarities.

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

BSML support is sup-closed ([Ant21] Proposition 2.2.8, second part). BSML's connective set lacks the global disjunction ⨼, so the union-closure obstruction is absent and all formulas satisfy the property.

source
theorem BSML.support_empty_of_neFree {W : Type u_1} [DecidableEq W] {Atom : Type u_2} {φ : Formula Atom} (hNE : φ.NEFree) (M : ModalLogic.KripkeModel W Atom) :
support M φ ∅

NE-free BSML formulas are supported on the empty team. The only obstruction is NE itself, which fails on ∅ by definition.

source
theorem BSML.isLowerSet_support_of_neFree {W : Type u_1} [DecidableEq W] {Atom : Type u_2} {φ : Formula Atom} (hNE : φ.NEFree) (M : ModalLogic.KripkeModel W Atom) :
IsLowerSet {t : Finset W | support M φ t}

An NE-free BSML formula is downward closed, so its support survives passing to a subteam.

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

BSML support is order-convex for every formula, NE included ([Ant25] Proposition 3.3.6 and the remark after Theorem 3.3.7, pp. 82–83), so a team between two supporting teams supports the formula too. With supClosed_support, this is the property for which BSML is expressively complete.

Flatness corollary (Anttila 2.2.16) #

source
theorem BSML.isFlat_support_of_neFree {W : Type u_1} [DecidableEq W] {Atom : Type u_2} {φ : Formula Atom} (hNE : φ.NEFree) (M : ModalLogic.KripkeModel W Atom) :
Team.IsFlat {t : Finset W | support M φ t}

An NE-free BSML formula is flat ([Ant21] Proposition 2.2.16), by Anttila's Proposition 2.2.2 applied to the three closure properties above.

Bisimulation invariance #

source
theorem BSML.invariant_eval {W : Type u_1} [DecidableEq W] {Atom : Type u_2} {W' : Type u_3} [DecidableEq W'] {M : ModalLogic.KripkeModel W Atom} {M' : ModalLogic.KripkeModel W' Atom} {k : ℕ} (φ : Formula Atom) (hd : φ.modalDepth ≤ k) (b : Bool) :
Team.Invariant (fun (x1 : W) (x2 : W') => ModalLogic.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 formula of modal depth at most k, in both polarities ([AAY24] Theorem 3.8).

Soundness for the closure cell (Definability bridge) #

source
theorem BSML.definableClass_support_neFree_subset {W : Type u_1} [DecidableEq W] {Atom : Type u_2} (M : ModalLogic.KripkeModel W Atom) :
(Team.definableClass fun (φ : { φ : Formula Atom // φ.NEFree }) => support M ↑φ) ⊆ {P : Team.TeamProperty W | Team.IsFlat P}

The NE-free fragment of BSML defines flat properties ([Ant21] Proposition 2.2.16), the fragment being the subtype of NE-free formulas. NE is exactly what moves a formula off the flat properties into the convex, union-closed ones (definableClass_support_subset in BSML/ExpressiveCompleteness.lean).