Documentation

Linglib.Logic.Team.QBSML.Enrichment

Pragmatic enrichment in QBSML #

This file defines the pragmatic enrichment [·]⁺ of a QBSML formula and proves that it strengthens NE-free formulas in both polarities. Enrichment conjoins the non-emptiness atom NE to every subformula, quantifiers included, so a state supports an enriched formula only when each subformula is witnessed by a non-empty state. Aloni and van Ormondt extend Aloni's propositional enrichment to the first-order language and derive from it the ignorance, distribution and free-choice facts proved in Logic/Team/QBSML/FreeChoice.lean.

Main definitions #

Main results #

Implementation notes #

The paper defines [·]⁺ on the NE-free fragment only; enrich is total and sends NE to itself. □ is the derived ¬◇¬, so the paper's clause [□φ]⁺ = □[φ]⁺ ∧ NE has no counterpart. support_enrich_nec_iff shows that the derived enrichment has the same support as that clause; their anti-supports differ on the empty state, which anti-supports the paper's form but not the derived one. The file parallels Logic/Team/BSML/Enrichment.lean over the first-order formula type.

References #

Enrichment #

source
def QBSML.Formula.enrich {Var : Type u_1} {Const : Type u_2} {Pred : Type u_3} :
Formula Var Const Pred → Formula Var Const Pred

The pragmatic enrichment [φ]⁺ conjoins NE to every subformula of φ.

Equations
Instances For
    source
    theorem QBSML.nonempty_of_support_enrich {Var : Type u_1} {Const : Type u_2} {Pred : Type u_3} {W : Type u_4} {Domain : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] {M : Model W Domain Const Pred} {φ : Formula Var Const Pred} {s : Finset (Index W Var Domain)} (h : support M φ.enrich s) :
    s.Nonempty

    A state supporting an enriched formula is non-empty.

    source
    theorem QBSML.antiSupport_conj_ne {Var : Type u_1} {Const : Type u_2} {Pred : Type u_3} {W : Type u_4} {Domain : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : Model W Domain Const Pred) (φ : Formula Var Const Pred) (s : Finset (Index W Var Domain)) :
    antiSupport M (φ.conj Formula.ne) s ↔ antiSupport M φ s

    Only the empty state anti-supports NE, so anti-support of φ ∧ NE reduces to anti-support of φ.

    Enrichment strengthens #

    source
    theorem QBSML.eval_of_eval_enrich {Var : Type u_1} {Const : Type u_2} {Pred : Type u_3} {W : Type u_4} {Domain : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] {M : Model W Domain Const Pred} {φ : Formula Var Const Pred} {s : Finset (Index W Var Domain)} {pol : Bool} (hNE : φ.NEFree) (h : eval M pol φ.enrich s) :
    eval M pol φ s

    Enrichment strengthens an NE-free formula in both polarities, the first-order form of Aloni's Fact 1.

    source
    theorem QBSML.support_of_support_enrich {Var : Type u_1} {Const : Type u_2} {Pred : Type u_3} {W : Type u_4} {Domain : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] {M : Model W Domain Const Pred} {φ : Formula Var Const Pred} {s : Finset (Index W Var Domain)} (hNE : φ.NEFree) (h : support M φ.enrich s) :
    support M φ s

    [α]⁺ ⊨ α for NE-free α.

    source
    theorem QBSML.antiSupport_of_antiSupport_enrich {Var : Type u_1} {Const : Type u_2} {Pred : Type u_3} {W : Type u_4} {Domain : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] {M : Model W Domain Const Pred} {φ : Formula Var Const Pred} {s : Finset (Index W Var Domain)} (hNE : φ.NEFree) (h : antiSupport M φ.enrich s) :
    antiSupport M φ s

    [α]⁺ ⫤ α for NE-free α, the anti-support half of eval_of_eval_enrich.

    The enriched derived □ #

    source
    theorem QBSML.support_enrich_nec_iff {Var : Type u_1} {Const : Type u_2} {Pred : Type u_3} {W : Type u_4} {Domain : Type u_5} [DecidableEq W] [DecidableEq Var] [Fintype Var] [DecidableEq Domain] [Fintype Domain] (M : Model W Domain Const Pred) (φ : Formula Var Const Pred) (s : Finset (Index W Var Domain)) :
    support M φ.nec.enrich s ↔ (∀ i ∈ s, support M φ.enrich (State.modalLift (M.access i.world) i.assign)) ∧ s.Nonempty

    Support of the enriched derived □φ is enriched support of φ at every index's full accessible lift R(wᵢ)[gᵢ], on a non-empty state.