BSML formula closure properties (Anttila 2021 Proposition 2.2.8)

[Ant21] [Alo22]

For BSML's support relation, this file proves the three constituent properties from Anttila 2021 Proposition 2.2.8 (specialised to a logic without global disjunction ⨼) plus the flatness corollary from Anttila 2.2.16 / [Alo22] Fact 15.

Main declarations

• supClosed_support — every BSML formula has sup-closed support (Anttila 2.2.8 part 2; BSML's connective set has no ⨼, so the union-closure obstruction is absent).
• support_empty_of_isNEFree — NE-free BSML formulas are supported on the empty team (Anttila 2.2.8 part 1).
• isLowerSet_support_of_isNEFree — NE-free BSML formulas are downward-closed (Anttila 2.2.8 part 1).
• isFlat_support_of_isNEFree — NE-free BSML formulas are flat (Anttila 2.2.16 / [Alo22] Fact 15), derived via Anttila Proposition 2.2.2 from the three properties above.

Implementation notes

The negation case needs bilateral mutual induction (support of ¬φ is anti-support of φ), so each property is proved as a joint statement over support + anti-support via a private helper, then the public form projects the support component.

A direct flatness proof is also available in Bridge.lean as neFree_flat_eq, which proves the stronger statement support t ↔ ∀ w ∈ t, classicalEval w (flatness + classical-evaluation bridge). This file's proof routes through the foundational decomposition; neFree_flat_eq provides the additional bridge to classical Kripke semantics.

The decomposition through Anttila 2.2.8 + 2.2.2 is reusable: any future team-semantic logic in linglib (QBSML, inquisitive, dependence logic) needs the same structural argument — proving the three closure properties separately and composing them via Core.Logic.Team.isFlat_iff.

Sup-closure (Anttila 2.2.8 part 2)

theorem Core.Logic.Modal.BSML.supClosed_support {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ : BSMLFormula Atom) : SupClosed {t : Finset W | support M φ t}

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

Empty-team property for NE-free formulas (Anttila 2.2.8 part 1)

theorem Core.Logic.Modal.BSML.support_empty_of_isNEFree {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} {φ : BSMLFormula Atom} (hNE : φ.isNEFree = true) (M : BSMLModel 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.

Downward closure for NE-free formulas (Anttila 2.2.8 part 1)

theorem Core.Logic.Modal.BSML.isLowerSet_support_of_isNEFree {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} {φ : BSMLFormula Atom} (hNE : φ.isNEFree = true) (M : BSMLModel W Atom) : IsLowerSet {t : Finset W | support M φ t}

NE-free BSML formulas are downward-closed: support survives under taking subsets of the team.

Convexity for all formulas (Anttila 2025, Proposition 3.3.1)

theorem Core.Logic.Modal.BSML.ordConnected_support {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) (φ : BSMLFormula Atom) : {t : Finset W | support M φ t}.OrdConnected

BSML support is order-convex for every formula — NE-bearing included ([Ant25] Proposition 3.3.1): { t | support M φ t } is Set.OrdConnected, i.e. s ⊆ t ⊆ u with support M φ s and support M φ u forces support M φ t.

Generalizes isLowerSet_support_of_isNEFree: for NE-free φ the empty-team property holds, and Core.Logic.Team.isLowerSet_iff_ordConnected_of_empty recovers downward closure from convexity. Together with supClosed_support, this is the convex-and-union-closed property for which BSML is expressively complete ([Ant25]).

Flatness corollary (Anttila 2.2.16)

theorem Core.Logic.Modal.BSML.isFlat_support_of_isNEFree {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} {φ : BSMLFormula Atom} (hNE : φ.isNEFree = true) (M : BSMLModel W Atom) : Team.IsFlat {t : Finset W | support M φ t}

Anttila Proposition 2.2.16 (BSML specialisation of Fact 15 from [Alo22]): NE-free BSML formulas are flat — team support equals pointwise support at each world in the team.

Derived from Anttila 2.2.2 (Core.Logic.Team.isFlat_iff) applied to the three closure properties proved above. The same conclusion has a direct classical-evaluation-bridge proof in Bridge.lean as neFree_flat_eq.

Soundness for the closure cell (Definability bridge)

theorem Core.Logic.Modal.BSML.soundFor_convex_inter_unionClosed {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) : Team.SoundFor (support M) (Team.convexProperties ∩ Team.unionClosedProperties)

BSML is sound for its closure cell: every BSML-definable team property is convex and union-closed — the soundness half of BSML's expressive completeness ([Ant25] Proposition 3.3.1: BSML is complete for the convex, union-closed modal properties, modulo bounded bisimulation).

Composes ordConnected_support and supClosed_support through the Team/Definability.lean bridge. The converse (every such property is BSML-definable) is the open half.

theorem Core.Logic.Modal.BSML.soundFor_flat_neFree {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (M : BSMLModel W Atom) : (Team.definableClassWhere (support M) fun (φ : BSMLFormula Atom) => φ.isNEFree = true) ⊆ Team.flatProperties

The NE-free fragment of BSML is sound for the flat cell (Anttila Proposition 2.2.16 / [Alo22] Fact 15): NE-free BSML formulas define flat properties. Companion to soundFor_convex_inter_unionClosed: NE is exactly what moves a formula off the flat cell into the strictly larger convex, union-closed cell.