Grove and White (2025): Factivity, Presupposition Projection, and Discrete Knowledge

This file formalizes the response models of Grove and White, who ask whether the gradience of projection judgments comes from resolved indeterminacy, factivity being a discrete property of token occurrences, or from unresolved indeterminacy. A model is a distribution over answers in the unit interval to how likely is it that φ?. Factivity is resolved when a reading of the predicate is drawn and the answer computed under it, and unresolved when it enters the probability of the answer. World knowledge is gradient when the answer is the complement's probability and discrete when it is the complement's truth at a drawn index. The four combinations are the models the paper fits to Degen and Tonhauser's projection data; they share their mean answer and differ in spread.

Main definitions

• likely: the probability of a proposition under a distribution over indices.
• update: the common ground conditioned on a reading of the lexical entry (13).
• resolvedFactivity, unresolvedFactivity: the completions of a norming model by factivity.
• discreteFactivity, whollyDiscrete, whollyGradient, discreteWorld: the four models.

Main results

• discreteFactivity_eq_bind_update, whollyDiscrete_eq_bind_update: the resolved models draw a reading of (13) and answer from the common ground updated with it.
• discreteFactivity_eq, whollyDiscrete_eq, whollyGradient_eq, discreteWorld_eq: the models in closed form.
• integral_discreteFactivity and its siblings: the four share the mean answer.
• variance_whollyGradient and its siblings: only the models with a discrete component spread.

Implementation notes

Updating the common ground conditions a prior over Factivity.World on a reading's content, belief and the complement being independent under the prior; under unresolved factivity the factivity value of an index is likewise independent of the complement. The response noise of section 4.1, the truncated normal likelihood, is not modeled, so each model is the distribution of the intended answer. The paper's illustrative sentences are rows of GroveWhite2025.Examples.

References

• [GW25a]
• [DT21]

Likelihood

noncomputable def GroveWhite2025.likely {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] (s : Set Ω) : ↑unitInterval

likely μ s is the probability of the proposition s under the distribution μ over indices, as a point of the unit interval.

Equations

• GroveWhite2025.likely μ s = ⟨μ.real s, ⋯⟩

@[simp]

theorem GroveWhite2025.coe_likely {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsZeroOrProbabilityMeasure μ] (s : Set Ω) : ↑(likely μ s) = μ.real s

The lexical entry (13)

inductive GroveWhite2025.FactivityReading : Type

A clause-embedding predicate has two readings in (13).

• factive : FactivityReading

  The reading m, which triggers the projective inference.

• nonfactive : FactivityReading

  The reading n, which does not.

@[instance_reducible]

instance GroveWhite2025.instDecidableEqFactivityReading : DecidableEq FactivityReading

Equations

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

@[instance_reducible]

instance GroveWhite2025.instMeasurableSpaceFactivityReading : MeasurableSpace FactivityReading

Equations

• GroveWhite2025.instMeasurableSpaceFactivityReading = ⊤

instance GroveWhite2025.instDiscreteMeasurableSpaceFactivityReading : DiscreteMeasurableSpace FactivityReading

def GroveWhite2025.clauseEmbeddingSem : FactivityReading → Factivity.World → Prop

The content of know under its factive reading is Factivity.World.Knows, belief together with the complement, and under its non-factive reading Factivity.World.Thinks, belief alone.

Equations

• GroveWhite2025.clauseEmbeddingSem GroveWhite2025.FactivityReading.factive = Factivity.World.Knows
• GroveWhite2025.clauseEmbeddingSem GroveWhite2025.FactivityReading.nonfactive = Factivity.World.Thinks

noncomputable def GroveWhite2025.commonGround (b p : ↑unitInterval) : MeasureTheory.Measure Factivity.World

The common ground is a prior over worlds under which belief and the complement are independent, with probabilities b and p.

Equations

• GroveWhite2025.commonGround b p = (ProbabilityTheory.bernoulliMeasure true false b).prod (ProbabilityTheory.bernoulliMeasure true false p)

instance GroveWhite2025.instIsProbabilityMeasureWorldCommonGround (b p : ↑unitInterval) : MeasureTheory.IsProbabilityMeasure (commonGround b p)

