Barnett, Griffiths and Hawkins (2022): A Pragmatic Account of the Weak Evidence Effect

In the Stick Contest a judge decides whether five hidden sticks, each one to nine inches long, are longer than five inches on average, after a contestant who wants the verdict longer reveals one of them. A literal listener takes the stick at face value. A persuasive speaker reveals a stick with weight L0(longer | u)^β, so a pragmatic listener who expects such a speaker takes a weak stick as a sign that no stronger one was available.

The pragmatic listener discounts every stick and still believes more in longer the longer the stick shown. The sticks that backfire, evidence for longer that lowers the belief in it below the prior, therefore form an interval, and there are none without a persuasive goal. As the bias grows the speaker shows the longest stick, the listener's belief tends to the probability of longer given that the longest stick has the length shown, and the sticks of length five to seven backfire while the longer ones do not.

Main results

• pragmaticListener_real_le_literal: the pragmatic listener discounts every stick.
• pragmaticListener_real_mono: the belief in longer grows with the stick shown.
• backfires_zero, ordConnected_backfires: the backfiring sticks form an interval, empty without a persuasive goal.
• tendsto_speaker_real_singleton_atTop, tendsto_pragmaticListener_real_atTop: as the bias grows the speaker shows the longest stick and the listener conditions on it being the longest.
• eventually_backfires_eq: for a strongly biased speaker the backfiring sticks are those of length five to seven.

Implementation notes

• As in the authors' code, the sticks are independent and uniform, an average of exactly five counts as longer, the speaker chooses which of the five sticks to reveal, and the literal listener conditions on one given stick having the length shown. The verdict is computed exactly, where the code's floating-point mean misclassifies some ties.
• The paper's Figure 3A used sticks of length 0 to 10 and measures the effect against 0.5. Here sticks run from 1 to 9, as in the experiment and the fitted model, and the effect is measured against the prior; with these sticks a shown 8 does not backfire.
• Counts are tabulated by total one stick at a time, so the kernel never enumerates tuples.

TODO

• The finite-bias values of the simulation are numerical: near the fitted bias β ≈ 2 sticks of length five and six backfire, and the backfiring range widens with β. The belief itself is not antitone in β (a shown 9 is not), so the widening is a property of the set.

References

• [BGH22]
• [Hol74]

The Stick Contest

def BarnettEtAl2022.length (i : Fin 9) : ℕ

The length of a stick, from 1 to 9 inches.

Equations

• BarnettEtAl2022.length i = ↑i + 1

theorem BarnettEtAl2022.length_mono : Monotone length

def BarnettEtAl2022.longer (n : ℕ) : Set (Fin (n + 1) → Fin 9)

The verdict longer holds of n + 1 sticks whose average is at least the midpoint of five inches.

Equations

• BarnettEtAl2022.longer n = {w : Fin (n + 1) → Fin 9 | 5 * (n + 1) ≤ ∑ i : Fin (n + 1), BarnettEtAl2022.length (w i)}

@[instance_reducible]

instance BarnettEtAl2022.instDecidableMemForallFinHAddNatOfNatSetLonger (n : ℕ) (w : Fin (n + 1) → Fin 9) : Decidable (w ∈ longer n)

Equations

• BarnettEtAl2022.instDecidableMemForallFinHAddNatOfNatSetLonger n w = (5 * (n + 1)).decLe (∑ i : Fin (n + 1), BarnettEtAl2022.length (w i))

theorem BarnettEtAl2022.isUpperSet_longer (n : ℕ) : IsUpperSet (longer n)

theorem BarnettEtAl2022.cons_mem_longer {n : ℕ} {u : Fin 9} {x : Fin n → Fin 9} : Fin.cons u x ∈ longer n ↔ 5 * (n + 1) ≤ length u + ∑ i : Fin n, length (x i)

theorem BarnettEtAl2022.insertNth_mem_longer {n : ℕ} (i : Fin (n + 1)) (u : Fin 9) (x : Fin n → Fin 9) : i.insertNth u x ∈ longer n ↔ Fin.cons u x ∈ longer n

Which position holds the shown stick does not matter to the verdict.

