Free choice in QBSML #
This file proves the free-choice, ignorance, distribution and negation facts of QBSML for
arbitrary models. Each fact is a support consequence whose premise is a pragmatically enriched
formula: an enriched split disjunction under a modal or a quantifier needs a non-empty witness
for each disjunct, and the witness is transplanted into a ◇ or ∃ claim. Aloni and van
Ormondt state the facts for the numerals three ∨ more of their modified-numeral puzzles;
here they are stated for NE-free α, β where the proof allows, and for atoms where it
does not.
Main results #
QBSML.diamond_split: an enriched split disjunction supported on a modal pairing yields a non-empty world-set witness for each disjunct, the shared core.QBSML.narrowScopeFC,QBSML.boxFC,QBSML.universalFC: the free-choice facts, Facts 8, 7 and 9.QBSML.boxExiFC: quantified box free choice,[□∃x(α ∨ β)]⁺ ⊨ ◇∃xα ∧ ◇∃xβ.QBSML.ignorance,QBSML.distribution,QBSML.distributionEpi,QBSML.negationStrip: Facts 3, 5, 6 and 10.
Implementation notes #
Facts 3 and 6 need a state-based accessibility relation; the others hold in every model. Fact
4, obviation, is a countermodel claim and lives with its model in
Studies/AloniVanOrmondt2023.lean. □ is the derived ¬◇¬, so Fact 7 and the quantified
composite go through support_enrich_nec_iff rather than the paper's primitive □ clause.
Universal free choice is the pattern Chemla attested experimentally, and the quantified
composite is the shape behind Yan's Asher and Heim solutions.
References #
- [AvO23] Aloni and van Ormondt, Modified Numerals and Split Disjunction: The First-Order Case
- [Alo22] Aloni, Logic and Conversation: The Case of Free Choice
- [Che09b] Chemla, Universal implicatures and free choice effects: Experimental data
- [Yan23] Yan, Monotonicity in Intensional Contexts: Weakening and Pragmatic Effects under Modals and Attitudes
The diamond split #
An enriched split disjunction supported on a modal pairing yields a non-empty world-set witness for each disjunct. This is the shared core of the free-choice facts.
Free choice (Facts 7, 8 and 9) #
Narrow-scope free choice (Fact 8) is [◇(α ∨ β)]⁺ ⊨ ◇α ∧ ◇β for NE-free α, β.
Universal free choice (Fact 9) is [∀x◇(α ∨ β)]⁺ ⊨ ∀x◇α ∧ ∀x◇β for NE-free α, β.
It is Fact 8 at the universal extension s[x].
Box free choice (Fact 7) is [□(α ∨ β)]⁺ ⊨ ◇α ∧ ◇β for NE-free α, β, with the
derived □. The enriched premise puts the enriched disjunction on each index's full accessible
lift, where the diamond split produces the witnesses.
Quantified □-free choice #
[□∃x(α ∨ β)]⁺ ⊨ ◇∃xα ∧ ◇∃xβ is the composite of Fact 7 with an existential under the
modal, the form Yan's Asher and Heim solutions invoke (see Studies/Yan2023.lean).
Quantified box free choice is [□∃x(α ∨ β)]⁺ ⊨ ◇∃xα ∧ ◇∃xβ for NE-free α, β.
The enriched premise puts the enriched split disjunction on the functional extension of each
index's full accessible lift, and each non-empty half yields a ◇∃x witness.
Ignorance (Fact 3) #
Ignorance (Fact 3) is [Pc₁ ∨ Qc₂]⁺ ⊨ ◇Pc₁ ∧ ◇Qc₂ on a state-based R. It is stated
for constant atoms, as in the paper's Pa ∨ Pb, since the transplant argument needs
assignment-invariance and fails with a free variable in place of the constant.
Negation behaviour (Fact 10) #
Negation behaviour (Fact 10) is [¬(α ∨ β)]⁺ ⊨ ¬α ∧ ¬β for NE-free α, β, in every
model. Stripping the outer NE leaves anti-support of the enriched disjuncts, which
enrichment strengthens to classical anti-support of each.
Distribution (Facts 5 and 6) #
Distribution at maximal information (Fact 5) is [∀x(α ∨ β)]⁺ ⊨ ∃xα ∧ ∃xβ for NE-free
α, β on a singleton state {i}. The enriched premise splits the universal extension of
{i} into non-empty parts, and each part extends the same index, so it is the image of a
functional extension witnessing the existential.
Epistemic distribution (Fact 6) is [∀x(Px ∨ Qx)]⁺ ⊨ ∃x◇Px ∧ ∃x◇Qx on a state-based
R. It is stated for atoms, as in the paper, since the proof evaluates the atom pointwise at
a single transplanted world.