Answerhood operators on Hamblin sets

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 [Kar77b] set of true members;
• weakAnswer H w, their intersection, the weakly exhaustive answer of [Hei94b] (Ans₁) and [BR99a];
• strongAnswer H w, the worlds deciding every member as w does, the strongly exhaustive answer of [GS84], 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, [Day96]'s maximally informative true member: the least true member under entailment, IsLeast. Its existence is Dayal's existential presupposition IsExhaustivelyResolvable; 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 ([Xia22]), 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, [Day25]'s requirement on the perspectival center of a question;
• exhCell H p, [Fox18]'s cells;
• ofFinset F, a finite family of finite propositions, on which the presuppositions are decidable.

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 [Day16] needs Hamblin sets whose members entail one another, which alt discards.

References

• [Kar77b]
• [GS84]
• [Hei94b]
• [Day96]
• [BR99a]
• [Day16]
• [Day25]
• [Fox18]
• [Xia22]

Karttunen sets and the weak and strong answers

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

The true answers at w are the members of H true at w, the [Kar77b] denotation.

Equations

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

@[simp]

theorem Question.mem_trueAnswers {W : Type u_1} (H : Set (Set W)) (w : W) {p : Set W} : p ∈ trueAnswers H w ↔ p ∈ H ∧ w ∈ p

theorem Question.trueAnswers_subset {W : Type u_1} (H : Set (Set W)) (w : W) : trueAnswers H w ⊆ H

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

The weakly exhaustive answer is the intersection of the true members ([Hei94b]'s Ans₁, [BR99a]'s Ans-BR).

Equations

• Question.weakAnswer H w = ⋂₀ Question.trueAnswers H w

@[simp]

theorem Question.mem_weakAnswer {W : Type u_1} (H : Set (Set W)) (w : W) {v : W} : v ∈ weakAnswer H w ↔ ∀ p ∈ H, w ∈ p → v ∈ p

theorem Question.self_mem_weakAnswer {W : Type u_1} (H : Set (Set W)) (w : W) : w ∈ weakAnswer H w

theorem Question.weakAnswer_subset {W : Type u_1} (H : Set (Set W)) (w : W) {p : Set W} (hp : p ∈ H) (hw : w ∈ p) : weakAnswer H w ⊆ p

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

