Exhaustivity Presuppositions for Questions @cite{xiang-2022} @cite{dayal-1996}

Formalizes Dayal's Exhaustivity Presupposition (EP, definition 90) and Xiang's Relativized Exhaustivity (RelExh, definition 91) from:

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

Key Definitions

• dayalEP: @cite{dayal-1996}'s Exhaustivity Presupposition — the question presupposes that there exists a strongest true answer (one whose proposition entails all other true answers' propositions).
• relExh: Xiang's Relativized Exhaustivity — EP is evaluated relative to singleton modal bases. For each accessible world v, restrict the modal base to {v} and check EP there. This weakens EP just enough to license mention-some for ability-can questions while preserving mention-all for non-modal and other modal questions.
• foQDen: First-order question denotation (◇φ_x interpretation) — the building block for can-questions where the wh-trace scopes below the modal.

Design

All definitions are polymorphic in W (worlds) and P (individuals/answers), taking explicit List W universe parameters for decidable computation via native_decide. No imports beyond basic Lean — this is pure theory.

Propositional Entailment

def Theories.Semantics.Questions.Exhaustivity.propEntails {W : Type u_1} (p q : W → Bool) (worlds : List W) : Bool

Propositional entailment as Bool: p ⊆ q over a finite universe. propEntails p q worlds = true iff every world where p holds also has q.

Equations

• Theories.Semantics.Questions.Exhaustivity.propEntails p q worlds = worlds.all fun (v : W) => !p v || q v

True Answers

def Theories.Semantics.Questions.Exhaustivity.trueAnswers {W : Type u_1} {P : Type u_2} (qden : (W → List W) → P → W → Bool) (mb : W → List W) (answers : List P) (w : W) : List P

The answers whose denotation is true at world w under modal base mb.

Equations

• Theories.Semantics.Questions.Exhaustivity.trueAnswers qden mb answers w = List.filter (fun (α : P) => qden mb α w) answers

First-Order Question Denotation

def Theories.Semantics.Questions.Exhaustivity.foQDen {W : Type u_1} {P : Type u_2} (pred : W → P → Bool) (mb : W → List W) (α : P) (w : W) : Bool

First-order question denotation: ◇φ_x interpretation.

foQDen pred mb α w = true iff there exists an accessible world v ∈ mb(w) where pred(v, α) holds. This is the denotation for can-questions where the wh-trace takes scope below the modal: ⟦who can VP⟧(mb)(α)(w) = ∃v ∈ mb(w). VP(v)(α)

Equations

• Theories.Semantics.Questions.Exhaustivity.foQDen pred mb α w = (mb w).any fun (v : W) => pred v α

Dayal's Exhaustivity Presupposition

def Theories.Semantics.Questions.Exhaustivity.dayalEP {W : Type u_1} {P : Type u_2} (qden : (W → List W) → P → W → Bool) (mb : W → List W) (answers : List P) (worlds : List W) (w : W) : Bool

Dayal's Exhaustivity Presupposition (@cite{dayal-1996}; @cite{xiang-2022}, definition 90).

EP holds at w iff there exists a true answer α whose proposition entails the proposition of every other true answer β: ∃α ∈ True(w). ∀β ∈ True(w). ⟦α⟧ ⊆ ⟦β⟧

When EP holds, α is the strongest true answer — the exhaustive answer to the question. When EP fails, no single answer subsumes all others, so the question has no well-defined exhaustive reading.

Equations

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

Relativized Exhaustivity

def Theories.Semantics.Questions.Exhaustivity.relExh {W : Type u_1} {P : Type u_2} (qden : (W → List W) → P → W → Bool) (mb : W → List W) (answers : List P) (worlds : List W) (w : W) : Bool

Relativized Exhaustivity (@cite{xiang-2022}, definition 91).

RelExh holds at w iff for every singleton modal base {v} where v ∈ mb(w), if {v} makes some answer relevant (both true under {v} and true under the full mb), then EP holds for {v}: ∀v ∈ mb(w). [∃α. qden({v})(α)(w) ∧ qden(mb)(α)(w)] → EP({v})(w)

