Docs / Semantics / Questions / HamblinSet

Answerhood operators on Hamblin sets

import Linglib.Semantics.Questions.HamblinSet · namespace Question

A Hamblin set H : Set (Set W) is a set of propositions. The theories that take a question to denote such a set locate "the answer at world w" by an operator on the members of H true at w:

trueAnswers H w, the Karttunen 1977 set of true members;
weakAnswer H w, their intersection, the weakly exhaustive answer of Heim 1994 (Ans₁) and Beck & Rullmann 1999;
strongAnswer H w, the worlds deciding every member as w does, the strongly exhaustive answer of Groenendijk & Stokhof 1984, and on a Hamblin set also Heim's Ans₂, since the weak answer determines the true members (ker_weakAnswer);
partition H, the Groenendijk–Stokhof partition as a Setoid, the kernel of trueAnswers H: its cells are the strong answers (strongAnswer_eq_cell), and as an inquisitive question it is the meet of the members' polar questions (fromSetoid_partition);
IsStrongestTrueAnswer H w p, Dayal 1996's maximally informative true member: the least true member under entailment, IsLeast. Its existence is Dayal's existential presupposition IsExhaustivelyResolvable, which holds on the worlds presupposition H; dayalAns returns it and dayalStrongAns applies Heim's strengthening to it;
IsExhaustivelyResolvableOn H s, the presupposition on an information state: a least member the state supports, Dayal's at the singleton {w};
isExhaustivelyResolvable_range_iff, the presupposition on a topical property P : α → Set W from short answers to propositions (Xiang 2022), whose Hamblin set is Set.range P: a true short answer entailing every true one, the maximally informative member of Fox and Hackl, which on a strictly monotone property is the greatest or least true degree (isExhaustivelyResolvable_range_iff_isGreatest);
box H R, the question under necessity, the image of H under SetRel.core R, whose presupposition at a world is the prejacent's on that world's modal base (isExhaustivelyResolvable_box_iff);
KnowsAnswer H w Dox, the center's knowledge of the answer, the box SetRel.core over its doxastic alternatives applied to the weak answer, and PossiblyIgnorant H c Dox, Dayal 2025's requirement on the perspectival center of a question;
KnowsSomeAnswer H w Dox, mention-some knowledge of a true member, which knowing the answer implies when there is a true member and equals on a unique one;
Exhaustification.exh H p, Fox 2018's exhaustification of a member against the question, which holds where the member is the strongest true one (mem_exh_iff_isStrongestTrueAnswer), so that the presupposition holds throughout a set of worlds exactly when exhaustifying members gives each of their cells there (forall_isExhaustivelyResolvable_iff_exh_inter); a strongest true member is never dominated (not_dominated_of_isStrongestTrueAnswer).

The presupposition holds exactly when the weak answer is itself a member (isExhaustivelyResolvable_iff), so Dayal's operator agrees with Heim's and Beck and Rullmann's wherever it is defined, and its strong form agrees with the Groenendijk–Stokhof answer (dayalStrongAns_eq_some_iff). An inquisitive question Q : Question W enters through its alternatives alt Q, an antichain, over which the least true member is the only true member (isStrongestTrueAnswer_iff_of_antichain): the number-sensitive answerhood of Dayal 2016 needs Hamblin sets whose members entail one another, which alt discards.

References

Karttunen 1977, Syntax and Semantics of Questions formalized
Belnap 1982, Questions and Answers in Montague Grammar formalized
Groenendijk & Stokhof 1984, Studies on the Semantics of Questions and the Pragmatics of Answers formalized
Heim 1994, Interrogative Semantics and Karttunen’s Semantics for know
Dayal 1996, Locality in WH Quantification: Questions and Relative Clauses in Hindi
Beck & Rullmann 1999, A Flexible Approach to Exhaustivity in Questions
Dayal 2016, Questions formalized
Dayal 2025, The Interrogative Left Periphery: How a Clause Becomes a Question formalized
Fox 2018, Partition by Exhaustification: Comments on Dayal 1996 formalized
Xiang 2022, Relativized Exhaustivity: Mention-Some and Uniqueness formalized

