Zheng (2025): Nandao-Q Felicity [Zhe25]

Mandarin nandao-question felicity. Self-contained study file: empirical data, the Mandarin Fragment entry, and bridges to the Kernel-theoretic felicity predicate nandaoFelicitous.

The core finding is that positive evidential bias is necessary for nandao-Q felicity, while negative epistemic bias is neither necessary nor sufficient.

Key Generalizations

1. Positive evidential bias (contextual evidence for p) → nandao felicitous
2. Epistemic bias alone (prior belief against p, no evidence) → nandao infelicitous
3. Evidence must be unexpected relative to prior information state
4. Nandao-Qs can function as pure inquiry (no prior belief required)

Predictions verified

• nandaoContextualEvidence / nandaoOriginalBias: Zheng's bias classification of nandao, grounded in evidential_bias_necessary and epistemic_bias_not_necessary
• kernel_requires_evidence: Kernel nandaoFelicitous entails evidenceSupports
• nandaoFullFelicity: integrated two-layer felicity (singleton sister presupposition ∧ Kernel-bias check) — §5
• biasedUse_integrated_felicity: dripping-raincoat scenario satisfies integrated felicity at the §5 level — §6
• biasedUse_witnesses_integrated_felicity: §1 datum (ex. 2) ↔ §6 theoretical prediction

Known gaps

• No formalization of the unexpectedness requirement in the Kernel theory

structure Zheng2025.NandaoDatum : Type

A nandao-Q felicity datum.

• exampleNum : String

  Example number from [Zhe25]

• context : String

  Context description

• sentence : String

  The nandao-Q sentence (pinyin)

• evidentialBias : Bool

  Is there positive evidential bias (contextual evidence for p)?

• epistemicBias : Bool

  Is there negative epistemic bias (prior belief against p)?

• unexpectedEvidence : Bool

  Is the evidence unexpected?

• felicitous : Bool

  Is the nandao-Q felicitous?

def Zheng2025.instReprNandaoDatum.repr : NandaoDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Zheng2025.instReprNandaoDatum : Repr NandaoDatum

Equations

• Zheng2025.instReprNandaoDatum = { reprPrec := Zheng2025.instReprNandaoDatum.repr }

def Zheng2025.instDecidableEqNandaoDatum.decEq (x✝ x✝¹ : NandaoDatum) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Zheng2025.instDecidableEqNandaoDatum : DecidableEq NandaoDatum

Equations

• Zheng2025.instDecidableEqNandaoDatum = Zheng2025.instDecidableEqNandaoDatum.decEq

def Zheng2025.rhetoricalUse : NandaoDatum

Ex. 1: Rhetorical use. Lee working on Sunday (evidence) contradicts B's norm that people don't work Sundays (epistemic/deontic bias).

Equations

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

def Zheng2025.biasedUse : NandaoDatum

Ex. 2: Biased question. A believes not-raining; B enters with dripping raincoat (evidence contradicting belief).

Equations

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

def Zheng2025.pureInquiry : NandaoDatum

Ex. 3: Pure inquiry (NOVEL). Same evidence as ex. 2 but A has NO prior belief about the weather. Nandao is still felicitous.

Equations

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

def Zheng2025.epistemicOnly : NandaoDatum

Ex. 4a: Epistemic bias without evidence. Speaker believes room is empty but has no contextual evidence either way.

Equations

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

def Zheng2025.evidenceNoBelief : NandaoDatum

Ex. 5 ctx 1: Evidence + no belief → felicitous.

Equations

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

def Zheng2025.noEvidenceNoBelief : NandaoDatum

Ex. 5 ctx 2: No evidence + no belief → infelicitous.

Equations

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

def Zheng2025.beliefNoEvidence : NandaoDatum

Ex. 5 ctx 3: No evidence + epistemic bias → infelicitous.

Equations

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

def Zheng2025.unexpectedEvidence_ : NandaoDatum

Ex. 6 ctx 1: Unexpected evidence → felicitous.

Equations

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

def Zheng2025.expectedEvidence : NandaoDatum

Ex. 6 ctx 2: Expected evidence → infelicitous.

Equations

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

def Zheng2025.allData : List NandaoDatum

Equations

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

theorem Zheng2025.evidential_bias_necessary : ((List.filter (fun (x : NandaoDatum) => x.felicitous) allData).all fun (x : NandaoDatum) => x.evidentialBias) = true

Generalization 1: All felicitous nandao-Qs have evidential bias.

theorem Zheng2025.epistemic_bias_not_necessary : (List.filter (fun (d : NandaoDatum) => d.felicitous && !d.epistemicBias) allData).length > 0

Generalization 2: Some felicitous nandao-Qs lack epistemic bias (the pure inquiry use).

theorem Zheng2025.epistemic_bias_not_sufficient : (List.filter (fun (d : NandaoDatum) => d.epistemicBias && !d.felicitous) allData).length > 0

Generalization 3: Some infelicitous nandao-Qs have epistemic bias (epistemic bias is not sufficient).