noncomputable def GroveWhite2025.update (b p : ↑unitInterval) (r : FactivityReading) : MeasureTheory.Measure Factivity.World

Updating the common ground with a reading conditions it on the reading's content.

Equations

• GroveWhite2025.update b p r = (GroveWhite2025.commonGround b p)[|{w : Factivity.World | GroveWhite2025.clauseEmbeddingSem r w}]

instance GroveWhite2025.instIsZeroOrProbabilityMeasureWorldUpdate (b p : ↑unitInterval) (r : FactivityReading) : MeasureTheory.IsZeroOrProbabilityMeasure (update b p r)

theorem GroveWhite2025.update_factive {b p : ↑unitInterval} (hb : b ≠ 0) (hp : p ≠ 0) : update b p FactivityReading.factive = MeasureTheory.Measure.dirac (true, true)

Under the factive reading the updated common ground is the world where the complement is believed and true.

theorem GroveWhite2025.update_nonfactive {b p : ↑unitInterval} (hb : b ≠ 0) : update b p FactivityReading.nonfactive = (MeasureTheory.Measure.dirac true).prod (ProbabilityTheory.bernoulliMeasure true false p)

Under the non-factive reading the updated common ground fixes belief and keeps the prior on the complement.

theorem GroveWhite2025.likely_update_factive {b p : ↑unitInterval} (hb : b ≠ 0) (hp : p ≠ 0) : likely (update b p FactivityReading.factive) {w : Factivity.World | w.complement = true} = 1

Know entails its complement, so the complement is certain under the factive reading.

theorem GroveWhite2025.likely_update_nonfactive {b p : ↑unitInterval} (hb : b ≠ 0) : likely (update b p FactivityReading.nonfactive) {w : Factivity.World | w.complement = true} = p

Belief is independent of the complement, so the complement keeps its prior under the non-factive reading.

Norming models, section 4.2

@[reducible, inline]

noncomputable abbrev GroveWhite2025.normingGradient (p : ↑unitInterval) : MeasureTheory.Measure ↑unitInterval

World knowledge as unresolved indeterminacy answers with the complement's probability p under the common ground.

Equations

• GroveWhite2025.normingGradient p = MeasureTheory.Measure.dirac p

@[reducible, inline]

noncomputable abbrev GroveWhite2025.normingDiscrete (p : ↑unitInterval) : MeasureTheory.Measure ↑unitInterval

World knowledge as resolved indeterminacy answers with the complement's truth at an index drawn from the common ground, true with probability p.

Equations

• GroveWhite2025.normingDiscrete p = ProbabilityTheory.bernoulliMeasure 1 0 p

Completing a norming model by factivity, section 4.3

noncomputable def GroveWhite2025.resolvedFactivity (τ : ↑unitInterval) (ν : MeasureTheory.Measure ↑unitInterval) : MeasureTheory.Measure ↑unitInterval

Resolved factivity draws a reading of (13), the factive one with probability τ, and answers 1 under it and as the norming model ν does otherwise.

Equations

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

noncomputable def GroveWhite2025.disjunction (τ d : ↑unitInterval) : ↑unitInterval

disjunction τ d is the probability that an index is factive or the complement true there, the two independent with probabilities τ and d.

Equations

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

theorem GroveWhite2025.disjunction_eq (τ d : ↑unitInterval) : disjunction τ d = unitInterval.symm (unitInterval.symm τ * unitInterval.symm d)

theorem GroveWhite2025.measurable_disjunction (τ : ↑unitInterval) : Measurable (disjunction τ)

noncomputable def GroveWhite2025.unresolvedFactivity (τ : ↑unitInterval) (ν : MeasureTheory.Measure ↑unitInterval) : MeasureTheory.Measure ↑unitInterval

Unresolved factivity, the lexical entry (14), answers with the probability that the index is factive or the complement true there, given the norming model's answer.

Equations

• GroveWhite2025.unresolvedFactivity τ ν = MeasureTheory.Measure.map (GroveWhite2025.disjunction τ) ν

@[reducible, inline]

noncomputable abbrev GroveWhite2025.discreteFactivity (τ p : ↑unitInterval) : MeasureTheory.Measure ↑unitInterval