Karttunen sets and the weak and strong answers

The true answers at w are the members of H true at w, the Karttunen 1977 denotation.

def trueAnswers L91–92

{W : Type u_1} (H : Set (Set W)) (w : W) :

Set (Set W)

trueAnswers H w = {p : Set W | p ∈ H ∧ w ∈ p}

Used by mem_trueAnswers, trueAnswers_subset, iUnion_trueAnswers, weakAnswer, partition, IsStrongestTrueAnswer, trueAnswers_image, trueAnswers_range, isStrongestTrueAnswer_iff_of_antichain, isExhaustivelyResolvable_iff_of_antichain, isStrongestTrueAnswer_alt_iff, KnowsSomeAnswer, KnowsAnswer.knowsSomeAnswer, knowsSomeAnswer_iff_knowsAnswer, supported_singleton, trueAnswers_eq_of_isStrongestTrueAnswer, trueAnswers_polar_of_pos, trueAnswers_polar_of_neg

Used in Belnap1982, Dayal2016, Enguehard2025, George2011, Heim1994b and 3 more

L94–95

L97

L99–102

The weakly exhaustive answer is the intersection of the true members (Heim 1994's Ans₁, Beck & Rullmann 1999's Ans-BR).

def weakAnswer L104–106

{W : Type u_1} (H : Set (Set W)) (w : W) :

Set W

weakAnswer H w = ⋂₀ trueAnswers H w

Built from

Used by mem_weakAnswer, self_mem_weakAnswer, weakAnswer_subset, strongAnswer_subset_weakAnswer, weakAnswer_union_image_compl, ker_weakAnswer, isStrongestTrueAnswer_iff, isExhaustivelyResolvable_iff, KnowsAnswer, knowsAnswer_univ_iff, dayalAns, weakAnswer_polar_of_pos, weakAnswer_polar_of_neg, weakAnswer_ofSet_of_pos

Used in Semantics/Questions/Number, Belnap1982, ElliottNicolaeSauerland2022, George2011, Heim1994b

L108–110

L112

L114–116

