Grove 2022: Presupposition Projection as a Scope Phenomenon

@cite{grove-2022}

Presupposition projection as a scope phenomenon. Semantics and Pragmatics 15, Article 15: 1–39.

Core Claim

The proviso problem — where @cite{heim-1983}'s satisfaction theory predicts weak conditional presuppositions for sentences that intuitively have unconditional ones — dissolves when presupposition projection is treated as scope-taking. Presupposition triggers have Option-typed denotations and interact with their context via monadic bind, exactly paralleling @cite{charlow-2020}'s treatment of indefinites.

Key Predictions

For "If Theo has a brother, he'll bring his wetsuit":

• Local reading (narrow scope): the trigger "his wetsuit" stays inside the consequent → presupposition is hasBrother → hasWetsuit (conditional)
• Global reading (wide scope): the trigger scopes over the conditional → presupposition is hasWetsuit (unconditional)

The two readings are a genuine scope ambiguity, not a semantic + pragmatic strengthening. The proviso problem does not arise because the unconditional presupposition is semantically available.

Connection to @cite{heim-1992}

For attitude verbs ("Theo believes he lost his wetsuit"), the same scope mechanism predicts:

• Local (de dicto): presupposition is that Theo believes he has a wetsuit
• Global (de re): presupposition is that Theo has a wetsuit

This connects to Heim1992.lean's know/believe asymmetry but derives it from scope rather than from local-context filtering.

Empirical Data

• (1) If Theo has a brother, he'll bring his wetsuit. ↝ Theo has a wetsuit.
• (2) If Theo is a scuba diver, he'll bring his wetsuit. ↝ If Theo is a scuba diver, he has a wetsuit.
• (6) John: I am already in bed. Mary: My parents think I am also in bed. ↝ John is in bed.
• (22) Theo believes he lost his wetsuit. ↝ Theo has a wetsuit / Theo believes he has a wetsuit.

§1 World model

Four worlds varying two properties: whether Theo has a brother, and whether Theo has a (unique) wetsuit.

inductive Grove2022.CWorld : Type

Worlds for the conditional examples.

• broSuit : CWorld
• broNoSuit : CWorld
• noBroSuit : CWorld
• noBro : CWorld

@[implicit_reducible]

instance Grove2022.instDecidableEqCWorld : DecidableEq CWorld

Equations

• Grove2022.instDecidableEqCWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Grove2022.instReprCWorld : Repr CWorld

Equations

• Grove2022.instReprCWorld = { reprPrec := Grove2022.instReprCWorld.repr }

def Grove2022.instReprCWorld.repr : CWorld → ℕ → Std.Format

Equations

• Grove2022.instReprCWorld.repr Grove2022.CWorld.broSuit prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grove2022.CWorld.broSuit")).group prec✝
• Grove2022.instReprCWorld.repr Grove2022.CWorld.broNoSuit prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grove2022.CWorld.broNoSuit")).group prec✝
• Grove2022.instReprCWorld.repr Grove2022.CWorld.noBroSuit prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grove2022.CWorld.noBroSuit")).group prec✝
• Grove2022.instReprCWorld.repr Grove2022.CWorld.noBro prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Grove2022.CWorld.noBro")).group prec✝

def Grove2022.hasBrother : CWorld → Bool

Equations

• Grove2022.hasBrother Grove2022.CWorld.broSuit = true
• Grove2022.hasBrother Grove2022.CWorld.broNoSuit = true
• Grove2022.hasBrother Grove2022.CWorld.noBroSuit = false
• Grove2022.hasBrother Grove2022.CWorld.noBro = false

def Grove2022.hasWetsuit : CWorld → Bool

Equations

• Grove2022.hasWetsuit Grove2022.CWorld.broSuit = true
• Grove2022.hasWetsuit Grove2022.CWorld.noBroSuit = true
• Grove2022.hasWetsuit Grove2022.CWorld.broNoSuit = false
• Grove2022.hasWetsuit Grove2022.CWorld.noBro = false

def Grove2022.bringsWetsuit : CWorld → Bool

Whether Theo brings his wetsuit (only meaningful when he has one).

Equations

• Grove2022.bringsWetsuit Grove2022.CWorld.broSuit = true
• Grove2022.bringsWetsuit x✝ = false

§2 The presupposition trigger

"His wetsuit" denotes type e_# (= Option Entity): defined when Theo has a unique wetsuit, undefined otherwise. In our simplified model, the entity is irrelevant — what matters is the definedness condition. So we model the trigger's contribution to the truth value as Option Bool: defined (with value bring(t)) when hasWetsuit, undefined otherwise.

