BSML formula properties — Anttila 2021 Proposition 2.2.8 + corollary

@cite{anttila-2021}

For BSML's support relation, this file proves the three constituent properties from Anttila 2021 Proposition 2.2.8 (specialized to a logic without ⨼ / global disjunction):

1. All BSML formulas have union closure (Anttila 2.2.8 part 2). BSML's connective set has no ⨼; the only source of union-closure failure is absent.

2. NE-free BSML formulas have the empty team property (Anttila 2.2.8 part 1). The only formula without the empty team property is NE itself.

3. NE-free BSML formulas are downward-closed (Anttila 2.2.8 part 1). NE is the only non-downward-closed primitive.

The corollary, via Core.Logic.Team.flat_of_downwardClosed_unionClosed_emptyTeam (our formalization of Anttila Proposition 2.2.2), is:

4. NE-free BSML formulas are flat (Anttila Proposition 2.2.16 / Fact 15 from @cite{aloni-2022}).

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 + the classical-evaluation bridge). This file's proof routes through the foundational decomposition; neFree_flat_eq provides the additional bridge to classical Kripke semantics.

Why both proofs?

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 its three properties separately and composing them via Core.Logic.Team.flat_iff_.... The Bridge.lean direct proof is BSML-specific (uses BSML's classicalEval).

Status

Property theorems currently SKETCHED (statements + proof structure). Full proofs require structural induction with careful handling of negation (bilateral mutual induction for the neg case). Tracked as in-flight; the flatness corollary is proved fully against the sketches.

theorem Semantics.BSML.unionClosed_support {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} (φ : BSMLFormula Atom) : Core.Logic.Team.unionClosed support φ

All BSML formulas are union-closed. BSML's connective set lacks the global disjunction ⨼ — Anttila Proposition 2.2.8 part 2 specializes to "all formulas" in this case.

theorem Semantics.BSML.emptyTeam_support_of_isNEFree {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} {φ : BSMLFormula Atom} (hNE : φ.isNEFree = true) : Core.Logic.Team.emptyTeam support φ

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

theorem Semantics.BSML.downwardClosed_support_of_isNEFree {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} {φ : BSMLFormula Atom} (hNE : φ.isNEFree = true) : Core.Logic.Team.downwardClosed support φ

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

theorem Semantics.BSML.flat_support_of_isNEFree {W : Type u_1} [DecidableEq W] [Fintype W] {Atom : Type u_2} {φ : BSMLFormula Atom} (hNE : φ.isNEFree = true) : Core.Logic.Team.flat support φ

Anttila Proposition 2.2.16 (BSML specialization of Fact 15 from @cite{aloni-2022}): NE-free BSML formulas are flat — team support equals pointwise support at each world in the team.

Derived as a corollary of the foundational flat_iff_downwardClosed_unionClosed_emptyTeam (Core.Logic.Team.Properties) applied to the three properties proved above.

The same conclusion is also proved directly with the classical-evaluation bridge in Bridge.lean as neFree_flat_eq.