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

@[reducible, inline]

abbrev Phenomena.ScalarImplicatures.Embedded.Attitudes.StudentOutcome : Type

Student outcomes in the actual world and John's beliefs use the canonical SomeAllWorld from Phenomena.ScalarImplicatures.Basic: .none (no students passed), .someNotAll (some-but-not-all passed), .all (all students passed).

Equations

• Phenomena.ScalarImplicatures.Embedded.Attitudes.StudentOutcome = Phenomena.ScalarImplicatures.SomeAllWorld

structure Phenomena.ScalarImplicatures.Embedded.Attitudes.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 Phenomena.ScalarImplicatures.Embedded.Attitudes.instDecidableEqBeliefWorld.decEq (x✝ x✝¹ : BeliefWorld) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.Embedded.Attitudes.instDecidableEqBeliefWorld : DecidableEq BeliefWorld

Equations

• Phenomena.ScalarImplicatures.Embedded.Attitudes.instDecidableEqBeliefWorld = Phenomena.ScalarImplicatures.Embedded.Attitudes.instDecidableEqBeliefWorld.decEq

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.Embedded.Attitudes.instReprBeliefWorld : Repr BeliefWorld

Equations

• Phenomena.ScalarImplicatures.Embedded.Attitudes.instReprBeliefWorld = { reprPrec := Phenomena.ScalarImplicatures.Embedded.Attitudes.instReprBeliefWorld.repr }

def Phenomena.ScalarImplicatures.Embedded.Attitudes.instReprBeliefWorld.repr : BeliefWorld → ℕ → Std.Format

Equations

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

def Phenomena.ScalarImplicatures.Embedded.Attitudes.instInhabitedBeliefWorld.default : BeliefWorld

Equations

• Phenomena.ScalarImplicatures.Embedded.Attitudes.instInhabitedBeliefWorld.default = { actual := default, johnBelieves := default }

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.Embedded.Attitudes.instInhabitedBeliefWorld : Inhabited BeliefWorld

Equations

• Phenomena.ScalarImplicatures.Embedded.Attitudes.instInhabitedBeliefWorld = { default := Phenomena.ScalarImplicatures.Embedded.Attitudes.instInhabitedBeliefWorld.default }

def Phenomena.ScalarImplicatures.Embedded.Attitudes.BeliefWorld.actuallyNone (w : BeliefWorld) : Bool

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

Equations

• w.actuallyNone = (w.actual == Phenomena.ScalarImplicatures.SomeAllWorld.none)

def Phenomena.ScalarImplicatures.Embedded.Attitudes.BeliefWorld.actuallySome (w : BeliefWorld) : Bool

Equations

• w.actuallySome = (w.actual == Phenomena.ScalarImplicatures.SomeAllWorld.someNotAll || w.actual == Phenomena.ScalarImplicatures.SomeAllWorld.all)

def Phenomena.ScalarImplicatures.Embedded.Attitudes.BeliefWorld.actuallyAll (w : BeliefWorld) : Bool

Equations

• w.actuallyAll = (w.actual == Phenomena.ScalarImplicatures.SomeAllWorld.all)

def Phenomena.ScalarImplicatures.Embedded.Attitudes.BeliefWorld.johnBelievesNone (w : BeliefWorld) : Bool

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

Equations

• w.johnBelievesNone = (w.johnBelieves == Phenomena.ScalarImplicatures.SomeAllWorld.none)

def Phenomena.ScalarImplicatures.Embedded.Attitudes.BeliefWorld.johnBelievesSome (w : BeliefWorld) : Bool

Equations

• w.johnBelievesSome = (w.johnBelieves == Phenomena.ScalarImplicatures.SomeAllWorld.someNotAll || w.johnBelieves == Phenomena.ScalarImplicatures.SomeAllWorld.all)

def Phenomena.ScalarImplicatures.Embedded.Attitudes.BeliefWorld.johnBelievesAll (w : BeliefWorld) : Bool

Equations