theorem BarnettEtAl2022.exists_sum_length_eq {n t : ℕ} (h₁ : n ≤ t) (h₂ : t ≤ 9 * n) : ∃ (x : Fin n → Fin 9), ∑ i : Fin n, length (x i) = t

Every total between n and 9 * n inches is the total of some n sticks.

theorem BarnettEtAl2022.sum_cons {n : ℕ} {M : Type u_1} [AddCommMonoid M] (f : (Fin (n + 1) → Fin 9) → M) : ∑ w : Fin (n + 1) → Fin 9, f w = ∑ u : Fin 9, ∑ x : Fin n → Fin 9, f (Fin.cons u x)

Sums over n + 1 sticks are sums over the first stick and the other n.

The literal listener

noncomputable def BarnettEtAl2022.literal (n : ℕ) (u : Fin 9) : ℝ

The literal listener's belief in longer is that of the uniform prior conditioned on the revealed stick, taken to be the first, having length u.

Equations

• BarnettEtAl2022.literal n u = (ProbabilityTheory.uniformOn {w : Fin (n + 1) → Fin 9 | w 0 = u}).real (BarnettEtAl2022.longer n)

theorem BarnettEtAl2022.literal_eq_card {n : ℕ} (u : Fin 9) : literal n u = ↑{x : Fin n → Fin 9 | Fin.cons u x ∈ longer n}.card / 9 ^ n

theorem BarnettEtAl2022.prior_eq_average {n : ℕ} : (ProbabilityTheory.uniformOn Set.univ).real (longer n) = (∑ u : Fin 9, literal n u) / 9

The prior belief in longer is the average of the literal beliefs over the stick shown.

theorem BarnettEtAl2022.literal_pos {n : ℕ} [NeZero n] (u : Fin 9) : 0 < literal n u

theorem BarnettEtAl2022.literal_strictMono {n : ℕ} [NeZero n] : StrictMono (literal n)

Literal support for longer grows strictly with the stick shown.

theorem BarnettEtAl2022.literal_mono {n : ℕ} [NeZero n] : Monotone (literal n)

The persuasive speaker and the pragmatic listener

noncomputable def BarnettEtAl2022.reveal (n : ℕ) (β : ℝ) : ProbabilityTheory.Kernel (Fin (n + 1) → Fin 9) (Fin (n + 1))

The persuasive speaker chooses which stick to reveal, with weight L0(longer | u)^β.

Equations

• BarnettEtAl2022.reveal n β = ProbabilityTheory.Kernel.ofWeights fun (w : Fin (n + 1) → Fin 9) (i : Fin (n + 1)) => ENNReal.ofReal (BarnettEtAl2022.literal n (w i) ^ β)

theorem BarnettEtAl2022.reveal_eq_softmax {n : ℕ} [NeZero n] (β : ℝ) : reveal n β = ProbabilityTheory.Kernel.softmax fun (w : Fin (n + 1) → Fin 9) (i : Fin (n + 1)) => ↑(β * Real.log (literal n (w i)))

The revealing speaker is the RSA speaker whose utility is β times the log of the literal support for longer.

instance BarnettEtAl2022.instIsMarkovKernelForallFinHAddNatOfNatReveal {n : ℕ} [NeZero n] (β : ℝ) : ProbabilityTheory.IsMarkovKernel (reveal n β)

noncomputable def BarnettEtAl2022.speaker (n : ℕ) (β : ℝ) : ProbabilityTheory.Kernel (Fin (n + 1) → Fin 9) (Fin 9)

The speaker as the listener hears it reports the length of the revealed stick.

Equations

• BarnettEtAl2022.speaker n β = ProbabilityTheory.Kernel.ofFunOfCountable fun (w : Fin (n + 1) → Fin 9) => MeasureTheory.Measure.map w ((BarnettEtAl2022.reveal n β) w)

instance BarnettEtAl2022.instIsMarkovKernelForallFinHAddNatOfNatSpeaker {n : ℕ} [NeZero n] (β : ℝ) : ProbabilityTheory.IsMarkovKernel (speaker n β)

noncomputable def BarnettEtAl2022.pragmaticListener (n : ℕ) (β : ℝ) : ProbabilityTheory.Kernel (Fin 9) (Fin (n + 1) → Fin 9)

The pragmatic listener inverts the speaker against the uniform prior.

Equations

