[Wan25a] Presupposition, Competition, and Coherence

[Hei91] [Kat07] [Wan25a] [Wan25b]

Self-contained study of [Wan25a] "Presupposition, Competition, and Coherence": both the experimental data (three experiments on Mandarin presupposition triggers) and the constraint-based formalization (IC ≫ FP ≫ MP) that derives Wang's three-way obligatoriness pattern.

Experimental Data

Experiment 1: Naturalness Judgments (9 triggers × 3 contexts)

9 Mandarin presupposition triggers tested in 3 context conditions:

• Full: CommonGround fully entails the presupposition
• Partial: CommonGround partially entails the presupposition
• None: CommonGround does not support the presupposition

Experiment 2: Polarity-Reversed Alternatives (4 triggers × 3 contexts)

4 triggers with polarity-reversed non-presuppositional alternatives: tests whether alternative structure affects felicity.

Experiment 3: De Re Judgments

Presuppositional triggers under attitude verbs: tests whether presuppositions can be resolved de re (against CommonGround) vs. de dicto (against attitude holder's beliefs).

Constraint-based Formalization

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): CommonGround entails S_p's presupposition. Violable — partial CommonGround support may be tolerated.
3. MP (Maximize Presupposition): prefer S_p over S when CommonGround supports the presupposition and S_p is more informative. Violable — overridable by IC or FP violations.

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

• Obligatory triggers (ye, you, reng): deletion alternatives — MP forces use of the trigger when CommonGround fully supports presupposition.
• Optional triggers (buzai, kaishi): replacement alternatives — competitor is informative enough that MP doesn't strongly prefer the trigger.
• Blocked triggers (jiu, zhidao under partial CommonGround): 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

inductive Wang2025.ContextCondition : Type

Context condition for presupposition support.

• full : ContextCondition
• partialSupport : ContextCondition
• noSupport : ContextCondition

@[implicit_reducible]

instance Wang2025.instDecidableEqContextCondition : DecidableEq ContextCondition

Equations

• Wang2025.instDecidableEqContextCondition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Wang2025.instReprContextCondition.repr : ContextCondition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Wang2025.instReprContextCondition : Repr ContextCondition

Equations

• Wang2025.instReprContextCondition = { reprPrec := Wang2025.instReprContextCondition.repr }

structure Wang2025.Exp1Datum : Type

A single naturalness judgment datum (Experiment 1).

• trigger : Mandarin.Particles.MandarinTrigger
• context : ContextCondition
• meanRating : ℚ

  Mean naturalness rating (1-7 Likert scale, ×10 for rational representation)

• felicity : Features.Acceptability

  Observed felicity judgment, encoded as a standard acceptability diacritic (Features.Acceptability): .ok = felicitous, .marginal = borderline ?, .anomalous = pragmatically odd #.

def Wang2025.instReprExp1Datum.repr : Exp1Datum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Wang2025.instReprExp1Datum : Repr Exp1Datum

Equations

• Wang2025.instReprExp1Datum = { reprPrec := Wang2025.instReprExp1Datum.repr }

def Wang2025.ye_full : Exp1Datum

Experiment 1 key finding: ye/also is felicitous under full and partial CommonGround.

Equations

• Wang2025.ye_full = { trigger := Mandarin.Particles.MandarinTrigger.ye, context := Wang2025.ContextCondition.full, meanRating := 62 / 10, felicity := Features.Acceptability.ok }

def Wang2025.ye_partial : Exp1Datum

Equations

• Wang2025.ye_partial = { trigger := Mandarin.Particles.MandarinTrigger.ye, context := Wang2025.ContextCondition.partialSupport, meanRating := 51 / 10, felicity := Features.Acceptability.ok }

def Wang2025.ye_none : Exp1Datum

Equations

• Wang2025.ye_none = { trigger := Mandarin.Particles.MandarinTrigger.ye, context := Wang2025.ContextCondition.noSupport, meanRating := 28 / 10, felicity := Features.Acceptability.anomalous }

def Wang2025.you_full : Exp1Datum

Experiment 1 key finding: you/again is felicitous under full and partial CommonGround.

Equations

• Wang2025.you_full = { trigger := Mandarin.Particles.MandarinTrigger.you, context := Wang2025.ContextCondition.full, meanRating := 6, felicity := Features.Acceptability.ok }

def Wang2025.you_partial : Exp1Datum

