[BGH22]: the weak evidence effect

RSA with a persuasive speaker whose utility adds β · ln L0(w*|u) for a goal state w* to the epistemic term (eq. 6; β = 0 is standard RSA). With w* = "longer" the speaker weight is L0(longer|u)^β · 𝟙[u ∈ w] (eq. 8; α = 1, so the exponent is β, here 2). A pragmatic listener who expects the strongest available evidence reads weak positive evidence as implying no stronger evidence exists — so it backfires.

The paper's Stick Contest (5 sticks from {1,…,9}, 126 worlds) is formalized at 3 sticks from {1,…,5} (10 worlds, midpoint 3), preserving the load-bearing structure: the prior favors ¬longer (2/5) and L0(longer|·) is monotone in stick length.

Main results

• weak_evidence_effect: at β = 2, stick 4 — positive literal evidence — backfires under the pragmatic listener; strong_evidence_works shows the strongest evidence cannot be explained away.
• l0_s5_positive / l0_s1_negative / l0_s5_strongest / l0_monotone: the literal-listener evidence ordering.
• argStr_positive_but_backfires: stick 4 has positive [CF21] argumentative strength yet backfires — the model's wedge between argumentative and pragmatic evidence.
• model_predicts_interaction / pragmatic_backfire: the predicted listener-type × evidence interaction matches the behavioral data.

Implementation notes

The uniform world prior cancels from both listeners, so the chain is two PMF.ofScores levels over ℚ≥0 scores and every prediction is one event-mass kernel certificate.

Domain Types

inductive BarnettEtAl2022.Stick : Type

Stick lengths 1–5

• s1 : Stick
• s2 : Stick
• s3 : Stick
• s4 : Stick
• s5 : Stick

@[implicit_reducible]

instance BarnettEtAl2022.instDecidableEqStick : DecidableEq Stick

Equations

• BarnettEtAl2022.instDecidableEqStick x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BarnettEtAl2022.instReprStick.repr : Stick → ℕ → Std.Format

Equations

• BarnettEtAl2022.instReprStick.repr BarnettEtAl2022.Stick.s1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BarnettEtAl2022.Stick.s1")).group prec✝
• BarnettEtAl2022.instReprStick.repr BarnettEtAl2022.Stick.s2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BarnettEtAl2022.Stick.s2")).group prec✝
• BarnettEtAl2022.instReprStick.repr BarnettEtAl2022.Stick.s3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BarnettEtAl2022.Stick.s3")).group prec✝
• BarnettEtAl2022.instReprStick.repr BarnettEtAl2022.Stick.s4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BarnettEtAl2022.Stick.s4")).group prec✝
• BarnettEtAl2022.instReprStick.repr BarnettEtAl2022.Stick.s5 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BarnettEtAl2022.Stick.s5")).group prec✝

@[implicit_reducible]

instance BarnettEtAl2022.instReprStick : Repr Stick

Equations

• BarnettEtAl2022.instReprStick = { reprPrec := BarnettEtAl2022.instReprStick.repr }

@[implicit_reducible]

instance BarnettEtAl2022.instInhabitedStick : Inhabited Stick

Equations

• BarnettEtAl2022.instInhabitedStick = { default := BarnettEtAl2022.instInhabitedStick.default }

@[implicit_reducible]

instance BarnettEtAl2022.instFintypeStick : Fintype Stick

Equations

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

inductive BarnettEtAl2022.StickWorld : Type

Worlds: sets of 3 distinct sticks from {1,...,5}. C(5,3) = 10 worlds.

• w123 : StickWorld
• w124 : StickWorld
• w125 : StickWorld
• w134 : StickWorld
• w135 : StickWorld
• w145 : StickWorld
• w234 : StickWorld
• w235 : StickWorld
• w245 : StickWorld
• w345 : StickWorld

@[implicit_reducible]

instance BarnettEtAl2022.instDecidableEqStickWorld : DecidableEq StickWorld

Equations

• BarnettEtAl2022.instDecidableEqStickWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance BarnettEtAl2022.instReprStickWorld : Repr StickWorld

Equations

• BarnettEtAl2022.instReprStickWorld = { reprPrec := BarnettEtAl2022.instReprStickWorld.repr }

def BarnettEtAl2022.instReprStickWorld.repr : StickWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance BarnettEtAl2022.instInhabitedStickWorld : Inhabited StickWorld

Equations

