QBSML formula properties — Anttila 2021 Proposition 2.2.8 (substrate test)

@cite{aloni-vanormondt-2023} @cite{anttila-2021}

Substrate test: prove the three structural properties from Anttila 2021 Proposition 2.2.8 for QBSML's support relation, using the SAME Core.Logic.Team.flat_iff_downwardClosed_unionClosed_emptyTeam template that BSML uses (via Theories/Semantics/BSML/Properties.lean).

The substrate composes for first-order team semantics: the bilateral mutual induction pattern from BSML carries over directly, with additional cases for quantifiers exi and univ using State.extendUniversal_union_distrib, State.extendUniversal_subset_mono, State.extendFunctional_union_distrib, State.extendFunctional_subset_mono from Defs.lean.

Why one big joint induction (not two)

BSML splits the proof into separate joint inductions per property (unionClosed standalone, downwardClosed standalone, emptyTeam standalone). That works because BSML's unionClosed is unconditional — no operator in BSML needs downwardClosed of its subformula to establish union closure.

QBSML's exi (and dually antiSupport univ) is different. The union case of support exi x ψ constructs a witness h_st from the witnesses on s and t, leaving an (t \ s).extendFunctional x h_t term that has to be weakened to t.extendFunctional x h_t via State.extendFunctional_subset_mono plus downward closure of ψ. So the proof of UC needs DC of ψ as IH — which only works if both properties are proved in a single joint induction.

This narrows the result: QBSML's unionClosed requires NE-free (BSML's doesn't). The flat corollary still composes, since flat consumers use NE-free anyway.

Status

• emptyTeam_support_of_isNEFree: fully proved (joint bilateral induction over all 8 QBSMLFormula constructors).
• unionClosed_support_of_isNEFree, downwardClosed_support_of_isNEFree: fully proved via single 4-property joint bilateral induction.
• flat_support_of_isNEFree corollary: derives via Core.Logic.Team.flat_of_downwardClosed_unionClosed_emptyTeam.

theorem Semantics.QBSML.emptyTeam_support_of_isNEFree {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Pred : Type u_4} [DecidableEq W] [Fintype W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] {φ : QBSMLFormula Var Pred} (hNE : φ.isNEFree = true) : Core.Logic.Team.emptyTeam support φ

NE-free QBSML formulas are supported on the empty team.

theorem Semantics.QBSML.downwardClosed_support_of_isNEFree {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Pred : Type u_4} [DecidableEq W] [Fintype W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] {φ : QBSMLFormula Var Pred} (hNE : φ.isNEFree = true) : Core.Logic.Team.downwardClosed support φ

NE-free QBSML formulas are downward-closed (Anttila 2.2.8 part 1 extended to first-order).

theorem Semantics.QBSML.unionClosed_support_of_isNEFree {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Pred : Type u_4} [DecidableEq W] [Fintype W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] {φ : QBSMLFormula Var Pred} (hNE : φ.isNEFree = true) : Core.Logic.Team.unionClosed support φ

NE-free QBSML formulas are union-closed.

NB: Stronger than BSML's unionClosed_support requires no NE-free hypothesis, but QBSML's exi UC needs DC of ψ as IH (see file docstring), so we narrow to NE-free. The downstream flat corollary consumes NE-free anyway.

theorem Semantics.QBSML.flat_support_of_isNEFree {W : Type u_1} {Var : Type u_2} {Domain : Type u_3} {Pred : Type u_4} [DecidableEq W] [Fintype W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] {φ : QBSMLFormula Var Pred} (hNE : φ.isNEFree = true) : Core.Logic.Team.flat support φ

Anttila Proposition 2.2.16 (QBSML specialization): NE-free QBSML formulas are flat. Same call structure as BSML's flat_support_of_isNEFree — substrate validates.