Documentation

Linglib.Phenomena.Presupposition.Studies.GroveWhite2025

@cite{grove-white-2025} #

Factivity, presupposition projection, and the role of discrete knowledge in gradient inference judgments. Natural Language Semantics 34:1–45.

Core Contribution #

Grove & White compare two hypotheses about the gradience observed in inference judgments for clause-embedding predicates:

Fundamental Discreteness Hypothesis (FDH) (definition (7a), p. 10): Factivity is a discrete property of an expression on a particular occasion of use. A given use either triggers a projective inference, or it does not. Observed gradience arises from resolved indeterminacy — variation across occasions in which reading is selected.
Fundamental Gradience Hypothesis (FGH) (definition (7b), p. 10): There is no property distinguishing factive from non-factive occurrences. Gradient distinctions observed among predicates reflect gradient contributions to inferences about their complement clauses.

The Four Models #

The paper crosses two binary choices — factivity (discrete/gradient) × world knowledge (discrete/gradient) — yielding four models:

Model	Factivity	World knowledge	Fits best?
discrete-factivity	discrete (τ_v)	gradient	Yes
wholly-discrete	discrete (τ_v)	discrete	Second
discrete-world	gradient	discrete
wholly-gradient	gradient	gradient	Worst

The discrete-factivity model extends the norming-gradient model (Sect. 4.2) by adding a Bernoulli switch τ_v on top of the gradient world knowledge model. The wholly-discrete model similarly extends the norming-discrete model.

Formalization Strategy #

The discrete-factivity model is structurally a ParamPred over FactivityReading:

semantics .factive = factivePos (BEL ∧ C)
semantics .nonfactive = nonFactivePos (BEL)
prior = ⟨τ_v, 1 − τ_v⟩

This directly reuses Factivity.lean for the two readings and ParamPred for the parameterized semantics.

Connection to PDS #

The paper's formal framework is Probabilistic Dynamic Semantics (PDS), developed in @cite{grove-white-2025b}. The discreteFactivityPred construction is structurally equivalent to applying PDS's probProp to a Boolean predicate parameterized by reading type — graded truth emerges from marginalizing over a discrete parameter, exactly as in Semantics.Dynamic.Probabilistic.

Connection to @cite{scontras-tonhauser-2025} #

Scontras & Tonhauser's RSA model uses factivePos for know and nonFactivePos for think — exactly the two readings of clauseEmbeddingSem. Their model is the special case of the discrete-factivity model with τ=1 (know is always factive) and τ=0 (think is never factive). The bridge theorems certain_factive_eq_know and certain_nonfactive_eq_think make this connection explicit.

Key Results #

Across all four datasets — @cite{degen-tonhauser-2021} original, a replication, bleached contexts, and templatic contexts — the discrete-factivity model achieves the best ELPD (expected log pointwise predictive density), supporting the FDH over the FGH.

def Phenomena.Presupposition.Studies.GroveWhite2025.FDH :

Gradience.GradienceSource

The Fundamental Discreteness Hypothesis (definition (7a), p. 10): factivity is a discrete property of an expression on a particular occasion of use. A given use either triggers a projective inference, or it does not. The FDH is neutral on why the resolved indeterminacy arises — it may be due to polysemy, structural ambiguity, or discourse sensitivity (QUD/common ground).

Equations

Phenomena.Presupposition.Studies.GroveWhite2025.FDH = Phenomena.Presupposition.Gradience.GradienceSource.resolved

Instances For

def Phenomena.Presupposition.Studies.GroveWhite2025.FGH :

Gradience.GradienceSource

The Fundamental Gradience Hypothesis (definition (7b), p. 10): there is no property distinguishing factive from non-factive occurrences. Gradient distinctions reflect gradient contributions to inferences.

Equations

Phenomena.Presupposition.Studies.GroveWhite2025.FGH = Phenomena.Presupposition.Gradience.GradienceSource.unresolved

Instances For

inductive Phenomena.Presupposition.Studies.GroveWhite2025.ResolvedMechanism :

Possible mechanisms for resolved indeterminacy under the FDH. These are mentioned on p. 10 as different ways the discreteness could be cashed out. The FDH itself is neutral among them.

