Dayal (2016): Questions

The book's baseline theory, chapter 2, blends the three classic theories of questions into the account the later chapters build on. From Hamblin it keeps the denotation, a set of propositions; from Karttunen the truth requirement, moved out of the denotation into an answerhood operator, because in scope marking (What does John think? Where is Mary?) the second question must contribute its false members too; from Groenendijk and Stokhof strong exhaustiveness, obtained by Heim's device of collecting the worlds with the same answer. Its own contribution is number sensitivity: which woman ranges over the atoms of a Sharvy–Link domain, which women and who over the whole domain, and Ans-D returns the true member that entails every other true member, so a singular question presupposes exactly one witness and a plural one at least one, while Beck and Rullmann's intersection operator, being number-blind, cannot draw the distinction. The same operator makes a polar question with a wh phrase unanswerable, and its existential presupposition is a soft one, deniable only by another speaker, which a cleft turns hard.

We state the scope-marking argument on a two-place model, the number paradigm over any atomistic complete lattice, the polar-wh and Beck–Rullmann comparisons, and check the chapter's judgments.

Implementation notes

• A situation is identified with the plurality the nucleus holds of, so the nucleus proposition for x is Set.Ici x; this builds in the distributivity the chapter's entailments assume (John likes Mary and Betty entails John likes Mary).
• The plurality implicature of a plural wh is a stated felicity condition (Felicitous), not part of Ans-D, as in the chapter.

TODO

• Chapters 3–6: the weak–strong distinction and mention-some answers, pair-list and functional answers, embedded and concealed questions, and weak islands through maximality are not formalized.

References

• V. Dayal, Questions (2016)
• V. Dayal, Locality in WH quantification (1996)
• V. Dayal, Scope marking as indirect wh-dependency (1994)
• L. Karttunen, Syntax and semantics of questions (1977)
• I. Heim, Interrogative semantics and Karttunen's semantics for know (1994)
• J. Groenendijk and M. Stokhof, Studies on the semantics of questions (1984)
• S. Beck and H. Rullmann, A flexible approach to exhaustivity in questions (1999)
• M. Bittner, Cross-linguistic semantics for questions (1998)
• U. Lahiri, Questions and answers in embedded contexts (2002)
• D. Abusch, Presupposition triggering from alternatives (2010)
• L. Karttunen and S. Peters, What indirect questions conventionally implicate (1976)
• R. Sharvy, A more general theory of definite descriptions (1980)
• G. Link, The logical analysis of plurals and mass terms (1983)
• J. Hintikka, Knowledge and belief (1962)

Scope marking (34)–(37): the truth requirement leaves the denotation

inductive Dayal2016.Place : Type

Where Mary may be.

• london : Place
• paris : Place

@[instance_reducible]

instance Dayal2016.instDecidableEqPlace : DecidableEq Place

Equations

• Dayal2016.instDecidableEqPlace x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev Dayal2016.World : Type

A world fixes where Mary is and where John thinks she is.

Equations

• Dayal2016.World = (Dayal2016.Place × Dayal2016.Place)

def Dayal2016.isAt (x : Place) : Set World

The nucleus of Where is Mary?: Mary is at x.

Equations

• Dayal2016.isAt x = {w : Dayal2016.World | w.1 = x}

def Dayal2016.believes : SetRel World World

John's doxastic alternatives: the worlds where Mary is where he thinks she is.

Equations

• Dayal2016.believes = {p : Dayal2016.World × Dayal2016.World | p.2.1 = p.1.2}

def Dayal2016.think (q : Set World) : Set World

John thinks that q: the [Hin62] box over believes.

Equations

• Dayal2016.think q = {w : Dayal2016.World | ModalLogic.Box Dayal2016.believes (fun (x : Dayal2016.World) => x ∈ q) w}

def Dayal2016.whereMary : Set (Set World)

(36a): the Hamblin set of Where is Mary?.

Equations

• Dayal2016.whereMary = Set.range Dayal2016.isAt

def Dayal2016.scopeMarked : Set (Set World)

(34b): What does John think? Where is Mary? — the matrix question quantifies over propositions with whereMary as its restriction, the indirect dependency.

Equations

• Dayal2016.scopeMarked = Dayal2016.think '' Dayal2016.whereMary

def Dayal2016.w₀ : World

Mary is in Paris and John thinks she is in London.

Equations

• Dayal2016.w₀ = (Dayal2016.Place.paris, Dayal2016.Place.london)

theorem Dayal2016.trueAnswers_whereMary : Question.trueAnswers whereMary w₀ = {isAt Place.paris}

