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

Formalizes two answerhood notions from @cite{dayal-1996} with increasing strength:

1. Dayal's Ans(Q) with EP (@cite{dayal-1996}): the unique strongest true answer
2. Xiang's Relativized Exhaustivity (@cite{xiang-2022}): EP relative to singleton modal bases

Key Definitions

• trueAnswers: @cite{karttunen-1977}-style answerhood — all true answers (no maximality). This is Dayal's first version of Ans(Q) (p. 87, eq. 47; restated as eq. 47a on p. 116): Ans(Q) = λp [p ∈ Q ∧ ᵛp].
• dayalAns: @cite{dayal-1996}'s Ans(Q) — returns the strongest true answer (if EP holds), implementing the full revised Ans(Q) (p. 116, eq. 47b): Ans(Q) = ιp[p∈Q ∧ ᵛp ∧ ∀p'∈Q [ᵛp' → p ⊆ p']].
• dayalEP: @cite{dayal-1996}'s Exhaustivity Presupposition — defined as (dayalAns ...).isSome so that the equivalence with the existence of a strongest answer is true by construction. Verified as definition 90 in @cite{xiang-2022}.
• dayalAnsProposition: extracts the proposition (W → Bool) from dayalAns.
• relExh: @cite{xiang-2022}'s Relativized Exhaustivity. Verified as definition 91 in @cite{xiang-2022}.
• toHamblinDen: converts the explicit question representation to a Hamblin.QuestionDen, bridging the parametric interface used here with the Hamblin denotation type from Denotation/Hamblin.lean.

Key Theorems

• dayalAns_implies_ep / ep_implies_dayalAns: dayalAns returns some iff dayalEP holds. Trivial by construction (dayalEP := (dayalAns).isSome).
• dayalAns_eq_conjunction: the strongest answer's proposition is pointwise equivalent to the conjunction of all true answers — connecting Dayal's Ans(Q) to @cite{karttunen-1977}'s complete answer (Answerhood.karttunenCompleteAnswer).
• maximality_strictly_strengthens: having true answers does NOT imply EP (concrete counterexample with incomparable propositions).

Design

All definitions are polymorphic in W (worlds) and P (individuals/answers), taking explicit List W universe parameters for decidable computation via native_decide.

Fox 2018 exhaustification machinery (Exh, IE, MC-sets, foxAns, foxPartition) is in the companion file FoxExhaustification.lean.

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 (@cite{karttunen-1977})

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.

This is @cite{karttunen-1977}-style answerhood — the set of all true answer-propositions with no maximality requirement. Corresponds to Dayal's first version of Ans(Q) (p. 87, eq. 47 in @cite{dayal-1996}; restated as eq. 47a on p. 116), before the maximality revision to dayalAns (p. 116, eq. 47b).

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 Ans(Q)

def Theories.Semantics.Questions.Exhaustivity.dayalAns {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) : Option P

Dayal's Ans(Q) operator (@cite{dayal-1996}, p. 116, eq. 47b): returns the strongest true answer when EP holds.

Ans(Q) = ιp[p∈Q ∧ ᵛp ∧ ∀p'∈Q [ᵛp' → p ⊆ p']]

Returns some α where α is the strongest true answer (its proposition entails every other true answer's proposition), or none if EP fails.

Equations

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

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}, p. 116, eq. 47b). Verified as definition 90 in @cite{xiang-2022}.

EP holds at w iff dayalAns returns a strongest true answer: ∃α ∈ True(w). ∀β ∈ True(w). ⟦α⟧ ⊆ ⟦β⟧

Defined as (dayalAns ...).isSome so that the equivalence between EP and the existence of a strongest answer is true by construction, eliminating the need for separate dayalAns_implies_ep / ep_implies_dayalAns proofs.

Equations

• Theories.Semantics.Questions.Exhaustivity.dayalEP qden mb answers worlds w = (Theories.Semantics.Questions.Exhaustivity.dayalAns qden mb answers worlds w).isSome

def Theories.Semantics.Questions.Exhaustivity.dayalAnsProposition {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) : Option (W → Bool)

Extract the proposition (W → Bool) from dayalAns. When EP holds, this is the strongest true proposition — the one that entails all other true answer-propositions. This is what left-peripheral semantics refers to as "Ans(Q)" in contexts like ◇¬know(x, Ans(Q)).

Equations

• Theories.Semantics.Questions.Exhaustivity.dayalAnsProposition qden mb answers worlds w = Option.map (qden mb) (Theories.Semantics.Questions.Exhaustivity.dayalAns qden mb answers worlds w)

Theorems: dayalAns ↔ dayalEP