polysemy : ResolvedMechanism
Polysemy: a predicate has multiple senses, at least one factive and at least one nonfactive (conventionalist account, Sect. 6.1).
structuralAmbiguity : ResolvedMechanism
Structural ambiguity: a predicate occurs in multiple structures, at least one implicated in triggering projection and one not.
discourseSensitivity : ResolvedMechanism
Discourse sensitivity: the predicate's complement content may or may not be entailed by a discourse construct like the QUD (conversationalist account, Sect. 6.2).

Instances For

instance Phenomena.Presupposition.Studies.GroveWhite2025.instDecidableEqResolvedMechanism :

DecidableEq ResolvedMechanism

Equations

Phenomena.Presupposition.Studies.GroveWhite2025.instDecidableEqResolvedMechanism x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.GroveWhite2025.instReprResolvedMechanism.repr :

ResolvedMechanism → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Presupposition.Studies.GroveWhite2025.instReprResolvedMechanism :

Repr ResolvedMechanism

Equations

Phenomena.Presupposition.Studies.GroveWhite2025.instReprResolvedMechanism = { reprPrec := Phenomena.Presupposition.Studies.GroveWhite2025.instReprResolvedMechanism.repr }

structure Phenomena.Presupposition.Studies.GroveWhite2025.FactivityParam :

Per-predicate factivity probability. On each occasion of use, a clause- embedding predicate is factive with probability τ_v and nonfactive with probability 1 − τ_v. This is the key parameter of the discrete-factivity model (Sect. 3.7, definition (13)).

τ : ℚ
The probability of the factive reading.
τ_nonneg : 0 ≤ self.τ
τ_le_one : self.τ ≤ 1

Instances For

inductive Phenomena.Presupposition.Studies.GroveWhite2025.FactivityReading :

The two readings of a clause-embedding predicate under the FDH.

factive : FactivityReading
The factive reading: BEL ∧ C.
nonfactive : FactivityReading
The nonfactive reading: BEL only.

Instances For

instance Phenomena.Presupposition.Studies.GroveWhite2025.instDecidableEqFactivityReading :

DecidableEq FactivityReading

Equations

Phenomena.Presupposition.Studies.GroveWhite2025.instDecidableEqFactivityReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.GroveWhite2025.instReprFactivityReading.repr :

FactivityReading → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Presupposition.Studies.GroveWhite2025.instReprFactivityReading :

Repr FactivityReading

Equations

Phenomena.Presupposition.Studies.GroveWhite2025.instReprFactivityReading = { reprPrec := Phenomena.Presupposition.Studies.GroveWhite2025.instReprFactivityReading.repr }

def Phenomena.Presupposition.Studies.GroveWhite2025.instBEqFactivityReading.beq :

FactivityReading → FactivityReading → Bool

Equations

Phenomena.Presupposition.Studies.GroveWhite2025.instBEqFactivityReading.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Presupposition.Studies.GroveWhite2025.instBEqFactivityReading :

BEq FactivityReading

Equations

Phenomena.Presupposition.Studies.GroveWhite2025.instBEqFactivityReading = { beq := Phenomena.Presupposition.Studies.GroveWhite2025.instBEqFactivityReading.beq }

instance Phenomena.Presupposition.Studies.GroveWhite2025.instInhabitedFactivityReading :

Inhabited FactivityReading

Equations

Phenomena.Presupposition.Studies.GroveWhite2025.instInhabitedFactivityReading = { default := Phenomena.Presupposition.Studies.GroveWhite2025.instInhabitedFactivityReading.default }

def Phenomena.Presupposition.Studies.GroveWhite2025.instInhabitedFactivityReading.default :

FactivityReading

Equations

Phenomena.Presupposition.Studies.GroveWhite2025.instInhabitedFactivityReading.default = Phenomena.Presupposition.Studies.GroveWhite2025.FactivityReading.factive

Instances For

instance Phenomena.Presupposition.Studies.GroveWhite2025.instFintypeFactivityReading :

Fintype FactivityReading

Equations

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

