Presupposition triggers

A presupposition trigger is an expression whose use takes some proposition for granted. A trigger belongs to a class by the kind of expression that hosts it (TriggerClass), the consensus inventory of the projection literature after Zeevat and after Tonhauser, Beaver, Roberts and Simons. Abusch divides triggers into hard ones, whose presupposition always projects, and soft ones, whose presupposition can be suspended (Hardness). Karttunen divides the factive predicates into true factives and semi-factives (Factivity). A verb's entry records its factivity, and whether it is a trigger is derived (Verb.IsTrigger); an adverb, particle or affix that triggers a presupposition is a TriggerItem.

Implementation notes

What a predicate does with the presuppositions of its complement is not recorded on its entry. It follows from the predicate's semantics: a factive, an aspectual or an implicative passes them on unchanged, and an attitude verb makes its report presuppose that the holder believes them, as Karttunen and Heim argue.

References

• [Zee92]
• [TBRS13]
• [Abu10]
• [Kar71b]
• [Kar74a]
• [Hei92]
• [vS96]
• [Ipp07]
• [Kri09c]

inductive Presupposition.Hardness : Type

Whether a presupposition trigger is hard or soft, in the classification of [Abu10]. Hard triggers always project (too, again, also), and soft triggers project context-sensitively (stop, know).

• hard : Hardness

  A trigger whose presupposition projects in every context.

• soft : Hardness

  A trigger whose presupposition can be suspended in context.

@[instance_reducible]

instance Presupposition.instDecidableEqHardness : DecidableEq Hardness

Equations

• Presupposition.instDecidableEqHardness x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Presupposition.instReprHardness.repr : Hardness → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Presupposition.instReprHardness : Repr Hardness

Equations

• Presupposition.instReprHardness = { reprPrec := Presupposition.instReprHardness.repr }

inductive Presupposition.Factivity : Type

The factivity class of a predicate ([Kar71b]).

• full : Factivity

  A true factive such as regret or forget, whose complement follows even from the possibility of the sentence.

• semi : Factivity

  A semi-factive such as realize or discover, whose complement follows from the sentence and its negation only.

@[instance_reducible]

instance Presupposition.instDecidableEqFactivity : DecidableEq Factivity

Equations

• Presupposition.instDecidableEqFactivity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Presupposition.instReprFactivity.repr : Factivity → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Presupposition.instReprFactivity : Repr Factivity

Equations

• Presupposition.instReprFactivity = { reprPrec := Presupposition.instReprFactivity.repr }

inductive Presupposition.TriggerClass : Type

The class of a presupposition trigger, by the kind of expression that hosts it.

• definite : TriggerClass

  A definite description the X presupposes that a unique X exists.

• factive : TriggerClass

  A factive predicate, know or regret that p, presupposes p.

• changeOfState : TriggerClass

  A change-of-state expression, stop, start or no longer, presupposes the prior state.

• iterative : TriggerClass

  A repetitive iterative, again, presupposes a prior occurrence. An intervening interval without the eventuality is presupposed only for stative hosts, in competition with the continuative; eventive again (John won again) requires precedence only ([vS96]). Its meaning is Presupposition.again.

• continuative : TriggerClass

  A continuative, still, presupposes that the state has held without interruption up to the reference time ([Ipp07]).

• additive : TriggerClass

  An additive, too or also, presupposes that a distinct salient alternative satisfies the predicate, and is the paradigm anaphoric trigger ([Kri09c]).

• exclusive : TriggerClass

  An exclusive, only p, presupposes its prejacent p.

• contrastive : TriggerClass

  A contrastive, instead, presupposes that a salient alternative is false.

• cleft : TriggerClass

  A cleft it was X that ... presupposes existence.

• aspectual : TriggerClass

  An aspectual predicate, finish or continue, presupposes event structure.

@[instance_reducible]

instance Presupposition.instDecidableEqTriggerClass : DecidableEq TriggerClass

Equations

• Presupposition.instDecidableEqTriggerClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Presupposition.instReprTriggerClass.repr : TriggerClass → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Presupposition.instReprTriggerClass : Repr TriggerClass

Equations

• Presupposition.instReprTriggerClass = { reprPrec := Presupposition.instReprTriggerClass.repr }

structure Presupposition.TriggerItem : Type

A presupposition trigger outside the verbal lexicon, an adverb, particle or affix, with its trigger class. A verb's presuppositions are recorded on its Verb entry.

• form : String

  The citation form, a romanization where the language is not written in Latin script.

• script : Option String

  The native-script form of a romanized item.

• triggerClass : TriggerClass

  The trigger class.

def Presupposition.instDecidableEqTriggerItem.decEq (x✝ x✝¹ : TriggerItem) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Presupposition.instDecidableEqTriggerItem : DecidableEq TriggerItem

Equations

• Presupposition.instDecidableEqTriggerItem = Presupposition.instDecidableEqTriggerItem.decEq

@[instance_reducible]

instance Presupposition.instReprTriggerItem : Repr TriggerItem

Equations

• Presupposition.instReprTriggerItem = { reprPrec := Presupposition.instReprTriggerItem.repr }

def Presupposition.instReprTriggerItem.repr : TriggerItem → Nat → Std.Format

Equations

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