inductive Implicature.Presuppositions.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

  Iteratives: "again", "still" presuppose prior occurrence

• cleft : PresupTrigger

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

• aspectual : PresupTrigger

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

instance Implicature.Presuppositions.instDecidableEqPresupTrigger : DecidableEq PresupTrigger

Equations

• Implicature.Presuppositions.instDecidableEqPresupTrigger x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Implicature.Presuppositions.instReprPresupTrigger.repr : PresupTrigger → ℕ → Std.Format

Equations

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

instance Implicature.Presuppositions.instReprPresupTrigger : Repr PresupTrigger

Equations

• Implicature.Presuppositions.instReprPresupTrigger = { reprPrec := Implicature.Presuppositions.instReprPresupTrigger.repr }

structure Implicature.Presuppositions.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

instance Implicature.Presuppositions.instReprTriggerOccurrence : Repr TriggerOccurrence

Equations

• Implicature.Presuppositions.instReprTriggerOccurrence = { reprPrec := Implicature.Presuppositions.instReprTriggerOccurrence.repr }

def Implicature.Presuppositions.instReprTriggerOccurrence.repr : TriggerOccurrence → ℕ → Std.Format

Equations

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

structure Implicature.Presuppositions.PresupDerivation (W : Type u_1) : Type u_1

A derivation extended with presupposition tracking.

This extends the basic Implicature infrastructure to track 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 Implicature.Presuppositions.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

Alternative Structure for Presupposition Triggers

@cite{wang-2025} Table 4.1 classifies presuppositional triggers by what non-presuppositional alternative they have. This determines their behavior under the IC >> FP >> MP constraint ranking.

Three patterns:

1. Deletion alternatives: trigger can be deleted (ye/also → ∅, you/again → ∅)
2. Replacement alternatives: trigger has a specific lexical alternative (zhidao/know → believe, buzai/no-longer → not)
3. No structural alternative: no available alternative (jiu/only → ∅)

This classification predicts obligatoriness:

• Deletion/replacement alternatives → trigger can be optional or obligatory
• No alternative → trigger is mandatorily omitted when presupposition only partially holds

inductive Implicature.Presuppositions.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)

instance Implicature.Presuppositions.instDecidableEqAltStructure : DecidableEq AltStructure

Equations

• Implicature.Presuppositions.instDecidableEqAltStructure x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Implicature.Presuppositions.instReprAltStructure : Repr AltStructure

Equations

• Implicature.Presuppositions.instReprAltStructure = { reprPrec := Implicature.Presuppositions.instReprAltStructure.repr }

def Implicature.Presuppositions.instReprAltStructure.repr : AltStructure → ℕ → Std.Format

Equations

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

instance Implicature.Presuppositions.instBEqAltStructure : BEq AltStructure

Equations

• Implicature.Presuppositions.instBEqAltStructure = { beq := Implicature.Presuppositions.instBEqAltStructure.beq }

def Implicature.Presuppositions.instBEqAltStructure.beq : AltStructure → AltStructure → Bool

Equations

• Implicature.Presuppositions.instBEqAltStructure.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Implicature.Presuppositions.PragConstraint : Type

@cite{wang-2025} pragmatic constraint ranking: IC >> FP >> MP.

• IC (Internal Coherence): S_p's presupposition is consistent with its assertion. Non-violable.
• FP (Felicity Presupposition): S_p's presupposition is entailed by the CG. Violable but ranked above MP.
• MP (Maximize Presupposition): Prefer the presuppositional S_p over its non-presuppositional alternative S when context supports it. Violable.

• IC : PragConstraint

  Internal Coherence: presupposition consistent with assertion (non-violable)

• FP : PragConstraint

  Felicity Presupposition: CG entails presupposition (violable)

• MP : PragConstraint

  Maximize Presupposition: prefer presuppositional form (violable)

instance Implicature.Presuppositions.instDecidableEqPragConstraint : DecidableEq PragConstraint

Equations