Equations

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

def Wang2025.you_none : Exp1Datum

Equations

• Wang2025.you_none = { trigger := Mandarin.Particles.MandarinTrigger.you, context := Wang2025.ContextCondition.noSupport, meanRating := 25 / 10, felicity := Features.Acceptability.anomalous }

def Wang2025.jiu_full : Exp1Datum

Experiment 1 key finding: jiu/only is blocked under partial CommonGround.

Equations

• Wang2025.jiu_full = { trigger := Mandarin.Particles.MandarinTrigger.jiu, context := Wang2025.ContextCondition.full, meanRating := 58 / 10, felicity := Features.Acceptability.ok }

def Wang2025.jiu_partial : Exp1Datum

Equations

• Wang2025.jiu_partial = { trigger := Mandarin.Particles.MandarinTrigger.jiu, context := Wang2025.ContextCondition.partialSupport, meanRating := 3, felicity := Features.Acceptability.anomalous }

def Wang2025.jiu_none : Exp1Datum

Equations

• Wang2025.jiu_none = { trigger := Mandarin.Particles.MandarinTrigger.jiu, context := Wang2025.ContextCondition.noSupport, meanRating := 22 / 10, felicity := Features.Acceptability.anomalous }

def Wang2025.zhidao_full : Exp1Datum

Experiment 1 key finding: zhidao/know is blocked under partial CommonGround.

Equations

• Wang2025.zhidao_full = { trigger := Mandarin.Particles.MandarinTrigger.zhidao, context := Wang2025.ContextCondition.full, meanRating := 59 / 10, felicity := Features.Acceptability.ok }

def Wang2025.zhidao_partial : Exp1Datum

Equations

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

def Wang2025.zhidao_none : Exp1Datum

Equations

• Wang2025.zhidao_none = { trigger := Mandarin.Particles.MandarinTrigger.zhidao, context := Wang2025.ContextCondition.noSupport, meanRating := 2, felicity := Features.Acceptability.anomalous }

theorem Wang2025.ye_jiu_partial_diverge : ye_partial.felicity ≠ jiu_partial.felicity

Key contrast: ye and jiu diverge under partial CommonGround support.

theorem Wang2025.obligatory_trigger_pattern : ye_full.felicity = Features.Acceptability.ok ∧ ye_partial.felicity = Features.Acceptability.ok ∧ ye_none.felicity = Features.Acceptability.anomalous

Obligatory triggers are felicitous under both full and partial CommonGround.

theorem Wang2025.blocked_trigger_pattern : jiu_full.felicity = Features.Acceptability.ok ∧ jiu_partial.felicity = Features.Acceptability.anomalous ∧ jiu_none.felicity = Features.Acceptability.anomalous

Blocked triggers are only felicitous under full CommonGround.

inductive Wang2025.Resolution : Type

Resolution locus for presupposition under attitude verbs.

• deRe : Resolution

  Presupposition resolved against CommonGround (de re)

• deDicto : Resolution

  Presupposition resolved against attitude holder's beliefs (de dicto)

@[implicit_reducible]

instance Wang2025.instDecidableEqResolution : DecidableEq Resolution

Equations

• Wang2025.instDecidableEqResolution x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Wang2025.instReprResolution.repr : Resolution → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Wang2025.instReprResolution.repr Wang2025.Resolution.deRe prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Wang2025.Resolution.deRe")).group prec✝

@[implicit_reducible]

instance Wang2025.instReprResolution : Repr Resolution

Equations

• Wang2025.instReprResolution = { reprPrec := Wang2025.instReprResolution.repr }

structure Wang2025.Exp3Datum : Type

A de re judgment datum (Experiment 3).

• trigger : Mandarin.Particles.MandarinTrigger
• resolution : Resolution
• accepted : Bool

  Whether this resolution was accepted by participants

def Wang2025.instReprExp3Datum.repr : Exp3Datum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Wang2025.instReprExp3Datum : Repr Exp3Datum

Equations

• Wang2025.instReprExp3Datum = { reprPrec := Wang2025.instReprExp3Datum.repr }

def Wang2025.ye_deRe : Exp3Datum

ye/also under attitude verb: de re reading available.

Equations

• Wang2025.ye_deRe = { trigger := Mandarin.Particles.MandarinTrigger.ye, resolution := Wang2025.Resolution.deRe, accepted := true }