theorem Zheng2025.unexpectedness_necessary : ((List.filter (fun (x : NandaoDatum) => x.felicitous) allData).all fun (x : NandaoDatum) => x.unexpectedEvidence) = true

Generalization 4: All felicitous nandao-Qs have unexpected evidence.

theorem Zheng2025.dataset_size : allData.length = 9

9 data points from 6 examples covering 4 conditions.

def Zheng2025.nandaoContextualEvidence : Option Semantics.Questions.Bias.ContextualEvidence

Zheng's evidential classification of nandao: requires contextual evidence for p — the lexical face of evidential_bias_necessary. (Formerly a fragment field; a particle's bias requirement is the analysis, so it lives here.)

Equations

• Zheng2025.nandaoContextualEvidence = some Semantics.Questions.Bias.ContextualEvidence.forP

def Zheng2025.nandaoOriginalBias : Option Semantics.Questions.Bias.OriginalBias

Zheng's classification: nandao does NOT require epistemic bias — compatible with a neutral epistemic state (pure inquiry use, ex. 3); the lexical face of epistemic_bias_not_necessary.

Equations

• Zheng2025.nandaoOriginalBias = none

theorem Zheng2025.kernel_requires_evidence (k : Semantics.Modality.Kernel Semantics.Modality.World) (u : Semantics.Modality.Background Semantics.Modality.World) (φ : Semantics.Modality.World → Prop) [DecidablePred φ] (h : Semantics.Modality.nandaoFelicitous k u φ) : k.evidenceSupports φ

Kernel nandaoFelicitous entails evidenceSupports, connecting the Theory predicate to nandaoContextualEvidence and the empirical generalization evidential_bias_necessary.

def Zheng2025.ma_layer : Particle → Features.QParticleLayer

Zheng's layer assignments for the three Mandarin Q-particles in the [Day25] cartography [SAP [PerspP [CP ...]]]. The _ argument is unused: the layer is a theoretical overlay on the fragment particle, not a computed property of its lexical fields.

Equations

• Zheng2025.ma_layer x✝ = Features.QParticleLayer.cp

def Zheng2025.ba_layer : Particle → Features.QParticleLayer

Equations

• Zheng2025.ba_layer x✝ = Features.QParticleLayer.perspP

def Zheng2025.nandao_layer : Particle → Features.QParticleLayer

Equations

• Zheng2025.nandao_layer x✝ = Features.QParticleLayer.perspP

theorem Zheng2025.ma_is_CP : ma_layer Mandarin.QuestionParticles.ma = Features.QParticleLayer.cp

ma is the unmarked CP-layer particle: widest distribution (matrix, subordinated, quasi-subordinated).

theorem Zheng2025.ba_nandao_PerspP : ba_layer Mandarin.QuestionParticles.ba = Features.QParticleLayer.perspP ∧ nandao_layer Mandarin.QuestionParticles.nandao = Features.QParticleLayer.perspP

ba and nandao are PerspP-layer biased particles: matrix + quasi-subordinated only.

def Zheng2025.baOriginalBias : Option Semantics.Questions.Bias.OriginalBias

Zheng's classification of ba: speaker-bias (expects a positive answer, seeks confirmation), no evidential requirement; the unbiased ma imposes neither. The layer split mirrors this bias split — the unbiased particle is CP (ma_is_CP), the biased ones PerspP (ba_nandao_PerspP).

Equations

• Zheng2025.baOriginalBias = some Semantics.Questions.Bias.OriginalBias.forP

[BD20] fn. 11 explicitly cites the parallel Mandarin nandao analysis as the model for their kya: proposal. At the algebraic level, both particles share the same singleton presupposition: their sister question must denote a singleton-cell issue ([BD20] eq. 23). The cross-particle generalization is captured by inheriting the same Question.IsSingleton predicate — both kya: and nandao take a SingletonQuestion W as well-typed sister content.

theorem Zheng2025.nandao_felicitous_declarative {W : Type u} (p : Set W) : (Question.declarative p).IsSingleton

nandao is felicitous on a one-cell ("highlighted") polar — same canonical good-input case as kya:. The proof reduces to isSingleton_declarative, identical to the kya: side.

theorem Zheng2025.nandao_kya_share_felicity {W : Type u} (p : Set W) : ⋯ = ⋯

Cross-particle agreement: the felicity conditions for kya: and nandao on a one-cell polar are the same theorem — both reduce to isSingleton_declarative. The convergence noted in [BD20] fn. 11 holds by construction.

Bridge §2 and §4. Nandao's full felicity has two independent layers:

• Layer 1 (Question-level, §4): the sister content Q : Question World is singleton — alt Q = {p} for some unique witness p. This is the [BD20] eq. 23 presupposition: nandao requires a one-cell sister, not a two-cell Hamblin polar.
• Layer 2 (Kernel-level, §2): the Kernel-bias check nandaoFelicitous k u p holds for the witness — the evidence in K raises P(p), K is incompatible with the prior U, and p is not directly settled.

These layers are independent concerns: Layer 1 is about semantic well-formedness of the sister content, Layer 2 is about discourse felicity in context. The integrated predicate composes them into a single statement, and the bridges below show that Layer 1 failure (e.g. a non-trivial two-cell polar) blocks felicity at the integrated level regardless of (k, u).

