[Gro22]: Presupposition Projection as a Scope Phenomenon

Julian Grove (2022). "Presupposition projection as a scope phenomenon." Semantics and Pragmatics 15, Article 15: 1–39. https://doi.org/10.3765/sp.15.15

Thesis

The proviso problem — where [Hei83]'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 α#-typed denotations (= Option α); they interact with the surrounding context via monadic bind, exactly paralleling [Cha20]'s treatment of indefinites with the set monad.

The paper develops the apparatus (Part I below) and applies it to the classic "If Theo has a brother, he'll bring his wetsuit" minimal pair plus attitude-verb examples (Part II).

Part I — Apparatus (Grove §§3–4)

• materialCond — material conditional with middle Kleene semantics (eq. 16): ⊤ ⇒ ψ = ψ, ⊥ ⇒ ψ = ⊤, # ⇒ ψ = #
• meetWK / joinWK — weak Kleene conjunction / disjunction (used by the presuppositional universal, where undefinedness absorbs from either side)
• Iₚ I := ReaderT I Option — Grove's I# (footnote 18: "Reader monad transformer applied to the maybe monad"); Iₚ is a Lean-typographical rename since # isn't a Lean subscript
• Monad laws (Figure 7) inherited via mathlib's LawfulMonad ReaderT
• evalI — evaluation (·)^ž (eq. 20)
• forallP / existsP — presuppositional quantifiers (eq. 27)
• believe — doxastic attitude verb (eq. 28)
• Bridges to Truth3, Prop3, PartialProp

Part II — Empirical predictions (Grove §3, §4.2)

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

• Local reading (narrow scope): trigger stays in the consequent → presupposition is hasBrother → hasWetsuit (conditional)
• Global reading (wide scope): trigger scopes over the conditional via roll-up pied-piping → 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.

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

• 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 Heim1992Projection.lean's know/believe asymmetry but derives it from scope rather than from local-context filtering.

Parallel with the set monad ([Cha20])

	Alternatives ([Cha20])	Presupposition ([Gro22])
Monad	S α = α → Prop (sets)	Option α (maybe)
Unit	η_S(x) = {x}	η_#(v) = some v
Bind	m ⫝̸_S f = ⋃_{x∈m} f(x)	v ⋆_# k = k(v); # ⋆_# k = #
Effect	Indeterminacy	Partiality
Scope	Indefinites escape islands	Presuppositions project past filters

Part I — Apparatus

§1 Connectives on Option Bool

Grove uses two distinct gap-propagation policies:

• Middle Kleene for the material conditional ⇒: left-undefined absorbs, but right-undefined does NOT absorb when the left is false (⊥ ⇒ # = ⊤).
• Weak Kleene for ∀_#: undefinedness absorbs from either side (⊥ ∧ # = #, unlike Strong Kleene where ⊥ ∧ # = ⊥).

def Grove2022.materialCond : Option Bool → Option Bool → Option Bool

Material conditional ⇒ with middle Kleene semantics (eq. 16): ⊤ ⇒ ψ = ψ, ⊥ ⇒ ψ = ⊤, # ⇒ ψ = #. The conditional is true when its antecedent is false (regardless of consequent definedness), and propagates the consequent when the antecedent is true. Undefinedness in the antecedent absorbs.

Equations

• Grove2022.materialCond none x✝ = none
• Grove2022.materialCond (some false) x✝ = some true
• Grove2022.materialCond (some true) x✝ = x✝

def Grove2022.meetWK : Option Bool → Option Bool → Option Bool

Weak Kleene conjunction (used by forallP). Undefinedness absorbs from either side, then falsity absorbs. (Contrast Strong Kleene: ⊥ ∧ # = ⊥ vs Weak Kleene ⊥ ∧ # = #.)

Equations

• Grove2022.meetWK none x✝ = none
• Grove2022.meetWK x✝ none = none
• Grove2022.meetWK (some false) x✝ = some false
• Grove2022.meetWK x✝ (some false) = some false
• Grove2022.meetWK (some true) (some true) = some true

def Grove2022.joinWK : Option Bool → Option Bool → Option Bool

Weak Kleene disjunction. Dual of meetWK.

Equations

• Grove2022.joinWK none x✝ = none
• Grove2022.joinWK x✝ none = none
• Grove2022.joinWK (some true) x✝ = some true
• Grove2022.joinWK x✝ (some true) = some true
• Grove2022.joinWK (some false) (some false) = some false

theorem Grove2022.materialCond_false_absorbs (ψ : Option Bool) : materialCond (some false) ψ = some true

theorem Grove2022.materialCond_true_passes (ψ : Option Bool) : materialCond (some true) ψ = ψ

theorem Grove2022.materialCond_undef_absorbs (ψ : Option Bool) : materialCond none ψ = none

theorem Grove2022.meetWK_comm (a b : Option Bool) : meetWK a b = meetWK b a

§2 The intensional-presuppositional monad Iₚ

Iₚ I α = I → Option α: the Reader monad transformer applied to the maybe monad. An expression of type Iₚ I α reads an index i (world, world-assignment pair, etc.) and returns some v if defined at i, or none on presupposition failure — Grove §4.1's uniform treatment of intensionality and presupposition (replacing t with t_# in the intensional type i → t).

Defining Iₚ as ReaderT I Option makes pure/>>= Grove's η_#/⋆_# and inherits Monad/LawfulMonad from mathlib. (Grove writes I#; Iₚ here is a Lean-friendly rename since # isn't a subscript glyph.)

@[reducible, inline]

abbrev Grove2022.Iₚ (I α : Type) : Type

Equations

• Grove2022.Iₚ I = ReaderT I Option

§3 Monad laws

Iₚ = ReaderT I Option is a LawfulMonad, so Grove's three laws (Figure 7: Left Identity, Right Identity, Associativity) hold via pure_bind, bind_pure, bind_assoc — no standalone rfl theorems needed. Left Identity and Associativity are the load-bearing scope-taking properties: Left Identity gives reconstruction (η + ⋆ = no scope; fn. 13), and Associativity makes cyclic scope-taking (roll-up pied-piping) sound (the presuppositional analog of [Cha20]'s ASSOCIATIVITY for the set monad).

