@cite{xiang-2022}: Relativized Exhaustivity @cite{xiang-2022}

Empirical data on mention-some and uniqueness from: @cite{xiang-2022}. Relativized Exhaustivity: mention-some and uniqueness. Natural Language Semantics 30:311–362.

Overview

@cite{xiang-2022} makes three contributions:

1. MS answers are subject to a "mention-one-only" constraint: they must name a single individual, not a disjunction (ex. 3–4).
2. MS is primarily grammatically licensed by ability can inside the question nucleus, not pragmatically by decision problems. The MS/MA ambiguity in can-questions reflects structural scope ambiguity of the wh-trace relative to the modal (first-order vs higher-order).
3. The RelExh presupposition (91) — exhaustivity evaluated relative to singleton modal bases — unifies MS licensing, avoids over-generation for non-can questions, and derives local-uniqueness effects in modalized singular wh-questions.

Data points

Empirical generalizations from the paper, with exact example numbers:

1. "Who can chair the committee?" — MS available (ex. 2)
2. "Who called?" — MA required (ex. 1)
3. Mention-one-only constraint (ex. 3–4)
4. Non-can modals block MS: should, might (ex. 6)
5. Same question, different contexts → MS vs MA (Section 2.2)
6. Singular uniqueness effects (Section 4.3, Section 6.3)
7. Table 3 summary: RelExh vs Dayal's EP predictions

inductive Phenomena.Questions.Studies.Xiang2022.MSMAJudgment : Type

Whether a question receives mention-some, mention-all, or is ambiguous between the two readings.

• mentionSome : MSMAJudgment
• mentionAll : MSMAJudgment
• ambiguous : MSMAJudgment

instance Phenomena.Questions.Studies.Xiang2022.instDecidableEqMSMAJudgment : DecidableEq MSMAJudgment

Equations

• Phenomena.Questions.Studies.Xiang2022.instDecidableEqMSMAJudgment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Questions.Studies.Xiang2022.instReprMSMAJudgment : Repr MSMAJudgment

Equations

• Phenomena.Questions.Studies.Xiang2022.instReprMSMAJudgment = { reprPrec := Phenomena.Questions.Studies.Xiang2022.instReprMSMAJudgment.repr }

def Phenomena.Questions.Studies.Xiang2022.instReprMSMAJudgment.repr : MSMAJudgment → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

inductive Phenomena.Questions.Studies.Xiang2022.ModalType : Type

Type of modal in the question, which affects MS/MA availability. Xiang's key claim: only ability can grammatically licenses MS.

• none : ModalType
• abilityCan : ModalType
• epistemicMight : ModalType
• deonticShould : ModalType

instance Phenomena.Questions.Studies.Xiang2022.instDecidableEqModalType : DecidableEq ModalType

Equations

• Phenomena.Questions.Studies.Xiang2022.instDecidableEqModalType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Questions.Studies.Xiang2022.instReprModalType.repr : ModalType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Phenomena.Questions.Studies.Xiang2022.instReprModalType : Repr ModalType

Equations

• Phenomena.Questions.Studies.Xiang2022.instReprModalType = { reprPrec := Phenomena.Questions.Studies.Xiang2022.instReprModalType.repr }

structure Phenomena.Questions.Studies.Xiang2022.Xiang2022Datum : Type

A single empirical datum from.

• question : String

  The question under study

• modalType : ModalType

  What modal (if any) appears in the question

• judgment : MSMAJudgment

  Observed MS/MA judgment

• exampleAnswer : String

  An example answer or context

• source : String

  Source reference within the paper

def Phenomena.Questions.Studies.Xiang2022.instReprXiang2022Datum.repr : Xiang2022Datum → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Phenomena.Questions.Studies.Xiang2022.instReprXiang2022Datum : Repr Xiang2022Datum

Equations

• Phenomena.Questions.Studies.Xiang2022.instReprXiang2022Datum = { reprPrec := Phenomena.Questions.Studies.Xiang2022.instReprXiang2022Datum.repr }

Core data: MS licensing by modal type

def Phenomena.Questions.Studies.Xiang2022.canQuestionMS : Xiang2022Datum

Ability can licenses mention-some (ex. 2).

"Who can chair the committee?" — naming a single individual is a sufficient answer. This is the paper's central empirical observation: MS is grammatically licensed by can.

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.Studies.Xiang2022.bareQuestionMA : Xiang2022Datum

Bare wh-question requires mention-all (ex. 1).

"Who called?" — without a modal, the question demands exhaustive listing. Non-modalized questions uniformly receive MA.

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.Studies.Xiang2022.deonticBlocksMS : Xiang2022Datum

Deontic should blocks mention-some (ex. 6b).

"Which students should pass the test?" — even though modal, deontic modals pattern with MA. Only ability can licenses MS.

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.Studies.Xiang2022.epistemicBlocksMS : Xiang2022Datum

