Xiang (2022): Relativized Exhaustivity: Mention-Some and Uniqueness

This file formalizes [Xia22]'s Relativized Exhaustivity, the presupposition that replaces [Day96]'s exhaustivity presupposition in modalized questions. A question is a topical property P : α → Set W from short answers to propositions, answered by [Fox13]'s max-informative true short answers, those not asymmetrically entailed by another true answer (MaxI, mathlib's MinimalFor), so that a can-question may have several complete answers. Dayal's presupposition that a strongest true answer exists (DEP) rules these out; Relativized Exhaustivity (RelExh) requires it instead of the non-modalized question at every accessible world verifying a true answer.

The main results are the paper's generalization for existential modals, that the mention-some readings of Wh-A can P? satisfy Relativized Exhaustivity exactly when Wh-A P? satisfies Dayal's presupposition at every accessible world where some member of A satisfies P (relExh_poss_iff), and the scenarios separating the two presuppositions. Local exhaustification of the nucleus makes the non-modalized question uniquely answered wherever it has a true answer, so the exhaustified mention-some reading of a can-question always satisfies Relativized Exhaustivity while Dayal's presupposition fails (relExh_poss_localExh, chair_scenario). A have to-question with a narrow-scope disjunctive answer separates them the other way: Dayal's presupposition holds while Relativized Exhaustivity fails wherever an accessible world violates uniqueness, the local-uniqueness inference of [HS20] (assign_scenario).

Implementation notes

The paper states Relativized Exhaustivity by quantifying over modal bases that send the evaluation world to a singleton subset of the original base; RelExh states the intended condition directly, for the modalized question O ∘ P built from the non-modalized property by an operator O over the accessibility relation. Local exhaustification is Exhaustification.exh over the alternatives of the wh-trace. Modal flavour and the anti-exhaustification analysis of disjunctive mention-all answers are not modelled.

References

• [Xia22]
• [Day96]
• [Fox13]
• [HS20]

Answerhood over topical properties

def Xiang2022.trueShort {W : Type u_1} {α : Type u_2} (P : α → Set W) (w : W) : Set α

The short answers true at a world.

Equations

• Xiang2022.trueShort P w = {a : α | w ∈ P a}

@[simp]

theorem Xiang2022.mem_trueShort {W : Type u_1} {α : Type u_2} {P : α → Set W} {w : W} {a : α} : a ∈ trueShort P w ↔ w ∈ P a

def Xiang2022.DEP {W : Type u_1} {α : Type u_2} (P : α → Set W) (w : W) : Prop

Dayal's exhaustivity presupposition for a topical property: its answer space has a strongest true member.

Equations

• Xiang2022.DEP P w = Question.IsExhaustivelyResolvable (Set.range P) w

theorem Xiang2022.dep_iff {W : Type u_1} {α : Type u_2} (P : α → Set W) (w : W) : DEP P w ↔ ∃ (a : α), w ∈ P a ∧ ∀ (b : α), w ∈ P b → P a ⊆ P b

The presupposition over short answers: a true short answer whose proposition entails every true one.

@[reducible, inline]

abbrev Xiang2022.MaxI {W : Type u_1} {α : Type u_2} (P : α → Set W) (w : W) (a : α) : Prop

A max-informative true short answer: true, and minimal under entailment among the true short answers.

Equations

• Xiang2022.MaxI P w a = MinimalFor (fun (x : α) => x ∈ Xiang2022.trueShort P w) P a

theorem Xiang2022.maxI_iff {W : Type u_1} {α : Type u_2} {P : α → Set W} {w : W} {a : α} : MaxI P w a ↔ w ∈ P a ∧ ∀ (b : α), w ∈ P b → ¬P b ⊂ P a

The paper's form: true, and not asymmetrically entailed by another true answer.

def Xiang2022.ansS {W : Type u_1} {α : Type u_2} (P : α → Set W) (w : W) : Set α

The short-answer operator: the max-informative true short answers.

