Ying, Zhi-Xuan, Wong, Mansinghka & Tenenbaum (2025): Understanding Epistemic Language

This file formalizes the epistemic language of thought of Ying and colleagues, a degree-based semantics for attitude verbs, modal verbs and modal adjectives grounded in the probability an agent assigns to a formula, following the scalar semantics of Lassiter. Each expression is the positive form of the probability scale at a lexical threshold (Thresholds), the preimage of Set.Ici: believes, certain, the modal verbs from could to must, and likely hold when the probability clears their threshold; uncertain and unlikely when it falls below (the preimage of Set.Iio); knows that is belief plus truth, knows if knowledge of the question, and the about operators quantify over a contextually restricted domain (knowsAbout, certainAbout, uncertainAbout). A modal under believes is lowered to a comparison with the modal's own threshold rather than the belief threshold (believesModal_might). Comparatives and superlatives compare probabilities, and the strengthened superlative scales the threshold by a multiplier (mostStr). The entailments among the expressions follow from the ordering of the thresholds alone (Thresholds.Ordered, must_entails_might, certainAbout_believes, uncertainAbout_certainAbout), and the fitted values of the paper's lexicon respect that ordering (fitted, fitted_ordered). The modal verbs' forces in the English fragment agree with the ordering: no possibility modal carries a higher threshold than a necessity modal (force_threshold_le).

Implementation notes

An agent's credences are a Markov kernel from agents to worlds, Pr a φ the probability agent a assigns to φ; the Bayesian theory-of-mind inference that produces it from observed actions is not modelled. Thresholds live on the probability scale ℝ≥0∞. The fitted thresholds and the literature-derived initial values of the paper's second appendix are recorded as instances of Thresholds, and the theorems are stated for any thresholds satisfying the ordering. The paper states no ordering; Thresholds.Ordered is this file's, and its modal part agrees with Lassiter's θ_might < θ_likely < θ_must < θ_certain (p. 152), weakened to ≤ since the fitted values tie.

References

• [YZXW+25]
• [Las17a]
• [Hin62]

Thresholds

structure YingEtAl2025.Thresholds : Type

The probability thresholds of the epistemic lexicon and the multiplier of the strengthened superlative.

• believes : ENNReal
• certain : ENNReal
• uncertain : ENNReal
• likely : ENNReal
• unlikely : ENNReal
• could : ENNReal
• might : ENNReal
• may : ENNReal
• should : ENNReal
• must : ENNReal
• most : ENNReal

structure YingEtAl2025.Thresholds.Ordered (Θ : Thresholds) : Prop

The thresholds are ordered as the entailments need when the modal verbs form a scale from could to must, likely sits between may and should, belief lies above likely and below certain, and the reversed-polarity thresholds lie below certain.

• could_might : Θ.could ≤ Θ.might
• might_may : Θ.might ≤ Θ.may
• may_likely : Θ.may ≤ Θ.likely
• likely_believes : Θ.likely ≤ Θ.believes
• believes_should : Θ.believes ≤ Θ.should
• should_must : Θ.should ≤ Θ.must
• must_certain : Θ.must ≤ Θ.certain
• unlikely_uncertain : Θ.unlikely ≤ Θ.uncertain
• uncertain_certain : Θ.uncertain ≤ Θ.certain
• one_le_most : 1 ≤ Θ.most

noncomputable def YingEtAl2025.fitted : Thresholds

The thresholds fitted against human plausibility ratings.

Equations

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

noncomputable def YingEtAl2025.initial : Thresholds

The initial thresholds derived from the literature, before fitting.

Equations

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

theorem YingEtAl2025.fitted_ordered : fitted.Ordered

theorem YingEtAl2025.initial_ordered : initial.Ordered

The epistemic expressions

def YingEtAl2025.believes {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] (Θ : Thresholds) (Pr : ProbabilityTheory.Kernel E W) (a : E) (φ : Set W) : Prop

A believes that φ.

Equations

