[GS84]: Studies on the Semantics of Questions

[Bel82]

Single-paper formalisation of the partition-semantics theorems from [GS84] (Ch. I), formulated over the GSQuestion W substrate. The substrate primitive ans and its basic algebraic properties live in Semantics/Questions/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.

The Ch. VI judgment data (mention-some, pragmatic answerhood, pair-list/choice scope readings) lives as typed LinguisticExample rows in the generated Data.Examples.GroenendijkStokhof1984 module; per-phenomenon accessors are below. TODO: wiring the Italian-newspaper row (gs1984_mentionsome_italian_newspaper) to the MentionSome predicates of Semantics/Questions/Resolution.lean is the genuine future contribution.

Wh ↔ polar refinement

theorem 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 [GS84]: 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).

theorem 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.

theorem 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)

theorem GroenendijkStokhof1984.answerhood_thesis {W : Type u_1} (q : Semantics.Questions.GSQuestion W) (i : W) : ∃ (p : W → Bool), p = QUD.ans q i

[GS84] p. 15: the complete true answer at any index is determined by Q (functionally projected).

theorem 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

theorem 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)

def 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

• GroenendijkStokhof1984.deDictoAnswer description pred w = pred (description w) w

theorem 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

[GS84] 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.

Refinement ↔ answer transfer

theorem GroenendijkStokhof1984.refinement_transfers_answers {W : Type u_1} (q1 q2 : Semantics.Questions.GSQuestion W) (hRefines : QUD.refines q1 q2) (w v : W) : QUD.ans q1 w v = true → QUD.ans q2 w v = true

G&S refinement transfers answers: q1 ⊑ q2 implies that any ans q1-true world v is also ans q2-true.

theorem GroenendijkStokhof1984.answer_transfer_implies_refinement {W : Type u_1} (q1 q2 : Semantics.Questions.GSQuestion W) (hTransfer : ∀ (w v : W), QUD.ans q1 w v = true → QUD.ans q2 w v = true) : QUD.refines q1 q2

Converse: ANS-transfer implies refinement.

theorem GroenendijkStokhof1984.refinement_iff_answer_transfer {W : Type u_1} (q1 q2 : Semantics.Questions.GSQuestion W) : QUD.refines q1 q2 ↔ ∀ (w v : W), QUD.ans q1 w v = true → QUD.ans q2 w v = true

G&S refinement ↔ answer transfer.

Ch. VI example data

def GroenendijkStokhof1984.mentionSomeExamples : List Data.Examples.LinguisticExample

Ch. VI §5 mention-some examples.

Equations

• One or more equations did not get rendered due to their size.

def GroenendijkStokhof1984.pragmaticAnswerhoodExamples : List Data.Examples.LinguisticExample

Ch. VI pragmatic-answerhood examples.

Equations

• One or more equations did not get rendered due to their size.

def GroenendijkStokhof1984.scopeReadingExamples : List Data.Examples.LinguisticExample

Ch. VI §2 scope-reading examples (pair-list and choice).

Equations

• One or more equations did not get rendered due to their size.

theorem GroenendijkStokhof1984.mentionSome_licensor_partition : ((List.filterMap (fun (e : Data.Examples.LinguisticExample) => if (List.lookup "licenses_mention_some" e.paperFeatures == some "false") = true then List.lookup "licensor" e.paperFeatures else none) mentionSomeExamples).eraseDups, (List.filterMap (fun (e : Data.Examples.LinguisticExample) => if (List.lookup "licenses_mention_some" e.paperFeatures == some "true") = true then List.lookup "licensor" e.paperFeatures else none) mentionSomeExamples).eraseDups) = (["depends", "matter", "determine"], ["know", "wonder", "find out"])

Data consistency for the Ch. VI §5.4 verb-licensing rows: the licensors marked as blocking mention-some are exactly depends, matter, determine, and those marked as allowing it are know, wonder, find out — the split the dissertation claims.