def Semantics.Questions.Answerhood.ans {W : Type u_1} (q : GSQuestion W) (i : W) : W → Bool

ANS(Q, i) = cell of Q's partition containing i (@cite{groenendijk-stokhof-1984}, p. 14-15).

Equations

• Semantics.Questions.Answerhood.ans q i w = q.sameAnswer i w

theorem Semantics.Questions.Answerhood.ans_true_at_index {W : Type u_1} (q : GSQuestion W) (i : W) : ans q i i = true

ANS is true at the index of evaluation.

theorem Semantics.Questions.Answerhood.ans_constant_on_cells {W : Type u_1} (q : GSQuestion W) (w v : W) (hEquiv : q.sameAnswer w v = true) (u : W) : ans q w u = ans q v u

Worlds in the same cell get the same ANS.

theorem Semantics.Questions.Answerhood.ans_disjoint {W : Type u_1} (q : GSQuestion W) (w v u : W) (hNotEquiv : q.sameAnswer w v = false) : ¬(ans q w u = true ∧ ans q v u = true)

ANS propositions from different cells are disjoint.

theorem Semantics.Questions.Answerhood.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 := GSQuestion.ofProject fun (w : W) => List.map (fun (x : E) => pred x w) domain; have polarQ := 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).

theorem Semantics.Questions.Answerhood.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 := GSQuestion.ofProject fun (w' : W) => List.map (fun (x : E) => pred x w') domain; ans whQ w v = true → have polarQ := polarQuestion (pred e); ans polarQ w v = true

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

theorem Semantics.Questions.Answerhood.composed_polar_refines {W : Type u_1} (p1 p2 : W → Bool) : (QUD.compose (polarQuestion p1) (polarQuestion p2)).refines (polarQuestion p1)

Composed polar questions refine their components.

def Semantics.Questions.Answerhood.karttunenDenotation {W : Type u_1} {E : Type u_2} [BEq W] (domain : List E) (pred : E → W → Bool) (w : W) (_worlds : List W) : List (W → Bool)

Karttunen denotation: set of true answer-propositions at index w (de re).

Equations

• Semantics.Questions.Answerhood.karttunenDenotation domain pred w _worlds = List.map (fun (e : E) => pred e) (List.filter (fun (x : E) => pred x w) domain)

def Semantics.Questions.Answerhood.karttunenCompleteAnswer {W : Type u_1} {E : Type u_2} [BEq W] (domain : List E) (pred : E → W → Bool) (w : W) (worlds : List W) : W → Bool

Karttunen complete answer: conjunction of all true answer-propositions.

Equations

• Semantics.Questions.Answerhood.karttunenCompleteAnswer domain pred w worlds v = (Semantics.Questions.Answerhood.karttunenDenotation domain pred w worlds).all fun (p : W → Bool) => p v

theorem Semantics.Questions.Answerhood.gs_ans_implies_karttunen {W : Type u_1} {E : Type u_2} [BEq W] [DecidableEq E] (domain : List E) (pred : E → W → Bool) (w : W) (worlds : List W) : have gsQ := GSQuestion.ofProject fun (w' : W) => List.map (fun (x : E) => pred x w') domain; ∀ (v : W), ans gsQ w v = true → karttunenCompleteAnswer domain pred w worlds v = true

G&S ANS implies Karttunen's complete answer (@cite{groenendijk-stokhof-1984}, pp. 53-54). If the full extension matches at v (G&S), then a fortiori the positive extension matches (Karttunen). This is the sound direction: G&S is strictly stronger than Karttunen. Proof: G&S ANS says every entity has the same truth value at w and v. Karttunen only checks entities true at w — which is a subset of "all entities".

theorem Semantics.Questions.Answerhood.karttunen_not_implies_gs : have domain := [true, false]; have pred := fun (e w : Bool) => match e, w with | true, x => true | false, true => false | false, false => true; have w := true; have v := false; karttunenCompleteAnswer domain pred w [w, v] v = true ∧ ans (GSQuestion.ofProject fun (w' : Bool) => List.map (fun (x : Bool) => pred x w') domain) w v = false