def Phenomena.Presupposition.Studies.GroveWhite2025.clauseEmbeddingSem {W : Type u_1} [Semantics.Attitudes.Factivity.HasBelief W] [Semantics.Attitudes.Factivity.HasComplement W] :

FactivityReading → W → Bool

The two Boolean readings of a clause-embedding predicate, derived directly from Factivity.lean. Under reading factive, the predicate has semantics BEL ∧ C (factivePos); under nonfactive, just BEL (nonFactivePos). This corresponds to the paper's DAG in (13), p. 20.

Equations

Instances For

theorem Phenomena.Presupposition.Studies.GroveWhite2025.factive_entails_nonfactive_reading {W : Type u_1} [Semantics.Attitudes.Factivity.HasBelief W] [Semantics.Attitudes.Factivity.HasComplement W] (w : W) :

clauseEmbeddingSem FactivityReading.factive w = true → clauseEmbeddingSem FactivityReading.nonfactive w = true

The factive reading entails the nonfactive reading.

def Phenomena.Presupposition.Studies.GroveWhite2025.discreteFactivityPred {W : Type u_1} [Semantics.Attitudes.Factivity.HasBelief W] [Semantics.Attitudes.Factivity.HasComplement W] (fp : FactivityParam) :

Semantics.Probabilistic.ParamPred.ParamPred W FactivityReading

Construct a ParamPred for a clause-embedding predicate from its factivity parameter τ_v. This is the discrete-factivity model: Boolean semantics parameterized by a binary reading, with a prior ⟨τ_v, 1 − τ_v⟩ over readings.

Equations

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

Instances For

theorem Phenomena.Presupposition.Studies.GroveWhite2025.discreteFactivity_gradedTruth {W : Type u_1} [Semantics.Attitudes.Factivity.HasBelief W] [Semantics.Attitudes.Factivity.HasComplement W] (fp : FactivityParam) (w : W) :

(discreteFactivityPred fp).gradedTruth w = (fp.τ * if Semantics.Attitudes.Factivity.factivePos w = true then 1 else 0) + (1 - fp.τ) * if Semantics.Attitudes.Factivity.nonFactivePos w = true then 1 else 0

The graded truth value of a clause-embedding predicate under the discrete-factivity model equals the τ-weighted mixture of the two Boolean readings.

theorem Phenomena.Presupposition.Studies.GroveWhite2025.discreteFactivity_eq_probProp {W : Type u_1} [Semantics.Attitudes.Factivity.HasBelief W] [Semantics.Attitudes.Factivity.HasComplement W] [Fintype W] (fp : FactivityParam) (w : W) :

(discreteFactivityPred fp).gradedTruth w = Semantics.Dynamic.Probabilistic.probProp (discreteFactivityPred fp).prior.mass fun (r : FactivityReading) => clauseEmbeddingSem r w

The discrete-factivity model's graded truth is exactly PDS's probProp: the probability of a Boolean predicate under a finite distribution. This is the formal content of the paper's core claim — graded inference judgments emerge from marginalizing over a discrete reading parameter.

theorem Phenomena.Presupposition.Studies.GroveWhite2025.discreteFactivity_certain_factive {W : Type u_1} [Semantics.Attitudes.Factivity.HasBelief W] [Semantics.Attitudes.Factivity.HasComplement W] (w : W) :

(discreteFactivityPred { τ := 1, τ_nonneg := ⋯, τ_le_one := ⋯ }).gradedTruth w = if Semantics.Attitudes.Factivity.factivePos w = true then 1 else 0

With τ = 1 (certainly factive), graded truth reduces to factivePos.

theorem Phenomena.Presupposition.Studies.GroveWhite2025.discreteFactivity_certain_nonfactive {W : Type u_1} [Semantics.Attitudes.Factivity.HasBelief W] [Semantics.Attitudes.Factivity.HasComplement W] (w : W) :

(discreteFactivityPred { τ := 0, τ_nonneg := ⋯, τ_le_one := ⋯ }).gradedTruth w = if Semantics.Attitudes.Factivity.nonFactivePos w = true then 1 else 0

