Parameterized Predicates

@cite{lassiter-goodman-2017} @cite{grove-white-2025}

Boolean predicates parameterized by a latent variable, with a prior over that variable. Graded truth values emerge from marginalizing over the parameter: P(x) = E_θ[P_θ(x)].

This pattern applies whenever gradience arises from uncertainty over a discrete parameter:

• Gradable adjectives: θ = threshold, ⟦tall⟧_θ(x) = height(x) > θ
• Factivity: θ ∈ {factive, nonfactive}, ⟦know⟧_factive = BEL ∧ C
• Generics: θ = prevalence threshold
• Polysemy: θ indexes word senses

The key theorem gradedTruth_pure shows that a point-mass prior (no uncertainty) recovers Boolean truth — gradience is not stipulated but emerges from parameter uncertainty.

structure Semantics.Probabilistic.ParamPred (E : Type u_1) (Θ : Type u_2) [Fintype Θ] : Type (max u_1 u_2)

A parameterized predicate has:

• A parameter space Θ
• For each θ, a Boolean predicate on entities
• A prior distribution over Θ (mathlib PMF, ℝ≥0∞-valued)

The graded truth value emerges from marginalizing over Θ.

• semantics : Θ → E → Bool
• prior : PMF Θ

noncomputable def Semantics.Probabilistic.ParamPred.gradedTruth {E : Type u_1} {Θ : Type u_2} [Fintype Θ] (pred : ParamPred E Θ) (x : E) : ENNReal

Graded truth value: P(x) = prior {θ | semantics θ x}. The prior's mass on the set of parameter values where the Boolean predicate holds.

Equations

• pred.gradedTruth x = pred.prior.probOfSet {θ : Θ | pred.semantics θ x = true}

theorem Semantics.Probabilistic.ParamPred.gradedTruth_pure {E : Type u_1} {Θ : Type u_2} [Fintype Θ] (sem : Θ → E → Bool) (θ₀ : Θ) (x : E) : { semantics := sem, prior := PMF.pure θ₀ }.gradedTruth x = if sem θ₀ x = true then 1 else 0

For a point-mass prior (no uncertainty), graded truth = Boolean truth. The substantive theorem: gradience emerges from parameter uncertainty, not from the predicate itself.