Bale, Noguchi, Rolland and Barner (2025): Competence by Default: Do Listeners Assume That Speakers Are Knowledgeable When Computing Conversational Inferences?

A strong scalar implicature needs more than the weak one. From some the hearer infers that the speaker does not know that all holds, and only with competence, the speaker knowing whether all holds, does this become knowledge that all is false. Bale, Noguchi, Rolland and Barner test two hypotheses about competence. Under competence by default, after Geurts and after van Rooij and Schulz, the hearer assumes it and cancels it when the speaker's contextual knowledge state contradicts it. Under contextual licensing, after Soames and Horn, it is adopted only when the context supplies it. Farmer Brown opens two of three boxes, both with red cubes, looks or does not look into the third, and says that some or all of the boxes have red cubes; the participant is asked whether the third box has red cubes. The speaker's knowledge states are the observation states of Goodman and Stuhlmüller.

Integrating the speaker's state, the two hypotheses give the same answers. They come apart only when integration fails, where a hearer who keeps the default derives the strong implicature from an ignorant speaker. Participants under cognitive load answered no to the ignorant speaker's some more than twice as often as those without load, while the knowledgeable speaker's some showed only the usual small reduction.

Main statements

• competent_iff_looked: the speaker is competent about all exactly when he looked into the third box.
• competenceDefault_eq_contextual: with integration the default is cancelled exactly where the context contradicts it, so the two hypotheses agree.
• load_diverges, load_agrees_of_knowledgeable: without integration the default yields the strong implicature from the ignorant speaker and nothing new from the knowledgeable one.
• rows_expected: the expected response in each trial type is the contextual-licensing answer.

References

• [BNRB25]
• [Geu10]
• [Soa82]
• [Hor89]
• [vRS04]
• [GS13]

Worlds, evidence and knowledge states

def BaleEtAl2025.prop (q : GoodmanStuhlmuller2013.QUtt) : Set (Fin 4)

The proposition a quantified statement about the three boxes expresses.

Equations

• BaleEtAl2025.prop q = ↑q.extension

@[instance_reducible]

instance BaleEtAl2025.instDecidablePredFinOfNatNatMemSetProp (q : GoodmanStuhlmuller2013.QUtt) : DecidablePred fun (x : Fin 4) => x ∈ prop q

Equations

• BaleEtAl2025.instDecidablePredFinOfNatNatMemSetProp q w = decidable_of_iff (w ∈ q.extension) ⋯

@[reducible, inline]

abbrev BaleEtAl2025.all : Set (Fin 4)

The statement all of the boxes have red cubes is the alternative, and the question asked.

Equations

• BaleEtAl2025.all = BaleEtAl2025.prop GoodmanStuhlmuller2013.QUtt.all

def BaleEtAl2025.seen : Set (Fin 4)

The participant sees that boxes 1 and 2 have red cubes.

Equations

• BaleEtAl2025.seen = {w : Fin 4 | 2 ≤ ↑w}

@[instance_reducible]

instance BaleEtAl2025.instDecidablePredFinOfNatNatMemSetSeen : DecidablePred fun (x : Fin 4) => x ∈ seen

Equations

• BaleEtAl2025.instDecidablePredFinOfNatNatMemSetSeen w = { decide := Nat.ble 2 ↑w, reflects_decide := ⋯ }

def BaleEtAl2025.speakerState (a w : Fin 4) : Set (Fin 4)

After looking into a boxes, boxes 1 and 2 among them, Farmer Brown knows in world w that the world is one of those compatible with the red cubes he saw.

Equations

• BaleEtAl2025.speakerState a w = ↑(GoodmanStuhlmuller2013.compatible ↑a ⟨min ↑a ↑w, ⋯⟩)

@[instance_reducible]

instance BaleEtAl2025.instDecidablePredFinOfNatNatMemSetSpeakerState (a w : Fin 4) : DecidablePred fun (x : Fin 4) => x ∈ speakerState a w

Equations

• BaleEtAl2025.instDecidablePredFinOfNatNatMemSetSpeakerState a w x✝ = decidable_of_iff (ProbabilityTheory.hypergeometricCount 3 ↑x✝ ↑a ↑⟨min ↑a ↑w, ⋯⟩ ≠ 0) ⋯

@[instance_reducible]

instance BaleEtAl2025.instDecidableLeSetFinOfNatNatOfDecidablePredMem_studies (S T : Set (Fin 4)) [DecidablePred fun (x : Fin 4) => x ∈ S] [DecidablePred fun (x : Fin 4) => x ∈ T] : Decidable (S ⊆ T)

Equations

• BaleEtAl2025.instDecidableLeSetFinOfNatNatOfDecidablePredMem_studies S T = decidable_of_iff (∀ w ∈ S, w ∈ T) ⋯

@[instance_reducible]

