[GW25a]

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 reflect gradient inference contributions.

Both hypotheses are recorded as FactivityHypothesis.FDH and FactivityHypothesis.FGH, exposed as the two GradienceSource values (resolved vs unresolved indeterminacy). The paper's distinctive formal content is the τ-parameterised model and the 2 × 2 model space crossing factivity discreteness with world-knowledge discreteness.

The Discrete-Factivity Model

The discrete-factivity model is a ParamPred over FactivityReading:

• clauseEmbeddingSem .factive = factivePos (BEL ∧ C)
• clauseEmbeddingSem .nonfactive = nonFactivePos (BEL)
• prior over readings: ⟨τ, 1 − τ⟩ for τ : Rat01

The graded truth value of a predicate at a world w then unfolds to τ · 1[BEL∧C] + (1−τ) · 1[BEL] (discreteFactivity_gradedTruth). This is the closed-form reduction of the τ-vertex of the paper's DAG (definition (13), p. 20).

The Four Models

Crossing factivity (discrete/gradient) × world knowledge (discrete/gradient) yields four model variants. The paper reports that the discrete-factivity × gradient-world variant achieves the best ELPD across all four datasets (Sect. 4.3–4.4). The 2 × 2 is captured by ModelVariant, with the discrete-factivity-vs-wholly-gradient pair sharing world-knowledge treatment (best_worst_share_world_knowledge) so that switching factivity hypothesis is the active variable.

Connection to PDS

The paper's formal framework is Probabilistic Dynamic Semantics (PDS), developed in [GW25b]. The model's graded truth is the PMF.probOfSet (= toOuterMeasure) of the satisfied-readings event under the Bernoulli prior: graded inference judgments emerge from marginalising over a discrete reading parameter, exactly the PDS pattern in which a bind over a discrete probability node feeds a Boolean predicate.

Connection to [ST25]

[ST25]'s RSA model uses the same factivePos / nonFactivePos foundation from Semantics.Attitudes.Factivity for know / think. The bridges clauseEmbedding_factive_eq_st_know and clauseEmbedding_nonfactive_eq_st_think make this explicit. The S&T binary treatment is the τ → {0, 1} limiting case of the discrete-factivity model (st_is_limiting_case).

Connection to D&T 2021/2022

The empirical anchoring is provided by DegenTonhauser2022's aggregate projection ratings: under the discrete-factivity model with τ_know > τ_think, the model predicts the empirically observed know > think projection ordering (empirical_ordering_consistent_with_tau). The prior-belief modulation finding from [DT21] (replicated in 2b) is the specific empirical regularity the world-knowledge component is fit to.

§1. Clause-embedding semantics

inductive GroveWhite2025.FactivityReading : Type

The two readings of a clause-embedding predicate under the FDH. The factive reading triggers a projective inference (BEL ∧ C); the nonfactive reading does not (BEL).

• factive : FactivityReading
• nonfactive : FactivityReading

@[implicit_reducible]

instance GroveWhite2025.instDecidableEqFactivityReading : DecidableEq FactivityReading

Equations

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

def GroveWhite2025.instReprFactivityReading.repr : FactivityReading → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance GroveWhite2025.instReprFactivityReading : Repr FactivityReading

Equations

• GroveWhite2025.instReprFactivityReading = { reprPrec := GroveWhite2025.instReprFactivityReading.repr }

@[implicit_reducible]

instance GroveWhite2025.instInhabitedFactivityReading : Inhabited FactivityReading

Equations

• GroveWhite2025.instInhabitedFactivityReading = { default := GroveWhite2025.instInhabitedFactivityReading.default }

@[implicit_reducible]

instance GroveWhite2025.instFintypeFactivityReading : Fintype FactivityReading

Equations

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

theorem GroveWhite2025.FactivityReading.sum_univ {α : Type u_1} [AddCommMonoid α] (f : FactivityReading → α) : ∑ x : FactivityReading, f x = f factive + f nonfactive