• w.johnBelievesAll = (w.johnBelieves == Phenomena.ScalarImplicatures.SomeAllWorld.all)

def Phenomena.ScalarImplicatures.Embedded.Attitudes.BeliefWorld.johnBelievesSomeNotAll (w : BeliefWorld) : Bool

Equations

• w.johnBelievesSomeNotAll = (w.johnBelieves == Phenomena.ScalarImplicatures.SomeAllWorld.someNotAll)

inductive Phenomena.ScalarImplicatures.Embedded.Attitudes.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

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.Embedded.Attitudes.instDecidableEqAttitudeInterpretation : DecidableEq AttitudeInterpretation

Equations

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

def Phenomena.ScalarImplicatures.Embedded.Attitudes.instReprAttitudeInterpretation.repr : AttitudeInterpretation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.Embedded.Attitudes.instReprAttitudeInterpretation : Repr AttitudeInterpretation

Equations

• Phenomena.ScalarImplicatures.Embedded.Attitudes.instReprAttitudeInterpretation = { reprPrec := Phenomena.ScalarImplicatures.Embedded.Attitudes.instReprAttitudeInterpretation.repr }

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.Embedded.Attitudes.instInhabitedAttitudeInterpretation : Inhabited AttitudeInterpretation

Equations

• Phenomena.ScalarImplicatures.Embedded.Attitudes.instInhabitedAttitudeInterpretation = { default := Phenomena.ScalarImplicatures.Embedded.Attitudes.instInhabitedAttitudeInterpretation.default }

def Phenomena.ScalarImplicatures.Embedded.Attitudes.instInhabitedAttitudeInterpretation.default : AttitudeInterpretation

Equations

• Phenomena.ScalarImplicatures.Embedded.Attitudes.instInhabitedAttitudeInterpretation.default = Phenomena.ScalarImplicatures.Embedded.Attitudes.AttitudeInterpretation.global

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.Embedded.Attitudes.instFintypeAttitudeInterpretation : Fintype AttitudeInterpretation

Equations

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

def Phenomena.ScalarImplicatures.Embedded.Attitudes.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

• Phenomena.ScalarImplicatures.Embedded.Attitudes.believesSomeMeaning Phenomena.ScalarImplicatures.Embedded.Attitudes.AttitudeInterpretation.global w = w.johnBelievesSome
• Phenomena.ScalarImplicatures.Embedded.Attitudes.believesSomeMeaning Phenomena.ScalarImplicatures.Embedded.Attitudes.AttitudeInterpretation.local_ w = w.johnBelievesSomeNotAll

def Phenomena.ScalarImplicatures.Embedded.Attitudes.believesAllMeaning (w : BeliefWorld) : Bool

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

Equations

• Phenomena.ScalarImplicatures.Embedded.Attitudes.believesAllMeaning w = w.johnBelievesAll

def Phenomena.ScalarImplicatures.Embedded.Attitudes.believesNoneMeaning (w : BeliefWorld) : Bool

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

Equations

• Phenomena.ScalarImplicatures.Embedded.Attitudes.believesNoneMeaning w = w.johnBelievesNone

def Phenomena.ScalarImplicatures.Embedded.Attitudes.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.

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.Embedded.Attitudes.instFintypeBeliefWorld : Fintype BeliefWorld

Equations

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

inductive Phenomena.ScalarImplicatures.Embedded.Attitudes.AttitudeUtterance : Type

Utterances for the attitude scenario.

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

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.Embedded.Attitudes.instDecidableEqAttitudeUtterance : DecidableEq AttitudeUtterance

Equations

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

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.Embedded.Attitudes.instReprAttitudeUtterance : Repr AttitudeUtterance

Equations

• Phenomena.ScalarImplicatures.Embedded.Attitudes.instReprAttitudeUtterance = { reprPrec := Phenomena.ScalarImplicatures.Embedded.Attitudes.instReprAttitudeUtterance.repr }