def Grove2022.hisWetsuit : CWorld → Option Bool

"his wetsuit" contributes definedness + the bring predicate.

Modeling the trigger's contribution to the sentential truth value:

• At worlds where Theo has a wetsuit: some (bringsWetsuit w)
• At worlds where he doesn't: none (presupposition failure)

Equations

• Grove2022.hisWetsuit w = if Grove2022.hasWetsuit w = true then some (Grove2022.bringsWetsuit w) else none

§3 Local reading (narrow scope)

The trigger takes scope within the consequent clause. The conditional's interpretation uses materialCond, which checks the consequent only when the antecedent is true. Result: the presupposition is conditional (hasBrother → hasWetsuit).

def Grove2022.localReading : CWorld → Option Bool

Local reading of "If Theo has a brother, he'll bring his wetsuit."

The trigger stays inside the consequent. The conditional filters: materialCond (some (hasBrother w)) (hisWetsuit w).

Equations

• Grove2022.localReading w = Semantics.Composition.MaybeMonad.materialCond (some (Grove2022.hasBrother w)) (Grove2022.hisWetsuit w)

theorem Grove2022.local_broSuit : localReading CWorld.broSuit = some true

At broSuit: brother ✓, wetsuit ✓, brings ✓ → some true.

theorem Grove2022.local_broNoSuit : localReading CWorld.broNoSuit = none

At broNoSuit: brother ✓, no wetsuit → none (presup failure).

theorem Grove2022.local_noBroSuit : localReading CWorld.noBroSuit = some true

At noBroSuit: no brother → some true (conditional vacuously true).

theorem Grove2022.local_noBro : localReading CWorld.noBro = some true

At noBro: no brother → some true (vacuously true).

theorem Grove2022.local_definedness (w : CWorld) : (localReading w).isSome = (!hasBrother w || hasWetsuit w)

The local reading is defined iff hasBrother → hasWetsuit.

This is the conditional presupposition that @cite{geurts-1996} observed satisfaction accounts predict — and which Grove argues is merely one of two available readings.

§4 Global reading (wide scope)

The trigger takes scope over the entire conditional via cyclic scope-taking (roll-up pied-piping). The trigger's definedness is checked first; only then does the conditional apply. Result: the presupposition is unconditional (hasWetsuit).

def Grove2022.globalReading : CWorld → Option Bool

Global reading: the trigger scopes over the conditional.

hisWetsuit w >>= (λ b => materialCond (some (hasBrother w)) (some b))

First check definedness of the trigger; then, if defined, evaluate the conditional with a fully-defined consequent.

Equations

• Grove2022.globalReading w = do let b ← Grove2022.hisWetsuit w Semantics.Composition.MaybeMonad.materialCond (some (Grove2022.hasBrother w)) (some b)

theorem Grove2022.global_broSuit : globalReading CWorld.broSuit = some true

At broSuit: wetsuit ✓ → defined. Brother ✓, brings ✓ → some true.

theorem Grove2022.global_broNoSuit : globalReading CWorld.broNoSuit = none

At broNoSuit: no wetsuit → none (presup failure).

theorem Grove2022.global_noBroSuit : globalReading CWorld.noBroSuit = some true

At noBroSuit: wetsuit ✓ → defined. No brother → some true.

theorem Grove2022.global_noBro : globalReading CWorld.noBro = none

At noBro: no wetsuit → none (presup failure).

theorem Grove2022.global_definedness (w : CWorld) : (globalReading w).isSome = hasWetsuit w

The global reading is defined iff hasWetsuit.

This is the unconditional presupposition that speakers actually accommodate for "If Theo has a brother, he'll bring his wetsuit." The proviso problem does not arise: this reading is semantically available without pragmatic strengthening.

§5 Scope ambiguity = no proviso problem

The two readings differ only in scope. At worlds where both readings are defined, they agree on truth value — the readings differ only in their presuppositions (definedness conditions).

theorem Grove2022.readings_agree_when_defined (w : CWorld) (hl : (localReading w).isSome = true) (hg : (globalReading w).isSome = true) : localReading w = globalReading w

Where both readings are defined, they agree on truth value.

theorem Grove2022.global_stronger_than_local : (∀ (w : CWorld), hasWetsuit w = true → (!hasBrother w || hasWetsuit w) = true) ∧ ¬∀ (w : CWorld), (!hasBrother w || hasWetsuit w) = true → hasWetsuit w = true