• YingEtAl2025.believes Θ Pr a φ = (φ ∈ ⇑(Pr a) ⁻¹' Set.Ici Θ.believes)

def YingEtAl2025.believesModal {E : Type u_1} (a : E) (M : E → Prop) : Prop

A believes M, for a modal claim M, applies the modal to the agent.

Equations

• YingEtAl2025.believesModal a M = M a

def YingEtAl2025.knowsThat {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] (Θ : Thresholds) (Pr : ProbabilityTheory.Kernel E W) (a : E) (φ : Set W) (w : W) : Prop

A knows that φ holds when A believes φ and φ is true.

Equations

• YingEtAl2025.knowsThat Θ Pr a φ w = (YingEtAl2025.believes Θ Pr a φ ∧ w ∈ φ)

def YingEtAl2025.knowsIf {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] (Θ : Thresholds) (Pr : ProbabilityTheory.Kernel E W) (a : E) (φ : Set W) (w : W) : Prop

A knows if φ holds when A knows the answer.

Equations

• YingEtAl2025.knowsIf Θ Pr a φ w = (YingEtAl2025.knowsThat Θ Pr a φ w ∨ YingEtAl2025.knowsThat Θ Pr a φᶜ w)

def YingEtAl2025.knowsAbout {E : Type u_1} {W : Type u_2} {X : Type u_3} [MeasurableSpace E] [MeasurableSpace W] (Θ : Thresholds) (Pr : ProbabilityTheory.Kernel E W) (a : E) (C : X → Prop) (φ : X → Set W) (w : W) : Prop

A knows about φ holds when the agent knows φ of some relevant entity.

Equations

• YingEtAl2025.knowsAbout Θ Pr a C φ w = ∃ (x : X), C x ∧ YingEtAl2025.knowsThat Θ Pr a (φ x) w

def YingEtAl2025.notKnowsThat {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] (Θ : Thresholds) (Pr : ProbabilityTheory.Kernel E W) (a : E) (φ : Set W) (w : W) : Prop

A does not know that φ holds when φ is true but not believed.

Equations

• YingEtAl2025.notKnowsThat Θ Pr a φ w = (¬YingEtAl2025.believes Θ Pr a φ ∧ w ∈ φ)

def YingEtAl2025.certainThat {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] (Θ : Thresholds) (Pr : ProbabilityTheory.Kernel E W) (a : E) (φ : Set W) : Prop

A is certain that φ.

Equations

• YingEtAl2025.certainThat Θ Pr a φ = (φ ∈ ⇑(Pr a) ⁻¹' Set.Ici Θ.certain)

def YingEtAl2025.certainAbout {E : Type u_1} {W : Type u_2} {X : Type u_3} [MeasurableSpace E] [MeasurableSpace W] (Θ : Thresholds) (Pr : ProbabilityTheory.Kernel E W) (a : E) (C : X → Prop) (φ : X → Set W) : Prop

A is certain about φ holds when the agent is certain of φ for some relevant entity.

Equations

• YingEtAl2025.certainAbout Θ Pr a C φ = ∃ (x : X), C x ∧ YingEtAl2025.certainThat Θ Pr a (φ x)

def YingEtAl2025.uncertainIf {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] (Θ : Thresholds) (Pr : ProbabilityTheory.Kernel E W) (a : E) (φ ψ : Set W) : Prop

A is uncertain if φ or ψ holds when neither alternative reaches the threshold.

Equations

• YingEtAl2025.uncertainIf Θ Pr a φ ψ = (φ ∈ ⇑(Pr a) ⁻¹' Set.Iio Θ.uncertain ∧ ψ ∈ ⇑(Pr a) ⁻¹' Set.Iio Θ.uncertain)

def YingEtAl2025.uncertainAbout {E : Type u_1} {W : Type u_2} {X : Type u_3} [MeasurableSpace E] [MeasurableSpace W] (Θ : Thresholds) (Pr : ProbabilityTheory.Kernel E W) (a : E) (C : X → Prop) (φ : X → Set W) : Prop

A is uncertain about φ holds when no relevant entity reaches the threshold.

Equations

• YingEtAl2025.uncertainAbout Θ Pr a C φ = ∀ (x : X), C x → φ x ∈ ⇑(Pr a) ⁻¹' Set.Iio Θ.uncertain

def YingEtAl2025.could {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] (Θ : Thresholds) (Pr : ProbabilityTheory.Kernel E W) (φ : Set W) (a : E) : Prop

The modal verbs and adjective, each a property of agents.

Equations

• YingEtAl2025.could Θ Pr φ a = (φ ∈ ⇑(Pr a) ⁻¹' Set.Ici Θ.could)

def YingEtAl2025.might {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] (Θ : Thresholds) (Pr : ProbabilityTheory.Kernel E W) (φ : Set W) (a : E) : Prop

Equations

• YingEtAl2025.might Θ Pr φ a = (φ ∈ ⇑(Pr a) ⁻¹' Set.Ici Θ.might)

def YingEtAl2025.may {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] (Θ : Thresholds) (Pr : ProbabilityTheory.Kernel E W) (φ : Set W) (a : E) : Prop

Equations

• YingEtAl2025.may Θ Pr φ a = (φ ∈ ⇑(Pr a) ⁻¹' Set.Ici Θ.may)

def YingEtAl2025.should {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] (Θ : Thresholds) (Pr : ProbabilityTheory.Kernel E W) (φ : Set W) (a : E) : Prop

Equations

• YingEtAl2025.should Θ Pr φ a = (φ ∈ ⇑(Pr a) ⁻¹' Set.Ici Θ.should)

def YingEtAl2025.must {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] (Θ : Thresholds) (Pr : ProbabilityTheory.Kernel E W) (φ : Set W) (a : E) : Prop

Equations

• YingEtAl2025.must Θ Pr φ a = (φ ∈ ⇑(Pr a) ⁻¹' Set.Ici Θ.must)

def YingEtAl2025.likely {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] (Θ : Thresholds) (Pr : ProbabilityTheory.Kernel E W) (φ : Set W) (a : E) : Prop

Equations

• YingEtAl2025.likely Θ Pr φ a = (φ ∈ ⇑(Pr a) ⁻¹' Set.Ici Θ.likely)

def YingEtAl2025.unlikely {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] (Θ : Thresholds) (Pr : ProbabilityTheory.Kernel E W) (φ : Set W) (a : E) : Prop

Equations

• YingEtAl2025.unlikely Θ Pr φ a = (φ ∈ ⇑(Pr a) ⁻¹' Set.Iio Θ.unlikely)

def YingEtAl2025.more {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] (Pr : ProbabilityTheory.Kernel E W) (φ ψ : Set W) (a : E) : Prop

φ is more likely than ψ.

Equations

• YingEtAl2025.more Pr φ ψ a = ((Pr a) ψ < (Pr a) φ)

def YingEtAl2025.mostSup {E : Type u_1} {W : Type u_2} {X : Type u_3} [MeasurableSpace E] [MeasurableSpace W] (Pr : ProbabilityTheory.Kernel E W) (o : X) (C : X → Prop) (φ : X → Set W) (a : E) : Prop

φ of o is most likely among the relevant alternatives.

Equations

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

def YingEtAl2025.mostStr {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] (Θ : Thresholds) (Pr : ProbabilityTheory.Kernel E W) (θ : ENNReal) (φ : Set W) (a : E) : Prop

The strengthened superlative holds when the probability reaches the multiplied threshold.

Equations

• YingEtAl2025.mostStr Θ Pr θ φ a = (φ ∈ ⇑(Pr a) ⁻¹' Set.Ici (Θ.most * θ))

Entailments from the ordering

theorem YingEtAl2025.knowsThat_believes {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] {Θ : Thresholds} {Pr : ProbabilityTheory.Kernel E W} {a : E} {φ : Set W} {w : W} (h : knowsThat Θ Pr a φ w) : believes Θ Pr a φ

Knowledge entails belief.

theorem YingEtAl2025.knowsThat_mem {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] {Θ : Thresholds} {Pr : ProbabilityTheory.Kernel E W} {a : E} {φ : Set W} {w : W} (h : knowsThat Θ Pr a φ w) : w ∈ φ

Knowledge is veridical.

theorem YingEtAl2025.knowsIf_of_knowsThat {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] {Θ : Thresholds} {Pr : ProbabilityTheory.Kernel E W} {a : E} {φ : Set W} {w : W} (h : knowsThat Θ Pr a φ w) : knowsIf Θ Pr a φ w

Knowing that answers the question.

theorem YingEtAl2025.not_notKnowsThat_of_believes {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] {Θ : Thresholds} {Pr : ProbabilityTheory.Kernel E W} {a : E} {φ : Set W} {w : W} (h : believes Θ Pr a φ) : ¬notKnowsThat Θ Pr a φ w

Belief and not knowing exclude one another.

theorem YingEtAl2025.believesModal_might {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] {Θ : Thresholds} {Pr : ProbabilityTheory.Kernel E W} (a : E) (φ : Set W) : believesModal a (might Θ Pr φ) ↔ φ ∈ ⇑(Pr a) ⁻¹' Set.Ici Θ.might

A modal under believes is lowered to the modal's own threshold.

theorem YingEtAl2025.must_entails_might {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] {Θ : Thresholds} {Pr : ProbabilityTheory.Kernel E W} (h : Θ.Ordered) {φ : Set W} {a : E} (hm : must Θ Pr φ a) : might Θ Pr φ a

must entails should, likely, may, might and could under the ordering.

theorem YingEtAl2025.must_entails_should {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] {Θ : Thresholds} {Pr : ProbabilityTheory.Kernel E W} (h : Θ.Ordered) {φ : Set W} {a : E} (hm : must Θ Pr φ a) : should Θ Pr φ a

theorem YingEtAl2025.should_entails_likely {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] {Θ : Thresholds} {Pr : ProbabilityTheory.Kernel E W} (h : Θ.Ordered) {φ : Set W} {a : E} (hm : should Θ Pr φ a) : likely Θ Pr φ a

theorem YingEtAl2025.might_entails_could {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] {Θ : Thresholds} {Pr : ProbabilityTheory.Kernel E W} (h : Θ.Ordered) {φ : Set W} {a : E} (hm : might Θ Pr φ a) : could Θ Pr φ a

theorem YingEtAl2025.certainThat_believes {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] {Θ : Thresholds} {Pr : ProbabilityTheory.Kernel E W} (h : Θ.Ordered) {a : E} {φ : Set W} (hc : certainThat Θ Pr a φ) : believes Θ Pr a φ

Certainty entails belief.

theorem YingEtAl2025.certainAbout_believes {E : Type u_1} {W : Type u_2} {X : Type u_3} [MeasurableSpace E] [MeasurableSpace W] {Θ : Thresholds} {Pr : ProbabilityTheory.Kernel E W} (h : Θ.Ordered) {a : E} {C : X → Prop} {φ : X → Set W} (hc : certainAbout Θ Pr a C φ) : ∃ (x : X), C x ∧ believes Θ Pr a (φ x)

Certainty about supplies a believed witness.

theorem YingEtAl2025.uncertainAbout_certainAbout {E : Type u_1} {W : Type u_2} {X : Type u_3} [MeasurableSpace E] [MeasurableSpace W] {Θ : Thresholds} {Pr : ProbabilityTheory.Kernel E W} (h : Θ.Ordered) {a : E} {C : X → Prop} {φ : X → Set W} (hu : uncertainAbout Θ Pr a C φ) (hc : certainAbout Θ Pr a C φ) : False

Uncertainty about and certainty about are incompatible.

theorem YingEtAl2025.mostStr_meets {E : Type u_1} {W : Type u_2} [MeasurableSpace E] [MeasurableSpace W] {Θ : Thresholds} {Pr : ProbabilityTheory.Kernel E W} (h : Θ.Ordered) {θ : ENNReal} {φ : Set W} {a : E} (hm : mostStr Θ Pr θ φ a) : φ ∈ ⇑(Pr a) ⁻¹' Set.Ici θ

The strengthened superlative entails the plain threshold reading.

The English modal verbs

inductive YingEtAl2025.ModalVerb : Type

The modal verbs of the lexicon.

• could : ModalVerb
• might : ModalVerb
• may : ModalVerb
• should : ModalVerb
• must : ModalVerb

@[instance_reducible]

instance YingEtAl2025.instDecidableEqModalVerb : DecidableEq ModalVerb

Equations

• YingEtAl2025.instDecidableEqModalVerb x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def YingEtAl2025.instReprModalVerb.repr : ModalVerb → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance YingEtAl2025.instReprModalVerb : Repr ModalVerb

Equations

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

@[instance_reducible]

instance YingEtAl2025.instFintypeModalVerb : Fintype ModalVerb

Equations

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

def YingEtAl2025.ModalVerb.threshold (Θ : Thresholds) : ModalVerb → ENNReal

The threshold of each modal verb.

Equations

• YingEtAl2025.ModalVerb.threshold Θ YingEtAl2025.ModalVerb.could = Θ.could
• YingEtAl2025.ModalVerb.threshold Θ YingEtAl2025.ModalVerb.might = Θ.might
• YingEtAl2025.ModalVerb.threshold Θ YingEtAl2025.ModalVerb.may = Θ.may
• YingEtAl2025.ModalVerb.threshold Θ YingEtAl2025.ModalVerb.should = Θ.should
• YingEtAl2025.ModalVerb.threshold Θ YingEtAl2025.ModalVerb.must = Θ.must

def YingEtAl2025.ModalVerb.aux : ModalVerb → Auxiliary

The English auxiliary of each modal verb.

Equations

• YingEtAl2025.ModalVerb.could.aux = English.Auxiliaries.could
• YingEtAl2025.ModalVerb.might.aux = English.Auxiliaries.might
• YingEtAl2025.ModalVerb.may.aux = English.Auxiliaries.may
• YingEtAl2025.ModalVerb.should.aux = English.Auxiliaries.should
• YingEtAl2025.ModalVerb.must.aux = English.Auxiliaries.must

def YingEtAl2025.ModalVerb.forces (v : ModalVerb) : Finset Modality.ModalForce

The epistemic forces of each modal verb, read off the fragment.

Equations

• v.forces = v.aux.toModalItem.forcesOf Modality.ModalFlavor.epistemic

theorem YingEtAl2025.forces_might : ModalVerb.might.forces = {Modality.ModalForce.possibility}

theorem YingEtAl2025.forces_must : ModalVerb.must.forces = {Modality.ModalForce.necessity}

theorem YingEtAl2025.forces_should : ModalVerb.should.forces = {Modality.ModalForce.weakNecessity}

theorem YingEtAl2025.force_threshold_le {Θ : Thresholds} (h : Θ.Ordered) {v v' : ModalVerb} (hv : v.forces = {Modality.ModalForce.possibility}) (hv' : v'.forces ≠ {Modality.ModalForce.possibility}) : ModalVerb.threshold Θ v ≤ ModalVerb.threshold Θ v'

Under the ordering, a possibility modal never carries a higher threshold than a modal of necessity or weak necessity.