@cite{groenendijk-stokhof-1984}: Studies on the Semantics of Questions #

@cite{belnap-1982}

Single-paper formalisation of the partition-semantics theorems from @cite{groenendijk-stokhof-1984} (Ch. I), formulated over the GSQuestion W substrate. The substrate primitive ans and its basic algebraic properties live in Core/Question/Partition/Cells.lean; this file owns the paper-anchored theorems about refinement, exhaustivity, and de dicto answers.

Theorems #

wh_refines_polar (p. ~13): a wh-question refines the polar question for any individual in the domain. Knowing the answer to Who walks? determines the answer to Does John walk?.
answerhood_thesis (p. 15): the complete true answer at any index is determined by Q (functionally projected).
ans_situation_dependent: the same question can have different answers at different worlds.
exhaustive_answers: ANS pins down the full extension of the predicate.
nonrigid_may_fail_semantic (p. 27): non-rigid descriptions are not guaranteed to give semantic (partition-based) answers.
refinement_iff_answer_transfer: G&S refinement is equivalent to ANS-transfer between questions.

Wh ↔ polar refinement #

source

theorem Phenomena.Questions.Studies.GroenendijkStokhof1984.wh_refines_polar {W : Type u_1} {E : Type u_2} [DecidableEq E] (domain : List E) (pred : E → W → Bool) (e : E) (he : e ∈ domain) :

have whQ := Semantics.Questions.GSQuestion.ofProject fun (w : W) => List.map (fun (x : E) => pred x w) domain; have polarQ := Semantics.Questions.polarQuestion (pred e); QUD.refines whQ polarQ

Wh-question refines the polar question for any individual in the domain. Core result of @cite{groenendijk-stokhof-1984}: knowing the answer to Who walks? determines the answer to Does John walk? because the full extension determines each individual's value.

Proof: if the lists domain.map (pred · w) and domain.map (pred · v) are equal (same wh-answer), then pred e w = pred e v for any e ∈ domain (same polar answer).

source

theorem Phenomena.Questions.Studies.GroenendijkStokhof1984.wh_ans_determines_polar_ans {W : Type u_1} {E : Type u_2} [DecidableEq E] (domain : List E) (pred : E → W → Bool) (e : E) (he : e ∈ domain) (w v : W) :

have whQ := Semantics.Questions.GSQuestion.ofProject fun (w' : W) => List.map (fun (x : E) => pred x w') domain; QUD.ans whQ w v = true → have polarQ := Semantics.Questions.polarQuestion (pred e); QUD.ans polarQ w v = true

If ANS("Who walks?", i) is known, ANS("Does John walk?", i) is determined. Direct corollary of wh_refines_polar.

source

theorem Phenomena.Questions.Studies.GroenendijkStokhof1984.composed_polar_refines {W : Type u_1} (p1 p2 : W → Bool) :

(QUD.compose (Semantics.Questions.polarQuestion p1) (Semantics.Questions.polarQuestion p2)).refines (Semantics.Questions.polarQuestion p1)

Composed polar questions refine their components.

Answerhood thesis (p. 15) #

source

theorem Phenomena.Questions.Studies.GroenendijkStokhof1984.answerhood_thesis {W : Type u_1} (q : Semantics.Questions.GSQuestion W) (i : W) :

∃ (p : W → Bool), p = QUD.ans q i

@cite{groenendijk-stokhof-1984} p. 15: the complete true answer at any index is determined by Q (functionally projected).

source

theorem Phenomena.Questions.Studies.GroenendijkStokhof1984.ans_situation_dependent {W : Type u_1} (q : Semantics.Questions.GSQuestion W) (w v : W) (hDiff : ¬QUD.r q w v) :

∃ (u : W), QUD.ans q w u ≠ QUD.ans q v u

The same question can have different answers at different indices.

Exhaustivity #

source

theorem Phenomena.Questions.Studies.GroenendijkStokhof1984.exhaustive_answers {W : Type u_1} {E : Type u_2} [DecidableEq E] (domain : List E) (pred : E → W → Bool) (w v : W) :

have q := Semantics.Questions.GSQuestion.ofProject fun (w' : W) => List.map (fun (x : E) => pred x w') domain; QUD.ans q w v = true ↔ ∀ e ∈ domain, pred e w = pred e v

Exhaustive answers: ANS pins down the full extension of the predicate.

De dicto / non-rigid descriptions (p. 27) #

source

def Phenomena.Questions.Studies.GroenendijkStokhof1984.deDictoAnswer {W : Type u_1} {E : Type u_2} [DecidableEq E] (description : W → E) (pred : E → W → Bool) :

W → Bool

De dicto answer via a (possibly non-rigid) description.

Equations

Phenomena.Questions.Studies.GroenendijkStokhof1984.deDictoAnswer description pred w = pred (description w) w

Instances For

source

theorem Phenomena.Questions.Studies.GroenendijkStokhof1984.nonrigid_may_fail_semantic {W : Type u_1} {E : Type u_2} [DecidableEq E] (description : W → E) (hNonrigid : ∃ (w : W) (v : W), description w ≠ description v) :

∃ (pred : E → W → Bool) (q : Semantics.Questions.GSQuestion W) (w : W) (v : W), QUD.r q w v ∧ deDictoAnswer description pred w = true ∧ deDictoAnswer description pred v = false

@cite{groenendijk-stokhof-1984} p. 27: non-rigid descriptions may fail to be semantic answers. For any non-rigid description there exists a predicate and question such that the de dicto answer holds at one world but fails at another world in the same cell — witnessing that de dicto answers are not semantic (partition-based).

Proof: given description w₀ ≠ description v₀, let pred e _ := decide (e = description w₀) and q := QUD.trivial. Then de dicto at w₀ = true (reflexivity) and at v₀ = false (non-rigidity).

The original statement universally quantified pred, which is false — a constant predicate makes de dicto answers trivially uniform. The correct G&S claim is that non-rigid descriptions are not guaranteed to give semantic answers, i.e., there exists a breaking scenario for any non-rigid description.