• BarnettEtAl2022.instInhabitedStickWorld = { default := BarnettEtAl2022.instInhabitedStickWorld.default }

@[implicit_reducible]

instance BarnettEtAl2022.instFintypeStickWorld : Fintype StickWorld

Equations

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

def BarnettEtAl2022.worldContains : StickWorld → Stick → Bool

Whether a stick is available in a given world.

Equations

• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w123 BarnettEtAl2022.Stick.s1 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w123 BarnettEtAl2022.Stick.s2 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w123 BarnettEtAl2022.Stick.s3 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w124 BarnettEtAl2022.Stick.s1 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w124 BarnettEtAl2022.Stick.s2 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w124 BarnettEtAl2022.Stick.s4 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w125 BarnettEtAl2022.Stick.s1 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w125 BarnettEtAl2022.Stick.s2 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w125 BarnettEtAl2022.Stick.s5 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w134 BarnettEtAl2022.Stick.s1 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w134 BarnettEtAl2022.Stick.s3 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w134 BarnettEtAl2022.Stick.s4 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w135 BarnettEtAl2022.Stick.s1 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w135 BarnettEtAl2022.Stick.s3 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w135 BarnettEtAl2022.Stick.s5 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w145 BarnettEtAl2022.Stick.s1 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w145 BarnettEtAl2022.Stick.s4 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w145 BarnettEtAl2022.Stick.s5 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w234 BarnettEtAl2022.Stick.s2 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w234 BarnettEtAl2022.Stick.s3 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w234 BarnettEtAl2022.Stick.s4 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w235 BarnettEtAl2022.Stick.s2 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w235 BarnettEtAl2022.Stick.s3 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w235 BarnettEtAl2022.Stick.s5 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w245 BarnettEtAl2022.Stick.s2 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w245 BarnettEtAl2022.Stick.s4 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w245 BarnettEtAl2022.Stick.s5 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w345 BarnettEtAl2022.Stick.s3 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w345 BarnettEtAl2022.Stick.s4 = true
• BarnettEtAl2022.worldContains BarnettEtAl2022.StickWorld.w345 BarnettEtAl2022.Stick.s5 = true
• BarnettEtAl2022.worldContains x✝¹ x✝ = false

def BarnettEtAl2022.longer : StickWorld → Bool

A world is "longer" if the average stick length exceeds the midpoint (3); equivalently, the three sticks sum past 9. 4 of 10 worlds qualify.

Equations

• BarnettEtAl2022.longer BarnettEtAl2022.StickWorld.w145 = true
• BarnettEtAl2022.longer BarnettEtAl2022.StickWorld.w235 = true
• BarnettEtAl2022.longer BarnettEtAl2022.StickWorld.w245 = true
• BarnettEtAl2022.longer BarnettEtAl2022.StickWorld.w345 = true
• BarnettEtAl2022.longer x✝ = false

Persuasive-speaker scores

def BarnettEtAl2022.l0LongerQ : Stick → ℚ≥0

The literal listener's longer-probability per stick: each stick appears in six worlds, and l0LongerQ_eq_eventMass certifies these fractions against the chain.

Equations

• BarnettEtAl2022.l0LongerQ BarnettEtAl2022.Stick.s1 = 1 / 6
• BarnettEtAl2022.l0LongerQ BarnettEtAl2022.Stick.s2 = 1 / 3
• BarnettEtAl2022.l0LongerQ BarnettEtAl2022.Stick.s3 = 1 / 3
• BarnettEtAl2022.l0LongerQ BarnettEtAl2022.Stick.s4 = 1 / 2
• BarnettEtAl2022.l0LongerQ BarnettEtAl2022.Stick.s5 = 2 / 3

theorem BarnettEtAl2022.l0LongerQ_eq_eventMass (u : Stick) : l0LongerQ u = PMF.eventMass (PMF.scoresWith PMF.Fallback.uniform fun (w : StickWorld) => if worldContains w u = true then 1 else 0) longer

l0LongerQ agrees with the chain: it is the literal listener's longer-event mass at each stick.

def BarnettEtAl2022.priorLonger : ℚ

Prior probability of "longer": 4 out of 10 worlds

Equations

• BarnettEtAl2022.priorLonger = 2 / 5

def BarnettEtAl2022.s1Score (w : StickWorld) (u : Stick) : ℚ≥0

Persuasive-speaker weight (eq. 8 at β = 2): L0(longer|u)² · 𝟙[u ∈ w].

