Zheng (2025): Nandao-Q Felicity

Mandarin nandao-question felicity: positive evidential bias is necessary, while negative epistemic bias is neither necessary nor sufficient. The felicity conditions ([Zhe25] condition (11)) are built on [vFG10]'s kernel: some evidence in the kernel K raises the probability of the prejacent, K conflicts with the prior information state U, and the prejacent is not directly settled in K.

Main declarations

• evidential_bias_necessary, epistemic_bias_not_necessary, epistemic_bias_not_sufficient, unexpectedness_necessary: the felicity generalizations over the example rows of Data.Examples.Zheng2025
• nandaoFelicitous: condition (11) — evidence raises P(φ), the kernel is unexpected given the prior state, φ unsettled
• raincoat_nandao_felicitous: the dripping-raincoat scenario (exx. 2–3) satisfies all three conditions; no_evidence_nandao_infelicitous and expected_evidence_infelicitous are the matching negative checks
• nandaoContextualEvidence / nandaoOriginalBias: Zheng's bias classification of nandao
• nandaoFullFelicity: integrated two-layer felicity — singleton sister presupposition (shared with [BD20]'s kya:) ∧ kernel-bias check
• biasedUse_integrated_felicity: the raincoat scenario satisfies the integrated predicate

Empirical data

The example rows of exx. 1–6 live in Data/Examples/Zheng2025.json; the adapters below read each row's felicity and bias profile off the generated Data.Examples.Zheng2025 module.

def Zheng2025.evidentialBias (row : Data.Examples.LinguisticExample) : Bool

The row records positive evidential bias (contextual evidence for p).

Equations

• Zheng2025.evidentialBias row = (row.feature? "evidential_bias" == some "true")

def Zheng2025.epistemicBias (row : Data.Examples.LinguisticExample) : Bool

The row records negative epistemic bias (prior belief against p).

Equations

• Zheng2025.epistemicBias row = (row.feature? "epistemic_bias" == some "true")

def Zheng2025.unexpectedEvidence (row : Data.Examples.LinguisticExample) : Bool

The row records evidence unexpected to the speaker.

Equations

• Zheng2025.unexpectedEvidence row = (row.feature? "unexpected_evidence" == some "true")

def Zheng2025.felicitous (row : Data.Examples.LinguisticExample) : Bool

The row's nandao-Q is felicitous.

Equations

• Zheng2025.felicitous row = (row.judgment == Features.Judgment.acceptable)

theorem Zheng2025.evidential_bias_necessary : (List.filter felicitous Examples.all).all evidentialBias = true

All felicitous nandao-Qs have evidential bias (Generalization 1).

theorem Zheng2025.epistemic_bias_not_necessary : (List.filter (fun (d : Data.Examples.LinguisticExample) => felicitous d && !epistemicBias d) Examples.all).length > 0

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

theorem Zheng2025.epistemic_bias_not_sufficient : (List.filter (fun (d : Data.Examples.LinguisticExample) => epistemicBias d && !felicitous d) Examples.all).length > 0

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

theorem Zheng2025.unexpectedness_necessary : (List.filter felicitous Examples.all).all unexpectedEvidence = true

All felicitous nandao-Qs have unexpected evidence (Generalization 4).

Kernel-theoretic felicity conditions

A nandao question is felicitous when some evidence in the kernel raises the probability of the prejacent, the kernel conflicts with the prior information state U — the beliefs, norms, and desires in place before encountering the evidence — and the prejacent is not directly settled (condition (11); its "significantly raises" (≫) is sharpened to strict raising). The last conjunct is the presupposition of [vFG10]'s kernelMust.

def Zheng2025.evidenceRaises {W : Type u_1} (p φ : Set W) : Prop

Evidence p raises the probability of φ under the uniform counting measure on a finite W: P(φ|p) > P(φ).

Equations

• Zheng2025.evidenceRaises p φ = ((p ∩ φ).ncard * Nat.card W > φ.ncard * p.ncard)

@[instance_reducible]

instance Zheng2025.instDecidableEvidenceRaisesOfFintypeOfDecidablePred {W : Type u_1} (p φ : W → Prop) [Fintype W] [DecidablePred p] [DecidablePred φ] : Decidable (evidenceRaises p φ)

Equations

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

def Zheng2025.evidenceSupports {W : Type u_1} (k : Modality.Kernel W) (φ : W → Prop) : Prop

Some proposition in K raises the probability of φ (condition (11i)).

Equations

• Zheng2025.evidenceSupports k φ = ∃ p ∈ k.props, Zheng2025.evidenceRaises p φ

def Zheng2025.unexpected {W : Type u_1} (k : Modality.Kernel W) (u : List (W → Prop)) : Prop

The evidence in K is unexpected given the prior information state U (condition (11ii)).

Equations

• Zheng2025.unexpected k u = Disjoint k.base (Intensional.Premise.propIntersection u)

def Zheng2025.nandaoFelicitous {W : Type u_1} (k : Modality.Kernel W) (u : List (W → Prop)) (φ : W → Prop) : Prop

Nandao φ? is felicitous iff some evidence in K raises P(φ), the evidence is unexpected given the prior state U, and φ is not directly settled in K (condition (11), final version for polar questions).

Equations

• Zheng2025.nandaoFelicitous k u φ = (Zheng2025.evidenceSupports k φ ∧ Zheng2025.unexpected k u ∧ ¬k.directlySettles φ)

The dripping-raincoat scenario (exx. 2–3, 5)

K = {wearingRaincoat}: direct evidence that someone entered with a wet coat. U = {expectDry}: prior expectation of no rain (doxastic or normative).

inductive Zheng2025.World : Type

Four worlds for the raincoat scenario, where it rains, the sprinkler ran (wet coat without rain), it is dry, or nothing is known.

• rain : World
• sprinkler : World
• dry : World
• unknown : World

@[instance_reducible]

instance Zheng2025.instDecidableEqWorld : DecidableEq World

Equations

• Zheng2025.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Zheng2025.instReprWorld : Repr World

Equations

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

def Zheng2025.instReprWorld.repr : World → ℕ → Std.Format

Equations

• Zheng2025.instReprWorld.repr Zheng2025.World.rain prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Zheng2025.World.rain")).group prec✝
• Zheng2025.instReprWorld.repr Zheng2025.World.sprinkler prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Zheng2025.World.sprinkler")).group prec✝
• Zheng2025.instReprWorld.repr Zheng2025.World.dry prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Zheng2025.World.dry")).group prec✝
• Zheng2025.instReprWorld.repr Zheng2025.World.unknown prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Zheng2025.World.unknown")).group prec✝

@[instance_reducible]

instance Zheng2025.instInhabitedWorld : Inhabited World

Equations

• Zheng2025.instInhabitedWorld = { default := Zheng2025.instInhabitedWorld.default }

@[instance_reducible]

instance Zheng2025.instFintypeWorld : Fintype World

Equations

• Zheng2025.instFintypeWorld = { elems := { val := ↑Zheng2025.World.enumList, nodup := Zheng2025.World.enumList_nodup }, complete := Zheng2025.instFintypeWorld._proof_1 }

@[reducible, inline]

abbrev Zheng2025.wearingRaincoat : World → Prop

B enters wearing a dripping raincoat: true where the coat is wet.

Equations

• Zheng2025.wearingRaincoat w = (w = Zheng2025.World.rain ∨ w = Zheng2025.World.sprinkler)

@[reducible, inline]

abbrev Zheng2025.expectDry : World → Prop

A's prior expectation of no rain.

Equations

• Zheng2025.expectDry w = (w = Zheng2025.World.dry ∨ w = Zheng2025.World.unknown)

@[reducible, inline]

abbrev Zheng2025.isRaining : World → Prop

It is raining outside.

Equations

• Zheng2025.isRaining x✝ = (x✝ = Zheng2025.World.rain)

def Zheng2025.raincoatK : Modality.Kernel World

The raincoat kernel, carrying the direct evidence of the wet coat.

Equations

• Zheng2025.raincoatK = { props := [Zheng2025.wearingRaincoat] }

def Zheng2025.dryU : List (World → Prop)

The prior information state in which A expects dry weather.

Equations

• Zheng2025.dryU = [Zheng2025.expectDry]

theorem Zheng2025.raincoat_nandao_felicitous : nandaoFelicitous raincoatK dryU isRaining

"Nandao waimian xiayu-le ma?" is felicitous in the dripping-raincoat context (exx. 2–3).

theorem Zheng2025.no_evidence_nandao_infelicitous : ¬nandaoFelicitous { props := [] } dryU isRaining

Without evidence, nandao is infelicitous (ex. 5 ctx 2).

theorem Zheng2025.expected_evidence_infelicitous : ¬nandaoFelicitous raincoatK [wearingRaincoat] isRaining

When evidence is expected (K compatible with U), nandao is infelicitous (ex. 6 ctx 2, transposed to the raincoat scenario: a prior expectation of wet coats makes the evidence unremarkable).

Bias classification

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

Nandao requires contextual evidence for p — Zheng's evidential classification, the lexical face of evidential_bias_necessary.

Equations

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

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

Nandao does not require epistemic bias — it is 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 : Modality.Kernel World) (u : List (World → Prop)) (φ : World → Prop) (h : nandaoFelicitous k u φ) : evidenceSupports k φ

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