Epistemic might blocks mention-some (ex. 6c).

"Which students might pass the test?" — epistemics pattern with MA, not MS. The question demands the full epistemic picture.

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.Studies.Xiang2022.nonModalMA : Xiang2022Datum

Non-modalized question requires MA (ex. 6a).

"Which students passed the test?" — without a modal, exhaustive.

Equations

• One or more equations did not get rendered due to their size.

Context sensitivity (Section 2.2)

def Phenomena.Questions.Studies.Xiang2022.goalDrivenMS : Xiang2022Datum

Goal-driven MS: same question, recruit-one goal (Section 2.2).

"Who can chair the committee?" with the goal of recruiting one person. @cite{van-rooy-2003} models this via a decision problem where any single committee member resolves the DP.

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.Studies.Xiang2022.goalDrivenMA : Xiang2022Datum

Goal-driven MA: same question, know-all goal (Section 2.2).

Same question as above, but the goal of knowing the full candidate list. The DP requires complete information, so all candidates must be named.

Equations

• One or more equations did not get rendered due to their size.

Mention-one-only constraint (ex. 3–4)

structure Phenomena.Questions.Studies.Xiang2022.MentionOneOnlyDatum : Type

Whether an MS answer obeys the mention-one-only constraint.

• question : String

  The question

• answer : String

  The proposed MS answer

• acceptable : Bool

  Is this answer acceptable as an MS answer?

• source : String

  Source

instance Phenomena.Questions.Studies.Xiang2022.instReprMentionOneOnlyDatum : Repr MentionOneOnlyDatum

Equations

• Phenomena.Questions.Studies.Xiang2022.instReprMentionOneOnlyDatum = { reprPrec := Phenomena.Questions.Studies.Xiang2022.instReprMentionOneOnlyDatum.repr }

def Phenomena.Questions.Studies.Xiang2022.instReprMentionOneOnlyDatum.repr : MentionOneOnlyDatum → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.Studies.Xiang2022.mentionOneValid : MentionOneOnlyDatum

Valid MS answer: single individual (ex. 3a).

"Anne can." — a single-individual MS answer is acceptable.

Equations

• Phenomena.Questions.Studies.Xiang2022.mentionOneValid = { question := "Who can chair the committee?", answer := "Anne can.", acceptable := true, source := "Xiang 2022, ex. 3a" }

def Phenomena.Questions.Studies.Xiang2022.mentionOneInvalid : MentionOneOnlyDatum

Invalid MS answer: disjunction (ex. 3b).

"#Anne or Bill can." — a disjunctive MS answer is blocked by the mention-one-only constraint. This is NOT predicted by van Rooij's decision-theoretic account but IS predicted by Xiang's semantic analysis.

Equations

• Phenomena.Questions.Studies.Xiang2022.mentionOneInvalid = { question := "Who can chair the committee?", answer := "#Anne or Bill can.", acceptable := false, source := "Xiang 2022, ex. 3b" }

Uniqueness effects (Section 4.3, Section 6.3)

inductive Phenomena.Questions.Studies.Xiang2022.UniquenessType : Type

Types of uniqueness inference observed in singular wh-questions. Xiang distinguishes global vs local uniqueness (Table 3).

• global : UniquenessType
• local : UniquenessType
• existLocal : UniquenessType
• none : UniquenessType

instance Phenomena.Questions.Studies.Xiang2022.instDecidableEqUniquenessType : DecidableEq UniquenessType

Equations

• Phenomena.Questions.Studies.Xiang2022.instDecidableEqUniquenessType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Questions.Studies.Xiang2022.instReprUniquenessType.repr : UniquenessType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Phenomena.Questions.Studies.Xiang2022.instReprUniquenessType : Repr UniquenessType

Equations

• Phenomena.Questions.Studies.Xiang2022.instReprUniquenessType = { reprPrec := Phenomena.Questions.Studies.Xiang2022.instReprUniquenessType.repr }

structure Phenomena.Questions.Studies.Xiang2022.UniquenessDatum : Type

A datum about uniqueness effects in singular wh-questions.

• question : String

  The question

• modalType : ModalType

  Modal type

• uniqueness : UniquenessType

  Type of uniqueness inference

• dayalEPPredicts : Bool

  Whether Dayal's EP predicts this

• relExhPredicts : Bool

  Whether RelExh predicts this

• source : String

  Source

instance Phenomena.Questions.Studies.Xiang2022.instReprUniquenessDatum : Repr UniquenessDatum

Equations

• Phenomena.Questions.Studies.Xiang2022.instReprUniquenessDatum = { reprPrec := Phenomena.Questions.Studies.Xiang2022.instReprUniquenessDatum.repr }

def Phenomena.Questions.Studies.Xiang2022.instReprUniquenessDatum.repr : UniquenessDatum → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.Studies.Xiang2022.nonModalUniqueness : UniquenessDatum

