RSA Attitude Verb Embedding

@cite{chierchia-fox-spector-2012} @cite{geurts-2010} @cite{sauerland-2004}

Models scalar implicatures embedded under attitude verbs like "believe".

The Phenomenon

"John believes some students passed"

Can have two readings:

1. Global: John believes [some passed] - speaker implicates "not all"
2. Local: John believes [some-but-not-all passed] - John's belief includes "not all"

Unlike DE contexts, attitude verbs allow BOTH interpretations.

Theoretical Background

Attitude verbs create INTENSIONAL contexts:

• The embedded clause is evaluated at John's belief worlds, not the actual world
• Implicatures can be computed globally (about the speaker's assertion) or locally (about John's belief content)

This differs from DE contexts where:

• Local implicature strengthens the embedded clause
• Which weakens the overall sentence (due to downward monotonicity)
• So global is pragmatically preferred

With attitude verbs:

• Local implicature changes what John believes
• This doesn't weaken the overall sentence
• Both interpretations are felicitous

inductive RSA.AttitudeEmbedding.StudentOutcome : Type

Student outcomes in the actual world and John's beliefs.

For "John believes some students passed", we need to track:

1. How many students ACTUALLY passed
2. How many students JOHN BELIEVES passed

• noneO : StudentOutcome
• someO : StudentOutcome
• allO : StudentOutcome

instance RSA.AttitudeEmbedding.instDecidableEqStudentOutcome : DecidableEq StudentOutcome

Equations

• RSA.AttitudeEmbedding.instDecidableEqStudentOutcome x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RSA.AttitudeEmbedding.instReprStudentOutcome.repr : StudentOutcome → ℕ → Std.Format

Equations

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

instance RSA.AttitudeEmbedding.instReprStudentOutcome : Repr StudentOutcome

Equations

• RSA.AttitudeEmbedding.instReprStudentOutcome = { reprPrec := RSA.AttitudeEmbedding.instReprStudentOutcome.repr }

def RSA.AttitudeEmbedding.instBEqStudentOutcome.beq : StudentOutcome → StudentOutcome → Bool

Equations

• RSA.AttitudeEmbedding.instBEqStudentOutcome.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.AttitudeEmbedding.instBEqStudentOutcome : BEq StudentOutcome

Equations

• RSA.AttitudeEmbedding.instBEqStudentOutcome = { beq := RSA.AttitudeEmbedding.instBEqStudentOutcome.beq }

def RSA.AttitudeEmbedding.instInhabitedStudentOutcome.default : StudentOutcome

Equations

• RSA.AttitudeEmbedding.instInhabitedStudentOutcome.default = RSA.AttitudeEmbedding.StudentOutcome.noneO

instance RSA.AttitudeEmbedding.instInhabitedStudentOutcome : Inhabited StudentOutcome

Equations

• RSA.AttitudeEmbedding.instInhabitedStudentOutcome = { default := RSA.AttitudeEmbedding.instInhabitedStudentOutcome.default }

structure RSA.AttitudeEmbedding.BeliefWorld : Type

World state tracking both reality and John's beliefs.

Key insight: John's beliefs may differ from reality!

• John might believe "some passed" when actually "all passed"
• John might believe "all passed" when actually "some passed"

• actual : StudentOutcome

  What actually happened

• johnBelieves : StudentOutcome

  What John believes happened

def RSA.AttitudeEmbedding.instDecidableEqBeliefWorld.decEq (x✝ x✝¹ : BeliefWorld) : Decidable (x✝ = x✝¹)

Equations

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

instance RSA.AttitudeEmbedding.instDecidableEqBeliefWorld : DecidableEq BeliefWorld

Equations

• RSA.AttitudeEmbedding.instDecidableEqBeliefWorld = RSA.AttitudeEmbedding.instDecidableEqBeliefWorld.decEq

def RSA.AttitudeEmbedding.instReprBeliefWorld.repr : BeliefWorld → ℕ → Std.Format

Equations

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

instance RSA.AttitudeEmbedding.instReprBeliefWorld : Repr BeliefWorld

Equations

• RSA.AttitudeEmbedding.instReprBeliefWorld = { reprPrec := RSA.AttitudeEmbedding.instReprBeliefWorld.repr }

instance RSA.AttitudeEmbedding.instBEqBeliefWorld : BEq BeliefWorld

Equations

• RSA.AttitudeEmbedding.instBEqBeliefWorld = { beq := RSA.AttitudeEmbedding.instBEqBeliefWorld.beq }

def RSA.AttitudeEmbedding.instBEqBeliefWorld.beq : BeliefWorld → BeliefWorld → Bool

Equations

• RSA.AttitudeEmbedding.instBEqBeliefWorld.beq { actual := a, johnBelieves := a_1 } { actual := b, johnBelieves := b_1 } = (a == b && a_1 == b_1)
• RSA.AttitudeEmbedding.instBEqBeliefWorld.beq x✝¹ x✝ = false