The global presupposition is strictly stronger than the local one: hasWetsuit → (hasBrother → hasWetsuit) but not vice versa.

theorem Grove2022.eta_bind_reconstructs (w : CWorld) : some (hisWetsuit w) >>= id = hisWetsuit w

Left Identity ensures that η-shifting inside the trigger's scope and then binding is the same as not shifting at all — this is why the narrow- scope derivation is equivalent to the standard satisfaction-theory prediction (Grove fn. 13).

§6 Attitude verb example: "Theo believes he lost his wetsuit"

We reuse the world model from @cite{heim-1992} (AttWorld with actual and believed) and show that the scope theory derives the same empirical predictions via different machinery.

def Grove2022.lostWetsuit : Semantics.Composition.MaybeMonad.Iₚ Heim1992.AttWorld Bool

The complement "he lost his wetsuit" as an Iₚ-typed meaning.

Presupposes Theo has a wetsuit at the evaluation world. When defined, asserts he lost it. At believed: has wetsuit ✓, lost it ✓. At actual: no wetsuit → undefined.

Equations

• Grove2022.lostWetsuit Heim1992.AttWorld.believed = some true
• Grove2022.lostWetsuit Heim1992.AttWorld.actual = none

def Grove2022.believeLocal : Semantics.Composition.MaybeMonad.Iₚ Heim1992.AttWorld Bool

Local reading of "Theo believes he lost his wetsuit."

The complement stays in situ; believe quantifies over doxastic alternatives with the complement evaluated locally.

Equations

• Grove2022.believeLocal = Semantics.Composition.MaybeMonad.believe (fun (x : Unit) => Heim1992.believesRBool) [Heim1992.AttWorld.actual, Heim1992.AttWorld.believed] Grove2022.lostWetsuit ()

theorem Grove2022.believe_local_actual : believeLocal Heim1992.AttWorld.actual = some true

Local reading at actual: Theo's only belief-world is believed, where the complement is defined and true → some true.

theorem Grove2022.believe_local_believed : believeLocal Heim1992.AttWorld.believed = some true

Local reading at believed: same → some true.

theorem Grove2022.believe_local_always_defined (w : Heim1992.AttWorld) : (believeLocal w).isSome = true

The local reading is always defined.

The presupposition is that Theo believes he has a wetsuit (= the complement is defined at all doxastic alternatives). Since believed is the only belief-accessible world from either world, and the complement is defined there, this always holds. No projection to the actual world.

def Grove2022.believeGlobal : Semantics.Composition.MaybeMonad.Iₚ Heim1992.AttWorld Bool

Global reading: the complement scopes out.

The complement's definedness is evaluated at the actual world (not within the scope of believe).

Equations

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

theorem Grove2022.believe_global_actual : believeGlobal Heim1992.AttWorld.actual = none

Global reading at actual: complement is undefined → none.

The presupposition projects globally: Theo must actually have a wetsuit at the evaluation world.

theorem Grove2022.believe_global_believed : believeGlobal Heim1992.AttWorld.believed = some true

Global reading at believed: complement defined → some true.

theorem Grove2022.believe_global_definedness (w : Heim1992.AttWorld) : (believeGlobal w).isSome = (lostWetsuit w).isSome

The global reading is defined iff the complement is defined at the evaluation world — the presupposition projects past believe.

§7 Connection to @cite{heim-1992}

@cite{heim-1992}'s know/believe asymmetry is derived in Heim1992.lean via local-context filtering and KD45 frame conditions. The scope theory provides an alternative explanation: the asymmetry arises because the trigger can take different scopes relative to the attitude verb.

The local reading corresponds to Heim's standard satisfaction-theory prediction. The global reading is what the satisfaction theory cannot derive — and what the scope theory adds.

theorem Grove2022.local_matches_heim_belief : (believeLocal Heim1992.AttWorld.actual).isSome = true ∧ (lostWetsuit Heim1992.AttWorld.actual).isSome = false

The local reading's definedness matches Heim's belief-embedding prediction: the presupposition is filtered (projected into the attitude holder's beliefs, not to the actual world).

theorem Grove2022.global_projects_past_attitude : (believeGlobal Heim1992.AttWorld.actual).isSome = false ∧ (lostWetsuit Heim1992.AttWorld.actual).isSome = false

The global reading adds what Heim's account lacks: a reading where the presupposition projects past the attitude verb entirely.