Mandarin Negation Fragment

[Mie05] [DH13a] [Zha25]

Mandarin Chinese has two standard negation particles:

Particle	Domain	Symmetric?
不 bù	General (non-perfective)	Yes
没(有) méi(yǒu)	Perfective / existential	No (A/Fin)

SymAsy: Symmetric and Asymmetric

WALS classifies Mandarin as both symmetric and asymmetric:

• Symmetric: 不 bù negation simply adds the particle before the verb, with no structural change. Available across tenses and moods.

• Asymmetric (A/Fin): 没(有) méi(yǒu) is restricted to perfective/ existential contexts and introduces a finiteness-like change: it is incompatible with certain aspect markers (e.g., 了 le perfective). The bù/méi split itself constitutes an asymmetry — the choice of negator depends on aspect, unlike in the affirmative.

Connection to AspectComparison

The méi(yǒu) entry connects to Mandarin.AspectComparison, where it is formalized as a cross-domain particle (negative perfective / not-exceed-threshold).

def Mandarin.Negation.bu : Syntax.Negation.NegMarkerEntry

不 bù — the general non-perfective negation particle. Used with imperfective, stative, modal, and future contexts; excluded from perfective and existential. Symmetric: simply adds to the verb without further structural change.

Equations

• Mandarin.Negation.bu = { form := "bù", morphemeType := Syntax.Negation.NegMorphemeType.particle, position := Syntax.Negation.NegMarkerPosition.preverbal }

def Mandarin.Negation.mei : Syntax.Negation.NegMarkerEntry

没 méi (long form 没有 méi-yǒu) — the perfective/existential negation particle. Asymmetric: incompatible with the perfective aspect marker 了 le; required as the negator of 有 yǒu 'have'. The choice between bù and méi is aspect-conditioned.

Equations

• Mandarin.Negation.mei = { form := "méi", morphemeType := Syntax.Negation.NegMorphemeType.particle, position := Syntax.Negation.NegMarkerPosition.preverbal }

def Mandarin.Negation.negationSystem : Syntax.Negation.NegationSystem

The Mandarin negation system: two aspect-conditioned markers. bù (default, non-perfective) listed first per the ordering convention in NegationSystem; méi second. The Fragment-side joint consumed by Studies/Dryer2013Negation.lean.

Equations

• Mandarin.Negation.negationSystem = Syntax.Negation.NegationSystem.ofISO "cmn" [Mandarin.Negation.bu, Mandarin.Negation.mei]

structure Mandarin.Negation.NegExample : Type

A Mandarin negation example.

• affirmative : String
• negative : String
• glossAff : String
• glossNeg : String
• negator : String

  Which negation particle is used

• symmetric : Bool

  Is this construction symmetric (neg = aff + neg marker, no other change)?

def Mandarin.Negation.instReprNegExample.repr : NegExample → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Mandarin.Negation.instReprNegExample : Repr NegExample

Equations

• Mandarin.Negation.instReprNegExample = { reprPrec := Mandarin.Negation.instReprNegExample.repr }

def Mandarin.Negation.instBEqNegExample.beq : NegExample → NegExample → Bool

Equations

• One or more equations did not get rendered due to their size.
• Mandarin.Negation.instBEqNegExample.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Mandarin.Negation.instBEqNegExample : BEq NegExample

Equations

• Mandarin.Negation.instBEqNegExample = { beq := Mandarin.Negation.instBEqNegExample.beq }

def Mandarin.Negation.buPresent : NegExample

不 bù + present/habitual: symmetric.

Equations

• Mandarin.Negation.buPresent = { affirmative := "tā chī", negative := "tā bù chī", glossAff := "3SG eat", glossNeg := "3SG NEG eat", negator := "bù", symmetric := true }

def Mandarin.Negation.buStative : NegExample

不 bù + stative: symmetric.

Equations

• Mandarin.Negation.buStative = { affirmative := "tā gāo", negative := "tā bù gāo", glossAff := "3SG tall", glossNeg := "3SG NEG tall", negator := "bù", symmetric := true }

def Mandarin.Negation.buFuture : NegExample

不 bù + future/modal: symmetric.

Equations

• Mandarin.Negation.buFuture = { affirmative := "tā huì lái", negative := "tā bù huì lái", glossAff := "3SG will come", glossNeg := "3SG NEG will come", negator := "bù", symmetric := true }

def Mandarin.Negation.meiPerfective : NegExample

没(有) méi(yǒu) + perfective: asymmetric. The perfective marker 了 le is dropped under negation.

Equations

• Mandarin.Negation.meiPerfective = { affirmative := "tā chī le", negative := "tā méi chī", glossAff := "3SG eat PFV", glossNeg := "3SG NEG.PFV eat", negator := "méi", symmetric := false }

def Mandarin.Negation.meiExistential : NegExample

没(有) méi(yǒu) + existential: asymmetric. 有 yǒu 'have/exist' can only be negated with 没, not 不.

Equations

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

def Mandarin.Negation.allExamples : List NegExample

Equations

• Mandarin.Negation.allExamples = [Mandarin.Negation.buPresent, Mandarin.Negation.buStative, Mandarin.Negation.buFuture, Mandarin.Negation.meiPerfective, Mandarin.Negation.meiExistential]

structure Mandarin.Negation.NegatorDistribution : Type

Which negation particle applies in which aspectual context.

• context : String
• negator : String

@[implicit_reducible]

