Alternative Competition for Presupposition Triggers

@cite{heim-1991} @cite{katzir-2007} @cite{wang-2025}

Constraint-based evaluation of presuppositional vs. non-presuppositional alternatives, following @cite{wang-2025} "Presupposition, Competition, and Coherence" Ch. 4.

Framework

Presuppositional sentences S_p compete with non-presuppositional alternatives S under three ranked pragmatic constraints:

1. IC (Internal Coherence): S_p's presupposition is consistent with its assertion. Non-violable — IC violation always blocks the presuppositional form.

2. FP (Felicity Presupposition): CG entails S_p's presupposition. Violable — partial CG support may be tolerated.

3. MP (Maximize Presupposition): Prefer S_p over S when CG supports the presupposition and S_p is more informative. Violable — can be overridden by IC or FP violations.

Key Predictions

The constraint ranking IC >> FP >> MP, together with the trigger's alternative structure (Table 4.1), derives three obligatoriness patterns:

1. Obligatory triggers (ye, you, reng): deletion alternatives — MP forces use of trigger when CG fully supports presupposition.
2. Optional triggers (buzai, kaishi): replacement alternatives — competitor is informative enough that MP doesn't strongly prefer the trigger.
3. Blocked triggers (jiu, zhidao under partial CG): no alternative or replacement with stronger assertion — FP violation blocks the trigger.

K Operator Interaction

