Ying et al. 2025: epistemic language as threshold semantics over credence

[YZXW+25] ("Understanding Epistemic Language with a Language-augmented Bayesian Theory of Mind", TACL 13) interpret epistemic vocabulary — attitude verbs, modal verbs, and modal adjectives — as threshold functions over agent credence, with credence computed by Bayesian theory-of-mind inference from observed actions. EpistemicEntry renders their lexical entries (their Table 1): a credence threshold plus a factivity flag, with the threshold values the paper's grid-search best fits against human plausibility ratings in a Doors, Keys & Gems gridworld — the ordering is the theoretical commitment, the specific values are empirical fits. The Table 1 operator inventory (knowsIf, uncertainIf, knowsAbout, mostSup, ...) and the scalar entailments (knows_entails_believes, must_entails_might, ...) follow.

The bridge section connects the English modal fragment (English.Auxiliaries) to the fitted entries: the Fragment's forms map to entries, necessity-force modals carry strictly higher thresholds than possibility-force modals, and the within-force scalar ordering (must > should; may > might) captures differences binary force cannot express. The final section records the divergence from [HF19]'s independently fitted threshold for probably.

The epistemic lexicon (Table 1)

structure YingEtAl2025.EpistemicEntry : Type

An epistemic lexical entry: the expression holds iff credence clears θ, with factive marking the additional truth requirement of knows. The lexical form is carried by the Fragment (English.Auxiliaries), not the entry.

• θ : ℚ

  Credence threshold.

• factive : Bool

  Truth requirement at the evaluation world (knows but not believes).

@[instance_reducible]

instance YingEtAl2025.instDecidableEqEpistemicEntry : DecidableEq EpistemicEntry

Equations

• YingEtAl2025.instDecidableEqEpistemicEntry = YingEtAl2025.instDecidableEqEpistemicEntry.decEq

def YingEtAl2025.instDecidableEqEpistemicEntry.decEq (x✝ x✝¹ : EpistemicEntry) : Decidable (x✝ = x✝¹)

Equations

