RSA Question Embedding

@cite{geurts-2010} @cite{hamblin-1973b} @cite{groenendijk-stokhof-1984}

Models scalar implicatures embedded in questions.

The Phenomenon

"Did some students pass?"

Questions have a unique status regarding scalar implicatures:

• Not clearly upward-entailing (UE) like assertions
• Not clearly downward-entailing (DE) like negation
• Implicatures may arise, but weaker than in assertions

Theoretical Background

Questions are often analyzed as sets of propositions or partitions of logical space. The key insight:

A question "Did some students pass?" asks the hearer to choose between:

• "Yes, some passed" (weak: >=1)
• "No, no one passed"

If the implicature "not all" is computed:

• "Yes, some-but-not-all passed"
• "No, either none or all passed" (??)

The second option doesn't make sense, suggesting local SI in questions is problematic.

Predictions

Unlike assertions (where local SI strengthens) or DE contexts (where local SI weakens), questions create an asymmetry:

• The "yes" answer benefits from SI (more precise)
• The "no" answer becomes weird with SI (disjunctive)

RSA should predict: Local SI is dispreferred in questions because it makes one answer pragmatically odd.

inductive Phenomena.ScalarImplicatures.Embedded.Questions.StudentResult : Type

Student outcome for question scenario.

• noneP : StudentResult
• someP : StudentResult
• allP : StudentResult

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.Embedded.Questions.instDecidableEqStudentResult : DecidableEq StudentResult

Equations

• Phenomena.ScalarImplicatures.Embedded.Questions.instDecidableEqStudentResult x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.Embedded.Questions.instReprStudentResult : Repr StudentResult

Equations

• Phenomena.ScalarImplicatures.Embedded.Questions.instReprStudentResult = { reprPrec := Phenomena.ScalarImplicatures.Embedded.Questions.instReprStudentResult.repr }

def Phenomena.ScalarImplicatures.Embedded.Questions.instReprStudentResult.repr : StudentResult → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.Embedded.Questions.instInhabitedStudentResult : Inhabited StudentResult

Equations

• Phenomena.ScalarImplicatures.Embedded.Questions.instInhabitedStudentResult = { default := Phenomena.ScalarImplicatures.Embedded.Questions.instInhabitedStudentResult.default }

def Phenomena.ScalarImplicatures.Embedded.Questions.instInhabitedStudentResult.default : StudentResult

Equations

• Phenomena.ScalarImplicatures.Embedded.Questions.instInhabitedStudentResult.default = Phenomena.ScalarImplicatures.Embedded.Questions.StudentResult.noneP

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.Embedded.Questions.instFintypeStudentResult : Fintype StudentResult

Equations

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

def Phenomena.ScalarImplicatures.Embedded.Questions.questionWorlds : List StudentResult

Worlds represent the actual state of affairs.

Equations

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

structure Phenomena.ScalarImplicatures.Embedded.Questions.YesNoPartition : Type

A yes/no question partitions the world into "yes" and "no" answers.

For "Did some students pass?":

• Yes-worlds: where some (>=1) passed
• No-worlds: where none passed

• yesWorlds : List StudentResult
• noWorlds : List StudentResult

inductive Phenomena.ScalarImplicatures.Embedded.Questions.QuestionInterpretation : Type

Interpretations of "Did some students pass?":

1. Global: "some" = at least one

• Yes: someP, allP (some passed)
• No: noneP (none passed)

2. Local: "some" = some-but-not-all

• Yes: someP (some-but-not-all passed)
• No: noneP, allP (?? disjunctive/weird)

• global : QuestionInterpretation
• local_ : QuestionInterpretation

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.Embedded.Questions.instDecidableEqQuestionInterpretation : DecidableEq QuestionInterpretation

Equations

• Phenomena.ScalarImplicatures.Embedded.Questions.instDecidableEqQuestionInterpretation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.Embedded.Questions.instReprQuestionInterpretation : Repr QuestionInterpretation

Equations

• Phenomena.ScalarImplicatures.Embedded.Questions.instReprQuestionInterpretation = { reprPrec := Phenomena.ScalarImplicatures.Embedded.Questions.instReprQuestionInterpretation.repr }

def Phenomena.ScalarImplicatures.Embedded.Questions.instReprQuestionInterpretation.repr : QuestionInterpretation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.Embedded.Questions.instInhabitedQuestionInterpretation : Inhabited QuestionInterpretation

Equations

• Phenomena.ScalarImplicatures.Embedded.Questions.instInhabitedQuestionInterpretation = { default := Phenomena.ScalarImplicatures.Embedded.Questions.instInhabitedQuestionInterpretation.default }

def Phenomena.ScalarImplicatures.Embedded.Questions.instInhabitedQuestionInterpretation.default : QuestionInterpretation

