Exhaustivity — the weak / strong / Dayal / Xiang ladder

@cite{karttunen-1977} @cite{heim-1994} @cite{groenendijk-stokhof-1984} @cite{dayal-1996} @cite{george-2011} @cite{klinedinst-rothschild-2011} @cite{xiang-2022} @cite{fox-2018} @cite{theiler-etal-2018}

The canonical exhaustivity operators on Core.Question W. Different authors over the past 50 years have proposed sibling operators that extract "the answer to Q at the actual world w" with different strength profiles. This file states them in one place, in mathlib-style Prop+Set form (no Bool/List substrate).

The ladder

Given Q : Core.Question W and a world w : W:

• weakAnswer(Q, w) (@cite{heim-1994}, @cite{karttunen-1977}): the intersection of all true alternatives at w. The natural "what σ must entail to count as truly answering Q."

• strongAnswer(Q, w) (@cite{groenendijk-stokhof-1984}, @cite{heim-1994}): the set of worlds that agree with w on every alternative. Equivalent to MentionAll evaluated at w on partition questions.

• dayalAns(Q, w) (@cite{dayal-1996}): when defined, the unique strongest true alternative — the proposition p ∈ alt Q such that w ∈ p and p ⊆ q for every other true alternative q. Returns Option (Set W); existence is Dayal's Exhaustivity Presupposition (IsExhaustivelyResolvable).

• relExh(Q, w, M) (@cite{xiang-2022} Def 91): exhaustivity relativized to a modal base M : Set W. The strongest true answer computed against the M-restricted alternatives.

• intermediateExh (@cite{george-2011}, @cite{klinedinst-rothschild-2011}): weak exhaustivity plus a no-false-positives clause. Stub.

• foxExhaustifiedAnswer(Q, w) (@cite{fox-2018}): the answer derived by applying the exhaustification operator Exh to alternatives. Stub.

Weak exhaustivity (Heim 1994 / Karttunen 1977)

def Semantics.Questions.Exhaustivity.weakAnswer {W : Type u} (Q : Core.Question W) (w : W) : Set W

Weak exhaustive answer: the set of worlds that lie in every true alternative at w (⋂ {p ∈ alt Q | w ∈ p}). A state σ "weakly answers" Q at w iff σ ⊆ weakAnswer Q w.

Equations

• Semantics.Questions.Exhaustivity.weakAnswer Q w = {v : W | ∀ p ∈ Q.alt, w ∈ p → v ∈ p}

Strong exhaustivity (Groenendijk-Stokhof 1984 / Heim 1994)

def Semantics.Questions.Exhaustivity.strongAnswer {W : Type u} (Q : Core.Question W) (w : W) : Set W

Strong exhaustive answer: the set of worlds that decide every alternative the same way as w.

Equations

• Semantics.Questions.Exhaustivity.strongAnswer Q w = {v : W | ∀ p ∈ Q.alt, w ∈ p ↔ v ∈ p}

def Semantics.Questions.Exhaustivity.IsStronglyExhaustiveAnswer {W : Type u} (σ : Set W) (Q : Core.Question W) (w : W) : Prop

A state σ is the strong-exhaustive answer at w iff σ equals strongAnswer Q w.

Equations

• Semantics.Questions.Exhaustivity.IsStronglyExhaustiveAnswer σ Q w = (σ = Semantics.Questions.Exhaustivity.strongAnswer Q w)

Dayal's strongest-true answer (@cite{dayal-1996})

def Semantics.Questions.Exhaustivity.trueAlternatives {W : Type u} (Q : Core.Question W) (w : W) : Set (Set W)

True alternatives at w: alternatives of Q that contain w.

Equations

• Semantics.Questions.Exhaustivity.trueAlternatives Q w = {p : Set W | p ∈ Q.alt ∧ w ∈ p}

def Semantics.Questions.Exhaustivity.IsStrongestTrueAnswer {W : Type u} (Q : Core.Question W) (w : W) (p : Set W) : Prop

A proposition p is the strongest true answer to Q at w iff p ∈ alt Q, w ∈ p, and p ⊆ q for every other true alternative q. (@cite{dayal-1996} Ans(Q) when defined.)

Equations

• Semantics.Questions.Exhaustivity.IsStrongestTrueAnswer Q w p = (p ∈ Q.alt ∧ w ∈ p ∧ ∀ q ∈ Q.alt, w ∈ q → p ⊆ q)

def Semantics.Questions.Exhaustivity.IsExhaustivelyResolvable {W : Type u} (Q : Core.Question W) (w : W) : Prop

Dayal's Exhaustivity Presupposition (@cite{dayal-1996}): a strongest true answer exists at w.

Equations

