@cite{barnett-griffiths-hawkins-2022}: A Pragmatic Account of the Weak Evidence Effect

@cite{barnett-griffiths-hawkins-2022}

Extends RSA with a persuasive speaker who has a goal state w* that may differ from the true world state w. The speaker's utility combines epistemic and persuasive components (Eq. 6):

U(u; w, w*) = U_epi(u; w) + β · U_pers(u; w*)

where U_epi = ln P_L0(w|u) and U_pers = ln P_L0(w*|u). The parameter β controls persuasive bias (β=0 recovers standard RSA).

Key Result: The Weak Evidence Effect

When β > 0, weak positive evidence can backfire: a pragmatic listener who expects the speaker to show the strongest available evidence infers that the absence of strong evidence means it doesn't exist, shifting beliefs in the opposite direction.

Stick Contest Domain

The paper's experiment uses 5 sticks from {1,...,9} (C(9,5)=126 worlds, midpoint 5). We formalize a simplified Stick Contest (3 sticks from {1,...,5}, 10 worlds, midpoint 3) that preserves the key structural properties: the prior favors ¬longer (P(longer)=0.4), and sticks have monotonically increasing L0(longer|·) values. The simplification enables verified interval arithmetic via rsa_predict.

RSAConfig Design

The paper's Eq. 8 gives:

S(u|w, w*=longer, β) ∝ L0(longer|u)^β · 𝟙[u ∈ w]

Since the paper fixes α=1 and treats αβ as a single parameter, RSAConfig's α plays the role of β. The s1Score uses precomputed L0(longer|u) values squared (β=2), gated by stick availability.

Findings

#	Finding	Theorem
1	L0: stick 5 is positive evidence for "longer"	l0_s5_positive
2	L0: stick 5 is the strongest evidence	l0_s5_strongest
3	L0: stick 1 is evidence against "longer"	l0_s1_negative
4	WEE: stick 4 backfires under L1 (β=2)	weak_evidence_effect
5	Strong evidence works: stick 5 favors "longer" under L1	strong_evidence_works
6	L0(longer	·) is monotone in stick length
7	Stick 4 has positive argStr yet backfires	argStr_positive_but_backfires
8	Model predicts the observed interaction effect	model_predicts_interaction
9	Pragmatic group shows backfire in experiment	pragmatic_backfire
10	RSA speaker-dependent model fits best	rsa_speaker_dep_best_waic

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 ⋯

@[implicit_reducible]

instance BarnettEtAl2022.instReprStick : Repr Stick

Equations

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

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.instInhabitedStick : Inhabited Stick

Equations

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

def BarnettEtAl2022.instInhabitedStick.default : Stick

Equations

• BarnettEtAl2022.instInhabitedStick.default = BarnettEtAl2022.Stick.s1