instance BaleEtAl2025.instDecidableLtSetFinOfNatNatOfDecidablePredMem_studies (S T : Set (Fin 4)) [DecidablePred fun (x : Fin 4) => x ∈ S] [DecidablePred fun (x : Fin 4) => x ∈ T] : Decidable (S ⊂ T)

Equations

• BaleEtAl2025.instDecidableLtSetFinOfNatNatOfDecidablePredMem_studies S T = decidable_of_iff (S ⊆ T ∧ ¬T ⊆ S) ⋯

@[instance_reducible]

instance BaleEtAl2025.instDecidableEqSetFinOfNatNatOfDecidablePredMem_studies (S T : Set (Fin 4)) [DecidablePred fun (x : Fin 4) => x ∈ S] [DecidablePred fun (x : Fin 4) => x ∈ T] : Decidable (S = T)

Equations

• BaleEtAl2025.instDecidableEqSetFinOfNatNatOfDecidablePredMem_studies S T = decidable_of_iff (∀ (w : Fin 4), w ∈ S ↔ w ∈ T) ⋯

@[instance_reducible]

instance BaleEtAl2025.instDecidablePredFinOfNatNatMemSetCoeFinset_studies (S : Finset (Fin 4)) : DecidablePred fun (x : Fin 4) => x ∈ ↑S

Equations

• BaleEtAl2025.instDecidablePredFinOfNatNatMemSetCoeFinset_studies S w = decidable_of_iff (w ∈ S) ⋯

@[instance_reducible]

instance BaleEtAl2025.instDecidableMemSetFinOfNatNatCompetentAllOfDecidablePred (S : Set (Fin 4)) [DecidablePred fun (x : Fin 4) => x ∈ S] : Decidable (S ∈ NeoGricean.competent all)

Equations

• BaleEtAl2025.instDecidableMemSetFinOfNatNatCompetentAllOfDecidablePred S = decidable_of_iff (S ⊆ BaleEtAl2025.all ∨ S ⊆ BaleEtAl2025.allᶜ) ⋯

theorem BaleEtAl2025.competent_iff_looked (a w : Fin 4) (hw : w ∈ seen) : speakerState a w ∈ NeoGricean.competent all ↔ a = 3

The speaker is competent about all exactly when he looked into the third box.

The recipe and its integration with context

def BaleEtAl2025.uttered (q : GoodmanStuhlmuller2013.QUtt) : Set (Set (Fin 4))

An utterance conveys Quality and the weak implicatures of its stronger scalar alternatives, so the speaker knows the statement and does not know any stronger one.

Equations

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

@[instance_reducible]

instance BaleEtAl2025.instDecidableMemSetFinOfNatNatUtteredOfDecidablePred (S : Set (Fin 4)) [DecidablePred fun (x : Fin 4) => x ∈ S] (q : GoodmanStuhlmuller2013.QUtt) : Decidable (S ∈ uttered q)

Equations

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

def BaleEtAl2025.integrated (a : Fin 4) (E : Set (Set (Fin 4))) : Set (Fin 4)

With the speaker's contextual knowledge state integrated, the hearer keeps the worlds in which what the speaker saw satisfies the epistemic constraints.

Equations

• BaleEtAl2025.integrated a E = {w : Fin 4 | w ∈ BaleEtAl2025.seen ∧ BaleEtAl2025.speakerState a w ∈ E}

@[instance_reducible]

instance BaleEtAl2025.instDecidablePredFinOfNatNatMemSetIntegratedOfDecidableSpeakerState (a : Fin 4) (E : Set (Set (Fin 4))) [(w : Fin 4) → Decidable (speakerState a w ∈ E)] : DecidablePred fun (x : Fin 4) => x ∈ integrated a E

Equations

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

def BaleEtAl2025.unintegrated (E : Set (Set (Fin 4))) : Set (Fin 4)

Without that integration the hearer keeps the worlds that some knowledge state satisfying the constraints contains, knowledge being factive.

Equations

• BaleEtAl2025.unintegrated E = {w : Fin 4 | w ∈ BaleEtAl2025.seen ∧ ∃ (S : Finset (Fin 4)), ↑S ∈ E ∧ w ∈ S}

@[instance_reducible]

instance BaleEtAl2025.instDecidablePredFinOfNatNatMemSetUnintegratedOfDecidableCoeFinset (E : Set (Set (Fin 4))) [(S : Finset (Fin 4)) → Decidable (↑S ∈ E)] : DecidablePred fun (x : Fin 4) => x ∈ unintegrated E

Equations

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

The two hypotheses

def BaleEtAl2025.contextual (a : Fin 4) (q : GoodmanStuhlmuller2013.QUtt) : Set (Fin 4)

Contextual licensing grants competence only as the speaker's contextual knowledge state supplies it.

Equations

• BaleEtAl2025.contextual a q = BaleEtAl2025.integrated a (BaleEtAl2025.uttered q)

@[instance_reducible]