• Semantics.Questions.Exhaustivity.IsExhaustivelyResolvable Q w = ∃ (p : Set W), Semantics.Questions.Exhaustivity.IsStrongestTrueAnswer Q w p

noncomputable def Semantics.Questions.Exhaustivity.dayalAns {W : Type u} (Q : Core.Question W) (w : W) : Option (Set W)

Dayal's answer (when EP holds): the unique strongest true alternative at w.

Equations

• Semantics.Questions.Exhaustivity.dayalAns Q w = if h : Semantics.Questions.Exhaustivity.IsExhaustivelyResolvable Q w then some (Classical.choose h) else none

theorem Semantics.Questions.Exhaustivity.dayalAns_isSome_iff_EP {W : Type u} (Q : Core.Question W) (w : W) : (dayalAns Q w).isSome = true ↔ IsExhaustivelyResolvable Q w

dayalAns returns some iff EP holds.

Xiang's relativized exhaustivity (@cite{xiang-2022} Def 91)

def Semantics.Questions.Exhaustivity.trueAlternativesIn {W : Type u} (Q : Core.Question W) (w : W) (M : Set W) : Set (Set W)

True alternatives restricted to a modal base M: alternatives of Q that contain w AND have non-empty intersection with M.

Equations

• Semantics.Questions.Exhaustivity.trueAlternativesIn Q w M = {p : Set W | p ∈ Q.alt ∧ w ∈ p ∧ ∃ v ∈ M, v ∈ p}

def Semantics.Questions.Exhaustivity.IsStrongestRelTrueAnswer {W : Type u} (Q : Core.Question W) (w : W) (M p : Set W) : Prop

A proposition p is the strongest true answer relative to modal base M at w: p ∈ alt Q, w ∈ p, intersects M, and M-entails every other M-true alternative.

Equations

• Semantics.Questions.Exhaustivity.IsStrongestRelTrueAnswer Q w M p = (p ∈ Q.alt ∧ w ∈ p ∧ (∃ v ∈ M, v ∈ p) ∧ ∀ q ∈ Q.alt, w ∈ q → (∃ v ∈ M, v ∈ q) → p ∩ M ⊆ q ∩ M)

def Semantics.Questions.Exhaustivity.relExh {W : Type u} (Q : Core.Question W) (w : W) (M : Set W) : Prop

Xiang's relExh: relativized exhaustivity at w against modal base M (@cite{xiang-2022} Def 91).

Equations

• Semantics.Questions.Exhaustivity.relExh Q w M = ∃ (p : Set W), Semantics.Questions.Exhaustivity.IsStrongestRelTrueAnswer Q w M p

Bridges

theorem Semantics.Questions.Exhaustivity.stronglyExhaustive_imp_mentionAll {W : Type u} (σ : Set W) (Q : Core.Question W) (w : W) (h : IsStronglyExhaustiveAnswer σ Q w) : Resolution.MentionAll σ Q

A strong-exhaustive answer at w mention-all-answers Q.

theorem Semantics.Questions.Exhaustivity.dayalAns_spec {W : Type u} (Q : Core.Question W) (w : W) (p : Set W) (h : dayalAns Q w = some p) : IsStrongestTrueAnswer Q w p

The Dayal answer is by construction a strongest-true answer when it fires.

Strong ⊆ Weak (the substrate exhaustivity ladder)

theorem Semantics.Questions.Exhaustivity.strongAnswer_subset_weakAnswer {W : Type u} (Q : Core.Question W) (w : W) : strongAnswer Q w ⊆ weakAnswer Q w

The strong-exhaustive answer is contained in the weak-exhaustive answer: any state deciding every alternative the same way as w automatically lies inside every alternative true at w. @cite{heim-1994} §4 / @cite{george-2011} §2.6 substrate fact.

strongAnswer partition properties (@cite{fox-2018} §1.1)

strongAnswer Q : W → Set W partitions W into equivalence classes: v ∈ strongAnswer Q w is the equivalence relation "agrees with w on every alternative of Q". The image Set.range (strongAnswer Q) is what @cite{fox-2018} eq (3) calls the Logical Partition of Q.

@[simp]

theorem Semantics.Questions.Exhaustivity.strongAnswer_self_mem {W : Type u} (Q : Core.Question W) (w : W) : w ∈ strongAnswer Q w

Reflexivity: w decides every alternative the same way as itself.

theorem Semantics.Questions.Exhaustivity.mem_strongAnswer_symm {W : Type u} (Q : Core.Question W) {w v : W} : v ∈ strongAnswer Q w ↔ w ∈ strongAnswer Q v

Symmetry of the underlying equivalence: v ∈ strongAnswer Q w ↔ w ∈ strongAnswer Q v.