Equations

• BarnettEtAl2022.s1Score w u = if BarnettEtAl2022.worldContains w u = true then BarnettEtAl2022.l0LongerQ u ^ 2 else 0

The chain

The world prior is uniform, so it cancels from both listeners: L0 is the normalized extension indicator, the persuasive speaker normalizes s1Score per world, and L1 is the normalized speaker column.

noncomputable def BarnettEtAl2022.l0 (u : Stick) : PMF StickWorld

Literal listener over worlds (uniform prior conditioned on the extension).

Equations

• BarnettEtAl2022.l0 u = PMF.ofScores PMF.Fallback.uniform fun (w : BarnettEtAl2022.StickWorld) => if BarnettEtAl2022.worldContains w u = true then 1 else 0

noncomputable def BarnettEtAl2022.l0Event (u : Stick) (P : StickWorld → Bool) : ENNReal

Event marginal of the literal listener.

Equations

• BarnettEtAl2022.l0Event u P = ∑' (w : BarnettEtAl2022.StickWorld), if P w = true then (BarnettEtAl2022.l0 u) w else 0

noncomputable def BarnettEtAl2022.s1Persuade (w : StickWorld) : PMF Stick

Persuasive speaker (eq. 8 at β = 2).

Equations

• BarnettEtAl2022.s1Persuade w = PMF.ofScores PMF.Fallback.uniform (BarnettEtAl2022.s1Score w)

noncomputable def BarnettEtAl2022.l1w (u : Stick) : PMF StickWorld

Pragmatic listener over worlds: the normalized speaker column (the uniform prior cancels).

Equations

• BarnettEtAl2022.l1w u = PMF.ofScores PMF.Fallback.uniform fun (w : BarnettEtAl2022.StickWorld) => PMF.scoresWith PMF.Fallback.uniform (BarnettEtAl2022.s1Score w) u

noncomputable def BarnettEtAl2022.l1Event (u : Stick) (P : StickWorld → Bool) : ENNReal

Event marginal of the pragmatic listener.

Equations

• BarnettEtAl2022.l1Event u P = ∑' (w : BarnettEtAl2022.StickWorld), if P w = true then (BarnettEtAl2022.l1w u) w else 0

Predictions — L0

theorem BarnettEtAl2022.l0_s5_positive : (l0Event Stick.s5 fun (w : StickWorld) => !longer w) < l0Event Stick.s5 longer

L0(longer|s5) > L0(¬longer|s5): stick 5 is positive evidence for "longer". 4 of 6 worlds containing s5 are longer, vs 2 not-longer.

theorem BarnettEtAl2022.l0_s5_strongest : l0Event Stick.s4 longer < l0Event Stick.s5 longer

L0(longer|s5) > L0(longer|s4): stick 5 provides stronger evidence than s4.

theorem BarnettEtAl2022.l0_s1_negative : l0Event Stick.s1 longer < l0Event Stick.s1 fun (w : StickWorld) => !longer w

L0(¬longer|s1) > L0(longer|s1): stick 1 is evidence against "longer". Only 1 of 6 worlds containing s1 is longer.

theorem BarnettEtAl2022.l0_monotone : l0LongerQ Stick.s1 ≤ l0LongerQ Stick.s2 ∧ l0LongerQ Stick.s2 ≤ l0LongerQ Stick.s3 ∧ l0LongerQ Stick.s3 ≤ l0LongerQ Stick.s4 ∧ l0LongerQ Stick.s4 ≤ l0LongerQ Stick.s5

L0(longer|·) is monotonically increasing in stick length. This structural property ensures the simplified domain faithfully mirrors the paper's full domain (Appendix Theorem 2).

Predictions — L1 (weak evidence effect)

theorem BarnettEtAl2022.weak_evidence_effect : l1Event Stick.s4 longer < l1Event Stick.s4 fun (w : StickWorld) => !longer w

The weak evidence effect: at β = 2, showing stick 4 — positive literal evidence — decreases the pragmatic listener's belief in "longer" below the ¬longer mass (p. 172: "the absence of strong evidence from a speaker who would be highly motivated to show it statistically implies that no such evidence exists").

theorem BarnettEtAl2022.strong_evidence_works : (l1Event Stick.s5 fun (w : StickWorld) => !longer w) < l1Event Stick.s5 longer

Strong evidence works: the strongest available evidence cannot be explained away by the absence of something better.

