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
Team.isFlat_iff template as
Logic/Team/BSML/Properties.lean.
Main declarations #
support_empty_of_neFree,isLowerSet_support_of_neFree,supClosed_support_of_neFree— the three closure properties.isFlat_support_of_neFree— flatness of the NE-free fragment ([Ant21] Proposition 2.2.16, QBSML specialisation).definableClass_support_neFree_subset— the NE-free fragment defines flat properties.Formula.toFormula?,support_iff_forall_realizeAt— the modal-free case of [AvO23] Proposition 4.1: support of a translatable formula is mathlibFormula.Realizeat every index.Formula.toModal?,support_iff_forall_realize— the full Proposition 4.1: the NE-free fragment (modals included) translates intoModalFormulaoverLogic/Modal/FirstOrder/Semantics.lean, and support is Kripke satisfaction at every index; the translation is total on exactly the NE-free fragment (exists_toModal?_of_neFree).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 #
The closure inductions are folds over the connective-level lemmas of
Team/Operations.lean and the quantifier clauses State.univ/State.exi
of QBSML/Defs.lean. BSML proves its closure properties in separate
inductions; QBSML cannot: union closure of the functional-extension clause
(State.supClosed_exi) needs downward closure of the subformula, so the
two properties 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.
Downward and union 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 #
NE-free QBSML formulas are flat, the QBSML case of [Ant21] Proposition 2.2.16.
It follows from [Ant21] Proposition 2.2.2
(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, since 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).
The De Morgan law ¬(φ ∨ ψ) ≡ ¬φ ∧ ¬ψ ([AvO23] Fact 1).
The De Morgan law ¬(φ ∧ ψ) ≡ ¬φ ∨ ¬ψ ([AvO23] Fact 1).
The modal duality ¬□φ ≡ ◇¬φ ([AvO23] Fact 1).
The modal duality ¬◇φ ≡ □¬φ ([AvO23] Fact 1).
The quantifier duality ¬∀xφ ≡ ∃x¬φ ([AvO23] Fact 1).
The 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 (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 #
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
(Logic/Team/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: Formula.toFormula?
translates the fragment into ((Language.monadic Pred)[[Const]]).Formula Var — quantifiers
via the computable named binders Formula.all₁ / Formula.ex₁ of
Core/ModelTheory/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.
- (QBSML.Formula.pred P x_1).toFormula? = some ((QBSML.predSymb P).formula₁ (FirstOrder.Language.var x_1))
- (QBSML.Formula.predc P c).toFormula? = some ((QBSML.predSymb P).formula₁ ((FirstOrder.Language.monadic Pred).con c).term)
- φ.neg.toFormula? = Option.map (fun (x : ((FirstOrder.Language.monadic Pred).withConstants Const).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.
A translatable formula is supported by a state iff it is classically satisfied at every index,
[AvO23] Proposition 4.1 for the modal-free fragment: 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: Formula.toModal?
translates the whole NE-free fragment — modals included — into
ModalFormula over the monadic signature
(Logic/Modal/FirstOrder/Semantics.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.diamond,
quantifiers become named binders; only NE returns none.
Equations
- One or more equations did not get rendered due to their size.
- (QBSML.Formula.pred P x_1).toModal? = some ((QBSML.predSymb P).modalFormula₁ (FirstOrder.Language.var x_1))
- (QBSML.Formula.predc P c).toModal? = some ((QBSML.predSymb P).modalFormula₁ ((FirstOrder.Language.monadic Pred).con c).term)
- QBSML.Formula.ne.toModal? = none
- φ.neg.toModal? = Option.map FirstOrder.Language.ModalFormula.not φ.toModal?
- φ.poss.toModal? = Option.map FirstOrder.Language.ModalFormula.diamond φ.toModal?
Instances For
Modally translatable formulas are NE-free.
The modal translation is total on the NE-free fragment: together with
neFree_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.