Non-modalized singular: global uniqueness. "Which child came?" — presupposes exactly one child came. Both Dayal's EP and RelExh predict this. (Table 3, row 1)

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.Studies.Xiang2022.boxModalGlobalUniq : UniquenessDatum

□-modal singular (have-to), global uniqueness. "Which chapter do we have to assign?" — global uniqueness reading. Both Dayal's EP and RelExh predict. (Table 3, row 3)

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.Studies.Xiang2022.boxModalLocalUniq : UniquenessDatum

□-modal singular (have-to), local uniqueness. "Which chapter do we have to assign?" — local uniqueness reading. Dayal's EP does NOT predict this; RelExh DOES. This is a key advantage of RelExh over Dayal's EP. (Table 3, row 4)

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.Studies.Xiang2022.canModalLocalUniqMS : UniquenessDatum

◇-modal singular (can), local uniqueness in MS. "Which chapter can we assign?" — existential local uniqueness. Dayal's EP does NOT predict; RelExh DOES. (Table 3, row 8)

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.Studies.Xiang2022.canModalGlobalUniq : UniquenessDatum

◇-modal singular (can), global uniqueness. "Which chapter can we assign?" — global uniqueness. Dayal's EP predicts this but RelExh does NOT — the only cell in Table 3 where Dayal's EP has coverage that RelExh lacks. (Table 3, row 7)

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.Studies.Xiang2022.uniquenessData : List UniquenessDatum

Equations

• One or more equations did not get rendered due to their size.

Aggregation

def Phenomena.Questions.Studies.Xiang2022.allData : List Xiang2022Datum

All MS/MA judgment data points from the paper.

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.Studies.Xiang2022.msCount : ℕ

Data points classified as mention-some.

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.Studies.Xiang2022.maCount : ℕ

Data points classified as mention-all.

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.Studies.Xiang2022.relExhAdvantages : ℕ

Table 3 cells where RelExh has coverage that Dayal's EP lacks.

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.Studies.Xiang2022.dayalAdvantages : ℕ

Table 3 cells where Dayal's EP has coverage that RelExh lacks.

Equations

• One or more equations did not get rendered due to their size.

Bridge: RelExh Derivation + Decision-Theoretic Agreement

Formalizes the derivation chain from, Section 5.2 (ex. 93):

1. Define the paper's own scenario (3 worlds, 2 individuals, ability modal base)
2. Show EP fails for the FO can-question (overlapping answer propositions)
3. Show RelExh passes (each singleton modal base has a strongest answer)
4. Show DecisionTheory independently classifies this as mention-some
5. Prove both frameworks agree on the same finite model
6. Contrast with partition reading: EP holds → MA

This connects Xiang's semantic theory (Theories.Semantics.Questions.Exhaustivity) to the decision-theoretic infrastructure (Core.Agent.DecisionTheory) through a shared concrete scenario, exercising both and proving agreement.

Scenario (ex. 93)

• Worlds: w0 (utterance world), w1, w2
• Individuals: a, b
• Base predicate: chairs(w1, a) = true, chairs(w2, b) = true, else false
• Ability modal base: mb(w0) = [w1, w2], mb(w1) = [w1], mb(w2) = [w2]

Under the FO interpretation, "Who can chair?" gets overlapping cells:

• ◇chair(a) = {w0, w1} (a can chair at w0 via w1, and trivially at w1)
• ◇chair(b) = {w0, w2} (b can chair at w0 via w2, and trivially at w2)

These overlap at w0 → EP fails → but RelExh passes → MS licensed.

Definitions Exercised

Definition	Source	How Exercised
dayalEP	Exhaustivity.lean	2 theorems (fails FO, holds partition)
relExh	Exhaustivity.lean	2 theorems (passes FO, holds partition)
foQDen	Exhaustivity.lean	Used throughout scenario
propEntails	Exhaustivity.lean	2 theorems (incomparability)
DecisionProblem	Core.Agent.DecisionTheory	findChairDP, identifyAllDP
isMentionSome	Core.Agent.DecisionTheory	canQ_mentionSome
isMentionAll	Core.Agent.DecisionTheory	foQ_identifyAll_mentionAll
questionUtility	Core.Agent.DecisionTheory	questionUtility_positive
completeInformationDP	Core.Agent.DecisionTheory	identifyAllDP

Finite Types (ex. 93 scenario)

inductive Phenomena.Questions.Studies.Xiang2022.XW : Type

Three worlds: w0 is the utterance world, w1 and w2 are accessible.

• w0 : XW
• w1 : XW
• w2 : XW

instance Phenomena.Questions.Studies.Xiang2022.instDecidableEqXW : DecidableEq XW

Equations

• Phenomena.Questions.Studies.Xiang2022.instDecidableEqXW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Questions.Studies.Xiang2022.instReprXW.repr : XW → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance Phenomena.Questions.Studies.Xiang2022.instReprXW : Repr XW

