Documentation

Linglib.Studies.DelPinalBassiSauerland2024

Del Pinal, Bassi & Sauerland (2024): free choice and presuppositional exhaustification #

[DPBS24] derive free choice with pex^{IE+II} (Exhaustification.Presuppositional.pexIEII), which asserts its prejacent and presupposes the negation of the innocently excludable alternatives together with homogeneity over the innocently includable ones. On ◇(p ∨ q) this is (14): the presupposed ◇p ↔ ◇q with the asserted disjunction entails ◇p ∧ ◇q (pex_fc), and the same structure gives double prohibition under negation (16) (pex_double_prohibition) and, with the necessity alternatives relabelled, negative free choice (19a)–(20) (pex_negative_fc, pex_double_requirement). The split is what flat exh^{IE+II} lacks, and the paper's embedded puzzles turn on it. Under a negative factive (§3), the factive presupposes the whole pex output, so free choice is presupposed (fc_presupposed_under_neg_factive), while the assertion denies belief in the bare prejacent, which denies belief in either disjunct (pex_unaware_target); a flat exh complement yields only denial of belief in the exhaustified conjunction, which a believer in free choice can satisfy (exh_unaware_too_weak). In a disjunction (§4) the homogeneity presupposition of the second disjunct is filtered in its local context ([Sch09a]) and free choice follows there (filtering_fc), whereas flat exh leaves nothing to project (exh_filtering_trivial). Under quantifiers (§5.1) universal projection of the presupposition gives universal, universal-negative, and existential free choice, (62), (63), (75) (universal_fc, universal_negative_fc, existential_fc), and under exactly one (§5.2) the salient readings of (76)–(77) of [GRS20] (exactly_one_fc, exactly_one_double_prohibition). The five-world model and alternative set are [BLF20]'s.

pex^{IE+II} on ◇(p ∨ q) (§2) #

(14): the presupposed homogeneity ◇p ↔ ◇q with the asserted ◇(p ∨ q) gives free choice.

(16): negation denies the prejacent and leaves the presupposition, so ¬pex[◇(p ∨ q)] is double prohibition.

@[reducible, inline]

¬□T, read on the five-world model: the alternatives to ¬□(T ∧ B)¬□T, ¬□B, ¬□(T ∨ B) — have the same innocent-exclusion/inclusion structure as those to ◇(p ∨ q), with ¬□T in the place of ◇q and ¬□B in the place of ◇p.

Equations
Instances For
    @[reducible, inline]

    ¬□B on the five-world model.

    Equations
    Instances For

      (19a): pex^{IE+II}[¬□(T ∧ B)] gives negative free choice.

      (20): ¬pex^{IE+II}[□(T ∧ B)] gives double requirement.

      Free choice under negative factives (§3) #

      Under a negative factive the whole pex output is presupposed, so free choice is presupposed, (21a).

      The factive's assertion denies belief in the prejacent ◇(p ∨ q), hence belief in either disjunct, (21b).

      With a flat exh complement the factive's assertion only denies belief in the exhaustified conjunction, which an attitude holder who believes free choice but not exclusivity satisfies (§3.1).

      Filtering free choice (§4) #

      In A or pex[◇(p ∨ q)] the homogeneity presupposition is satisfied in the second disjunct's local context c ∧ ¬A, and free choice follows there.

      Free choice under quantifiers (§5) #

      theorem DelPinalBassiSauerland2024.universal_fc {Student : Type u_1} (S permC permIC : StudentProp) (hassert : ∀ (x : Student), S xpermC x permIC x) (hhomog : ∀ (x : Student), S x(permC x permIC x)) :
      (∀ (x : Student), S xpermC x) ∀ (x : Student), S xpermIC x

      (62): universal projection of homogeneity and the universal assertion give universal free choice.

      theorem DelPinalBassiSauerland2024.universal_negative_fc {Student : Type u_1} (S reqA reqB : StudentProp) (hassert : ¬∃ (x : Student), S x reqA x reqB x) (hhomog : ∀ (x : Student), S x(reqA x reqB x)) :
      (¬∃ (x : Student), S x reqA x) ¬∃ (x : Student), S x reqB x

      (63): with a negated existential assertion, universal negative free choice.

      theorem DelPinalBassiSauerland2024.existential_fc {Student : Type u_1} (S permC permIC : StudentProp) (hassert : ∃ (x : Student), S x (permC x permIC x)) (hhomog : ∀ (x : Student), S x(permC x permIC x)) :
      ∃ (x : Student), S x permC x permIC x

      (75): with an existential assertion, existential free choice.

      theorem DelPinalBassiSauerland2024.exactly_one_fc {Student : Type u_1} (S permL permC : StudentProp) (x₀ : Student) (hx₀ : S x₀) (hpos : permL x₀ permC x₀) (hneg : ∀ (x : Student), S xx x₀¬(permL x permC x)) (hhomog : ∀ (x : Student), S x(permL x permC x)) :
      (permL x₀ permC x₀) ∀ (x : Student), S xx x₀¬permL x ¬permC x

      (76a): under exactly one, the witness has free choice and every other student double prohibition.

      theorem DelPinalBassiSauerland2024.exactly_one_double_prohibition {Student : Type u_1} (S permL permC : StudentProp) (x₀ : Student) (hneg : ¬(permL x₀ permC x₀)) (hpos : ∀ (x : Student), S xx x₀permL x permC x) (hhomog : ∀ (x : Student), S x(permL x permC x)) :
      (¬permL x₀ ¬permC x₀) ∀ (x : Student), S xx x₀permL x permC x

      (77a): under exactly one … can't, the witness has double prohibition and every other student free choice.