Epistemic Threshold Semantics

@cite{ying-zhi-xuan-wong-mansinghka-tenenbaum-2025} @cite{baker-jara-ettinger-saxe-tenenbaum-2017} @cite{klein-1980} @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, φ).

This file formalizes the probabilistic-credence-with-threshold tradition (LaBToM: @cite{ying-zhi-xuan-wong-mansinghka-tenenbaum-2025}; epistemic modals: @cite{lassiter-goodman-2017}). It is not a formalization of @cite{cariani-santorio-wellwood-2024}'s confidence semantics — CSW's account is in Confidence.lean and is explicitly non-probabilistic. §6 below documents the empirical disagreement between the two traditions; the refutation theorem confidence_not_probabilistic packages it formally.

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/Basic.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). 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 → (W → Bool) → ℚ)

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)

The lexical form (English string) is not stored on the entry — Fragment files (Fragments/English/...) carry the form-to-entry mapping; the entry itself is purely semantic.

• θ : ℚ

  Credence threshold

• factive : Bool

  Factivity flag

@[implicit_reducible]

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.

@[implicit_reducible]

instance Semantics.Attitudes.EpistemicThreshold.instReprEpistemicEntry : Repr EpistemicEntry

Equations

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

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

Equations

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

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_ = { θ := 3 / 4 }

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

Equations

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

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

Equations

• Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.certain_ = { θ := 19 / 20 }

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

Equations

• Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.must_ = { θ := 19 / 20 }

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

Equations

• Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.should_ = { θ := 4 / 5 }

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

Equations

• Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.likely_ = { θ := 7 / 10 }

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

Equations

• Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.may_ = { θ := 3 / 10 }

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

Equations

• Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.might_ = { θ := 1 / 5 }

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

Equations

• Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.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_ = { θ := 7 / 10 }

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

Equations

• Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.unlikely_ = { θ := 2 / 5 }

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

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

Proven by reducing IsChain on the explicit list to a conjunction of pairwise inequalities, then closing each by norm_num.

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) (φ : W → Bool) : 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) (φ : W → Bool) : 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) (φ : W → Bool) (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) (φ : W → Bool) (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) (φ : W → Bool) (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) (φ ψ : W → Bool) : 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.moreCredent {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ ψ : W → Bool) : Prop

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

The agent's credence in φ strictly exceeds credence in ψ. Mirrors the comparative from Confidence.lean and from Degree/Basic.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) (φ : W → Bool) : 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) (φ : W → Bool) {θ₁ θ₂ : ℚ} (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.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 : AgentCredence E W) (a : E) (φ : W → Bool) (w : W) : holdsAt cr e₂ a φ w → holdsAt cr e₁ a φ w

Generic holdsAt entailment: a stronger entry (higher threshold, weaker factivity) entails a weaker one.

Factors threshold_monotone plus the factivity-loss requirement. Every named pairwise entailment below is one application of this lemma.

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

knows entails believes: same threshold, knows adds factivity.

theorem Semantics.Attitudes.EpistemicThreshold.knows_is_veridical {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ : W → Bool) (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) (φ : W → Bool) (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) (φ : W → Bool) (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) (φ : W → Bool) (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) (φ : W → Bool) (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.

theorem Semantics.Attitudes.EpistemicThreshold.believes_entails_may {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (a : E) (φ : W → Bool) (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) (φ ψ χ : W → Bool) (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) (φ ψ : W → Bool) (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 (W → Bool): 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 (W → Bool) (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) (φ ψ : W → Bool) : (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) (φ ψ : W → Bool) (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).

theorem Semantics.Attitudes.EpistemicThreshold.confidence_not_probabilistic : ∃ (cr : AgentCredence Unit Bool), ¬isProbabilistic cr ∧ ∃ (φ : Bool → Bool) (ψ : Bool → Bool), cr () φ < cr () fun (w : Bool) => φ w && ψ w

CSW vs threshold-credence divergence theorem.

There exists an AgentCredence admitting a conjunction-fallacy witness — formally, an instance where cr (φ ∧ ψ) > cr φ — and consequently failing isProbabilistic.

This formalizes the empirical disagreement CSW §4.6 (around (52)) use to argue against probabilistic-credence accounts of confidence: Confidence.conjunction_fallacy_compatible shows the CSW ordering admits such witnesses (the John/Linda case from @cite{tversky-kahneman-1983}); this theorem shows that any credence function reproducing such a witness cannot satisfy isProbabilistic. The two theories therefore make incompatible predictions about the same data point.

Witness construction: cr assigns 1 to the always-false proposition and 0 to everything else, on Unit-agent / Bool-world. Then id ∧ (fun w => !w) = (fun _ => false), so cr (id ∧ neg) = 1 > 0 = cr id realizes the John/Linda pattern. The cr is non-monotone because (fun _ => false) ≤ id pointwise but 1 > 0.

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 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.BToMModel F A P B D S M W) (eval : B → (W → Bool) → F) (a : A) (φ : W → Bool) : F

Agent credence derived from BToM belief-marginal inference.

Given a BToM model with belief type B and an evaluation function eval : B → (W → Bool) → 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.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.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 → (W → Bool) → F) (a : A) (φ : W → Bool) : 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 × (W → Bool)) ℚ

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

The entity type is E × (W → Bool) (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) (φ : W → Bool) : meetsThreshold cr θ a φ ↔ Degree.positiveSem (fun (p : E × (W → Bool)) => 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) (φ : W → Bool) (θ₁ θ₂ : ℚ) : θ₁ ≤ θ₂ → 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) (φ : W → Bool) (θ₁ θ₂ : ℚ) : θ₁ ≤ θ₂ → 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 }

Klein's Reduction: Comparative from Positive

The central formal insight of @cite{klein-1980} — 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 (or contexts, in Klein's original delineation semantics):

"φ 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) (φ ψ : W → Bool) : moreCredent cr a φ ψ ↔ ∃ (θ : ℚ), meetsThreshold cr θ a φ ∧ ¬meetsThreshold cr θ a ψ

Klein'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, originally due to @cite{klein-1980}'s delineation semantics for adjectives and extended to epistemic vocabulary by treating credence as a measure function.

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

Note: linglib's Theories/Semantics/Gradability/Theory.lean follows @cite{kennedy-2007}'s degree typology (open/closed scales, min/max-standard adjectives), which is downstream of Klein's comparative reduction.

theorem Semantics.Attitudes.EpistemicThreshold.meetsThreshold_iff_not_failsThreshold {E : Type u_1} {W : Type u_2} (cr : AgentCredence E W) (θ : ℚ) (a : E) (φ : W → Bool) : 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) (φ ψ : W → Bool) : 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 → W → Bool) (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 → W → Bool) : 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 → W → Bool) : 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 → W → Bool) : 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 → W → Bool) (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 → W → Bool) (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 → W → Bool) (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). "A believes it might rain" = might(rain)(A) = Pr(A, rain) ≥ θ_might. The belief verb contributes only agent projection; the modal's threshold wins.

This is direct function application — no believesModal wrapper is needed in the substrate. Study files that want to mark "this is the modal-embedding position" should annotate at the call site rather than introduce an identity-function alias.

Conjunction-Closure Side of the CSW Divergence

The headline empirical disagreement between this file and Confidence.lean is conjunction elimination. CSW's confidence ordering admits the conjunction fallacy (Confidence.conjunction_fallacy_compatible). Probabilistic credence rules it out, as the lemmas in this section make precise. The packaged refutation lives in §6 (confidence_not_probabilistic) above.

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) (φ ψ : W → Bool) (θ : ℚ) : (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) (φ : W → Bool) : 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 ℚ.