Documentation

Linglib.Studies.TonhauserEtAl2013

Tonhauser, Beaver, Roberts & Simons (2013): Taxonomy from Local Contexts #

Derives the four-class projective-content taxonomy of [TBRS13] from [Sch09a]-style local contexts ([Hei83], [Lew79b]). The classes cross-classify two properties:

Class	SCF	OLE	Derived behavior
A	yes	yes	Requires context + shifts under belief
B	no	no	Informative + speaker-anchored
C	no	yes	Informative + shifts under belief
D	yes	no	Requires context + speaker-anchored

[TBRS13] object to satisfaction theories:

"In theories like those of [Sch09a], where it is assumed that a presupposition is satisfied in its local context if it is entailed by it. Since, in general, the relevant local context is the context set ('which encodes what the speech act participants take for granted'), presuppositions are predicted to project. The heterogeneity of projective content, in particular the finding that many such contents are not associated with a strong contextual felicity constraint, provides an argument against an inclusive analysis of projection based on local satisfaction."

The resolution formalized here: projection is uniform (the local-context machinery), while accommodation varies by trigger class. OLE is derived directly from belief local contexts; SCF is characterized as a constraint on accommodation, not built into local contexts (a full SCF derivation needs QUD/information-structure machinery).

Main declarations #

SCF_Requires / SCF_Allows: Strong Contextual Felicity in local-context terms.
OLE_Obligatory / OLE_NotObligatory: Obligatory Local Effect via belief local contexts.
belief_derives_ole: belief embedding filters holder-attributed presuppositions, deriving OLE=yes behavior.
classes_partition: the SCF × OLE feature space partitions triggers into exactly the four classes.
schlenker_derives_tonhauser: the local-context theory reproduces the taxonomy's structural predictions.
traditional_crosscuts_classes: the traditional presupposition/CI labels cross-cut the SCF × OLE classes.

structure TonhauserEtAl2013.SCF_Requires (W : Type u_3) :

Type u_3

SCF (Strong Contextual Felicity) in local context terms.

A trigger has SCF=yes iff its projective content MUST be entailed by the global context for felicitous use. Accommodation is blocked.

In Schlenker's terms: the local context at matrix level IS the global context, and the presupposition must be entailed (not just "could be accommodated").

This is a marker structure. The constraint that accommodation is blocked is a property of the trigger class, not derivable from the content alone. Full derivation requires connecting to Accommodation.AccommodationOK and trigger-specific constraints (anaphoric binding, salience, etc.).

content : Set W
The projective content that must be established

Instances For

structure TonhauserEtAl2013.SCF_Allows (W : Type u_3) :

Type u_3

SCF=no means accommodation is ALLOWED.

The projective content can be informative — it can update the context rather than being required to already hold.

Witness: there exist non-empty contexts where the content is NOT entailed yet the trigger's use is still felicitous (via accommodation).

content : Set W
The projective content
accommodable : ∃ (c : CommonGround.ContextSet W), Set.Nonempty c ∧ ¬c.entails self.content
Accommodation is possible: there exist contexts where content is informative (not entailed) yet use is felicitous

Instances For

def TonhauserEtAl2013.OLE_Obligatory {W : Type u_1} {Agent : Type u_2} (Dox : Core.Logic.Modal.AgentAccessRel W Agent) (content : Set W) :

OLE (Obligatory Local Effect) in local context terms.

OLE=yes means: under belief embedding, the local context is the attitude holder's belief state. The projective content is attributed to the holder.

Equations

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

Instances For

def TonhauserEtAl2013.OLE_NotObligatory {W : Type u_1} {Agent : Type u_2} (Dox : Core.Logic.Modal.AgentAccessRel W Agent) (content : Set W) :

OLE=no means: under belief embedding, the projective content is still evaluated relative to the speaker's (global) context, not the holder's beliefs.

Formally: there exist doxastic contexts where the content holds globally but NOT in the attitude holder's beliefs. The content is "speaker-anchored" — it does not shift under belief embedding.

Class B triggers (expressives) and Class D triggers exhibit this behavior.

Equations

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

Instances For

theorem TonhauserEtAl2013.belief_derives_ole {W : Type u_1} {Agent : Type u_2} (blc : Semantics.Presupposition.BeliefEmbedding.BeliefLocalCtx W Agent) (p : Semantics.Presupposition.PartialProp W) (h : Semantics.Presupposition.BeliefEmbedding.presupAttributedToHolder blc p) (w_star : W) (hw : blc.globalCtx w_star) :

Semantics.Presupposition.LocalContext.presupFiltered (Semantics.Presupposition.BeliefEmbedding.beliefToLocalCtx blc w_star hw) p

OLE derivation: belief embedding creates an attitude-holder context.

Under "x believes φ", the local context at φ is x's belief state, so a presupposition attributed to the holder is filtered there. This derives OLE=yes behavior from [Sch09a]'s belief local contexts.

def TonhauserEtAl2013.shiftsUnderBelief :

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

theorem TonhauserEtAl2013.ole_matches_shift (c : Semantics.Presupposition.ProjectiveContent.ProjectiveClass) :

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

OLE status matches shift behavior.

theorem TonhauserEtAl2013.ole_from_local_contexts (trigger : Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger) :