• BarnettEtAl2022.pragmaticListener n β = RSA.listener (ProbabilityTheory.uniformOn Set.univ) ⇑(BarnettEtAl2022.speaker n β)

noncomputable def BarnettEtAl2022.share (n : ℕ) (β : ℝ) (u : Fin 9) (x : Fin n → Fin 9) : ℝ

The speaker's probability of revealing the stick u rather than one of the others x.

Equations

• BarnettEtAl2022.share n β u x = BarnettEtAl2022.literal n u ^ β / (BarnettEtAl2022.literal n u ^ β + ∑ i : Fin n, BarnettEtAl2022.literal n (x i) ^ β)

theorem BarnettEtAl2022.reveal_real_singleton {n : ℕ} [NeZero n] (β : ℝ) (w : Fin (n + 1) → Fin 9) (i : Fin (n + 1)) : ((reveal n β) w).real {i} = literal n (w i) ^ β / ∑ j : Fin (n + 1), literal n (w j) ^ β

theorem BarnettEtAl2022.speaker_real_singleton {n : ℕ} [NeZero n] (β : ℝ) (w : Fin (n + 1) → Fin 9) (u : Fin 9) : ((speaker n β) w).real {u} = ∑ i : Fin (n + 1) with w i = u, ((reveal n β) w).real {i}

theorem BarnettEtAl2022.speaker_real_singleton_eq_mul {n : ℕ} [NeZero n] (β : ℝ) (w : Fin (n + 1) → Fin 9) (u : Fin 9) : ((speaker n β) w).real {u} = ↑{i : Fin (n + 1) | w i = u}.card * (literal n u ^ β / ∑ j : Fin (n + 1), literal n (w j) ^ β)

theorem BarnettEtAl2022.share_pos {n : ℕ} [NeZero n] (β : ℝ) (u : Fin 9) (x : Fin n → Fin 9) : 0 < share n β u x

theorem BarnettEtAl2022.pragmaticListener_real_longer {n : ℕ} [NeZero n] (β : ℝ) (u : Fin 9) : ((pragmaticListener n β) u).real (longer n) = (∑ x : Fin n → Fin 9 with Fin.cons u x ∈ longer n, share n β u x) / ∑ x : Fin n → Fin 9, share n β u x

The pragmatic listener's belief in longer is the share-weighted proportion of the other sticks on which the shown stick makes longer true, as in the authors' code.

Discounting

theorem BarnettEtAl2022.share_antitone {n : ℕ} [NeZero n] {β : ℝ} (hβ : 0 ≤ β) (u : Fin 9) : Antitone (share n β u)

The share of the shown stick falls as the other sticks grow.

theorem BarnettEtAl2022.share_mul_share_le {n : ℕ} [NeZero n] {β : ℝ} (hβ : 0 ≤ β) {u v : Fin 9} (huv : u ≤ v) (x y : Fin n → Fin 9) : share n β u x * share n β v y ≤ share n β u (x ⊓ y) * share n β v (x ⊔ y)

For u ≤ v the shares of showing u and of showing v satisfy the condition of Holley's inequality, so a longer shown stick moves the share up the lattice of the other sticks.

theorem BarnettEtAl2022.pragmaticListener_real_le_literal {n : ℕ} [NeZero n] {β : ℝ} (hβ : 0 ≤ β) (u : Fin 9) : ((pragmaticListener n β) u).real (longer n) ≤ literal n u

The pragmatic listener discounts every stick.

theorem BarnettEtAl2022.pragmaticListener_zero {n : ℕ} [NeZero n] (u : Fin 9) : ((pragmaticListener n 0) u).real (longer n) = literal n u

Without a persuasive goal the pragmatic listener is the literal one.

theorem BarnettEtAl2022.pragmaticListener_real_mono {n : ℕ} [NeZero n] {β : ℝ} (hβ : 0 ≤ β) : Monotone fun (u : Fin 9) => ((pragmaticListener n β) u).real (longer n)

The pragmatic belief in longer grows with the stick shown.

def BarnettEtAl2022.backfires (n : ℕ) (β : ℝ) : Set (Fin 9)

A stick backfires at bias β when it is literal evidence for longer but, revealed by the persuasive speaker, lowers the belief in longer below the prior.

Equations

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