Discrete factivity with gradient world knowledge is the model of section 4.3.1.

Equations

• GroveWhite2025.discreteFactivity τ p = GroveWhite2025.resolvedFactivity τ (GroveWhite2025.normingGradient p)

@[reducible, inline]

noncomputable abbrev GroveWhite2025.whollyDiscrete (τ p : ↑unitInterval) : MeasureTheory.Measure ↑unitInterval

Discrete factivity with discrete world knowledge is the other model of section 4.3.1.

Equations

• GroveWhite2025.whollyDiscrete τ p = GroveWhite2025.resolvedFactivity τ (GroveWhite2025.normingDiscrete p)

@[reducible, inline]

noncomputable abbrev GroveWhite2025.whollyGradient (τ p : ↑unitInterval) : MeasureTheory.Measure ↑unitInterval

Gradient factivity with gradient world knowledge is the model of section 4.3.2.

Equations

• GroveWhite2025.whollyGradient τ p = GroveWhite2025.unresolvedFactivity τ (GroveWhite2025.normingGradient p)

@[reducible, inline]

noncomputable abbrev GroveWhite2025.discreteWorld (τ p : ↑unitInterval) : MeasureTheory.Measure ↑unitInterval

Gradient factivity with discrete world knowledge is the other model of section 4.3.2.

Equations

• GroveWhite2025.discreteWorld τ p = GroveWhite2025.unresolvedFactivity τ (GroveWhite2025.normingDiscrete p)

theorem GroveWhite2025.resolvedFactivity_eq (τ : ↑unitInterval) (ν : MeasureTheory.Measure ↑unitInterval) : resolvedFactivity τ ν = unitInterval.toNNReal τ • MeasureTheory.Measure.dirac 1 + unitInterval.toNNReal (unitInterval.symm τ) • ν

Resolved factivity is a mixture of the endpoint 1, with weight τ, and the norming model.

theorem GroveWhite2025.unresolvedFactivity_eq (τ : ↑unitInterval) (ν : MeasureTheory.Measure ↑unitInterval) : unresolvedFactivity τ ν = MeasureTheory.Measure.map (fun (d : ↑unitInterval) => unitInterval.symm (unitInterval.symm τ * unitInterval.symm d)) ν

instance GroveWhite2025.instIsProbabilityMeasureElemRealUnitIntervalResolvedFactivity (τ : ↑unitInterval) (ν : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsProbabilityMeasure ν] : MeasureTheory.IsProbabilityMeasure (resolvedFactivity τ ν)

instance GroveWhite2025.instIsProbabilityMeasureElemRealUnitIntervalUnresolvedFactivity (τ : ↑unitInterval) (ν : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsProbabilityMeasure ν] : MeasureTheory.IsProbabilityMeasure (unresolvedFactivity τ ν)

@[simp]

theorem GroveWhite2025.resolvedFactivity_zero (ν : MeasureTheory.Measure ↑unitInterval) : resolvedFactivity 0 ν = ν

At τ = 0 each completion is the norming model it completes, and at τ = 1 every model answers 1.

@[simp]

theorem GroveWhite2025.resolvedFactivity_one (ν : MeasureTheory.Measure ↑unitInterval) : resolvedFactivity 1 ν = MeasureTheory.Measure.dirac 1

@[simp]

theorem GroveWhite2025.unresolvedFactivity_zero (ν : MeasureTheory.Measure ↑unitInterval) : unresolvedFactivity 0 ν = ν

@[simp]

theorem GroveWhite2025.unresolvedFactivity_one (ν : MeasureTheory.Measure ↑unitInterval) [MeasureTheory.IsProbabilityMeasure ν] : unresolvedFactivity 1 ν = MeasureTheory.Measure.dirac 1

The resolved models from the lexical entry

def GroveWhite2025.complementValue (w : Factivity.World) : ↑unitInterval

The answer at an index under discrete world knowledge is the complement's truth value.

Equations

• GroveWhite2025.complementValue w = bif w.complement then 1 else 0