• YingEtAl2025.instDecidableEqEpistemicEntry.decEq { θ := a, factive := a_1 } { θ := b, factive := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance YingEtAl2025.instReprEpistemicEntry : Repr EpistemicEntry

Equations

• YingEtAl2025.instReprEpistemicEntry = { reprPrec := YingEtAl2025.instReprEpistemicEntry.repr }

def YingEtAl2025.instReprEpistemicEntry.repr : EpistemicEntry → ℕ → Std.Format

Equations

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

The fitted thresholds (Table 1(b)): must = certain (0.95) > should (0.80) > believes (0.75) > likely = uncertain (0.70) > unlikely (0.40) > may (0.30) > might = could (0.20). uncertain and unlikely are reversed-polarity: they hold when credence is strictly below the threshold (failsThreshold).

def YingEtAl2025.EpistemicEntry.believes : EpistemicEntry

Equations

• YingEtAl2025.EpistemicEntry.believes = { θ := 3 / 4 }

def YingEtAl2025.EpistemicEntry.knows : EpistemicEntry

Equations

• YingEtAl2025.EpistemicEntry.knows = { θ := 3 / 4, factive := true }

def YingEtAl2025.EpistemicEntry.certain : EpistemicEntry

Equations

• YingEtAl2025.EpistemicEntry.certain = { θ := 19 / 20 }

def YingEtAl2025.EpistemicEntry.must : EpistemicEntry

Equations

• YingEtAl2025.EpistemicEntry.must = { θ := 19 / 20 }

def YingEtAl2025.EpistemicEntry.should : EpistemicEntry

Equations

• YingEtAl2025.EpistemicEntry.should = { θ := 4 / 5 }

def YingEtAl2025.EpistemicEntry.likely : EpistemicEntry

Equations

• YingEtAl2025.EpistemicEntry.likely = { θ := 7 / 10 }

def YingEtAl2025.EpistemicEntry.may : EpistemicEntry

Equations

• YingEtAl2025.EpistemicEntry.may = { θ := 3 / 10 }

def YingEtAl2025.EpistemicEntry.might : EpistemicEntry

Equations

• YingEtAl2025.EpistemicEntry.might = { θ := 1 / 5 }

def YingEtAl2025.EpistemicEntry.could : EpistemicEntry

Equations

• YingEtAl2025.EpistemicEntry.could = { θ := 1 / 5 }

def YingEtAl2025.EpistemicEntry.uncertain : EpistemicEntry

Equations

• YingEtAl2025.EpistemicEntry.uncertain = { θ := 7 / 10 }

def YingEtAl2025.EpistemicEntry.unlikely : EpistemicEntry

Equations

• YingEtAl2025.EpistemicEntry.unlikely = { θ := 2 / 5 }

def YingEtAl2025.EpistemicEntry.α_most : ℚ

The superlative multiplier α_most (Table 1(b)).

Equations

• YingEtAl2025.EpistemicEntry.α_most = 3 / 2

theorem YingEtAl2025.EpistemicEntry.scale_sorted : List.IsChain (fun (x1 x2 : ℚ) => x1 > x2) [19 / 20, 4 / 5, 3 / 4, 7 / 10, 2 / 5, 3 / 10, 1 / 5]

The threshold scale is strictly decreasing: must = certain > should > believes > likely = uncertain > unlikely > may > might = could.

def YingEtAl2025.holdsAt {E : Type u_1} {W : Type u_2} (cr : E → Set W → ℚ) (e : EpistemicEntry) (a : E) (φ : Set W) (w : W) : Prop

Full evaluation of an entry: credence clears the threshold, and factive entries additionally require the complement at the evaluation world.

Equations

• YingEtAl2025.holdsAt cr e a φ w = (EpistemicThreshold.meetsThreshold cr e.θ a φ ∧ (e.factive = true → w ∈ φ))

theorem YingEtAl2025.holdsAt_mono_of_le {E : Type u_1} {W : Type u_2} {e₁ e₂ : EpistemicEntry} (hθ : e₁.θ ≤ e₂.θ) (hf : e₁.factive = true → e₂.factive = true) (cr : E → Set W → ℚ) (a : E) (φ : Set W) (w : W) : holdsAt cr e₂ a φ w → holdsAt cr e₁ a φ w

A stronger entry — higher threshold, weaker factivity — entails a weaker one. Every pairwise entailment below is one application.

theorem YingEtAl2025.knows_entails_believes {E : Type u_1} {W : Type u_2} (cr : E → Set W → ℚ) (a : E) (φ : Set W) (w : W) : holdsAt cr EpistemicEntry.knows a φ w → holdsAt cr EpistemicEntry.believes a φ w

knows entails believes: same threshold, knows adds factivity.

theorem YingEtAl2025.knows_is_veridical {E : Type u_1} {W : Type u_2} (cr : E → Set W → ℚ) (a : E) (φ : Set W) (w : W) : holdsAt cr EpistemicEntry.knows a φ w → w ∈ φ

knows is veridical: knowledge entails truth.

theorem YingEtAl2025.certain_entails_believes {E : Type u_1} {W : Type u_2} (cr : E → Set W → ℚ) (a : E) (φ : Set W) (w : W) : holdsAt cr EpistemicEntry.certain a φ w → holdsAt cr EpistemicEntry.believes a φ w

certain entails believes.

theorem YingEtAl2025.must_entails_should {E : Type u_1} {W : Type u_2} (cr : E → Set W → ℚ) (a : E) (φ : Set W) (w : W) : holdsAt cr EpistemicEntry.must a φ w → holdsAt cr EpistemicEntry.should a φ w

must entails should.

theorem YingEtAl2025.should_entails_likely {E : Type u_1} {W : Type u_2} (cr : E → Set W → ℚ) (a : E) (φ : Set W) (w : W) : holdsAt cr EpistemicEntry.should a φ w → holdsAt cr EpistemicEntry.likely a φ w

should entails likely.

theorem YingEtAl2025.must_entails_might {E : Type u_1} {W : Type u_2} (cr : E → Set W → ℚ) (a : E) (φ : Set W) (w : W) : holdsAt cr EpistemicEntry.must a φ w → holdsAt cr EpistemicEntry.might a φ w

must entails might: necessity entails possibility on the threshold scale.

theorem YingEtAl2025.believes_entails_may {E : Type u_1} {W : Type u_2} (cr : E → Set W → ℚ) (a : E) (φ : Set W) (w : W) : holdsAt cr EpistemicEntry.believes a φ w → holdsAt cr EpistemicEntry.may a φ w

believes entails may.

Structural operators (Table 1(a))

def YingEtAl2025.knowsIf {E : Type u_1} {W : Type u_2} (cr : E → Set W → ℚ) (a : E) (φ : Set W) (w : W) : Prop

knows_if: the agent knows the answer to the polar question ?φ.

Equations

• YingEtAl2025.knowsIf cr a φ w = (YingEtAl2025.holdsAt cr YingEtAl2025.EpistemicEntry.knows a φ w ∨ YingEtAl2025.holdsAt cr YingEtAl2025.EpistemicEntry.knows a φᶜ w)

def YingEtAl2025.notKnowsThat {E : Type u_1} {W : Type u_2} (cr : E → Set W → ℚ) (a : E) (φ : Set W) (w : W) : Prop

not_knows_that: φ is true but the agent does not believe it.

Equations

• YingEtAl2025.notKnowsThat cr a φ w = (¬EpistemicThreshold.meetsThreshold cr YingEtAl2025.EpistemicEntry.believes.θ a φ ∧ w ∈ φ)

def YingEtAl2025.uncertainIf {E : Type u_1} {W : Type u_2} (cr : E → Set W → ℚ) (a : E) (φ ψ : Set W) : Prop

uncertain_if: the agent's credence in both alternatives falls below the uncertain threshold.

Equations

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

def YingEtAl2025.mostStr {E : Type u_1} {W : Type u_2} (cr : E → Set W → ℚ) (e : EpistemicEntry) (a : E) (φ : Set W) : Prop

The strengthened superlative most_str: credence reaches α_most times the entry's threshold.

Equations

• YingEtAl2025.mostStr cr e a φ = (YingEtAl2025.EpistemicEntry.α_most * e.θ ≤ cr a φ)

Quantified operators (Table 1(a))

knows_about, certain_about, uncertain_about, and most_sup quantify over a context-restricted entity domain, for sentences like "the player knows which box has the key".

def YingEtAl2025.knowsAbout {E : Type u_1} {W : Type u_2} {X : Type u_3} (cr : E → Set W → ℚ) (a : E) (C : X → Prop) (φ : X → Set W) (w : W) : Prop

knows_about: for some contextually relevant entity, the agent knows that φ holds of it.

Equations

• YingEtAl2025.knowsAbout cr a C φ w = ∃ (x : X), C x ∧ YingEtAl2025.holdsAt cr YingEtAl2025.EpistemicEntry.knows a (φ x) w

def YingEtAl2025.certainAbout {E : Type u_1} {W : Type u_2} {X : Type u_3} (cr : E → Set W → ℚ) (a : E) (C : X → Prop) (φ : X → Set W) : Prop

certain_about: for some contextually relevant entity, credence in φ of it clears the certain threshold.

Equations

• YingEtAl2025.certainAbout cr a C φ = ∃ (x : X), C x ∧ EpistemicThreshold.meetsThreshold cr YingEtAl2025.EpistemicEntry.certain.θ a (φ x)

def YingEtAl2025.uncertainAbout {E : Type u_1} {W : Type u_2} {X : Type u_3} (cr : E → Set W → ℚ) (a : E) (C : X → Prop) (φ : X → Set W) : Prop

uncertain_about: for every contextually relevant entity, credence falls below the uncertain threshold — the universal dual of certainAbout's existential.

Equations

• YingEtAl2025.uncertainAbout cr a C φ = ∀ (x : X), C x → EpistemicThreshold.failsThreshold cr YingEtAl2025.EpistemicEntry.uncertain.θ a (φ x)

def YingEtAl2025.mostSup {E : Type u_1} {W : Type u_2} {X : Type u_3} (cr : E → Set W → ℚ) (a : E) (o : X) (C : X → Prop) (φ : X → Set W) : Prop

most_sup: credence in φ of the object is at least credence in φ of every contextually relevant alternative.

Equations

• YingEtAl2025.mostSup cr a o C φ = ∀ (x : X), C x → cr a (φ x) ≤ cr a (φ o)

theorem YingEtAl2025.knowsAbout_of_holdsAt {E : Type u_1} {W : Type u_2} {X : Type u_3} (cr : E → Set W → ℚ) (a : E) (C : X → Prop) (φ : X → Set W) (w : W) (x : X) (hC : C x) (h : holdsAt cr EpistemicEntry.knows a (φ x) w) : knowsAbout cr a C φ w

A known witness gives knows_about.

theorem YingEtAl2025.certainAbout_entails_believes {E : Type u_1} {W : Type u_2} {X : Type u_3} (cr : E → Set W → ℚ) (a : E) (C : X → Prop) (φ : X → Set W) (h : certainAbout cr a C φ) : ∃ (x : X), C x ∧ EpistemicThreshold.meetsThreshold cr EpistemicEntry.believes.θ a (φ x)

certain_about supplies a believed witness.

theorem YingEtAl2025.uncertainAbout_contradicts_certainAbout {E : Type u_1} {W : Type u_2} {X : Type u_3} (cr : E → Set W → ℚ) (a : E) (C : X → Prop) (φ : X → Set W) (h_unc : uncertainAbout cr a C φ) (h_cert : certainAbout cr a C φ) : False

uncertain_about and certain_about are incompatible.

Fragment bridge: English modal auxiliaries

def YingEtAl2025.toEpistemicEntry (a : English.Auxiliaries.AuxEntry) : Option EpistemicEntry

Map an English modal auxiliary to its epistemic threshold entry; non-epistemic modals (deontic shall) have none. The mapping derives from the Fragment's form field.

Equations

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

def YingEtAl2025.epistemicForce (a : English.Auxiliaries.AuxEntry) : Option Modality.ModalForce

The epistemic force of a modal auxiliary, if it has an epistemic reading.

Equations

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

Per-entry checks of the form → entry → threshold pipeline; these break if the Fragment's form field or the fitted threshold changes.

theorem YingEtAl2025.must_threshold : Option.map (fun (x : EpistemicEntry) => x.θ) (toEpistemicEntry English.Auxiliaries.must) = some (19 / 20)

theorem YingEtAl2025.should_threshold : Option.map (fun (x : EpistemicEntry) => x.θ) (toEpistemicEntry English.Auxiliaries.should) = some (4 / 5)

theorem YingEtAl2025.may_threshold : Option.map (fun (x : EpistemicEntry) => x.θ) (toEpistemicEntry English.Auxiliaries.may) = some (3 / 10)

theorem YingEtAl2025.might_threshold : Option.map (fun (x : EpistemicEntry) => x.θ) (toEpistemicEntry English.Auxiliaries.might) = some (1 / 5)

theorem YingEtAl2025.could_threshold : Option.map (fun (x : EpistemicEntry) => x.θ) (toEpistemicEntry English.Auxiliaries.could) = some (1 / 5)

theorem YingEtAl2025.shall_no_threshold : toEpistemicEntry English.Auxiliaries.shall = none

Non-epistemic modals have no threshold entry.

Force–threshold consistency

Necessity-force epistemic modals carry strictly higher thresholds than possibility-force ones — [Kra81]'s algebraic force and the fitted thresholds characterize the same items consistently.

theorem YingEtAl2025.necessity_gt_possibility_must_might : EpistemicEntry.might.θ < EpistemicEntry.must.θ

theorem YingEtAl2025.necessity_gt_possibility_must_may : EpistemicEntry.may.θ < EpistemicEntry.must.θ

theorem YingEtAl2025.necessity_gt_possibility_should_might : EpistemicEntry.might.θ < EpistemicEntry.should.θ

theorem YingEtAl2025.necessity_gt_possibility_should_may : EpistemicEntry.may.θ < EpistemicEntry.should.θ

theorem YingEtAl2025.necessity_gt_possibility_should_could : EpistemicEntry.could.θ < EpistemicEntry.should.θ

theorem YingEtAl2025.must_is_necessity : epistemicForce English.Auxiliaries.must = some Modality.ModalForce.necessity

The epistemic force of must is necessity (from the Fragment).

theorem YingEtAl2025.might_is_possibility : epistemicForce English.Auxiliaries.might = some Modality.ModalForce.possibility

The epistemic force of might is possibility.

theorem YingEtAl2025.should_is_weakNecessity : epistemicForce English.Auxiliaries.should = some Modality.ModalForce.weakNecessity

The epistemic force of should is weak necessity.

theorem YingEtAl2025.may_is_possibility : epistemicForce English.Auxiliaries.may = some Modality.ModalForce.possibility

The epistemic force of may is possibility.

Within-force ordering

The □ > □w gap (must > should) is expressible by the three-way ModalForce; the within-◇ gap (may > might) remains a purely scalar difference.

theorem YingEtAl2025.must_gt_should : EpistemicEntry.should.θ < EpistemicEntry.must.θ

Strong necessity must outranks weak necessity should.

theorem YingEtAl2025.may_gt_might : EpistemicEntry.might.θ < EpistemicEntry.may.θ

Among possibility modals, may outranks might.

theorem YingEtAl2025.might_eq_could : EpistemicEntry.might.θ = EpistemicEntry.could.θ

might and could share a threshold.

Divergence from Herbstritt & Franke 2019

[HF19] (Cognition 186) independently infer a credence threshold for probably by Bayesian fitting against urn-production data, reporting a posterior mean of 0.549 with 95% HDI [0.500, 0.594] (their Table 6). The fitted threshold for likely here (0.70) lies above that interval's upper bound, so the two parameter-fitted accounts disagree at the 95%-credibility level. Candidate explanations: lexical (probably ≠ likely), task (urn production vs. theory-of-mind in a gridworld), or posterior uncertainty (points vs. intervals).

theorem YingEtAl2025.likely_above_hf_probably_hdi : 594 / 1000 < EpistemicEntry.likely.θ

The fitted likely threshold exceeds the upper bound of [HF19]'s 95% HDI for probably (their Table 6).