With τ = 0 (certainly nonfactive), graded truth reduces to nonFactivePos.

inductive Phenomena.Presupposition.Studies.GroveWhite2025.ModelVariant :

The four models from the paper (Sect. 4.3–4.4), crossing factivity × world knowledge. Each model is a completion of one of the two norming models (Sect. 4.2) with a factivity component.

discreteFactivity : ModelVariant
Discrete factivity + gradient world knowledge. Best fit. Extends norming-gradient (Sect. 4.2.1).
whollyDiscrete : ModelVariant
Discrete factivity + discrete world knowledge. Extends norming-discrete (Sect. 4.2.2).
whollyGradient : ModelVariant
Gradient factivity + gradient world knowledge. Worst fit. Extends norming-gradient with gradient factivity.
discreteWorld : ModelVariant
Gradient factivity + discrete world knowledge. Extends norming-discrete with gradient factivity.

Instances For

instance Phenomena.Presupposition.Studies.GroveWhite2025.instDecidableEqModelVariant :

DecidableEq ModelVariant

Equations

Phenomena.Presupposition.Studies.GroveWhite2025.instDecidableEqModelVariant x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.GroveWhite2025.instReprModelVariant.repr :

ModelVariant → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Presupposition.Studies.GroveWhite2025.instReprModelVariant :

Repr ModelVariant

Equations

Phenomena.Presupposition.Studies.GroveWhite2025.instReprModelVariant = { reprPrec := Phenomena.Presupposition.Studies.GroveWhite2025.instReprModelVariant.repr }

def Phenomena.Presupposition.Studies.GroveWhite2025.ModelVariant.factivityHypothesis :

ModelVariant → Gradience.GradienceSource

Whether a model treats factivity as discrete (FDH) or gradient (FGH).

Equations

Instances For

def Phenomena.Presupposition.Studies.GroveWhite2025.ModelVariant.worldKnowledgeSource :

ModelVariant → Gradience.GradienceSource

Whether a model treats world knowledge as gradient (unresolved) or discrete (resolved).

Equations

Instances For

theorem Phenomena.Presupposition.Studies.GroveWhite2025.best_worst_share_world_knowledge :

ModelVariant.discreteFactivity.worldKnowledgeSource = ModelVariant.whollyGradient.worldKnowledgeSource ∧ ModelVariant.discreteFactivity.factivityHypothesis ≠ ModelVariant.whollyGradient.factivityHypothesis

The best and worst models both use gradient world knowledge but differ in factivity treatment. This isolates discrete factivity as the key factor driving model fit: holding world knowledge constant at gradient, switching from discrete to gradient factivity drops ELPD from best to worst.

inductive Phenomena.Presupposition.Studies.GroveWhite2025.NormingModel :

Each factivity model extends one of two norming models. The extension relationship is determined by how the model treats world knowledge: gradient world knowledge = extends norming-gradient, discrete world knowledge = extends norming-discrete.

gradient : NormingModel
Norming-gradient (Sect. 4.2.1): world knowledge as unresolved.
discrete : NormingModel
Norming-discrete (Sect. 4.2.2): world knowledge as resolved.

Instances For

instance Phenomena.Presupposition.Studies.GroveWhite2025.instDecidableEqNormingModel :

DecidableEq NormingModel

Equations

Phenomena.Presupposition.Studies.GroveWhite2025.instDecidableEqNormingModel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.GroveWhite2025.instReprNormingModel.repr :

NormingModel → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Presupposition.Studies.GroveWhite2025.instReprNormingModel :

Repr NormingModel

Equations

Phenomena.Presupposition.Studies.GroveWhite2025.instReprNormingModel = { reprPrec := Phenomena.Presupposition.Studies.GroveWhite2025.instReprNormingModel.repr }

def Phenomena.Presupposition.Studies.GroveWhite2025.ModelVariant.baseNormingModel :

ModelVariant → NormingModel

Each factivity model extends one of the two norming models.

Equations

Instances For

theorem Phenomena.Presupposition.Studies.GroveWhite2025.certain_factive_eq_know {W : Type u_1} [Semantics.Attitudes.Factivity.HasBelief W] [Semantics.Attitudes.Factivity.HasComplement W] (w : W) :

