Mandarin Presuppositional Particles

@cite{wang-2025}

Lexical entries for Mandarin presupposition triggers, linking Fragment-level lexical data to the NeoGricean trigger typology (@cite{wang-2025} Table 4.1) and experimental data (@cite{wang-2025} Experiments 1-3).

Triggers

Particle	Gloss	Trigger Type	Alt Structure	Alt Form
也 ye	also	iterative	deletion	∅
又 you	again	iterative	deletion	∅
仍 reng	still	continuative	deletion	∅
就 jiu	only	cleft	none	∅
知道 zhidao	know	factive	replacement	believe (以为)
不再 buzai	no longer	changeOfState	replacement	not (不)
开始 kaishi	start	aspectual	replacement	do (做)
反而 fan'er	instead	iterative	replacement	and (和)
而 er	instead	iterative	replacement	and (和)
还 hai	still	continuative	deletion	∅

Cross-Module Connections

• Semantics.Presupposition.TriggerTypology.AltStructure: alternative classification
• Semantics.Presupposition.TriggerTypology.PresupTrigger: trigger type
• Wang2025: experimental data

inductive Fragments.Mandarin.Particles.MandarinTrigger : Type

Mandarin presupposition triggers studied in @cite{wang-2025} Experiments 1-2.

• ye : MandarinTrigger
• you : MandarinTrigger
• reng : MandarinTrigger
• jiu : MandarinTrigger
• zhidao : MandarinTrigger
• buzai : MandarinTrigger
• kaishi : MandarinTrigger
• faner : MandarinTrigger
• er : MandarinTrigger

@[implicit_reducible]

instance Fragments.Mandarin.Particles.instDecidableEqMandarinTrigger : DecidableEq MandarinTrigger

Equations

• Fragments.Mandarin.Particles.instDecidableEqMandarinTrigger x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Mandarin.Particles.instReprMandarinTrigger : Repr MandarinTrigger

Equations

• Fragments.Mandarin.Particles.instReprMandarinTrigger = { reprPrec := Fragments.Mandarin.Particles.instReprMandarinTrigger.repr }

def Fragments.Mandarin.Particles.instReprMandarinTrigger.repr : MandarinTrigger → ℕ → Std.Format

Equations

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

structure Fragments.Mandarin.Particles.PresupParticle : Type

A Mandarin presuppositional particle entry. Links surface form to trigger type and alternative structure.

• hanzi : String

  Chinese character(s)

• pinyin : String

  Pinyin romanization

• gloss : String

  English gloss

• triggerEntry : Semantics.Presupposition.TriggerTypology.PresupTriggerEntry

  Corresponding trigger entry (type + alternative structure)

• dataTrigger : MandarinTrigger

  Link to experimental data trigger identifier

@[implicit_reducible]

instance Fragments.Mandarin.Particles.instReprPresupParticle : Repr PresupParticle

Equations

• Fragments.Mandarin.Particles.instReprPresupParticle = { reprPrec := Fragments.Mandarin.Particles.instReprPresupParticle.repr }

def Fragments.Mandarin.Particles.instReprPresupParticle.repr : PresupParticle → ℕ → Std.Format

Equations

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

def Fragments.Mandarin.Particles.ye : PresupParticle

也 ye 'also' — additive particle, deletion alternative.

Equations

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

def Fragments.Mandarin.Particles.you : PresupParticle

又 you 'again' — repetitive, deletion alternative.

Equations

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

def Fragments.Mandarin.Particles.reng : PresupParticle

仍 reng 'still' — continuative, deletion alternative. Distinct from 又 you 'again' (iterative): reng's presupposition is uninterrupted continuation of P throughout an interval, whereas you presupposes P-then-not-P-then-P-again. The original encoding of reng as .iterative (matching you) collapsed this contrast; .continuative was added to PresupTrigger to distinguish them.

Equations

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

def Fragments.Mandarin.Particles.jiu : PresupParticle

就 jiu 'only' — exclusive, NO structural alternative.

Equations

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

def Fragments.Mandarin.Particles.zhidao : PresupParticle

知道 zhidao 'know' — factive, replacement alternative (以为 yiwei 'believe').

Equations

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

def Fragments.Mandarin.Particles.buzai : PresupParticle

不再 buzai 'no longer' — cessative, replacement alternative (不 bu 'not').

Equations

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

def Fragments.Mandarin.Particles.kaishi : PresupParticle

开始 kaishi 'start' — inchoative, replacement alternative (做 zuo 'do').

Equations

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

def Fragments.Mandarin.Particles.faner : PresupParticle

反而 fan'er 'instead' — contrastive, replacement alternative.

Equations

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

def Fragments.Mandarin.Particles.er : PresupParticle

而 er 'instead' — weaker contrastive, replacement alternative.

Equations

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

def Fragments.Mandarin.Particles.wang2025Particles : List PresupParticle

All particles studied in @cite{wang-2025}.

Equations

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

theorem Fragments.Mandarin.Particles.ye_deletion : ye.triggerEntry.altStructure = Semantics.Presupposition.TriggerTypology.AltStructure.deletion

ye has deletion alternative structure.

theorem Fragments.Mandarin.Particles.jiu_no_alt : jiu.triggerEntry.altStructure = Semantics.Presupposition.TriggerTypology.AltStructure.none

jiu has no structural alternative.

theorem Fragments.Mandarin.Particles.zhidao_replacement : zhidao.triggerEntry.altStructure = Semantics.Presupposition.TriggerTypology.AltStructure.replacement

zhidao has replacement alternative.

theorem Fragments.Mandarin.Particles.obligatory_all_deletion : ye.triggerEntry.altStructure = Semantics.Presupposition.TriggerTypology.AltStructure.deletion ∧ you.triggerEntry.altStructure = Semantics.Presupposition.TriggerTypology.AltStructure.deletion ∧ reng.triggerEntry.altStructure = Semantics.Presupposition.TriggerTypology.AltStructure.deletion

Obligatory triggers (ye, you, reng) all have deletion alternatives.

theorem Fragments.Mandarin.Particles.blocked_no_alt : jiu.triggerEntry.altStructure = Semantics.Presupposition.TriggerTypology.AltStructure.none

Blocked trigger (jiu) has no alternative — this is what predicts blocking.

theorem Fragments.Mandarin.Particles.ye_data_link : ye.dataTrigger = MandarinTrigger.ye

ye links to experimental data trigger.ye

theorem Fragments.Mandarin.Particles.jiu_data_link : jiu.dataTrigger = MandarinTrigger.jiu

jiu links to experimental data trigger.jiu