def Wang2025.ye_deDicto : Exp3Datum

ye/also under attitude verb: de dicto reading also available.

Equations

• Wang2025.ye_deDicto = { trigger := Mandarin.Particles.MandarinTrigger.ye, resolution := Wang2025.Resolution.deDicto, accepted := true }

theorem Wang2025.additive_deRe_available : ye_deRe.accepted = true

Additive presupposition allows de re resolution.

@[reducible, inline]

abbrev Wang2025.BAccessRel (W : Type u_1) : Type u_1

Local Bool-valued accessibility used by Wang2025 for List.all evaluation of the speaker-K operator. The Prop-valued canonical version lives in Core.Logic.Modal.AccessRel; lift via fun a b => R a b = true to bridge.

Equations

• Wang2025.BAccessRel W = (W → W → Bool)

inductive Wang2025.PragConstraint : Type

[Wan25a] 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 CommonGround. 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: CommonGround entails presupposition (violable)

• MP : PragConstraint

  Maximize Presupposition: prefer presuppositional form (violable)

@[implicit_reducible]

instance Wang2025.instDecidableEqPragConstraint : DecidableEq PragConstraint

Equations

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

@[implicit_reducible]

instance Wang2025.instReprPragConstraint : Repr PragConstraint

Equations

• Wang2025.instReprPragConstraint = { reprPrec := Wang2025.instReprPragConstraint.repr }

def Wang2025.instReprPragConstraint.repr : PragConstraint → ℕ → Std.Format

Equations

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

def Wang2025.PragConstraint.isViolable : PragConstraint → Bool

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

Equations

• Wang2025.PragConstraint.IC.isViolable = false
• Wang2025.PragConstraint.FP.isViolable = true
• Wang2025.PragConstraint.MP.isViolable = true

def Wang2025.constraintRanking : List PragConstraint

The canonical constraint ranking: IC ≫ FP ≫ MP.

Equations

• Wang2025.constraintRanking = [Wang2025.PragConstraint.IC, Wang2025.PragConstraint.FP, Wang2025.PragConstraint.MP]