def Zheng2025.nandaoFullFelicity (Q : Question Semantics.Modality.World) (k : Semantics.Modality.Kernel Semantics.Modality.World) (u : Semantics.Modality.Background Semantics.Modality.World) (p : Set Semantics.Modality.World) [DecidablePred p] : Prop

Integrated nandao felicity: the conjunction of Layer 1 (singleton presupposition: alt Q = {p}) and Layer 2 (Kernel-bias check on the witness). The witness p is supplied externally so decidability is concrete; for the noncomputable choice from a SingletonQuestion use SingletonQuestion.witness.

Equations

• Zheng2025.nandaoFullFelicity Q k u p = (Q.alt = {p} ∧ Semantics.Modality.nandaoFelicitous k u p)

theorem Zheng2025.nandaoFullFelicity_isSingleton {Q : Question Semantics.Modality.World} {k : Semantics.Modality.Kernel Semantics.Modality.World} {u : Semantics.Modality.Background Semantics.Modality.World} {p : Set Semantics.Modality.World} [DecidablePred p] (h : nandaoFullFelicity Q k u p) : Q.IsSingleton

Layer-1 projection: integrated felicity entails the §4 singleton presupposition.

theorem Zheng2025.nandaoFullFelicity_kernel {Q : Question Semantics.Modality.World} {k : Semantics.Modality.Kernel Semantics.Modality.World} {u : Semantics.Modality.Background Semantics.Modality.World} {p : Set Semantics.Modality.World} [DecidablePred p] (h : nandaoFullFelicity Q k u p) : Semantics.Modality.nandaoFelicitous k u p

Layer-2 projection: integrated felicity entails the §2 Kernel-bias check on the witness.

theorem Zheng2025.nandao_polar_no_witness {p₀ : Set Semantics.Modality.World} (hne : p₀ ≠ ∅) (hnu : p₀ ≠ Set.univ) (k : Semantics.Modality.Kernel Semantics.Modality.World) (u : Semantics.Modality.Background Semantics.Modality.World) : ¬∃ (p : Set Semantics.Modality.World) (x : DecidablePred p), nandaoFullFelicity (Question.polar p₀) k u p

Layer-1 obstruction: a two-cell Hamblin polar polar p₀ (with non-trivial p₀) admits no integrated-felicity witness. No Kernel + Background can rescue it: the §4 type-level barrier propagates upward through the alt Q = {p} requirement. The structural reason polar two-cell questions are universally blocked from nandao licensing.

theorem Zheng2025.nandaoFullFelicity_declarative_iff {p : Set Semantics.Modality.World} [DecidablePred p] (k : Semantics.Modality.Kernel Semantics.Modality.World) (u : Semantics.Modality.Background Semantics.Modality.World) : nandaoFullFelicity (Question.declarative p) k u p ↔ Semantics.Modality.nandaoFelicitous k u p

Declarative reduction: on a one-cell sister declarative p, integrated felicity is exactly the §2 Kernel-bias check on p. The Layer-1 component holds trivially because alt (declarative p) = {p} (alt_declarative). This makes the §2 ↔ §5 connection explicit on the canonical felicitous case.

Apply §5 to the canonical biased-use scenario from [Zhe25] ex. 2:

• K = [wearingRaincoat] — direct evidence (B enters with dripping coat)
• U = [expectDry] — A's prior expectation it is not raining
• p = isRaining — the question content

The Kernel-side bias check is raincoat_nandao_felicitous (proven in Semantics/Modality/Kernel.lean from explicit cardinality counts on World4). Pairing it with the singleton presupposition yields integrated felicity at the §5 level. The §1 datum biasedUse records the same scenario as empirical data (evidentialBias = true, epistemicBias = true, felicitous = true); the bridge below makes the data ↔ theory correspondence explicit.

theorem Zheng2025.biasedUse_integrated_felicity : nandaoFullFelicity (Question.declarative Semantics.Modality.isRaining) Semantics.Modality.raincoatK Semantics.Modality.dryU Semantics.Modality.isRaining

§1 ex. 2 ↔ §5 integrated felicity: in the dripping-raincoat scenario with sister declarative isRaining, both layers of nandao felicity hold simultaneously. Reduces to raincoat_nandao_felicitous via nandaoFullFelicity_declarative_iff.

theorem Zheng2025.biasedUse_witnesses_integrated_felicity : biasedUse.felicitous = true ∧ biasedUse.evidentialBias = true ∧ biasedUse.epistemicBias = true ∧ nandaoFullFelicity (Question.declarative Semantics.Modality.isRaining) Semantics.Modality.raincoatK Semantics.Modality.dryU Semantics.Modality.isRaining

Data ↔ theory bridge: the §1 datum biasedUse is felicitous and has both bias profiles set; the §5 integrated felicity holds for the matching Kernel scenario. The shared scaffold is the dripping-raincoat setup of [Zhe25] ex. 2 — empirical observation on the data side, derived prediction on the theory side.