Mandarin Presuppositional Particles

Lexical entries for the Mandarin presupposition triggers studied experimentally in [Wan25a]. Entries carry consensus trigger-type metadata only; [Wan25a]'s alternative-structure classification and the competition analysis built on it live in Studies/Wang2025.lean.

Particle	Gloss	Trigger Type
也 ye	also	additive
又 you	again	iterative
仍 reng	still	continuative
就 jiu	only	exclusive
知道 zhidao	know	factive
不再 buzai	no longer	changeOfState
开始 kaishi	start	aspectual
反而 fan'er	instead	contrastive
而 er	instead	contrastive

inductive Mandarin.Particles.MandarinTrigger : Type

Mandarin presupposition triggers studied in [Wan25a] Experiments 1-2.

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

@[instance_reducible]

instance Mandarin.Particles.instDecidableEqMandarinTrigger : DecidableEq MandarinTrigger

Equations

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

def Mandarin.Particles.instReprMandarinTrigger.repr : MandarinTrigger → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Mandarin.Particles.instReprMandarinTrigger : Repr MandarinTrigger

Equations

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

structure Mandarin.Particles.PresupParticle : Type

A Mandarin presuppositional particle entry.

• hanzi : String

  Chinese character(s)

• pinyin : String

  Pinyin romanization

• gloss : String

  English gloss

• trigger : Semantics.Presupposition.TriggerTypology.PresupTrigger

  Trigger type (consensus classification)

• dataTrigger : MandarinTrigger

  Link to experimental data trigger identifier

@[instance_reducible]

instance Mandarin.Particles.instReprPresupParticle : Repr PresupParticle

Equations

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

def Mandarin.Particles.instReprPresupParticle.repr : PresupParticle → Nat → Std.Format

Equations

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

def Mandarin.Particles.ye : PresupParticle

也 ye 'also' — additive particle ([Kri09]'s too-class).

Equations

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

def Mandarin.Particles.you : PresupParticle

又 you 'again' — repetitive iterative.

Equations

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

def Mandarin.Particles.reng : PresupParticle

仍 reng 'still' — continuative. 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 Mandarin.Particles.jiu : PresupParticle

就 jiu 'only' — exclusive; presupposes its prejacent.

Equations

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

def Mandarin.Particles.zhidao : PresupParticle

知道 zhidao 'know' — factive (non-factive counterpart: 以为 yiwei 'believe').

Equations

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

def Mandarin.Particles.buzai : PresupParticle

不再 buzai 'no longer' — cessative change-of-state.

Equations

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

def Mandarin.Particles.kaishi : PresupParticle

开始 kaishi 'start' — inchoative aspectual.

Equations

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

def Mandarin.Particles.faner : PresupParticle

反而 fan'er 'instead' — contrastive.

Equations

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

def Mandarin.Particles.er : PresupParticle

而 er 'instead' — weaker contrastive.

Equations

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

def Mandarin.Particles.wang2025Particles : List PresupParticle

All particles studied in [Wan25a].

Equations

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