Equations

• Xiang2022.ansS P w = {a : α | Xiang2022.MaxI P w a}

def Xiang2022.ansP {W : Type u_1} {α : Type u_2} (P : α → Set W) (w : W) : Set (Set W)

The propositional operator: the image of the short-answer operator.

Equations

• Xiang2022.ansP P w = P '' Xiang2022.ansS P w

theorem Xiang2022.mem_ansP_iff {W : Type u_1} {α : Type u_2} {P : α → Set W} {w : W} {p : Set W} : p ∈ ansP P w ↔ Minimal (fun (x : Set W) => x ∈ Question.trueAnswers (Set.range P) w) p

The propositional operator returns the minimal true members of the answer space.

theorem Xiang2022.ansP_eq_singleton {W : Type u_1} {α : Type u_2} {P : α → Set W} {w : W} {p : Set W} (h : Question.IsStrongestTrueAnswer (Set.range P) w p) : ansP P w = {p}

Under Dayal's presupposition the operator returns the strongest true answer alone.

Modalized questions

def Xiang2022.RelExh {W : Type u_1} {α : Type u_2} (O : Set W → Set W) (R : SetRel W W) (P : α → Set W) (w : W) : Prop

Relativized Exhaustivity for the question O ∘ P built from the non-modalized P by the operator O over the accessibility R: at every accessible world verifying one of the modalized question's true short answers, P satisfies Dayal's presupposition.

Equations

• Xiang2022.RelExh O R P w = ∀ (v : W), (w, v) ∈ R → (∃ (a : α), w ∈ O (P a) ∧ v ∈ P a) → Xiang2022.DEP P v

theorem Xiang2022.relExh_poss_iff {W : Type u_1} {α : Type u_2} (R : SetRel W W) (P : α → Set W) (w : W) : RelExh R.preimage R P w ↔ ∀ (v : W), (w, v) ∈ R → (trueShort P v).Nonempty → DEP P v

The generalization for existential modals: the mention-some readings satisfy Relativized Exhaustivity exactly when the non-modalized question satisfies Dayal's presupposition at every accessible world where some short answer is true.

theorem Xiang2022.relExh_id_iff {W : Type u_1} {α : Type u_2} (P : α → Set W) (w : W) : RelExh id SetRel.id P w ↔ (trueShort P w).Nonempty → DEP P w

For a non-modalized question, over the identity relation on which both modals are the identity, Relativized Exhaustivity is Dayal's presupposition wherever the question has a true answer.

Local exhaustification

def Xiang2022.localExh {W : Type u_1} {α : Type u_2} (P : α → Set W) : α → Set W

The nucleus exhaustified against the alternatives of the wh-trace: each short answer, and no other.

Equations

• Xiang2022.localExh P = Exhaustification.exh (Set.range P) ∘ P

theorem Xiang2022.eq_of_mem_localExh {W : Type u_1} {α : Type u_2} {P : α → Set W} {w : W} {a b : α} (ha : w ∈ localExh P a) (hb : w ∈ localExh P b) : P a = P b

Two true exhaustified short answers have the same proposition.

theorem Xiang2022.dep_localExh {W : Type u_1} {α : Type u_2} {P : α → Set W} {w : W} (h : (trueShort (localExh P) w).Nonempty) : DEP (localExh P) w

The exhaustified question satisfies Dayal's presupposition wherever it has a true answer.

theorem Xiang2022.relExh_poss_localExh {W : Type u_1} {α : Type u_2} (R : SetRel W W) (P : α → Set W) (w : W) : RelExh R.preimage R (localExh P) w

The exhaustified mention-some reading of a can-question satisfies Relativized Exhaustivity over any accessibility relation: the uniqueness it presupposes is existential.

The committee scenario

@[reducible, inline]

abbrev Xiang2022.CW : Type

The worlds of the committee scenario: the evaluation world 0 and the accessible worlds 1 and 2.

Equations

