Zheng (2025): Nandao-Qs, When Surprise Sparks Inquiry

This file formalizes [Zhe25]'s felicity conditions for Mandarin nandao questions, which are driven by unexpected contextual evidence rather than by the speaker's epistemic bias. The conditions are stated over [vFG10]'s kernel, the set of propositions directly available in the context: some piece of evidence in the kernel raises the probability of the prejacent (evidenceSupports), the kernel conflicts with the information state U in place before the evidence, the beliefs, norms, desires or default expectations of the speaker (unexpected), and the prejacent is not itself directly settled in the kernel (nandaoFelicitous, the final condition (11)). Generalized to questions through the instantiations of the question's highlighted property, (13), the first condition requires every instantiation to follow from the evidence (nandaoQFelicitous), which reduces to (11) for a polar question (nandaoQFelicitous_singleton) and excludes a wh-question one of whose instantiations no evidence supports (not_nandaoQFelicitous_of_unsupported), the paper's derivation of the distribution recorded in the fragment (nandao_distribution, (12)).

The dripping-raincoat scenario of (2), (3) and (5) is a four-world model: the question is felicitous whether the conflicting state is a belief that it is not raining or the default expectation that people do not wear raincoats (raincoat_nandao_felicitous, raincoat_default_felicitous), and infelicitous without the evidence (no_evidence_infelicitous) or when the evidence is expected (expected_evidence_infelicitous), which is (6). The link to rhetorical questions in §5 runs through [Far25]'s closed-question condition: a closed polar question is resolved in the common ground whenever the speaker's beliefs are consistent with it (resolved_of_closed_polar), the argument of the paper's footnote on (17).

Implementation notes

• The paper's "significantly raises" is sharpened to strict raising of the conditional probability under the uniform counting measure on a finite set of worlds (evidenceRaises).
• The information state U is a list of propositions, like the kernel; the default state of the paper's footnote is one such proposition.
• Highlighted properties enter only through their set of instantiations.

References

• [Zhe25]
• [vFG10]
• [Xu12a]
• [Far25]

Kernel-theoretic felicity conditions

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 φ, (11i).

Equations

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

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

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

Equations

• Zheng2025.unexpected k u = Disjoint k.base {w : W | sInf u w}

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

Nandao φ? is felicitous iff some evidence in K raises the probability of φ, the evidence is unexpected given the prior state U, and φ is not directly settled in K, (11).

Equations

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

Questions through their highlighted property, (13)

def Zheng2025.nandaoQFelicitous {W : Type u_1} (k : Modality.Kernel W) (u f : Set (W → Prop)) : Prop

Nandao Q? is felicitous iff some evidence in K raises the probability of every instantiation of the question's highlighted property, the evidence is unexpected, and no instantiation is directly settled in K.

Equations

• Zheng2025.nandaoQFelicitous k u f = ((∃ p ∈ k.props, ∀ φ ∈ f, Zheng2025.evidenceRaises p φ) ∧ Zheng2025.unexpected k u ∧ ∀ φ ∈ f, ¬k.directlySettles φ)

theorem Zheng2025.nandaoQFelicitous_singleton {W : Type u_1} (k : Modality.Kernel W) (u : Set (W → Prop)) (φ : W → Prop) : nandaoQFelicitous k u {φ} ↔ nandaoFelicitous k u φ

For a polar question, whose highlighted property has the prejacent as its one instantiation, (13) is (11).

theorem Zheng2025.not_nandaoQFelicitous_of_unsupported {W : Type u_1} {k : Modality.Kernel W} {u f : Set (W → Prop)} {φ : W → Prop} (hφ : φ ∈ f) (h : ∀ p ∈ k.props, ¬evidenceRaises p φ) : ¬nandaoQFelicitous k u f

A question one of whose instantiations no evidence in the kernel supports, such as what is the weather outside? with its sunny instantiation, is infelicitous with nandao.

theorem Zheng2025.nandao_distribution : ¬Mandarin.QuestionParticles.nandao.LicensedIn Clause.SentenceType.declarative ∧ Mandarin.QuestionParticles.nandao.LicensedIn Clause.SentenceType.polar ∧ ¬Mandarin.QuestionParticles.nandao.LicensedIn Clause.SentenceType.constituent

Nandao combines with polar questions only, (12), as the fragment records.

def Zheng2025.nandaoProfile : Question.BiasProfile

The bias profile of nandao: it requires contextual evidence for the prejacent, the paper's evidential bias, and places no requirement on the prior state of the speaker, so that a neutral prior state is compatible with it, (3).

Equations

• Zheng2025.nandaoProfile = { evidential := Question.BiasValue.plus Polarity.positive, epistemic := Finset.univ }

The dripping-raincoat scenario, (2), (3) and (5)

inductive Zheng2025.World : Type

The worlds of the scenario: it rains, the sprinkler ran and the coat is wet without rain, it is dry, or the weather is unknown.

• 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.

Equations

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

@[reducible, inline]

abbrev Zheng2025.expectDry : World → Prop

A's belief that it is not raining, (2).

Equations

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

@[reducible, inline]

abbrev Zheng2025.expectNoRaincoat : World → Prop

The default expectation that people do not wear raincoats, the state of (3) and of context 1 of (5).

Equations

• Zheng2025.expectNoRaincoat w = ¬Zheng2025.wearingRaincoat w

@[reducible, inline]

abbrev Zheng2025.isRaining : World → Prop

It is raining outside, the prejacent.

Equations

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

def Zheng2025.raincoatK : Modality.Kernel World

The kernel carrying the direct evidence of the wet coat.

Equations

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

theorem Zheng2025.raincoat_nandao_felicitous : nandaoFelicitous raincoatK {expectDry} isRaining

Nandao waimian xiayu-le ma? is felicitous when A believes it is not raining, (2).

theorem Zheng2025.raincoat_default_felicitous : nandaoFelicitous raincoatK {expectNoRaincoat} isRaining

The question is equally felicitous when A has no belief about the weather and only the default expectation that people do not wear raincoats, (3) and context 1 of (5): epistemic bias is not necessary.

theorem Zheng2025.no_evidence_infelicitous (u : Set (World → Prop)) : ¬nandaoFelicitous { props := ∅ } u isRaining

Without the evidence the question is infelicitous, whatever A believes, contexts 2 and 3 of (5): epistemic bias is not sufficient.

theorem Zheng2025.expected_evidence_infelicitous : ¬nandaoFelicitous raincoatK {wearingRaincoat} isRaining

When the evidence is expected, the prior state already allowing wet coats, the question is infelicitous, as in context 2 of (6).

Closed questions and rhetorical use, §5

def Zheng2025.Closed {W : Type u_1} (issue : Set (Set W)) (cg dox : Set W) : Prop

[Far25]'s closed-question condition: every alternative of the issue not already entailed by the common ground is doxastically inconsistent with it, given the speaker's doxastic state dox.

Equations

• Zheng2025.Closed issue cg dox = ∀ p ∈ issue, ¬cg ⊆ p → Disjoint (cg ∩ p) dox

theorem Zheng2025.resolved_of_closed_polar {W : Type u_1} {p cg dox : Set W} (hcons : (cg ∩ dox).Nonempty) (h : Closed {p, pᶜ} cg dox) : cg ⊆ p ∨ cg ⊆ pᶜ

A closed polar question is resolved in the common ground, provided the speaker's beliefs are consistent with it: if neither alternative were entailed, both would be inconsistent, and so would the common ground itself.