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 Schlenker2009.shiftsUnderBelief :

Phenomena.Presupposition.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 Schlenker2009.ole_matches_shift (c : Phenomena.Presupposition.ProjectiveContent.ProjectiveClass) :

shiftsUnderBelief c = true ↔ c.ole = Phenomena.Presupposition.ProjectiveContent.ObligatoryLocalEffect.obligatory

OLE status matches shift behavior.

source

theorem Schlenker2009.ole_from_local_contexts (trigger : Phenomena.Presupposition.ProjectiveContent.ProjectiveTrigger) :

shiftsUnderBelief trigger.toClass = true ↔ trigger.toClass.ole = Phenomena.Presupposition.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 Schlenker2009.TriggerBehavior (W : Type u_3) (Agent : Type u_4) :

Type u_3

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

content : Set W
scf : Phenomena.Presupposition.ProjectiveContent.StrongContextualFelicity
ole : Phenomena.Presupposition.ProjectiveContent.ObligatoryLocalEffect

Instances For

source

def 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 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 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 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 Schlenker2009.class_from_scf_ole {W : Type u_1} {Agent : Type u_2} (tb : TriggerBehavior W Agent) :

SCF-OLE correspondence with Tonhauser classes.

source

theorem 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 Schlenker2009.stop_is_classC :

Phenomena.Presupposition.ProjectiveContent.ProjectiveTrigger.stop_prestate.toClass = Phenomena.Presupposition.ProjectiveContent.ProjectiveClass.classC

source

theorem Schlenker2009.expressive_is_classB :

Phenomena.Presupposition.ProjectiveContent.ProjectiveTrigger.expressive.toClass = Phenomena.Presupposition.ProjectiveContent.ProjectiveClass.classB

source

theorem Schlenker2009.pronoun_is_classA :

Phenomena.Presupposition.ProjectiveContent.ProjectiveTrigger.pronoun_existence.toClass = Phenomena.Presupposition.ProjectiveContent.ProjectiveClass.classA

source

theorem Schlenker2009.demonstrative_is_classD :

Phenomena.Presupposition.ProjectiveContent.ProjectiveTrigger.demonstrative_indication.toClass = Phenomena.Presupposition.ProjectiveContent.ProjectiveClass.classD

source

theorem Schlenker2009.schlenker_derives_tonhauser {W : Type u_1} {Agent : Type u_2} :

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

source

theorem Schlenker2009.stop_allows_informativity :

Phenomena.Presupposition.ProjectiveContent.ProjectiveTrigger.stop_prestate.toClass.scf = Phenomena.Presupposition.ProjectiveContent.StrongContextualFelicity.noRequires

source

theorem Schlenker2009.stop_shifts_under_belief :

Phenomena.Presupposition.ProjectiveContent.ProjectiveTrigger.stop_prestate.toClass.ole = Phenomena.Presupposition.ProjectiveContent.ObligatoryLocalEffect.obligatory

source

theorem Schlenker2009.expressive_allows_informativity :

Phenomena.Presupposition.ProjectiveContent.ProjectiveTrigger.expressive.toClass.scf = Phenomena.Presupposition.ProjectiveContent.StrongContextualFelicity.noRequires

source

theorem Schlenker2009.expressive_stays_with_speaker :

Phenomena.Presupposition.ProjectiveContent.ProjectiveTrigger.expressive.toClass.ole = Phenomena.Presupposition.ProjectiveContent.ObligatoryLocalEffect.notObligatory

source

theorem Schlenker2009.pronoun_requires_antecedent :

Phenomena.Presupposition.ProjectiveContent.ProjectiveTrigger.pronoun_existence.toClass.scf = Phenomena.Presupposition.ProjectiveContent.StrongContextualFelicity.requires

source

theorem Schlenker2009.pronoun_shifts_under_belief :

Phenomena.Presupposition.ProjectiveContent.ProjectiveTrigger.pronoun_existence.toClass.ole = Phenomena.Presupposition.ProjectiveContent.ObligatoryLocalEffect.obligatory

Documentation

Linglib.Phenomena.Presupposition.Studies.Schlenker2009

Belief Embedding -> Projective Content Taxonomy #