Biased Polar Questions — VERUM/FALSUM and the evidential-bias modal

[BG00] [Lad81] [Rep13] [Rom19] [Rom24] [RH04] [Sim24] [Sta25]

The modal machinery for polar question bias, building on the form and bias vocabulary in Semantics.Questions.Bias.Defs. Formalizes VERUM and FALSUM (line b of [Rom20]'s clustering — [RH04]) and the evidential-bias necessity modal □_ev using Kratzer modal and CommonGround infrastructure, the line adopted by Staňková (2026) for Czech.

Main definitions

• verum, FalsumContent/mkFalsum, FalsumCZ/mkFalsumCZ — VERUM and FALSUM.
• EvidentialBiasFlavor, evidentialNecessity/evidentialPossibility — □_ev.
• innerBias/medialBias, falsumAlternatives — scope interactions and focus.

VERUM ([RH04])

def Semantics.Questions.Bias.verum {W : Type u_1} (epistemic : Modality.Kratzer.ModalBase W) (conversational : Modality.Kratzer.OrderingSource W) (cg p : Set W) (w : W) : Prop

VERUM operator ([RH04], line b).

⟦VERUM_x⟧ = λp. λw. ∀w' ∈ Epi_x(w). ∀w'' ∈ Conv_x(w'). [p ∈ CommonGround]

"x is sure that p should be added to the Common Ground."

We model this as: in all epistemically accessible worlds where the speaker's conversational goals are fulfilled, p is in the CommonGround. This is a double universal: necessity over epistemic alternatives, then necessity over conversational goals.

Equations

• Semantics.Questions.Bias.verum epistemic conversational cg p w = ∀ w' ∈ Semantics.Modality.Kratzer.bestWorlds epistemic conversational w, cg w' ∧ p w'

structure Semantics.Questions.Bias.FalsumContent (W : Type u_2) : Type u_2

FALSUM operator ([Rep13], [Rom19], [Rom24] def. 33).

At-issue content: ¬p CommonGround-management content: ∀w' ∈ Epi(w). ∀w'' ∈ Conv(w'). [p ∉ CommonGround]

"x is sure that p should NOT be added to the Common Ground."

FALSUM is the CommonGround-management negation of VERUM. The at-issue content is simply ¬p, while the non-at-issue content (CommonGround-management) expresses that p is not to become common ground.

• atIssue : Set W

  At-issue content: ¬p

• cgManagement : Set W

  CommonGround-management: p should not be added to CommonGround. Modeled as: the speaker considers it epistemically possible that p, but p is not CommonGround-entailed.

def Semantics.Questions.Bias.mkFalsum {W : Type u_1} (epistemic : Modality.Kratzer.ModalBase W) (conversational : Modality.Kratzer.OrderingSource W) (cg p : Set W) : FalsumContent W

Construct FALSUM content for a proposition p.

Equations

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

theorem Semantics.Questions.Bias.falsum_atIssue_is_negation {W : Type u_1} (ep : Modality.Kratzer.ModalBase W) (cv : Modality.Kratzer.OrderingSource W) (cg p : Set W) (w : W) : (mkFalsum ep cv cg p).atIssue w ↔ ¬p w

FALSUM's at-issue content is propositional negation.

Czech FALSUM, FALSUM^CZ ([Sim24])

structure Semantics.Questions.Bias.FalsumCZ (W : Type u_2) : Type u_2

Czech FALSUM ([Sim24] eq. 44), weaker than standard FALSUM.

⟦FALSUM_1^CZ⟧^g(p) = λw : ∃w' ∈ EPI_{g(1)}(w)[p(w') = 1]. p ∉ CG_w

Key differences from Repp's FALSUM:

1. Weak commitment: epistemic possibility rather than necessity/belief
2. Not tied to speaker/addressee: attitude holder g(1) can be anyone
3. Commitment not at issue: it is a presupposition/conventional implicature
4. Not conventionally tied to conversational goals: the commitment need not be at stake in the conversation

This weaker version accounts for the broader distribution of Czech InterNPQs compared to English high negation PQs: Czech FALSUM^CZ is compatible with more bias configurations because it only requires epistemic possibility, not belief.