instance RSA.AttitudeEmbedding.instInhabitedBeliefWorld : Inhabited BeliefWorld

Equations

• RSA.AttitudeEmbedding.instInhabitedBeliefWorld = { default := RSA.AttitudeEmbedding.instInhabitedBeliefWorld.default }

def RSA.AttitudeEmbedding.instInhabitedBeliefWorld.default : BeliefWorld

Equations

• RSA.AttitudeEmbedding.instInhabitedBeliefWorld.default = { actual := default, johnBelieves := default }

def RSA.AttitudeEmbedding.BeliefWorld.actuallyNone (w : BeliefWorld) : Bool

The actual world determines what's true at the matrix level

Equations

• w.actuallyNone = (w.actual == RSA.AttitudeEmbedding.StudentOutcome.noneO)

def RSA.AttitudeEmbedding.BeliefWorld.actuallySome (w : BeliefWorld) : Bool

Equations

• w.actuallySome = (w.actual == RSA.AttitudeEmbedding.StudentOutcome.someO || w.actual == RSA.AttitudeEmbedding.StudentOutcome.allO)

def RSA.AttitudeEmbedding.BeliefWorld.actuallyAll (w : BeliefWorld) : Bool

Equations

• w.actuallyAll = (w.actual == RSA.AttitudeEmbedding.StudentOutcome.allO)

def RSA.AttitudeEmbedding.BeliefWorld.johnBelievesNone (w : BeliefWorld) : Bool

John's beliefs determine what's true in embedded contexts

Equations

• w.johnBelievesNone = (w.johnBelieves == RSA.AttitudeEmbedding.StudentOutcome.noneO)

def RSA.AttitudeEmbedding.BeliefWorld.johnBelievesSome (w : BeliefWorld) : Bool

Equations

• w.johnBelievesSome = (w.johnBelieves == RSA.AttitudeEmbedding.StudentOutcome.someO || w.johnBelieves == RSA.AttitudeEmbedding.StudentOutcome.allO)

def RSA.AttitudeEmbedding.BeliefWorld.johnBelievesAll (w : BeliefWorld) : Bool

Equations

• w.johnBelievesAll = (w.johnBelieves == RSA.AttitudeEmbedding.StudentOutcome.allO)

def RSA.AttitudeEmbedding.BeliefWorld.johnBelievesSomeNotAll (w : BeliefWorld) : Bool

Equations

• w.johnBelievesSomeNotAll = (w.johnBelieves == RSA.AttitudeEmbedding.StudentOutcome.someO)

inductive RSA.AttitudeEmbedding.AttitudeInterpretation : Type

Two possible interpretations of "John believes some students passed":

1. Global: The "some" gets its weak meaning; implicature computed at matrix

• Literal: John believes [∃x. student(x) ∧ passed(x)]
• Implicature: Speaker implicates John doesn't believe all passed

2. Local: The "some" gets strong meaning inside the belief

• Literal: John believes [∃x. student(x) ∧ passed(x) ∧ ¬∀y. student(y) → passed(y)]
• = John believes some-but-not-all passed

• global : AttitudeInterpretation
• local_ : AttitudeInterpretation

instance RSA.AttitudeEmbedding.instDecidableEqAttitudeInterpretation : DecidableEq AttitudeInterpretation

Equations

• RSA.AttitudeEmbedding.instDecidableEqAttitudeInterpretation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance RSA.AttitudeEmbedding.instReprAttitudeInterpretation : Repr AttitudeInterpretation

Equations

• RSA.AttitudeEmbedding.instReprAttitudeInterpretation = { reprPrec := RSA.AttitudeEmbedding.instReprAttitudeInterpretation.repr }

def RSA.AttitudeEmbedding.instReprAttitudeInterpretation.repr : AttitudeInterpretation → ℕ → Std.Format

Equations

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

def RSA.AttitudeEmbedding.instBEqAttitudeInterpretation.beq : AttitudeInterpretation → AttitudeInterpretation → Bool

Equations

• RSA.AttitudeEmbedding.instBEqAttitudeInterpretation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.AttitudeEmbedding.instBEqAttitudeInterpretation : BEq AttitudeInterpretation

Equations

• RSA.AttitudeEmbedding.instBEqAttitudeInterpretation = { beq := RSA.AttitudeEmbedding.instBEqAttitudeInterpretation.beq }

def RSA.AttitudeEmbedding.instInhabitedAttitudeInterpretation.default : AttitudeInterpretation

Equations

• RSA.AttitudeEmbedding.instInhabitedAttitudeInterpretation.default = RSA.AttitudeEmbedding.AttitudeInterpretation.global

instance RSA.AttitudeEmbedding.instInhabitedAttitudeInterpretation : Inhabited AttitudeInterpretation