clauseEmbeddingSem FactivityReading.factive w = Semantics.Attitudes.Factivity.factivePos w

@cite{scontras-tonhauser-2025}'s literalMeaning .knowPos is exactly the factive reading of clauseEmbeddingSem. Their model implicitly sets τ = 1 for know.

theorem Phenomena.Presupposition.Studies.GroveWhite2025.certain_nonfactive_eq_think {W : Type u_1} [Semantics.Attitudes.Factivity.HasBelief W] [Semantics.Attitudes.Factivity.HasComplement W] (w : W) :

clauseEmbeddingSem FactivityReading.nonfactive w = Semantics.Attitudes.Factivity.nonFactivePos w

@cite{scontras-tonhauser-2025}'s literalMeaning .thinkPos is exactly the nonfactive reading of clauseEmbeddingSem. Their model implicitly sets τ = 0 for think.

theorem Phenomena.Presupposition.Studies.GroveWhite2025.st_is_limiting_case {W : Type u_1} [Semantics.Attitudes.Factivity.HasBelief W] [Semantics.Attitudes.Factivity.HasComplement W] :

(∀ (w : W), (discreteFactivityPred { τ := 1, τ_nonneg := ⋯, τ_le_one := ⋯ }).gradedTruth w = if Semantics.Attitudes.Factivity.factivePos w = true then 1 else 0) ∧ ∀ (w : W), (discreteFactivityPred { τ := 0, τ_nonneg := ⋯, τ_le_one := ⋯ }).gradedTruth w = if Semantics.Attitudes.Factivity.nonFactivePos w = true then 1 else 0

S&T's binary model is the limiting case of the discrete-factivity model: know uses τ=1 (certain factive), think uses τ=0 (certain nonfactive). The discrete-factivity model generalizes this by allowing intermediate τ values for the same predicate across occasions.

theorem Phenomena.Presupposition.Studies.GroveWhite2025.higher_tau_higher_gradedTruth {W : Type u_1} [Semantics.Attitudes.Factivity.HasBelief W] [Semantics.Attitudes.Factivity.HasComplement W] (fp₁ fp₂ : FactivityParam) (w : W) (h_tau : fp₁.τ > fp₂.τ) (h_factive : Semantics.Attitudes.Factivity.factivePos w = true) (h_nonfactive : Semantics.Attitudes.Factivity.nonFactivePos w = false) :

(discreteFactivityPred fp₁).gradedTruth w > (discreteFactivityPred fp₂).gradedTruth w

The discrete-factivity model's theoretical prediction: higher τ means more projection. This is a monotonicity property — if τ₁ > τ₂ and the factive reading satisfies factivePos w but the nonfactive reading does not satisfy nonFactivePos w, then the predicate with higher τ gets higher graded truth at w.

theorem Phenomena.Presupposition.Studies.GroveWhite2025.empirical_ordering_consistent_with_tau :

DegenTonhauser2022.projectionRating_Exp1a DegenTonhauser2021.Predicate.know > DegenTonhauser2022.projectionRating_Exp1a DegenTonhauser2021.Predicate.think

The empirical ordering from @cite{degen-tonhauser-2022} — know projects more than think — is consistent with the model's τ ordering. Under the discrete-factivity model, this ordering holds when τ_know > τ_think. The S&T limiting case (τ_know=1, τ_think=0) is a special case.

theorem Phenomena.Presupposition.Studies.GroveWhite2025.prior_effect_consistent :

(DegenTonhauser2021.exp1_priorEffect DegenTonhauser2021.PriorLevel.categorical).β > 0 ∧ DegenTonhauser2021.exp2b_priorEffect DegenTonhauser2021.PriorLevel.categorical = some { β := 0.18, se := 1e-2, t := 12.81 }

The prior-belief modulation finding from @cite{degen-tonhauser-2021} is the empirical observation that the discrete-factivity model explains: observed gradience arises from uncertainty over the discrete τ parameter interacting with world knowledge (prior beliefs about complement content). Both experiments confirm that higher prior → stronger projection.