theorem Semantics.Questions.Exhaustivity.strongAnswer_trans {W : Type u} (Q : Core.Question W) {w v u : W} (huv : u ∈ strongAnswer Q v) (hvw : v ∈ strongAnswer Q w) : u ∈ strongAnswer Q w

Transitivity: u ∈ strongAnswer Q v and v ∈ strongAnswer Q w implies u ∈ strongAnswer Q w.

theorem Semantics.Questions.Exhaustivity.strongAnswer_eq_or_disjoint {W : Type u} (Q : Core.Question W) (w v : W) : strongAnswer Q w = strongAnswer Q v ∨ Disjoint (strongAnswer Q w) (strongAnswer Q v)

Two strong-answer cells are either equal or disjoint — the equivalence-relation partition property.

@[simp]

theorem Semantics.Questions.Exhaustivity.iUnion_strongAnswer {W : Type u} (Q : Core.Question W) : ⋃ (w : W), strongAnswer Q w = Set.univ

The cells of the strong-answer partition cover W: every world is in some cell (its own).

theorem Semantics.Questions.Exhaustivity.mem_range_strongAnswer_iff {W : Type u} (Q : Core.Question W) (C : Set W) : C ∈ Set.range (strongAnswer Q) ↔ ∃ w ∈ C, C = strongAnswer Q w

The Fox 2018 LogicalPartition characterization: any cell in Set.range (strongAnswer Q) is uniquely determined by any of its elements.

Fox's exhaustification primitives (@cite{fox-2018})

@cite{fox-2018} derives Dayal's exhaustivity presupposition from the demand that question denotations partition the Stalnakerian context-set via point-wise exhaustification of Hamblin alternatives. Two substrate-level primitives:

• exhCell Q p (eq 11): the set of worlds where p is the maximally informative true alternative — i.e., {w | IsStrongestTrueAnswer Q w p}.
• exhaustifiedPartition Q (eq 3): the equivalence-class image Set.range (strongAnswer Q), the "Logical Partition" of Q.

The paper-specific apparatus (Cell Identification, Non-Vacuity, QPM) lives in Phenomena/Questions/Studies/Fox2018.lean; here we expose only the substrate primitives the paper consumes.

def Semantics.Questions.Exhaustivity.exhCell {W : Type u} (Q : Core.Question W) (p : Set W) : Set W

@cite{fox-2018} (eq 11): the Exh-cell of proposition p in question Q — the set of worlds where p is the maximally informative true Hamblin alternative. Identifies a cell of the logical partition by the alt that "Exh-strengthens to it". Substrate identification: {w | IsStrongestTrueAnswer Q w p}.

Equations

• Semantics.Questions.Exhaustivity.exhCell Q p = {w : W | Semantics.Questions.Exhaustivity.IsStrongestTrueAnswer Q w p}

@[simp]

theorem Semantics.Questions.Exhaustivity.mem_exhCell {W : Type u} {Q : Core.Question W} {p : Set W} {w : W} : w ∈ exhCell Q p ↔ IsStrongestTrueAnswer Q w p

theorem Semantics.Questions.Exhaustivity.exhCell_subset {W : Type u} (Q : Core.Question W) (p : Set W) : exhCell Q p ⊆ p

An Exh-cell membership entails the world is in the alternative.

def Semantics.Questions.Exhaustivity.exhaustifiedPartition {W : Type u} (Q : Core.Question W) : Set (Set W)

@cite{fox-2018} (eq 3): the Logical Partition of Q — the image of strongAnswer. Substrate-level: equivalence classes of W under "agreement on every alternative". A partition by strongAnswer_eq_or_disjoint and iUnion_strongAnswer.

Equations

• Semantics.Questions.Exhaustivity.exhaustifiedPartition Q = Set.range (Semantics.Questions.Exhaustivity.strongAnswer Q)

@[simp]

theorem Semantics.Questions.Exhaustivity.mem_exhaustifiedPartition {W : Type u} {Q : Core.Question W} {C : Set W} : C ∈ exhaustifiedPartition Q ↔ ∃ (w : W), C = strongAnswer Q w

theorem Semantics.Questions.Exhaustivity.exhaustifiedPartition_nonempty {W : Type u} (Q : Core.Question W) {C : Set W} (h : C ∈ exhaustifiedPartition Q) : C.Nonempty

The exhaustified partition cells are nonempty (each contains its representative world).

theorem Semantics.Questions.Exhaustivity.exhaustifiedPartition_eq_or_disjoint {W : Type u} (Q : Core.Question W) {C₁ C₂ : Set W} (h₁ : C₁ ∈ exhaustifiedPartition Q) (h₂ : C₂ ∈ exhaustifiedPartition Q) : C₁ = C₂ ∨ Disjoint C₁ C₂