Sum over FactivityReading.univ reduces to a two-term sum. Used by factivityPrior.mass_sum_one and discreteFactivity_gradedTruth so the Fintype enumeration doesn't reappear inline at every call site.

def GroveWhite2025.clauseEmbeddingSem {W : Type u_1} [Semantics.Attitudes.Factivity.HasBelief W] [Semantics.Attitudes.Factivity.HasComplement W] : FactivityReading → W → Bool

The Boolean denotation of a clause-embedding predicate, parameterized by the resolved reading. The two readings dispatch directly to Semantics.Attitudes.Factivity — factivePos and nonFactivePos — so this study shares its foundations with [ST25]'s know / think denotations.

Equations

• GroveWhite2025.clauseEmbeddingSem GroveWhite2025.FactivityReading.factive = Semantics.Attitudes.Factivity.factivePos
• GroveWhite2025.clauseEmbeddingSem GroveWhite2025.FactivityReading.nonfactive = Semantics.Attitudes.Factivity.nonFactivePos

§2. The τ-parameterised prior

noncomputable def GroveWhite2025.Rat01.toNNReal (τ : Core.Order.Rat01) : NNReal

τ.val : ℚ lifted to ℝ≥0 via the canonical ℝ-coercion. Lives outside the Rat01 namespace because Rat01 is an abbrev for a Subtype, so dot notation on τ : Rat01 resolves through the underlying Subtype rather than the Rat01 namespace.

Equations

• GroveWhite2025.Rat01.toNNReal τ = (↑↑τ).toNNReal

theorem GroveWhite2025.Rat01.toNNReal_le_one (τ : Core.Order.Rat01) : toNNReal τ ≤ 1

theorem GroveWhite2025.Rat01.toNNReal_val (τ : Core.Order.Rat01) : ↑(toNNReal τ) = ↑↑τ

noncomputable def GroveWhite2025.factivityPrior (τ : Core.Order.Rat01) : PMF FactivityReading

The Bernoulli prior over FactivityReading: factive with probability τ.val, nonfactive with probability 1 − τ.val. The τ parameter is bundled as Rat01 (↥(Set.Icc (0:ℚ) 1)), so the [0,1] constraint is intrinsic to the type rather than threaded as side hypotheses. This is the τ-vertex of the discrete-factivity DAG (definition (13), p. 20).

Built from mathlib's PMF.bernoulli (a PMF Bool) by relabeling true ↦ .factive, false ↦ .nonfactive.

Equations

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

@[simp]

theorem GroveWhite2025.factivityPrior_apply_factive (τ : Core.Order.Rat01) : (factivityPrior τ) FactivityReading.factive = ↑(Rat01.toNNReal τ)

@[simp]

theorem GroveWhite2025.factivityPrior_apply_nonfactive (τ : Core.Order.Rat01) : (factivityPrior τ) FactivityReading.nonfactive = ↑(1 - Rat01.toNNReal τ)

§3. The discrete-factivity ParamPred

noncomputable def GroveWhite2025.discreteFactivityPred {W : Type u_1} [Semantics.Attitudes.Factivity.HasBelief W] [Semantics.Attitudes.Factivity.HasComplement W] (τ : Core.Order.Rat01) : Semantics.Probabilistic.ParamPred W FactivityReading

The discrete-factivity model packaged as a ParamPred: Boolean semantics dispatched on FactivityReading, with a Bernoulli prior over that reading. The graded truth value gradedTruth is then the ℝ≥0∞-valued probability mass on the satisfied-readings set — PMF.probOfSet of the "predicate satisfied at this world" event.

Equations

• GroveWhite2025.discreteFactivityPred τ = { semantics := GroveWhite2025.clauseEmbeddingSem, prior := GroveWhite2025.factivityPrior τ }