• Implicature.Presuppositions.instDecidableEqPragConstraint x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Implicature.Presuppositions.instReprPragConstraint.repr : PragConstraint → ℕ → Std.Format

Equations

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

instance Implicature.Presuppositions.instReprPragConstraint : Repr PragConstraint

Equations

• Implicature.Presuppositions.instReprPragConstraint = { reprPrec := Implicature.Presuppositions.instReprPragConstraint.repr }

instance Implicature.Presuppositions.instBEqPragConstraint : BEq PragConstraint

Equations

• Implicature.Presuppositions.instBEqPragConstraint = { beq := Implicature.Presuppositions.instBEqPragConstraint.beq }

def Implicature.Presuppositions.instBEqPragConstraint.beq : PragConstraint → PragConstraint → Bool

Equations

• Implicature.Presuppositions.instBEqPragConstraint.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Implicature.Presuppositions.PragConstraint.isViolable : PragConstraint → Bool

IC is non-violable; FP and MP are violable.

Equations

• Implicature.Presuppositions.PragConstraint.IC.isViolable = false
• Implicature.Presuppositions.PragConstraint.FP.isViolable = true
• Implicature.Presuppositions.PragConstraint.MP.isViolable = true

def Implicature.Presuppositions.constraintRanking : List PragConstraint

The canonical constraint ranking: IC >> FP >> MP.

Equations

• Implicature.Presuppositions.constraintRanking = [Implicature.Presuppositions.PragConstraint.IC, Implicature.Presuppositions.PragConstraint.FP, Implicature.Presuppositions.PragConstraint.MP]

inductive Implicature.Presuppositions.Obligatoriness : Type

Obligatoriness pattern predicted by the alternative competition framework.

@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)

instance Implicature.Presuppositions.instDecidableEqObligatoriness : DecidableEq Obligatoriness

Equations

• Implicature.Presuppositions.instDecidableEqObligatoriness x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Implicature.Presuppositions.instReprObligatoriness : Repr Obligatoriness

Equations

• Implicature.Presuppositions.instReprObligatoriness = { reprPrec := Implicature.Presuppositions.instReprObligatoriness.repr }

def Implicature.Presuppositions.instReprObligatoriness.repr : Obligatoriness → ℕ → Std.Format

Equations

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

instance Implicature.Presuppositions.instBEqObligatoriness : BEq Obligatoriness

Equations

• Implicature.Presuppositions.instBEqObligatoriness = { beq := Implicature.Presuppositions.instBEqObligatoriness.beq }

def Implicature.Presuppositions.instBEqObligatoriness.beq : Obligatoriness → Obligatoriness → Bool

Equations

• Implicature.Presuppositions.instBEqObligatoriness.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Implicature.Presuppositions.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)

instance Implicature.Presuppositions.instReprPresupTriggerEntry : Repr PresupTriggerEntry

Equations

• Implicature.Presuppositions.instReprPresupTriggerEntry = { reprPrec := Implicature.Presuppositions.instReprPresupTriggerEntry.repr }

def Implicature.Presuppositions.instReprPresupTriggerEntry.repr : PresupTriggerEntry → ℕ → Std.Format

Equations

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

def Implicature.Presuppositions.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

• Implicature.Presuppositions.PresupTrigger.definite.defaultAltStructure = Implicature.Presuppositions.AltStructure.replacement
• Implicature.Presuppositions.PresupTrigger.factive.defaultAltStructure = Implicature.Presuppositions.AltStructure.replacement
• Implicature.Presuppositions.PresupTrigger.changeOfState.defaultAltStructure = Implicature.Presuppositions.AltStructure.replacement
• Implicature.Presuppositions.PresupTrigger.iterative.defaultAltStructure = Implicature.Presuppositions.AltStructure.deletion
• Implicature.Presuppositions.PresupTrigger.cleft.defaultAltStructure = Implicature.Presuppositions.AltStructure.none
• Implicature.Presuppositions.PresupTrigger.aspectual.defaultAltStructure = Implicature.Presuppositions.AltStructure.replacement