Two exhaustified-partition cells are equal or disjoint — direct consequence of strongAnswer_eq_or_disjoint.

@[simp]

theorem Semantics.Questions.Exhaustivity.sUnion_exhaustifiedPartition {W : Type u} (Q : Core.Question W) : ⋃₀ exhaustifiedPartition Q = Set.univ

The exhaustified partition covers W — every world is in its own cell. Direct consequence of iUnion_strongAnswer.

Per-constructor characterizations

theorem Semantics.Questions.Exhaustivity.trueAlternatives_polar_iff_of_nontrivial {W : Type u} (p : Set W) (hne : p ≠ ∅) (hnu : p ≠ Set.univ) (w : W) (q : Set W) : q ∈ trueAlternatives (Core.Question.polar p) w ↔ w ∈ p ∧ q = p ∨ w ∉ p ∧ q = pᶜ

True alternatives of polar p at w: just {p} if w ∈ p, else {pᶜ}. (For nontrivial polar.)

theorem Semantics.Questions.Exhaustivity.weakAnswer_polar_of_pos {W : Type u} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) {w : W} (hwp : w ∈ p) : weakAnswer (Core.Question.polar p) w = p

The weak (Heim/Karttunen) answer to polar p at a p-true world is p itself. (For nontrivial polar.)

theorem Semantics.Questions.Exhaustivity.weakAnswer_polar_of_neg {W : Type u} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) {w : W} (hwp : w ∉ p) : weakAnswer (Core.Question.polar p) w = pᶜ

The weak (Heim/Karttunen) answer to polar p at a p-false world is pᶜ. (For nontrivial polar.)

theorem Semantics.Questions.Exhaustivity.strongAnswer_polar_of_pos {W : Type u} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) {w : W} (hwp : w ∈ p) : strongAnswer (Core.Question.polar p) w = p

The strong (G&S) answer to polar p at a p-true world is p itself. (For nontrivial polar.)

theorem Semantics.Questions.Exhaustivity.strongAnswer_polar_of_neg {W : Type u} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) {w : W} (hwp : w ∉ p) : strongAnswer (Core.Question.polar p) w = pᶜ

The strong (G&S) answer to polar p at a p-false world is pᶜ. (For nontrivial polar.)

declarative characterizations

theorem Semantics.Questions.Exhaustivity.weakAnswer_declarative_of_pos {W : Type u} {p : Set W} {w : W} (hwp : w ∈ p) : weakAnswer (Core.Question.declarative p) w = p

The weak answer to a declarative is the proposition itself. The single alt is p; if w ∈ p then weakAnswer = p.

theorem Semantics.Questions.Exhaustivity.strongAnswer_declarative_of_pos {W : Type u} {p : Set W} {w : W} (hwp : w ∈ p) : strongAnswer (Core.Question.declarative p) w = p

The strong answer to a declarative at a p-true world is p.

dayalAns characterizations

theorem Semantics.Questions.Exhaustivity.isExhaustivelyResolvable_polar_of_nontrivial {W : Type u} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) (w : W) : IsExhaustivelyResolvable (Core.Question.polar p) w

For a non-trivial polar question, the existential presupposition is always satisfied: at any world, exactly one of p, pᶜ is true, and the singleton trivially has a maximum.

theorem Semantics.Questions.Exhaustivity.isStrongestTrueAnswer_polar_of_pos {W : Type u} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) {w : W} (hwp : w ∈ p) : IsStrongestTrueAnswer (Core.Question.polar p) w p

The strongest true answer to polar p at a p-true world is p itself.

theorem Semantics.Questions.Exhaustivity.isStrongestTrueAnswer_polar_of_neg {W : Type u} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) {w : W} (hwp : w ∉ p) : IsStrongestTrueAnswer (Core.Question.polar p) w pᶜ

The strongest true answer to polar p at a p-false world is pᶜ.

Decidability for polar EP

For nontrivial polar questions, IsExhaustivelyResolvable is always true (isExhaustivelyResolvable_polar_of_nontrivial), so the Decidable instance is isTrue. This is the substrate fact that underlies @cite{dayal-1996}'s observation that polar EP is unproblematic — the EP only becomes contentful for wh-questions.

@[implicit_reducible]

instance Semantics.Questions.Exhaustivity.IsExhaustivelyResolvable.decidable_polar {W : Type u} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) (w : W) : Decidable (IsExhaustivelyResolvable (Core.Question.polar p) w)

Equations

• Semantics.Questions.Exhaustivity.IsExhaustivelyResolvable.decidable_polar hne hnu w = isTrue ⋯