Presupposition Trigger Typology

@cite{wang-2025}

Cross-linguistic typology of presupposition triggers, classifying triggers by what non-presuppositional alternative they have. The classification follows @cite{wang-2025} Table 4.1 and is consumed by:

• Phenomena/Presupposition/Studies/Wang2025.lean — IC ≫ FP ≫ MP constraint-based competition analysis
• Fragments/Mandarin/Particles.lean — Mandarin trigger entries

Classification

Three patterns of trigger ↔ alternative relationship:

1. Deletion alternatives — trigger can be deleted (ye/also → ∅)
2. Replacement alternatives — specific lexical replacement (zhidao/know → believe)
3. No structural alternative — no available alternative (jiu/only)

The alternative-structure axis predicts obligatoriness:

• Deletion / replacement → trigger can be optional or obligatory
• No alternative → trigger is mandatorily omitted under partial CG support

Relation to MP infrastructure

This file provides the typology; the constraint-based formulation of Maximize Presupposition lives in MaximizePresupposition.lean, and the paper-specific IC/FP/MP ranking in Phenomena/Presupposition/Studies/Wang2025.lean.

inductive Semantics.Presupposition.TriggerTypology.PresupTrigger : Type

Types of presupposition triggers in natural language.

Each trigger type introduces a characteristic presupposition pattern. These are used for alternative generation in SI computation.

• definite : PresupTrigger

  Definite descriptions: "the X" presupposes X exists and is unique

• factive : PresupTrigger

  Factive predicates: "know/regret that P" presupposes P

• changeOfState : PresupTrigger

  Change-of-state predicates: "stop/start V-ing" presupposes prior state

• iterative : PresupTrigger

  Repetitive iteratives: "again" presuppose prior occurrence followed by an interruption (P-then-¬P-then-P-again). English again, German wieder, Mandarin you 又, Cantonese jau.

• continuative : PresupTrigger

  Continuatives: "still" presuppose uninterrupted continuation of P throughout an interval up to and including the reference time. Distinct from .iterative (which presupposes P-¬P-P) and from .changeOfState (which involves a polarity flip). English still, Mandarin reng 仍 / hai 还, Cantonese zung 仲. Cf. Ippolito 2007 on still vs again.

• cleft : PresupTrigger

  Cleft constructions: "It was X that..." presupposes existence

• aspectual : PresupTrigger

  Aspectual predicates: "finish", "continue" presuppose event structure

@[implicit_reducible]

instance Semantics.Presupposition.TriggerTypology.instDecidableEqPresupTrigger : DecidableEq PresupTrigger

Equations

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

def Semantics.Presupposition.TriggerTypology.instReprPresupTrigger.repr : PresupTrigger → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Presupposition.TriggerTypology.instReprPresupTrigger : Repr PresupTrigger

Equations

• Semantics.Presupposition.TriggerTypology.instReprPresupTrigger = { reprPrec := Semantics.Presupposition.TriggerTypology.instReprPresupTrigger.repr }

structure Semantics.Presupposition.TriggerTypology.TriggerOccurrence : Type

A presupposition trigger occurrence in a sentence.

Records the position and type of trigger, enabling compositional presupposition computation and alternative generation.

• position : ℕ

  Word position in the sentence

• trigger : PresupTrigger

  Type of trigger

def Semantics.Presupposition.TriggerTypology.instReprTriggerOccurrence.repr : TriggerOccurrence → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Presupposition.TriggerTypology.instReprTriggerOccurrence : Repr TriggerOccurrence

Equations

• Semantics.Presupposition.TriggerTypology.instReprTriggerOccurrence = { reprPrec := Semantics.Presupposition.TriggerTypology.instReprTriggerOccurrence.repr }

structure Semantics.Presupposition.TriggerTypology.PresupDerivation (W : Type u_1) : Type u_1

A derivation extended with presupposition tracking.

Tracks presuppositions through the derivation, enabling:

• Presupposition projection computation
• Interaction between presuppositions and SIs

• meaning : Core.Presupposition.PrProp W

  The underlying presuppositional proposition

• triggers : List TriggerOccurrence

  Presupposition triggers in the sentence

• polarity : Core.NaturalLogic.ContextPolarity

  Current polarity context

• surface : List String

  Surface form (optional, for display)

structure Semantics.Presupposition.TriggerTypology.ExhWithPresup (W : Type u_1) : Type u_1

Exhaustification may strengthen presuppositions.

When alternatives to a sentence have presuppositions, exhaustification (negating those alternatives) can introduce additional presuppositions.

This is a structural observation; detailed computation would require integrating with the Exhaustivity module.

• base : Core.Presupposition.PrProp W

  The base sentence

• alternatives : List (Core.Presupposition.PrProp W)

  Alternatives with their presuppositions