• Xiang2022.CW = Fin 3

def Xiang2022.chair : Fin 2 → Set CW

x chairs the committee: Andy (0) chairs in world 1, Billy (1) in world 2.

Equations

• Xiang2022.chair 0 = {1}
• Xiang2022.chair 1 = {2}

def Xiang2022.chairR : SetRel CW CW

The modal base: the evaluation world accesses both alternatives, each of which accesses only itself.

Equations

• Xiang2022.chairR = {p : Xiang2022.CW × Xiang2022.CW | if p.1 = 0 then p.2 ≠ 0 else p.1 = p.2}

theorem Xiang2022.poss_localExh_chair (a : Fin 2) : chairR.preimage (localExh chair a) = {0, a.succ}

Under the base, x can chair holds at the evaluation world and at x's own world.

theorem Xiang2022.chair_scenario : ansS (chairR.preimage ∘ localExh chair) 0 = Set.univ ∧ RelExh chairR.preimage chairR (localExh chair) 0 ∧ ¬DEP (chairR.preimage ∘ localExh chair) 0

The exhaustified mention-some reading of Who can chair the committee? has both short answers max-informative, satisfies Relativized Exhaustivity, and violates Dayal's presupposition.

The chapter scenario

@[reducible, inline]

abbrev Xiang2022.AW : Type

The worlds of the chapter scenario: the evaluation worlds 0 and 4, and the accessible worlds 1, 2, 3.

Equations

• Xiang2022.AW = Fin 5

def Xiang2022.assigned : Fin 2 → Set AW

We assign chapter c: chapter 1 is assigned in worlds 1 and 3, chapter 2 in worlds 2 and 3.

Equations

• Xiang2022.assigned 0 = {1, 3}
• Xiang2022.assigned 1 = {2, 3}

def Xiang2022.assign : Fin 3 → Set AW

The narrow-scope higher-order answers: either chapter, or their disjunction.

Equations

• Xiang2022.assign 0 = Xiang2022.assigned 0
• Xiang2022.assign 1 = Xiang2022.assigned 1
• Xiang2022.assign 2 = Xiang2022.assigned 0 ∪ Xiang2022.assigned 1

theorem Xiang2022.range_assign : Set.range assign = supClosure (Set.range assigned)

The higher-order answer space is the disjunctive closure of the first-order one.

def Xiang2022.assignR : SetRel AW AW

The modal base: world 0 accesses the uniqueness-violating world 3, world 4 does not.

Equations

• Xiang2022.assignR = {p : Xiang2022.AW × Xiang2022.AW | if p.1 = 0 then p.2 ∈ {1, 2, 3} else if p.1 = 4 then p.2 ∈ {1, 2} else p.1 = p.2}

theorem Xiang2022.dep_assigned_iff (v : AW) : DEP assigned v ↔ v = 1 ∨ v = 2

The first-order question satisfies Dayal's presupposition exactly at the worlds assigning one chapter.

theorem Xiang2022.dep_assign_iff (v : AW) : DEP assign v ↔ v = 1 ∨ v = 2

So does the higher-order question: at world 3 the disjunction is entailed by both disjuncts, so no true answer is strongest.

theorem Xiang2022.assign_scenario : DEP (assignR.core ∘ assign) 0 ∧ ¬RelExh assignR.core assignR assign 0 ∧ RelExh assignR.core assignR assign 4

Dayal's presupposition holds of the modalized question at world 0, where the disjunction is its only true answer, while Relativized Exhaustivity fails there and holds at world 4: the local-uniqueness inference of Which chapter do we have to assign?.

theorem Xiang2022.assign_can_scenario : ¬RelExh assignR.preimage assignR assigned 0 ∧ RelExh assignR.preimage assignR assigned 4

The first-order mention-some reading of Which chapter can we assign? over the same base: Relativized Exhaustivity fails at world 0, whose accessible world 3 assigns both chapters, and holds at world 4, the universal local-uniqueness inference.