Equations

• Phenomena.Questions.Studies.Xiang2022.instReprXW = { reprPrec := Phenomena.Questions.Studies.Xiang2022.instReprXW.repr }

def Phenomena.Questions.Studies.Xiang2022.instBEqXW.beq : XW → XW → Bool

Equations

• Phenomena.Questions.Studies.Xiang2022.instBEqXW.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Questions.Studies.Xiang2022.instBEqXW : BEq XW

Equations

• Phenomena.Questions.Studies.Xiang2022.instBEqXW = { beq := Phenomena.Questions.Studies.Xiang2022.instBEqXW.beq }

instance Phenomena.Questions.Studies.Xiang2022.instFintypeXW : Fintype XW

Equations

• One or more equations did not get rendered due to their size.

inductive Phenomena.Questions.Studies.Xiang2022.XP : Type

Two individuals who might chair the committee.

• a : XP
• b : XP

instance Phenomena.Questions.Studies.Xiang2022.instDecidableEqXP : DecidableEq XP

Equations

• Phenomena.Questions.Studies.Xiang2022.instDecidableEqXP x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Questions.Studies.Xiang2022.instReprXP : Repr XP

Equations

• Phenomena.Questions.Studies.Xiang2022.instReprXP = { reprPrec := Phenomena.Questions.Studies.Xiang2022.instReprXP.repr }

def Phenomena.Questions.Studies.Xiang2022.instReprXP.repr : XP → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.Studies.Xiang2022.instBEqXP.beq : XP → XP → Bool

Equations

• Phenomena.Questions.Studies.Xiang2022.instBEqXP.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Questions.Studies.Xiang2022.instBEqXP : BEq XP

Equations

• Phenomena.Questions.Studies.Xiang2022.instBEqXP = { beq := Phenomena.Questions.Studies.Xiang2022.instBEqXP.beq }

instance Phenomena.Questions.Studies.Xiang2022.instFintypeXP : Fintype XP

Equations

• One or more equations did not get rendered due to their size.

Base Predicate and Modal Base

def Phenomena.Questions.Studies.Xiang2022.chairs : XW → XP → Bool

Base predicate: who actually chairs in each world. In w1, individual a chairs; in w2, individual b chairs; w0 is the utterance world where no one directly chairs.

Equations

• Phenomena.Questions.Studies.Xiang2022.chairs Phenomena.Questions.Studies.Xiang2022.XW.w1 Phenomena.Questions.Studies.Xiang2022.XP.a = true
• Phenomena.Questions.Studies.Xiang2022.chairs Phenomena.Questions.Studies.Xiang2022.XW.w2 Phenomena.Questions.Studies.Xiang2022.XP.b = true
• Phenomena.Questions.Studies.Xiang2022.chairs x✝¹ x✝ = false

def Phenomena.Questions.Studies.Xiang2022.abilityMB : XW → List XW

Ability modal base: from w0, both w1 and w2 are accessible (representing what is possible). From w1/w2, only the world itself is accessible (the abilities are settled).

Equations

• Phenomena.Questions.Studies.Xiang2022.abilityMB Phenomena.Questions.Studies.Xiang2022.XW.w0 = [Phenomena.Questions.Studies.Xiang2022.XW.w1, Phenomena.Questions.Studies.Xiang2022.XW.w2]
• Phenomena.Questions.Studies.Xiang2022.abilityMB Phenomena.Questions.Studies.Xiang2022.XW.w1 = [Phenomena.Questions.Studies.Xiang2022.XW.w1]
• Phenomena.Questions.Studies.Xiang2022.abilityMB Phenomena.Questions.Studies.Xiang2022.XW.w2 = [Phenomena.Questions.Studies.Xiang2022.XW.w2]

def Phenomena.Questions.Studies.Xiang2022.allWorlds : List XW

All worlds in the scenario.

Equations

• Phenomena.Questions.Studies.Xiang2022.allWorlds = [Phenomena.Questions.Studies.Xiang2022.XW.w0, Phenomena.Questions.Studies.Xiang2022.XW.w1, Phenomena.Questions.Studies.Xiang2022.XW.w2]

def Phenomena.Questions.Studies.Xiang2022.allIndividuals : List XP

All individuals.

Equations

• Phenomena.Questions.Studies.Xiang2022.allIndividuals = [Phenomena.Questions.Studies.Xiang2022.XP.a, Phenomena.Questions.Studies.Xiang2022.XP.b]

FO Question Denotation (can-question, wh below modal)

Under the FO interpretation, the question "Who can chair?" has denotation: ⟦who can chair⟧(mb)(α)(w) = ∃v ∈ mb(w). chairs(v, α)

This gives overlapping cells at w0:

• ◇chair(a) at w0: w1 ∈ mb(w0) and chairs(w1,a) → true
• ◇chair(b) at w0: w2 ∈ mb(w0) and chairs(w2,b) → true

def Phenomena.Questions.Studies.Xiang2022.foCells : Core.DecisionTheory.Question XW

The FO cells as explicit propositions, for use with DecisionTheory.

Equations

• One or more equations did not get rendered due to their size.

Partition Question Denotation (HO reading / non-modal)

Under the partition interpretation, each cell identifies a single world. This models the higher-order reading where the questioner wants to know exactly which world obtains.

def Phenomena.Questions.Studies.Xiang2022.partQDen : (XW → List XW) → XW → XW → Bool

Partition qden: ignores modal base, directly tests world identity.

Equations

• Phenomena.Questions.Studies.Xiang2022.partQDen x✝ target w = (w == target)

def Phenomena.Questions.Studies.Xiang2022.partCells : Core.DecisionTheory.Question XW

Partition cells: one cell per world.

Equations

• One or more equations did not get rendered due to their size.

Decision Problems

def Phenomena.Questions.Studies.Xiang2022.findChairDP : Core.DecisionTheory.DecisionProblem XW XP

Find-chair DP: utility 1 iff the nominated person can chair in some accessible world. Models the "recruit one committee member" context.

Equations

• One or more equations did not get rendered due to their size.

def Phenomena.Questions.Studies.Xiang2022.identifyAllDP : Core.DecisionTheory.DecisionProblem XW XW

Identify-all DP: utility 1 iff guessed world matches true world. Models the "complete roster" context.

Equations

• Phenomena.Questions.Studies.Xiang2022.identifyAllDP = { utility := Core.DecisionTheory.completeInformationDP.utility, prior := fun (x : Phenomena.Questions.Studies.Xiang2022.XW) => 1 / 3 }

Part I: EP/RelExh Derivation Chain (Section 5.2)

The derivation follows ex. 93 exactly:

1. Both a and b are true answers at w0 under FO interpretation
2. Their propositions are incomparable (neither entails the other)
3. Therefore EP fails at w0 (no strongest true answer)
4. But RelExh passes: each singleton {w1}, {w2} has EP
5. Therefore MS is semantically licensed

Step 1: True answers at w0

theorem Phenomena.Questions.Studies.Xiang2022.foAnswer_true_a : Theories.Semantics.Questions.Exhaustivity.foQDen chairs abilityMB XP.a XW.w0 = true

◇chair(a) holds at w0: there exists v ∈ mb(w0) where a chairs (namely w1).

theorem Phenomena.Questions.Studies.Xiang2022.foAnswer_true_b : Theories.Semantics.Questions.Exhaustivity.foQDen chairs abilityMB XP.b XW.w0 = true

◇chair(b) holds at w0: there exists v ∈ mb(w0) where b chairs (namely w2).

Step 2: Propositions are incomparable

theorem Phenomena.Questions.Studies.Xiang2022.propExt_a_not_entails_b : Theories.Semantics.Questions.Exhaustivity.propEntails (Theories.Semantics.Questions.Exhaustivity.foQDen chairs abilityMB XP.a) (Theories.Semantics.Questions.Exhaustivity.foQDen chairs abilityMB XP.b) allWorlds = false

The a-proposition does not entail the b-proposition. ◇chair(a) = {w0, w1} and ◇chair(b) = {w0, w2}: w1 ∈ ◇chair(a) but w1 ∉ ◇chair(b).

theorem Phenomena.Questions.Studies.Xiang2022.propExt_b_not_entails_a : Theories.Semantics.Questions.Exhaustivity.propEntails (Theories.Semantics.Questions.Exhaustivity.foQDen chairs abilityMB XP.b) (Theories.Semantics.Questions.Exhaustivity.foQDen chairs abilityMB XP.a) allWorlds = false

The b-proposition does not entail the a-proposition. w2 ∈ ◇chair(b) but w2 ∉ ◇chair(a).

Step 3: EP fails

theorem Phenomena.Questions.Studies.Xiang2022.canQ_ep_fails : Theories.Semantics.Questions.Exhaustivity.dayalEP (Theories.Semantics.Questions.Exhaustivity.foQDen chairs) abilityMB [XP.a, XP.b] allWorlds XW.w0 = false

EP fails for the FO can-question at w0 (ex. 93).

Both a and b are true answers at w0, but neither proposition entails the other (they overlap at w0 but diverge at w1 vs w2). So there is no strongest true answer, and Dayal's exhaustivity presupposition is not met.

Step 4: RelExh passes

theorem Phenomena.Questions.Studies.Xiang2022.canQ_relExh_passes : Theories.Semantics.Questions.Exhaustivity.relExh (Theories.Semantics.Questions.Exhaustivity.foQDen chairs) abilityMB [XP.a, XP.b] allWorlds XW.w0 = true

RelExh passes for the FO can-question at w0 (ex. 93).