The converse fails: Karttunen's complete answer does NOT imply G&S ANS. Karttunen only tracks the positive extension (entities satisfying pred at w), while G&S requires the full extension to match. Counterexample (@cite{groenendijk-stokhof-1984}, pp. 53-54): domain = {john, mary}. At w: john walks, mary doesn't. At v: both walk. Karttunen: true (john walks at v ✓ — all who walk at w also walk at v). G&S: false (extension [T,F] ≠ [T,T] — mary's value differs). This is the central weakness G&S identify in Karttunen's semantics: it only tracks who does φ, not who doesn't.

def Semantics.Questions.Answerhood.karttunenEntails {W : Type u_1} {E : Type u_2} [BEq W] (domain1 : List E) (pred1 : E → W → Bool) (domain2 : List E) (pred2 : E → W → Bool) (worlds : List W) : Prop

Karttunen entailment: denotation inclusion at every index.

Equations

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

theorem Semantics.Questions.Answerhood.karttunen_coordination_problem : have domain := [true, false]; have walk := fun (e w : Bool) => e == w; have talk := fun (e _w : Bool) => e; have w := true; have worlds := [true, false]; (karttunenDenotation domain walk w worlds).length > 0 ∧ (karttunenDenotation domain talk w worlds).length > 0 ∧ ((karttunenDenotation domain walk w worlds).all fun (p : Bool → Bool) => (karttunenDenotation domain talk w worlds).all fun (q : Bool → Bool) => !worlds.all fun (v : Bool) => p v == q v) = true ∧ (QUD.compose (GSQuestion.ofProject fun (w : Bool) => List.map (fun (x : Bool) => walk x w) domain) (GSQuestion.ofProject fun (w : Bool) => List.map (fun (x : Bool) => talk x w) domain)).sameAnswer true false = false

Karttunen's intersection-based coordination fails for questions with different predicates (@cite{groenendijk-stokhof-1984}, Ch. VI §3.1).

Setup: W = {w₁, w₂}, E = {john, mary}. "Who walks?" — john walks at w₁, mary at w₂ (complementary). "Who talks?" — john always talks, mary never talks (constant).

Both Karttunen denotations are non-empty at w₁, but no proposition appears in both: walk(john) = id while talk(john) = const true, so their pointwise intersection is empty.

Meanwhile, G&S partition composition correctly cross-classifies: walkQ distinguishes the two worlds (different extensions), and compose(walkQ, talkQ) inherits this, yielding a non-trivial partition.

This witnesses that Karttunen's approach to question coordination (denotation intersection) is fundamentally broken for multi-predicate coordinations, while G&S's algebraic approach (partition meet) works.

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

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

theorem Semantics.Questions.Answerhood.ans_situation_dependent {W : Type u_1} (q : GSQuestion W) (w v : W) (hDiff : q.sameAnswer w v = false) : ∃ (u : W), ans q w u ≠ ans q v u

The same question can have different answers at different indices.

theorem Semantics.Questions.Answerhood.unique_answer_fallacy {W : Type u_1} (q : GSQuestion W) (w v : W) (hDiff : q.sameAnswer w v = false) : ∃ (u : W), ans q w u ≠ ans q v u

@cite{belnap-1982}'s Unique Answer Fallacy: it is a fallacy to assume that each question has a unique complete true answer. In the G&S framework, ans q w varies with the index w — the same question Q yields different complete true answers at different worlds.

def Semantics.Questions.Answerhood.isPartialAnswer {W : Type u_1} (p : W → Bool) (q : GSQuestion W) (worlds : List W) : Bool

Partial answer: eliminates some cells but not all.

Equations

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

theorem Semantics.Questions.Answerhood.exhaustive_answers {W : Type u_1} {E : Type u_2} [DecidableEq E] (domain : List E) (pred : E → W → Bool) (w v : W) : have q := GSQuestion.ofProject fun (w' : W) => List.map (fun (x : E) => pred x w') domain; ans q w v = true ↔ ∀ e ∈ domain, pred e w = pred e v

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

theorem Semantics.Questions.Answerhood.distributivity_principle {W : Type u_1} {E : Type u_2} [DecidableEq E] (domain : List E) (pred : E → W → Bool) (w : W) (epState : W → Bool) : have q := GSQuestion.ofProject fun (w' : W) => List.map (fun (x : E) => pred x w') domain; (∀ (v : W), epState v = true → ans q w v = true) ↔ ∀ e ∈ domain, ∀ (v : W), epState v = true → pred e v = pred e w

@cite{belnap-1982}'s Distributivity Principle: knowing the answer to a wh-question is equivalent to knowing, for each individual, whether the predicate holds.

An agent whose epistemic state (the set of worlds they consider possible) is epState knows the answer to Q at w iff their state is a subset of ans(Q, w) — i.e., every world they consider possible agrees with w on the full extension of the predicate.

The Distributivity Principle says this is equivalent to knowing each atomic fact: for every entity e in the domain, the agent knows whether pred e holds. This bridges question-embedding ("knows who walks") and propositional attitudes ("knows that John walks ∧ knows that Mary walks ∧ ...").

def Semantics.Questions.Answerhood.failsDistributivityTest {W : Type u_1} (p : W → Bool) (q : GSQuestion W) (w : W) (worlds : List W) : Bool

@cite{belnap-1982}'s Distributivity Test (§2.4, p. 177): a negative criterion for ruling out candidate answers. For any proposition P and indirect question IQ, if the following is consistent:

Sally knows that P, but Sally doesn't know IQ.

then P is NOT an answer to IQ. The test "distributes" the know inside the question and onto its answers: if knowing P doesn't suffice to know IQ, then P doesn't answer IQ.

Formalization: P fails the test for Q at w if there exists an epistemic state (set of worlds the agent considers possible) that is a subset of P (the agent knows P) but NOT a subset of ans(Q, w) (the agent doesn't know Q).

Equations

• Semantics.Questions.Answerhood.failsDistributivityTest p q w worlds = worlds.any fun (v : W) => p v && !Semantics.Questions.Answerhood.ans q w v

theorem Semantics.Questions.Answerhood.passes_test_implies_answer {W : Type u_1} (p : W → Bool) (q : GSQuestion W) (w : W) (worlds : List W) (hPasses : failsDistributivityTest p q w worlds = false) (v : W) : v ∈ worlds → p v = true → ans q w v = true

If P passes the Distributivity Test (no witnessing world exists), then knowing P implies knowing Q — i.e., P is at least as informative as Q w.r.t. the partition. This is the contrapositive of the test.

theorem Semantics.Questions.Answerhood.distributivity_test_examples : have q := QUD.ofProject id; have worlds := [0, 1, 2]; failsDistributivityTest (fun (w : Fin 3) => decide (w = 0)) q 0 worlds = false ∧ failsDistributivityTest (fun (w : Fin 3) => decide (↑w < 2)) q 0 worlds = true

Concrete demonstration of the Distributivity Test.

@cite{belnap-1982}, §2.4, p. 177: "Peter knows that the person who kicked Sam is John, but Peter doesn't know who kicked Sam." This is inconsistent — so the person who kicked Sam is John IS an answer to who kicked Sam.

Vs: "Peter knows that China is populous, but Peter doesn't know which person kicked Sam." This IS consistent — so China is populous is NOT an answer.

We verify on Fin 3 with identity partition (who kicked Sam → full extension):

• "the answer is 0" passes the test (knowing the answer IS knowing the question)
• "w.val < 2" (an irrelevant fact) fails the test

def Semantics.Questions.Answerhood.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

• Semantics.Questions.Answerhood.deDictoAnswer description pred w = pred (description w) w

theorem Semantics.Questions.Answerhood.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 : GSQuestion W) (w : W) (v : W), q.sameAnswer w v = true ∧ deDictoAnswer description pred w = true ∧ deDictoAnswer description pred v = false

Non-rigid descriptions may fail to be semantic answers (@cite{groenendijk-stokhof-1984}, p. 27). 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,_) := (e = description(w₀)) and q := trivial (all worlds equivalent). Then:

