QBSML formula properties #
The QBSML instances of the closure properties of [Ant21]
Proposition 2.2.8: NE-free formulas have downward-closed, sup-closed,
empty-team support, hence flat support, via the same
Core.Logic.Team.isFlat_iff template as
Core/Logic/Modal/BSML/Properties.lean.
Main declarations #
support_empty_of_isNEFree,isLowerSet_support_of_isNEFree,supClosed_support_of_isNEFree— the three closure properties.isFlat_support_of_isNEFree— flatness of the NE-free fragment ([Ant21] Proposition 2.2.16, QBSML specialisation).soundFor_flat_neFree— the NE-free fragment is sound for the flat cell ofTeam/Definability.lean.QBSMLFormula.toFormula?,support_iff_forall_realizeAt— the modal-free case of [AvO23] Proposition 4.1: support of a translatable formula is mathlibFormula.Realizeat every index.QBSMLFormula.toModal?,support_iff_forall_realize— the full Proposition 4.1: the NE-free fragment (modals included) translates intoModalFormulaoverCore/Logic/FirstOrder/Kripke.lean, and support is Kripke satisfaction at every index; the translation is total on exactly the NE-free fragment (exists_toModal?_of_isNEFree).eval_mapAtoms_iff— atom-substitution congruence: an atom map with bilaterally equivalent images is salva veritate.support_disj_inl,support_nec_iff,support_nec_mono,support_exi_of_update_closure— upward monotonicity of the NE-free fragment and existential introduction via witness reconstruction.
Implementation notes #
BSML proves the closure properties in separate inductions; QBSML cannot.
The union case of support for exi (dually, anti-support for univ)
weakens (t \ s).extendFunctional x h_t to t.extendFunctional x h_t via
State.extendFunctional_mono plus downward closure of the subformula, so
union closure and downward closure must live in one joint induction — and
union closure holds only on the NE-free fragment, whereas BSML's is
unconditional. The flatness corollary is unaffected: flat consumers use
NE-free anyway.
Empty-team property for NE-free formulas #
NE-free QBSML formulas are supported on the empty team.
Joint downward + sup closure for NE-free formulas #
NE-free QBSML formulas are downward-closed ([Ant21] Proposition 2.2.8 part 1, extended to first-order).
NE-free QBSML formulas have sup-closed support.
NB: BSML's supClosed_support needs no NE-free hypothesis, but
QBSML's exi UC case needs downward closure of the subformula as IH
(see the module docstring), so the QBSML version narrows to NE-free.
The downstream flat corollary consumes NE-free anyway.
Flatness corollary #
[Ant21] Proposition 2.2.16 (QBSML specialisation): NE-free
QBSML formulas are flat. Derived from [Ant21] Proposition 2.2.2
(Core.Logic.Team.isFlat_iff) applied to the three closure properties
above.
Soundness for the flat cell (Definability bridge) #
The NE-free fragment of QBSML is sound for the flat cell: every team
property definable by an NE-free QBSML formula is flat (downward-closed,
union-closed, empty-team). This restates [AvO23]'s
observation that NE-free QBSML reduces to classical first-order modal
logic, whose support is flat, in the Team/Definability.lean vocabulary.
The restriction to the NE-free fragment is essential, not incidental: NE
is the only source of non-classical behaviour, and union closure of exi
already needs downward closure of the subformula as IH (see the module
docstring), which NE breaks. So QBSML has no unconditional all-formula
cell — unlike BSML, whose NE-bearing formulas still land in the convex,
union-closed cell.
Fact 1: classical validities #
[AvO23] Fact 1 lists the classical equivalences QBSML
validates: double negation elimination, the De Morgan laws, and the □/◇
and ∀/∃ dualities. In the bilateral setup every one is definitional —
negation literally swaps support and antiSupport, whose clauses are
arranged in De Morgan pairs — so each is Iff.rfl.
Double negation elimination ([AvO23] Fact 1).
De Morgan: ¬(φ ∨ ψ) ≡ ¬φ ∧ ¬ψ ([AvO23] Fact 1).
De Morgan: ¬(φ ∧ ψ) ≡ ¬φ ∨ ¬ψ ([AvO23] Fact 1).
Modal duality: ¬□φ ≡ ◇¬φ ([AvO23] Fact 1).
Modal duality: ¬◇φ ≡ □¬φ ([AvO23] Fact 1).
Quantifier duality: ¬∀xφ ≡ ∃x¬φ ([AvO23] Fact 1).
Quantifier duality: ¬∃xφ ≡ ∀x¬φ ([AvO23] Fact 1).
Flatness as pointwise evaluation #
Flat (NE-free) support is pointwise: a team supports φ iff each of its
singletons does (Core.Logic.Team.IsFlat unfolded at the support set).
Anti-support of an NE-free formula is likewise pointwise: flatness of the bilateral negation.
Atom substitution salva veritate #
Atom-substitution congruence: an atom map whose images are
bilaterally equivalent to the atoms they replace is salva veritate —
φ.mapAtoms fp fc and φ are supported and anti-supported by exactly
the same states. Atom-rewriting operations (e.g. [Yan23]'s
reinterpretation function, Studies/Yan2023.lean) get truth-conditional
harmlessness for the price of their two atom lemmas.
Upward monotonicity of the NE-free fragment #
Disjunction introduction: α ⊨ α ∨ β for NE-free β (the right
disjunct is supported by the empty half of the split).
Support of the derived □ is pointwise support at the full accessible
lift — definitional, by the neg/poss clauses of eval.
□ is monotone: a state-wise entailment between prejacents lifts to
their necessitations.
Existential introduction via witness reconstruction #
A state t of x-updates of s (covering all of s) that supports
γ witnesses ∃x γ on s: the functional collecting, at each index,
the values whose updates land in t reconstructs t exactly
(State.extendFunctional_filter_of_update_mem). The shared
existential-witness step of the free-choice facts
(Core/Logic/Modal/QBSML/FreeChoice.lean).
Classicality: the modal-free Realize bridge #
[AvO23] Proposition 4.1 reduces the NE-free fragment to
classical quantified modal logic. The modal-free part of that reduction is
stated against mathlib first-order satisfaction: QBSMLFormula.toFormula?
translates the fragment into (monadicLang Const Pred).Formula Var — quantifiers
via the computable named binders Formula.all₁ / Formula.ex₁ of
Core/Logic/FirstOrder/Binders.lean — support at a singleton state is
Formula.Realize in the structure the model carries at that world
(support_singleton_iff_realizeAt), and flatness extends the bridge to
arbitrary states (support_iff_forall_realizeAt). Modals remain outside the
bridge: their right-hand side is classical modal logic, which mathlib's
ModelTheory does not carry.
Translate the modal-free fragment of QBSML into mathlib first-order
formulas over the monadic signature: quantifiers via the computable named
binders Formula.all₁ / Formula.ex₁ (none on NE and modal
formulas).
Equations
- One or more equations did not get rendered due to their size.
- (Core.Logic.Modal.QBSML.QBSMLFormula.pred P x_1).toFormula? = some ((Core.Logic.Modal.QBSML.monadicRel P).formula₁ (FirstOrder.Language.var x_1))
- (Core.Logic.Modal.QBSML.QBSMLFormula.predc P c).toFormula? = some ((Core.Logic.Modal.QBSML.monadicRel P).formula₁ (Core.Logic.Modal.QBSML.monadicConst c).term)
- φ.neg.toFormula? = Option.map (fun (x : (Core.Logic.Modal.QBSML.monadicLang Const Pred).Formula Var) => x.not) φ.toFormula?
- x✝.toFormula? = none
Instances For
Translatable formulas are NE-free.
[AvO23] Proposition 4.1, singleton case (modal-free fragment): support of a translatable formula at a singleton state is classical first-order satisfaction at that index's world, for any total valuation the index's partial assignment refines.
Anti-support of a translatable formula at a singleton state is the classical falsity of its translation.
[AvO23] Proposition 4.1 (modal-free fragment): a
translatable formula is supported by a state iff it is classically
satisfied at every index — M, s ⊨ φ(x̄) iff M, w ⊨_g φ(x̄) for all
⟨w, g⟩ ∈ s, with the right-hand side mathlib's Formula.Realize.
Classicality II: the full modal bridge #
The complete [AvO23] Proposition 4.1: QBSMLFormula.toModal?
translates the whole NE-free fragment — modals included — into
ModalFormula over the monadic signature
(Core/Logic/FirstOrder/Kripke.lean), and support is Kripke satisfaction at
every index. The translation is total on exactly the NE-free fragment.
Translate QBSML into modal formulas over the monadic signature: atoms
embed as classical formulas, ◇ becomes the derived ModalFormula.dia,
quantifiers become named binders; only NE returns none.
Equations
- One or more equations did not get rendered due to their size.
- Core.Logic.Modal.QBSML.QBSMLFormula.ne.toModal? = none
- φ.neg.toModal? = Option.map FirstOrder.Language.ModalFormula.not φ.toModal?
- φ.poss.toModal? = Option.map FirstOrder.Language.ModalFormula.dia φ.toModal?
Instances For
Modally translatable formulas are NE-free.
The modal translation is total on the NE-free fragment: together with
isNEFree_of_toModal?, the translatable and NE-free fragments
coincide.
[AvO23] Proposition 4.1, singleton case (full NE-free fragment): support of a modally translatable formula at a singleton state is Kripke satisfaction at that index's world.
Anti-support of a modally translatable formula at a singleton state is classical modal falsity.
[AvO23] Proposition 4.1 (full NE-free fragment):
an NE-free formula is supported by a state iff its modal translation is
classically satisfied at every index — M, s ⊨ φ(x̄) iff
M, w ⊨_g φ(x̄) for all ⟨w, g⟩ ∈ s, the right-hand side Kripke
satisfaction over mathlib structures.