§4 Semantic operations

def Grove2022.evalI {I : Type} (φ : Iₚ I (I → Bool)) : Iₚ I Bool

Evaluation function (·)^ž (eq. 20). Given φ : Iₚ I (I → Bool) (a proposition that reads an index, possibly undefined, to return an intension), evalI φ feeds the index to itself: evalI φ i = (φ i).map (· i).

Equations

• Grove2022.evalI φ i = Option.map (fun (x : I → Bool) => x i) (φ i)

def Grove2022.forallP {α : Type} (xs : List α) (φ : α → Option Bool) : Option Bool

Presuppositional universal ∀_# (eq. 27). Weak Kleene: none absorbs (if the scope is undefined at any value, the whole universal is undefined).

Equations

• Grove2022.forallP xs φ = List.foldl (fun (acc : Option Bool) (x : α) => Grove2022.meetWK acc (φ x)) (some true) xs

def Grove2022.existsP {α : Type} (xs : List α) (φ : α → Option Bool) : Option Bool

Presuppositional existential (dual of forallP).

Equations

• Grove2022.existsP xs φ = List.foldl (fun (acc : Option Bool) (x : α) => Grove2022.joinWK acc (φ x)) (some false) xs

theorem Grove2022.forallP_all_true {α : Type} (xs : List α) (φ : α → Option Bool) (h : ∀ x ∈ xs, φ x = some true) : forallP xs φ = some true

forallP on an all-true list is some true.

theorem Grove2022.forallP_undef {α : Type} (xs : List α) (φ : α → Option Bool) (x : α) (hx : x ∈ xs) (hu : φ x = none) : forallP xs φ = none

forallP with an undefined element is none — meetWK has none as a zero element, so once any φ(x) = none is encountered, the accumulator becomes none and stays none.

§5 Attitude verb semantics (Grove §4.2, eq. 28)

believe = λφ,x,i. ∀_# j : dox(x,i,j) ⇒ φ(j) — the verb quantifies over doxastically accessible worlds with ∀_# and uses the material conditional ⇒. The ⇒ contributes the key filtering behavior: when dox(x,i,j) = false, ⇒ returns some true regardless of φ(j)'s definedness.

def Grove2022.believe {W E : Type} (dox : E → W → W → Bool) (worlds : List W) (φ : Iₚ W Bool) (x : E) : Iₚ W Bool

believe (eq. 28). Given an accessibility relation dox, a list of worlds, a complement φ : Iₚ W Bool, an agent x, and an evaluation world i: believe dox worlds φ x i = ∀_# j ∈ worlds : dox(x,i,j) ⇒ φ(j)

Equations

• Grove2022.believe dox worlds φ x i = Grove2022.forallP worlds fun (j : W) => Grove2022.materialCond (some (dox x i j)) (φ j)

