Rees, Reksnes, and Rohde (2026): Why are you telling me this? The availability and timing of relevance inferences

Rees, Reksnes and Rohde ask why an addressee takes a trivial remark such as the library walls are blue to mean that the walls used to be a different colour. A speaker makes a remark only when it is worth enough to her, and a quiet speaker's bar is higher. Here the addressee conditions a prior over whether the situation changed on the pasts in which the speaker would have spoken; a change can make a trivial remark worth making only to a speaker who knows the situation over time. Across four experiments the inference is drawn more often for a knowledgeable speaker and, in the second, for a quiet one. Two verification experiments with opposite question polarity locate a cost when the inference is endorsed, which the paper attributes to considering the alternative situation.

Main statements

• Speaker.prior_lt_posterior_iff: speaking raises the probability that the situation changed exactly when the remark is trivial on its own and a change would make it worth making.
• Speaker.posterior_eq_prior_of_not_knowledgeable: a speaker who does not know the situation over time conveys nothing about its past by speaking.
• Speaker.prior_lt_posterior_of_bar_le: a quieter speaker licenses whatever a more talkative one does, as long as a change would still be worth mentioning to her.
• ResponseModel.exp3_no_eq_exp4_no, AdditiveModel.yes_eq_yes_of_no_eq_no: if considering the alternative is the cost, the no answers of the two experiments take equally long, as found; separate costs of a negative answer and of the inference could not also give the slower inference-endorsing yes.

Implementation notes

Conditioning on the decision to speak is Rohde, Hoek, Keshev and Franke's account of the listener's expectation, which the paper cites. The speaker speaks exactly when the remark's worth to her meets her bar, so the model says which inferences are available, not how often participants draw them. Every item describes a situation that may plausibly have changed. The emphasis cue and the paper's post hoc account of the interaction in its second experiment are not modelled.

References

• A. Rees, V. Reksnes, H. Rohde, Why are you telling me this? The availability and timing of relevance inferences (2026)
• H. Rohde, J. Hoek, M. Keshev, M. Franke, This better be interesting: a speaker's decision to speak cues listeners to expect informative content (2022)

The decision to speak

inductive ReesReksnesRohde2026.Past : Type

A past of the described situation says whether, a few months ago, it was the same as now or different.

• same : Past
• different : Past

@[instance_reducible]

instance ReesReksnesRohde2026.instDecidableEqPast : DecidableEq Past

Equations

• ReesReksnesRohde2026.instDecidableEqPast x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ReesReksnesRohde2026.instFintypePast : Fintype Past

Equations

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

@[instance_reducible]

instance ReesReksnesRohde2026.instMeasurableSpacePast : MeasurableSpace Past

Equations

• ReesReksnesRohde2026.instMeasurableSpacePast = ⊤

instance ReesReksnesRohde2026.instDiscreteMeasurableSpacePast : DiscreteMeasurableSpace Past

instance ReesReksnesRohde2026.instNonemptyPast : Nonempty Past

structure ReesReksnesRohde2026.Speaker : Type

The addressee models the speaker making a remark by what the remark is worth to her in each past of the situation and by the bar a remark must clear for her to make it.

• worth : Past → ℝ
• bar : ℝ

def ReesReksnesRohde2026.Speaker.Knowledgeable (s : Speaker) : Prop

The speaker knows the situation over time when the worth of her remark depends on its past.

Equations

• s.Knowledgeable = (s.worth ReesReksnesRohde2026.Past.same ≠ s.worth ReesReksnesRohde2026.Past.different)

def ReesReksnesRohde2026.Speaker.Trivial (s : Speaker) : Prop

The remark is trivial when, with nothing changed, it falls short of the speaker's bar.

Equations

• s.Trivial = (s.worth ReesReksnesRohde2026.Past.same < s.bar)

noncomputable def ReesReksnesRohde2026.Speaker.spoke (s : Speaker) : ProbabilityTheory.Kernel Past Bool

The speaker makes the remark exactly in the pasts in which it is worth it to her.

Equations

• s.spoke = ProbabilityTheory.Kernel.deterministic (fun (p : ReesReksnesRohde2026.Past) => decide (s.bar ≤ s.worth p)) ⋯

instance ReesReksnesRohde2026.Speaker.instIsMarkovKernelPastBoolSpoke (s : Speaker) : ProbabilityTheory.IsMarkovKernel s.spoke

theorem ReesReksnesRohde2026.Speaker.spoke_real_true (s : Speaker) (p : Past) : (s.spoke p).real {true} = if s.bar ≤ s.worth p then 1 else 0