• atIssue : Set W

  At-issue content: ¬p (same as standard FALSUM)

• definedness : Set W

  Presupposition: attitude holder considers p epistemically possible. This is the definedness condition — the question is defined only if the attitude holder considers the positive prejacent possible.

• cgContent : Set W

  CommonGround-management: p is not part of the common ground at w.

def Semantics.Questions.Bias.mkFalsumCZ {W : Type u_1} (attitudeEpi : Modality.Kratzer.ModalBase W) (ordering : Modality.Kratzer.OrderingSource W) (cg p : Set W) : FalsumCZ W

Construct [Sim24]'s FALSUM^CZ for a proposition p.

The attitude holder's epistemic state is modeled via the modal base (their epistemic alternatives).

Equations

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

theorem Semantics.Questions.Bias.falsumCZ_atIssue_is_negation {W : Type u_1} (ep : Modality.Kratzer.ModalBase W) (cv : Modality.Kratzer.OrderingSource W) (cg p : Set W) (w : W) : (mkFalsumCZ ep cv cg p).atIssue w ↔ ¬p w

FALSUM^CZ at-issue content is still propositional negation.

theorem Semantics.Questions.Bias.standard_falsum_entails_CZ_definedness {W : Type u_1} (ep : Modality.Kratzer.ModalBase W) (cv : Modality.Kratzer.OrderingSource W) (cg p : Set W) (w : W) (hStd : ∃ w' ∈ Modality.Kratzer.bestWorlds ep cv w, p w') : (mkFalsumCZ ep cv cg p).definedness w

Standard FALSUM entails FALSUM^CZ definedness: if the speaker believes p is possible (necessity over goals), then they certainly consider it possible. This captures why standard FALSUM is a special case of FALSUM^CZ.

Náhodou as ordering-source modifier ([Sim24])

def Semantics.Questions.Bias.loosenOrderingSource {W : Type u_1} : Modality.Kratzer.OrderingSource W → (loosened : Modality.Kratzer.OrderingSource W) → Modality.Kratzer.OrderingSource W

Náhodou 'by chance' loosens the stereotypical ordering source of FALSUM^CZ to include more remote (less stereotypical) possibilities.

[Sim24] §5.1: "its function is to 'loosen' the default stereotypical ordering source of the epistemic modal contributed by FALSUM so as to include more remote (less likely) possibilities in the quantification domain of the modal."

Formally, náhodou replaces the ordering source g with a weaker g' such that Best(f, g', w) ⊇ Best(f, g, w). The resulting proposition is stronger because ruling out p in less likely worlds entails ruling it out in more likely worlds.

Equations

• Semantics.Questions.Bias.loosenOrderingSource x✝ loosened = loosened

theorem Semantics.Questions.Bias.nahodou_widens_domain {W : Type u_1} (ep : Modality.Kratzer.ModalBase W) (cv cvLoose : Modality.Kratzer.OrderingSource W) (cg p : Set W) (w : W) (hSubset : ∀ w' ∈ Modality.Kratzer.bestWorlds ep cv w, w' ∈ Modality.Kratzer.bestWorlds ep cvLoose w) : (mkFalsumCZ ep cv cg p).definedness w → (mkFalsumCZ ep cvLoose cg p).definedness w

With náhodou, FALSUM^CZ quantifies over a larger set of worlds, making the epistemic possibility condition easier to satisfy. This is why náhodou is licensed in contexts where the speaker's evidence is weaker — it signals willingness to explore remote possibilities.

Evidential-bias modal □_ev

structure Semantics.Questions.Bias.EvidentialBiasFlavor (W : Type u_2) : Type u_2

Evidential bias flavor (Staňková 2026 §3.1).

□_ev is a Kratzer necessity modal where:

• Modal base: the context set (what is established in the discourse)
• Ordering source: stereotypical/evidential (how "normal" a world is)
• Force: necessity

This captures evidential bias in PQs: the speaker's expectation about the answer, derived from contextual evidence rather than prior epistemic state. It corresponds to Romero's "contextual evidence bias" dimension.