(36b)/(37c): the Karttunen set of Where is Mary? at w₀ keeps only the Paris member.

theorem Dayal2016.trueAnswers_scopeMarked : Question.trueAnswers scopeMarked w₀ = {think (isAt Place.london)}

The true members of the scope-marked question at w₀: John's thought about London.

theorem Dayal2016.think_london_mem : think (isAt Place.london) ∈ Question.trueAnswers scopeMarked w₀

(35b): John thinks Mary is in London is a true answer although Mary is in Paris.

theorem Dayal2016.trueAnswers_karttunen_composition : Question.trueAnswers (think '' Question.trueAnswers whereMary w₀) w₀ = ∅

(36): composed from the Karttunen set instead, the question has no true member at w₀.

theorem Dayal2016.dayalAns_scopeMarked : Question.dayalAns scopeMarked w₀ = some (think (isAt Place.london))

(37b): Ans-D returns John's thought about London.

Number (41)–(44), (63): singular which ranges over atoms

def Dayal2016.domain {E : Type u_1} [CompleteLattice E] : Number → Set E

(63): what a wh phrase ranges over — singular which N the atoms, plural which N and number-neutral who and what the whole domain.

Equations

• Dayal2016.domain Number.singular = {a : E | IsAtom a}
• Dayal2016.domain x✝ = {x : E | x ≠ ⊥}

theorem Dayal2016.domain_of_ne_singular {E : Type u_1} [CompleteLattice E] {n : Number} (h : n ≠ Number.singular) : domain n = {x : E | x ≠ ⊥}

def Dayal2016.hamblin {E : Type u_1} [CompleteLattice E] (n : Number) : Set (Set E)

(44)/(63): the Hamblin set of which N / who does John like?: a situation is the plurality John likes, so the member for x is Ici x.

Equations

• Dayal2016.hamblin n = Set.Ici '' Dayal2016.domain n

theorem Dayal2016.trueAnswers_image_Ici {E : Type u_1} [CompleteLattice E] (D : Set E) (w : E) : Question.trueAnswers (Set.Ici '' D) w = Set.Ici '' {x : E | x ∈ D ∧ x ≤ w}

The true members: the domain elements John likes, those below the situation.

theorem Dayal2016.weakAnswer_image_Ici {E : Type u_1} [CompleteLattice E] (D : Set E) (w : E) : Question.weakAnswer (Set.Ici '' D) w = Set.Ici (sSup {x : E | x ∈ D ∧ x ≤ w})

The weak answer over a distributive nucleus names the sum of the true witnesses.

Polar questions with a wh phrase (51)

def Dayal2016.polarWh {E : Type u_1} [CompleteLattice E] (n : Number) : Set (Set E)

(51): Does John like which woman/women? — each member of the Hamblin set and its negation.

Equations

• Dayal2016.polarWh n = Dayal2016.hamblin n ∪ compl '' Dayal2016.hamblin n

theorem Dayal2016.mem_polarWh {E : Type u_1} [CompleteLattice E] {n : Number} {p : Set E} : p ∈ polarWh n ↔ ∃ x ∈ domain n, Set.Ici x = p ∨ (Set.Ici x)ᶜ = p

theorem Dayal2016.not_isExhaustivelyResolvable_polarWh_singular {E : Type u_1} [CompleteLattice E] {a b : E} (ha : IsAtom a) (hb : IsAtom b) (hab : a ≠ b) (w : E) : ¬Question.IsExhaustivelyResolvable (polarWh Number.singular) w

(51b): with two women in the domain the singular polar-wh question has no strongest true member at any situation.

theorem Dayal2016.isExhaustivelyResolvable_polarWh_plural_iff {E : Type u_1} [CompleteLattice E] {a b : E} (ha : IsAtom a) (hb : IsAtom b) (hab : a ≠ b) (w : E) : Question.IsExhaustivelyResolvable (polarWh Number.plural) w ↔ w = ⊤

(51c): with two women in the domain the plural polar-wh question is answerable only when John likes everyone.

theorem Dayal2016.sSup_domain_le {E : Type u_1} [CompleteLattice E] [IsAtomistic E] (n : Number) (w : E) : sSup {x : E | x ∈ domain n ∧ x ≤ w} = w

theorem Dayal2016.weakAnswer_hamblin {E : Type u_1} [CompleteLattice E] [IsAtomistic E] (n : Number) (w : E) : Question.weakAnswer (hamblin n) w = Set.Ici w