theorem ReesReksnesRohde2026.Speaker.spoke_comp_apply_true {s : Speaker} (μ : MeasureTheory.Measure Past) : (μ.bind ⇑s.spoke) {true} = μ {p : Past | s.bar ≤ s.worth p}

The prior probability that the speaker speaks is that of the pasts in which the remark is worth it to her.

theorem ReesReksnesRohde2026.Speaker.Trivial.mono {s t : Speaker} (h : s.Trivial) (hw : s.worth = t.worth) (hb : s.bar ≤ t.bar) : t.Trivial

A quieter speaker with the same view of the situation finds trivial whatever a more talkative one does.

theorem ReesReksnesRohde2026.Speaker.spoke_comp_apply_true_eq_zero {s : Speaker} (μ : MeasureTheory.Measure Past) (hk : ¬s.Knowledgeable) (ht : s.Trivial) : (μ.bind ⇑s.spoke) {true} = 0

A speaker who does not know the situation over time would stay silent about a trivial remark whatever its past, so no past explains her making it.

theorem ReesReksnesRohde2026.Speaker.posterior_spoke {s : Speaker} (μ : MeasureTheory.Measure Past) [MeasureTheory.IsProbabilityMeasure μ] (hx : (μ.bind ⇑s.spoke) {true} ≠ 0) : (ProbabilityTheory.posterior s.spoke μ) true = μ[|{p : Past | s.bar ≤ s.worth p}]

Hearing the remark conditions the prior on the pasts in which the speaker would make it.

theorem ReesReksnesRohde2026.Speaker.prior_lt_posterior_iff {s : Speaker} (μ : MeasureTheory.Measure Past) [MeasureTheory.IsProbabilityMeasure μ] (hx : (μ.bind ⇑s.spoke) {true} ≠ 0) (hs : μ {Past.same} ≠ 0) (hd : μ {Past.different} ≠ 0) : μ.real {Past.different} < ((ProbabilityTheory.posterior s.spoke μ) true).real {Past.different} ↔ s.Trivial ∧ s.bar ≤ s.worth Past.different

Speaking raises the probability that the situation used to be different exactly when the remark is trivial with nothing changed and worth making had the situation changed.

theorem ReesReksnesRohde2026.Speaker.posterior_eq_prior_of_not_knowledgeable {s : Speaker} (μ : MeasureTheory.Measure Past) [MeasureTheory.IsProbabilityMeasure μ] (hk : ¬s.Knowledgeable) (hx : (μ.bind ⇑s.spoke) {true} ≠ 0) : (ProbabilityTheory.posterior s.spoke μ) true = μ

A speaker who does not know the situation over time makes the remark in every past or in none, so hearing it leaves the prior unchanged.

theorem ReesReksnesRohde2026.Speaker.not_prior_lt_posterior_of_not_knowledgeable {s : Speaker} (μ : MeasureTheory.Measure Past) [MeasureTheory.IsProbabilityMeasure μ] (hk : ¬s.Knowledgeable) (hx : (μ.bind ⇑s.spoke) {true} ≠ 0) : ¬μ.real {Past.different} < ((ProbabilityTheory.posterior s.spoke μ) true).real {Past.different}

In particular such a speaker never licenses the inference that the situation changed, as Suzy cannot at the Prime Minister's office.