The strongly exhaustive answer at w is the set of worlds that decide every member of H as w does (Groenendijk & Stokhof 1984, Heim 1994's Ans₂).

def strongAnswer L118–120

{W : Type u_1} (H : Set (Set W)) (w : W) :

Set W

strongAnswer H w = {v : W | ∀ p ∈ H, w ∈ p ↔ v ∈ p}

Used by mem_strongAnswer, strongAnswer_subset_weakAnswer, self_mem_strongAnswer, weakAnswer_union_image_compl, strongAnswer_eq_cell, classes_partition, strongAnswer_eq_or_disjoint, completelyAnsweredBy_strongAnswer, knowsAnswer_of_mem_core_strongAnswer, exh_eq_strongAnswer, dayalStrongAns_eq_some_iff, forall_isExhaustivelyResolvable_iff_exh_inter, strongAnswer_polar_of_pos, strongAnswer_polar_of_neg, strongAnswer_ofSet_of_pos

Used in Dayal2016, Fox2018, George2011, Heim1994b

In the partition of Groenendijk & Stokhof 1984, two worlds are equivalent when they have the same true members: the kernel of the Karttunen denotation, whose cell Heim 1994's generalized analysis has the agent believe.

def partition L141–144

{W : Type u_1} (H : Set (Set W)) :

Setoid W

partition H = Setoid.ker (trueAnswers H)

Built from

Used by partition_iff, partition_eq_iInf, ker_weakAnswer, strongAnswer_eq_cell, classes_partition, fromSetoid_partition, forall_isExhaustivelyResolvable_iff_classes_subset

Used in Semantics/Questions/Closure, Enguehard2025, GarassinoJacob2018, George2011, GroenendijkStokhof1984 and 1 more

L147–148

L150–152

theorem ker_weakAnswer L154–165

{W : Type u_1} (H : Set (Set W)) :

Setoid.ker (weakAnswer H) = partition H

Built from ,

theorem strongAnswer_eq_cell L167–170

{W : Type u_1} (H : Set (Set W)) (w : W) :

strongAnswer H w = (partition H).cell w

Built from ,

L172–175

L177–179

theorem fromSetoid_partition L181–182

{W : Type u_1} (H : Set (Set W)) :

fromSetoid (partition H) = ⨅ p ∈ H, polar p

Built from

L184–189

Dayal's strongest true answer

A strongest true answer at w is a member of H true at w that entails every member true at w, Dayal 1996's maximally informative true member.

@[reducible, inline] abbrev IsStrongestTrueAnswer L193–195

{W : Type u_1} (H : Set (Set W)) (w : W) (p : Set W) :

Prop

IsStrongestTrueAnswer H w p = IsLeast (trueAnswers H w) p

Built from

Used in Semantics/Questions/Closure, AlonsoOvalleRouillard2023, Dayal2016, ElliottNicolaeSauerland2022, Fox2018 and 5 more

Dayal's existential presupposition holds at w when a strongest true member exists.

def IsExhaustivelyResolvable L197–198

{W : Type u_1} (H : Set (Set W)) (w : W) :

Prop

IsExhaustivelyResolvable H w = ∃ (p : Set W), IsStrongestTrueAnswer H w p

Built from

Used in Semantics/Questions/Number, AlonsoOvalleMoghiseh2025b, AlonsoOvalleRouillard2023, Dayal2016, ElliottNicolaeSauerland2022 and 4 more

The worlds where Dayal's existential presupposition holds.

def presupposition L200–201

{W : Type u_1} (H : Set (Set W)) :

Set W

presupposition H = {w : W | IsExhaustivelyResolvable H w}

Built from

Used by mem_presupposition

Used in Semantics/Questions/Closure, Semantics/Questions/Number, AlonsoOvalleMoghiseh2025b, AlonsoOvalleRouillard2023, ElliottNicolaeSauerland2022

L203

L205–212

theorem isExhaustivelyResolvable_iff L214–218

{W : Type u_1} (H : Set (Set W)) (w : W) :

IsExhaustivelyResolvable H w ↔ weakAnswer H w ∈ H

Built from ,

L220–222

Topical properties

A question as a topical property P : α → Set W, from short answers to propositions (Xiang 2022), has the Hamblin set Set.range P, or P '' D over a domain D of short answers, whose true members are the image of the true short answers.

L234–241

L243–245

theorem isExhaustivelyResolvable_range_iff L247–254

{W : Type u_1} {α : Type u_2} (P : α → Set W) (w : W) :

IsExhaustivelyResolvable (Set.range P) w ↔ ∃ (a : α), w ∈ P a ∧ ∀ (b : α), w ∈ P b → P a ⊆ P b

Built from

L256–259

L261–266

theorem isExhaustivelyResolvable_range_iff_isGreatest L272–276

{W : Type u_1} {α : Type u_2} [LinearOrder α] {φ : α → Set W} {w : W} (hφ : StrictAnti φ) :

IsExhaustivelyResolvable (Set.range φ) w ↔ ∃ (m : α), IsGreatest {d : α | w ∈ φ d} m

Built from

L278–281

L287–288

theorem isStrongestTrueAnswer_iff_of_antichain L290–299

{W : Type u_1} (H : Set (Set W)) (w : W) (hH : IsAntichain (fun (x1 x2 : Set W) => x1 ⊆ x2) H) {p : Set W} :

IsStrongestTrueAnswer H w p ↔ trueAnswers H w = {p}

Built from ,

L301–303

L305–307

Knowing the answer

The center knows the answer to H at w when the weak answer holds throughout its doxastic alternatives Dox, Karttunen 1977's meaning postulate for know.

def KnowsAnswer L315–317

{W : Type u_1} (H : Set (Set W)) (w : W) (Dox : SetRel W W) :

Prop

KnowsAnswer H w Dox = (w ∈ Dox.core (weakAnswer H w))

Built from

Used by PossiblyIgnorant, not_possiblyIgnorant_inter_of_subset, possiblyIgnorant_inter_compl_iff, knowsAnswer_id, knowsAnswer_univ_iff, knowsAnswer_of_mem_core_strongAnswer, KnowsAnswer.knowsSomeAnswer, knowsSomeAnswer_iff_knowsAnswer

Used in Dayal2025, GroenendijkStokhof1984, Heim1994b, Karttunen1977

The center knows some answer to H at w when some true member holds throughout its alternatives Dox, the mention-some know of Belnap 1982 and Groenendijk & Stokhof 1984.

def KnowsSomeAnswer L319–321

{W : Type u_1} (H : Set (Set W)) (w : W) (Dox : SetRel W W) :

Prop

KnowsSomeAnswer H w Dox = ∃ p ∈ trueAnswers H w, w ∈ Dox.core p

Built from

Used by knowsSomeAnswer_of_mem, KnowsAnswer.knowsSomeAnswer, knowsSomeAnswer_iff_knowsAnswer

Used in Belnap1982, GroenendijkStokhof1984

The perspectival center is possibly ignorant in the context c when it may not know the answer there, Dayal 2025's requirement on the center of a question.

def PossiblyIgnorant L323–325

{W : Type u_1} (H : Set (Set W)) (c : Set W) (Dox : SetRel W W) :

Prop

PossiblyIgnorant H c Dox = ∃ w ∈ c, ¬KnowsAnswer H w Dox

Built from

Used by not_possiblyIgnorant_inter_of_subset, possiblyIgnorant_inter_compl_iff, possiblyIgnorant_inter_union_compl_iff

Used in Dayal2025

Dayal's answerhood operator Ans-D returns the strongest true member when the presupposition holds.

dayalAns L369–372

noncomputable def Question.dayalAns {W : Type u_1} (H : Set (Set W)) (w : W) :

Option (Set W)

dayalAns H w = if weakAnswer H w ∈ H then some (weakAnswer H w) else none

Built from

Used by dayalAns_eq_some_iff, dayalAns_isSome_iff, dayalAns_eq_none_iff, dayalStrongAns, dayalStrongAns_eq_some_iff_eq_setOf

Used in AlonsoOvalleMoghiseh2025b, Dayal2016

L374–384

L386–388

L390–392

Resolvability on an information state

L396–397

L399

L401–403

Dayal's presupposition holds on an information state when the state supports a least member. On the singleton state {w} it is the presupposition at w.

def IsExhaustivelyResolvableOn L405–407

{W : Type u_1} (H : Set (Set W)) (s : Set W) :

Prop

IsExhaustivelyResolvableOn H s = ∃ (p : Set W), IsLeast (supported H s) p

Built from

Used by isExhaustivelyResolvableOn_singleton, isExhaustivelyResolvable_box_iff

Used in Semantics/Questions/Closure, AlonsoOvalleRouillard2023, ElliottNicolaeSauerland2022

L409–412

Questions under necessity

The question □Q over the accessibility R necessitates every member: it is the image of H under SetRel.core R.

def box L416–418

{W : Type u_1} (H : Set (Set W)) {W' : Type u_2} (R : SetRel W' W) :

Set (Set W')

box H R = R.core '' H

Used by mem_box, isExhaustivelyResolvable_box_iff

Used in AlonsoOvalleMoghiseh2025b, Fox2018

L420–421

theorem isExhaustivelyResolvable_box_iff L423–439

{W : Type u_1} (H : Set (Set W)) {W' : Type u_2} {R : SetRel W' W} (hR : ∀ (v : W), ∃ (x : W'), ∀ (u : W), (x, u) ∈ R ↔ u = v) {x : W'} {s : Set W} (hs : ∀ (v : W), (x, v) ∈ R ↔ v ∈ s) :

IsExhaustivelyResolvable (box H R) x ↔ IsExhaustivelyResolvableOn H s

Built from , ,

Exhaustification ([Fox18])

Exhaustifying a member p against H, Exhaustification.exh H p, asserts p and denies every member p does not entail. On a member it holds exactly where p is the strongest true member, so it is a cell of the partition.

L447–449

A member exhaustified against the question holds where it is the strongest true member: Fox's Exh(Q, p) is the set of worlds w with Max_inf(Q, w) = p (Fox 2018, (11), after Dayal 1996's Max_inf).

theorem mem_exh_iff_isStrongestTrueAnswer L452–458