For each v ∈ mb(w0) = {w1, w2}:

• Singleton {w1}: only a chairs → ◇chair(a) is the unique true answer → EP holds
• Singleton {w2}: only b chairs → ◇chair(b) is the unique true answer → EP holds

Since EP holds for every singleton subbase, RelExh is satisfied.

Step 5: DecisionTheory agrees

theorem Phenomena.Questions.Studies.Xiang2022.canQ_mentionSome : Core.DecisionTheory.isMentionSome findChairDP {XW.w0, XW.w1, XW.w2} {XP.a, XP.b} foCells = true

DecisionTheory independently classifies the FO can-question as mention-some. Both FO cells resolve findChairDP (learning that a can chair → nominate a; learning that b can chair → nominate b), and the cells overlap at w0.

theorem Phenomena.Questions.Studies.Xiang2022.canQ_semantic_pragmatic_agree : Theories.Semantics.Questions.Exhaustivity.relExh (Theories.Semantics.Questions.Exhaustivity.foQDen chairs) abilityMB [XP.a, XP.b] allWorlds XW.w0 = true ∧ Core.DecisionTheory.isMentionSome findChairDP {XW.w0, XW.w1, XW.w2} {XP.a, XP.b} foCells = true

Semantic–pragmatic agreement on MS: RelExh passes AND DecisionTheory says mention-some, on the same finite model.

Structural link: cells are qden

theorem Phenomena.Questions.Studies.Xiang2022.foCells_eq_qden : foCells = [Theories.Semantics.Questions.Exhaustivity.foQDen chairs abilityMB XP.a, Theories.Semantics.Questions.Exhaustivity.foQDen chairs abilityMB XP.b]

The FO cells used for DecisionTheory are structurally identical to the foQDen-derived propositions. This makes the agreement non-accidental: both frameworks operate on the same answer-space structure.

Part II: Partition Contrast (MA reading)

