Documentation

Linglib.Phenomena.Presupposition.Studies.Schlenker2009

Belief Embedding -> Projective Content Taxonomy #

@cite{schlenker-2009} @cite{tonhauser-beaver-roberts-simons-2013}

Connects the Schlenker local context machinery for belief embedding to the @cite{tonhauser-beaver-roberts-simons-2013} projective content taxonomy.

Proves that OLE (Obligatory Local Effect) status matches shift behavior under belief predicates, and verifies trigger-specific predictions.

source
def Phenomena.Presupposition.Studies.Schlenker2009.shiftsUnderBelief :
ProjectiveContent.ProjectiveClass → Bool

Determines whether a projective trigger's content shifts to the attitude holder's perspective under belief embedding.

OLE = yes: Content shifts to attitude holder (computed from their beliefs) OLE = no: Content remains attributed to speaker (no perspective shift)

Equations
Instances For
    source
    theorem Phenomena.Presupposition.Studies.Schlenker2009.ole_matches_shift (c : ProjectiveContent.ProjectiveClass) :
    shiftsUnderBelief c = true ↔ c.ole = ProjectiveContent.ObligatoryLocalEffect.obligatory

    OLE status matches shift behavior.

    source
    theorem Phenomena.Presupposition.Studies.Schlenker2009.ole_from_local_contexts (trigger : ProjectiveContent.ProjectiveTrigger) :
    shiftsUnderBelief trigger.toClass = true ↔ trigger.toClass.ole = ProjectiveContent.ObligatoryLocalEffect.obligatory

    The Schlenker local context machinery derives the OLE predictions from @cite{tonhauser-beaver-roberts-simons-2013}.

    For any trigger:

    • If OLE=yes (Class A, C): Local context under belief = attitude holder's beliefs
    • If OLE=no (Class B, D): Local context under belief = global context (speaker)

    This explains why "stop" presuppositions shift to attitude holders but "damn" expressives don't.

    Connects Schlenker's local context theory to the full empirical taxonomy of @cite{tonhauser-beaver-roberts-simons-2013}. The four-class taxonomy is derived from the SCF x OLE feature space.

    source
    structure Phenomena.Presupposition.Studies.Schlenker2009.TriggerBehavior (W : Type u_3) (Agent : Type u_4) :
    Type u_3

    A projective trigger's behavior characterized by SCF and OLE values.

    Instances For
      source
      def Phenomena.Presupposition.Studies.Schlenker2009.isClassA {W : Type u_1} {Agent : Type u_2} (tb : TriggerBehavior W Agent) :
      Prop
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Phenomena.Presupposition.Studies.Schlenker2009.isClassB {W : Type u_1} {Agent : Type u_2} (tb : TriggerBehavior W Agent) :
        Prop
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Phenomena.Presupposition.Studies.Schlenker2009.isClassC {W : Type u_1} {Agent : Type u_2} (tb : TriggerBehavior W Agent) :
          Prop
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Phenomena.Presupposition.Studies.Schlenker2009.isClassD {W : Type u_1} {Agent : Type u_2} (tb : TriggerBehavior W Agent) :
            Prop
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Phenomena.Presupposition.Studies.Schlenker2009.class_from_scf_ole {W : Type u_1} {Agent : Type u_2} (tb : TriggerBehavior W Agent) :
              (isClassA tb ↔ tb.scf = ProjectiveContent.StrongContextualFelicity.requires ∧ tb.ole = ProjectiveContent.ObligatoryLocalEffect.obligatory) ∧ (isClassB tb ↔ tb.scf = ProjectiveContent.StrongContextualFelicity.noRequires ∧ tb.ole = ProjectiveContent.ObligatoryLocalEffect.notObligatory) ∧ (isClassC tb ↔ tb.scf = ProjectiveContent.StrongContextualFelicity.noRequires ∧ tb.ole = ProjectiveContent.ObligatoryLocalEffect.obligatory) ∧ (isClassD tb ↔ tb.scf = ProjectiveContent.StrongContextualFelicity.requires ∧ tb.ole = ProjectiveContent.ObligatoryLocalEffect.notObligatory)

              SCF-OLE correspondence with Tonhauser classes.

              source
              theorem Phenomena.Presupposition.Studies.Schlenker2009.classes_partition {W : Type u_1} {Agent : Type u_2} (tb : TriggerBehavior W Agent) :
              (isClassA tb ∨ isClassB tb ∨ isClassC tb ∨ isClassD tb) ∧ ¬(isClassA tb ∧ isClassB tb) ∧ ¬(isClassA tb ∧ isClassC tb) ∧ ¬(isClassA tb ∧ isClassD tb) ∧ ¬(isClassB tb ∧ isClassC tb) ∧ ¬(isClassB tb ∧ isClassD tb) ∧ ¬(isClassC tb ∧ isClassD tb)

              Classes partition the space.

              source
              theorem Phenomena.Presupposition.Studies.Schlenker2009.stop_is_classC :
              ProjectiveContent.ProjectiveTrigger.stop_prestate.toClass = ProjectiveContent.ProjectiveClass.classC
              source
              theorem Phenomena.Presupposition.Studies.Schlenker2009.expressive_is_classB :
              ProjectiveContent.ProjectiveTrigger.expressive.toClass = ProjectiveContent.ProjectiveClass.classB
              source
              theorem Phenomena.Presupposition.Studies.Schlenker2009.pronoun_is_classA :
              ProjectiveContent.ProjectiveTrigger.pronoun_existence.toClass = ProjectiveContent.ProjectiveClass.classA
              source
              theorem Phenomena.Presupposition.Studies.Schlenker2009.demonstrative_is_classD :
              ProjectiveContent.ProjectiveTrigger.demonstrative_indication.toClass = ProjectiveContent.ProjectiveClass.classD
              source
              theorem Phenomena.Presupposition.Studies.Schlenker2009.schlenker_derives_tonhauser {W : Type u_1} {Agent : Type u_2} :
              (∀ (c : Core.CommonGround.ContextSet W), (Semantics.Presupposition.LocalContext.initialLocalCtx c).worlds = c) ∧ (∀ (blc : Semantics.Presupposition.BeliefEmbedding.BeliefLocalCtx W Agent) (w : W) (h : blc.globalCtx w), (Semantics.Presupposition.BeliefEmbedding.beliefToLocalCtx blc w h).worlds = blc.atWorld w) ∧ (∀ (c : ProjectiveContent.ProjectiveClass), c = ProjectiveContent.classFromProperties c.scf c.ole) ∧ ProjectiveContent.ProjectiveClass.classA ≠ ProjectiveContent.ProjectiveClass.classB ∧ ProjectiveContent.ProjectiveClass.classA ≠ ProjectiveContent.ProjectiveClass.classC ∧ ProjectiveContent.ProjectiveClass.classA ≠ ProjectiveContent.ProjectiveClass.classD ∧ ProjectiveContent.ProjectiveClass.classB ≠ ProjectiveContent.ProjectiveClass.classC ∧ ProjectiveContent.ProjectiveClass.classB ≠ ProjectiveContent.ProjectiveClass.classD ∧ ProjectiveContent.ProjectiveClass.classC ≠ ProjectiveContent.ProjectiveClass.classD

              Schlenker's local context theory derives Tonhauser's taxonomy.

              source
              theorem Phenomena.Presupposition.Studies.Schlenker2009.stop_allows_informativity :
              ProjectiveContent.ProjectiveTrigger.stop_prestate.toClass.scf = ProjectiveContent.StrongContextualFelicity.noRequires
              source
              theorem Phenomena.Presupposition.Studies.Schlenker2009.stop_shifts_under_belief :
              ProjectiveContent.ProjectiveTrigger.stop_prestate.toClass.ole = ProjectiveContent.ObligatoryLocalEffect.obligatory
              source
              theorem Phenomena.Presupposition.Studies.Schlenker2009.expressive_allows_informativity :
              ProjectiveContent.ProjectiveTrigger.expressive.toClass.scf = ProjectiveContent.StrongContextualFelicity.noRequires
              source
              theorem Phenomena.Presupposition.Studies.Schlenker2009.expressive_stays_with_speaker :
              ProjectiveContent.ProjectiveTrigger.expressive.toClass.ole = ProjectiveContent.ObligatoryLocalEffect.notObligatory
              source
              theorem Phenomena.Presupposition.Studies.Schlenker2009.pronoun_requires_antecedent :
              ProjectiveContent.ProjectiveTrigger.pronoun_existence.toClass.scf = ProjectiveContent.StrongContextualFelicity.requires
              source
              theorem Phenomena.Presupposition.Studies.Schlenker2009.pronoun_shifts_under_belief :
              ProjectiveContent.ProjectiveTrigger.pronoun_existence.toClass.ole = ProjectiveContent.ObligatoryLocalEffect.obligatory