The key insight: under a singleton modal base {v}, each individual α either determinately can or determinately cannot VP at v. So for each v, there IS a strongest true answer (trivially — the answers don't overlap when the modal base is a singleton). This means RelExh passes for ability-can questions even when the full EP fails due to overlapping answer propositions.

Equations

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

@cite{fox-2018}: Partition by Exhaustification @cite{fox-2018}

@cite{fox-2018} "Partition by Exhaustification" derives Dayal's EP from the exhaustification operator Exh. The key insight: a question partitions the logical space iff every world has exactly one exhaustified true answer.

The definitions below are Bool-valued analogues of the Prop-valued MC-set/IE machinery in Exhaustification.Basic, specialized to question cells for decidable computation via native_decide.

• cellMCSets mirrors isMCSet from Exhaustification
• cellIE mirrors IE from Exhaustification
• foxExh mirrors exhIE from Exhaustification
• foxAns implements @cite{fox-2018}, definition 35 (answer operator)
• foxPartition implements Schwarzschild's partition test ((38))

def Theories.Semantics.Questions.Exhaustivity.sublists : List Nat → List (List Nat)

All sublists (power set) of a list, preserving order. Used to enumerate candidate MC-sets of cell indices.

Equations

• One or more equations did not get rendered due to their size.
• Theories.Semantics.Questions.Exhaustivity.sublists [] = [[]]

def Theories.Semantics.Questions.Exhaustivity.getCell {W : Type u_1} (cells : List (W → Bool)) (i : Nat) : W → Bool

Safe cell accessor: returns the cell at index i, or (λ _ => false) for OOB.

Equations

• Theories.Semantics.Questions.Exhaustivity.getCell cells i = cells.getD i fun (x : W) => false

def Theories.Semantics.Questions.Exhaustivity.negConsistent {W : Type u_1} (cells : List (W → Bool)) (pIdx : Nat) (excluded : List Nat) (worlds : List W) : Bool

Negation consistency: can cells at excluded indices be simultaneously negated while cell pIdx stays true?

negConsistent cells pIdx excluded worlds = true iff ∃w ∈ worlds. cellspIdx ∧ ∀j ∈ excluded. ¬cellsj

This is the Bool analogue of SetConsistent in Exhaustification, specialized to the pattern φ ∧ ⋀{¬a : a ∈ excluded}.

Equations

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

def Theories.Semantics.Questions.Exhaustivity.cellMCSets {W : Type u_1} (cells : List (W → Bool)) (pIdx : Nat) (worlds : List W) : List (List Nat)

MC-sets (maximal consistent sets) of cell indices for cell pIdx.

A subset S of alternative indices (excluding pIdx) is an MC-set iff:

1. Negating all cells in S is consistent with pIdx being true
2. No proper superset of S is also consistent

Bool analogue of isMCSet in Exhaustification.Basic.

Equations

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

def Theories.Semantics.Questions.Exhaustivity.cellIE {W : Type u_1} (cells : List (W → Bool)) (pIdx : Nat) (worlds : List W) : List Nat

Innocently excludable alternatives for cell pIdx: the indices that appear in every MC-set (intersection of all MC-sets).

Bool analogue of IE in Exhaustification.Basic: IE_(ALT,φ) = {ψ : ψ belongs to every MC_(ALT,φ)-set}

Equations

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

def Theories.Semantics.Questions.Exhaustivity.foxExh {W : Type u_1} (cells : List (W → Bool)) (pIdx : Nat) (worlds : List W) : W → Bool

Fox's exhaustified cell: Exh(Q)(p)(w) = cellspIdx ∧ ∀j ∈ IE. ¬cellsj.

The exhaustified meaning of answer p negates all innocently excludable alternatives. Bool analogue of exhIE in Exhaustification.Basic.

Equations

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

def Theories.Semantics.Questions.Exhaustivity.foxNV {W : Type u_1} (cells : List (W → Bool)) (pIdx : Nat) (worlds : List W) : Bool

Non-vacuity: Exh(Q)(p) is satisfiable (true at some world). @cite{fox-2018} requires non-vacuity for QPM.

Equations

• Theories.Semantics.Questions.Exhaustivity.foxNV cells pIdx worlds = worlds.any (Theories.Semantics.Questions.Exhaustivity.foxExh cells pIdx worlds)

def Theories.Semantics.Questions.Exhaustivity.exhTrueCount {W : Type u_1} (cells : List (W → Bool)) (worlds : List W) (w : W) : Nat

Count of Exh-true cells at world w: the number of cells whose exhaustified meaning holds at w. This is NOT Fox's |Ans| (Definition 35) but a simpler diagnostic: how many exclusive readings are true at w. When = 0, no cell exclusively holds (overlap); when = 1, one cell dominates; when > 1, multiple exclusive readings coexist.

Equations

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

def Theories.Semantics.Questions.Exhaustivity.pointwiseNV {W : Type u_1} (cells : List (W → Bool)) (worlds : List W) (w : W) : Bool

Pointwise non-vacuity: every cell true at w has a satisfiable exhaustified version. This is a necessary condition for Fox's QPM (Definition 34) but weaker — it checks NV for true cells at a single world, while Fox's QPM requires both CI and NV globally over the partition induced by Q.

Equations

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

def Theories.Semantics.Questions.Exhaustivity.foxAns {W : Type u_1} (cells : List (W → Bool)) (worlds : List W) (w : W) : Nat

Fox's answer operator (Definition 35). At world w, finds the unique cell-identifier (the unique j where foxExh(cells, j, worlds)(w) = true) and returns the count of Q-members that are true at w AND whose denotation entails the cell-identifier proposition cells[j].

Fox's (37): Ans(Q)(w) = {q∈Q : w∈q ∧ q ⊆ (ιp∈Q)[Exh(Q,p,w)=1]} The ι picks the unique proposition p whose exhaustification is true at w; the entailment check is q ⊆ p (q entails the proposition p, not Exh(p)).

Returns 0 if no unique cell-identifier exists (zero or multiple Exh-true cells at w). When foxAns > 1, Fox predicts mention-some (the cell-identifier is weaker than individual true answers). When = 1, mention-all (the cell-identifier is the strongest true answer).

Equations

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

def Theories.Semantics.Questions.Exhaustivity.foxPartition {W : Type u_1} (cells : List (W → Bool)) (worlds : List W) : Bool

Schwarzschild's partition test (@cite{fox-2018}, (38)): do the exhaustified cells {Exh(Q)(p) : p ∈ Q} partition the world set? Holds iff every world has exactly one Exh-true cell. When this holds, Fox's QPM (Definition 34) is satisfied and foxAns is well-defined at every world.

Equations

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