@cite{wang-2025} Presupposition, Competition, and Coherence

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

Self-contained study of @cite{wang-2025} "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: CG fully entails the presupposition
• Partial: CG partially entails the presupposition
• None: CG 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 CG) 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): 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 — 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 CG 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 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

inductive Phenomena.Presupposition.Studies.Wang2025.ContextCondition : Type

Context condition for presupposition support.

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

@[implicit_reducible]

instance Phenomena.Presupposition.Studies.Wang2025.instDecidableEqContextCondition : DecidableEq ContextCondition

Equations

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

def Phenomena.Presupposition.Studies.Wang2025.instReprContextCondition.repr : ContextCondition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Presupposition.Studies.Wang2025.instReprContextCondition : Repr ContextCondition

Equations

• Phenomena.Presupposition.Studies.Wang2025.instReprContextCondition = { reprPrec := Phenomena.Presupposition.Studies.Wang2025.instReprContextCondition.repr }

structure Phenomena.Presupposition.Studies.Wang2025.Exp1Datum : Type

A single naturalness judgment datum (Experiment 1).

• trigger : Fragments.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 Phenomena.Presupposition.Studies.Wang2025.instReprExp1Datum.repr : Exp1Datum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Presupposition.Studies.Wang2025.instReprExp1Datum : Repr Exp1Datum

Equations

• Phenomena.Presupposition.Studies.Wang2025.instReprExp1Datum = { reprPrec := Phenomena.Presupposition.Studies.Wang2025.instReprExp1Datum.repr }

def Phenomena.Presupposition.Studies.Wang2025.ye_full : Exp1Datum

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

Equations

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

def Phenomena.Presupposition.Studies.Wang2025.ye_partial : Exp1Datum

Equations

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

def Phenomena.Presupposition.Studies.Wang2025.ye_none : Exp1Datum

Equations

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

def Phenomena.Presupposition.Studies.Wang2025.you_full : Exp1Datum

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

Equations

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

def Phenomena.Presupposition.Studies.Wang2025.you_partial : Exp1Datum

Equations

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

def Phenomena.Presupposition.Studies.Wang2025.you_none : Exp1Datum

Equations

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

def Phenomena.Presupposition.Studies.Wang2025.jiu_full : Exp1Datum

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

Equations

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

def Phenomena.Presupposition.Studies.Wang2025.jiu_partial : Exp1Datum

Equations

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

def Phenomena.Presupposition.Studies.Wang2025.jiu_none : Exp1Datum

Equations

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

def Phenomena.Presupposition.Studies.Wang2025.zhidao_full : Exp1Datum

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

Equations

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

def Phenomena.Presupposition.Studies.Wang2025.zhidao_partial : Exp1Datum

Equations

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

def Phenomena.Presupposition.Studies.Wang2025.zhidao_none : Exp1Datum

Equations

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

theorem Phenomena.Presupposition.Studies.Wang2025.ye_jiu_partial_diverge : ye_partial.felicity ≠ jiu_partial.felicity

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

theorem Phenomena.Presupposition.Studies.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 CG.

theorem Phenomena.Presupposition.Studies.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 CG.

inductive Phenomena.Presupposition.Studies.Wang2025.Resolution : Type

Resolution locus for presupposition under attitude verbs.

• deRe : Resolution

  Presupposition resolved against CG (de re)

• deDicto : Resolution

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

@[implicit_reducible]

instance Phenomena.Presupposition.Studies.Wang2025.instDecidableEqResolution : DecidableEq Resolution

Equations

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

def Phenomena.Presupposition.Studies.Wang2025.instReprResolution.repr : Resolution → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Presupposition.Studies.Wang2025.instReprResolution : Repr Resolution

Equations

• Phenomena.Presupposition.Studies.Wang2025.instReprResolution = { reprPrec := Phenomena.Presupposition.Studies.Wang2025.instReprResolution.repr }

structure Phenomena.Presupposition.Studies.Wang2025.Exp3Datum : Type

