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.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 Θ

The graded truth value emerges from marginalizing over Θ.

• semantics : Θ → E → Bool
• prior : Core.FinitePMF Θ

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

Graded truth value: P(x) = E_θ[P_θ(x)].

Equations

• pred.gradedTruth x = pred.prior.prob fun (θ : Θ) => pred.semantics θ x

def Semantics.Probabilistic.ParamPred.ParamPred.toGPred {E : Type u_1} {Θ : Type u_2} [Fintype Θ] (pred : ParamPred E Θ) : Core.GradedProposition.GPred E

Convert a parameterized predicate to a graded predicate.

Equations

• pred.toGPred = pred.gradedTruth

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

For a point mass prior (no uncertainty), graded truth = Boolean truth.

theorem Semantics.Probabilistic.ParamPred.ParamPred.gradedTruth_eq_expect {E : Type u_1} {Θ : Type u_2} [Fintype Θ] [DecidableEq Θ] (sem : Θ → E → Bool) (prior : Core.FinitePMF Θ) (x : E) : { semantics := sem, prior := prior }.gradedTruth x = prior.expect fun (θ : Θ) => if sem θ x = true then 1 else 0

Graded truth unfolds to expected value of the Boolean indicator.

def Semantics.Probabilistic.ParamPred.ParamPred.conj {E : Type u_1} {Θ₁ : Type u_2} {Θ₂ : Type u_3} [Fintype Θ₁] [Fintype Θ₂] [DecidableEq Θ₁] [DecidableEq Θ₂] (p : ParamPred E Θ₁) (q : ParamPred E Θ₂) : ParamPred E (Θ₁ × Θ₂)

Compose two parameterized predicates via conjunction.

The result has uncertainty over both parameters (product space). Under independence, the joint prior is the product of individual priors.

Equations

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