• exhaustified : Core.Presupposition.PrProp W

  The exhaustified meaning

inductive Semantics.Presupposition.TriggerTypology.AltStructure : Type

@cite{wang-2025} Table 4.1: How a presupposition trigger relates to its non-presuppositional alternative.

• deletion : AltStructure

  Alternative is obtained by deleting the trigger (ye/also → ∅, you/again → ∅)

• replacement : AltStructure

  Alternative is a specific lexical replacement (zhidao/know → believe)

• none : AltStructure

  No structural alternative available (jiu/only)

@[implicit_reducible]

instance Semantics.Presupposition.TriggerTypology.instDecidableEqAltStructure : DecidableEq AltStructure

Equations

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

@[implicit_reducible]

instance Semantics.Presupposition.TriggerTypology.instReprAltStructure : Repr AltStructure

Equations

• Semantics.Presupposition.TriggerTypology.instReprAltStructure = { reprPrec := Semantics.Presupposition.TriggerTypology.instReprAltStructure.repr }

def Semantics.Presupposition.TriggerTypology.instReprAltStructure.repr : AltStructure → ℕ → Std.Format

Equations

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

inductive Semantics.Presupposition.TriggerTypology.Obligatoriness : Type

Obligatoriness pattern predicted by the alternative-structure typology.

@cite{wang-2025} derives three patterns from the interaction of trigger type, alternative structure, and constraint ranking:

1. Obligatory: trigger must be used when CG supports presupposition
2. Optional: trigger may or may not be used
3. Blocked: trigger must NOT be used (mandatorily omitted)

• obligatory : Obligatoriness

  Trigger is obligatory when presupposition is fully entailed by CG

• optional : Obligatoriness

  Trigger is optional (either form is acceptable)

• blocked : Obligatoriness

  Trigger is blocked (mandatorily omitted in this context)

@[implicit_reducible]

instance Semantics.Presupposition.TriggerTypology.instDecidableEqObligatoriness : DecidableEq Obligatoriness

Equations

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

def Semantics.Presupposition.TriggerTypology.instReprObligatoriness.repr : Obligatoriness → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Presupposition.TriggerTypology.instReprObligatoriness : Repr Obligatoriness

Equations

• Semantics.Presupposition.TriggerTypology.instReprObligatoriness = { reprPrec := Semantics.Presupposition.TriggerTypology.instReprObligatoriness.repr }

structure Semantics.Presupposition.TriggerTypology.PresupTriggerEntry : Type

A presupposition trigger entry with @cite{wang-2025} alternative structure.

Extends the basic trigger type with information about what non-presuppositional alternative exists, enabling the constraint-based competition analysis.

• trigger : PresupTrigger

  The trigger type (from existing classification)

• altStructure : AltStructure

  Alternative structure (Wang Table 4.1)

• altForm : Option String

  Lexical form of the alternative (if replacement)

def Semantics.Presupposition.TriggerTypology.instReprPresupTriggerEntry.repr : PresupTriggerEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Presupposition.TriggerTypology.instReprPresupTriggerEntry : Repr PresupTriggerEntry

Equations

• Semantics.Presupposition.TriggerTypology.instReprPresupTriggerEntry = { reprPrec := Semantics.Presupposition.TriggerTypology.instReprPresupTriggerEntry.repr }

def Semantics.Presupposition.TriggerTypology.PresupTrigger.defaultAltStructure : PresupTrigger → AltStructure

Assign alternative structure to standard trigger types.

Default mapping based on cross-linguistic generalizations. Language-specific entries may override (see Fragments/Mandarin/).

Equations

• Semantics.Presupposition.TriggerTypology.PresupTrigger.definite.defaultAltStructure = Semantics.Presupposition.TriggerTypology.AltStructure.replacement
• Semantics.Presupposition.TriggerTypology.PresupTrigger.factive.defaultAltStructure = Semantics.Presupposition.TriggerTypology.AltStructure.replacement
• Semantics.Presupposition.TriggerTypology.PresupTrigger.changeOfState.defaultAltStructure = Semantics.Presupposition.TriggerTypology.AltStructure.replacement
• Semantics.Presupposition.TriggerTypology.PresupTrigger.iterative.defaultAltStructure = Semantics.Presupposition.TriggerTypology.AltStructure.deletion
• Semantics.Presupposition.TriggerTypology.PresupTrigger.continuative.defaultAltStructure = Semantics.Presupposition.TriggerTypology.AltStructure.deletion
• Semantics.Presupposition.TriggerTypology.PresupTrigger.cleft.defaultAltStructure = Semantics.Presupposition.TriggerTypology.AltStructure.none
• Semantics.Presupposition.TriggerTypology.PresupTrigger.aspectual.defaultAltStructure = Semantics.Presupposition.TriggerTypology.AltStructure.replacement