structure Semantics.Questions.VerumFocus.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 Semantics.Questions.VerumFocus.EpistemicAccessibility (W : Type u_1) : Type u_1

Epistemic accessibility: worlds compatible with agent's knowledge

Equations

• Semantics.Questions.VerumFocus.EpistemicAccessibility W = (W → W → Bool)

@[reducible, inline]

abbrev Semantics.Questions.VerumFocus.ConversationalAccessibility (W : Type u_1) : Type u_1

Conversational accessibility: worlds compatible with agent's conversational goals

Equations

• Semantics.Questions.VerumFocus.ConversationalAccessibility W = (W → W → Bool)

structure Semantics.Questions.VerumFocus.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 Semantics.Questions.VerumFocus.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 Semantics.Questions.VerumFocus.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

• Semantics.Questions.VerumFocus.verum cgMembership epiWorlds convWorlds w p = (epiWorlds w).all fun (w' : W) => (convWorlds w').all fun (w'' : W) => cgMembership w'' p

structure Semantics.Questions.VerumFocus.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 Semantics.Questions.VerumFocus.balancedQuestion {W : Type u_1} (p : W → Bool) : QuestionPartition W

Standard balanced polar question: {p, ¬p}

Equations

• Semantics.Questions.VerumFocus.balancedQuestion p = { cell1 := p, cell2 := fun (w : W) => !p w, pronounced := p }

def Semantics.Questions.VerumFocus.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 Semantics.Questions.VerumFocus.NegQuestionReading : Type

Reading type for negative polar questions

• PI : NegQuestionReading
• NI : NegQuestionReading

instance Semantics.Questions.VerumFocus.instReprNegQuestionReading : Repr NegQuestionReading

Equations

• Semantics.Questions.VerumFocus.instReprNegQuestionReading = { reprPrec := Semantics.Questions.VerumFocus.instReprNegQuestionReading.repr }

def Semantics.Questions.VerumFocus.instReprNegQuestionReading.repr : NegQuestionReading → ℕ → Std.Format

Equations

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

instance Semantics.Questions.VerumFocus.instDecidableEqNegQuestionReading : DecidableEq NegQuestionReading

Equations

• Semantics.Questions.VerumFocus.instDecidableEqNegQuestionReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Semantics.Questions.VerumFocus.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 Semantics.Questions.VerumFocus.NegQuestionLF.proposition {W : Type u_1} : NegQuestionLF W → W → Bool

Extract the embedded proposition

Equations

• (Semantics.Questions.VerumFocus.NegQuestionLF.piLF p).proposition = p
• (Semantics.Questions.VerumFocus.NegQuestionLF.niLF p).proposition = p

def Semantics.Questions.VerumFocus.NegQuestionLF.reading {W : Type u_1} : NegQuestionLF W → NegQuestionReading

Get the reading type

Equations

• (Semantics.Questions.VerumFocus.NegQuestionLF.piLF p).reading = Semantics.Questions.VerumFocus.NegQuestionReading.PI
• (Semantics.Questions.VerumFocus.NegQuestionLF.niLF p).reading = Semantics.Questions.VerumFocus.NegQuestionReading.NI

def Semantics.Questions.VerumFocus.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.

structure Semantics.Questions.VerumFocus.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 Semantics.Questions.VerumFocus.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

• Semantics.Questions.VerumFocus.epistemicImplicature Semantics.Questions.VerumFocus.NegQuestionReading.PI _p = "Speaker believes p (expected 'yes')"
• Semantics.Questions.VerumFocus.epistemicImplicature Semantics.Questions.VerumFocus.NegQuestionReading.NI _p = "Speaker believes ¬p (expected 'no')"

def Semantics.Questions.VerumFocus.implicaturePolarity (reading : NegQuestionReading) : String

Derive the implicature direction

Equations

• Semantics.Questions.VerumFocus.implicaturePolarity Semantics.Questions.VerumFocus.NegQuestionReading.PI = "positive"
• Semantics.Questions.VerumFocus.implicaturePolarity Semantics.Questions.VerumFocus.NegQuestionReading.NI = "negative"

inductive Semantics.Questions.VerumFocus.PolarityItem : Type

Polarity item type

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

instance Semantics.Questions.VerumFocus.instReprPolarityItem : Repr PolarityItem

Equations

• Semantics.Questions.VerumFocus.instReprPolarityItem = { reprPrec := Semantics.Questions.VerumFocus.instReprPolarityItem.repr }

def Semantics.Questions.VerumFocus.instReprPolarityItem.repr : PolarityItem → ℕ → Std.Format

Equations

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

instance Semantics.Questions.VerumFocus.instDecidableEqPolarityItem : DecidableEq PolarityItem

Equations

• Semantics.Questions.VerumFocus.instDecidableEqPolarityItem = Semantics.Questions.VerumFocus.instDecidableEqPolarityItem.decEq

def Semantics.Questions.VerumFocus.instDecidableEqPolarityItem.decEq (x✝ x✝¹ : PolarityItem) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Questions.VerumFocus.instDecidableEqPolarityItem.decEq (Semantics.Questions.VerumFocus.PolarityItem.PPI a) (Semantics.Questions.VerumFocus.PolarityItem.NPI a_1) = isFalse ⋯
• Semantics.Questions.VerumFocus.instDecidableEqPolarityItem.decEq (Semantics.Questions.VerumFocus.PolarityItem.NPI a) (Semantics.Questions.VerumFocus.PolarityItem.PPI a_1) = isFalse ⋯

