@cite{dayal-2016}: Questions

@cite{dayal-1994} @cite{dayal-1996} @cite{karttunen-1977} @cite{groenendijk-stokhof-1984}

Single-paper formalisation of the Dayal answerhood operator Ans-D and the existential presupposition (EP) from @cite{dayal-2016}, Questions (Oxford Surveys in Semantics and Pragmatics 4), Chapter 2 §2.2–§2.3. Builds on Dayal's earlier work (@cite{dayal-1994}, @cite{dayal-1996}).

Substrate identification

@cite{dayal-2016} (48a) defines

Ans-D_W (Q) = λw ιp [p_w ∧ p ∈ Q ∧ ∀p' [[p'_w ∧ p' ∈ Q] → p ⊆ p']]

— the maximally-informative true alternative, with ι (iota) the definite-description operator. The iota's definedness condition is the existential presupposition: a unique strongest true answer must exist.

This matches Exhaustivity.IsStrongestTrueAnswer Q w p exactly: p ∈ alt Q ∧ w ∈ p ∧ ∀ q ∈ alt Q, w ∈ q → p ⊆ q. The substrate's dayalAns Q w : Option (Set W) returns some precisely when EP holds (IsExhaustivelyResolvable).

What this file proves

• Identification: AnsD = dayalAns, AnsHS (strong-exhaustivity bridge of (48b)) is the substrate's IsExhaustivelyResolvable-based per-world equivalence.
• §2.2.2 architectural move: Dayal separates the truth requirement from question denotation. Captured by the substrate's Question-vs-trueAlternatives split.
• §2.3.4 EP empirical predictions:
  • (57a): cancelling EP with no one leaves the question itself well-formed (the EP fails post hoc; the question is felicitous). Captured by IsExhaustivelyResolvable_polar_of_nontrivial: polar questions never have EP failure.
  • (57b): a singular wh-question with multiple incomparable true alternatives has no maximally informative answer. EP fails.
• Polar EP: a non-trivial polar question always satisfies EP.

What this file does NOT replicate

• Number sensitivity (§2.3.1–§2.3.3) requires plural / atomic individuals (Sharvy 1980/Link 1983 join semilattice). Deferred to a follow-up that uses Phenomena.Plurality substrate.
• Scope marking (§2.2.2 ex. 33–37) is a syntax-side phenomenon (German was-construction, Hindi-Urdu kyaa); deferred to the Hindi-Urdu fragment + Dayal-2025 study.
• Beck-Rullmann's Ans-BR (§2.3.3 ex. 52) — alternative proposal rejected by Dayal; not formalised.

Substrate identification

noncomputable def Phenomena.Questions.Studies.Dayal2016.AnsD {W : Type u_1} (Q : Core.Question W) (w : W) : Option (Set W)

@cite{dayal-2016} (48a): the maximally informative true answer, when defined. Identified with the substrate's dayalAns.

Equations

• Phenomena.Questions.Studies.Dayal2016.AnsD Q w = Semantics.Questions.Exhaustivity.dayalAns Q w

@[simp]

theorem Phenomena.Questions.Studies.Dayal2016.ansD_eq_dayalAns {W : Type u_1} (Q : Core.Question W) (w : W) : AnsD Q w = Semantics.Questions.Exhaustivity.dayalAns Q w

def Phenomena.Questions.Studies.Dayal2016.AnsDHStrong {W : Type u_1} (Q : Core.Question W) (w w' : W) : Prop

@cite{dayal-2016} (48b): strong-exhaustivity bridge — two worlds map to the same maximally-informative true answer.

Equations

• Phenomena.Questions.Studies.Dayal2016.AnsDHStrong Q w w' = (Phenomena.Questions.Studies.Dayal2016.AnsD Q w = Phenomena.Questions.Studies.Dayal2016.AnsD Q w')

def Phenomena.Questions.Studies.Dayal2016.IsEPSatisfied {W : Type u_1} (Q : Core.Question W) (w : W) : Prop

The existential presupposition of @cite{dayal-2016} (the iota definedness condition of (48a)) — at world w, the question Q has a unique strongest true alternative.

Equations

• Phenomena.Questions.Studies.Dayal2016.IsEPSatisfied Q w = Semantics.Questions.Exhaustivity.IsExhaustivelyResolvable Q w

@[simp]

