Questions/PragmaticAnswerhood.lean

@cite{groenendijk-stokhof-1984}

Pragmatic answerhood theory from @cite{groenendijk-stokhof-1984}, Chapter IV.

Insight

Semantic answerhood is a limit case of pragmatic answerhood. When J = I (total ignorance), pragmatic answerhood reduces to semantic answerhood.

Core Definitions (@cite{groenendijk-stokhof-1984}, pp. 352-358)

Given:

• I = set of all indices (worlds)
• Q = question (partition of I)
• J ⊆ I = information set (questioner's knowledge)
• J/Q = restricted partition = {P ∩ J : P ∈ I/Q, P ∩ J ≠ ∅}

Then:

• Q is a question in J iff ∃X∃Y: X,Y ∈ J/Q ∧ X ≠ Y
• P is a pragmatic answer to Q in J iff P ∩ J ∈ J/Q
• P gives a pragmatic answer to Q in J iff P ∩ J ≠ ∅ ∧ ∃P' ∈ J/Q: P ∩ J ⊆ P'

Term Properties (pragmatic versions)

• Pragmatically exhaustive: like semantic, but quantification restricted to J
• Pragmatically rigid: term denotes same individual across all indices in J
• Pragmatically definite: term picks out unique individual in J

def Semantics.Questions.isPragmaticAnswer {W : Type u_1} (p : W → Bool) (q : GSQuestion W) (j : InfoSet W) (worlds : List W) : Bool

P is a pragmatic answer to Q in J iff P ∩ J is exactly a cell of J/Q.

@cite{groenendijk-stokhof-1984}, p. 352: "P is a pragmatic answer to Q in J iff P ∩ J ∈ J/Q"

This is the strict notion: the intersection must exactly match a cell.

Equations

• Semantics.Questions.isPragmaticAnswer p q j worlds = (q.restrictedCells j worlds).any fun (cell : W → Bool) => worlds.all fun (w : W) => j.intersect p w == cell w

def Semantics.Questions.givesPragmaticAnswer {W : Type u_1} (p : W → Bool) (q : GSQuestion W) (j : InfoSet W) (worlds : List W) : Bool

P gives a pragmatic answer to Q in J iff P ∩ J ⊆ some cell of J/Q.

@cite{groenendijk-stokhof-1984}, p. 352: "P gives a pragmatic answer to Q in J iff P ∩ J ≠ ∅ ∧ ∃P' ∈ J/Q: P ∩ J ⊆ P'"

This is the weaker notion: the intersection is contained in some cell.

Equations

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

theorem Semantics.Questions.isPragmaticAnswer_implies_gives {W : Type u_1} (p : W → Bool) (q : GSQuestion W) (j : InfoSet W) (worlds : List W) : isPragmaticAnswer p q j worlds = true → givesPragmaticAnswer p q j worlds = true

Giving a pragmatic answer is weaker than being a pragmatic answer.

@cite{groenendijk-stokhof-1984}, p. 352: "If P is a pragmatic answer, then P gives a pragmatic answer."

theorem Semantics.Questions.semantic_is_pragmatic_limit {W : Type u_1} (p : W → Bool) (q : GSQuestion W) (worlds : List W) (hNonEmpty : worlds.any p = true) : givesPragmaticAnswer p q totalIgnorance worlds = answers p (q.toQuestion worlds) worlds

theorem Semantics.Questions.pragmaticAnswer_monotone_up {W : Type u_1} (p : W → Bool) (q : GSQuestion W) (j j' : InfoSet W) (worlds : List W) (hSubset : ∀ (w : W), j' w = true → j w = true) (hPinJ' : ∀ (w : W), p w = true → j' w = true) : givesPragmaticAnswer p q j' worlds = true → givesPragmaticAnswer p q j worlds = true

Upward monotonicity of pragmatic answerhood for propositions within J'.

If P gives a pragmatic answer in J' ⊆ J, and P is entirely within J' (every P-world is a J'-world), then P also gives a pragmatic answer in J.

The hypothesis hPinJ' is essential: without it, expanding J can introduce new P-worlds that fall into different cells, breaking containment. For example: W={a,b,c}, Q partitions {a}|{b}|{c}, J'={a,b}, J={a,b,c}, P={a,c}. P gives an answer in J' (P∩J'={a} ⊆ cell {a}) but not in J (P∩J={a,c} straddles cells).

@cite{groenendijk-stokhof-1984}, p. 355: "Reducing the information set cannot make a non-answer into an answer." This holds when P represents the answerer's evidence, which is naturally contained in the current information set.

@[reducible, inline]

abbrev Semantics.Questions.TermDenotation (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A term denotation function: maps indices to individuals.

Equations

• Semantics.Questions.TermDenotation W E = (W → E)

def Semantics.Questions.pragmaticallyRigid {W : Type u_1} {E : Type u_2} [DecidableEq E] (t : TermDenotation W E) (j : InfoSet W) (worlds : List W) : Bool

Pragmatically rigid: term denotes the same individual across all indices in J.

@cite{groenendijk-stokhof-1984}, p. 359: "Your father" is not semantically rigid, but pragmatically rigid for anyone who knows who their father is.

Equations

• Semantics.Questions.pragmaticallyRigid t j worlds = match List.filter j worlds with | [] => true | w :: ws => ws.all fun (v : W) => t w == t v

def Semantics.Questions.semanticallyRigid {W : Type u_1} {E : Type u_2} [DecidableEq E] (t : TermDenotation W E) (worlds : List W) : Bool

Semantically rigid: term denotes the same individual across ALL indices.

@cite{groenendijk-stokhof-1984}: Proper names are semantically rigid. Definite descriptions typically are not.

Equations

• Semantics.Questions.semanticallyRigid t worlds = Semantics.Questions.pragmaticallyRigid t Semantics.Questions.totalIgnorance worlds

def Semantics.Questions.pragmaticallyDefinite {W : Type u_1} {E : Type u_2} [DecidableEq E] (t : TermDenotation W E) (j : InfoSet W) (worlds : List W) : Bool

Pragmatically definite: term picks out a unique individual in J.

@cite{groenendijk-stokhof-1984}, p. 360: An indefinite "an elderly lady wearing glasses" can be pragmatically definite if the questioner's information uniquely identifies the referent.

Equations

• Semantics.Questions.pragmaticallyDefinite t j worlds = decide ((List.map t (List.filter j worlds)).dedup.length ≤ 1)

theorem Semantics.Questions.pragmaticallyRigid_implies_definite {W : Type u_1} {E : Type u_2} [DecidableEq E] (t : TermDenotation W E) (j : InfoSet W) (worlds : List W) : pragmaticallyRigid t j worlds = true → pragmaticallyDefinite t j worlds = true

Pragmatic rigidity implies pragmatic definiteness.

theorem Semantics.Questions.semanticallyRigid_implies_pragmaticallyRigid {W : Type u_1} {E : Type u_2} [DecidableEq E] (t : TermDenotation W E) (j : InfoSet W) (worlds : List W) : semanticallyRigid t worlds = true → pragmaticallyRigid t j worlds = true

Semantic rigidity implies pragmatic rigidity (for any J).

def Semantics.Questions.pragmaticallyExhaustive {W : Type u_1} {E : Type u_2} [DecidableEq E] (t : TermDenotation W E) (predicate : W → E → Bool) (j : InfoSet W) (worlds : List W) : Bool

A term is pragmatically exhaustive for a question Q in J if it picks out all and only the individuals satisfying the question's predicate in J.

@cite{groenendijk-stokhof-1984}, p. 358: Quantification is restricted to J.

Equations

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

theorem Semantics.Questions.exhaustive_rigid_gives_complete_answer {W E : Type} [DecidableEq E] (t : TermDenotation W E) (predicate : W → E → Bool) (j : InfoSet W) (worlds : List W) (_hExh : pragmaticallyExhaustive t predicate j worlds = true) (_hRigid : pragmaticallyRigid t j worlds = true) (hNonEmpty : (worlds.any fun (w : W) => j w && predicate w (t w)) = true) : have answerProp := fun (w : W) => predicate w (t w); have q := GSQuestion.ofPredicate answerProp; givesPragmaticAnswer answerProp q j worlds = true

G&S Theorem (12): If a term t is exhaustive and rigid, then t(a) is a complete answer to "?x.P(x)" in any information set J.

This is the core result connecting term properties to answerhood.

Note: non-emptiness is required — if no J-world satisfies the predicate, the proposition P∩J is empty and cannot be a pragmatic answer.

theorem Semantics.Questions.nonExhaustive_witness {W E : Type} [DecidableEq E] (t : TermDenotation W E) (predicate : W → E → Bool) (j : InfoSet W) (worlds : List W) (hNotExh : pragmaticallyExhaustive t predicate j worlds = false) : ∃ w ∈ List.filter j worlds, predicate w (t w) ≠ (List.filter j worlds).all fun (v : W) => predicate v (t w)

G&S Theorem (17): Non-exhaustive terms cannot completely answer the ORIGINAL question Q (not the derived binary question ofPredicate answerProp).

Note: The original formalization used q = ofPredicate answerProp, which has at most 2 cells and makes answerProp trivially match the "true" cell. This rendered the theorem vacuously false. The correct G&S claim involves an independently given question Q that is FINER than the binary partition, but formalizing this requires additional infrastructure connecting term exhaustiveness to general question partitions.

Instead, we prove a related fact: if a term is not exhaustive, then there exist J-worlds where the term's denotation does not accurately reflect the extension of the predicate.

def Semantics.Questions.requiresSemanticAnswer (_institutionalized : Bool) : Bool

@cite{groenendijk-stokhof-1984}, p. 363, 390: In highly institutionalized settings (courts, etc.), semantic answers are required because information sets vary widely.

Questions are posed on behalf of a social community with diverse information states, so answers must work for many different J. The safest strategy is to use semantically rigid terms.

Equations

• Semantics.Questions.requiresSemanticAnswer _institutionalized = _institutionalized

theorem Semantics.Questions.diverse_audience_prefers_semantic {W : Type u_1} {E : Type u_2} [DecidableEq E] (t : TermDenotation W E) (worlds : List W) : semanticallyRigid t worlds = true → ∀ (j : InfoSet W), pragmaticallyRigid t j worlds = true

The more diverse the audience's information states, the closer answers should stay to semantic answerhood.

@cite{groenendijk-stokhof-1984}, p. 355: "Since we know our information about the information of others to be imperfect, the safest way to answer a question is to stay as close to semantic answers as one can."