instance Mandarin.Negation.instReprNegatorDistribution : Repr NegatorDistribution

Equations

• Mandarin.Negation.instReprNegatorDistribution = { reprPrec := Mandarin.Negation.instReprNegatorDistribution.repr }

def Mandarin.Negation.instReprNegatorDistribution.repr : NegatorDistribution → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Mandarin.Negation.instBEqNegatorDistribution : BEq NegatorDistribution

Equations

• Mandarin.Negation.instBEqNegatorDistribution = { beq := Mandarin.Negation.instBEqNegatorDistribution.beq }

def Mandarin.Negation.instBEqNegatorDistribution.beq : NegatorDistribution → NegatorDistribution → Bool

Equations

• Mandarin.Negation.instBEqNegatorDistribution.beq { context := a, negator := a_1 } { context := b, negator := b_1 } = (a == b && a_1 == b_1)
• Mandarin.Negation.instBEqNegatorDistribution.beq x✝¹ x✝ = false

def Mandarin.Negation.negatorContexts : List NegatorDistribution

Equations

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

Verification

theorem Mandarin.Negation.all_examples_count : allExamples.length = 5

theorem Mandarin.Negation.bu_symmetric_mei_asymmetric : ((List.filter (fun (x : NegExample) => x.negator == "bù") allExamples).all fun (x : NegExample) => x.symmetric) = true ∧ ((List.filter (fun (e : NegExample) => e.negator == "méi" || e.negator == "méi-yǒu") allExamples).all fun (e : NegExample) => !e.symmetric) = true

The bù constructions are symmetric; the méi constructions are not.

theorem Mandarin.Negation.symasy_distribution : (List.filter (fun (x : NegExample) => x.symmetric) allExamples).length = 3 ∧ (List.filter (fun (e : NegExample) => !e.symmetric) allExamples).length = 2

3 symmetric + 2 asymmetric constructions = SymAsy.

Bridge to AspectComparison

The méi-yǒu entry in AspectComparison formalizes the same particle as a cross-domain negative perfective.

theorem Mandarin.Negation.meiyou_matches_aspect_comparison : AspectComparison.meiyou.hanzi = "没有" ∧ AspectComparison.meiyou.pinyin = "méi-yǒu"

Expletive Negation

[JK21]

Mandarin EN negators show striking trigger-class covariation: different trigger classes select different expletive negators, and the choice is semantically motivated.

Trigger class	EN negator	Gloss	Note
FEAR	别 bié	don't (imperative)	Neither 不 nor 没 allowed
FEAR	不要 búyào	not-want (imp.)	Neither 不 nor 没 allowed
REGRET	不该 bùgāi	shouldn't (deontic)	Must include deontic modal
COMPLAIN	不该 bùgāi	shouldn't (deontic)	Must include deontic modal
DENY	不 bù	NEG (general)	Standard negator
BEFORE	不 bù	NEG (general)	Via 以前 yǐqián
ALMOST	没 méi	NEG (perfective)	Via 差点儿 chàdiǎnr

The imperative negators bié/búyào for FEAR connect to the desiderative semantics: fear activates the desire for ¬p, and the imperative form lexicalizes the prohibition component.

The deontic negator bùgāi for REGRET/COMPLAIN connects to the behavioral-standards semantics: the negative inference is that ¬p is consistent with X's standards, i.e., p shouldn't have happened.

def Mandarin.Negation.bieParticle : String

Mandarin imperative negation particle (used as EN for FEAR).

Equations

• Mandarin.Negation.bieParticle = "bié"

def Mandarin.Negation.buyaoParticle : String

Mandarin imperative negation 'not-want' (used as EN for FEAR).

Equations

• Mandarin.Negation.buyaoParticle = "búyào"

def Mandarin.Negation.bugaiParticle : String

Mandarin deontic negation 'shouldn't' (used as EN for REGRET/COMPLAIN).

Equations

• Mandarin.Negation.bugaiParticle = "bùgāi"

def Mandarin.Negation.enTriggerNegators : List Syntax.Negation.ENTriggerNegator

EN trigger-negator pairings (pinyin forms) from [JK21], Table 5 and §6.1–6.4.

Equations

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

theorem Mandarin.Negation.fear_uses_imperative_neg : ((List.filter (fun (x : Syntax.Negation.ENTriggerNegator) => x.triggerClass == "FEAR") enTriggerNegators).all fun (x : Syntax.Negation.ENTriggerNegator) => x.enNegatorForm == "bié") = true

FEAR triggers use imperative negators, not the standard bù or méi. This connects to the desiderative semantics: fear activates desire for ¬p, and imperative negation lexicalizes prohibition ([JK21], §6.1.1, ex. 14).

theorem Mandarin.Negation.regret_uses_deontic_neg : ((List.filter (fun (e : Syntax.Negation.ENTriggerNegator) => e.triggerClass == "REGRET" || e.triggerClass == "COMPLAIN") enTriggerNegators).all fun (x : Syntax.Negation.ENTriggerNegator) => x.enNegatorForm == "bùgāi") = true

REGRET/COMPLAIN triggers use the deontic negator bùgāi 'shouldn't'. This connects to the behavioral-standards semantics: ¬p is consistent with X's standards → p shouldn't have happened ([JK21], §6.1.2).

def Mandarin.Negation.negationProfile : Syntax.Negation.NegationProfile

Mandarin Chinese negation profile (WALS Ch 112-115 + Greco/JinKoenig fields).

Equations

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