Epistemic Threshold Semantics

@cite{ying-zhi-xuan-wong-mansinghka-tenenbaum-2025} @cite{baker-jara-ettinger-saxe-tenenbaum-2017} @cite{cariani-santorio-wellwood-2024} @cite{kennedy-2007} @cite{lassiter-goodman-2017} @cite{hintikka-1962}

Epistemic vocabulary — attitude verbs (believes, knows), modal verbs (might, must), and modal adjectives (likely, certain) — denotes threshold functions over agent credence Pr(A, φ).

The Core Idea

Every epistemic expression reduces to a comparison of the agent's credence against a threshold (Table 1(a)):

believes(A, φ) ⟺ Pr(A, φ) ≥ θ_believes
knows_that(A, φ) ⟺ believes(A, φ) ∧ φ
certain(A, φ) ⟺ Pr(A, φ) ≥ θ_certain
must(φ) ⟺ λA. Pr(A, φ) ≥ θ_must
likely(φ) ⟺ λA. Pr(A, φ) ≥ θ_likely
might(φ) ⟺ λA. Pr(A, φ) ≥ θ_might

Degree-Threshold Isomorphism

The threshold semantics is structurally identical to the positive form of gradable adjectives:

⟦tall⟧(x) = height(x) ≥ θ_tall (Degree/Core.positiveSem)
⟦believes⟧(A, φ) = Pr(A, φ) ≥ θ_bel (meetsThreshold)

Both are instances of the same degree-threshold architecture: a measure function maps an entity to a degree on a scale, and the predicate holds iff the degree meets a contextual/lexical threshold. Epistemic expressions are gradable predicates on a probability scale bounded by [0, 1].

This connection is formalized in §8 via epistemicAsGradable.

Unification of Three Formalizations

This collapses three previously separate treatments in the library:

1. Doxastic.lean (Hintikka): Boolean accessibility. Believes iff φ holds at ALL accessible worlds — the θ → 1 limit of threshold semantics.

2. Confidence.lean: Ordinal confidence ordering. Credence induces the same upward-monotone preorder (credence_upward_monotone below), but CSW's ordering is explicitly non-probabilistic (conjunction fallacy compatible), while LaBToM's Pr is a genuine probability.

3. Modality/ProbabilityOrdering.lean: Probability → Kratzer ordering. Threshold semantics generalizes this to agent-relative epistemic modality, unifying epistemic modals with attitude verbs under one mechanism.

Attitude–Modal Unification

Attitude verbs and epistemic modals differ only in threshold and whether the agent is syntactically projected or λ-abstracted:

Expression	Agent	θ	Category
believes	explicit	0.75	attitude verb
knows	explicit	0.75 + factive	attitude verb
certain	explicit	0.95	attitude adj
should	abstracted	0.80	modal verb
must	abstracted	0.95	modal verb
likely	abstracted	0.70	modal adj
may	abstracted	0.30	modal verb
might	abstracted	0.20	modal verb

BToM Grounding

Pr(A, φ) is computed via BToM inference (Core.BToM). Given an observed action a, the observer estimates agent credence by marginalizing:

Pr_obs(Agent, φ | a) = Σ_b P(b | a) · ⟦φ⟧_b

where P(b | a) is the BToM belief marginal (BToMModel.beliefMarginal). Through the RSA-BToM bridge (L1_eq_btom_worldMarginal), this connects to the pragmatic listener's interpretation of epistemic language.

@[reducible, inline]

abbrev Semantics.Attitudes.EpistemicThreshold.AgentCredence (E : Type u_1) (W : Type u_2) : Type (max u_1 u_2)

Agent credence: the degree of confidence agent a assigns to proposition φ being true.

This is the fundamental primitive of epistemic threshold semantics. In LaBToM, it is grounded in BToM inference: the observer computes the agent's credence by marginalizing over inferred belief states. In the abstract theory, it is any function from agents and propositions to rationals satisfying basic ordering axioms.

Equations

• Semantics.Attitudes.EpistemicThreshold.AgentCredence E W = (E → BProp W → ℚ)

structure Semantics.Attitudes.EpistemicThreshold.EpistemicEntry : Type

An epistemic lexical entry: a threshold comparison over agent credence.

Each epistemic expression (attitude verb, modal verb, modal adjective) is characterized by:

• θ: the credence threshold — the expression holds iff Pr(A, φ) ≥ θ
• factive: whether the expression additionally requires φ to be true at the evaluation world (e.g., knows but not believes)

• name : String

  Lexical item name

• θ : ℚ

  Credence threshold

• factive : Bool

  Factivity flag

instance Semantics.Attitudes.EpistemicThreshold.instDecidableEqEpistemicEntry : DecidableEq EpistemicEntry

Equations

• Semantics.Attitudes.EpistemicThreshold.instDecidableEqEpistemicEntry = Semantics.Attitudes.EpistemicThreshold.instDecidableEqEpistemicEntry.decEq

def Semantics.Attitudes.EpistemicThreshold.instDecidableEqEpistemicEntry.decEq (x✝ x✝¹ : EpistemicEntry) : Decidable (x✝ = x✝¹)

Equations

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

def Semantics.Attitudes.EpistemicThreshold.instReprEpistemicEntry.repr : EpistemicEntry → ℕ → Std.Format

Equations

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