def Semantics.Questions.VerumFocus.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

• Semantics.Questions.VerumFocus.isLicensed (Semantics.Questions.VerumFocus.PolarityItem.PPI a) Semantics.Questions.VerumFocus.NegQuestionReading.PI = true
• Semantics.Questions.VerumFocus.isLicensed (Semantics.Questions.VerumFocus.PolarityItem.NPI a) Semantics.Questions.VerumFocus.NegQuestionReading.NI = true
• Semantics.Questions.VerumFocus.isLicensed (Semantics.Questions.VerumFocus.PolarityItem.PPI a) Semantics.Questions.VerumFocus.NegQuestionReading.NI = false
• Semantics.Questions.VerumFocus.isLicensed (Semantics.Questions.VerumFocus.PolarityItem.NPI a) Semantics.Questions.VerumFocus.NegQuestionReading.PI = false

def Semantics.Questions.VerumFocus.too : PolarityItem

Common polarity items

Equations

• Semantics.Questions.VerumFocus.too = Semantics.Questions.VerumFocus.PolarityItem.PPI "too"

def Semantics.Questions.VerumFocus.some_ : PolarityItem

Equations

• Semantics.Questions.VerumFocus.some_ = Semantics.Questions.VerumFocus.PolarityItem.PPI "some"

def Semantics.Questions.VerumFocus.already : PolarityItem

Equations

• Semantics.Questions.VerumFocus.already = Semantics.Questions.VerumFocus.PolarityItem.PPI "already"

def Semantics.Questions.VerumFocus.either : PolarityItem

Equations

• Semantics.Questions.VerumFocus.either = Semantics.Questions.VerumFocus.PolarityItem.NPI "either"

def Semantics.Questions.VerumFocus.any : PolarityItem

Equations

• Semantics.Questions.VerumFocus.any = Semantics.Questions.VerumFocus.PolarityItem.NPI "any"

def Semantics.Questions.VerumFocus.yet : PolarityItem

Equations

• Semantics.Questions.VerumFocus.yet = Semantics.Questions.VerumFocus.PolarityItem.NPI "yet"

theorem Semantics.Questions.VerumFocus.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 Semantics.Questions.VerumFocus.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 Semantics.Questions.VerumFocus.instReprVerumSource.repr : VerumSource → ℕ → Std.Format

Equations

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

instance Semantics.Questions.VerumFocus.instReprVerumSource : Repr VerumSource

Equations

• Semantics.Questions.VerumFocus.instReprVerumSource = { reprPrec := Semantics.Questions.VerumFocus.instReprVerumSource.repr }

instance Semantics.Questions.VerumFocus.instDecidableEqVerumSource : DecidableEq VerumSource

Equations

• Semantics.Questions.VerumFocus.instDecidableEqVerumSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Questions.VerumFocus.necessarilyTriggersVerum : VerumSource → Bool

Does this source necessarily trigger VERUM?

Equations

• Semantics.Questions.VerumFocus.necessarilyTriggersVerum Semantics.Questions.VerumFocus.VerumSource.preposedNegation = true
• Semantics.Questions.VerumFocus.necessarilyTriggersVerum Semantics.Questions.VerumFocus.VerumSource.reallyAdverb = true
• Semantics.Questions.VerumFocus.necessarilyTriggersVerum Semantics.Questions.VerumFocus.VerumSource.auxiliaryFocus = true
• Semantics.Questions.VerumFocus.necessarilyTriggersVerum Semantics.Questions.VerumFocus.VerumSource.negationFocus = true

theorem Semantics.Questions.VerumFocus.preposed_negation_forces_verum : necessarilyTriggersVerum VerumSource.preposedNegation = true

Romero & Han's Generalization 1

Relationship to Polarity.lean

@cite{romero-han-2004}

Van Rooy & Šafářová (2003) and @cite{romero-han-2004} are complementary:

1. vR&S (Polarity.lean): Explains which polar question to use

   • Decision-theoretic: choose question that maximizes expected utility
   • Predicts bias based on speaker's credences and stakes

2. R&H (this file): Explains why preposed negation forces bias

   • VERUM semantics: preposed negation introduces FOR-SURE-CG
   • Explains structural ambiguity (PI vs NI)
   • Explains polarity item licensing

Together they explain:

• WHY certain forms have bias (VERUM)
• WHEN speakers choose biased forms (decision theory)

structure Semantics.Questions.VerumFocus.IntegrationWithPolarity : Type

Marker type for cross-theory reference

• decisionTheoreticChoice : Bool

  vR&Š explains question choice

• verumSourceOfBias : Bool

  R&H explains structural source of bias

def Semantics.Questions.VerumFocus.examplePI : 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

• Semantics.Questions.VerumFocus.examplePI = Semantics.Questions.VerumFocus.NegQuestionLF.piLF fun (x : Unit) => true

def Semantics.Questions.VerumFocus.exampleNI : 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

• Semantics.Questions.VerumFocus.exampleNI = Semantics.Questions.VerumFocus.NegQuestionLF.niLF fun (x : Unit) => true