Connection to RSA Theory

@cite{bergen-goodman-2015} @cite{rooth-1992}

This phenomenon is modeled by @cite{bergen-goodman-2015}'s noisy channel RSA. See Phenomena.Ellipsis.Studies.BergenGoodman2015 for the model and proofs.

The key insight: prosodic stress reduces noise rate on stressed words. This signals exhaustive knowledge to the listener.

Connection to unified noise theory: Theories/RSA/Core/Noise.lean

inductive Phenomena.Focus.ProsodicExhaustivity.StressPattern : Type

Stress pattern

• noStress : StressPattern
• subjectFocus : StressPattern
• objectFocus : StressPattern
• verbFocus : StressPattern

instance Phenomena.Focus.ProsodicExhaustivity.instDecidableEqStressPattern : DecidableEq StressPattern

Equations

• Phenomena.Focus.ProsodicExhaustivity.instDecidableEqStressPattern x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Focus.ProsodicExhaustivity.instBEqStressPattern.beq : StressPattern → StressPattern → Bool

Equations

• Phenomena.Focus.ProsodicExhaustivity.instBEqStressPattern.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Focus.ProsodicExhaustivity.instBEqStressPattern : BEq StressPattern

Equations

• Phenomena.Focus.ProsodicExhaustivity.instBEqStressPattern = { beq := Phenomena.Focus.ProsodicExhaustivity.instBEqStressPattern.beq }

instance Phenomena.Focus.ProsodicExhaustivity.instReprStressPattern : Repr StressPattern

Equations

• Phenomena.Focus.ProsodicExhaustivity.instReprStressPattern = { reprPrec := Phenomena.Focus.ProsodicExhaustivity.instReprStressPattern.repr }

def Phenomena.Focus.ProsodicExhaustivity.instReprStressPattern.repr : StressPattern → Nat → Std.Format

Equations

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

inductive Phenomena.Focus.ProsodicExhaustivity.Exhaustivity : Type

Exhaustivity interpretation

• exhaustive : Exhaustivity
• nonExhaustive : Exhaustivity
• neutral : Exhaustivity

instance Phenomena.Focus.ProsodicExhaustivity.instDecidableEqExhaustivity : DecidableEq Exhaustivity

Equations

• Phenomena.Focus.ProsodicExhaustivity.instDecidableEqExhaustivity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Focus.ProsodicExhaustivity.instBEqExhaustivity : BEq Exhaustivity

Equations

• Phenomena.Focus.ProsodicExhaustivity.instBEqExhaustivity = { beq := Phenomena.Focus.ProsodicExhaustivity.instBEqExhaustivity.beq }

def Phenomena.Focus.ProsodicExhaustivity.instBEqExhaustivity.beq : Exhaustivity → Exhaustivity → Bool

Equations

• Phenomena.Focus.ProsodicExhaustivity.instBEqExhaustivity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Focus.ProsodicExhaustivity.instReprExhaustivity : Repr Exhaustivity

Equations

• Phenomena.Focus.ProsodicExhaustivity.instReprExhaustivity = { reprPrec := Phenomena.Focus.ProsodicExhaustivity.instReprExhaustivity.repr }

def Phenomena.Focus.ProsodicExhaustivity.instReprExhaustivity.repr : Exhaustivity → Nat → Std.Format

Equations

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

structure Phenomena.Focus.ProsodicExhaustivity.ProsodyDatum : Type

A prosodic exhaustivity datum

• question : String

  The question context

• answer : String

  The answer (CAPS = stress)

• stress : StressPattern

  Stress pattern

• reading : Exhaustivity

  Resulting interpretation

• exhaustiveContent : String

  The exhaustive proposition (if applicable)

• notes : String

  Notes

• source : String

  Source

def Phenomena.Focus.ProsodicExhaustivity.instReprProsodyDatum.repr : ProsodyDatum → Nat → Std.Format

Equations

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

instance Phenomena.Focus.ProsodicExhaustivity.instReprProsodyDatum : Repr ProsodyDatum

Equations

• Phenomena.Focus.ProsodicExhaustivity.instReprProsodyDatum = { reprPrec := Phenomena.Focus.ProsodicExhaustivity.instReprProsodyDatum.repr }