(52): the intersection answer names the liked plurality whatever the number of the wh phrase, so Beck and Rullmann's operator cannot see number.

theorem Dayal2016.isExhaustivelyResolvable_hamblin_iff {E : Type u_1} [CompleteLattice E] [IsAtomistic E] (n : Number) (w : E) : Question.IsExhaustivelyResolvable (hamblin n) w ↔ w ∈ domain n

Ans-D is defined at w iff the situation lies in the wh phrase's domain: exactly one atom for a singular wh ((49), (65)), at least one for a plural or neutral one ((50), (66)).

theorem Dayal2016.isExhaustivelyResolvable_singular_iff {E : Type u_1} [CompleteLattice E] [IsAtomistic E] (w : E) : Question.IsExhaustivelyResolvable (hamblin Number.singular) w ↔ IsAtom w

theorem Dayal2016.isExhaustivelyResolvable_plural_iff {E : Type u_1} [CompleteLattice E] [IsAtomistic E] (w : E) : Question.IsExhaustivelyResolvable (hamblin Number.plural) w ↔ w ≠ ⊥

theorem Dayal2016.dayalAns_hamblin {E : Type u_1} [CompleteLattice E] [IsAtomistic E] {n : Number} {w : E} (h : w ∈ domain n) : Question.dayalAns (hamblin n) w = some (Set.Ici w)

(49c), (50c), (65b), (66b): the answer names the liked plurality.

theorem Dayal2016.strongAnswer_hamblin {E : Type u_1} [CompleteLattice E] [IsAtomistic E] (n : Number) (w : E) : Question.strongAnswer (hamblin n) w = {w}

The strongly exhaustive answer is the situation itself: Bill saw only w.

theorem Dayal2016.dayalStrongAns_hamblin {E : Type u_1} [CompleteLattice E] [IsAtomistic E] {n : Number} {w : E} (h : w ∈ domain n) : Question.dayalStrongAns (hamblin n) w = some {w}

(65c), (66c): Ans-D/H returns only w.

Felicity (41)–(42), (65)–(66)

def Dayal2016.Felicitous {E : Type u_1} [CompleteLattice E] (n : Number) (w : E) : Prop

A wh question is felicitous in situation w when Ans-D is defined and, for a plural wh, the plurality implicature of its existential presupposition holds.

Equations

• Dayal2016.Felicitous n w = (Question.IsExhaustivelyResolvable (Dayal2016.hamblin n) w ∧ (n = Number.plural → ¬IsAtom w))

theorem Dayal2016.felicitous_singular_iff {E : Type u_1} [CompleteLattice E] [IsAtomistic E] (w : E) : Felicitous Number.singular w ↔ IsAtom w

theorem Dayal2016.felicitous_plural_iff {E : Type u_1} [CompleteLattice E] [IsAtomistic E] (w : E) : Felicitous Number.plural w ↔ w ≠ ⊥ ∧ ¬IsAtom w

theorem Dayal2016.felicitous_general_iff {E : Type u_1} [CompleteLattice E] [IsAtomistic E] (w : E) : Felicitous Number.general w ↔ w ≠ ⊥

theorem Dayal2016.not_felicitous_bot {E : Type u_1} [CompleteLattice E] [IsAtomistic E] (n : Number) : ¬Felicitous n ⊥

(57a), (65)–(66): with no witness no wh question is felicitous; no one is not an answer but a denial of the presupposition.

Beck and Rullmann's intersection on scales (53)

theorem Dayal2016.isStrongestTrueAnswer_range_Iic {α : Type u_1} [Preorder α] (t : α) : Question.IsStrongestTrueAnswer (Set.range Set.Iic) t (Set.Iic t)

(53a)–(53b): on an upward scale (n eggs are sufficient holds at threshold t iff t ≤ n) the member for the threshold is the strongest true member, and Ans-D agrees with the intersection.

theorem Dayal2016.isStrongestTrueAnswer_range_Ici {α : Type u_1} [Preorder α] (c : α) : Question.IsStrongestTrueAnswer (Set.range Set.Ici) c (Set.Ici c)

(53c)–(53d): on a downward scale (n people left holds at count c iff n ≤ c) the member for the count is the strongest true member.

The chapter's women (44), (49)–(52), (65)–(66)

inductive Dayal2016.Woman : Type

The women of (44).

• mary : Woman
• sue : Woman
• betty : Woman

@[instance_reducible]

instance Dayal2016.instDecidableEqWoman : DecidableEq Woman

Equations

• Dayal2016.instDecidableEqWoman x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Dayal2016.instFintypeWoman : Fintype Woman