theorem GroveWhite2025.discreteFactivity_eq_bind_update (τ : ↑unitInterval) {b p : ↑unitInterval} (hb : b ≠ 0) (hp : p ≠ 0) : discreteFactivity τ p = (ProbabilityTheory.bernoulliMeasure FactivityReading.factive FactivityReading.nonfactive τ).bind fun (r : FactivityReading) => MeasureTheory.Measure.dirac (likely (update b p r) {w : Factivity.World | w.complement = true})

The discrete-factivity model draws a reading of (13) and answers with the probability of the complement under the common ground updated with it.

theorem GroveWhite2025.whollyDiscrete_eq_bind_update (τ : ↑unitInterval) {b p : ↑unitInterval} (hb : b ≠ 0) (hp : p ≠ 0) : whollyDiscrete τ p = (ProbabilityTheory.bernoulliMeasure FactivityReading.factive FactivityReading.nonfactive τ).bind fun (r : FactivityReading) => MeasureTheory.Measure.map complementValue (update b p r)

The wholly-discrete model draws a reading of (13) and answers with the complement's truth at an index drawn from the common ground updated with it.

The four models in closed form

theorem GroveWhite2025.discreteFactivity_eq (τ p : ↑unitInterval) : discreteFactivity τ p = ProbabilityTheory.bernoulliMeasure 1 p τ

theorem GroveWhite2025.whollyDiscrete_eq (τ p : ↑unitInterval) : whollyDiscrete τ p = ProbabilityTheory.bernoulliMeasure 1 0 (unitInterval.symm (unitInterval.symm τ * unitInterval.symm p))

theorem GroveWhite2025.whollyGradient_eq (τ p : ↑unitInterval) : whollyGradient τ p = MeasureTheory.Measure.dirac (unitInterval.symm (unitInterval.symm τ * unitInterval.symm p))

theorem GroveWhite2025.discreteWorld_eq (τ p : ↑unitInterval) : discreteWorld τ p = ProbabilityTheory.bernoulliMeasure 1 τ p

Mean answer

The four models share the mean τ + (1 - τ) * p.

theorem GroveWhite2025.integral_discreteFactivity (τ p : ↑unitInterval) : ∫ (d : ↑unitInterval), ↑d ∂discreteFactivity τ p = ↑τ + (1 - ↑τ) * ↑p

theorem GroveWhite2025.integral_whollyDiscrete (τ p : ↑unitInterval) : ∫ (d : ↑unitInterval), ↑d ∂whollyDiscrete τ p = ↑τ + (1 - ↑τ) * ↑p

theorem GroveWhite2025.integral_whollyGradient (τ p : ↑unitInterval) : ∫ (d : ↑unitInterval), ↑d ∂whollyGradient τ p = ↑τ + (1 - ↑τ) * ↑p

theorem GroveWhite2025.integral_discreteWorld (τ p : ↑unitInterval) : ∫ (d : ↑unitInterval), ↑d ∂discreteWorld τ p = ↑τ + (1 - ↑τ) * ↑p

Spread of the answer

The wholly gradient model is a single degenerate distribution; the models with a discrete component are mixtures with a component at the endpoint 1, the shape that section 4.4 credits with capturing the dips in the middle of the scale.

theorem GroveWhite2025.variance_discreteFactivity (τ p : ↑unitInterval) : ProbabilityTheory.variance (fun (d : ↑unitInterval) => ↑d) (discreteFactivity τ p) = ↑τ * (1 - ↑τ) * (1 - ↑p) ^ 2

theorem GroveWhite2025.variance_whollyDiscrete (τ p : ↑unitInterval) : ProbabilityTheory.variance (fun (d : ↑unitInterval) => ↑d) (whollyDiscrete τ p) = (↑τ + (1 - ↑τ) * ↑p) * (1 - ↑τ) * (1 - ↑p)

theorem GroveWhite2025.variance_whollyGradient (τ p : ↑unitInterval) : ProbabilityTheory.variance (fun (d : ↑unitInterval) => ↑d) (whollyGradient τ p) = 0

theorem GroveWhite2025.variance_discreteWorld (τ p : ↑unitInterval) : ProbabilityTheory.variance (fun (d : ↑unitInterval) => ↑d) (discreteWorld τ p) = ↑p * (1 - ↑p) * (1 - ↑τ) ^ 2