theorem GroveWhite2025.discreteFactivity_gradedTruth {W : Type u_1} [Semantics.Attitudes.Factivity.HasBelief W] [Semantics.Attitudes.Factivity.HasComplement W] (τ : Core.Order.Rat01) (w : W) : (discreteFactivityPred τ).gradedTruth w = (if Semantics.Attitudes.Factivity.factivePos w = true then ↑(Rat01.toNNReal τ) else 0) + if Semantics.Attitudes.Factivity.nonFactivePos w = true then ↑(1 - Rat01.toNNReal τ) else 0

Closed-form reduction: graded truth = τ · 1[factivePos] + (1−τ) · 1[nonFactivePos]. This is the substantive content of the τ-parameterised model — graded inference values arise from a τ-weighted mixture of two crisp Boolean readings.

theorem GroveWhite2025.discreteFactivity_certain_factive {W : Type u_1} [Semantics.Attitudes.Factivity.HasBelief W] [Semantics.Attitudes.Factivity.HasComplement W] (w : W) : (discreteFactivityPred Core.Order.Rat01.one).gradedTruth w = if Semantics.Attitudes.Factivity.factivePos w = true then 1 else 0

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

theorem GroveWhite2025.discreteFactivity_certain_nonfactive {W : Type u_1} [Semantics.Attitudes.Factivity.HasBelief W] [Semantics.Attitudes.Factivity.HasComplement W] (w : W) : (discreteFactivityPred Core.Order.Rat01.zero).gradedTruth w = if Semantics.Attitudes.Factivity.nonFactivePos w = true then 1 else 0

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

theorem GroveWhite2025.higher_tau_higher_gradedTruth {W : Type u_1} [Semantics.Attitudes.Factivity.HasBelief W] [Semantics.Attitudes.Factivity.HasComplement W] (τ₁ τ₂ : Core.Order.Rat01) (w : W) (h_tau : ↑τ₁ > ↑τ₂) (h_factive : Semantics.Attitudes.Factivity.factivePos w = true) (h_nonfactive : Semantics.Attitudes.Factivity.nonFactivePos w = false) : (discreteFactivityPred τ₁).gradedTruth w > (discreteFactivityPred τ₂).gradedTruth w

Monotonicity in τ: at a world that satisfies the factive reading but not the nonfactive reading, increasing τ strictly increases graded truth. The hypothesis pattern factivePos w ∧ ¬ nonFactivePos w is impossible in standard Boolean semantics (factive_entails_nonfactive rules it out), so this lemma is vacuously achievable; the substantive case is the contrapositive one supplied by discreteFactivity_gradedTruth plus monotonicity of the Bernoulli mixture.

§4. The 2 × 2 model space

inductive GroveWhite2025.GradienceSource : Type

Sources of gradience in inference judgment tasks.

• resolved : GradienceSource

  Resolved on each occasion but varying across occasions (type-level).

• unresolved : GradienceSource

  Persists even after fixing the interpretation (token-level).

@[implicit_reducible]

instance GroveWhite2025.instDecidableEqGradienceSource : DecidableEq GradienceSource

Equations

• GroveWhite2025.instDecidableEqGradienceSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance GroveWhite2025.instReprGradienceSource : Repr GradienceSource

Equations

• GroveWhite2025.instReprGradienceSource = { reprPrec := GroveWhite2025.instReprGradienceSource.repr }

def GroveWhite2025.instReprGradienceSource.repr : GradienceSource → ℕ → Std.Format

Equations

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

@[reducible]

def GroveWhite2025.FactivityHypothesis : Type

The choice between the discrete (FDH) and gradient (FGH) hypotheses is a binary choice of source for the gradient projection observations.

Defined as @[reducible] def rather than abbrev so the unfolding is explicit (mathlib convention).

Equations

• GroveWhite2025.FactivityHypothesis = GroveWhite2025.GradienceSource

def GroveWhite2025.FactivityHypothesis.FDH : FactivityHypothesis

