Romero & Han (2004): Negative Yes/No Questions and Epistemic Bias

@cite{romero-han-2004} @cite{ladd-1981}

Core Contribution

Preposed negation in yes/no questions forces an epistemic implicature via the VERUM operator (FOR-SURE-CG). Ladd's PI/NI ambiguity is scope ambiguity:

• PI: [Q [not [VERUM [p]]]] → speaker believes p, double-checking
• NI: [Q [VERUM [not [p]]]] → speaker believes ¬p, double-checking

The VERUM operator is the conversational-epistemic mechanism:

FOR-SURE-CG_x(p) = ∀w' ∈ Epi_x(w)[∀w'' ∈ Conv_x(w')[p ∈ CG_w'']]

"For all worlds compatible with x's knowledge, for all worlds compatible with x's conversational goals, p is in the Common Ground." Short form: "It is for sure that we should add p to the CG."

Results

1. VERUM creates unbalanced partitions: {FOR-SURE-CG(p), ¬FOR-SURE-CG(p)} rather than {p, ¬p}.
2. Ladd's PI/NI ambiguity is scope ambiguity over VERUM and negation.
3. Epistemic implicature follows from intent/pronunciation:
   • Asserting ¬FOR-SURE-CG(p) (PI) implicates belief in p
   • Asserting FOR-SURE-CG(¬p) (NI) implicates belief in ¬p

Related Work

• Phenomena/Questions/Studies/Holmberg2016.lean — complementary analysis. R&H explains the structural source of bias (preposed negation forces an epistemic expectation via VERUM); Holmberg explains cross-linguistic answer variation (the [±Pol] feature, negation height). Both agree that negative questions denote an unbalanced partition; R&H derives this from VERUM scope, Holmberg from negation-height + [±Pol].
• van Rooy & Šafářová (2003) decision-theoretic complement: vR&Š explain which polar question to use; R&H explain why certain forms have bias. (Apparatus deleted in Bool/List → Prop/Set migration; reinstate in Prop/Set form when needed.)
• Theories/Syntax/Minimalism/Polarity.lean — the [±Pol] feature.

structure RomeroHan2004.Verum.CGWorld (W : Type u_1) : Type u_1

A world type with Common Ground

• world : W

  The possible world

• cg : List (W → Bool)

  The Common Ground at this world (set of propositions)

@[reducible, inline]

abbrev RomeroHan2004.Verum.EpistemicAccessibility (W : Type u_1) : Type u_1

Epistemic accessibility: worlds compatible with agent's knowledge

Equations

• RomeroHan2004.Verum.EpistemicAccessibility W = (W → W → Bool)

@[reducible, inline]

abbrev RomeroHan2004.Verum.ConversationalAccessibility (W : Type u_1) : Type u_1

Conversational accessibility: worlds compatible with agent's conversational goals

Equations

• RomeroHan2004.Verum.ConversationalAccessibility W = (W → W → Bool)

structure RomeroHan2004.Verum.VerumFrame (W : Type u_1) : Type u_1

Full modal frame for VERUM semantics

• worlds : List W

  Set of worlds

• epiAccessible : EpistemicAccessibility W

  Epistemic accessibility (Epi_x)

• convAccessible : ConversationalAccessibility W

  Conversational accessibility (Conv_x)

• commonGround : W → List (W → Bool)

  Common Ground function: for each world, what's in the CG

def RomeroHan2004.Verum.forSureCG {W : Type u_1} (frame : VerumFrame W) (w : W) (p : W → Bool) : Bool

FOR-SURE-CG: The VERUM operator.

∀w' ∈ Epi_x(w)[∀w'' ∈ Conv_x(w')[p ∈ CG_w'']]

For all epistemic alternatives w', for all conversational alternatives w'', p is in the Common Ground at w''.

This captures: "It is for sure that we should add p to the CG."

Equations

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

def RomeroHan2004.Verum.verum {W : Type u_1} [DecidableEq W] (cgMembership : W → (W → Bool) → Bool) (epiWorlds convWorlds : W → List W) (w : W) (p : W → Bool) : Bool

Simplified VERUM for finite models

Equations

• RomeroHan2004.Verum.verum cgMembership epiWorlds convWorlds w p = (epiWorlds w).all fun (w' : W) => (convWorlds w').all fun (w'' : W) => cgMembership w'' p

structure RomeroHan2004.Verum.QuestionPartition (W : Type u_1) : Type u_1

A polar question partition

