Mandarin Question Particles

@cite{zheng-2025}

Lexical entries for Mandarin interrogative particles with distributional properties and bias profiles. The fragment commits only to theory-neutral lexical primitives; the left-peripheral layer assignment lives in Phenomena.Questions.Studies.Zheng2025.

Particles

Particle	Gloss	Evidential	Epistemic	Restriction
吗 ma	PQ marker	±	±	polar + wh
吧 ba	TAG/confirm	±	+forP	polar only
难道 nándào	NANDAO	+forP	±	polar only

Cross-Module Connections

• BiasedPQ.OriginalBias: ba requires .forP; nandao/ma compatible with .neutral
• BiasedPQ.ContextualEvidence: nandao requires .forP; ma/ba do not
• Kernel.nandaoFelicitous: formal felicity conditions for nandao

structure Fragments.Mandarin.QuestionParticles.QuestionParticleEntry : Type

A Mandarin interrogative particle entry.

• hanzi : String
• pinyin : String
• gloss : String
• polarOk : Bool

  Compatible with polar questions?

• declOk : Bool

  Compatible with declaratives?

• whOk : Bool

  Compatible with wh-questions?

• requiresEvidentialBias : Bool

  Requires positive evidential bias (contextual evidence for p)?

• requiresEpistemicBias : Bool

  Requires negative epistemic bias (prior belief against p)?

@[implicit_reducible]

instance Fragments.Mandarin.QuestionParticles.instReprQuestionParticleEntry : Repr QuestionParticleEntry

Equations

• Fragments.Mandarin.QuestionParticles.instReprQuestionParticleEntry = { reprPrec := Fragments.Mandarin.QuestionParticles.instReprQuestionParticleEntry.repr }

def Fragments.Mandarin.QuestionParticles.instReprQuestionParticleEntry.repr : QuestionParticleEntry → ℕ → Std.Format

Equations

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

def Fragments.Mandarin.QuestionParticles.instDecidableEqQuestionParticleEntry.decEq (x✝ x✝¹ : QuestionParticleEntry) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Fragments.Mandarin.QuestionParticles.instDecidableEqQuestionParticleEntry : DecidableEq QuestionParticleEntry

Equations

• Fragments.Mandarin.QuestionParticles.instDecidableEqQuestionParticleEntry = Fragments.Mandarin.QuestionParticles.instDecidableEqQuestionParticleEntry.decEq

def Fragments.Mandarin.QuestionParticles.ma : QuestionParticleEntry

吗 ma — unmarked polar question particle. Sentence-final particle that turns a declarative into a yes/no question. No bias requirements; compatible with all contexts.

Equations

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

def Fragments.Mandarin.QuestionParticles.ba : QuestionParticleEntry

吧 ba — confirmation-seeking particle. Speaker expects a positive answer and seeks confirmation. Comparable to English tag questions ("It's raining, isn't it?"). Requires original speaker bias for p but no evidential bias.

Equations

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

def Fragments.Mandarin.QuestionParticles.nandao : QuestionParticleEntry

难道 nándào — evidential question particle. Marks that the speaker has encountered unexpected contextual evidence supporting the prejacent. Compatible with neutral epistemic state (pure inquiry use, @cite{zheng-2025} ex. 3).

Equations

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

def Fragments.Mandarin.QuestionParticles.allQuestionParticles : List QuestionParticleEntry

Equations

• Fragments.Mandarin.QuestionParticles.allQuestionParticles = [Fragments.Mandarin.QuestionParticles.ma, Fragments.Mandarin.QuestionParticles.ba, Fragments.Mandarin.QuestionParticles.nandao]

theorem Fragments.Mandarin.QuestionParticles.ma_no_bias : ma.requiresEvidentialBias = false ∧ ma.requiresEpistemicBias = false

ma is the unmarked baseline: no bias requirements.

theorem Fragments.Mandarin.QuestionParticles.ma_wh_ok : ma.whOk = true

ma is compatible with wh-questions (unlike ba and nandao).

theorem Fragments.Mandarin.QuestionParticles.ba_requires_epistemic : ba.requiresEpistemicBias = true ∧ ba.requiresEvidentialBias = false

ba requires epistemic bias (speaker expects p).

theorem Fragments.Mandarin.QuestionParticles.ba_polar_only : ba.polarOk = true ∧ ba.declOk = false ∧ ba.whOk = false

ba is restricted to polar questions.

theorem Fragments.Mandarin.QuestionParticles.nandao_polar_only : nandao.polarOk = true ∧ nandao.declOk = false ∧ nandao.whOk = false

nandao is restricted to polar questions (@cite{zheng-2025} ex. 12).

theorem Fragments.Mandarin.QuestionParticles.nandao_bias_profile : nandao.requiresEvidentialBias = true ∧ nandao.requiresEpistemicBias = false

nandao requires evidential but not epistemic bias (@cite{zheng-2025} §2).

theorem Fragments.Mandarin.QuestionParticles.nandao_neutral_bias_ok : nandao.requiresEpistemicBias = false

nandao is compatible with neutral original speaker bias (pure inquiry).

theorem Fragments.Mandarin.QuestionParticles.bias_contrast_triple : ma.requiresEvidentialBias = false ∧ ma.requiresEpistemicBias = false ∧ ba.requiresEvidentialBias = false ∧ ba.requiresEpistemicBias = true ∧ nandao.requiresEvidentialBias = true ∧ nandao.requiresEpistemicBias = false

The three particles form a bias contrast triple: ma is neutral, ba requires epistemic, nandao requires evidential.

theorem Fragments.Mandarin.QuestionParticles.only_ma_allows_wh : List.filter (fun (x : QuestionParticleEntry) => x.whOk) allQuestionParticles = [ma]

Only ma is compatible with wh-questions.

theorem Fragments.Mandarin.QuestionParticles.no_double_bias : (allQuestionParticles.all fun (p : QuestionParticleEntry) => !(p.requiresEvidentialBias && p.requiresEpistemicBias)) = true

No particle requires BOTH evidential and epistemic bias.