def Wang2025.satisfiesIC {W : Type u_1} (p : Semantics.Presupposition.PartialProp 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.

[Wan25a]: IC is NON-VIOLABLE.

Equations

• Wang2025.satisfiesIC p = ∃ (w : W), Semantics.Presupposition.PartialProp.holds w p

def Wang2025.satisfiesFP {W : Type u_1} (cg : CommonGround.ContextSet W) (p : Semantics.Presupposition.PartialProp W) : Prop

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

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

Equations

• Wang2025.satisfiesFP cg p = ∀ (w : W), cg w → Semantics.Presupposition.PartialProp.defined w p

def Wang2025.partialFP {W : Type u_1} (cg : CommonGround.ContextSet W) (p : Semantics.Presupposition.PartialProp W) : Prop

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

[Wan25a] Ch. 2-3: some triggers tolerate partial satisfaction (ye, you, reng) while others don't (jiu, zhidao).

Equations

• Wang2025.partialFP cg p = ((∃ (w : W), cg w ∧ Semantics.Presupposition.PartialProp.defined w p) ∧ ¬Wang2025.satisfiesFP cg p)

def Wang2025.mpPrefers {W : Type u_1} (cg : CommonGround.ContextSet W) (sp : Semantics.Presupposition.PartialProp W) : Prop

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

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

Equations

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

def Wang2025.predictObligatoriness (altStr : Semantics.Presupposition.TriggerTypology.AltStructure) (cgEntailsPresup cgPartialPresup : Bool) : Semantics.Presupposition.TriggerTypology.Obligatoriness

Predict obligatoriness from alternative structure and context.

[Wan25a] Ch. 4: The three-way prediction follows from constraint interaction.

Equations

• Wang2025.predictObligatoriness Semantics.Presupposition.TriggerTypology.AltStructure.deletion true cgPartialPresup = Semantics.Presupposition.TriggerTypology.Obligatoriness.obligatory
• Wang2025.predictObligatoriness Semantics.Presupposition.TriggerTypology.AltStructure.replacement true cgPartialPresup = Semantics.Presupposition.TriggerTypology.Obligatoriness.obligatory
• Wang2025.predictObligatoriness Semantics.Presupposition.TriggerTypology.AltStructure.none true cgPartialPresup = Semantics.Presupposition.TriggerTypology.Obligatoriness.obligatory
• Wang2025.predictObligatoriness Semantics.Presupposition.TriggerTypology.AltStructure.deletion false true = Semantics.Presupposition.TriggerTypology.Obligatoriness.optional
• Wang2025.predictObligatoriness Semantics.Presupposition.TriggerTypology.AltStructure.replacement false true = Semantics.Presupposition.TriggerTypology.Obligatoriness.optional
• Wang2025.predictObligatoriness Semantics.Presupposition.TriggerTypology.AltStructure.none false true = Semantics.Presupposition.TriggerTypology.Obligatoriness.blocked
• Wang2025.predictObligatoriness altStr false false = Semantics.Presupposition.TriggerTypology.Obligatoriness.blocked

theorem Wang2025.deletion_alt_partial_resolution : predictObligatoriness Semantics.Presupposition.TriggerTypology.AltStructure.deletion false true = Semantics.Presupposition.TriggerTypology.Obligatoriness.optional

Triggers with deletion alternatives remain felicitous under partial CommonGround.

[Wan25a] Ch. 4: ye/also, you/again, reng/still have deletion alternatives, so even when the CommonGround only partially entails the presupposition, the presuppositional form is not blocked.

theorem Wang2025.no_alt_blocked_partial : predictObligatoriness Semantics.Presupposition.TriggerTypology.AltStructure.none false true = Semantics.Presupposition.TriggerTypology.Obligatoriness.blocked

Triggers with no structural alternative are blocked under partial CommonGround.

[Wan25a] Ch. 4: jiu/only has no non-presuppositional alternative, so when the CommonGround doesn't fully support the presupposition, the presuppositional form cannot be used.

theorem Wang2025.full_cg_obligatory (alt : Semantics.Presupposition.TriggerTypology.AltStructure) (b : Bool) : predictObligatoriness alt true b = Semantics.Presupposition.TriggerTypology.Obligatoriness.obligatory

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

theorem Wang2025.no_cg_blocks (alt : Semantics.Presupposition.TriggerTypology.AltStructure) : predictObligatoriness alt false false = Semantics.Presupposition.TriggerTypology.Obligatoriness.blocked

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

def Wang2025.icNecessary {W : Type u_1} (p : Semantics.Presupposition.PartialProp W) (h : satisfiesIC p) : ∃ (w : W), Semantics.Presupposition.PartialProp.holds w p

IC satisfaction is necessary for felicity.

Equations

• ⋯ = h

noncomputable def Wang2025.speakerK {W : Type u_1} [Fintype W] (R : BAccessRel W) (φ : W → Bool) : W → Bool

The epistemic K operator: speaker believes φ.

[Wan25a] 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 a local Bool-valued accessibility relation; for the Prop-valued canonical Kripke semantics see Intensional.box.

Equations

• Wang2025.speakerK R φ w = (List.filter (R w) Finset.univ.toList).all φ

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

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

• sentence : Semantics.Presupposition.PartialProp W

  The presuppositional sentence

• altStructure : Semantics.Presupposition.TriggerTypology.AltStructure

  The trigger's alternative structure

• cgFull : Bool

  Whether CommonGround fully entails the presupposition

• cgPartial : Bool

  Whether CommonGround partially entails the presupposition

• ic : Bool

  Whether the sentence is internally coherent

def Wang2025.wangCheck {W : Type u_1} (input : WangInput W) : Features.Acceptability

[Wan25a] felicity check: evaluates constraint satisfaction.

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

Equations

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

theorem Wang2025.IC_violation_always_blocks {W : Type u_1} (input : WangInput W) (hIC : input.ic = false) : wangCheck input = Features.Acceptability.anomalous

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

[Wan25a]: IC is the only non-violable constraint. A sentence whose presupposition contradicts its assertion is always infelicitous, no matter what the CommonGround says or what alternatives exist.

theorem Wang2025.ciLift_felicitous_when_fp_holds {W : Type u_1} (presup assertion cg : W → Prop) (hfp : ∀ (w : W), cg w → presup w) (w : W) : cg w → (Pragmatics.Expressives.ciLift presup assertion).ci w

When CommonGround entails the presupposition, the CI-lifted form yields a felicitous two-dimensional meaning where the CI content (presupposition) is satisfied at all CommonGround worlds.

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