The Fundamental Discreteness Hypothesis (definition (7a), p. 10): factivity is a discrete property of an expression on each occasion of use. Observed gradience arises from resolved indeterminacy.

Equations

• GroveWhite2025.FactivityHypothesis.FDH = GroveWhite2025.GradienceSource.resolved

def GroveWhite2025.FactivityHypothesis.FGH : FactivityHypothesis

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

Equations

• GroveWhite2025.FactivityHypothesis.FGH = GroveWhite2025.GradienceSource.unresolved

inductive GroveWhite2025.ModelVariant : Type

The four model variants from Sect. 4.3–4.4, crossing factivity (discrete/gradient) × world knowledge (discrete/gradient). 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.

• discreteWorld : ModelVariant

  Gradient factivity + discrete world knowledge.

@[implicit_reducible]

instance GroveWhite2025.instDecidableEqModelVariant : DecidableEq ModelVariant

Equations

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

@[implicit_reducible]

instance GroveWhite2025.instReprModelVariant : Repr ModelVariant

Equations

• GroveWhite2025.instReprModelVariant = { reprPrec := GroveWhite2025.instReprModelVariant.repr }

def GroveWhite2025.instReprModelVariant.repr : ModelVariant → ℕ → Std.Format

Equations

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

inductive GroveWhite2025.NormingModel : Type

Two norming-model bases (Sect. 4.2).

• gradient : NormingModel

  Norming-gradient (Sect. 4.2.1): world knowledge as unresolved gradience.

• discrete : NormingModel

  Norming-discrete (Sect. 4.2.2): world knowledge as resolved gradience.

@[implicit_reducible]

instance GroveWhite2025.instDecidableEqNormingModel : DecidableEq NormingModel

Equations

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

@[implicit_reducible]

instance GroveWhite2025.instReprNormingModel : Repr NormingModel

Equations

• GroveWhite2025.instReprNormingModel = { reprPrec := GroveWhite2025.instReprNormingModel.repr }

def GroveWhite2025.instReprNormingModel.repr : NormingModel → ℕ → Std.Format

Equations

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

def GroveWhite2025.ModelVariant.factivityHypothesis : ModelVariant → FactivityHypothesis

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

Equations

• GroveWhite2025.ModelVariant.discreteFactivity.factivityHypothesis = GroveWhite2025.FactivityHypothesis.FDH
• GroveWhite2025.ModelVariant.whollyDiscrete.factivityHypothesis = GroveWhite2025.FactivityHypothesis.FDH
• GroveWhite2025.ModelVariant.whollyGradient.factivityHypothesis = GroveWhite2025.FactivityHypothesis.FGH
• GroveWhite2025.ModelVariant.discreteWorld.factivityHypothesis = GroveWhite2025.FactivityHypothesis.FGH

def GroveWhite2025.ModelVariant.worldKnowledgeSource : ModelVariant → GradienceSource

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

Equations

• GroveWhite2025.ModelVariant.discreteFactivity.worldKnowledgeSource = GroveWhite2025.GradienceSource.unresolved
• GroveWhite2025.ModelVariant.whollyDiscrete.worldKnowledgeSource = GroveWhite2025.GradienceSource.resolved
• GroveWhite2025.ModelVariant.whollyGradient.worldKnowledgeSource = GroveWhite2025.GradienceSource.unresolved
• GroveWhite2025.ModelVariant.discreteWorld.worldKnowledgeSource = GroveWhite2025.GradienceSource.resolved

def GroveWhite2025.ModelVariant.baseNormingModel : ModelVariant → NormingModel

Each factivity model extends one of two norming models. The extension relationship is determined by the world-knowledge treatment.

Equations