• cell1 : W → Bool

  The two cells of the partition

• cell2 : W → Bool
• pronounced : W → Bool

  Which cell is "pronounced" (the surface form asks about)

def RomeroHan2004.Verum.balancedQuestion {W : Type u_1} (p : W → Bool) : QuestionPartition W

Standard balanced polar question: {p, ¬p}

Equations

• RomeroHan2004.Verum.balancedQuestion p = { cell1 := p, cell2 := fun (w : W) => !p w, pronounced := p }

def RomeroHan2004.Verum.verumQuestion {W : Type u_1} [DecidableEq W] (cgMembership : W → (W → Bool) → Bool) (epiWorlds convWorlds : W → List W) (p : W → Bool) (pronounceNeg : Bool) : QuestionPartition W

Unbalanced VERUM question: {FOR-SURE-CG(p), ¬FOR-SURE-CG(p)}

When VERUM is present, the partition is about epistemic commitment to CG membership, not about p's truth directly.

Equations

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

inductive RomeroHan2004.Verum.NegQuestionReading : Type

Reading type for negative polar questions

• PI : NegQuestionReading
• NI : NegQuestionReading

@[implicit_reducible]

instance RomeroHan2004.Verum.instReprNegQuestionReading : Repr NegQuestionReading

Equations

• RomeroHan2004.Verum.instReprNegQuestionReading = { reprPrec := RomeroHan2004.Verum.instReprNegQuestionReading.repr }

def RomeroHan2004.Verum.instReprNegQuestionReading.repr : NegQuestionReading → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RomeroHan2004.Verum.instDecidableEqNegQuestionReading : DecidableEq NegQuestionReading

Equations

• RomeroHan2004.Verum.instDecidableEqNegQuestionReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive RomeroHan2004.Verum.NegQuestionLF (W : Type u_1) : Type u_1

LF structure for negative polar questions

• piLF {W : Type u_1} : (W → Bool) → NegQuestionLF W

  PI: [Q [not [VERUM [p]]]]

• niLF {W : Type u_1} : (W → Bool) → NegQuestionLF W

  NI: [Q [VERUM [not [p]]]]

def RomeroHan2004.Verum.NegQuestionLF.proposition {W : Type u_1} : NegQuestionLF W → W → Bool

Extract the embedded proposition

Equations

• (RomeroHan2004.Verum.NegQuestionLF.piLF p).proposition = p
• (RomeroHan2004.Verum.NegQuestionLF.niLF p).proposition = p

def RomeroHan2004.Verum.NegQuestionLF.reading {W : Type u_1} : NegQuestionLF W → NegQuestionReading

Get the reading type

Equations

• (RomeroHan2004.Verum.NegQuestionLF.piLF p).reading = RomeroHan2004.Verum.NegQuestionReading.PI
• (RomeroHan2004.Verum.NegQuestionLF.niLF p).reading = RomeroHan2004.Verum.NegQuestionReading.NI

def RomeroHan2004.Verum.interpretNegQuestion {W : Type u_1} [DecidableEq W] (cgMembership : W → (W → Bool) → Bool) (epiWorlds convWorlds : W → List W) (lf : NegQuestionLF W) : QuestionPartition W

Interpret a negative question LF as a partition

• PI: {¬FOR-SURE-CG(p), FOR-SURE-CG(p)}
• NI: {FOR-SURE-CG(¬p), ¬FOR-SURE-CG(¬p)}

Equations

• One or more equations did not get rendered due to their size.
• RomeroHan2004.Verum.interpretNegQuestion cgMembership epiWorlds convWorlds (RomeroHan2004.Verum.NegQuestionLF.piLF p) = RomeroHan2004.Verum.verumQuestion cgMembership epiWorlds convWorlds p true

structure RomeroHan2004.Verum.SpeakerEpistemicState (W : Type u_1) : Type u_1

Speaker's prior epistemic state

• beliefWorlds : List W

  Worlds compatible with speaker's beliefs

• believes : (W → Bool) → Bool

  Does speaker believe p?

def RomeroHan2004.Verum.epistemicImplicature {W : Type u_1} (reading : NegQuestionReading) (_p : W → Bool) : String

Implicature from pronounced cell

The pronounced cell of a VERUM question implicates the speaker's prior belief:

• PI pronounces ¬FOR-SURE-CG(p) → implicates belief in p
• NI pronounces FOR-SURE-CG(¬p) → implicates belief in ¬p