def Phenomena.Focus.ProsodicExhaustivity.stressedSubject : ProsodyDatum

Stressed subject → exhaustive

Equations

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

def Phenomena.Focus.ProsodicExhaustivity.unstressedSubject : ProsodyDatum

Unstressed subject → non-exhaustive

Equations

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

def Phenomena.Focus.ProsodicExhaustivity.stressContrast : List ProsodyDatum

Contrast: stressed vs unstressed

Equations

• Phenomena.Focus.ProsodicExhaustivity.stressContrast = [Phenomena.Focus.ProsodicExhaustivity.stressedSubject, Phenomena.Focus.ProsodicExhaustivity.unstressedSubject]

Selective Focus

In sentences with multiple potential focus positions, stress indicates WHICH dimension the speaker has exhaustive knowledge about.

"John introduced MARY to Bill" → Mary was the only one introduced TO BILL "John introduced Mary to BILL" → Bill was the only one Mary was introduced TO

def Phenomena.Focus.ProsodicExhaustivity.selectiveFocusMary : ProsodyDatum

Focus on first object

Equations

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

def Phenomena.Focus.ProsodicExhaustivity.selectiveFocusBill : ProsodyDatum

Focus on second object

Equations

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

def Phenomena.Focus.ProsodicExhaustivity.selectiveFocusData : List ProsodyDatum

Equations

• Phenomena.Focus.ProsodicExhaustivity.selectiveFocusData = [Phenomena.Focus.ProsodicExhaustivity.selectiveFocusMary, Phenomena.Focus.ProsodicExhaustivity.selectiveFocusBill]

Scalar Focus

Stress on scalar items strengthens scalar implicature:

• "I PASSED" → I know I didn't ace it (strong SI)
• "I passed" → I at least passed, maybe aced (weak SI)

def Phenomena.Focus.ProsodicExhaustivity.scalarStressed : ProsodyDatum

Stressed scalar → strong implicature

Equations

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

def Phenomena.Focus.ProsodicExhaustivity.scalarUnstressed : ProsodyDatum

Unstressed scalar → weak implicature

Equations

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

def Phenomena.Focus.ProsodicExhaustivity.scalarFocusData : List ProsodyDatum

Equations

• Phenomena.Focus.ProsodicExhaustivity.scalarFocusData = [Phenomena.Focus.ProsodicExhaustivity.scalarStressed, Phenomena.Focus.ProsodicExhaustivity.scalarUnstressed]

def Phenomena.Focus.ProsodicExhaustivity.allProsodyData : List ProsodyDatum

Equations

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

Noisy Channel Account

Prosodic stress reduces noise rate on stressed words.

• Louder, longer → more robust to environmental noise
• Speaker strategically protects important information

Mechanism

1. Speaker with exhaustive knowledge needs listener to hear correctly
2. Mishearing "Bob" as "Alice" would convey false information
3. Therefore: stress "Bob" to reduce noise
4. Listener infers: stress → speaker had reason to protect → exhaustive knowledge

Predictions

• Effect emerges at higher recursion depths (pragmatic inference)
• Stress increases exhaustive interpretation probability

See Phenomena.Ellipsis.Studies.BergenGoodman2015 for proofs.

Alternative Accounts

Focus Semantics

• Focus introduces alternatives
• Exhaustivity via exhaustification operator (Exh)
• Stress marks what's "at issue"

Question-Answer Congruence (@cite{groenendijk-stokhof-1984})

• Stressed material must match question's "wh" position
• Exhaustivity from partition semantics of questions

Connection to Verum Focus

Verum focus (see VerumFocus.lean) is focus on truth/polarity:

• "John DOES drink" (emphatic affirmation)

Prosodic exhaustivity is focus on answer content:

• "JOHN drinks" (John and only John)

Both involve focus interpretation but target different elements.

Connection to Question Exhaustivity

See Questions/Exhaustivity.lean for:

• Mention-some vs mention-all distinction
• When exhaustive answers are required
• Term type effects on exhaustivity

Prosodic stress can OVERRIDE default exhaustivity:

• Mention-some question + stress → forced exhaustive reading