def Phenomena.ScalarImplicatures.Embedded.Attitudes.instReprAttitudeUtterance.repr : AttitudeUtterance → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.Embedded.Attitudes.instInhabitedAttitudeUtterance : Inhabited AttitudeUtterance

Equations

• Phenomena.ScalarImplicatures.Embedded.Attitudes.instInhabitedAttitudeUtterance = { default := Phenomena.ScalarImplicatures.Embedded.Attitudes.instInhabitedAttitudeUtterance.default }

def Phenomena.ScalarImplicatures.Embedded.Attitudes.instInhabitedAttitudeUtterance.default : AttitudeUtterance

Equations

• Phenomena.ScalarImplicatures.Embedded.Attitudes.instInhabitedAttitudeUtterance.default = Phenomena.ScalarImplicatures.Embedded.Attitudes.AttitudeUtterance.believesSome

@[implicit_reducible]

instance Phenomena.ScalarImplicatures.Embedded.Attitudes.instFintypeAttitudeUtterance : Fintype AttitudeUtterance

Equations

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

def Phenomena.ScalarImplicatures.Embedded.Attitudes.utteranceMeaning (u : AttitudeUtterance) (interp : AttitudeInterpretation) (w : BeliefWorld) : Bool

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

Equations

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

theorem Phenomena.ScalarImplicatures.Embedded.Attitudes.global_includes_all_belief : believesSomeMeaning AttitudeInterpretation.global { actual := SomeAllWorld.all, johnBelieves := SomeAllWorld.all } = true

Under global interpretation:

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

theorem Phenomena.ScalarImplicatures.Embedded.Attitudes.local_excludes_all_belief : believesSomeMeaning AttitudeInterpretation.local_ { actual := SomeAllWorld.all, johnBelieves := SomeAllWorld.all } = false

Under local interpretation:

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

theorem Phenomena.ScalarImplicatures.Embedded.Attitudes.global_local_differ_at_all_belief : believesSomeMeaning AttitudeInterpretation.global { actual := SomeAllWorld.all, johnBelieves := SomeAllWorld.all } ≠ believesSomeMeaning AttitudeInterpretation.local_ { actual := SomeAllWorld.all, johnBelieves := SomeAllWorld.all }

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

theorem Phenomena.ScalarImplicatures.Embedded.Attitudes.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 Phenomena.ScalarImplicatures.Embedded.Attitudes.global_not_entails_local : ∃ (w : BeliefWorld), believesSomeMeaning AttitudeInterpretation.global w = true ∧ believesSomeMeaning AttitudeInterpretation.local_ w = false

But global does NOT entail local.

def Phenomena.ScalarImplicatures.Embedded.Attitudes.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:

• .none → false
• .someNotAll → true (some but not all)
• .all → true (all, which entails some)

Equations

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

def Phenomena.ScalarImplicatures.Embedded.Attitudes.someNotAllPassedProp (outcome : StudentOutcome) : Bool

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

Equations

• Phenomena.ScalarImplicatures.Embedded.Attitudes.someNotAllPassedProp outcome = (outcome == Phenomena.ScalarImplicatures.SomeAllWorld.someNotAll)

def Phenomena.ScalarImplicatures.Embedded.Attitudes.allPassedProp (outcome : StudentOutcome) : Bool

Semantic grounding for "all students passed".

Equations

• Phenomena.ScalarImplicatures.Embedded.Attitudes.allPassedProp outcome = (outcome == Phenomena.ScalarImplicatures.SomeAllWorld.all)

theorem Phenomena.ScalarImplicatures.Embedded.Attitudes.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 Phenomena.ScalarImplicatures.Embedded.Attitudes.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 Phenomena.ScalarImplicatures.Embedded.Attitudes.believes_all_grounded (w : BeliefWorld) : believesAllMeaning w = allPassedProp w.johnBelieves

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

theorem Phenomena.ScalarImplicatures.Embedded.Attitudes.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 Phenomena.ScalarImplicatures.Embedded.Attitudes.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.