• de dicto at w₀ = pred(description(w₀), w₀) = true (reflexivity)
• de dicto at v₀ = pred(description(v₀), v₀) = false (non-rigidity)

N.B. 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.

def Semantics.Questions.Answerhood.gsToHamblin {W : Type u_1} (q : GSQuestion W) (worlds : List W) : Hamblin.QuestionDen W

Convert G&S question to Hamblin denotation.

Equations

• Semantics.Questions.Answerhood.gsToHamblin q worlds p = worlds.any fun (w : W) => worlds.all fun (v : W) => p v == Semantics.Questions.Answerhood.ans q w v

theorem Semantics.Questions.Answerhood.gsToHamblin_recognizes_ans {W : Type u_1} (q : GSQuestion W) (worlds : List W) (w : W) (hw : w ∈ worlds) : gsToHamblin q worlds (ans q w) = true

ANS propositions are recognized by the derived Hamblin denotation. The Hamblin denotation checks: ∃ w' ∈ worlds, ∀ v ∈ worlds, p v == ans q w' v. Taking w' = w gives ans q w v == ans q w v, which is true by refl.

theorem Semantics.Questions.Answerhood.ans_answers {W : Type u_1} (q : GSQuestion W) (i : W) (worlds : List W) (hIn : i ∈ worlds) : answers (ans q i) (q.toQuestion worlds) worlds = true

ANS(Q, i) answers Q in the sense of Basic.answers. Requires i ∈ worlds; otherwise toCells may be empty.

theorem Semantics.Questions.Answerhood.ans_completely_answers {W : Type u_1} (q : GSQuestion W) (i : W) (worlds : List W) (hIn : i ∈ worlds) : completelyAnswers (ans q i) (q.toQuestion worlds) worlds = true

ANS(Q, i) selects exactly one cell (completeness). Uses filter_map_comm to pull the filter through toCells' map, then nodup_filter_eq_singleton to show exactly one representative passes.

theorem Semantics.Questions.Answerhood.complete_not_partial {W : Type u_1} (q : GSQuestion W) (i : W) (worlds : List W) (hIn : i ∈ worlds) : isPartialAnswer (ans q i) q worlds = false

A complete answer is not a partial answer.

theorem Semantics.Questions.Answerhood.partition_cells_are_hamblin_alternatives {W : Type u_1} (q : GSQuestion W) (worlds : List W) (cell : W → Bool) : cell ∈ QUD.toCells q worlds → gsToHamblin q worlds cell = true

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

G&S refinement ↔ ANS-transfer between questions.

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

Converse: ANS-transfer implies refinement.

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

G&S refinement ↔ answer transfer.