Selectional profile (§4)

Nandao combines only with polar questions — it is incompatible with declaratives and wh-questions ([Zhe25] ex. 12, after [Xu12a]) — and §4 derives the restriction from the felicity conditions: only a polar prejacent both follows from the contextual evidence and targets the source of the incompatibility.

theorem Zheng2025.nandao_distribution : ¬Mandarin.QuestionParticles.nandao.LicensedIn Particle.ClauseType.declarative ∧ Mandarin.QuestionParticles.nandao.LicensedIn Particle.ClauseType.polar ∧ ¬Mandarin.QuestionParticles.nandao.LicensedIn Particle.ClauseType.constituent

The fragment's recorded distribution matches the paper's ex. 12.

Singleton-alternative presupposition (parallel to kya:)

[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), captured by the shared Question.IsSingleton predicate.

theorem Zheng2025.nandao_felicitous_ofSet {W : Type u_1} (p : Set W) : (Question.ofSet p).IsSingleton

nandao is felicitous on a one-cell ("highlighted") polar — the same canonical good-input case as kya:. Both this and BhattDayal2020.kya_felicitous_singleton_polar are isSingleton_ofSet, capturing the kya:–nandao convergence [BD20] draw from [Xu12a].

Integrated felicity

Nandao's full felicity has two independent layers: the sister content is singleton — alt Q = {p} for a unique witness p (semantic well-formedness, the [BD20] eq. 23 presupposition) — and the kernel-bias check nandaoFelicitous k u p holds for the witness (discourse felicity in context). The integrated predicate composes them; a Layer-1 failure (a non-trivial two-cell polar) blocks felicity regardless of (k, u).