Bridge Theorems

theorem BarnettEtAl2022.goalOriented_at_one (uEpi uPers : ℚ) : RSA.CombinedUtility.goalOrientedUtility uEpi uPers 1 = RSA.CombinedUtility.combinedWeighted 1 1 uEpi uPers

At β=1, the persuasive utility equals combinedWeighted(1,1,...).

theorem BarnettEtAl2022.goalOriented_via_combined (uEpi uPers β : ℚ) (hβ : 0 ≤ β) : RSA.CombinedUtility.goalOrientedUtility uEpi uPers β = (1 + β) * RSA.CombinedUtility.combined (RSA.CombinedUtility.betaToLam β) uEpi uPers

The paper's Eq. 6 (additive: U_epi + β·U_pers) equals (1+β) · combined(β/(1+β), U_epi, U_pers).

theorem BarnettEtAl2022.s4_positive_argStr : RSA.ArgumentativeStrength.hasPositiveArgStr (↑(l0LongerQ Stick.s4)) priorLonger

Connection to ArgumentativeStrength: stick 4 has positive argumentative strength for the goal "longer" (L0(longer|s4) = 1/2 > 2/5 = P(longer)).

theorem BarnettEtAl2022.s3_not_positive_argStr : ¬RSA.ArgumentativeStrength.hasPositiveArgStr (↑(l0LongerQ Stick.s3)) priorLonger

Stick 3 does NOT have positive argumentative strength (L0(longer|s3) = 1/3 < 2/5 = P(longer)).

theorem BarnettEtAl2022.argStr_positive_but_backfires : RSA.ArgumentativeStrength.hasPositiveArgStr (↑(l0LongerQ Stick.s4)) priorLonger ∧ l1Event Stick.s4 longer < l1Event Stick.s4 fun (w : StickWorld) => !longer w

The weak evidence effect shows that argumentatively positive evidence can still backfire under a pragmatic listener model. This is the core insight connecting [BGH22] to [CF21]'s work on argumentative strength.

Stick 4 has positive argStr at L0 (1/2 > 2/5), yet L1 assigns more mass to ¬longer than longer after seeing s4.

Experimental Design & Behavioral Data

inductive BarnettEtAl2022.ListenerType : Type

Listener type inferred from speaker expectation phase

• pragmatic : ListenerType
• literal : ListenerType

@[implicit_reducible]

instance BarnettEtAl2022.instDecidableEqListenerType : DecidableEq ListenerType

Equations

• BarnettEtAl2022.instDecidableEqListenerType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance BarnettEtAl2022.instReprListenerType : Repr ListenerType

Equations

• BarnettEtAl2022.instReprListenerType = { reprPrec := BarnettEtAl2022.instReprListenerType.repr }

def BarnettEtAl2022.instReprListenerType.repr : ListenerType → ℕ → Std.Format

Equations

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

inductive BarnettEtAl2022.EvidenceStrength : Type