• contextBase : Modality.Kratzer.ModalBase W
• stereotypical : Modality.Kratzer.OrderingSource W

def Semantics.Questions.Bias.EvidentialBiasFlavor.toKratzerParams {W : Type u_1} (f : EvidentialBiasFlavor W) : Modality.Kratzer.KratzerParams W

Equations

• f.toKratzerParams = { base := f.contextBase, ordering := f.stereotypical }

def Semantics.Questions.Bias.evidentialNecessity {W : Type u_1} (f : EvidentialBiasFlavor W) (p : Set W) (w : W) : Prop

Evidential necessity: ∀w' ∈ Best(f,g,w). p(w').

Equations

• Semantics.Questions.Bias.evidentialNecessity f p w = Semantics.Modality.Kratzer.necessity f.contextBase f.stereotypical p w

def Semantics.Questions.Bias.evidentialPossibility {W : Type u_1} (f : EvidentialBiasFlavor W) (p : Set W) (w : W) : Prop

Evidential possibility: ∃w' ∈ Best(f,g,w). p(w').

Equations

• Semantics.Questions.Bias.evidentialPossibility f p w = Semantics.Modality.Kratzer.possibility f.contextBase f.stereotypical p w

theorem Semantics.Questions.Bias.evidentialBias_duality {W : Type u_1} (f : EvidentialBiasFlavor W) (p : Set W) (w : W) : evidentialNecessity f p w ↔ ¬evidentialPossibility f (fun (w' : W) => ¬p w') w

□_ev satisfies modal duality. One of five sibling theorem dualitys — the box–diamond duality underlying the modal square of opposition (Core.Logic.Modal.modalSquare_relations).

Scope interactions: inner vs medial negation

def Semantics.Questions.Bias.innerBias {W : Type u_1} (f : EvidentialBiasFlavor W) (p : Set W) (w : W) : Prop

Inner negation scopes under □_ev: □_ev(¬p).

Strong evidential bias: based on the context, it must be that ¬p.

Equations

• Semantics.Questions.Bias.innerBias f p w = Semantics.Questions.Bias.evidentialNecessity f (fun (w' : W) => ¬p w') w

def Semantics.Questions.Bias.medialBias {W : Type u_1} (f : EvidentialBiasFlavor W) (p : Set W) (w : W) : Prop

Medial negation scopes over □_ev: ¬□_ev(p).

Weak evidential bias: it's not the case that p must hold.

Equations

• Semantics.Questions.Bias.medialBias f p w = ¬Semantics.Questions.Bias.evidentialNecessity f p w

theorem Semantics.Questions.Bias.inner_entails_medial {W : Type u_1} (f : EvidentialBiasFlavor W) (p : Set W) (w : W) (hSerial : (Modality.Kratzer.bestWorlds f.contextBase f.stereotypical w).Nonempty) (hInner : innerBias f p w) : medialBias f p w

Inner bias entails medial bias given seriality (D axiom): □_ev(¬p) → ¬□_ev(p), provided Best(f,g,w) is non-empty.

TODO: The seriality condition holds whenever the modal base is realistic (cf. Kratzer.realistic_is_serial).

Focus requirement on FALSUM ([Rom24])

Outer negation (FALSUM) is obligatorily focused.

FALSUM targets discourse polarity — whether p is or is not in the CommonGround. Focus on FALSUM generates Rooth alternatives on polarity. The focus semantic value of FALSUM is {λw[p ∉ CommonGround], λw[p ∈ CommonGround]}, computed by falsumAlternatives below.

def Semantics.Questions.Bias.falsumAlternatives {W : Type u_1} (cg p : Set W) : List (Set W)

FALSUM generates exactly two alternatives (polarity contrast).

Equations

• Semantics.Questions.Bias.falsumAlternatives cg p = [fun (x : W) => ¬∀ (w' : W), cg w' → p w', fun (x : W) => ∀ (w' : W), cg w' → p w']

theorem Semantics.Questions.Bias.falsum_binary_alternatives {W : Type u_1} (cg p : Set W) : (falsumAlternatives cg p).length = 2