@[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.

def BarnettEtAl2022.instInhabitedStickWorld.default : StickWorld

Equations

• BarnettEtAl2022.instInhabitedStickWorld.default = BarnettEtAl2022.StickWorld.w123

@[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.IsLonger : StickWorld → Prop

A world is "longer" if the average stick length exceeds the midpoint (3). Equivalently, sum > 9 for 3 sticks. 4 of 10 worlds qualify.

Equations

• BarnettEtAl2022.IsLonger BarnettEtAl2022.StickWorld.w145 = True
• BarnettEtAl2022.IsLonger BarnettEtAl2022.StickWorld.w235 = True
• BarnettEtAl2022.IsLonger BarnettEtAl2022.StickWorld.w245 = True
• BarnettEtAl2022.IsLonger BarnettEtAl2022.StickWorld.w345 = True
• BarnettEtAl2022.IsLonger x✝ = False

@[implicit_reducible]

instance BarnettEtAl2022.instDecidablePredStickWorldIsLonger : DecidablePred IsLonger

Equations

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

def BarnettEtAl2022.l0LongerQ : Stick → ℚ

L0(longer|u) as ℚ for each stick. Each stick appears in C(4,2)=6 worlds; this gives the fraction where IsLonger holds.

• s1: 1/6 (only w145 is longer)
• s2: 2/6 = 1/3 (w235, w245)
• s3: 2/6 = 1/3 (w235, w345)
• s4: 3/6 = 1/2 (w145, w245, w345)
• s5: 4/6 = 2/3 (w145, w235, w245, w345)

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

def BarnettEtAl2022.priorLonger : ℚ

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

Equations

• BarnettEtAl2022.priorLonger = 2 / 5

def BarnettEtAl2022.s1ScoreQ (w : StickWorld) (u : Stick) : ℚ

S1 score as ℚ: L0(longer|u)^β · 𝟙[u ∈ w], at β=2. The squared L0 values are precomputed as literal fractions so that the reifier extracts concrete ℚ values from the ℚ→ℝ cast without needing to reduce function calls.

Equations

• BarnettEtAl2022.s1ScoreQ w BarnettEtAl2022.Stick.s1 = if BarnettEtAl2022.worldContains w BarnettEtAl2022.Stick.s1 = true then 1 / 36 else 0
• BarnettEtAl2022.s1ScoreQ w BarnettEtAl2022.Stick.s2 = if BarnettEtAl2022.worldContains w BarnettEtAl2022.Stick.s2 = true then 1 / 9 else 0
• BarnettEtAl2022.s1ScoreQ w BarnettEtAl2022.Stick.s3 = if BarnettEtAl2022.worldContains w BarnettEtAl2022.Stick.s3 = true then 1 / 9 else 0
• BarnettEtAl2022.s1ScoreQ w BarnettEtAl2022.Stick.s4 = if BarnettEtAl2022.worldContains w BarnettEtAl2022.Stick.s4 = true then 1 / 4 else 0
• BarnettEtAl2022.s1ScoreQ w BarnettEtAl2022.Stick.s5 = if BarnettEtAl2022.worldContains w BarnettEtAl2022.Stick.s5 = true then 4 / 9 else 0

noncomputable def BarnettEtAl2022.cfg : RSA.RSAConfig Stick StickWorld

@cite{barnett-griffiths-hawkins-2022} RSA with persuasive speaker.

The s1Score implements Eq. 8: S(u|w, longer, β) ∝ L0(longer|u)^β · 𝟙[u ∈ w]. The score is precomputed as s1ScoreQ (ℚ) and cast to ℝ, so that rsa_predict's reifier can extract the rational value directly.

Equations

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

theorem BarnettEtAl2022.l0_s5_positive : cfg.L0_marginal () Stick.s5 IsLonger > cfg.L0_marginal () Stick.s5 fun (w : StickWorld) => ¬IsLonger w

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 : cfg.L0_marginal () Stick.s5 IsLonger > cfg.L0_marginal () Stick.s4 IsLonger

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

theorem BarnettEtAl2022.l0_s1_negative : (cfg.L0_marginal () Stick.s1 fun (w : StickWorld) => ¬IsLonger w) > cfg.L0_marginal () Stick.s1 IsLonger

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).

theorem BarnettEtAl2022.weak_evidence_effect : (cfg.L1_marginal Stick.s4 fun (w : StickWorld) => ¬IsLonger w) > cfg.L1_marginal Stick.s4 IsLonger

Weak evidence effect: at β=2, showing stick 4 (positive literal evidence) decreases the pragmatic listener's belief in "longer" below the prior.

The listener reasons: "If the true average were high, the speaker would have had stronger sticks (like 5) available and would have shown them instead. The fact that they showed a 4 implies they lacked stronger evidence."

L1 assigns more posterior mass to ¬longer than longer worlds after seeing s4.

theorem BarnettEtAl2022.strong_evidence_works : cfg.L1_marginal Stick.s5 IsLonger > cfg.L1_marginal Stick.s5 fun (w : StickWorld) => ¬IsLonger w

Strong evidence does NOT backfire: stick 5 increases belief at β=2.

The strongest available evidence is always effective because it cannot be "explained away" by the absence of something better.

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 ∧ (cfg.L1_marginal Stick.s4 fun (w : StickWorld) => ¬IsLonger w) > cfg.L1_marginal Stick.s4 IsLonger

The weak evidence effect shows that argumentatively positive evidence can still backfire under a pragmatic listener model. This is the core insight connecting @cite{barnett-griffiths-hawkins-2022} to @cite{cummins-franke-2021}'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.

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 ⋯

@[implicit_reducible]

instance BarnettEtAl2022.instReprEvidenceStrength : Repr EvidenceStrength

Equations

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

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

Equations

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

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 ⋯

@[implicit_reducible]

instance BarnettEtAl2022.instReprFirstContestant : Repr FirstContestant

Equations

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

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

Equations

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

structure BarnettEtAl2022.StickContestDesign : Type

Stick Contest design parameters

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

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

Equations

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

@[implicit_reducible]

instance BarnettEtAl2022.instReprStickContestDesign : Repr StickContestDesign

Equations

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

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 : ℚ

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

Equations

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

@[implicit_reducible]

instance BarnettEtAl2022.instReprInteractionEffect : Repr InteractionEffect

Equations

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

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 ℚ

@[implicit_reducible]

instance BarnettEtAl2022.instReprGroupResult : Repr GroupResult

Equations

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

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

Equations

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

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

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

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)

theorem BarnettEtAl2022.model_predicts_interaction : RSA.ArgumentativeStrength.hasPositiveArgStr (l0LongerQ Stick.s4) priorLonger ∧ (cfg.L1_marginal Stick.s4 fun (w : StickWorld) => ¬IsLonger w) > cfg.L1_marginal Stick.s4 IsLonger ∧ 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.