instance Semantics.Attitudes.EpistemicThreshold.instReprEpistemicEntry : Repr EpistemicEntry

Equations

• Semantics.Attitudes.EpistemicThreshold.instReprEpistemicEntry = { reprPrec := Semantics.Attitudes.EpistemicThreshold.instReprEpistemicEntry.repr }

def Semantics.Attitudes.EpistemicThreshold.instBEqEpistemicEntry.beq : EpistemicEntry → EpistemicEntry → Bool

Equations

• Semantics.Attitudes.EpistemicThreshold.instBEqEpistemicEntry.beq { name := a, θ := a_1, factive := a_2 } { name := b, θ := b_1, factive := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Semantics.Attitudes.EpistemicThreshold.instBEqEpistemicEntry.beq x✝¹ x✝ = false

instance Semantics.Attitudes.EpistemicThreshold.instBEqEpistemicEntry : BEq EpistemicEntry

Equations

• Semantics.Attitudes.EpistemicThreshold.instBEqEpistemicEntry = { beq := Semantics.Attitudes.EpistemicThreshold.instBEqEpistemicEntry.beq }

Standard epistemic thresholds (@cite{ying-zhi-xuan-wong-mansinghka-tenenbaum-2025}, Table 1(b)).

These are the best-fit values from LaBToM's grid-search parameter fitting against human plausibility ratings in a Doors, Keys, & Gems gridworld experiment (§4.5, Table B1). The ordering is the theoretical commitment; the specific values are empirical fits:

must/certain (0.95) > should (0.80) > believes (0.75) > likely/uncertain (0.70) > unlikely (0.40) > may (0.30) > might/could (0.20)

def Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.believes_ : EpistemicEntry

Equations

• Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.believes_ = { name := "believes", θ := 3 / 4 }

def Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.knows_ : EpistemicEntry

Equations

• Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.knows_ = { name := "knows", θ := 3 / 4, factive := true }

def Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.certain_ : EpistemicEntry

Equations

• Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.certain_ = { name := "certain", θ := 19 / 20 }

def Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.must_ : EpistemicEntry

Equations

• Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.must_ = { name := "must", θ := 19 / 20 }

def Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.should_ : EpistemicEntry

Equations

• Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.should_ = { name := "should", θ := 4 / 5 }

def Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.likely_ : EpistemicEntry

Equations

• Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.likely_ = { name := "likely", θ := 7 / 10 }

def Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.may_ : EpistemicEntry

Equations

• Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.may_ = { name := "may", θ := 3 / 10 }

def Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.might_ : EpistemicEntry

Equations

• Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.might_ = { name := "might", θ := 1 / 5 }

def Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.could_ : EpistemicEntry

Equations

• Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.could_ = { name := "could", θ := 1 / 5 }

Reversed-polarity entries: these hold when credence is BELOW a threshold. uncertain and unlikely use strict < rather than ≥. They are not modeled via holdsAt but via failsThreshold (§3).

def Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.uncertain_ : EpistemicEntry

Equations

• Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.uncertain_ = { name := "uncertain", θ := 7 / 10 }

def Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.unlikely_ : EpistemicEntry

Equations

• Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.unlikely_ = { name := "unlikely", θ := 2 / 5 }

theorem Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.scale_must_gt_should : 19 / 20 > 4 / 5

The full threshold scale (Table 1(b)): must = certain > should > believes > likely = uncertain > unlikely > may > might = could

theorem Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.scale_should_gt_believes : 4 / 5 > 3 / 4

theorem Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.scale_believes_gt_likely : 3 / 4 > 7 / 10

theorem Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.scale_likely_gt_unlikely : 7 / 10 > 2 / 5

theorem Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.scale_unlikely_gt_may : 2 / 5 > 3 / 10

theorem Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.scale_may_gt_might : 3 / 10 > 1 / 5

def Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.α_most : ℚ

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

Equations

• Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.α_most = 3 / 2

def Semantics.Attitudes.EpistemicThreshold.meetsThreshold {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (θ : ℚ) (a : E) (φ : BProp W) : Prop

Threshold semantics: agent a's credence in φ meets threshold θ.

This is the single mechanism underlying all epistemic vocabulary. believes, knows, certain, must, might are all instances.

Structurally identical to Degree.positiveSem μ θ x: both are measure(entity) ≥ threshold.

Equations

• Semantics.Attitudes.EpistemicThreshold.meetsThreshold cr θ a φ = (cr a φ ≥ θ)

def Semantics.Attitudes.EpistemicThreshold.failsThreshold {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (θ : ℚ) (a : E) (φ : BProp W) : Prop

Reversed threshold: agent a's credence in φ is strictly BELOW θ.

Used for uncertain and unlikely: uncertain_if(A, φ, ψ) holds iff Pr(A, φ) < θ_uncertain ∧ Pr(A, ψ) < θ_uncertain (Table 1(a)).

Equations

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

def Semantics.Attitudes.EpistemicThreshold.holdsAt {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (entry : EpistemicEntry) (a : E) (φ : BProp W) (w : W) : Prop

Full epistemic evaluation: credence meets threshold, plus factivity.

• believes(A, φ, w) = Pr(A, φ) ≥ 0.75
• knows(A, φ, w) = Pr(A, φ) ≥ 0.75 ∧ φ(w) = true

Equations

• Semantics.Attitudes.EpistemicThreshold.holdsAt cr entry a φ w = (Semantics.Attitudes.EpistemicThreshold.meetsThreshold cr entry.θ a φ ∧ (entry.factive = true → φ w = true))

def Semantics.Attitudes.EpistemicThreshold.knowsIf {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ : BProp W) (w : W) : Prop

knows_if(A, φ) = knows_that(A, φ) ∨ knows_that(A, ¬φ). The agent knows the answer to the yes/no question ?φ.

Equations

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

def Semantics.Attitudes.EpistemicThreshold.notKnowsThat {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ : BProp W) (w : W) : Prop

not_knows_that(A, φ) = ¬believes(A, φ) ∧ φ. False belief: φ is true but the agent doesn't believe it.

Equations

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

def Semantics.Attitudes.EpistemicThreshold.uncertainIf {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ ψ : BProp W) : Prop

uncertain_if(A, φ, ψ) = Pr(A, φ) < θ_uncertain ∧ Pr(A, ψ) < θ_uncertain. The agent is uncertain between two alternatives.

Equations

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

def Semantics.Attitudes.EpistemicThreshold.degree {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ : BProp W) : ℚ

degree(likely, A, φ) = Pr(A, φ). The raw credence, used as input to comparative and superlative constructions. This IS the measure function on the epistemic scale.

Equations

• Semantics.Attitudes.EpistemicThreshold.degree cr a φ = cr a φ

def Semantics.Attitudes.EpistemicThreshold.moreCredent {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ ψ : BProp W) : Prop

Comparative credence: more(P, φ, ψ) = degree(P, A, φ) > degree(P, A, ψ).

The agent's credence in φ strictly exceeds credence in ψ. Mirrors the comparative from Confidence.lean and from Degree/Core.lean.

Equations

• Semantics.Attitudes.EpistemicThreshold.moreCredent cr a φ ψ = (cr a ψ < cr a φ)

def Semantics.Attitudes.EpistemicThreshold.mostStr {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (entry : EpistemicEntry) (a : E) (φ : BProp W) : Prop

Superlative: most_str(P, φ) = degree(P, A, φ) ≥ α_most · θ_P. Strengthened superlative with multiplier α_most = 1.5 (Table 1(b)).

Equations

• Semantics.Attitudes.EpistemicThreshold.mostStr cr entry a φ = (cr a φ ≥ Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.α_most * entry.θ)

theorem Semantics.Attitudes.EpistemicThreshold.threshold_monotone {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ : BProp W) {θ₁ θ₂ : ℚ} (h : θ₁ ≤ θ₂) : meetsThreshold cr θ₂ a φ → meetsThreshold cr θ₁ a φ

Higher thresholds entail lower thresholds.

If an expression with threshold θ₂ holds, then any expression with a lower threshold θ₁ ≤ θ₂ also holds. This derives the entailment patterns of epistemic vocabulary from the threshold ordering alone.

theorem Semantics.Attitudes.EpistemicThreshold.knows_entails_believes {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ : BProp W) (w : W) : holdsAt cr EpistemicEntry.knows_ a φ w → holdsAt cr EpistemicEntry.believes_ a φ w

knows entails believes: knowledge implies belief.

Since knows and believes share the same threshold (0.75) and knows only adds factivity, the credence condition carries over.

theorem Semantics.Attitudes.EpistemicThreshold.knows_is_veridical {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ : BProp W) (w : W) : holdsAt cr EpistemicEntry.knows_ a φ w → φ w = true

knows is veridical: knowledge entails truth.

This mirrors Veridicality.veridical in Doxastic.lean: veridical predicates entail their complement. In ELoT, veridicality is the factive = true flag.

theorem Semantics.Attitudes.EpistemicThreshold.certain_entails_believes {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ : BProp W) (w : W) : holdsAt cr EpistemicEntry.certain_ a φ w → holdsAt cr EpistemicEntry.believes_ a φ w

certain entails believes: θ_certain = 19/20 ≥ θ_believes = 3/4.

theorem Semantics.Attitudes.EpistemicThreshold.must_entails_should {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ : BProp W) (w : W) : holdsAt cr EpistemicEntry.must_ a φ w → holdsAt cr EpistemicEntry.should_ a φ w

must entails should: θ_must = 19/20 ≥ θ_should = 4/5.

theorem Semantics.Attitudes.EpistemicThreshold.should_entails_likely {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ : BProp W) (w : W) : holdsAt cr EpistemicEntry.should_ a φ w → holdsAt cr EpistemicEntry.likely_ a φ w

should entails likely: θ_should = 4/5 ≥ θ_likely = 7/10.

theorem Semantics.Attitudes.EpistemicThreshold.must_entails_might {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ : BProp W) (w : W) : holdsAt cr EpistemicEntry.must_ a φ w → holdsAt cr EpistemicEntry.might_ a φ w

must entails might: necessity entails possibility.

θ_must = 19/20 ≥ θ_might = 1/5. This is the epistemic modal analogue of □φ → ◇φ.

theorem Semantics.Attitudes.EpistemicThreshold.believes_entails_may {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ : BProp W) (w : W) : holdsAt cr EpistemicEntry.believes_ a φ w → holdsAt cr EpistemicEntry.may_ a φ w

believes entails may: θ_believes = 3/4 ≥ θ_may = 3/10.

theorem Semantics.Attitudes.EpistemicThreshold.moreCredent_transitive {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ ψ χ : BProp W) (h₁ : moreCredent cr a φ ψ) (h₂ : moreCredent cr a ψ χ) : moreCredent cr a φ χ

Comparative credence is transitive.

Mirrors comparative_transitive in Confidence.lean (CSW (54)).

theorem Semantics.Attitudes.EpistemicThreshold.credence_upward_monotone {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (θ : ℚ) (a : E) (φ ψ : BProp W) (h_bel : meetsThreshold cr θ a φ) (h_more : cr a φ ≤ cr a ψ) : meetsThreshold cr θ a ψ

Upward monotonicity of belief under the credence ordering.

If the agent believes φ and is at least as confident of ψ as of φ, then the agent believes ψ. This is the credence-based analogue of confidence_upward_monotone in Confidence.lean (CSW (53)).

Key Divergence from Confidence.lean

CSW's confidence ordering is NOT constrained to respect logical conjunction: conjunction_fallacy_compatible (Confidence.lean) shows it is consistent to be confident of (p ∧ q) without being confident of p.

When AgentCredence is a genuine probability measure (as in LaBToM), this cannot happen: Pr(A, p ∧ q) ≤ Pr(A, p) always. The two theories make different empirical predictions about conjunction fallacy data.

def Semantics.Attitudes.EpistemicThreshold.isProbabilistic {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) : Prop

A probabilistic credence function is Monotone (from Mathlib) in the pointwise Bool ordering on BProp W: if φ ⊆ ψ then Pr(A, φ) ≤ Pr(A, ψ).

This is the axiom that separates LaBToM's probabilistic credence from CSW's ordinal confidence ordering. CSW's ordering permits conjunction fallacies (conjunction_fallacy_compatible in Confidence.lean); isProbabilistic rules them out.

Conjunction elimination (isProbabilistic_conj_elim) is a consequence: since φ ∧ ψ ≤ φ pointwise, monotonicity gives Pr(A, φ ∧ ψ) ≤ Pr(A, φ). In fact the two are equivalent on BProp W (a SemilatticeInf), since a ≤ b ↔ a ⊓ b = a.

By using Mathlib's Monotone, this connects to the same abstract notion used throughout linglib: IsUpwardEntailing = Monotone (Entailment/Polarity.lean), MeasureMonotone = ∀ i w, Monotone (KnowledgeProbability.lean), etc.

Equations

• Semantics.Attitudes.EpistemicThreshold.isProbabilistic cr = ∀ (a : E), Monotone (cr a)

theorem Semantics.Attitudes.EpistemicThreshold.isProbabilistic_conj_elim {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (h_prob : isProbabilistic cr) (a : E) (φ ψ : BProp W) : (cr a fun (w : W) => φ w && ψ w) ≤ cr a φ

Conjunction elimination follows from isProbabilistic: since φ ∧ ψ ≤ φ in the pointwise Bool ordering, monotonicity gives Pr(A, φ ∧ ψ) ≤ Pr(A, φ).

theorem Semantics.Attitudes.EpistemicThreshold.prob_conjunction_elim {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (h_prob : isProbabilistic cr) (θ : ℚ) (a : E) (φ ψ : BProp W) (h_bel : meetsThreshold cr θ a fun (w : W) => φ w && ψ w) : meetsThreshold cr θ a φ

Probabilistic credence validates conjunction elimination for belief.

If the agent believes (φ ∧ ψ) and credence is probabilistic, then the agent believes φ. This fails for CSW's non-probabilistic ordering (conjunction fallacy).

Connection to BToM Inference

The observer estimates an agent's credence by marginalizing over the BToM belief marginal (BToMModel.beliefMarginal):

Pr_obs(Agent, φ | a) = Σ_b P(b | a) · ⟦φ⟧_b

When B = W (the RSA-BToM bridge's perfect-knowledge assumption, RSAConfig.toBToM), this becomes:

Pr_obs(Agent, φ | a) = Σ_w P(w | a) · φ(w)

which is just the observer's expected truth-value of φ under their posterior about the world — exactly what RSA's L1 listener computes. The full chain is:

L1 posterior → BToM belief marginal → agent credence → threshold → ELoT

This makes the interpretation of epistemic language a BToM inference problem: understanding "the player thinks the key might be in box 3" requires jointly inferring the player's belief state via inverse planning, then evaluating the ELoT formula against the inferred credences.

See BToMModel.beliefExpectation in Core.BToM for the generic belief-weighted sum, and L1_eq_btom_worldMarginal in RSA.Core.Config for the RSA-BToM identity.

noncomputable def Semantics.Attitudes.EpistemicThreshold.btomCredence {F : Type u_3} [CommSemiring F] {A : Type u_4} {P : Type u_5} {B : Type u_6} {D : Type u_7} {S : Type u_8} {M : Type u_9} {W : Type u_10} [Fintype P] [Fintype B] [Fintype D] [Fintype S] [Fintype M] [Fintype W] (model : Core.BToM.BToMModel F A P B D S M W) (eval : B → BProp W → F) (a : A) (φ : BProp W) : F

Agent credence derived from BToM belief-marginal inference.

Given a BToM model with belief type B and an evaluation function eval : B → BProp W → F that computes how belief state b rates proposition φ, the observer estimates the agent's credence after observing action a:

Pr_obs(Agent, φ | a) = Σ_b P(b | a) · eval(b, φ)

This is BToMModel.beliefExpectation applied to fun b => eval b φ, grounding the abstract AgentCredence in concrete BToM inference.

When B = W and eval b φ = if φ b then 1 else 0 (the RSA-BToM bridge's perfect-knowledge assumption), this reduces to the L1 listener's expected truth-value under their world posterior.

Polymorphic in F so it composes with both ℚ-valued (exact computation) and ℝ-valued (RSAConfig.toBToM) models.

Equations

• Semantics.Attitudes.EpistemicThreshold.btomCredence model eval a φ = model.beliefExpectation (fun (b : B) => eval b φ) a

theorem Semantics.Attitudes.EpistemicThreshold.identity_belief_eq_world_marginal {W : Type u_2} {F : Type u_3} [CommSemiring F] [DecidableEq W] {A : Type u_4} {D : Type u_5} {S : Type u_6} {M : Type u_7} [Fintype W] [Fintype D] [Fintype S] [Fintype M] (model : Core.BToM.BToMModel F A W W D S M W) (h_percept : ∀ (w p : W), model.perceptModel w p = if p = w then 1 else 0) (h_belief : ∀ (p b : W), model.beliefModel p b = if b = p then 1 else 0) (a : A) (b : W) : model.beliefMarginal a b = model.worldMarginal a b

theorem Semantics.Attitudes.EpistemicThreshold.btomCredence_eq_world_expectation {W : Type u_2} {F : Type u_3} [CommSemiring F] [DecidableEq W] {A : Type u_4} {D : Type u_5} {S : Type u_6} {M : Type u_7} [Fintype W] [Fintype D] [Fintype S] [Fintype M] (model : Core.BToM.BToMModel F A W W D S M W) (h_percept : ∀ (w p : W), model.perceptModel w p = if p = w then 1 else 0) (h_belief : ∀ (p b : W), model.beliefModel p b = if b = p then 1 else 0) (eval : W → BProp W → F) (a : A) (φ : BProp W) : btomCredence model eval a φ = ∑ w : W, model.worldMarginal a w * eval w φ

For identity-perception BToM models, btomCredence is the world-marginal-weighted evaluation of φ.

This connects the abstract btomCredence to concrete RSA inference: when the BToM model has identity perception/belief (as in RSAConfig.toBToM), computing agent credence via BToM belief marginals is the same as computing the L1 listener's expected truth-value.

btomCredence(model, eval, a, φ)
  = Σ_b beliefMarginal(a, b) · eval(b, φ)
  = Σ_w worldMarginal(a, w) · eval(w, φ)    [by identity_belief_eq_world_marginal]

The second line is exactly the L1 listener's posterior expectation (via L1_eq_btom_worldMarginal in RSA.Core.Config).

Epistemic Expressions as Gradable Predicates

The structural analogy between adjective degree semantics (@cite{kennedy-2007}, @cite{lassiter-goodman-2017}) and epistemic threshold semantics: both are instances of μ(entity) ≥ θ. The threshold semantics makes this precise:

⟦tall⟧(x) = height(x) ≥ θ_tall (Degree.positiveSem)
⟦believes⟧(A, φ) = Pr(A, φ) ≥ θ_bel (meetsThreshold)

Both are instances of μ(entity) ≥ θ. The epistemic scale is the probability interval [0, 1], which is closed in the sense of @cite{kennedy-2007}: it has both an upper bound (certainty, 1) and a lower bound (impossibility, 0).

This has consequences for scale structure:

• Closed-scale adjectives (like full, certain) license absolute standards (the endpoint). For certain, the endpoint IS θ = 0.95 ≈ 1.
• Open-scale adjectives (like tall) require contextual standards. For likely, the threshold θ = 0.70 is contextually fit.

The structural parallel also extends to comparatives and superlatives:

• "more likely than" = moreCredent (comparative on probability scale)
• "most likely" = mostStr with multiplier α_most = 1.5

See Theories/Semantics/Probabilistic/SDS/ThresholdSemantics.lean for the unified threshold pattern across adjectives, generics, and epistemic expressions.

def Semantics.Attitudes.EpistemicThreshold.epistemicBoundedness : Core.Scale.Boundedness

The epistemic probability scale is closed: bounded by [0, 1].

This classifies the credence scale as Boundedness.closed, meaning epistemic adjectives like certain license absolute standards.

Equations

• Semantics.Attitudes.EpistemicThreshold.epistemicBoundedness = Core.Scale.Boundedness.closed

def Semantics.Attitudes.EpistemicThreshold.epistemicAsGradable {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (entry : EpistemicEntry) : Degree.GradablePredicate (E × BProp W) ℚ

An epistemic gradable predicate: an EpistemicEntry viewed as a GradablePredicate on the probability scale.

The entity type is E × BProp W (agent–proposition pairs), and the measure function is agent credence cr. This makes the structural identity with degree semantics explicit and type-checked.

Polarity: threshold entries (believes, must, likely) are positive (upward monotone: higher credence → more likely to satisfy). Reversed entries (uncertain, unlikely) are negative (downward monotone).

Equations

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

theorem Semantics.Attitudes.EpistemicThreshold.meetsThreshold_eq_positiveSem {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (θ : ℚ) (a : E) (φ : BProp W) : meetsThreshold cr θ a φ ↔ Degree.positiveSem (fun (p : E × BProp W) => cr p.1 p.2) θ (a, φ)

The degree-threshold identity: meetsThreshold is positiveSem instantiated on the epistemic scale.

This is the formal statement that epistemic threshold semantics IS degree semantics with credence as the measure function.

theorem Semantics.Attitudes.EpistemicThreshold.epistemicScale_licensed : epistemicBoundedness.isLicensed = true

The epistemic scale is licensed: closed → admits absolute standards.

Since credence is bounded by [0, 1], @cite{kennedy-2007}'s licensing prediction says epistemic adjectives like certain can use endpoint standards (θ ≈ 1.0). This unifies with the five-framework licensing agreement from Core/EpistemicScale.lean.

From Credence to Comparative Likelihood

When AgentCredence is a genuine probability measure (probabilistic credence), it induces the full @cite{holliday-icard-2013} hierarchy:

AgentCredence → FinAddMeasure → EpistemicSystemFA
                                ↓
                          comparative likelihood ≿
                                ↓
                          threshold cuts → ELoT

The key insight: moreCredent cr a φ ψ (comparative epistemic) is exactly FinAddMeasure.inducedGe applied to singleton propositions. Threshold semantics then arises by cutting this comparative ordering at specific points on the scale.

This places the Ying et al. threshold semantics within the algebraic framework of Core/EpistemicScale.lean: the fitted thresholds from Table 1(b) are points on a finitely additive probability scale that satisfies System FA (and hence all of W ⊂ F ⊂ FA).

theorem Semantics.Attitudes.EpistemicThreshold.threshold_upwardMonotone {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ : BProp W) (θ₁ θ₂ : ℚ) : θ₁ ≤ θ₂ → meetsThreshold cr θ₂ a φ → meetsThreshold cr θ₁ a φ

Threshold semantics is upward monotone in the credence ordering: if cr a φ ≥ θ and cr a φ ≤ cr a ψ, then cr a ψ ≥ θ.

This is an instance of Core.Scale.IsUpwardMonotone applied to the epistemic scale. The family of propositions P(θ) = meetsThreshold θ is upward monotone in credence — higher credence always satisfies lower thresholds.

Connects to CSW's confidence_upward_monotone and to Lassiter's observation that epistemic modals form a Horn scale ordered by threshold strength.

theorem Semantics.Attitudes.EpistemicThreshold.failsThreshold_downwardMonotone {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ : BProp W) (θ₁ θ₂ : ℚ) : θ₁ ≤ θ₂ → failsThreshold cr θ₁ a φ → failsThreshold cr θ₂ a φ

failsThreshold is downward monotone: if credence is below θ₁ and θ₁ ≤ θ₂, then credence is below θ₂. This is the polarity reversal for uncertain/unlikely: higher thresholds are easier to fail.

Connects to Kennedy's negative adjective pattern (short, cold): negative polarity on the same scale.

def Semantics.Attitudes.EpistemicThreshold.epistemicComparativeScale : Core.Scale.ComparativeScale ℚ

The epistemic threshold scale forms a ComparativeScale with closed boundedness. This places it in the same categorical structure as Kennedy's adjective scales, Krifka's mereological scales, and Holliday–Icard's epistemic likelihood scales.

Equations

• Semantics.Attitudes.EpistemicThreshold.epistemicComparativeScale = { boundedness := Semantics.Attitudes.EpistemicThreshold.epistemicBoundedness }

theorem Semantics.Attitudes.EpistemicThreshold.moreCredent_iff_degree {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ ψ : BProp W) : moreCredent cr a φ ψ ↔ degree cr a ψ < degree cr a φ

Comparative credence is the measure-induced ordering on propositions: moreCredent cr a φ ψ ↔ cr a ψ < cr a φ.

This is the analogue of FinAddMeasure.inducedGe applied to agent credence: the comparative likelihood ordering on propositions is induced by the credence measure. The threshold entries from Table 1(b) are then points where we cut this ordering.

Kennedy's Reduction: Comparative from Positive

The central formal insight of @cite{kennedy-2007} — extended here to epistemic modality — is that the comparative is not an independent primitive but reduces to the positive form via existential quantification over thresholds:

"φ more likely than ψ" ↔ ∃θ. likely_θ(φ) ∧ ¬likely_θ(ψ)

In words: φ is more likely than ψ iff there is some threshold that φ's credence meets but ψ's doesn't. This means the comparative ordering on propositions is determined by the family of positive-form predicates {meetsThreshold θ | θ ∈ ℚ}. The same reduction works for adjectives:

"A taller than B" ↔ ∃θ. tall_θ(A) ∧ ¬tall_θ(B)

The non-trivial part is that this is a biconditional: not only does a separating threshold imply the comparative (easy direction), but the comparative implies a separating threshold exists (uses the witness θ = cr(a, φ), which meets for φ by reflexivity and fails for ψ by the comparative hypothesis). This is a genuine mathematical fact about the structure of threshold semantics on a linear order.

theorem Semantics.Attitudes.EpistemicThreshold.comparative_from_positive {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ ψ : BProp W) : moreCredent cr a φ ψ ↔ ∃ (θ : ℚ), meetsThreshold cr θ a φ ∧ ¬meetsThreshold cr θ a ψ

Kennedy's reduction: the comparative reduces to the positive form.

"φ more likely than ψ" iff there exists a threshold that φ meets and ψ fails. This is THE structural theorem connecting comparative and positive-form degree semantics.

• Forward: if cr(a,ψ) < cr(a,φ), witness θ = cr(a,φ).
• Backward: if θ separates, then cr(a,ψ) < θ ≤ cr(a,φ).

@cite{kennedy-2007} §3: the same reduction applies to epistemic modals because credence IS a measure function.

theorem Semantics.Attitudes.EpistemicThreshold.meetsThreshold_iff_not_failsThreshold {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (θ : ℚ) (a : E) (φ : BProp W) : meetsThreshold cr θ a φ ↔ ¬failsThreshold cr θ a φ

Polarity duality: meetsThreshold (positive) ↔ ¬failsThreshold.

On a linear order, cr(a,φ) ≥ θ iff ¬(cr(a,φ) < θ). This is not rfl — it requires not_lt on ℚ's linear order.

On a probability scale, positive and negative epistemic modals are contradictories, not contraries — the same threshold θ separates "likely" from "unlikely" (cf. @cite{lassiter-goodman-2017} fn. 8 for the analogous tall/short case).

theorem Semantics.Attitudes.EpistemicThreshold.antonymy_from_polarity {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ ψ : BProp W) : moreCredent cr a φ ψ ↔ ∃ (θ : ℚ), meetsThreshold cr θ a φ ∧ failsThreshold cr θ a ψ

Antonymy from polarity: the comparative holds iff there exists a threshold where the positive predicate holds for φ and the negative predicate holds for ψ.

This is the formal content of "antonymy = scale reversal": the comparative "more likely" decomposes into a threshold that is simultaneously met by φ (positive: likely_θ) and failed by ψ (negative: unlikely_θ). Unlike the rfl-level type coincidence, this derives the antonymy connection from comparative_from_positive

• meetsThreshold_iff_not_failsThreshold.

The likely/unlikely pattern parallels @cite{lassiter-goodman-2017}'s tall/short (Eqs. 22–23): same scale, reversed polarity.

Operators with Quantification over Entities

Table 1(a) includes operators that quantify over a context-restricted domain of entities: knows_about, certain_about, uncertain_about, and most_sup. These handle sentences like "The player knows which box has the key" (knows_about) or "The player is uncertain about what's in box 3" (uncertain_about).

These are parameterized by an entity type X (the quantification domain) and a context set C : X → Prop restricting the domain.

def Semantics.Attitudes.EpistemicThreshold.knowsAbout {E : Type u_1} {W : Type u_2} {X : Type u_3} (cr : AgentCredence E W) (a : E) (C : X → Prop) (φ : X → BProp W) (w : W) : Prop

knows_about(A, C, φ) = ∃x. C(x) ∧ knows_that(A, φ(x)).

The agent knows, for some contextually relevant entity x, that φ(x). Table 1(a): Type ε, Arg Types A, Φ/O, Φ/O.

Equations

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

def Semantics.Attitudes.EpistemicThreshold.certainAbout {E : Type u_1} {W : Type u_2} {X : Type u_3} (cr : AgentCredence E W) (a : E) (C : X → Prop) (φ : X → BProp W) : Prop

certain_about(A, C, φ) = ∃x. C(x) ∧ Pr(A, φ(x)) ≥ θ_certain.

The agent is certain, for some contextually relevant entity, that φ holds. Table 1(a).

Equations

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

def Semantics.Attitudes.EpistemicThreshold.uncertainAbout {E : Type u_1} {W : Type u_2} {X : Type u_3} (cr : AgentCredence E W) (a : E) (C : X → Prop) (φ : X → BProp W) : Prop

uncertain_about(A, C, φ) = ∀x. C(x) → Pr(A, φ(x)) < θ_uncertain.

The agent is uncertain about φ for ALL contextually relevant entities. Note the universal quantification — this is the dual of certain_about's existential. Table 1(a).

Equations

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

def Semantics.Attitudes.EpistemicThreshold.mostSup {E : Type u_1} {W : Type u_2} {X : Type u_3} (cr : AgentCredence E W) (a : E) (o : X) (C : X → Prop) (φ : X → BProp W) : Prop

most_sup(P, O, C, φ): the degree of φ(O) is at least as great as the degree of φ(x) for every x in the context set C.

"The player believes the key is most likely to be in box 1" means credence in "key in box 1" ≥ credence in "key in box x" for all relevant boxes x. Table 1(a).

Equations

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

theorem Semantics.Attitudes.EpistemicThreshold.knowsAbout_entails_knowsThat {E : Type u_1} {W : Type u_2} {X : Type u_3} (cr : AgentCredence E W) (a : E) (C : X → Prop) (φ : X → BProp W) (w : W) (x : X) (hC : C x) : holdsAt cr EpistemicEntry.knows_ a (φ x) w → knowsAbout cr a C φ w

knows_about entails knows_that for any witness.

theorem Semantics.Attitudes.EpistemicThreshold.certainAbout_entails_believes {E : Type u_1} {W : Type u_2} {X : Type u_3} (cr : AgentCredence E W) (a : E) (C : X → Prop) (φ : X → BProp W) (h : certainAbout cr a C φ) : ∃ (x : X), C x ∧ meetsThreshold cr EpistemicEntry.believes_.θ a (φ x)

certain_about entails that the agent believes the witness proposition.

theorem Semantics.Attitudes.EpistemicThreshold.uncertainAbout_contradicts_certainAbout {E : Type u_1} {W : Type u_2} {X : Type u_3} (cr : AgentCredence E W) (a : E) (C : X → Prop) (φ : X → BProp W) (h_unc : uncertainAbout cr a C φ) (h_cert : certainAbout cr a C φ) : False

uncertain_about and certain_about are incompatible: if the agent is uncertain about all C-entities, there is no C-entity about which the agent is certain.

Compositional Modal Embedding

The key compositional device from Table 1(a): believes_modal(A, M) = M(A). When a belief verb embeds a modal, the modal's threshold determines the evaluation, not the belief verb's.

"A believes it might rain" = believes_modal(A, might(rain)) = might(rain)(A) = Pr(A, rain) ≥ θ_might.

This uses θ_might (0.20), not θ_believes (0.75), because the compositional lowering rule passes through the modal operator rather than the attitude verb. The result is a genuine compositional semantics: the meaning of the complex expression is determined by its parts.

def Semantics.Attitudes.EpistemicThreshold.believesModal {E : Type u_1} (M : E → Prop) (a : E) : Prop

Modal embedding: believes_modal(A, M) = M(A).

M is a modal property of agents (e.g., fun a => meetsThreshold cr θ_might a φ). Applying believesModal to it just evaluates M at agent A — the modal's threshold wins. Table 1(a): Type ε, Arg Types A, ε/A, Definition M(A).

Equations

• Semantics.Attitudes.EpistemicThreshold.believesModal M a = M a

theorem Semantics.Attitudes.EpistemicThreshold.believesModal_lowers_to_modal_threshold {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ : BProp W) : believesModal (fun (a' : E) => meetsThreshold cr EpistemicEntry.might_.θ a' φ) a ↔ meetsThreshold cr EpistemicEntry.might_.θ a φ

The compositional lowering: "A believes might(φ)" uses θ_might, not θ_believes.

This is the formal content of the paper's compositional semantics: when a belief verb embeds a modal, the result is evaluated at the modal's threshold. The belief verb contributes nothing beyond agent projection.

theorem Semantics.Attitudes.EpistemicThreshold.believesModal_transparent {E : Type u_1} (M : E → Prop) (a : E) : believesModal M a ↔ M a

More generally, believesModal is transparent: believesModal M a ↔ M a.

Formal Bridges to Doxastic.lean and Confidence.lean

The claimed unification (§1) of three formalizations is backed by structural theorems:

1. Doxastic bridge: at θ = 1, threshold semantics recovers universal quantification (the Hintikka limit).

2. Confidence bridge: probabilistic credence induces a preorder that validates CSW's upward monotonicity but rules out their conjunction fallacy.

theorem Semantics.Attitudes.EpistemicThreshold.threshold_one_requires_max_credence {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ : BProp W) : meetsThreshold cr 1 a φ ↔ 1 ≤ cr a φ

Doxastic bridge: at threshold 1, meetsThreshold requires maximal credence (cr ≥ 1).

Since credence is a probability in [0, 1], this is equivalent to cr = 1, which corresponds to truth at ALL accessible worlds in Hintikka's semantics (Doxastic.boxAt). This justifies calling Boolean accessibility "the θ → 1 limit of threshold semantics."

The bridge is structural, not definitional: Doxastic.lean uses List-based universal quantification while this module uses ℚ-valued credence. The two coincide when the credence function assigns 1 iff φ holds universally.

theorem Semantics.Attitudes.EpistemicThreshold.credence_ordering_is_preorder {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) : (∀ (φ : BProp W), cr a φ ≤ cr a φ) ∧ ∀ (φ ψ χ : BProp W), cr a φ ≤ cr a ψ → cr a ψ ≤ cr a χ → cr a φ ≤ cr a χ

Confidence bridge: the credence ordering on propositions is a preorder (reflexive and transitive).

This mirrors the preorder axioms of CSW's confidence ordering (Confidence.lean), showing that probabilistic credence induces the same algebraic structure. The key difference is that probabilistic credence additionally validates conjunction elimination (isProbabilistic_conj_elim), which CSW's ordering does not (conjunction_fallacy_compatible).

theorem Semantics.Attitudes.EpistemicThreshold.probabilistic_conjunction_elim_for_all_thresholds {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (h_prob : isProbabilistic cr) (a : E) (φ ψ : BProp W) (θ : ℚ) : (meetsThreshold cr θ a fun (w : W) => φ w && ψ w) → meetsThreshold cr θ a φ

Probabilistic credence validates conjunction elimination for meetsThreshold, but CSW's non-probabilistic ordering does not. This is the key empirical divergence between the two theories.

Formally: under isProbabilistic, if meetsThreshold cr θ a (φ ∧ ψ) then meetsThreshold cr θ a φ. Under CSW's ordering, this can fail (conjunction fallacy).

theorem Semantics.Attitudes.EpistemicThreshold.threshold_exhaustive {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (θ : ℚ) (a : E) (φ : BProp W) : meetsThreshold cr θ a φ ∨ failsThreshold cr θ a φ

meetsThreshold and failsThreshold are exhaustive: for any credence and threshold, exactly one holds. This is excluded middle on the linear order ℚ.