@cite{wang-2025} Experimental Data

@cite{wang-2025} @cite{wang-yaxuan-2025}

Theory-neutral experimental data from @cite{wang-2025} "Presupposition, Competition, and Coherence" — three experiments on Mandarin presupposition triggers.

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

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

Context condition for presupposition support.

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

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.

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

Equations

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

instance Phenomena.Presupposition.Studies.Wang2025.instBEqContextCondition : BEq ContextCondition

Equations

• Phenomena.Presupposition.Studies.Wang2025.instBEqContextCondition = { beq := Phenomena.Presupposition.Studies.Wang2025.instBEqContextCondition.beq }

def Phenomena.Presupposition.Studies.Wang2025.instBEqContextCondition.beq : ContextCondition → ContextCondition → Bool

Equations

• Phenomena.Presupposition.Studies.Wang2025.instBEqContextCondition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

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 : Interfaces.FelicityStatus

  Observed felicity judgment

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.instReprExp1Datum.repr : Exp1Datum → ℕ → Std.Format

Equations

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

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 = Interfaces.FelicityStatus.felicitous ∧ ye_partial.felicity = Interfaces.FelicityStatus.felicitous ∧ ye_none.felicity = Interfaces.FelicityStatus.odd

Obligatory triggers are felicitous under both full and partial CG.

theorem Phenomena.Presupposition.Studies.Wang2025.blocked_trigger_pattern : jiu_full.felicity = Interfaces.FelicityStatus.felicitous ∧ jiu_partial.felicity = Interfaces.FelicityStatus.odd ∧ jiu_none.felicity = Interfaces.FelicityStatus.odd

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)

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.

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

Equations

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

instance Phenomena.Presupposition.Studies.Wang2025.instBEqResolution : BEq Resolution

Equations

• Phenomena.Presupposition.Studies.Wang2025.instBEqResolution = { beq := Phenomena.Presupposition.Studies.Wang2025.instBEqResolution.beq }

def Phenomena.Presupposition.Studies.Wang2025.instBEqResolution.beq : Resolution → Resolution → Bool

Equations

• Phenomena.Presupposition.Studies.Wang2025.instBEqResolution.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

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

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.instReprExp3Datum.repr : Exp3Datum → ℕ → Std.Format

Equations

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

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.