Equations

• RomeroHan2004.Verum.epistemicImplicature RomeroHan2004.Verum.NegQuestionReading.PI _p = "Speaker believes p (expected 'yes')"
• RomeroHan2004.Verum.epistemicImplicature RomeroHan2004.Verum.NegQuestionReading.NI _p = "Speaker believes ¬p (expected 'no')"

def RomeroHan2004.Verum.implicaturePolarity (reading : NegQuestionReading) : String

Derive the implicature direction

Equations

• RomeroHan2004.Verum.implicaturePolarity RomeroHan2004.Verum.NegQuestionReading.PI = "positive"
• RomeroHan2004.Verum.implicaturePolarity RomeroHan2004.Verum.NegQuestionReading.NI = "negative"

inductive RomeroHan2004.Verum.PolarityItem : Type

Polarity item type

• PPI : String → PolarityItem
• NPI : String → PolarityItem

def RomeroHan2004.Verum.instReprPolarityItem.repr : PolarityItem → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RomeroHan2004.Verum.instReprPolarityItem : Repr PolarityItem

Equations

• RomeroHan2004.Verum.instReprPolarityItem = { reprPrec := RomeroHan2004.Verum.instReprPolarityItem.repr }

@[implicit_reducible]

instance RomeroHan2004.Verum.instDecidableEqPolarityItem : DecidableEq PolarityItem

Equations

• RomeroHan2004.Verum.instDecidableEqPolarityItem = RomeroHan2004.Verum.instDecidableEqPolarityItem.decEq

def RomeroHan2004.Verum.instDecidableEqPolarityItem.decEq (x✝ x✝¹ : PolarityItem) : Decidable (x✝ = x✝¹)

Equations