§6 Bridges to existing linglib types

Option Bool, Truth3, and PartialProp W are three representations of possibly-undefined truth values. These conversions connect Grove's formalisation to the rest of the presupposition infrastructure.

def Grove2022.toTruth3 : Option Bool → Core.Duality.Truth3

Convert Option Bool to Truth3.

Equations

• Grove2022.toTruth3 (some true) = Core.Duality.Truth3.true
• Grove2022.toTruth3 (some false) = Core.Duality.Truth3.false
• Grove2022.toTruth3 none = Core.Duality.Truth3.indet

def Grove2022.ofTruth3 : Core.Duality.Truth3 → Option Bool

Convert Truth3 to Option Bool.

Equations

• Grove2022.ofTruth3 Core.Duality.Truth3.true = some true
• Grove2022.ofTruth3 Core.Duality.Truth3.false = some false
• Grove2022.ofTruth3 Core.Duality.Truth3.indet = none

theorem Grove2022.roundtrip_truth3 (v : Core.Duality.Truth3) : toTruth3 (ofTruth3 v) = v

theorem Grove2022.roundtrip_option (v : Option Bool) : ofTruth3 (toTruth3 v) = v

def Grove2022.impMK : Core.Duality.Truth3 → Core.Duality.Truth3 → Core.Duality.Truth3

Middle Kleene implication on Truth3.

Equations

• Grove2022.impMK Core.Duality.Truth3.indet x✝ = Core.Duality.Truth3.indet
• Grove2022.impMK Core.Duality.Truth3.false x✝ = Core.Duality.Truth3.true
• Grove2022.impMK Core.Duality.Truth3.true x✝ = x✝

theorem Grove2022.materialCond_eq_truth3 (p q : Option Bool) : toTruth3 (materialCond p q) = impMK (toTruth3 p) (toTruth3 q)

materialCond corresponds to middle Kleene implication on Truth3.

theorem Grove2022.meetWK_eq_truth3 (p q : Option Bool) : toTruth3 (meetWK p q) = (toTruth3 p).meetWeak (toTruth3 q)

meetWK corresponds to Truth3.meetWeak.

theorem Grove2022.joinWK_eq_truth3 (p q : Option Bool) : toTruth3 (joinWK p q) = (toTruth3 p).joinWeak (toTruth3 q)

joinWK corresponds to Truth3.joinWeak.

def Grove2022.toProp3 {W : Type} (φ : Iₚ W Bool) : Core.Duality.Prop3 W

Convert Iₚ W Bool to Prop3 W (world-indexed three-valued proposition).

Equations

• Grove2022.toProp3 φ w = Grove2022.toTruth3 (φ w)

def Grove2022.toPartialProp {W : Type} (φ : Iₚ W Bool) : Semantics.Presupposition.PartialProp W

Convert Iₚ W Bool to PartialProp W. The presupposition field is isSome (defined?), and the assertion is the Bool value (defaulting to false when undefined).

Equations

• Grove2022.toPartialProp φ = { presup := fun (w : W) => (φ w).isSome = true, assertion := fun (w : W) => (φ w).getD false = true }

theorem Grove2022.toPartialProp_presup {W : Type} (φ : Iₚ W Bool) (w : W) : (toPartialProp φ).presup w = ((φ w).isSome = true)

theorem Grove2022.toPartialProp_assertion {W : Type} (φ : Iₚ W Bool) (w : W) (v : Bool) (h : φ w = some v) : (toPartialProp φ).assertion w = (v = true)

Part II — Empirical predictions

§7 World model for the conditional cases

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

inductive Grove2022.CWorld : Type

• 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 ⋯

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✝

@[implicit_reducible]

instance Grove2022.instReprCWorld : Repr CWorld

Equations

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

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

§8 The presupposition trigger "his wetsuit"

"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.

• 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

§9 Local reading: conditional presupposition

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 = Grove2022.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 [geurts-1996] observed satisfaction accounts predict — and which Grove argues is merely one of two available readings.

§10 Global reading: unconditional presupposition

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 Grove2022.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.

§11 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).

§12 Attitude verbs: "Theo believes he lost his wetsuit"

Reuse the world model from [Hei92] (AttWorld with actual and believed) and show that the scope theory derives the same empirical predictions via different machinery.

def Grove2022.lostWetsuit : 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 : 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 = Grove2022.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 : 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.

§13 Bridge to [Hei92]

[Hei92]'s know/believe asymmetry is derived in Heim1992Projection.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.