• GroveWhite2025.ModelVariant.discreteFactivity.baseNormingModel = GroveWhite2025.NormingModel.gradient
• GroveWhite2025.ModelVariant.whollyDiscrete.baseNormingModel = GroveWhite2025.NormingModel.discrete
• GroveWhite2025.ModelVariant.whollyGradient.baseNormingModel = GroveWhite2025.NormingModel.gradient
• GroveWhite2025.ModelVariant.discreteWorld.baseNormingModel = GroveWhite2025.NormingModel.discrete

theorem GroveWhite2025.best_worst_share_world_knowledge : ModelVariant.discreteFactivity.worldKnowledgeSource = ModelVariant.whollyGradient.worldKnowledgeSource ∧ ModelVariant.discreteFactivity.factivityHypothesis ≠ ModelVariant.whollyGradient.factivityHypothesis

The best and worst models share their world-knowledge treatment but differ in factivity hypothesis. This isolates the discreteness of factivity as the variable explaining the ELPD spread between the two extremes.

§5. Bridge to [ST25]

theorem GroveWhite2025.clauseEmbedding_factive_eq_st_know : clauseEmbeddingSem FactivityReading.factive = ScontrasTonhauser2025.literalMeaning ScontrasTonhauser2025.Utterance.knowPos

The factive reading of clauseEmbeddingSem is the same Boolean predicate as [ST25]'s literalMeaning .knowPos. Both unfold to factivePos from Semantics.Attitudes.Factivity, so the equality is true by construction — a grounding theorem in the sense of CLAUDE.md, witnessing that two paper-specific lexical entries share their foundation.

theorem GroveWhite2025.clauseEmbedding_nonfactive_eq_st_think : clauseEmbeddingSem FactivityReading.nonfactive = ScontrasTonhauser2025.literalMeaning ScontrasTonhauser2025.Utterance.thinkPos

The nonfactive reading is [ST25]'s literalMeaning .thinkPos (both unfold to nonFactivePos).

theorem GroveWhite2025.st_is_limiting_case : (∀ (w : ScontrasTonhauser2025.WorldState), (discreteFactivityPred Core.Order.Rat01.one).gradedTruth w = if ScontrasTonhauser2025.literalMeaning ScontrasTonhauser2025.Utterance.knowPos w = true then 1 else 0) ∧ ∀ (w : ScontrasTonhauser2025.WorldState), (discreteFactivityPred Core.Order.Rat01.zero).gradedTruth w = if ScontrasTonhauser2025.literalMeaning ScontrasTonhauser2025.Utterance.thinkPos w = true then 1 else 0

The S&T binary model is the τ → {0, 1} limiting case of the discrete-factivity model: know corresponds to τ_know = 1 (always factive) and think corresponds to τ_think = 0 (never factive). The Grove–White model generalises by allowing intermediate τ values for the same predicate across occasions of use.

§6. Empirical anchoring (D&T 2021/2022)

theorem GroveWhite2025.empirical_ordering_consistent_with_tau : DegenTonhauser2022.projectionRating_Exp1a DegenTonhauser2021.Predicate.know > DegenTonhauser2022.projectionRating_Exp1a DegenTonhauser2021.Predicate.think

Under the discrete-factivity model with τ_know > τ_think, the model predicts a know > think projection ordering. The empirical ordering from [DT22] (Exp 1a, sliding scale) confirms this direction: aggregate ratings for know exceed those for think. norm_num closes the literal comparison since ratings are ℚ-valued.

theorem GroveWhite2025.prior_effect_consistent {acc : DegenTonhauser2021.PriorAccount} (h : DegenTonhauser2021.PriorSensitive acc) {p q : Core.Order.Rat01} (hpq : p < q) : acc p < acc q

The prior-belief modulation finding from [DT21] (replicated in Exp 2b) is the empirical regularity the world-knowledge component of the discrete-factivity model is fit to: a prior-sensitive (monotone) account predicts that higher prior probability of the complement yields stronger projection (DegenTonhauser2021.sensitive_predicts_modulation), which their data confirm for all 20 predicates.