theorem BarnettEtAl2022.backfires_zero {n : ℕ} [NeZero n] : backfires n 0 = ∅

theorem BarnettEtAl2022.ordConnected_backfires {n : ℕ} [NeZero n] {β : ℝ} (hβ : 0 ≤ β) : (backfires n β).OrdConnected

The sticks that backfire form an interval.

A fully persuasive speaker

theorem BarnettEtAl2022.tendsto_reveal_real_singleton_atTop {n : ℕ} [NeZero n] (w : Fin (n + 1) → Fin 9) (i : Fin (n + 1)) : Filter.Tendsto (fun (β : ℝ) => ((reveal n β) w).real {i}) Filter.atTop (nhds ((if w i = Finset.univ.sup w then 1 else 0) / ↑{j : Fin (n + 1) | w j = Finset.univ.sup w}.card))

As the bias grows the speaker reveals one of the longest sticks, each with equal probability.

theorem BarnettEtAl2022.tendsto_speaker_real_singleton_atTop {n : ℕ} [NeZero n] (w : Fin (n + 1) → Fin 9) (u : Fin 9) : Filter.Tendsto (fun (β : ℝ) => ((speaker n β) w).real {u}) Filter.atTop (nhds (if u = Finset.univ.sup w then 1 else 0))

As the bias grows the speaker shows the longest stick with certainty.

theorem BarnettEtAl2022.tendsto_pragmaticListener_real_atTop {n : ℕ} [NeZero n] (u : Fin 9) (E : Set (Fin (n + 1) → Fin 9)) : Filter.Tendsto (fun (β : ℝ) => ((pragmaticListener n β) u).real E) Filter.atTop (nhds ((ProbabilityTheory.uniformOn {w : Fin (n + 1) → Fin 9 | Finset.univ.sup w = u}).real E))

As the bias grows the pragmatic listener's beliefs tend to the uniform prior conditioned on the shown stick being the longest.

theorem BarnettEtAl2022.listener_dirac_sup {n : ℕ} (u : Fin 9) : (RSA.listener (ProbabilityTheory.uniformOn Set.univ) fun (w : Fin (n + 1) → Fin 9) => MeasureTheory.Measure.dirac (Finset.univ.sup w)) u = ProbabilityTheory.uniformOn {w : Fin (n + 1) → Fin 9 | Finset.univ.sup w = u}

A listener who expects the longest stick to be shown conditions the uniform prior on the shown stick being the longest.

Counting sticks by their total

Five sticks

theorem BarnettEtAl2022.card_cons_mem_longer (u : Fin 9) : {x : Fin 4 → Fin 9 | Fin.cons u x ∈ longer 4}.card = ![1680, 2100, 2556, 3036, 3525, 4005, 4461, 4881, 5256] u

The other four sticks on which each stick shown makes longer true.

theorem BarnettEtAl2022.literal_eq (u : Fin 9) : literal 4 u = ![1680, 2100, 2556, 3036, 3525, 4005, 4461, 4881, 5256] u / 6561

The literal listener's belief in longer for each stick shown, the β = 0 column of the simulation.

theorem BarnettEtAl2022.prior_eq : (ProbabilityTheory.uniformOn Set.univ).real (longer 4) = 3500 / 6561

theorem BarnettEtAl2022.prior_lt_literal_iff {u : Fin 9} : (ProbabilityTheory.uniformOn Set.univ).real (longer 4) < literal 4 u ↔ 5 ≤ length u

The sticks of length five and up are literal evidence for longer.

theorem BarnettEtAl2022.limit_eq (u : Fin 9) : (ProbabilityTheory.uniformOn {w : Fin 5 → Fin 9 | Finset.univ.sup w = u}).real (longer 4) = ![0, 0, 0, 0, 1 / 2101, 251 / 4651, 2471 / 9031, 8821 / 15961, 19956 / 26281] u

The belief in longer given that the longest of the five sticks has length u, the limit of the pragmatic listener's belief as the bias grows.

theorem BarnettEtAl2022.eventually_backfires_eq : ∀ᶠ (β : ℝ) in Filter.atTop, backfires 4 β = length ⁻¹' Set.Icc 5 7

For a strongly enough biased speaker the sticks that backfire are exactly those of length five to seven.