shiftsUnderBelief trigger.toClass = true ↔ trigger.toClass.ole = Semantics.Presupposition.ProjectiveContent.ObligatoryLocalEffect.obligatory

The Schlenker local context machinery derives the OLE predictions from [TBRS13].

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.

structure TonhauserEtAl2013.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 : Semantics.Presupposition.ProjectiveContent.StrongContextualFelicity
ole : Semantics.Presupposition.ProjectiveContent.ObligatoryLocalEffect

Instances For

def TonhauserEtAl2013.isClassA {W : Type u_1} {Agent : Type u_2} (tb : TriggerBehavior W Agent) :

Equations

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

Instances For

def TonhauserEtAl2013.isClassB {W : Type u_1} {Agent : Type u_2} (tb : TriggerBehavior W Agent) :

Equations

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

Instances For

def TonhauserEtAl2013.isClassC {W : Type u_1} {Agent : Type u_2} (tb : TriggerBehavior W Agent) :

Equations

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

Instances For

def TonhauserEtAl2013.isClassD {W : Type u_1} {Agent : Type u_2} (tb : TriggerBehavior W Agent) :

Equations

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

Instances For

theorem TonhauserEtAl2013.class_from_scf_ole {W : Type u_1} {Agent : Type u_2} (tb : TriggerBehavior W Agent) :

(isClassA tb ↔ tb.scf = Semantics.Presupposition.ProjectiveContent.StrongContextualFelicity.requires ∧ tb.ole = Semantics.Presupposition.ProjectiveContent.ObligatoryLocalEffect.obligatory) ∧ (isClassB tb ↔ tb.scf = Semantics.Presupposition.ProjectiveContent.StrongContextualFelicity.noRequires ∧ tb.ole = Semantics.Presupposition.ProjectiveContent.ObligatoryLocalEffect.notObligatory) ∧ (isClassC tb ↔ tb.scf = Semantics.Presupposition.ProjectiveContent.StrongContextualFelicity.noRequires ∧ tb.ole = Semantics.Presupposition.ProjectiveContent.ObligatoryLocalEffect.obligatory) ∧ (isClassD tb ↔ tb.scf = Semantics.Presupposition.ProjectiveContent.StrongContextualFelicity.requires ∧ tb.ole = Semantics.Presupposition.ProjectiveContent.ObligatoryLocalEffect.notObligatory)

SCF-OLE correspondence with Tonhauser classes.

theorem TonhauserEtAl2013.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.

theorem TonhauserEtAl2013.stop_is_classC :

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

theorem TonhauserEtAl2013.expressive_is_classB :

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

theorem TonhauserEtAl2013.pronoun_is_classA :

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

theorem TonhauserEtAl2013.demonstrative_is_classD :

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

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

(∀ (c : 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 : Semantics.Presupposition.ProjectiveContent.ProjectiveClass), c = Semantics.Presupposition.ProjectiveContent.classFromProperties c.scf c.ole) ∧ Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classA ≠ Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classB ∧ Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classA ≠ Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classC ∧ Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classA ≠ Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classD ∧ Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classB ≠ Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classC ∧ Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classB ≠ Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classD ∧ Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classC ≠ Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classD

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

theorem TonhauserEtAl2013.stop_allows_informativity :

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

theorem TonhauserEtAl2013.stop_shifts_under_belief :

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

theorem TonhauserEtAl2013.expressive_allows_informativity :

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

theorem TonhauserEtAl2013.expressive_stays_with_speaker :

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

theorem TonhauserEtAl2013.pronoun_requires_antecedent :

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

theorem TonhauserEtAl2013.pronoun_shifts_under_belief :

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

inductive TonhauserEtAl2013.TraditionalCategory :

Traditional labels for projective content, predating the SCF/OLE taxonomy.

presupposition : TraditionalCategory
Traditional "presupposition".
conventionalImplicature : TraditionalCategory
Potts-style "conventional implicature".
supplementary : TraditionalCategory
Supplementary/parenthetical content.

Instances For

@[implicit_reducible]

instance TonhauserEtAl2013.instDecidableEqTraditionalCategory :

DecidableEq TraditionalCategory

Equations

TonhauserEtAl2013.instDecidableEqTraditionalCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance TonhauserEtAl2013.instReprTraditionalCategory :

Repr TraditionalCategory

Equations

TonhauserEtAl2013.instReprTraditionalCategory = { reprPrec := TonhauserEtAl2013.instReprTraditionalCategory.repr }

def TonhauserEtAl2013.instReprTraditionalCategory.repr :

TraditionalCategory → ℕ → Std.Format

Equations

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

Instances For

def TonhauserEtAl2013.traditionalCategory :

Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger → TraditionalCategory

The traditional category conventionally assigned to each trigger. [TBRS13] argue this classification is inadequate: the SCF × OLE taxonomy cross-cuts it (traditional_crosscuts_classes).

Equations

Instances For

theorem TonhauserEtAl2013.traditional_crosscuts_classes :

traditionalCategory Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.pronoun_existence = traditionalCategory Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.stop_prestate ∧ Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.pronoun_existence.toClass ≠ Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.stop_prestate.toClass

Traditional categories don't carve at the joints: pronouns and stop are both traditional "presuppositions" yet land in different projective classes (A vs C).