Questions/MentionSome.lean

@cite{belnap-1982} @cite{groenendijk-stokhof-1984} @cite{partee-rooth-1983}

Mention-Some Interpretation from @cite{groenendijk-stokhof-1984}, Chapter VI, Section 5.

The Phenomenon

"Where can I buy an Italian newspaper?" can be answered with a single location, even though there may be many places selling Italian newspapers. This is the mention-some reading, in contrast to the mention-all reading that would require listing all such locations.

Section 5.2: Partial Answerhood

G&S first attempt to capture mention-some via partial answerhood (P-ANS):

P-ANS(p, q) ≡ ∃i[p(i) ∧ q(a)(i)] ∧ ¬∀a'∃i[p(i) ≡ q(a')(i)]

However, this fails because negative partial answers satisfy P-ANS but are NOT acceptable mention-some answers:

• Q: "Where is a pen?"
• A: "Not in the drawer" (satisfies P-ANS but doesn't help find a pen)

Section 5.3: The I-MS Rule

The proper treatment requires a special interrogative formation rule:

I-MS: λQ[∃x[β'(x) ∧ Q(λaλi[β'(x) = (λxβ')(a)(i)])]]

This creates a lifted interrogative that takes a property of questions and returns a proposition. The mention-some reading is built into the semantics.

Embedded Mention-Some

Under "know" (extensional): John knows who has a pen =

∃x[has-pen(x) ∧ know*(j, has-pen(x))]

Under "wonder" (intensional): John wonders who has a pen =

want(j, ∃x[has-pen(x) ∧ know*(j, has-pen(x))])

Licensing Factors (Section 5.4)

Mention-some is licensed by:

1. Human concerns (goals the questioner can achieve with partial information)
2. Wide-scope existentials
3. Some verbs block mention-some: "depends", "matter", "determine"

Partial Answerhood

@cite{groenendijk-stokhof-1984}, Section 5.2: A proposition p gives a partial answer to question q if:

1. p is compatible with some cell of q (overlaps with the answer)
2. p is NOT a complete answer (doesn't determine a unique cell)

This captures the intuition that "Not in the drawer" partially answers "Where is the pen?" but fails to capture why it's not a mention-some answer.

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

Partial answerhood: p overlaps with some cell but doesn't determine a unique cell.

@cite{groenendijk-stokhof-1984}, p. 335: P-ANS(p, q) ≡ ∃i[p(i) ∧ q(a)(i)] ∧ ¬∀a'∃i[p(i) ≡ q(a')(i)]

Equations

• Semantics.Questions.MentionSome.partialAnswer p q worlds = (worlds.any p && worlds.any fun (w : W) => worlds.any fun (v : W) => p w && p v && !q.equiv w v)

def Semantics.Questions.MentionSome.isPositivePartialAnswer {E : Type u_1} [BEq E] (answer : E) (satisfiers : List E) : Bool

Positive partial answer: mentions at least one satisfier.

@cite{groenendijk-stokhof-1984}, Section 5.2: The problem with P-ANS is that negative answers like "Not in the drawer" satisfy P-ANS but are NOT acceptable mention-some answers.

Only POSITIVE partial answers (that mention actual satisfiers) count as mention-some.

Equations

• Semantics.Questions.MentionSome.isPositivePartialAnswer answer satisfiers = satisfiers.contains answer

theorem Semantics.Questions.MentionSome.partialAnswer_includes_negative : ∃ (W : Type) (q : GSQuestion W) (worlds : List W) (p : W → Bool), partialAnswer p q worlds = true ∧ ¬(worlds.any p = true ∧ (worlds.all fun (w : W) => p w == true) = true)

Why partial answerhood fails to capture mention-some: Negative answers satisfy P-ANS but shouldn't be mention-some answers.

Example:

• Q: "Where is a pen?"
• "Not in the drawer" - satisfies P-ANS (eliminates some possibilities)
• "In the study" - satisfies P-ANS AND is a proper mention-some answer

The difference: only positive answers that mention actual locations work. This theorem witnesses a negative proposition that satisfies partialAnswer. [sorry: need concrete countermodel with worlds and question]

The I-MS Interrogative Formation Rule

@cite{groenendijk-stokhof-1984}, Section 5.3: The proper treatment of mention-some requires a special interrogative formation rule that creates lifted interrogatives.

Standard I-rule: λQ[∀x[P(x) → Q(x)]]

• Creates partition-based question (mention-all)

I-MS rule: λQ[∃x[β'(x) ∧ Q(λaλi[β'(x) = (λxβ')(a)(i)])]]

• Creates mention-some reading via existential quantification
• Q is a property of questions (type-shifted)
• The result says: "There exists an x satisfying β such that Q holds of the yes/no question 'does x satisfy β?'"

structure Semantics.Questions.MentionSome.MentionSomeInterrogative (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A mention-some interrogative: the semantic structure created by I-MS.

The whDomain lists possible values for the wh-phrase. The abstract β' is the predicate (e.g., "x has a pen" or "x sells newspapers").

• whDomain : List E

  The wh-domain (possible values for the wh-phrase)

• abstract : W → E → Bool

  The wh-abstract β'(w, x): does x satisfy the property in world w?

def Semantics.Questions.MentionSome.yesNoQuestionFor {W : Type u_1} {E : Type u_2} [DecidableEq E] (abstract : W → E → Bool) (x : E) : GSQuestion W

Yes/no question for a specific value: "Does x satisfy β?"

This is the inner question that the I-MS rule applies Q to.

Equations

• Semantics.Questions.MentionSome.yesNoQuestionFor abstract x = Semantics.Questions.GSQuestion.ofPredicate fun (x_1 : W) => abstract x_1 x

def Semantics.Questions.MentionSome.MentionSomeInterrogative.applyToProperty {W : Type u_1} {E : Type u_2} [DecidableEq E] (msi : MentionSomeInterrogative W E) (Q : GSQuestion W → Bool) (w : W) : Bool

The I-MS rule applied to a property of questions.

I-MS: λQ[∃x[β'(x) ∧ Q(λaλi[β'(x) = (λxβ')(a)(i)])]]

Given a property Q of questions (e.g., "John knows the answer to"), this returns true if there exists some x such that:

1. x satisfies β' in the actual world (β'(x))
2. Q holds of the yes/no question "does x satisfy β'?"

Equations

• msi.applyToProperty Q w = msi.whDomain.any fun (x : E) => msi.abstract w x && Q (Semantics.Questions.MentionSome.yesNoQuestionFor msi.abstract x)

Embedded Mention-Some

@cite{groenendijk-stokhof-1984}, Section 5.3: Mention-some questions embedded under attitude verbs:

Under "know" (extensional complement)

"John knows who has a pen" (mention-some) = ∃x[has-pen(x) ∧ know*(j, has-pen(x))]

Paraphrase: "There is someone who has a pen and John knows that they have a pen"

Under "wonder" (intensional complement)

"John wonders who has a pen" (mention-some) = want(j, ∃x[has-pen(x) ∧ know*(j, has-pen(x))])

Paraphrase: "John wants there to be someone who has a pen and whom he knows has a pen" (i.e., John wants to find out about one pen-haver)

def Semantics.Questions.MentionSome.knowMentionSome {W : Type u_1} {E : Type u_2} [DecidableEq E] (msi : MentionSomeInterrogative W E) (knows : W → E → (W → Bool) → Bool) (agent : E) (w : W) : Bool

"Know" embedding of mention-some question (extensional reading).

"John knows who has a pen" (mention-some) = ∃x[has-pen(x) ∧ know*(j, has-pen(x))]

The agent knows the answer iff they know of SOME satisfier that it's a satisfier.

Equations

• Semantics.Questions.MentionSome.knowMentionSome msi knows agent w = msi.whDomain.any fun (x : E) => msi.abstract w x && knows w agent fun (x_1 : W) => msi.abstract x_1 x

def Semantics.Questions.MentionSome.wonderMentionSome {W : Type u_1} {E : Type u_2} [DecidableEq E] (msi : MentionSomeInterrogative W E) (wants knows : W → E → (W → Bool) → Bool) (agent : E) (w : W) : Bool

"Wonder" embedding of mention-some question (intensional reading).

"John wonders who has a pen" (mention-some) = want(j, ∃x[has-pen(x) ∧ know*(j, has-pen(x))])

The agent wonders Q iff they want to know of SOME satisfier that it's a satisfier.

Equations

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

def Semantics.Questions.MentionSome.askMentionSome {W : Type u_1} {E : Type u_2} [DecidableEq E] (msi : MentionSomeInterrogative W E) (asks : W → E → (W → Bool) → Bool) (agent : E) (w : W) : Bool

"Ask" embedding of mention-some question.

"John asked who has a pen" (mention-some): John directed a question at some addressee, wanting to know of some pen-haver.

Equations

• Semantics.Questions.MentionSome.askMentionSome msi asks agent w = asks w agent fun (w' : W) => msi.whDomain.any fun (x : E) => msi.abstract w' x

Distinguishing Choice from Mention-Some

@cite{groenendijk-stokhof-1984}, Section 5.1-5.3: Both choice and mention-some readings yield non-exhaustive answers, but they are semantically distinct:

Choice Reading: The disjunction/existential takes wide scope. "Whom does John or Mary love?" - Answer varies by who the lover is.

Mention-Some Reading: Goal-driven; any satisfier suffices. "Where can I buy coffee?" - Just need one place.

Key difference: Choice involves scope ambiguity; mention-some involves pragmatic goal-based interpretation.

inductive Semantics.Questions.MentionSome.MentionSomeLicensor : Type

What licenses mention-some readings.

• humanConcern : String → MentionSomeLicensor

  Human concern: questioner has a practical goal

• wideExistential : MentionSomeLicensor

  Wide-scope existential: ∃x scopes over ?y

• contextualGoal : MentionSomeLicensor

  Contextual goal makes partial info sufficient

def Semantics.Questions.MentionSome.instReprMentionSomeLicensor.repr : MentionSomeLicensor → ℕ → Std.Format

Equations

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

instance Semantics.Questions.MentionSome.instReprMentionSomeLicensor : Repr MentionSomeLicensor

Equations

• Semantics.Questions.MentionSome.instReprMentionSomeLicensor = { reprPrec := Semantics.Questions.MentionSome.instReprMentionSomeLicensor.repr }

structure Semantics.Questions.MentionSome.MentionSomeQuestion' (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A mention-some question bundled with its reading type.

• interrogative : MentionSomeInterrogative W E

  The underlying interrogative structure

• licensor : MentionSomeLicensor

  What licenses the mention-some reading

• naturalForm : String

  Natural language form

Logical Relations Between Readings

@cite{groenendijk-stokhof-1984}, Section 5.3 establishes:

1. Choice implies mention-some: If you know the choice-answer (for whichever disjunct is relevant), you know a mention-some answer.

2. Mention-all implies mention-some (if non-empty): If you know all satisfiers, you certainly know at least one.

These are important for understanding the logical landscape of readings.

theorem Semantics.Questions.MentionSome.choice_implies_mentionSome {W : Type u_1} {E : Type u_2} (msi : MentionSomeInterrogative W E) (w : W) (y : E) (hy_mem : y ∈ msi.whDomain) (hy_sat : msi.abstract w y = true) : (msi.whDomain.any fun (x : E) => msi.abstract w x) = true

Choice reading implies mention-some reading.

@cite{groenendijk-stokhof-1984}, Section 5.3, p. 538: "The choice reading of (24) implies its mention-some reading. This is correct, to know of a particular pen who has that pen, implies to know a person who has a pen."

A choice answer selects a specific satisfier from the wh-domain. Any such witness directly satisfies the existential required by mention-some.

For the full two-domain case (wide-scope existential over a separate domain), see wideScope_existential_licenses_mentionSome in ScopeReadings.lean.

theorem Semantics.Questions.MentionSome.mentionAll_implies_mentionSome {W : Type u_1} {E : Type u_2} (msi : MentionSomeInterrogative W E) (w : W) (satisfiers : List E) (hAll : satisfiers = List.filter (msi.abstract w) msi.whDomain) (hNonempty : satisfiers.length > 0) : (msi.whDomain.any fun (x : E) => msi.abstract w x) = true

Mention-all implies mention-some for non-empty extensions.

If you know ALL satisfiers, and there is at least one, you know SOME.

Verbs That Block Mention-Some

@cite{groenendijk-stokhof-1984}, Section 5.4: Some verbs BLOCK mention-some readings:

• "It depends on who has a pen" - requires exhaustive answer
• "It matters who has a pen" - requires exhaustive answer
• "Whether John succeeds will determine who gets the prize" - exhaustive

These verbs require knowing the COMPLETE answer because they express functional dependencies or relevance that needs full information.

In contrast, these verbs ALLOW mention-some:

• "John knows who has a pen" - can be mention-some
• "John wonders who has a pen" - can be mention-some
• "John asked who has a pen" - can be mention-some

def Semantics.Questions.MentionSome.verbAllowsMentionSome : String → Bool

Does a verb allow mention-some readings?

@cite{groenendijk-stokhof-1984}, Section 5.4: "depends", "matter", "determine" block mention-some because they require complete functional information.

Equations

• Semantics.Questions.MentionSome.verbAllowsMentionSome "know" = true
• Semantics.Questions.MentionSome.verbAllowsMentionSome "knows" = true
• Semantics.Questions.MentionSome.verbAllowsMentionSome "wonder" = true
• Semantics.Questions.MentionSome.verbAllowsMentionSome "wonders" = true
• Semantics.Questions.MentionSome.verbAllowsMentionSome "ask" = true
• Semantics.Questions.MentionSome.verbAllowsMentionSome "asks" = true
• Semantics.Questions.MentionSome.verbAllowsMentionSome "asked" = true
• Semantics.Questions.MentionSome.verbAllowsMentionSome "find out" = true
• Semantics.Questions.MentionSome.verbAllowsMentionSome "discover" = true
• Semantics.Questions.MentionSome.verbAllowsMentionSome "tell" = true
• Semantics.Questions.MentionSome.verbAllowsMentionSome "depends" = false
• Semantics.Questions.MentionSome.verbAllowsMentionSome "depend" = false
• Semantics.Questions.MentionSome.verbAllowsMentionSome "matter" = false
• Semantics.Questions.MentionSome.verbAllowsMentionSome "matters" = false
• Semantics.Questions.MentionSome.verbAllowsMentionSome "determine" = false
• Semantics.Questions.MentionSome.verbAllowsMentionSome "determines" = false
• Semantics.Questions.MentionSome.verbAllowsMentionSome "decided by" = false
• Semantics.Questions.MentionSome.verbAllowsMentionSome x✝ = true

structure Semantics.Questions.MentionSome.EmbeddedQuestionSentence (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A sentence with embedded question and verb.

• verb : String

  The matrix verb

• question : MentionSomeInterrogative W E

  The embedded question

• subject : E

  The matrix subject

• mentionSomePossible : Bool

  Does the sentence have mention-some reading?

Mention-Two / Mention-N

@cite{groenendijk-stokhof-1984}, Section 5.3 (following @cite{belnap-1982}): Cumulative quantification with numerals gives "mention-n" readings:

"Where do two unicorns live?"

This is ambiguous:

1. Mention-some: One place where (at least) two unicorns live
2. Mention-two (cumulative): Two places that together house two unicorns (e.g., one unicorn in Paris, one in Rome)
3. Choice: Identify the specific two unicorns, then where they live

The cumulative reading requires the places to COLLECTIVELY satisfy the numeral, not each place individually.

structure Semantics.Questions.MentionSome.MentionNQuestion (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A mention-n question with cumulative quantification.

"Where do N unicorns live?" - asks for places collectively covering N entities.

• n : ℕ

  How many entities must be covered

• whDomain : List E

  The wh-domain (places)

• entityDomain : List E

  The entity domain (unicorns)

• relation : W → E → E → Bool

  The relation: lives(w, place, entity)

def Semantics.Questions.MentionSome.collectivelyCovers {W : Type u_1} {E : Type u_2} [DecidableEq E] (mnq : MentionNQuestion W E) (places : List E) (w : W) : Bool

Does a set of places collectively cover n entities?

For mention-n, we need the UNION of entities at these places to have size ≥ n.

Equations

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

def Semantics.Questions.MentionSome.mentionSomeAnswerToMentionN {W : Type u_1} {E : Type u_2} [DecidableEq E] (mnq : MentionNQuestion W E) (place : E) (w : W) : Bool

Mention-some answer to mention-n: ONE place with n entities.

"Where do two unicorns live?" (mention-some) = a single place with 2+ unicorns

Equations

• Semantics.Questions.MentionSome.mentionSomeAnswerToMentionN mnq place w = decide ((List.filter (fun (e : E) => mnq.relation w place e) mnq.entityDomain).length ≥ mnq.n)

def Semantics.Questions.MentionSome.cumulativeAnswer {W : Type u_1} {E : Type u_2} [DecidableEq E] (mnq : MentionNQuestion W E) (places : List E) (w : W) : Bool

Cumulative mention-n: multiple places collectively covering n entities.

"Where do two unicorns live?" (cumulative) = places that together have 2 unicorns

Equations

• Semantics.Questions.MentionSome.cumulativeAnswer mnq places w = Semantics.Questions.MentionSome.collectivelyCovers mnq places w

Categorematic Quantifier Grounding

@cite{belnap-1982}'s categorematic principle: the same quantifier words (every, some, most) work identically in declarative and interrogative contexts. The ∃ in I-MS is structurally the same generalized-quantifier application as some_sem in Semantics.Lexical.Determiner.Quantifier: both compute domain.any (λ x => restrictor(x) ∧ scope(x)).

def Semantics.Questions.MentionSome.gqApply {E : Type u_1} (domain : List E) (restrictor scope : E → Bool) : Bool

GQ application: ∃x ∈ domain. R(x) ∧ S(x). This is the shared computation underlying both declarative some_sem and interrogative I-MS.

Equations

• Semantics.Questions.MentionSome.gqApply domain restrictor scope = domain.any fun (x : E) => restrictor x && scope x

theorem Semantics.Questions.MentionSome.applyToProperty_eq_gqApply {W : Type u_1} {E : Type u_2} [DecidableEq E] (msi : MentionSomeInterrogative W E) (Q : GSQuestion W → Bool) (w : W) : msi.applyToProperty Q w = gqApply msi.whDomain (msi.abstract w) fun (x : E) => Q (yesNoQuestionFor msi.abstract x)

@cite{belnap-1982}'s categorematic principle: applyToProperty factors as gqApply(whDomain, abstract(w), λx. Q(yn-question(x))) — the same GQ existential used in declarative some_sem.

Partial Answer Taxonomy

@cite{belnap-1982} distinguishes direct answers (complete, non-redundant) from partial and eliminative answers. Two partial-answer definitions exist in linglib:

• Answerhood.isPartialAnswer: p overlaps with some but not all cells (p eliminates at least one possibility)
• partialAnswer (this file): p overlaps with at least two cells (p doesn't pin down a unique cell)

isPartialAnswer is strictly stronger: it additionally requires that p fails to overlap with at least one cell (ruling out tautological propositions).

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

The two partial-answer notions agree on genuine partial answers but diverge on tautologies. Concrete witness on Fin 3 with the identity partition.