theorem Theories.Semantics.Questions.Exhaustivity.dayalAns_implies_ep {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) (α : P) (h : dayalAns qden mb answers worlds w = some α) : dayalEP qden mb answers worlds w = true

If dayalAns returns an answer, then dayalEP holds. Trivial by construction: dayalEP := (dayalAns).isSome.

theorem Theories.Semantics.Questions.Exhaustivity.ep_implies_dayalAns {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) (h : dayalEP qden mb answers worlds w = true) : (dayalAns qden mb answers worlds w).isSome = true

If dayalEP holds, then dayalAns returns some answer. Trivial by construction: dayalEP := (dayalAns).isSome.

theorem Theories.Semantics.Questions.Exhaustivity.dayalAns_eq_conjunction {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) (α : P) (hα : dayalAns qden mb answers worlds w = some α) (v : W) : v ∈ worlds → qden mb α v = (trueAnswers qden mb answers w).all fun (β : P) => qden mb β v

The strongest true answer's proposition is pointwise equivalent to the conjunction of all true answers' propositions.

This connects Dayal's Ans(Q) to @cite{karttunen-1977}'s complete answer (Answerhood.karttunenCompleteAnswer in Answerhood.lean): when EP holds, the strongest true proposition is exactly the conjunction (intersection) of all true propositions over the finite world set.

Forward: α entails every β ∈ True(w), so if α holds at v, all β hold at v. Backward: α ∈ True(w), so if all β hold at v, α holds at v.

Maximality Strictly Strengthens Simple Answerhood

Dayal's maximality clause (EP) is strictly stronger than simple @cite{karttunen-1977}-style answerhood. Having true answers does NOT imply EP: when two answers have incomparable propositions (neither entails the other), both can be true but no single answer is strongest.

This is the core motivation for Dayal's revision from simple Ans(Q) (p. 87, eq. 47 in @cite{dayal-1996}; restated as eq. 47a on p. 116) to maximal Ans(Q) (p. 116, eq. 47b).

theorem Theories.Semantics.Questions.Exhaustivity.maximality_strictly_strengthens : have worlds := [0, 1, 2]; have answers := [0, 1]; have mb := fun (x : Fin 3) => [0, 1, 2]; have qden := fun (x : Fin 3 → List (Fin 3)) (ans : Fin 2) (w : Fin 3) => match ans, w with | ⟨0, isLt⟩, ⟨0, isLt_1⟩ => true | ⟨0, isLt⟩, ⟨1, isLt_1⟩ => true | ⟨1, isLt⟩, ⟨0, isLt_1⟩ => true | ⟨1, isLt⟩, ⟨2, isLt_1⟩ => true | x, x_1 => false; (trueAnswers qden mb answers 0).length > 0 ∧ dayalEP qden mb answers worlds 0 = false

Concrete counterexample: two answers with incomparable propositions. Answer 0 true at worlds {0,1}, answer 1 true at worlds {0,2}. At world 0 both are true (trueAnswers nonempty), but neither entails the other ({0,1} ⊄ {0,2} and {0,2} ⊄ {0,1}), so EP fails.

Hamblin Denotation Conversion

def Theories.Semantics.Questions.Exhaustivity.toHamblinDen {W : Type u_1} {P : Type u_2} [BEq W] (qden : (W → List W) → P → W → Bool) (mb : W → List W) (answers : List P) (worlds : List W) : Semantics.Questions.Hamblin.QuestionDen W

Convert a question given explicitly (answer function + answer list) to a Hamblin.QuestionDen — a set-of-propositions representation.

The resulting Hamblin denotation recognizes a proposition p as an answer iff p agrees pointwise (on worlds) with some qden mb α for α ∈ answers. This bridges the parametric interface used throughout this file with the Hamblin.QuestionDen type from Denotation/Hamblin.lean.

Equations

• Theories.Semantics.Questions.Exhaustivity.toHamblinDen qden mb answers worlds = Semantics.Questions.Hamblin.fromAlternatives (List.map (qden mb) answers) worlds

theorem Theories.Semantics.Questions.Exhaustivity.ep_is_hamblin_presupposition {W : Type u_1} {P : Type u_2} [BEq W] (qden : (W → List W) → P → W → Bool) (mb : W → List W) (answers : List P) (worlds : List W) (w : W) : dayalEP qden mb answers worlds w = true → ∃ (p : W → Bool), Semantics.Questions.Hamblin.isAnswer (toHamblinDen qden mb answers worlds) p = true

dayalEP is a presupposition on the Hamblin denotation: it holds iff the set of true propositions in the Hamblin denotation has a unique minimum (strongest element) under propositional entailment.

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}). Verified as definition 91 in @cite{xiang-2022}.

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.