Under the partition interpretation, each cell identifies exactly one world. EP trivially holds (the unique true cell entails itself), and DecisionTheory classifies this as mention-all (no resolving answers for identify-all DP, since individual cells don't tell you the exact world).

theorem Phenomena.Questions.Studies.Xiang2022.partQ_ep_holds : Theories.Semantics.Questions.Exhaustivity.dayalEP partQDen abilityMB [XW.w0, XW.w1, XW.w2] allWorlds XW.w0 = true

EP holds for the partition reading at w0. Under partQDen, only the w0-cell is true at w0, so it trivially entails all other true cells (there are none).

theorem Phenomena.Questions.Studies.Xiang2022.partQ_relExh_holds : Theories.Semantics.Questions.Exhaustivity.relExh partQDen abilityMB [XW.w0, XW.w1, XW.w2] allWorlds XW.w0 = true

RelExh holds for the partition reading at w0. EP holds for the full question, so a fortiori it holds for each singleton modal base.

theorem Phenomena.Questions.Studies.Xiang2022.foQ_identifyAll_mentionAll : Core.DecisionTheory.isMentionAll identifyAllDP {XW.w0, XW.w1, XW.w2} {XW.w0, XW.w1, XW.w2} foCells = true

DecisionTheory classifies the FO can-question as mention-all when the goal is complete identification. FO cells don't resolve identifyAllDP: knowing that a can chair (= being in {w0, w1}) doesn't identify whether you're in w0 or w1.

Part III: Preserved from Prior Bridge

Structural properties of the answer space and questionUtility.

theorem Phenomena.Questions.Studies.Xiang2022.questionUtility_positive : Core.DecisionTheory.questionUtility findChairDP {XP.a, XP.b} (Core.DecisionTheory.questionToFinset foCells) > 0

The MS question has positive expected utility value for findChairDP. Learning any FO cell improves decision-making over the prior.

Answer space structure (van Rooij–inspired predicates)

def Phenomena.Questions.Studies.Xiang2022.answersOverlap {W : Type} [BEq (W → Bool)] (q : Core.DecisionTheory.Question W) (worlds : List W) : Bool

Answer cells are not mutually exclusive: some pair of distinct cells shares at least one world.

Equations

• Phenomena.Questions.Studies.Xiang2022.answersOverlap q worlds = List.any q fun (c1 : W → Bool) => List.any q fun (c2 : W → Bool) => !c1 == c2 && worlds.any fun (w : W) => c1 w && c2 w

def Phenomena.Questions.Studies.Xiang2022.notClosedUnderConj {W : Type} (q : Core.DecisionTheory.Question W) (worlds : List W) : Bool

Answer space is not closed under conjunction: some pair of cells has a conjunction that isn't represented by any cell.

Equations

• One or more equations did not get rendered due to their size.

theorem Phenomena.Questions.Studies.Xiang2022.foCells_overlap : answersOverlap foCells allWorlds = true

FO cells overlap: the a-cell and b-cell share world w0.

theorem Phenomena.Questions.Studies.Xiang2022.foCells_not_closed : notClosedUnderConj foCells allWorlds = true

FO cells are not closed under ∧. The conjunction of the a-cell and b-cell is {w0}, which is not one of the two FO cells.

theorem Phenomena.Questions.Studies.Xiang2022.partCells_no_overlap : answersOverlap partCells allWorlds = false

Partition cells don't overlap: they are disjoint.

Part IV: @cite{fox-2018} Exhaustification @cite{fox-2018}

@cite{fox-2018} "Partition by Exhaustification" derives Dayal's EP from the exhaustification operator Exh. We exercise the Bool-valued Exh/IE/MC-set machinery from Questions.Exhaustivity on three question denotations:

1. FO cells {◇a, ◇b}: Exh identifies {w1} and {w2} but not {w0}. No unique cell-identifier at w0 → foxAns undefined → FO alone cannot derive MS (consistent with Fox's argument that higher-order quantification is needed).

2. HO cells {◇a, ◇b, ◇a∨◇b}: Fox's higher-order reading (Section 4.3). Exh(◇a∨◇b) = ◇a∨◇b (IE = ∅ since the two MC-sets {◇a} and {◇b} have empty intersection). At w0, this is the unique Exh-true cell, and both ◇a and ◇b entail ◇a∨◇b, so foxAns = 3 → MS.

3. Partition cells: trivially foxAns = 1 → MA.

Higher-order question denotation (@cite{fox-2018}, Section 4.3)

def Phenomena.Questions.Studies.Xiang2022.hoCells : List (XW → Bool)

Higher-order question denotation: adds the disjunctive cell ◇a∨◇b to the FO cells. Under Spector's analysis, the wh-variable ranges over generalized quantifiers, generating compound cells including disjunctions.

Equations

• One or more equations did not get rendered due to their size.

Exh on FO cells

theorem Phenomena.Questions.Studies.Xiang2022.canQ_foxExh_a_w0 : Theories.Semantics.Questions.Exhaustivity.foxExh foCells 0 allWorlds XW.w0 = false

Exh(◇chair(a)) is false at w0: both a and b can chair, so a's exhaustified answer (= only a can chair) doesn't hold at w0.

theorem Phenomena.Questions.Studies.Xiang2022.canQ_foxExh_a_w1 : Theories.Semantics.Questions.Exhaustivity.foxExh foCells 0 allWorlds XW.w1 = true

Exh(◇chair(a)) is true at w1: at w1 only a can chair.

theorem Phenomena.Questions.Studies.Xiang2022.canQ_foxExh_b_w2 : Theories.Semantics.Questions.Exhaustivity.foxExh foCells 1 allWorlds XW.w2 = true

Exh(◇chair(b)) is true at w2: at w2 only b can chair.

theorem Phenomena.Questions.Studies.Xiang2022.canQ_foxNV_a : Theories.Semantics.Questions.Exhaustivity.foxNV foCells 0 allWorlds = true

Exh(◇chair(a)) is satisfiable: true at w1.

theorem Phenomena.Questions.Studies.Xiang2022.canQ_foxNV_b : Theories.Semantics.Questions.Exhaustivity.foxNV foCells 1 allWorlds = true

Exh(◇chair(b)) is satisfiable: true at w2.

theorem Phenomena.Questions.Studies.Xiang2022.canQ_exhTrueCount_w0 : Theories.Semantics.Questions.Exhaustivity.exhTrueCount foCells allWorlds XW.w0 = 0

No Exh-true FO cell at w0: neither exclusive reading holds where both individuals can chair. This is why Fox needs higher-order Q.

theorem Phenomena.Questions.Studies.Xiang2022.canQ_fo_no_partition : Theories.Semantics.Questions.Exhaustivity.foxPartition foCells allWorlds = false

FO cells don't partition: w0 has no Exh-true cell (Schwarzschild test fails).

theorem Phenomena.Questions.Studies.Xiang2022.canQ_fo_foxAns_w0 : Theories.Semantics.Questions.Exhaustivity.foxAns foCells allWorlds XW.w0 = 0

foxAns is undefined for FO cells at w0: no unique cell-identifier (zero Exh-true cells). FO alone cannot derive Fox's MS prediction.

Exh on HO cells (Fox's Section 4.3)

theorem Phenomena.Questions.Studies.Xiang2022.canQ_ho_exh_disj_w0 : Theories.Semantics.Questions.Exhaustivity.foxExh hoCells 2 allWorlds XW.w0 = true

Exh(◇a∨◇b) at w0 under hoQ: the disjunctive cell's IE is empty (MC-sets {◇a} and {◇b} have empty intersection), so Exh(◇a∨◇b) = ◇a∨◇b. True at w0 since both can chair.

theorem Phenomena.Questions.Studies.Xiang2022.canQ_ho_exhTrueCount_w0 : Theories.Semantics.Questions.Exhaustivity.exhTrueCount hoCells allWorlds XW.w0 = 1

At w0 under hoQ, exactly one Exh is true: the disjunctive cell. The individual cells' Exh (= only-a, only-b) are false at w0.

theorem Phenomena.Questions.Studies.Xiang2022.canQ_ho_foxAns_w0 : Theories.Semantics.Questions.Exhaustivity.foxAns hoCells allWorlds XW.w0 = 3

Fox's Ans gives MS for HO cells at w0. The unique cell-identifier is Exh(◇a∨◇b) = ◇a∨◇b. All three Q-members are true at w0 and entail ◇a∨◇b (trivially, since ◇a → ◇a∨◇b and ◇b → ◇a∨◇b). |Ans| = 3 > 1 → mention-some.

This is Fox's key result: the cell-identifier is weaker than the individual true answers, so multiple answers are licensed.

theorem Phenomena.Questions.Studies.Xiang2022.canQ_ho_no_partition : Theories.Semantics.Questions.Exhaustivity.foxPartition hoCells allWorlds = false

HO cells don't partition: at w1 both Exh(◇a) and Exh(◇a∨◇b) are true (Exh(◇a) = {w1}, Exh(◇a∨◇b) = {w0,w1,w2}), so the Schwarzschild test fails. Fox's Ans requires a unique cell-identifier per world; the HO cells with ◇a∨◇b violate this outside w0. This reflects the gap between Fox's conceptual argument for MS and the formal QPM condition.

theorem Phenomena.Questions.Studies.Xiang2022.canQ_ho_foxAns_w1 : Theories.Semantics.Questions.Exhaustivity.foxAns hoCells allWorlds XW.w1 = 0

foxAns is undefined at w1 under HO cells: two Exh-true cells (Exh(◇a) and Exh(◇a∨◇b)), so no unique cell-identifier.

Partition question

theorem Phenomena.Questions.Studies.Xiang2022.partQ_partition : Theories.Semantics.Questions.Exhaustivity.foxPartition partCells allWorlds = true

Partition cells form a proper partition: every world has exactly one Exh-true cell (Schwarzschild test passes).

theorem Phenomena.Questions.Studies.Xiang2022.partQ_foxAns : Theories.Semantics.Questions.Exhaustivity.foxAns partCells allWorlds XW.w0 = 1

Fox's Ans = 1 for partition cells at w0 → mention-all. The unique true cell is the w0-cell; its Exh is itself.

Pointwise NV

theorem Phenomena.Questions.Studies.Xiang2022.canQ_pointwiseNV : Theories.Semantics.Questions.Exhaustivity.pointwiseNV foCells allWorlds XW.w0 = true

Pointwise NV holds for FO cells at w0: each true cell's Exh is satisfiable (though not true at w0 itself).

Cross-framework agreement

theorem Phenomena.Questions.Studies.Xiang2022.canQ_ep_exh_agree_fo : Theories.Semantics.Questions.Exhaustivity.dayalEP (Theories.Semantics.Questions.Exhaustivity.foQDen chairs) abilityMB [XP.a, XP.b] allWorlds XW.w0 = false ∧ Theories.Semantics.Questions.Exhaustivity.foxAns foCells allWorlds XW.w0 = 0

Dayal EP and Fox Exh agree on the FO can-question: EP fails (no strongest answer) and Exh identifies no cell at w0 (no unique cell-identifier). Both frameworks flag that the FO denotation alone cannot resolve the question at w0.

theorem Phenomena.Questions.Studies.Xiang2022.partQ_ep_fox_agree : Theories.Semantics.Questions.Exhaustivity.dayalEP partQDen abilityMB [XW.w0, XW.w1, XW.w2] allWorlds XW.w0 = true ∧ Theories.Semantics.Questions.Exhaustivity.foxAns partCells allWorlds XW.w0 = 1

Dayal EP and Fox Ans agree on MA for partition: EP holds (unique strongest answer) and Fox's |Ans| = 1.

theorem Phenomena.Questions.Studies.Xiang2022.canQ_ho_ms_agree : Theories.Semantics.Questions.Exhaustivity.foxAns hoCells allWorlds XW.w0 = 3 ∧ Theories.Semantics.Questions.Exhaustivity.relExh (Theories.Semantics.Questions.Exhaustivity.foQDen chairs) abilityMB [XP.a, XP.b] allWorlds XW.w0 = true ∧ Core.DecisionTheory.isMentionSome findChairDP {XW.w0, XW.w1, XW.w2} {XP.a, XP.b} foCells = true

Fox's HO reading derives MS: with the higher-order Q (including ◇a∨◇b), foxAns = 3 at w0 — the exhaustification framework predicts mention-some. This agrees with RelExh (which passes for the FO reading) and DecisionTheory.