Equations

• RSA.AttitudeEmbedding.instInhabitedAttitudeInterpretation = { default := RSA.AttitudeEmbedding.instInhabitedAttitudeInterpretation.default }

instance RSA.AttitudeEmbedding.instFintypeAttitudeInterpretation : Fintype AttitudeInterpretation

Equations

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

def RSA.AttitudeEmbedding.believesSomeMeaning (interp : AttitudeInterpretation) (w : BeliefWorld) : Bool

Truth conditions for "John believes some students passed".

• Global: True iff John believes at least one passed (The "not all" is an implicature about the speaker's claim)

• Local: True iff John believes some-but-not-all passed (The "not all" is part of what John believes)

Equations

• RSA.AttitudeEmbedding.believesSomeMeaning RSA.AttitudeEmbedding.AttitudeInterpretation.global w = w.johnBelievesSome
• RSA.AttitudeEmbedding.believesSomeMeaning RSA.AttitudeEmbedding.AttitudeInterpretation.local_ w = w.johnBelievesSomeNotAll

def RSA.AttitudeEmbedding.believesAllMeaning (w : BeliefWorld) : Bool

For comparison: "John believes all students passed" (unambiguous).

Equations

• RSA.AttitudeEmbedding.believesAllMeaning w = w.johnBelievesAll

def RSA.AttitudeEmbedding.believesNoneMeaning (w : BeliefWorld) : Bool

For comparison: "John believes no students passed" (unambiguous).

Equations

• RSA.AttitudeEmbedding.believesNoneMeaning w = w.johnBelievesNone

def RSA.AttitudeEmbedding.attitudeWorlds : List BeliefWorld

Relevant worlds for the attitude embedding scenario.

We focus on cases where John has a definite belief about the students. (More complex models could include uncertainty in John's beliefs.)

Equations

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

instance RSA.AttitudeEmbedding.instFintypeStudentOutcome : Fintype StudentOutcome

Equations

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

instance RSA.AttitudeEmbedding.instFintypeBeliefWorld : Fintype BeliefWorld

Equations

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

inductive RSA.AttitudeEmbedding.AttitudeUtterance : Type

Utterances for the attitude scenario.

• believesSome : AttitudeUtterance
• believesAll : AttitudeUtterance
• believesNone : AttitudeUtterance

instance RSA.AttitudeEmbedding.instDecidableEqAttitudeUtterance : DecidableEq AttitudeUtterance

Equations

• RSA.AttitudeEmbedding.instDecidableEqAttitudeUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance RSA.AttitudeEmbedding.instReprAttitudeUtterance : Repr AttitudeUtterance

Equations

• RSA.AttitudeEmbedding.instReprAttitudeUtterance = { reprPrec := RSA.AttitudeEmbedding.instReprAttitudeUtterance.repr }

def RSA.AttitudeEmbedding.instReprAttitudeUtterance.repr : AttitudeUtterance → ℕ → Std.Format

Equations

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

def RSA.AttitudeEmbedding.instBEqAttitudeUtterance.beq : AttitudeUtterance → AttitudeUtterance → Bool

Equations

• RSA.AttitudeEmbedding.instBEqAttitudeUtterance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance RSA.AttitudeEmbedding.instBEqAttitudeUtterance : BEq AttitudeUtterance

Equations

• RSA.AttitudeEmbedding.instBEqAttitudeUtterance = { beq := RSA.AttitudeEmbedding.instBEqAttitudeUtterance.beq }

instance RSA.AttitudeEmbedding.instInhabitedAttitudeUtterance : Inhabited AttitudeUtterance

Equations

• RSA.AttitudeEmbedding.instInhabitedAttitudeUtterance = { default := RSA.AttitudeEmbedding.instInhabitedAttitudeUtterance.default }

def RSA.AttitudeEmbedding.instInhabitedAttitudeUtterance.default : AttitudeUtterance

Equations

• RSA.AttitudeEmbedding.instInhabitedAttitudeUtterance.default = RSA.AttitudeEmbedding.AttitudeUtterance.believesSome

instance RSA.AttitudeEmbedding.instFintypeAttitudeUtterance : Fintype AttitudeUtterance

Equations

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

def RSA.AttitudeEmbedding.utteranceMeaning (u : AttitudeUtterance) (interp : AttitudeInterpretation) (w : BeliefWorld) : Bool

Truth under an interpretation (for "believes some" only).

Equations

• RSA.AttitudeEmbedding.utteranceMeaning RSA.AttitudeEmbedding.AttitudeUtterance.believesSome interp w = RSA.AttitudeEmbedding.believesSomeMeaning interp w
• RSA.AttitudeEmbedding.utteranceMeaning RSA.AttitudeEmbedding.AttitudeUtterance.believesAll interp w = RSA.AttitudeEmbedding.believesAllMeaning w
• RSA.AttitudeEmbedding.utteranceMeaning RSA.AttitudeEmbedding.AttitudeUtterance.believesNone interp w = RSA.AttitudeEmbedding.believesNoneMeaning w

theorem RSA.AttitudeEmbedding.global_includes_all_belief : believesSomeMeaning AttitudeInterpretation.global { actual := StudentOutcome.allO, johnBelieves := StudentOutcome.allO } = true

Under global interpretation:

• "John believes some" is true in worlds where John believes ≥1 passed
• This includes both johnBelieves =.someO AND johnBelieves =.allO

theorem RSA.AttitudeEmbedding.local_excludes_all_belief : believesSomeMeaning AttitudeInterpretation.local_ { actual := StudentOutcome.allO, johnBelieves := StudentOutcome.allO } = false

Under local interpretation:

• "John believes some" is true only when John believes some-but-not-all
• johnBelieves =.allO makes it FALSE

theorem RSA.AttitudeEmbedding.global_local_differ_at_all_belief : believesSomeMeaning AttitudeInterpretation.global { actual := StudentOutcome.allO, johnBelieves := StudentOutcome.allO } ≠ believesSomeMeaning AttitudeInterpretation.local_ { actual := StudentOutcome.allO, johnBelieves := StudentOutcome.allO }

The key difference: global and local differ when John believes all.

theorem RSA.AttitudeEmbedding.local_entails_global (w : BeliefWorld) : believesSomeMeaning AttitudeInterpretation.local_ w = true → believesSomeMeaning AttitudeInterpretation.global w = true

Local entails global for attitude embedding (unlike DE contexts).

theorem RSA.AttitudeEmbedding.global_not_entails_local : ∃ (w : BeliefWorld), believesSomeMeaning AttitudeInterpretation.global w = true ∧ believesSomeMeaning AttitudeInterpretation.local_ w = false

But global does NOT entail local.

def RSA.AttitudeEmbedding.somePassedProp (outcome : StudentOutcome) : Bool

Semantic grounding for "some students passed" as a proposition.

At a world, "some students passed" is true iff ≥1 student passed. We model this with StudentOutcome:

• .noneO → false
• .someO → true (some but not all)
• .allO → true (all, which entails some)

Equations

• RSA.AttitudeEmbedding.somePassedProp outcome = (outcome == RSA.AttitudeEmbedding.StudentOutcome.someO || outcome == RSA.AttitudeEmbedding.StudentOutcome.allO)

def RSA.AttitudeEmbedding.someNotAllPassedProp (outcome : StudentOutcome) : Bool

Semantic grounding for "some-but-not-all students passed".

Equations

• RSA.AttitudeEmbedding.someNotAllPassedProp outcome = (outcome == RSA.AttitudeEmbedding.StudentOutcome.someO)

def RSA.AttitudeEmbedding.allPassedProp (outcome : StudentOutcome) : Bool

Semantic grounding for "all students passed".

Equations

• RSA.AttitudeEmbedding.allPassedProp outcome = (outcome == RSA.AttitudeEmbedding.StudentOutcome.allO)

theorem RSA.AttitudeEmbedding.global_grounded (w : BeliefWorld) : believesSomeMeaning AttitudeInterpretation.global w = somePassedProp w.johnBelieves

Grounding Theorem 1: The global meaning corresponds to Montague semantics.

Global interpretation: "John believes some passed" = John's belief state satisfies "some passed" = somePassedProp(johnBelieves) = true

This theorem proves the stipulated johnBelievesSome equals the compositional evaluation somePassedProp.

theorem RSA.AttitudeEmbedding.local_grounded (w : BeliefWorld) : believesSomeMeaning AttitudeInterpretation.local_ w = someNotAllPassedProp w.johnBelieves

Grounding Theorem 2: The local meaning corresponds to Montague semantics.

Local interpretation: "John believes some-but-not-all passed" = John's belief state satisfies "some-but-not-all passed" = someNotAllPassedProp(johnBelieves) = true

theorem RSA.AttitudeEmbedding.believes_all_grounded (w : BeliefWorld) : believesAllMeaning w = allPassedProp w.johnBelieves

Grounding Theorem 3: The unambiguous "believes all" is grounded.

theorem RSA.AttitudeEmbedding.prop_entailment (o : StudentOutcome) : someNotAllPassedProp o = true → somePassedProp o = true

Semantic entailment grounding: "some-not-all" entails "some" at the propositional level.

This explains why local_entails_global holds: it follows from the semantics.

theorem RSA.AttitudeEmbedding.local_entails_global_grounded (w : BeliefWorld) : believesSomeMeaning AttitudeInterpretation.local_ w = true → believesSomeMeaning AttitudeInterpretation.global w = true

The local→global entailment is grounded in propositional semantics.