[AvO23]: QBSML applied to modified numerals + split disjunction #
Aloni & van Ormondt 2023 introduces QBSML, the first-order extension of
Aloni 2022's BSML, and applies it to a battery of inferences arising from
modified numerals analysed as disjunctions:
at least n φ ↦ n ∨ more, at most n φ ↦ n ∨ less.
The framework's central facts (paper §5):
| Fact | Statement |
|---|---|
| 3 | [Pa ∨ Pb]⁺ ⊨_epi ◇Pa ∧ ◇Pb (ignorance, R state-based) |
| 4 | [∀xPx ∨ Qx]⁺ ⊭ ∀x(◇Px ∧ ◇Qx) (obviation; counterexample on paper Fig. 14) |
| 5 | card(s)=1 ⇒ M, s ⊨ [∀x(Px ∨ Qx)]⁺ ⇒ M, s ⊨ ∃xPx ∧ ∃xQx (distribution under full information) |
| 6 | [∀x(Px ∨ Qx)]⁺ ⊨_epi ∃x◇Px ∧ ∃x◇Qx (distribution° on epistemic models) |
| 7 | [□(Pa ∨ Pb)]⁺ ⊨ ◇Pa ∧ ◇Pb (□-free choice) |
| 8 | [◇(Pa ∨ Pb)]⁺ ⊨ ◇Pa ∧ ◇Pb (◇-free choice; ≡ Aloni 2022 NS FC at first-order) |
| 9 | [∀x◇(Px ∨ Qx)]⁺ ⊨ ∀x◇Px ∧ ∀x◇Qx (universal FC; [Che09b]) |
| 10 | [¬(Pa ∨ Pb)]⁺ ⊨ ¬Pa ∧ ¬Pb (negation behaviour; ignorance disappears) |
Facts 3 and 5–10 are universal substrate theorems in
Core/Logic/Modal/QBSML/FreeChoice.lean (framework substrate with multiple
paper-anchored consumers — this file and Studies/Yan2023.lean); this file
instantiates the unconditional ones at a concrete model (avoModel).
Fact 4 is the paper's Fig. 14 countermodel, proved here. Facts 1–2 and
Proposition 4.1 live in Core/Logic/Modal/QBSML/{Enrichment,Properties}.lean
(the modal-free Proposition 4.1 against mathlib Formula.Realize is
instantiated here at avoModel, the translation discharged by rfl).
Fact 3 needs the individual constants of [AvO23]
Definition 4.1 — QBSMLFormula.predc atoms, interpreted world-relatively
via QBSMLModel.cInterp.
What is deferred #
Decidableinstance forQBSML.eval: well-defined, but of limited use — the split-disjunction clauses quantify over pairs of subteams of the index space (2^12 × 2^12already at this file's model sizes), so kerneldecideis infeasible for the interesting claims; the Fact 4 countermodel is therefore proved by hand.
Atoms and worlds #
The concrete model reuses Core.Logic.Modal.BSML.{FCAtom, PowerSet2World}
from the existing FreeChoice substrate, ensuring AvO 2023 + Aloni 2022 both
target the same world space.
Predicates and variables #
Two unary predicates P and Q: provides the non-degenerate disjunction
Pa ∨ Qa matching the paper's Pa ∨ Pb schema (where the a, b are
domain elements rather than predicate-instances). With monadic predicates
over a 2-element domain, Pa ∨ Qa and Pa ∨ Pb are equally non-trivial
instantiations of split disjunction.
Instances For
Equations
- AloniVanOrmondt2023.instDecidableEqQPred x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- AloniVanOrmondt2023.instReprQPred = { reprPrec := AloniVanOrmondt2023.instReprQPred.repr }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- AloniVanOrmondt2023.instFintypeQPred = { elems := {AloniVanOrmondt2023.QPred.P, AloniVanOrmondt2023.QPred.Q}, complete := AloniVanOrmondt2023.instFintypeQPred._proof_1 }
The concrete model #
Universal-access deontic-style model on PowerSet2World.
The interpretation is the monadicStructure of the valuation
V w P d := w.holds d: both predicates hold of d at w iff w
models the atom d. The disjunction Px ∨ Qx is non-degenerate at the
formula level even though at this model the two interpretations
coincide. A model with divergent P and Q extensions would discriminate
further; this minimal model suffices for the substrate-instantiation
tests below.
Universal access (access _ = univ) means R is indisputable on every
state but not state-based — same shape as Aloni2022.deonticModel.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Formulas #
Disjunction Px ∨ Qx — paper's Pa ∨ Pb-shape with two distinct
predicate-instances.
Instances For
The negation premise ¬(Px ∨ Qx) corresponding to the paper's
¬(Pa ∨ Pb) schema.
Instances For
The narrow-scope FC premise ◇(Px ∨ Qx) corresponding to the paper's
◇(Pa ∨ Pb) schema.
Instances For
The □-FC premise □(Px ∨ Qx) (paper's Fact 7 schema; □ derived).
Instances For
The universal-FC premise ∀x◇(Px ∨ Qx) (paper's Fact 9 schema).
Equations
Instances For
The distribution premise ∀x(Px ∨ Qx) (paper's Facts 4–6 schema).
Equations
Instances For
Fact 10 (negation): [¬(Pa ∨ Pb)]⁺ ⊨ ¬Pa ∧ ¬Pb #
Fact 10 (Negation behaviour) at avoModel:
Enriched negation [¬(Px ∨ Qx)]⁺ entails the conjunction of negated
disjuncts ¬Px ∧ ¬Qx. One-line invocation of the substrate's
negationStrip_Q (Core/Logic/Modal/QBSML/FreeChoice.lean).
Mirrors Aloni2022.aloni2022_fact11_dual_prohibition style — substrate
theorem, model + NE-free witnesses applied.
Facts 7 and 8 (free choice): [□/◇(Pa ∨ Pb)]⁺ ⊨ ◇Pa ∧ ◇Pb #
Fact 8 (Narrow-Scope free choice / ◇-FC) at avoModel:
Enriched possibility-disjunction [◇(Px ∨ Qx)]⁺ entails ◇Px ∧ ◇Qx.
One-line invocation of narrowScopeFC_Q. The first-order analogue of
Aloni2022.aloni2022_fact4_NS_FC — same template, lifted to QBSML's
monadic predicate language.
Fact 7 (□-free choice) at avoModel: [□(Px ∨ Qx)]⁺ entails
◇Px ∧ ◇Qx, with the derived □. One-line invocation of boxFC_Q.
Facts 9 and 5 (universal FC and distribution) #
Fact 9 (Universal free choice) at avoModel:
[∀x◇(Px ∨ Qx)]⁺ entails ∀x◇Px ∧ ∀x◇Qx. One-line invocation of
universalFC_Q — the [Che09b]-attested pattern.
Fact 5 (Distribution at maximal information) at avoModel: on any
singleton state, [∀x(Px ∨ Qx)]⁺ entails ∃xPx ∧ ∃xQx. One-line
invocation of distribution_Q.
Proposition 4.1 at the concrete model #
The (unenriched) universal premise ∀x(Px ∨ Qx) translates into mathlib
first-order syntax, and its support is classical Formula.Realize at
every index — [AvO23] Proposition 4.1 instantiated at
avoModel. The translation hypothesis is discharged by rfl: the
compiler computes.
The narrow-scope FC premise ◇(Px ∨ Qx) translates into the modal layer
over the monadic signature, and its support is Kripke satisfaction at
every index — the full [AvO23] Proposition 4.1
(modals included) at avoModel, the translation discharged by rfl.
The closed standard translation of ∀x(Px ∨ Qx): quantifiers
relativized to the individual sort, predicates world-relativized to the
current-world variable Sum.inr 0.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The closure is a genuine sentence: the compiler computes the free-variable finset.
Support of ∀x(Px ∨ Qx) at a singleton forces its sort-guarded closed
standard translation as a sentence of avoModel.stStructure — the
compactness-ready form, with every translation step (toModal?, st?,
the free-variable check) computed by the compiler.
Conversely, the sentence yields support at some singleton — sentencehood
of the translation makes ∀x(Px ∨ Qx)'s support assignment- and
state-independent.
Frame condition: avoModel is indisputable on every state #
avoModel's universal accessibility makes R indisputable on every state
(every world sees the same Finset.univ). Mirrors
Aloni2022.deonticModel_indisputable_on_team for the QBSML carrier.
Indisputability vs state-basedness (paper §4.1.1, Definition 4.10):
- Indisputable: all worlds in s↓ see the same accessible set (R constant).
- State-based: every w ∈ s↓ sees exactly s↓ (R(w) = s↓).
State-basedness is strictly stronger and is the precondition for the
epistemic facts: Fact 3 (ignorance_Q) and Fact 6 (distributionEpi_Q),
which therefore stay substrate-level (universal access is not
state-based). Facts 7, 8 and 10 need no frame condition at all — they
hold on every model.
Fact 4 (obviation): the Fig. 14 countermodel #
The paper's Fig. 14: a single index at the world where Pa and Qb both
hold, with an empty assignment and reflexive-only access. Its universal
x-extension supports the enriched disjunction by splitting horizontally
(x/a supports Px, x/b supports Qx), so the enriched premise holds;
but ∀x(◇Px ∧ ◇Qx) fails because the x/b index cannot see any world
where P holds of b.
The Fig. 14 domain: exactly the paper's two objects. (The third
FCAtom atom would give the universal extension an x/c index
supporting neither disjunct, breaking the premise — the paper notes the
split works "because the domain contains two objects".)
Instances For
Equations
- AloniVanOrmondt2023.instDecidableEqFig14Atom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
The Fig. 14 model: reflexive-only access at the both world.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Fig. 14 index: the both world with the empty assignment.
Equations
- AloniVanOrmondt2023.fig14Index = (Core.Logic.Modal.BSML.PowerSet2World.both, fun (x : Core.Logic.Modal.BSML.QVar) => none)
Instances For
The Fig. 14 state: the single-index state of the counterexample.
Instances For
The Fig. 14 state supports the enriched premise [∀x(Px ∨ Qx)]⁺: its
universal extension splits into the x/a half supporting [Px]⁺ and
the x/b half supporting [Qx]⁺ (paper Fig. 15).
The Fig. 14 state does not support ∀x(◇Px ∧ ◇Qx): at the x/b
index the only accessible world is both, where P holds of a alone
(paper Fig. 16's failing substate).
Fact 4 (obviation) of [AvO23]: the universal
quantifier obviates the free-choice/ignorance effect —
[∀x(Px ∨ Qx)]⁺ ⊭ ∀x(◇Px ∧ ◇Qx), witnessed by the Fig. 14
countermodel.