Gradient Projection in Inference Judgments

@cite{degen-tonhauser-2021} @cite{degen-tonhauser-2022} @cite{tonhauser-beaver-roberts-simons-2018}

Theory-neutral empirical observations about gradient patterns in presupposition projection and inference judgments.

Core Observations

1. Projection is gradient across predicates. Aggregate inference judgments for clause-embedding predicates vary continuously — there is no categorical gap separating "factive" from "nonfactive" predicates in projection strength.

2. Prior beliefs modulate projection. Higher prior probability of the complement content leads to stronger projection, at both the group level and the individual participant level (@cite{degen-tonhauser-2021}).

3. The gradient pattern is robust. The by-predicate ranking of projection strength replicates across experiments with Spearman's r = .991 (@cite{degen-tonhauser-2021}, Exp 1 vs Tonhauser & Degen 2020).

4. Optionally factive predicates overlap with canonically factive ones. Some "optionally factive" predicates (e.g., inform) project more strongly than some "canonically factive" predicates (e.g., reveal) (@cite{degen-tonhauser-2022}).

Sources of Gradience

Gradience in inference judgments may arise from multiple sources:

• Resolved (type-level) indeterminacy: Different occasions of use resolve an ambiguity differently (lexical ambiguity, structural ambiguity, QUD). This produces gradience at the experiment level but discreteness at the trial level.

• Unresolved (token-level) indeterminacy: Uncertainty persists even after fixing the interpretation — vagueness, world knowledge, task effects, response error. This produces genuine gradience at every level.

Whether gradient projection reflects resolved or unresolved indeterminacy is a theoretical question addressed by study files, not settled by the data alone.

inductive Phenomena.Presupposition.Gradience.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 Phenomena.Presupposition.Gradience.instDecidableEqGradienceSource : DecidableEq GradienceSource

Equations

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

def Phenomena.Presupposition.Gradience.instReprGradienceSource.repr : GradienceSource → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Presupposition.Gradience.instReprGradienceSource : Repr GradienceSource

Equations

• Phenomena.Presupposition.Gradience.instReprGradienceSource = { reprPrec := Phenomena.Presupposition.Gradience.instReprGradienceSource.repr }

@[reducible]

def Phenomena.Presupposition.Gradience.FactivityHypothesis : Type

A specific application of GradienceSource to factivity. The @cite{grove-white-2025} paper frames the choice between the discrete (FDH) and gradient (FGH) hypotheses as 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

• Phenomena.Presupposition.Gradience.FactivityHypothesis = Phenomena.Presupposition.Gradience.GradienceSource

def Phenomena.Presupposition.Gradience.FactivityHypothesis.FDH : FactivityHypothesis

The Fundamental Discreteness Hypothesis (@cite{grove-white-2025}): factivity is a discrete property of an expression on each occasion of use. Observed gradience arises from resolved indeterminacy.

Equations

• Phenomena.Presupposition.Gradience.FactivityHypothesis.FDH = Phenomena.Presupposition.Gradience.GradienceSource.resolved

def Phenomena.Presupposition.Gradience.FactivityHypothesis.FGH : FactivityHypothesis

The Fundamental Gradience Hypothesis (@cite{grove-white-2025}): there is no property distinguishing factive from non-factive occurrences. Gradient distinctions reflect gradient inference contributions.

Equations

• Phenomena.Presupposition.Gradience.FactivityHypothesis.FGH = Phenomena.Presupposition.Gradience.GradienceSource.unresolved

inductive Phenomena.Presupposition.Gradience.ResolvedMechanism : Type

Mechanisms by which resolved indeterminacy may be cashed out. Catalogue from @cite{grove-white-2025} (Sect. 6, p. 10). The FDH 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).

@[implicit_reducible]

instance Phenomena.Presupposition.Gradience.instDecidableEqResolvedMechanism : DecidableEq ResolvedMechanism

Equations

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

@[implicit_reducible]

instance Phenomena.Presupposition.Gradience.instReprResolvedMechanism : Repr ResolvedMechanism

Equations

• Phenomena.Presupposition.Gradience.instReprResolvedMechanism = { reprPrec := Phenomena.Presupposition.Gradience.instReprResolvedMechanism.repr }

