Documentation

Linglib.Phenomena.Presupposition.Studies.Grove2022

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

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:

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

Empirical Data #

§1 World model #

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

source
inductive Phenomena.Presupposition.Studies.Grove2022.CWorld :
Type

Worlds for the conditional examples.

Instances For
    source
    instance Phenomena.Presupposition.Studies.Grove2022.instDecidableEqCWorld :
    DecidableEq CWorld
    Equations
    source
    instance Phenomena.Presupposition.Studies.Grove2022.instBEqCWorld :
    BEq CWorld
    Equations
    source
    def Phenomena.Presupposition.Studies.Grove2022.instBEqCWorld.beq :
    CWorld → CWorld → Bool
    Equations
    Instances For
      source
      instance Phenomena.Presupposition.Studies.Grove2022.instReprCWorld :
      Repr CWorld
      Equations
      source
      def Phenomena.Presupposition.Studies.Grove2022.instReprCWorld.repr :
      CWorld → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Phenomena.Presupposition.Studies.Grove2022.hasBrother :
        CWorld → Bool
        Equations
        Instances For
          source
          def Phenomena.Presupposition.Studies.Grove2022.hasWetsuit :
          CWorld → Bool
          Equations
          Instances For
            source
            def Phenomena.Presupposition.Studies.Grove2022.bringsWetsuit :
            CWorld → Bool

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

            Equations
            Instances For

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

              source
              def Phenomena.Presupposition.Studies.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
              • One or more equations did not get rendered due to their size.
              Instances For

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

                source
                def Phenomena.Presupposition.Studies.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
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem Phenomena.Presupposition.Studies.Grove2022.local_broSuit :
                  localReading CWorld.broSuit = some true

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

                  source
                  theorem Phenomena.Presupposition.Studies.Grove2022.local_broNoSuit :
                  localReading CWorld.broNoSuit = none

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

                  source
                  theorem Phenomena.Presupposition.Studies.Grove2022.local_noBroSuit :
                  localReading CWorld.noBroSuit = some true

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

                  source
                  theorem Phenomena.Presupposition.Studies.Grove2022.local_noBro :
                  localReading CWorld.noBro = some true

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

                  source
                  theorem Phenomena.Presupposition.Studies.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).

                  source
                  def Phenomena.Presupposition.Studies.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
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem Phenomena.Presupposition.Studies.Grove2022.global_broSuit :
                    globalReading CWorld.broSuit = some true

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

                    source
                    theorem Phenomena.Presupposition.Studies.Grove2022.global_broNoSuit :
                    globalReading CWorld.broNoSuit = none

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

                    source
                    theorem Phenomena.Presupposition.Studies.Grove2022.global_noBroSuit :
                    globalReading CWorld.noBroSuit = some true

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

                    source
                    theorem Phenomena.Presupposition.Studies.Grove2022.global_noBro :
                    globalReading CWorld.noBro = none

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

                    source
                    theorem Phenomena.Presupposition.Studies.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).

                    source
                    theorem Phenomena.Presupposition.Studies.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.

                    source
                    theorem Phenomena.Presupposition.Studies.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.

                    source
                    theorem Phenomena.Presupposition.Studies.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.

                    source
                    def Phenomena.Presupposition.Studies.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
                    Instances For
                      source
                      def Phenomena.Presupposition.Studies.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
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        theorem Phenomena.Presupposition.Studies.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.

                        source
                        theorem Phenomena.Presupposition.Studies.Grove2022.believe_local_believed :
                        believeLocal Heim1992.AttWorld.believed = some true

                        Local reading at believed: same → some true.

                        source
                        theorem Phenomena.Presupposition.Studies.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.

                        source
                        def Phenomena.Presupposition.Studies.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.
                        Instances For
                          source
                          theorem Phenomena.Presupposition.Studies.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.

                          source
                          theorem Phenomena.Presupposition.Studies.Grove2022.believe_global_believed :
                          believeGlobal Heim1992.AttWorld.believed = some true

                          Global reading at believed: complement defined → some true.

                          source
                          theorem Phenomena.Presupposition.Studies.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.

                          source
                          theorem Phenomena.Presupposition.Studies.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).

                          source
                          theorem Phenomena.Presupposition.Studies.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.