The strongly exhaustive answer at w is the set of worlds that decide every member of H as w does ([GS84], [Hei94b]'s Ans₂).

Equations

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

@[simp]

theorem Question.mem_strongAnswer {W : Type u_1} (H : Set (Set W)) (w : W) {v : W} : v ∈ strongAnswer H w ↔ ∀ p ∈ H, w ∈ p ↔ v ∈ p

theorem Question.strongAnswer_subset_weakAnswer {W : Type u_1} (H : Set (Set W)) (w : W) : strongAnswer H w ⊆ weakAnswer H w

@[simp]

theorem Question.self_mem_strongAnswer {W : Type u_1} (H : Set (Set W)) (w : W) : w ∈ strongAnswer H w

def Question.partition {W : Type u_1} (H : Set (Set W)) : Setoid W

In the partition of [GS84], two worlds are equivalent when they have the same true members: the kernel of the Karttunen denotation, whose cell [Hei94b]'s generalized analysis has the agent believe.

Equations

• Question.partition H = Setoid.ker (Question.trueAnswers H)

theorem Question.partition_iff {W : Type u_1} {H : Set (Set W)} {v w : W} : (partition H) v w ↔ ∀ p ∈ H, v ∈ p ↔ w ∈ p

theorem Question.partition_eq_iInf {W : Type u_1} (H : Set (Set W)) : partition H = ⨅ p ∈ H, Setoid.polar p

The partition is the meet of the polar questions of the members.

theorem Question.ker_weakAnswer {W : Type u_1} (H : Set (Set W)) : Setoid.ker (weakAnswer H) = partition H

The weak answer determines the true members: a world lies in each one's weak answer and each one's weak answer lies in all of its true members, so [Hei94b]'s Ans₂ on a Hamblin set, the proposition that the weak answer is what it is, is the cell of the partition.

theorem Question.strongAnswer_eq_cell {W : Type u_1} (H : Set (Set W)) (w : W) : strongAnswer H w = (partition H).cell w

The strong answer at w is the cell of w.

theorem Question.classes_partition {W : Type u_1} (H : Set (Set W)) : (partition H).classes = Set.range (strongAnswer H)

theorem Question.strongAnswer_eq_or_disjoint {W : Type u_1} (H : Set (Set W)) (w v : W) : strongAnswer H w = strongAnswer H v ∨ Disjoint (strongAnswer H w) (strongAnswer H v)

Two strong answers are equal or disjoint.

theorem Question.fromSetoid_partition {W : Type u_1} (H : Set (Set W)) : fromSetoid (partition H) = ⨅ p ∈ H, polar p

As an inquisitive question, the partition is the meet of the polar questions of the members: a state resolves it iff it resolves whether each member holds.

theorem Question.completelyAnsweredBy_strongAnswer {W : Type u_1} (w : W) (Q : Question W) : Q.CompletelyAnsweredBy (strongAnswer Q.alt w)

The strongly exhaustive answer to an inquisitive question mention-all answers it.

Dayal's strongest true answer

@[reducible, inline]

abbrev Question.IsStrongestTrueAnswer {W : Type u_1} (H : Set (Set W)) (w : W) (p : Set W) : Prop

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

Equations

• Question.IsStrongestTrueAnswer H w p = IsLeast (Question.trueAnswers H w) p

def Question.IsExhaustivelyResolvable {W : Type u_1} (H : Set (Set W)) (w : W) : Prop

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

Equations

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

theorem Question.isStrongestTrueAnswer_iff {W : Type u_1} (H : Set (Set W)) (w : W) {p : Set W} : IsStrongestTrueAnswer H w p ↔ p ∈ H ∧ p = weakAnswer H w

theorem Question.isExhaustivelyResolvable_iff {W : Type u_1} (H : Set (Set W)) (w : W) : IsExhaustivelyResolvable H w ↔ weakAnswer H w ∈ H

The presupposition holds exactly when the weak answer is itself a member.

theorem Question.IsExhaustivelyResolvable.exists_mem {W : Type u_1} {H : Set (Set W)} {w : W} (h : IsExhaustivelyResolvable H w) : ∃ p ∈ H, w ∈ p

Topical properties

A question as a topical property P : α → Set W, from short answers to propositions ([Xia22]), has the Hamblin set Set.range P, whose true members are the image of the true short answers.

theorem Question.trueAnswers_range {W : Type u_1} {α : Type u_2} (P : α → Set W) (w : W) : trueAnswers (Set.range P) w = P '' {a : α | w ∈ P a}

theorem Question.isExhaustivelyResolvable_range_iff {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

On a topical property, Dayal's presupposition asks for a true short answer whose proposition entails every true one.

theorem Question.isStrongestTrueAnswer_range_iff {W : Type u_1} {α : Type u_2} {P : α → Set W} {a : α} {w : W} : IsStrongestTrueAnswer (Set.range P) w (P a) ↔ w ∈ P a ∧ ∀ (b : α), w ∈ P b → P a ⊆ P b

The proposition of a short answer is the strongest true answer of a topical property when it is true and entails every true one.

theorem Question.isExhaustivelyResolvable_range_iff_exists {W : Type u_1} {α : Type u_2} {P : α → Set W} {w : W} : IsExhaustivelyResolvable (Set.range P) w ↔ ∃ (a : α), IsStrongestTrueAnswer (Set.range P) w (P a)

A topical property has a strongest true answer exactly when the proposition of some short answer is one.

theorem Question.isExhaustivelyResolvable_range_iff_isGreatest {W : Type u_1} {α : Type u_2} [LinearOrder α] {φ : α → Set W} {w : W} (hφ : StrictAnti φ) : IsExhaustivelyResolvable (Set.range φ) w ↔ ∃ (m : α), IsGreatest {d : α | w ∈ φ d} m

On a strictly antitone topical property Dayal's presupposition holds exactly when some degree is the greatest true one.

theorem Question.isExhaustivelyResolvable_range_iff_isLeast {W : Type u_1} {α : Type u_2} [LinearOrder α] {φ : α → Set W} {w : W} (hφ : StrictMono φ) : IsExhaustivelyResolvable (Set.range φ) w ↔ ∃ (m : α), IsLeast {d : α | w ∈ φ d} m

On a strictly monotone topical property Dayal's presupposition holds exactly when some degree is the least true one.

theorem Question.isLeast_singleton {W : Type u_1} (p : Set W) : IsLeast {p} p

theorem Question.isStrongestTrueAnswer_iff_of_antichain {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}

Over an antichain the least true member is the only true member.

theorem Question.isExhaustivelyResolvable_iff_of_antichain {W : Type u_1} (H : Set (Set W)) (w : W) (hH : IsAntichain (fun (x1 x2 : Set W) => x1 ⊆ x2) H) : IsExhaustivelyResolvable H w ↔ ∃ (p : Set W), trueAnswers H w = {p}

theorem Question.isStrongestTrueAnswer_alt_iff {W : Type u_1} (w : W) (Q : Question W) {p : Set W} : IsStrongestTrueAnswer Q.alt w p ↔ trueAnswers Q.alt w = {p}

Over inquisitive alternatives the strongest true answer is the only true alternative.

Knowing the answer

def Question.KnowsAnswer {W : Type u_1} (H : Set (Set W)) (w : W) (Dox : SetRel W W) : Prop

The center knows the answer to H at w: the weak answer holds throughout its doxastic alternatives Dox, [Kar77b]'s meaning postulate for know.

Equations

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

def Question.PossiblyIgnorant {W : Type u_1} (H : Set (Set W)) (c : Set W) (Dox : SetRel W W) : Prop

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

Equations

• Question.PossiblyIgnorant H c Dox = ∃ w ∈ c, ¬Question.KnowsAnswer H w Dox

theorem Question.not_possiblyIgnorant_inter_of_subset {W : Type u_1} {H : Set (Set W)} {c A : Set W} {Dox : SetRel W W} (hA : A ⊆ {w : W | KnowsAnswer H w Dox}) : ¬PossiblyIgnorant H (c ∩ A) Dox

Asserting content that entails the center's knowledge of the answer leaves no world where the requirement holds.

theorem Question.possiblyIgnorant_inter_compl_iff {W : Type u_1} {H : Set (Set W)} {c : Set W} {Dox : SetRel W W} : PossiblyIgnorant H (c ∩ {w : W | KnowsAnswer H w Dox}ᶜ) Dox ↔ PossiblyIgnorant H c Dox

Asserting that the center does not know the answer leaves the requirement to the context.

theorem Question.possiblyIgnorant_inter_union_compl_iff {W : Type u_1} {H : Set (Set W)} {c A : Set W} {Dox : SetRel W W} : PossiblyIgnorant H (c ∩ (A ∪ Aᶜ)) Dox ↔ PossiblyIgnorant H c Dox

Asking whether some content holds leaves the requirement to the context.

theorem Question.knowsAnswer_id {W : Type u_1} {H : Set (Set W)} {w : W} : KnowsAnswer H w SetRel.id

A center whose only doxastic alternative is the actual world knows every answer.

theorem Question.knowsAnswer_univ_iff {W : Type u_1} {H : Set (Set W)} {w : W} : KnowsAnswer H w Set.univ ↔ weakAnswer H w = Set.univ

A center with every world open knows only trivial answers.

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

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

Equations

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

theorem Question.dayalAns_eq_some_iff {W : Type u_1} (H : Set (Set W)) (w : W) {p : Set W} : dayalAns H w = some p ↔ IsStrongestTrueAnswer H w p

theorem Question.dayalAns_isSome_iff {W : Type u_1} (H : Set (Set W)) (w : W) : (dayalAns H w).isSome = true ↔ IsExhaustivelyResolvable H w

theorem Question.dayalAns_eq_none_iff {W : Type u_1} (H : Set (Set W)) (w : W) : dayalAns H w = none ↔ ¬IsExhaustivelyResolvable H w

Resolvability on an information state

def Question.supported {W : Type u_1} (H : Set (Set W)) (s : Set W) : Set (Set W)

The members of H an information state s supports.

Equations

• Question.supported H s = {p : Set W | p ∈ H ∧ s ⊆ p}

@[simp]

theorem Question.mem_supported {W : Type u_1} (H : Set (Set W)) {s p : Set W} : p ∈ supported H s ↔ p ∈ H ∧ s ⊆ p

@[simp]

theorem Question.supported_singleton {W : Type u_1} (H : Set (Set W)) (w : W) : supported H {w} = trueAnswers H w

def Question.IsExhaustivelyResolvableOn {W : Type u_1} (H : Set (Set W)) (s : Set W) : Prop

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.

Equations

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

theorem Question.isExhaustivelyResolvableOn_singleton {W : Type u_1} (H : Set (Set W)) (w : W) : IsExhaustivelyResolvableOn H {w} ↔ IsExhaustivelyResolvable H w

Questions under necessity

def Question.box {W : Type u_1} (H : Set (Set W)) {W' : Type u_2} (R : SetRel W' W) : Set (Set W')

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

Equations

• Question.box H R = R.core '' H

theorem Question.mem_box {W : Type u_1} (H : Set (Set W)) {W' : Type u_2} {R : SetRel W' W} {q : Set W'} : q ∈ box H R ↔ ∃ p ∈ H, R.core p = q

theorem Question.isExhaustivelyResolvable_box_iff {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

Necessity lifts the presupposition: □Q is resolvable at x iff Q is resolvable on the worlds accessible from x, provided every world is the sole world accessible from some x.

Cells ([Fox18])

def Question.exhCell {W : Type u_1} (H : Set (Set W)) (p : Set W) : Set W

The cell of p is the set of worlds where p is the strongest true member.

Equations

• Question.exhCell H p = {w : W | Question.IsStrongestTrueAnswer H w p}

@[simp]

theorem Question.mem_exhCell {W : Type u_1} (H : Set (Set W)) {p : Set W} {w : W} : w ∈ exhCell H p ↔ IsStrongestTrueAnswer H w p

theorem Question.exhCell_subset {W : Type u_1} (H : Set (Set W)) (p : Set W) : exhCell H p ⊆ p

theorem Question.trueAnswers_eq_of_isStrongestTrueAnswer {W : Type u_1} (H : Set (Set W)) (w : W) {p : Set W} (h : IsStrongestTrueAnswer H w p) : trueAnswers H w = {q : Set W | q ∈ H ∧ p ⊆ q}

Where p is the strongest true member, the true members are those p entails.

theorem Question.exhCell_eq_strongAnswer {W : Type u_1} (H : Set (Set W)) (w : W) {p : Set W} (h : IsStrongestTrueAnswer H w p) : exhCell H p = strongAnswer H w

The cell of the strongest true member at w is the strong answer at w.

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

Dayal's strong operator Ans-D/H, [Hei94b]'s strengthening of Ans-D, returns the worlds with the same strongest true member as w.

Equations

• Question.dayalStrongAns H w = Option.map (Question.exhCell H) (Question.dayalAns H w)

theorem Question.dayalStrongAns_eq_some_iff {W : Type u_1} (H : Set (Set W)) (w : W) {A : Set W} : dayalStrongAns H w = some A ↔ IsExhaustivelyResolvable H w ∧ A = strongAnswer H w

Where defined, Dayal's strong operator is the Groenendijk–Stokhof answer.

Finite Hamblin sets

A finite family of finite propositions is the carrier on which the presupposition is decidable; ofFinset places it in the Set (Set W) API.

def Question.ofFinset {W : Type u_1} (F : Finset (Finset W)) : Set (Set W)

The Hamblin set of a finite family of finite propositions.

Equations

• Question.ofFinset F = SetLike.coe '' ↑F

@[simp]

theorem Question.mem_ofFinset {W : Type u_1} {F : Finset (Finset W)} {p : Set W} : p ∈ ofFinset F ↔ ∃ q ∈ F, ↑q = p

theorem Question.isExhaustivelyResolvable_ofFinset_iff {W : Type u_1} (F : Finset (Finset W)) (w : W) : IsExhaustivelyResolvable (ofFinset F) w ↔ ∃ p ∈ F, w ∈ p ∧ ∀ q ∈ F, w ∈ q → p ⊆ q

@[instance_reducible]

instance Question.instDecidableIsExhaustivelyResolvableOfFinsetOfDecidableEq {W : Type u_1} [DecidableEq W] (F : Finset (Finset W)) (w : W) : Decidable (IsExhaustivelyResolvable (ofFinset F) w)

Equations

• Question.instDecidableIsExhaustivelyResolvableOfFinsetOfDecidableEq F w = decidable_of_iff (∃ p ∈ F, w ∈ p ∧ ∀ q ∈ F, w ∈ q → p ⊆ q) ⋯

theorem Question.isExhaustivelyResolvableOn_ofFinset_iff {W : Type u_1} (F : Finset (Finset W)) (s : Finset W) : IsExhaustivelyResolvableOn (ofFinset F) ↑s ↔ ∃ p ∈ F, s ⊆ p ∧ ∀ q ∈ F, s ⊆ q → p ⊆ q

@[instance_reducible]

instance Question.instDecidableIsExhaustivelyResolvableOnOfFinsetCoeFinsetOfDecidableEq {W : Type u_1} [DecidableEq W] (F : Finset (Finset W)) (s : Finset W) : Decidable (IsExhaustivelyResolvableOn (ofFinset F) ↑s)

Equations

• Question.instDecidableIsExhaustivelyResolvableOnOfFinsetCoeFinsetOfDecidableEq F s = decidable_of_iff (∃ p ∈ F, s ⊆ p ∧ ∀ q ∈ F, s ⊆ q → p ⊆ q) ⋯

Polar and declarative questions

theorem Question.trueAnswers_polar_of_pos {W : Type u_1} {w : W} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) (hwp : w ∈ p) : trueAnswers (polar p).alt w = {p}

theorem Question.trueAnswers_polar_of_neg {W : Type u_1} {w : W} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) (hwp : w ∉ p) : trueAnswers (polar p).alt w = {pᶜ}

theorem Question.weakAnswer_polar_of_pos {W : Type u_1} {w : W} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) (hwp : w ∈ p) : weakAnswer (polar p).alt w = p

theorem Question.weakAnswer_polar_of_neg {W : Type u_1} {w : W} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) (hwp : w ∉ p) : weakAnswer (polar p).alt w = pᶜ

theorem Question.strongAnswer_polar_of_pos {W : Type u_1} {w : W} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) (hwp : w ∈ p) : strongAnswer (polar p).alt w = p

theorem Question.strongAnswer_polar_of_neg {W : Type u_1} {w : W} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) (hwp : w ∉ p) : strongAnswer (polar p).alt w = pᶜ

theorem Question.isStrongestTrueAnswer_polar_of_pos {W : Type u_1} {w : W} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) (hwp : w ∈ p) : IsStrongestTrueAnswer (polar p).alt w p

theorem Question.isStrongestTrueAnswer_polar_of_neg {W : Type u_1} {w : W} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) (hwp : w ∉ p) : IsStrongestTrueAnswer (polar p).alt w pᶜ

theorem Question.isExhaustivelyResolvable_polar_of_nontrivial {W : Type u_1} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) (w : W) : IsExhaustivelyResolvable (polar p).alt w

A non-trivial polar question always satisfies Dayal's presupposition.

theorem Question.weakAnswer_ofSet_of_pos {W : Type u_1} {p : Set W} {w : W} (hwp : w ∈ p) : weakAnswer (ofSet p).alt w = p

theorem Question.strongAnswer_ofSet_of_pos {W : Type u_1} {p : Set W} {w : W} (hwp : w ∈ p) : strongAnswer (ofSet p).alt w = p