Equations

• Dayal2016.instFintypeWoman = { elems := { val := ↑Dayal2016.Woman.enumList, nodup := Dayal2016.Woman.enumList_nodup }, complete := Dayal2016.instFintypeWoman._proof_1 }

theorem Dayal2016.ex49 : Question.dayalAns (hamblin Number.singular) {Woman.mary} = some (Set.Ici {Woman.mary})

(49): John likes Mary, and the singular question is answered by John likes Mary.

theorem Dayal2016.ex49_two : ¬Question.IsExhaustivelyResolvable (hamblin Number.singular) {Woman.mary, Woman.sue}

(49): John likes Mary and Sue, and the singular question has no answer.

theorem Dayal2016.ex50 : Question.dayalAns (hamblin Number.plural) {Woman.mary, Woman.betty} = some (Set.Ici {Woman.mary, Woman.betty})

(50): John likes Mary and Betty, and the plural question is answered by the sum.

theorem Dayal2016.ex50_one : Question.dayalAns (hamblin Number.plural) {Woman.mary} = some (Set.Ici {Woman.mary}) ∧ ¬Felicitous Number.plural {Woman.mary}

(50): with only Mary liked the plural question is answered, by an atom, and the plurality implicature fails.

theorem Dayal2016.ex51 : (∀ (w : Set Woman), ¬Question.IsExhaustivelyResolvable (polarWh Number.singular) w) ∧ ∀ (w : Set Woman), Question.IsExhaustivelyResolvable (polarWh Number.plural) w ↔ w = Set.univ

(51): with Mary and Sue in the domain, the singular polar-wh question is never answerable and the plural one only where John likes everyone.

theorem Dayal2016.ex52 : Question.weakAnswer (hamblin Number.singular) {Woman.mary, Woman.sue} = Set.Ici {Woman.mary, Woman.sue} ∧ Set.Ici {Woman.mary, Woman.sue} ∉ hamblin Number.singular

(52): Beck and Rullmann's intersection answers the singular question of (49) with John likes Mary and Sue, a member the singular Hamblin set lacks.

The chapter's judgments

def Dayal2016.number : String → Option Number

The wh phrase of a row.

Equations

• Dayal2016.number "singular" = some Number.singular
• Dayal2016.number "plural" = some Number.plural
• Dayal2016.number "neutral" = some Number.general
• Dayal2016.number x✝ = none

def Dayal2016.situation : String → Option (Finset Woman)

The situation of a row, as the plurality liked or seen.

Equations

• Dayal2016.situation "none" = some ∅
• Dayal2016.situation "one" = some {Dayal2016.Woman.mary}
• Dayal2016.situation "two" = some {Dayal2016.Woman.mary, Dayal2016.Woman.sue}
• Dayal2016.situation x✝ = none

theorem Dayal2016.isAtom_coe_iff (s : Finset Woman) : IsAtom ↑s ↔ s.card = 1

theorem Dayal2016.felicitous_coe_iff (n : Number) (s : Finset Woman) : Felicitous n ↑s ↔ (n = Number.singular → s.card = 1) ∧ (n ≠ Number.singular → s ≠ ∅) ∧ (n = Number.plural → s.card ≠ 1)

@[instance_reducible]

instance Dayal2016.instDecidableFelicitousSetWomanCoeFinset (n : Number) (s : Finset Woman) : Decidable (Felicitous n ↑s)

Equations

• Dayal2016.instDecidableFelicitousSetWomanCoeFinset n s = decidable_of_iff ((n = Number.singular → s.card = 1) ∧ (n ≠ Number.singular → s ≠ ∅) ∧ (n = Number.plural → s.card ≠ 1)) ⋯

theorem Dayal2016.rows_agree (e : Datum) : e ∈ Examples.all → ∀ (n : Number) (s : Finset Woman), (e.feature? "whNumber").bind number = some n → (e.feature? "situation").bind situation = some s → (e.judgment = Judgment.acceptable ↔ Felicitous n ↑s)

(41)–(42), (65)–(66): a question is acceptable in a situation iff the number of its wh phrase fits the plurality.

theorem Dayal2016.existence_rows (e : Datum) : e ∈ Examples.all → ∀ (v : String), e.feature? "existence" = some v → (e.judgment = Judgment.acceptable ↔ e.feature? "cleft" = some "false" ∧ (v = "suspended" ∨ e.feature? "speaker" = some "other"))

(57)–(59): the existential presupposition is denied only across speakers and suspended only without a cleft.