def Phenomena.Presupposition.Gradience.instReprResolvedMechanism.repr : ResolvedMechanism → ℕ → Std.Format

Equations

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

inductive Phenomena.Presupposition.Gradience.UnresolvedSource : Type

Subtypes of unresolved indeterminacy.

• vagueness : UnresolvedSource
• worldKnowledge : UnresolvedSource
• responseStrategy : UnresolvedSource
• responseError : UnresolvedSource

@[implicit_reducible]

instance Phenomena.Presupposition.Gradience.instDecidableEqUnresolvedSource : DecidableEq UnresolvedSource

Equations

• Phenomena.Presupposition.Gradience.instDecidableEqUnresolvedSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Gradience.instReprUnresolvedSource.repr : UnresolvedSource → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Presupposition.Gradience.instReprUnresolvedSource : Repr UnresolvedSource

Equations

• Phenomena.Presupposition.Gradience.instReprUnresolvedSource = { reprPrec := Phenomena.Presupposition.Gradience.instReprUnresolvedSource.repr }

structure Phenomena.Presupposition.Gradience.ProjectionProfile : Type

A projection profile records how strongly a predicate's complement projects, separated by prior probability condition.

• highPrior : Float

  Mean certainty rating with higher-probability background fact.

• lowPrior : Float

  Mean certainty rating with lower-probability background fact.

@[implicit_reducible]

instance Phenomena.Presupposition.Gradience.instReprProjectionProfile : Repr ProjectionProfile

Equations

• Phenomena.Presupposition.Gradience.instReprProjectionProfile = { reprPrec := Phenomena.Presupposition.Gradience.instReprProjectionProfile.repr }

def Phenomena.Presupposition.Gradience.instReprProjectionProfile.repr : ProjectionProfile → ℕ → Std.Format

Equations

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

def Phenomena.Presupposition.Gradience.ProjectionProfile.priorEffect (p : ProjectionProfile) : Float

The prior belief effect: higher prior → stronger projection.

Equations

• p.priorEffect = p.highPrior - p.lowPrior

def Phenomena.Presupposition.Gradience.priorBeliefModulatesProjection (profile : ProjectionProfile) : Prop

Prior beliefs modulate projection: the effect is positive for every predicate studied. This is the core finding of @cite{degen-tonhauser-2021}.

Equations

• Phenomena.Presupposition.Gradience.priorBeliefModulatesProjection profile = (profile.highPrior > profile.lowPrior)

structure Phenomena.Presupposition.Gradience.ProjectionVariability : Type

A predicate's projection variability across contexts, collapsing over prior probability. The mean and range characterize how "reliably factive" a predicate is.

• mean : Float

  Mean projection across all contexts.

• bimodal : Bool

  Whether the predicate shows bimodal responses (modes near 0 and 1).

@[implicit_reducible]

instance Phenomena.Presupposition.Gradience.instReprProjectionVariability : Repr ProjectionVariability

Equations

• Phenomena.Presupposition.Gradience.instReprProjectionVariability = { reprPrec := Phenomena.Presupposition.Gradience.instReprProjectionVariability.repr }

def Phenomena.Presupposition.Gradience.instReprProjectionVariability.repr : ProjectionVariability → ℕ → Std.Format

Equations

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

structure Phenomena.Presupposition.Gradience.NoCategoricalGap : Type

The key empirical observation: no categorical gap between traditional classes in projection strength. Formalized as: for any threshold that separates "factive" from "nonfactive" by projection rating, at least one predicate from each traditional class falls on the wrong side.

• optFactivePred : String

  An "optionally factive" predicate that projects more strongly than some "canonically factive" predicate.

• canonFactivePred : String
• optFactiveRating : Float
• canonFactiveRating : Float
• overlap : self.optFactiveRating > self.canonFactiveRating

def Phenomena.Presupposition.Gradience.noCategoricalGap_witness : NoCategoricalGap

Witnessed by inform (0.81) > reveal (0.70) in @cite{degen-tonhauser-2022} Experiment 1a (sliding scale, collapsing over facts).

Equations

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