theorem ReesReksnesRohde2026.Speaker.prior_lt_posterior_of_bar_le {s t : Speaker} (μ : MeasureTheory.Measure Past) [MeasureTheory.IsProbabilityMeasure μ] (hw : s.worth = t.worth) (hb : s.bar ≤ t.bar) (ht : t.bar ≤ t.worth Past.different) (hx : (μ.bind ⇑s.spoke) {true} ≠ 0) (hx' : (μ.bind ⇑t.spoke) {true} ≠ 0) (hs : μ {Past.same} ≠ 0) (hd : μ {Past.different} ≠ 0) (h : μ.real {Past.different} < ((ProbabilityTheory.posterior s.spoke μ) true).real {Past.different}) : μ.real {Past.different} < ((ProbabilityTheory.posterior t.spoke μ) true).real {Past.different}

A quieter speaker with the same view of the situation licenses the inference whenever a more talkative one does, as long as a change would still be worth mentioning to her.

The timing of the inference

def ReesReksnesRohde2026.asserted : Past → Bool → Past

The past that a yes or a no to was it q a few months ago? asserts.

Equations

• ReesReksnesRohde2026.asserted x✝ true = x✝
• ReesReksnesRohde2026.asserted ReesReksnesRohde2026.Past.same false = ReesReksnesRohde2026.Past.different
• ReesReksnesRohde2026.asserted ReesReksnesRohde2026.Past.different false = ReesReksnesRohde2026.Past.same

def ReesReksnesRohde2026.Endorses (q : Past) (a : Bool) : Prop

An answer endorses the inference when it asserts that the situation was different, as no to was it the same? does in Experiment 3 and yes to was it different? in Experiment 4.

Equations

• ReesReksnesRohde2026.Endorses q a = (ReesReksnesRohde2026.asserted q a = ReesReksnesRohde2026.Past.different)

def ReesReksnesRohde2026.ConsidersAlternative (q : Past) (a : Bool) : Prop

Answering considers the alternative to the situation as presented when the answer is negative or endorses the inference.

Equations

• ReesReksnesRohde2026.ConsidersAlternative q a = (a = false ∨ ReesReksnesRohde2026.Endorses q a)

@[instance_reducible]

instance ReesReksnesRohde2026.instDecidableRelPastBoolEndorses : DecidableRel Endorses

Equations

• ReesReksnesRohde2026.instDecidableRelPastBoolEndorses x✝¹ x✝ = ReesReksnesRohde2026.instDecidableRelPastBoolEndorses._aux_1 x✝¹ x✝

@[instance_reducible]

instance ReesReksnesRohde2026.instDecidableRelPastBoolConsidersAlternative : DecidableRel ConsidersAlternative

Equations

• ReesReksnesRohde2026.instDecidableRelPastBoolConsidersAlternative x✝¹ x✝ = { decide := decide (x✝ = false) || decide (ReesReksnesRohde2026.Endorses x✝¹ x✝), reflects_decide := ⋯ }

structure ReesReksnesRohde2026.ResponseModel : Type

In the paper's account of the verification times, an answer takes a base time, and longer by a fixed cost when it considers the alternative to the situation as presented.

• base : ℝ
• alternative : ℝ

def ReesReksnesRohde2026.ResponseModel.rt (m : ResponseModel) (q : Past) (a : Bool) : ℝ

The predicted time to answer a to was it q?.

Equations

• m.rt q a = m.base + if ReesReksnesRohde2026.ConsidersAlternative q a then m.alternative else 0

structure ReesReksnesRohde2026.AdditiveModel : Type

An additive model of the verification times with separate costs of a negative answer and of endorsing the inference.

• base : ℝ
• negative : ℝ
• inference : ℝ

def ReesReksnesRohde2026.AdditiveModel.rt (m : AdditiveModel) (q : Past) (a : Bool) : ℝ

The predicted time to answer a to was it q?.

Equations

• m.rt q a = (m.base + if a = false then m.negative else 0) + if ReesReksnesRohde2026.Endorses q a then m.inference else 0

theorem ReesReksnesRohde2026.ResponseModel.exp3_contrast (m : ResponseModel) : m.rt Past.same false - m.rt Past.same true = m.alternative

In Experiment 3 the inference-endorsing no is slower than yes by the cost of considering the alternative.

theorem ReesReksnesRohde2026.ResponseModel.exp4_yes_eq_no (m : ResponseModel) : m.rt Past.different true = m.rt Past.different false

In Experiment 4 yes and no take equally long.

theorem ReesReksnesRohde2026.ResponseModel.yes_contrast (m : ResponseModel) : m.rt Past.different true - m.rt Past.same true = m.alternative

The inference-endorsing yes of Experiment 4 is slower than the yes of Experiment 3 by the cost of considering the alternative.

theorem ReesReksnesRohde2026.ResponseModel.exp3_no_eq_exp4_no (m : ResponseModel) : m.rt Past.same false = m.rt Past.different false

The no answers of the two experiments take equally long, since both consider the alternative.

theorem ReesReksnesRohde2026.AdditiveModel.exp3_confounded (m : AdditiveModel) : m.rt Past.same false - m.rt Past.same true = m.negative + m.inference

In Experiment 3 the contrast between no and yes confounds the cost of the inference with that of a negative answer.

theorem ReesReksnesRohde2026.AdditiveModel.yes_contrast (m : AdditiveModel) : m.rt Past.different true - m.rt Past.same true = m.inference

The contrast between the yes answers of the two experiments isolates the cost of the inference.

theorem ReesReksnesRohde2026.AdditiveModel.yes_eq_yes_of_no_eq_no (m : AdditiveModel) (h : m.rt Past.same false = m.rt Past.different false) : m.rt Past.different true = m.rt Past.same true

If the no answers of the two experiments take equally long, so do the yes answers, so the additive model cannot give the paper's pattern.