The epistemic operator K (speaker's beliefs) interacts with exhaustification:

• K >> exh_mx: preferred for atomic sentences (speaker-oriented reading)
• exh_mx >> K: possible for complex sentences

def Implicature.Constraints.Wang2025.satisfiesIC {W : Type u_1} (p : Core.Presupposition.PrProp W) : Prop

IC (Internal Coherence): the presupposition is consistent with the assertion.

S_p is internally coherent iff there exists a world where both the presupposition and the assertion hold. IC violation means the presupposition contradicts the assertion — the sentence is semantically defective.

@cite{wang-2025}: IC is NON-VIOLABLE.

Equations

• Implicature.Constraints.Wang2025.satisfiesIC p = ∃ (w : W), Core.Presupposition.PrProp.holds w p

def Implicature.Constraints.Wang2025.satisfiesFP {W : Type u_1} (cg : Core.CommonGround.ContextSet W) (p : Core.Presupposition.PrProp W) : Prop

FP (Felicity Presupposition): the common ground entails the presupposition.

Standard Stalnakerian presupposition satisfaction. When the CG only partially entails the presupposition, FP is violated but may be tolerated.

Equations

• Implicature.Constraints.Wang2025.satisfiesFP cg p = ∀ (w : W), cg w → Core.Presupposition.PrProp.defined w p

def Implicature.Constraints.Wang2025.partialFP {W : Type u_1} (cg : Core.CommonGround.ContextSet W) (p : Core.Presupposition.PrProp W) : Prop

Partial FP satisfaction: the presupposition is compatible with the CG but not fully entailed.

@cite{wang-2025} Ch. 2-3: some triggers tolerate partial satisfaction (ye, you, reng) while others don't (jiu, zhidao).

Equations

• Implicature.Constraints.Wang2025.partialFP cg p = ((∃ (w : W), cg w ∧ Core.Presupposition.PrProp.defined w p) ∧ ¬Implicature.Constraints.Wang2025.satisfiesFP cg p)

def Implicature.Constraints.Wang2025.mpPrefers {W : Type u_1} (cg : Core.CommonGround.ContextSet W) (sp : Core.Presupposition.PrProp W) : Prop

MP (Maximize Presupposition): prefer S_p over S when the presuppositional form is more informative and the CG supports its presupposition.

MP is violated when the non-presuppositional alternative S is used despite the CG supporting S_p's presupposition.

Equations

• Implicature.Constraints.Wang2025.mpPrefers cg sp = (Implicature.Constraints.Wang2025.satisfiesFP cg sp ∧ Implicature.Constraints.Wang2025.satisfiesIC sp)

def Implicature.Constraints.Wang2025.predictObligatoriness (altStr : Presuppositions.AltStructure) (cgEntailsPresup cgPartialPresup : Bool) : Presuppositions.Obligatoriness

Predict obligatoriness from alternative structure and context.

@cite{wang-2025} Ch. 4: The three-way prediction follows from constraint interaction.

Equations

• Implicature.Constraints.Wang2025.predictObligatoriness Implicature.Presuppositions.AltStructure.deletion true cgPartialPresup = Implicature.Presuppositions.Obligatoriness.obligatory
• Implicature.Constraints.Wang2025.predictObligatoriness Implicature.Presuppositions.AltStructure.replacement true cgPartialPresup = Implicature.Presuppositions.Obligatoriness.obligatory
• Implicature.Constraints.Wang2025.predictObligatoriness Implicature.Presuppositions.AltStructure.none true cgPartialPresup = Implicature.Presuppositions.Obligatoriness.obligatory
• Implicature.Constraints.Wang2025.predictObligatoriness Implicature.Presuppositions.AltStructure.deletion false true = Implicature.Presuppositions.Obligatoriness.optional
• Implicature.Constraints.Wang2025.predictObligatoriness Implicature.Presuppositions.AltStructure.replacement false true = Implicature.Presuppositions.Obligatoriness.optional
• Implicature.Constraints.Wang2025.predictObligatoriness Implicature.Presuppositions.AltStructure.none false true = Implicature.Presuppositions.Obligatoriness.blocked
• Implicature.Constraints.Wang2025.predictObligatoriness altStr false false = Implicature.Presuppositions.Obligatoriness.blocked

theorem Implicature.Constraints.Wang2025.deletion_alt_partial_resolution : predictObligatoriness Presuppositions.AltStructure.deletion false true = Presuppositions.Obligatoriness.optional

Triggers with deletion alternatives remain felicitous under partial CG.

@cite{wang-2025} Ch. 4: ye/also, you/again, reng/still have deletion alternatives, so even when the CG only partially entails the presupposition, the presuppositional form is not blocked.

theorem Implicature.Constraints.Wang2025.no_alt_blocked_partial : predictObligatoriness Presuppositions.AltStructure.none false true = Presuppositions.Obligatoriness.blocked

Triggers with no structural alternative are blocked under partial CG.

@cite{wang-2025} Ch. 4: jiu/only has no non-presuppositional alternative, so when the CG doesn't fully support the presupposition, the presuppositional form cannot be used.

theorem Implicature.Constraints.Wang2025.full_cg_obligatory (alt : Presuppositions.AltStructure) (b : Bool) : predictObligatoriness alt true b = Presuppositions.Obligatoriness.obligatory

Full CG support always yields obligatoriness (for any alternative structure).

theorem Implicature.Constraints.Wang2025.no_cg_blocks (alt : Presuppositions.AltStructure) : predictObligatoriness alt false false = Presuppositions.Obligatoriness.blocked

No CG support always blocks (for any alternative structure).

def Implicature.Constraints.Wang2025.icNecessary {W : Type u_1} (p : Core.Presupposition.PrProp W) (h : satisfiesIC p) : ∃ (w : W), Core.Presupposition.PrProp.holds w p

IC satisfaction is necessary for felicity.

Equations

• ⋯ = h

def Implicature.Constraints.Wang2025.speakerK {W : Type u_1} [Core.Proposition.FiniteWorlds W] (R : Core.ModalLogic.AccessRel W) (φ : BProp W) : BProp W

The epistemic K operator: speaker believes φ.

@cite{wang-2025} Ch. 4: K is a covert doxastic operator marking the speaker's epistemic stance. It scopes relative to exh_mx:

• K >> exh_mx: preferred for atomic sentences
• exh_mx >> K: available for complex sentences

Uses the existing Kripke accessibility relation from Core.ModalLogic.

Equations

• Implicature.Constraints.Wang2025.speakerK R φ = Core.ModalLogic.kripkeEval R Core.Modality.ModalForce.necessity φ

structure Implicature.Constraints.Wang2025.WangInput (W : Type u_2) : Type u_2

Input for Wang's felicity prediction: a trigger entry in a context.

• sentence : Core.Presupposition.PrProp W

  The presuppositional sentence

• altStructure : Presuppositions.AltStructure

  The trigger's alternative structure

• cgFull : Bool

  Whether CG fully entails the presupposition

• cgPartial : Bool

  Whether CG partially entails the presupposition

• ic : Bool

  Whether the sentence is internally coherent

def Implicature.Constraints.Wang2025.wangCheck {W : Type u_1} (input : WangInput W) : Interfaces.FelicityResult

@cite{wang-2025} felicity check: evaluates constraint satisfaction.

IC violation → odd (non-violable). Otherwise, obligatoriness prediction from alternative structure and CG support determines the status.

Equations

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

theorem Implicature.Constraints.Wang2025.IC_violation_always_blocks {W : Type u_1} (input : WangInput W) (hIC : input.ic = false) : (wangCheck input).status = Interfaces.FelicityStatus.odd

IC violation always yields oddness, regardless of CG support and alternative structure.

@cite{wang-2025}: IC is the only non-violable constraint. A sentence whose presupposition contradicts its assertion is always infelicitous, no matter what the CG says or what alternatives exist.

theorem Implicature.Constraints.Wang2025.ciLift_felicitous_when_fp_holds {W : Type u_1} (p : Core.Presupposition.PrProp W) (cg : Core.CommonGround.ContextSet W) (hfp : satisfiesFP cg p) (w : W) : cg w → (Semantics.Lexical.Expressives.ciLift p).ci w = true

When IC is satisfied and CG entails the presupposition, the CI-lifted form yields a felicitous two-dimensional meaning where:

• The at-issue content is evaluable (assertion)
• The CI content (presupposition) is satisfied at all CG worlds

This connects the constraint-based analysis to the CI bifurcation approach for de re presupposition.