A de re judgment datum (Experiment 3).

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

  Whether this resolution was accepted by participants

def Phenomena.Presupposition.Studies.Wang2025.instReprExp3Datum.repr : Exp3Datum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Presupposition.Studies.Wang2025.instReprExp3Datum : Repr Exp3Datum

Equations

• Phenomena.Presupposition.Studies.Wang2025.instReprExp3Datum = { reprPrec := Phenomena.Presupposition.Studies.Wang2025.instReprExp3Datum.repr }

def Phenomena.Presupposition.Studies.Wang2025.ye_deRe : Exp3Datum

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

Equations

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

def Phenomena.Presupposition.Studies.Wang2025.ye_deDicto : Exp3Datum

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

Equations

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

theorem Phenomena.Presupposition.Studies.Wang2025.additive_deRe_available : ye_deRe.accepted = true

Additive presupposition allows de re resolution.

@[reducible, inline]

abbrev Phenomena.Presupposition.Studies.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.Intensional.AccessRel; lift via fun a b => R a b = true to bridge.

Equations

• Phenomena.Presupposition.Studies.Wang2025.BAccessRel W = (W → W → Bool)

inductive Phenomena.Presupposition.Studies.Wang2025.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)

@[implicit_reducible]

instance Phenomena.Presupposition.Studies.Wang2025.instDecidableEqPragConstraint : DecidableEq PragConstraint

Equations

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

@[implicit_reducible]

instance Phenomena.Presupposition.Studies.Wang2025.instReprPragConstraint : Repr PragConstraint

Equations

• Phenomena.Presupposition.Studies.Wang2025.instReprPragConstraint = { reprPrec := Phenomena.Presupposition.Studies.Wang2025.instReprPragConstraint.repr }

def Phenomena.Presupposition.Studies.Wang2025.instReprPragConstraint.repr : PragConstraint → ℕ → Std.Format

Equations

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

def Phenomena.Presupposition.Studies.Wang2025.PragConstraint.isViolable : PragConstraint → Bool

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

Equations

• Phenomena.Presupposition.Studies.Wang2025.PragConstraint.IC.isViolable = false
• Phenomena.Presupposition.Studies.Wang2025.PragConstraint.FP.isViolable = true
• Phenomena.Presupposition.Studies.Wang2025.PragConstraint.MP.isViolable = true

def Phenomena.Presupposition.Studies.Wang2025.constraintRanking : List PragConstraint

The canonical constraint ranking: IC ≫ FP ≫ MP.

Equations

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

def Phenomena.Presupposition.Studies.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

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

def Phenomena.Presupposition.Studies.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

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

def Phenomena.Presupposition.Studies.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

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

def Phenomena.Presupposition.Studies.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

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

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

Predict obligatoriness from alternative structure and context.

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

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Presupposition.Studies.Wang2025.predictObligatoriness altStr false false = Semantics.Presupposition.TriggerTypology.Obligatoriness.blocked

theorem Phenomena.Presupposition.Studies.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 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 Phenomena.Presupposition.Studies.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 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 Phenomena.Presupposition.Studies.Wang2025.full_cg_obligatory (alt : Semantics.Presupposition.TriggerTypology.AltStructure) (b : Bool) : predictObligatoriness alt true b = Semantics.Presupposition.TriggerTypology.Obligatoriness.obligatory

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

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

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

def Phenomena.Presupposition.Studies.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

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

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 a local Bool-valued accessibility relation; for the Prop-valued canonical Kripke semantics see Core.Logic.Intensional.boxR.

Equations

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

structure Phenomena.Presupposition.Studies.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 : Semantics.Presupposition.TriggerTypology.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 Phenomena.Presupposition.Studies.Wang2025.wangCheck {W : Type u_1} (input : WangInput W) : Features.Acceptability

@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 Phenomena.Presupposition.Studies.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 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 Phenomena.Presupposition.Studies.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 CG entails the presupposition, the CI-lifted form yields a felicitous two-dimensional meaning where 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.