Epistemic threshold semantics

Threshold semantics for epistemic vocabulary over agent credence, the probabilistic tradition of [LG17]: an attitude verb, modal verb, or modal adjective holds of a proposition iff the agent's credence in it clears a lexical threshold — meetsThreshold, with failsThreshold the reversed-polarity form (uncertain, unlikely). The pattern is the positive form of a gradable predicate on the credence scale, whose boundedness makes endpoint standards like certain available on the [Ken07] licensing story; the [Kle80] reduction of the comparative to the positive form holds on this scale (lt_iff_separating_threshold).

IsProbabilistic — monotonicity of credence in entailment — is what separates probabilistic credence from ordinal confidence orderings: it validates conjunction elimination (prob_conjunction_elim), which [CSW24]'s non-probabilistic confidence ordering deliberately does not (the divergence witness lives in Studies/CarianiSantorioWellwood2024.lean). The fitted threshold lexicon of Ying et al.'s Language-augmented Bayesian Theory of Mind ([YZXW+25], their Table 1) lives in Studies/YingEtAl2025.lean.

def EpistemicThreshold.meetsThreshold {E : Type u_1} {W : Type u_2} (cr : E → Set W → ℚ) (θ : ℚ) (a : E) (φ : Set W) : Prop

Agent a's credence in φ meets the threshold θ — the positive-form condition underlying believes, certain, must, likely, might.

Equations

• EpistemicThreshold.meetsThreshold cr θ a φ = (θ ≤ cr a φ)

def EpistemicThreshold.failsThreshold {E : Type u_1} {W : Type u_2} (cr : E → Set W → ℚ) (θ : ℚ) (a : E) (φ : Set W) : Prop

Agent a's credence in φ is strictly below the threshold θ — the reversed-polarity condition of uncertain and unlikely.

Equations

• EpistemicThreshold.failsThreshold cr θ a φ = (cr a φ < θ)

theorem EpistemicThreshold.threshold_exhaustive {E : Type u_1} {W : Type u_2} (cr : E → Set W → ℚ) (θ : ℚ) (a : E) (φ : Set W) : meetsThreshold cr θ a φ ∨ failsThreshold cr θ a φ

For any credence and threshold, exactly one of meetsThreshold and failsThreshold holds.

Probabilistic credence

def EpistemicThreshold.IsProbabilistic {E : Type u_1} {W : Type u_2} (cr : E → Set W → ℚ) : Prop

A credence function is probabilistic when it is monotone in entailment: φ ⊆ ψ implies cr a φ ≤ cr a ψ. This is the axiom that separates probabilistic credence from ordinal confidence orderings, which impose no such constraint and so admit conjunction fallacies.

Equations

• EpistemicThreshold.IsProbabilistic cr = ∀ (a : E), Monotone (cr a)

theorem EpistemicThreshold.IsProbabilistic.conj_elim {E : Type u_1} {W : Type u_2} {cr : E → Set W → ℚ} (h : IsProbabilistic cr) (a : E) (φ ψ : Set W) : cr a (φ ∩ ψ) ≤ cr a φ

Probabilistic credence never ranks a conjunction above a conjunct.

theorem EpistemicThreshold.prob_conjunction_elim {E : Type u_1} {W : Type u_2} {cr : E → Set W → ℚ} (h : IsProbabilistic cr) (θ : ℚ) (a : E) (φ ψ : Set W) (hm : meetsThreshold cr θ a (φ ∩ ψ)) : meetsThreshold cr θ a φ

Probabilistic credence validates conjunction elimination at every threshold: believing φ ∧ ψ entails believing φ.

The Klein reduction

theorem EpistemicThreshold.lt_iff_separating_threshold {E : Type u_1} {W : Type u_2} (cr : E → Set W → ℚ) (a : E) (φ ψ : Set W) : cr a ψ < cr a φ ↔ ∃ (θ : ℚ), meetsThreshold cr θ a φ ∧ ¬meetsThreshold cr θ a ψ

The comparative reduces to the positive form ([Kle80], extended from adjectives to the credence scale): φ is more credent than ψ iff some threshold separates them. The witness is θ = cr a φ itself.