• RomeroHan2004.Verum.instDecidableEqPolarityItem.decEq (RomeroHan2004.Verum.PolarityItem.PPI a) (RomeroHan2004.Verum.PolarityItem.PPI b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• RomeroHan2004.Verum.instDecidableEqPolarityItem.decEq (RomeroHan2004.Verum.PolarityItem.PPI a) (RomeroHan2004.Verum.PolarityItem.NPI a_1) = isFalse ⋯
• RomeroHan2004.Verum.instDecidableEqPolarityItem.decEq (RomeroHan2004.Verum.PolarityItem.NPI a) (RomeroHan2004.Verum.PolarityItem.PPI a_1) = isFalse ⋯
• RomeroHan2004.Verum.instDecidableEqPolarityItem.decEq (RomeroHan2004.Verum.PolarityItem.NPI a) (RomeroHan2004.Verum.PolarityItem.NPI b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def RomeroHan2004.Verum.isLicensed (item : PolarityItem) (reading : NegQuestionReading) : Bool

Check if polarity item is licensed under a reading

• PPIs licensed under PI reading (in scope of ¬FOR-SURE-CG)
• NPIs licensed under NI reading (in scope of VERUM over negation)

Equations

• RomeroHan2004.Verum.isLicensed (RomeroHan2004.Verum.PolarityItem.PPI a) RomeroHan2004.Verum.NegQuestionReading.PI = true
• RomeroHan2004.Verum.isLicensed (RomeroHan2004.Verum.PolarityItem.NPI a) RomeroHan2004.Verum.NegQuestionReading.NI = true
• RomeroHan2004.Verum.isLicensed (RomeroHan2004.Verum.PolarityItem.PPI a) RomeroHan2004.Verum.NegQuestionReading.NI = false
• RomeroHan2004.Verum.isLicensed (RomeroHan2004.Verum.PolarityItem.NPI a) RomeroHan2004.Verum.NegQuestionReading.PI = false

def RomeroHan2004.Verum.too : PolarityItem

Common polarity items

Equations

• RomeroHan2004.Verum.too = RomeroHan2004.Verum.PolarityItem.PPI "too"

def RomeroHan2004.Verum.some_ : PolarityItem

Equations

• RomeroHan2004.Verum.some_ = RomeroHan2004.Verum.PolarityItem.PPI "some"

def RomeroHan2004.Verum.already : PolarityItem

Equations

• RomeroHan2004.Verum.already = RomeroHan2004.Verum.PolarityItem.PPI "already"

def RomeroHan2004.Verum.either : PolarityItem

Equations

• RomeroHan2004.Verum.either = RomeroHan2004.Verum.PolarityItem.NPI "either"

def RomeroHan2004.Verum.any : PolarityItem

Equations

• RomeroHan2004.Verum.any = RomeroHan2004.Verum.PolarityItem.NPI "any"

def RomeroHan2004.Verum.yet : PolarityItem

Equations

• RomeroHan2004.Verum.yet = RomeroHan2004.Verum.PolarityItem.NPI "yet"

theorem RomeroHan2004.Verum.ppi_implies_pi (item : PolarityItem) (reading : NegQuestionReading) : isLicensed item reading = true → match item with | PolarityItem.PPI a => reading = NegQuestionReading.PI | PolarityItem.NPI a => reading = NegQuestionReading.NI

Ladd's generalization: PPIs → PI, NPIs → NI

inductive RomeroHan2004.Verum.VerumSource : Type

Sources that contribute VERUM to the LF

• preposedNegation : VerumSource

  Preposed negation: "Doesn't John..."

• reallyAdverb : VerumSource

  The adverb "really": "Does John really..."

• auxiliaryFocus : VerumSource

  Focus on auxiliary: "DOES John..."

• negationFocus : VerumSource

  Focus on negation: "Does John NOT..."

def RomeroHan2004.Verum.instReprVerumSource.repr : VerumSource → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RomeroHan2004.Verum.instReprVerumSource : Repr VerumSource

Equations

• RomeroHan2004.Verum.instReprVerumSource = { reprPrec := RomeroHan2004.Verum.instReprVerumSource.repr }

@[implicit_reducible]

instance RomeroHan2004.Verum.instDecidableEqVerumSource : DecidableEq VerumSource

Equations

• RomeroHan2004.Verum.instDecidableEqVerumSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RomeroHan2004.Verum.necessarilyTriggersVerum : VerumSource → Bool

Does this source necessarily trigger VERUM?

Equations

• RomeroHan2004.Verum.necessarilyTriggersVerum RomeroHan2004.Verum.VerumSource.preposedNegation = true
• RomeroHan2004.Verum.necessarilyTriggersVerum RomeroHan2004.Verum.VerumSource.reallyAdverb = true
• RomeroHan2004.Verum.necessarilyTriggersVerum RomeroHan2004.Verum.VerumSource.auxiliaryFocus = true
• RomeroHan2004.Verum.necessarilyTriggersVerum RomeroHan2004.Verum.VerumSource.negationFocus = true

theorem RomeroHan2004.Verum.preposed_negation_forces_verum : necessarilyTriggersVerum VerumSource.preposedNegation = true

Romero & Han's Generalization 1

structure RomeroHan2004.NegativeQuestionDatum : Type

A negative question datum records epistemic bias.

• sentence : String

  The sentence

• negationPosition : String

  Negation position

• epistemicBias : Option String

  Epistemic bias (positive, negative, or none)

• notes : String

  Notes

@[implicit_reducible]

instance RomeroHan2004.instReprNegativeQuestionDatum : Repr NegativeQuestionDatum

Equations

• RomeroHan2004.instReprNegativeQuestionDatum = { reprPrec := RomeroHan2004.instReprNegativeQuestionDatum.repr }

def RomeroHan2004.instReprNegativeQuestionDatum.repr : NegativeQuestionDatum → ℕ → Std.Format

Equations

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

def RomeroHan2004.preposedNegation : NegativeQuestionDatum

Preposed negation forces positive bias.

Equations

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

def RomeroHan2004.nonPreposedNegation : NegativeQuestionDatum

Non-preposed negation allows neutral reading.

Equations

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

def RomeroHan2004.reallyBias : NegativeQuestionDatum

Adverb "really" triggers positive bias.

Equations

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

theorem RomeroHan2004.preposed_triggers_verum : Verum.necessarilyTriggersVerum Verum.VerumSource.preposedNegation = true

Preposed negation necessarily triggers VERUM (bridge to Verum apparatus).

theorem RomeroHan2004.really_triggers_verum : Verum.necessarilyTriggersVerum Verum.VerumSource.reallyAdverb = true

"Really" also triggers VERUM.

@cite{ladd-1981}: the same negative question form is ambiguous between positive-implicature (PI) and negative-implicature (NI) readings, disambiguated by polarity items.

structure RomeroHan2004.LaddAmbiguityDatum : Type

A Ladd ambiguity datum: same form, opposite implicatures.

• question : String

  The question template

• piVariant : String

  Positive-implicature variant (with PPIs like "too")

• niVariant : String

  Negative-implicature variant (with NPIs like "either")

• piReading : String

  PI interpretation

• niReading : String

  NI interpretation

@[implicit_reducible]

instance RomeroHan2004.instReprLaddAmbiguityDatum : Repr LaddAmbiguityDatum

Equations

• RomeroHan2004.instReprLaddAmbiguityDatum = { reprPrec := RomeroHan2004.instReprLaddAmbiguityDatum.repr }

def RomeroHan2004.instReprLaddAmbiguityDatum.repr : LaddAmbiguityDatum → ℕ → Std.Format

Equations

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

def RomeroHan2004.laddJaneComing : LaddAmbiguityDatum

Classic Ladd example: too vs either.

Equations

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

def RomeroHan2004.laddSomeAny : LaddAmbiguityDatum

Some vs any.

Equations

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

def RomeroHan2004.laddAlreadyYet : LaddAmbiguityDatum

Already vs yet.

Equations

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

theorem RomeroHan2004.ppi_diagnoses_pi : Verum.isLicensed Verum.too Verum.NegQuestionReading.PI = true

PPIs diagnose PI readings; NPIs diagnose NI readings. Bridge to the polarity-item licensing apparatus.

theorem RomeroHan2004.npi_diagnoses_ni : Verum.isLicensed Verum.either Verum.NegQuestionReading.NI = true

theorem RomeroHan2004.ppi_blocks_ni : Verum.isLicensed Verum.too Verum.NegQuestionReading.NI = false

theorem RomeroHan2004.npi_blocks_pi : Verum.isLicensed Verum.either Verum.NegQuestionReading.PI = false

structure RomeroHan2004.CrossLinguisticDatum : Type

Cross-linguistic negative question data.

• language : String

  Language

• sentence : String

  Sentence

• gloss : String

  Gloss

• translation : String

  Translation

• biasStrategy : String

  How the language marks bias

def RomeroHan2004.instReprCrossLinguisticDatum.repr : CrossLinguisticDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RomeroHan2004.instReprCrossLinguisticDatum : Repr CrossLinguisticDatum

Equations

• RomeroHan2004.instReprCrossLinguisticDatum = { reprPrec := RomeroHan2004.instReprCrossLinguisticDatum.repr }

def RomeroHan2004.germanNegQ : CrossLinguisticDatum

German: clitic position determines PI vs NI.

Equations

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

def RomeroHan2004.spanishNegQ : CrossLinguisticDatum

Spanish: tampoco/también for NI/PI.

Equations

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

def RomeroHan2004.koreanNegQ : CrossLinguisticDatum

Korean: morphological marking.

Equations

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

def RomeroHan2004.bulgarianNegQ : CrossLinguisticDatum

Bulgarian: separate negation and question particles.

Equations

• RomeroHan2004.bulgarianNegQ = { language := "Bulgarian", sentence := "Ne dojde li Ivan?", gloss := "Not came Q Ivan?", translation := "Didn't Ivan come?", biasStrategy := "particle_order" }

def RomeroHan2004.greekNegQ : CrossLinguisticDatum

Modern Greek: dhen vs mi negation.

Equations

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

def RomeroHan2004.generalization1 : String

Generalization 1: preposed negation forces positive epistemic implicature.

Equations

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

def RomeroHan2004.generalization2 : String

Generalization 2: Ladd's p/¬p ambiguity.

Equations

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

def RomeroHan2004.examplePI : Verum.NegQuestionLF Unit

Example: "Doesn't John drink?" (PI reading)

LF: [Q [not [VERUM [John drinks]]]] Partition: {¬FOR-SURE-CG(drinks(j)), FOR-SURE-CG(drinks(j))} Pronounced: ¬FOR-SURE-CG(drinks(j)) Implicature: Speaker believes John drinks

Equations

• RomeroHan2004.examplePI = RomeroHan2004.Verum.NegQuestionLF.piLF fun (x : Unit) => true

def RomeroHan2004.exampleNI : Verum.NegQuestionLF Unit

Example: "Doesn't John drink?" (NI reading, with "either")

LF: [Q [VERUM [not [John drinks]]]] Partition: {FOR-SURE-CG(¬drinks(j)), ¬FOR-SURE-CG(¬drinks(j))} Pronounced: FOR-SURE-CG(¬drinks(j)) Implicature: Speaker believes John doesn't drink

Equations

• RomeroHan2004.exampleNI = RomeroHan2004.Verum.NegQuestionLF.niLF fun (x : Unit) => true