def Zheng2025.nandaoFullFelicity (Q : Question World) (k : Modality.Kernel World) (u : List (World → Prop)) (p : Set World) : Prop

The integrated felicity of nandao conjoins the singleton presupposition alt Q = {p} with the kernel-bias check on the witness. The witness p is supplied externally; for the noncomputable choice from a SingletonQuestion use SingletonQuestion.witness.

Equations

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

theorem Zheng2025.nandaoFullFelicity_isSingleton {Q : Question World} {k : Modality.Kernel World} {u : List (World → Prop)} {p : Set World} (h : nandaoFullFelicity Q k u p) : Q.IsSingleton

Integrated felicity entails the singleton presupposition.

theorem Zheng2025.nandaoFullFelicity_kernel {Q : Question World} {k : Modality.Kernel World} {u : List (World → Prop)} {p : Set World} (h : nandaoFullFelicity Q k u p) : nandaoFelicitous k u p

Integrated felicity entails the kernel-bias check on the witness.

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

A two-cell Hamblin polar polar p₀ (with non-trivial p₀) admits no integrated-felicity witness: no kernel and prior state can rescue it, because the singleton requirement alt Q = {p} already fails.

theorem Zheng2025.nandaoFullFelicity_declarative_iff {p : Set World} (k : Modality.Kernel World) (u : List (World → Prop)) : nandaoFullFelicity (Question.ofSet p) k u p ↔ nandaoFelicitous k u p

On a one-cell sister ofSet p, integrated felicity is exactly the kernel-bias check on p: the singleton component holds by alt_ofSet.

theorem Zheng2025.biasedUse_integrated_felicity : nandaoFullFelicity (Question.ofSet isRaining) raincoatK dryU isRaining

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. The row Examples.ex2 records the same scenario (ex. 2) as empirical data.