instance BaleEtAl2025.instDecidablePredFinOfNatNatMemSetContextual (a : Fin 4) (q : GoodmanStuhlmuller2013.QUtt) : DecidablePred fun (x : Fin 4) => x ∈ contextual a q

Equations

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

def BaleEtAl2025.competenceDefault (a : Fin 4) (q : GoodmanStuhlmuller2013.QUtt) : Set (Fin 4)

Competence by default with integration keeps the default where the speaker's contextual state bears it out and cancels it where that state contradicts it everywhere.

Equations

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

@[instance_reducible]

instance BaleEtAl2025.instDecidablePredFinOfNatNatMemSetCompetenceDefault (a : Fin 4) (q : GoodmanStuhlmuller2013.QUtt) : DecidablePred fun (x : Fin 4) => x ∈ competenceDefault a q

Equations

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

def BaleEtAl2025.competenceDefaultLoad (q : GoodmanStuhlmuller2013.QUtt) : Set (Fin 4)

The default with integration blocked, as under cognitive load.

Equations

• BaleEtAl2025.competenceDefaultLoad q = BaleEtAl2025.unintegrated (BaleEtAl2025.uttered q ∩ NeoGricean.competent BaleEtAl2025.all)

@[instance_reducible]

instance BaleEtAl2025.instDecidablePredFinOfNatNatMemSetCompetenceDefaultLoad (q : GoodmanStuhlmuller2013.QUtt) : DecidablePred fun (x : Fin 4) => x ∈ competenceDefaultLoad q

Equations

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

inductive BaleEtAl2025.Answer : Type

A participant answers Do you think there are red cubes in this box? with one of these.

• yes : Answer
• no : Answer
• dontKnow : Answer

@[instance_reducible]

instance BaleEtAl2025.instDecidableEqAnswer : DecidableEq Answer

Equations

• BaleEtAl2025.instDecidableEqAnswer x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BaleEtAl2025.instReprAnswer : Repr Answer

Equations

• BaleEtAl2025.instReprAnswer = { reprPrec := BaleEtAl2025.instReprAnswer.repr }

def BaleEtAl2025.instReprAnswer.repr : Answer → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• BaleEtAl2025.instReprAnswer.repr BaleEtAl2025.Answer.yes prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BaleEtAl2025.Answer.yes")).group prec✝
• BaleEtAl2025.instReprAnswer.repr BaleEtAl2025.Answer.no prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BaleEtAl2025.Answer.no")).group prec✝

def BaleEtAl2025.answer (worlds : Set (Fin 4)) [DecidablePred fun (x : Fin 4) => x ∈ worlds] : Answer

The remaining worlds support the answer yes if the third box has red cubes in all of them, and no if in none.

Equations

• BaleEtAl2025.answer worlds = if worlds ⊆ BaleEtAl2025.all then BaleEtAl2025.Answer.yes else if worlds ⊆ BaleEtAl2025.allᶜ then BaleEtAl2025.Answer.no else BaleEtAl2025.Answer.dontKnow

theorem BaleEtAl2025.competenceDefault_eq_contextual (a : Fin 4) (q : GoodmanStuhlmuller2013.QUtt) : competenceDefault a q = contextual a q

With integration the default is cancelled exactly where the context contradicts it, so the two hypotheses agree.

theorem BaleEtAl2025.load_diverges : answer (competenceDefaultLoad GoodmanStuhlmuller2013.QUtt.some_) = Answer.no ∧ answer (contextual 2 GoodmanStuhlmuller2013.QUtt.some_) = Answer.dontKnow

Without integration the default yields the strong implicature from the ignorant speaker, where contextual licensing leaves the third box open.

theorem BaleEtAl2025.load_agrees_of_knowledgeable (q : GoodmanStuhlmuller2013.QUtt) : answer (competenceDefaultLoad q) = answer (contextual 3 q)

For the knowledgeable speaker the blocked default changes nothing.

The trial types

def BaleEtAl2025.access? (r : Datum) : Option (Fin 4)

How many boxes Farmer Brown looked into.

Equations

• BaleEtAl2025.access? r = match r.feature? "boxesSeen" with | some "2" => some 2 | some "3" => some 3 | x => none

def BaleEtAl2025.quantifier? (r : Datum) : Option GoodmanStuhlmuller2013.QUtt

The quantifier of his statement.

Equations

• BaleEtAl2025.quantifier? r = match r.feature? "quantifier" with | some "some" => some GoodmanStuhlmuller2013.QUtt.some_ | some "all" => some GoodmanStuhlmuller2013.QUtt.all | x => none

def BaleEtAl2025.expected? (r : Datum) : Option Answer

The response the paper expects.

Equations

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

theorem BaleEtAl2025.rows_expected (r : Datum) : r ∈ Examples.all → ∀ a ∈ access? r, ∀ q ∈ quantifier? r, ∀ e ∈ expected? r, answer (contextual a q) = e

The expected response in each trial type is the contextual-licensing answer.