Equations

• Phenomena.ScalarImplicatures.Embedded.Questions.instInhabitedQuestionInterpretation.default = Phenomena.ScalarImplicatures.Embedded.Questions.QuestionInterpretation.global

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.Embedded.Questions.instFintypeQuestionInterpretation : Fintype QuestionInterpretation

Equations

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

def Phenomena.ScalarImplicatures.Embedded.Questions.questionPartition (interp : QuestionInterpretation) : YesNoPartition

The partition induced by each interpretation.

Equations

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

theorem Phenomena.ScalarImplicatures.Embedded.Questions.global_partition_natural : (questionPartition QuestionInterpretation.global).yesWorlds = [StudentResult.someP, StudentResult.allP] ∧ (questionPartition QuestionInterpretation.global).noWorlds = [StudentResult.noneP]

Global interpretation gives a natural partition:

• Yes = some passed (continuous region on scale)
• No = none passed (complementary region)

theorem Phenomena.ScalarImplicatures.Embedded.Questions.local_partition_disjunctive : (questionPartition QuestionInterpretation.local_).noWorlds = [StudentResult.noneP, StudentResult.allP]

Local interpretation gives a strange partition:

• Yes = some-but-not-all (specific point)
• No = none OR all (disjunctive!)

This disjunctive "no" answer is pragmatically odd.

def Phenomena.ScalarImplicatures.Embedded.Questions.isContiguous (worlds : List StudentResult) : Bool

The "no" answer under local interpretation is disjunctive. This is marked by the worlds being non-contiguous on the scale.

Equations

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

theorem Phenomena.ScalarImplicatures.Embedded.Questions.global_no_contiguous : isContiguous (questionPartition QuestionInterpretation.global).noWorlds = true

theorem Phenomena.ScalarImplicatures.Embedded.Questions.local_no_not_contiguous : isContiguous (questionPartition QuestionInterpretation.local_).noWorlds = false

def Phenomena.ScalarImplicatures.Embedded.Questions.exhaustiveAnswer (interp : QuestionInterpretation) (actual : StudentResult) : String

Exhaustive interpretation: the "yes" answer conveys the MAXIMAL true proposition consistent with "yes".

For global "Did some pass?":

• If someP: answer conveys "some but not all"
• If allP: answer conveys "all"

This makes local SI redundant - exhaustivity handles it.

Equations

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

theorem Phenomena.ScalarImplicatures.Embedded.Questions.local_all_gets_no : exhaustiveAnswer QuestionInterpretation.local_ StudentResult.allP = "No (all passed)"

Under local interpretation, the "all" world gets a "no" answer, which is pragmatically bizarre.

theorem Phenomena.ScalarImplicatures.Embedded.Questions.global_answers_natural : exhaustiveAnswer QuestionInterpretation.global StudentResult.noneP = "No, none passed" ∧ exhaustiveAnswer QuestionInterpretation.global StudentResult.someP = "Yes, some (but not all) passed" ∧ exhaustiveAnswer QuestionInterpretation.global StudentResult.allP = "Yes, all passed"

Under global interpretation with exhaustivity, all answers are natural.

theorem Phenomena.ScalarImplicatures.Embedded.Questions.question_prefers_global : isContiguous (questionPartition QuestionInterpretation.local_).noWorlds = false ∧ isContiguous (questionPartition QuestionInterpretation.global).noWorlds = true

RSA predicts: global interpretation preferred for questions.

Reason: Local creates pragmatically odd partition where "all passed" is a "no" answer.

structure Phenomena.ScalarImplicatures.Embedded.Questions.QuestionUniqueness : Prop

Questions differ from all other embedding contexts:

• Not about entailment direction (like DE vs UE)
• About pragmatic naturalness of the question-answer structure

• not_de_like : ∃ (w : StudentResult), List.elem w (questionPartition QuestionInterpretation.global).yesWorlds = true ∧ List.elem w (questionPartition QuestionInterpretation.local_).yesWorlds = false

  Global doesn't entail local (unlike DE): allP is in global-yes but not local-yes

• not_attitude_like : ∃ (w : StudentResult), List.elem w (questionPartition QuestionInterpretation.local_).yesWorlds = true ∧ List.elem w (questionPartition QuestionInterpretation.global).yesWorlds = true

  Local doesn't entail global (unlike attitude verbs): someP is in both

def Phenomena.ScalarImplicatures.Embedded.Questions.questionIsUnique : QuestionUniqueness

Questions are indeed unique - neither DE-like nor attitude-verb-like in their entailment pattern, yet still prefer global.

Equations

• Phenomena.ScalarImplicatures.Embedded.Questions.questionIsUnique = ⋯