theorem Phenomena.Questions.Studies.Dayal2016.isEPSatisfied_iff {W : Type u_1} (Q : Core.Question W) (w : W) : IsEPSatisfied Q w ↔ Semantics.Questions.Exhaustivity.IsExhaustivelyResolvable Q w

theorem Phenomena.Questions.Studies.Dayal2016.ansD_isSome_iff_EP {W : Type u_1} (Q : Core.Question W) (w : W) : (AnsD Q w).isSome = true ↔ IsEPSatisfied Q w

§2.2.2 architectural move

@cite{dayal-2016} §2.2.2: Dayal (following @cite{dayal-1994}) separates the truth requirement from the question denotation. Karttunen 1977 hard-wires truth into the question content; G&S 1984 inherits the truth requirement at the partition level. Dayal's move is to keep the denotation Hamblin-style (a set of propositions, no truth filter) and put the truth requirement in the answerhood operator (the λw, ι, ⊆ machinery of Ans-D).

The substrate captures this by keeping alt Q truth-independent and defining dayalAns (= Ans-D) as a separate operation that takes the world w as a parameter. The Karttunen denotation (the file Karttunen1977.lean) is then trueAlternatives Q w — a derived view, not the question itself.

theorem Phenomena.Questions.Studies.Dayal2016.karttunen_view_eq_trueAlternatives {W : Type u_1} (Q : Core.Question W) (w : W) : Semantics.Questions.Exhaustivity.trueAlternatives Q w = {p : Set W | p ∈ Q.alt ∧ w ∈ p}

The Karttunen-style "set of true alternatives" is recovered from the Dayal-style architecture by applying the truth filter to alt Q. The substrate exposes this directly via trueAlternatives.

Polar questions: EP always satisfied

theorem Phenomena.Questions.Studies.Dayal2016.polar_isEPSatisfied {W : Type u_1} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) (w : W) : IsEPSatisfied (Core.Question.polar p) w

A non-trivial polar question never has EP failure: at any world, exactly one of p, pᶜ is true, and that one is trivially the maximally-informative true answer.

theorem Phenomena.Questions.Studies.Dayal2016.isStrongestTrueAnswer_polar_pos {W : Type u_1} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) {w : W} (hwp : w ∈ p) : Semantics.Questions.Exhaustivity.IsStrongestTrueAnswer (Core.Question.polar p) w p

For a p-true world, p itself is a strongest true answer.

theorem Phenomena.Questions.Studies.Dayal2016.isStrongestTrueAnswer_polar_neg {W : Type u_1} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) {w : W} (hwp : w ∉ p) : Semantics.Questions.Exhaustivity.IsStrongestTrueAnswer (Core.Question.polar p) w pᶜ

For a p-false world, pᶜ is a strongest true answer.

§2.3.4 EP empirical predictions

The empirical content is in the failure cases for EP. We capture two: (a) wh-questions with no true witness; (b) singular-wh questions with multiple incomparable true atomic witnesses (where uniqueness fails).

The wh-question-with-no-witness case was already proved as Karttunen1977.karttunen_which_no_witness; here we add the EP-failure view.

theorem Phenomena.Questions.Studies.Dayal2016.ep_fails_when_no_true_alt {W : Type u_1} (Q : Core.Question W) (w : W) (h : ∀ p ∈ Q.alt, w ∉ p) : ¬IsEPSatisfied Q w

@cite{dayal-2016} §2.3.4 (57a) cancellation: when Q has no true alternative at w, the EP fails — the existence presupposition is the load-bearing condition that distinguishes Karttunen's truth-in-denotation from Dayal's truth-in-answerhood-operator.

theorem Phenomena.Questions.Studies.Dayal2016.ep_fails_when_two_incomparable_true_alts {W : Type u_1} (Q : Core.Question W) (w : W) (p₁ p₂ : Set W) (hp₁ : p₁ ∈ Q.alt) (hp₂ : p₂ ∈ Q.alt) (hwp₁ : w ∈ p₁) (hwp₂ : w ∈ p₂) (hp₁_not_sub : ¬p₁ ⊆ p₂) (hp₂_not_sub : ¬p₂ ⊆ p₁) : ¬IsEPSatisfied Q w

@cite{dayal-2016} §2.3.3 (45)/(49)/(51): a singular wh-question with multiple incomparable true atomic witnesses has no maximally-informative answer. EP fails.

Concrete: alternatives are like_w(j, m), like_w(j, s), like_w(j, b). If John likes Mary AND Sue (atomic individuals, incomparable propositions), no single proposition entails the other; iota is undefined.