Evidence strength conditions (distance from midpoint 5")

• weak : EvidenceStrength
• moderate : EvidenceStrength
• strong : EvidenceStrength
• strongest : EvidenceStrength

@[implicit_reducible]

instance BarnettEtAl2022.instDecidableEqEvidenceStrength : DecidableEq EvidenceStrength

Equations

• BarnettEtAl2022.instDecidableEqEvidenceStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BarnettEtAl2022.instReprEvidenceStrength.repr : EvidenceStrength → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance BarnettEtAl2022.instReprEvidenceStrength : Repr EvidenceStrength

Equations

• BarnettEtAl2022.instReprEvidenceStrength = { reprPrec := BarnettEtAl2022.instReprEvidenceStrength.repr }

inductive BarnettEtAl2022.FirstContestant : Type

Which contestant goes first

• longBiased : FirstContestant
• shortBiased : FirstContestant

@[implicit_reducible]

instance BarnettEtAl2022.instDecidableEqFirstContestant : DecidableEq FirstContestant

Equations

• BarnettEtAl2022.instDecidableEqFirstContestant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BarnettEtAl2022.instReprFirstContestant.repr : FirstContestant → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance BarnettEtAl2022.instReprFirstContestant : Repr FirstContestant

Equations

• BarnettEtAl2022.instReprFirstContestant = { reprPrec := BarnettEtAl2022.instReprFirstContestant.repr }

structure BarnettEtAl2022.StickContestDesign : Type

Stick Contest design parameters

• nSticks : ℕ
• minLength : ℕ
• maxLength : ℕ
• midpoint : ℕ
• nParticipants : ℕ

@[implicit_reducible]

instance BarnettEtAl2022.instReprStickContestDesign : Repr StickContestDesign

Equations

• BarnettEtAl2022.instReprStickContestDesign = { reprPrec := BarnettEtAl2022.instReprStickContestDesign.repr }

def BarnettEtAl2022.instReprStickContestDesign.repr : StickContestDesign → ℕ → Std.Format

Equations

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

def BarnettEtAl2022.design : StickContestDesign

The actual experimental parameters

Equations

• BarnettEtAl2022.design = { nSticks := 5, minLength := 1, maxLength := 9, midpoint := 5, nParticipants := 723 }

def BarnettEtAl2022.pragmaticProportion : ℚ

Proportion expecting strongest evidence (pragmatic listeners)

Equations

• BarnettEtAl2022.pragmaticProportion = 485 / 723

def BarnettEtAl2022.literalProportion : ℚ

Proportion expecting weaker evidence (literal listeners)

Equations

• BarnettEtAl2022.literalProportion = 238 / 723

theorem BarnettEtAl2022.pragmatic_is_majority : pragmaticProportion > 1 / 2

structure BarnettEtAl2022.InteractionEffect : Type

Key interaction: speaker expectations × evidence strength. t(718) = 5.2, p < 0.001 (p. 175)

• tStatistic : ℚ
• df : ℕ
• pLessThan : ℚ

@[implicit_reducible]

instance BarnettEtAl2022.instReprInteractionEffect : Repr InteractionEffect

Equations

• BarnettEtAl2022.instReprInteractionEffect = { reprPrec := BarnettEtAl2022.instReprInteractionEffect.repr }

def BarnettEtAl2022.instReprInteractionEffect.repr : InteractionEffect → ℕ → Std.Format

Equations

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

def BarnettEtAl2022.interactionEffect : InteractionEffect

Equations

• BarnettEtAl2022.interactionEffect = { tStatistic := 52 / 10, df := 718, pLessThan := 1 / 1000 }

structure BarnettEtAl2022.GroupResult : Type

Behavioral result for a listener group

• listenerType : ListenerType
• nParticipants : ℕ
• meanSlider : ℚ
• ci95Lower : Option ℚ
• ci95Upper : Option ℚ

def BarnettEtAl2022.instReprGroupResult.repr : GroupResult → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance BarnettEtAl2022.instReprGroupResult : Repr GroupResult

Equations

• BarnettEtAl2022.instReprGroupResult = { reprPrec := BarnettEtAl2022.instReprGroupResult.repr }

def BarnettEtAl2022.pragmaticResult : GroupResult

Pragmatic group: weak evidence backfires (mean below 50). 95% CI: [32.3, 37.3] (paper p. 175).

Equations

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

def BarnettEtAl2022.literalResult : GroupResult

Literal group: no weak evidence effect (mean at 50). CIs not reported in paper.

Equations

• BarnettEtAl2022.literalResult = { listenerType := BarnettEtAl2022.ListenerType.literal, nParticipants := 238, meanSlider := 501 / 10, ci95Lower := none, ci95Upper := none }

theorem BarnettEtAl2022.pragmatic_backfire : pragmaticResult.meanSlider < 50

Pragmatic group shows backfire: mean significantly below 50 (midpoint)

theorem BarnettEtAl2022.literal_no_backfire : literalResult.meanSlider > 49

Literal group shows no backfire: mean at midpoint

theorem BarnettEtAl2022.groups_differ : pragmaticResult.meanSlider < literalResult.meanSlider

The two groups differ in the predicted direction

Model Comparison (Table 1)

inductive BarnettEtAl2022.ModelFamily : Type

Model families compared

• anchorAdjust : ModelFamily
• minAcceptable : ModelFamily
• rsaPragmatic : ModelFamily

@[implicit_reducible]

instance BarnettEtAl2022.instDecidableEqModelFamily : DecidableEq ModelFamily

Equations

• BarnettEtAl2022.instDecidableEqModelFamily x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance BarnettEtAl2022.instReprModelFamily : Repr ModelFamily

Equations

• BarnettEtAl2022.instReprModelFamily = { reprPrec := BarnettEtAl2022.instReprModelFamily.repr }

def BarnettEtAl2022.instReprModelFamily.repr : ModelFamily → ℕ → Std.Format

Equations

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

inductive BarnettEtAl2022.ModelVariant : Type

Model variant (how individual differences are handled)

• homogeneous : ModelVariant
• heterogeneous : ModelVariant
• speakerDependent : ModelVariant

@[implicit_reducible]

instance BarnettEtAl2022.instDecidableEqModelVariant : DecidableEq ModelVariant

Equations

• BarnettEtAl2022.instDecidableEqModelVariant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BarnettEtAl2022.instReprModelVariant.repr : ModelVariant → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance BarnettEtAl2022.instReprModelVariant : Repr ModelVariant

Equations

• BarnettEtAl2022.instReprModelVariant = { reprPrec := BarnettEtAl2022.instReprModelVariant.repr }

structure BarnettEtAl2022.ModelComparisonDatum : Type

Model comparison result from Table 1

• family : ModelFamily
• variant : ModelVariant
• logLikelihood : ℚ
• waic : ℚ
• waicSE : ℚ
• psisLoo : ℚ
• psisLooSE : ℚ

@[implicit_reducible]

instance BarnettEtAl2022.instReprModelComparisonDatum : Repr ModelComparisonDatum

Equations

• BarnettEtAl2022.instReprModelComparisonDatum = { reprPrec := BarnettEtAl2022.instReprModelComparisonDatum.repr }

def BarnettEtAl2022.instReprModelComparisonDatum.repr : ModelComparisonDatum → ℕ → Std.Format

Equations

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

def BarnettEtAl2022.modelComparison : List ModelComparisonDatum

Table 1 data

Equations

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

theorem BarnettEtAl2022.rsa_speaker_dep_best_likelihood : 12 > 82 / 10

The RSA speaker-dependent model has the best (highest) log-likelihood

theorem BarnettEtAl2022.rsa_speaker_dep_best_waic : -164 / 10 < -133 / 10

The RSA speaker-dependent model has the best (lowest) WAIC

Fitted Parameters

structure BarnettEtAl2022.FittedParams : Type

Fitted parameters for the best model (RSA speaker-dependent). β̂ = 2.26 and mixture weights from main text (p. 178); β̄ = 2.03 and ō = −0.13 from Fig 3B caption (p. 177).

• betaMAP : ℚ
• betaCV : ℚ
• responseOffsetCV : ℚ
• pragmaticMixWeight : ℚ
• literalMixWeight : ℚ

def BarnettEtAl2022.instReprFittedParams.repr : FittedParams → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance BarnettEtAl2022.instReprFittedParams : Repr FittedParams

Equations

• BarnettEtAl2022.instReprFittedParams = { reprPrec := BarnettEtAl2022.instReprFittedParams.repr }

def BarnettEtAl2022.bestModelParams : FittedParams

Equations

• BarnettEtAl2022.bestModelParams = { betaMAP := 226 / 100, betaCV := 203 / 100, responseOffsetCV := -13 / 100, pragmaticMixWeight := 99 / 100, literalMixWeight := 1 / 10 }

theorem BarnettEtAl2022.beta_positive : bestModelParams.betaMAP > 0

β > 0 provides strong support for non-zero persuasive bias

theorem BarnettEtAl2022.pragmatic_group_uses_j1 : bestModelParams.pragmaticMixWeight > 9 / 10

Pragmatic group is best explained by J1 (pragmatic listener model)

theorem BarnettEtAl2022.literal_group_uses_j0 : bestModelParams.literalMixWeight < 2 / 10

Literal group is best explained by J0 (literal listener model)

Model–Data Connection

theorem BarnettEtAl2022.model_predicts_interaction : RSA.ArgumentativeStrength.hasPositiveArgStr (↑(l0LongerQ Stick.s4)) priorLonger ∧ (l1Event Stick.s4 longer < l1Event Stick.s4 fun (w : StickWorld) => !longer w) ∧ pragmaticResult.meanSlider < 50 ∧ literalResult.meanSlider > 49

The RSA model predicts the qualitative pattern underlying the observed interaction between listener type and evidence strength (t(718) = 5.2, p < 0.001). The literal model (L0) assigns s4 positive argumentative strength, predicting no backfire. The pragmatic model (L1) shows backfire. The experiment confirms exactly this divergence: pragmatic participants' mean (34.7) falls below neutral (50), while literal participants' mean (50.1) does not.