Documentation

Linglib.Theories.Semantics.Modality.BiasedPQ

Biased Polar Questions #

@cite{bring-gunlogson-2000} @cite{ladd-1981} @cite{repp-2013} @cite{romero-2019} @cite{romero-2024} @cite{romero-han-2004} @cite{simik-2024} @cite{stankova-2025}

Cross-linguistic framework for polar question bias, following @cite{romero-2024}. Polar questions come in three forms — PosQ, LoNQ, HiNQ — which differ in sensitivity to two independent bias dimensions: original speaker bias and contextual evidence bias.

Two Bias Dimensions #

Original speaker bias: The speaker's prior epistemic state (belief/expectation) about p before the current exchange.
Contextual evidence bias: Expectation about p induced by evidence that becomes available during the current exchange.

Three Theoretical Lines for High Negation #

@cite{romero-2020} clusters analyses into three lines:

Line a: Σ_neg at the expressed proposition level
Line b: VERUM/FALSUM
Line c: ¬ASSERT at the speech act level

We formalize VERUM and FALSUM (line b) using existing Kratzer modal and CommonGround infrastructure, as this is the line adopted by Staňková (2026) for Czech.

inductive Semantics.Modality.BiasedPQ.PQForm :

The three polar question forms (@cite{romero-2024} §1, exx. 1–3).

These forms are cross-linguistically attested and constitute the fundamental typology for polar question bias research.

PosQ : PQForm
Positive question: [p?]. "Is Jane coming?"
LoNQ : PQForm
Low negation question: [not p?]. "Is Jane not coming?"
HiNQ : PQForm
High negation question: [n't p?]. "Isn't Jane coming?" In Czech: interrogative (VSO) word order.

Instances For

instance Semantics.Modality.BiasedPQ.instDecidableEqPQForm :

DecidableEq PQForm

Equations

Semantics.Modality.BiasedPQ.instDecidableEqPQForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Modality.BiasedPQ.instBEqPQForm :

Equations

Semantics.Modality.BiasedPQ.instBEqPQForm = { beq := Semantics.Modality.BiasedPQ.instBEqPQForm.beq }

def Semantics.Modality.BiasedPQ.instBEqPQForm.beq :

PQForm → PQForm → Bool

Equations

Semantics.Modality.BiasedPQ.instBEqPQForm.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Semantics.Modality.BiasedPQ.instReprPQForm.repr :

PQForm → ℕ → Std.Format

Equations

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

Instances For

instance Semantics.Modality.BiasedPQ.instReprPQForm :

Equations

Semantics.Modality.BiasedPQ.instReprPQForm = { reprPrec := Semantics.Modality.BiasedPQ.instReprPQForm.repr }

inductive Semantics.Modality.BiasedPQ.OriginalBias :

Original speaker bias.

Belief or expectation of the speaker that p is true, based on her epistemic state prior to the current situational context and conversational exchange.

forP : OriginalBias
Speaker originally expected/believed p.
neutral : OriginalBias
Speaker had no prior expectation about p.
againstP : OriginalBias
Speaker originally expected/believed ¬p.

Instances For

instance Semantics.Modality.BiasedPQ.instDecidableEqOriginalBias :

DecidableEq OriginalBias

Equations

Semantics.Modality.BiasedPQ.instDecidableEqOriginalBias x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Modality.BiasedPQ.instBEqOriginalBias :

BEq OriginalBias

Equations

Semantics.Modality.BiasedPQ.instBEqOriginalBias = { beq := Semantics.Modality.BiasedPQ.instBEqOriginalBias.beq }

def Semantics.Modality.BiasedPQ.instBEqOriginalBias.beq :

OriginalBias → OriginalBias → Bool

Equations

Semantics.Modality.BiasedPQ.instBEqOriginalBias.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Semantics.Modality.BiasedPQ.instReprOriginalBias.repr :

OriginalBias → ℕ → Std.Format

Equations

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

Instances For

instance Semantics.Modality.BiasedPQ.instReprOriginalBias :

Repr OriginalBias

Equations

Semantics.Modality.BiasedPQ.instReprOriginalBias = { reprPrec := Semantics.Modality.BiasedPQ.instReprOriginalBias.repr }

def Semantics.Modality.BiasedPQ.originalBiasOK :

PQForm → OriginalBias → Bool

Original speaker bias conditions on PQ forms (@cite{romero-2024} Table 1).

Only HiNQ mandatorily conveys original speaker bias for p. LoNQ can convey bias for p but can also be neutral. PosQ is compatible with bias for ¬p or neutrality but was not tested for bias for p.

Equations

Instances For

theorem Semantics.Modality.BiasedPQ.hiNQ_requires_bias_for_p :

originalBiasOK PQForm.HiNQ OriginalBias.neutral = false ∧ originalBiasOK PQForm.HiNQ OriginalBias.againstP = false ∧ originalBiasOK PQForm.HiNQ OriginalBias.forP = true

HiNQs mandatorily convey original speaker bias for p (@cite{ladd-1981}, @cite{romero-han-2004}).

theorem Semantics.Modality.BiasedPQ.posQ_neutral_ok :

originalBiasOK PQForm.PosQ OriginalBias.neutral = true

PosQs can be used in neutral contexts.

theorem Semantics.Modality.BiasedPQ.loNQ_neutral_ok :

originalBiasOK PQForm.LoNQ OriginalBias.neutral = true

LoNQs can be neutral.

def Semantics.Modality.BiasedPQ.evidenceBiasOK :

PQForm → ContextualEvidence → Bool

Contextual evidence bias conditions on PQ forms (@cite{romero-2024} Table 2, @cite{bring-gunlogson-2000}).

PosQ requires evidence for p (or neutral). LoNQ requires evidence against p. Outer-HiNQ is felicitous with neutral or against-p evidence.

Equations

Instances For

theorem Semantics.Modality.BiasedPQ.loNQ_requires_evidence_against_p :

evidenceBiasOK PQForm.LoNQ Core.Discourse.Commitment.ContextualEvidence.forP = false ∧ evidenceBiasOK PQForm.LoNQ Core.Discourse.Commitment.ContextualEvidence.neutral = false ∧ evidenceBiasOK PQForm.LoNQ Core.Discourse.Commitment.ContextualEvidence.againstP = true

LoNQs require contextual evidence against p (@cite{bring-gunlogson-2000}).

theorem Semantics.Modality.BiasedPQ.hiNQ_evidence_against_ok :

evidenceBiasOK PQForm.HiNQ Core.Discourse.Commitment.ContextualEvidence.againstP = true

HiNQs are felicitous with evidence against p (contradiction scenarios).

theorem Semantics.Modality.BiasedPQ.hiNQ_evidence_neutral_ok :

evidenceBiasOK PQForm.HiNQ Core.Discourse.Commitment.ContextualEvidence.neutral = true

HiNQs are also felicitous with neutral evidence (suggestion scenarios).

def Semantics.Modality.BiasedPQ.verum (epistemic : Kratzer.ModalBase) (conversational : Kratzer.OrderingSource) (cg : Core.CommonGround.BContextSet Attitudes.Intensional.World) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) :

VERUM operator (@cite{romero-han-2004}, line b).

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

"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 CG. This is a double universal: necessity over epistemic alternatives, then necessity over conversational goals.

Equations

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

Instances For

structure Semantics.Modality.BiasedPQ.FalsumContent :

FALSUM operator (@cite{repp-2013}, @cite{romero-2019}, @cite{romero-2024} def. 33).

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

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

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

atIssue : BProp Attitudes.Intensional.World
At-issue content: ¬p
cgManagement : Attitudes.Intensional.World → Prop
CG-management: p should not be added to CG. Modeled as: the speaker considers it epistemically possible that p, but p is not CG-entailed.

Instances For

def Semantics.Modality.BiasedPQ.mkFalsum (epistemic : Kratzer.ModalBase) (conversational : Kratzer.OrderingSource) (cg : Core.CommonGround.BContextSet Attitudes.Intensional.World) (p : BProp Attitudes.Intensional.World) :

Construct FALSUM content for a proposition p.

Equations

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

Instances For

theorem Semantics.Modality.BiasedPQ.falsum_atIssue_is_negation (ep : Kratzer.ModalBase) (cv : Kratzer.OrderingSource) (cg : Core.CommonGround.BContextSet Attitudes.Intensional.World) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) :

(mkFalsum ep cv cg p).atIssue w = !p w

FALSUM's at-issue content is propositional negation.

structure Semantics.Modality.BiasedPQ.FalsumCZ :

Czech FALSUM (@cite{simik-2024} 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:

Weak commitment: epistemic possibility rather than necessity/belief
Not tied to speaker/addressee: attitude holder g(1) can be anyone
Commitment not at issue: it is a presupposition/conventional implicature
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 : BProp Attitudes.Intensional.World
At-issue content: ¬p (same as standard FALSUM)
definedness : Attitudes.Intensional.World → Prop
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 : Attitudes.Intensional.World → Prop
CG-management: p is not part of the common ground at w.

Instances For

def Semantics.Modality.BiasedPQ.mkFalsumCZ (attitudeEpi : Kratzer.ModalBase) (ordering : Kratzer.OrderingSource) (cg : Core.CommonGround.BContextSet Attitudes.Intensional.World) (p : BProp Attitudes.Intensional.World) :

Construct @cite{simik-2024}'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.

Instances For

theorem Semantics.Modality.BiasedPQ.falsumCZ_atIssue_is_negation (ep : Kratzer.ModalBase) (cv : Kratzer.OrderingSource) (cg : Core.CommonGround.BContextSet Attitudes.Intensional.World) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) :

(mkFalsumCZ ep cv cg p).atIssue w = !p w

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

theorem Semantics.Modality.BiasedPQ.standard_falsum_entails_CZ_definedness (ep : Kratzer.ModalBase) (cv : Kratzer.OrderingSource) (cg : Core.CommonGround.BContextSet Attitudes.Intensional.World) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hStd : (Kratzer.bestWorlds ep cv w).any p = true) :

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

def Semantics.Modality.BiasedPQ.loosenOrderingSource :

Kratzer.OrderingSource → (loosened : Kratzer.OrderingSource) → Kratzer.OrderingSource

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

@cite{simik-2024} §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.Modality.BiasedPQ.loosenOrderingSource x✝ loosened = loosened

Instances For

theorem Semantics.Modality.BiasedPQ.nahodou_widens_domain (ep : Kratzer.ModalBase) (cv cvLoose : Kratzer.OrderingSource) (cg : Core.CommonGround.BContextSet Attitudes.Intensional.World) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hSubset : ∀ w' ∈ Kratzer.bestWorlds ep cv w, w' ∈ 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.

theorem Semantics.Modality.BiasedPQ.nahodou_widens_domain.List.mem_of_subset {α : Type} {l1 l2 : List α} {x : α} (h : ∀ y ∈ l1, y ∈ l2) (hx : x ∈ l1) :

x ∈ l2

structure Semantics.Modality.BiasedPQ.EvidentialBiasFlavor :

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 : Kratzer.ModalBase
stereotypical : Kratzer.OrderingSource

Instances For

def Semantics.Modality.BiasedPQ.EvidentialBiasFlavor.toKratzerParams (f : EvidentialBiasFlavor) :

Kratzer.KratzerParams

Equations

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

Instances For

def Semantics.Modality.BiasedPQ.evidentialNecessity (f : EvidentialBiasFlavor) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) :

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

Equations

Semantics.Modality.BiasedPQ.evidentialNecessity f p w = Semantics.Modality.Kratzer.necessity f.contextBase f.stereotypical p w

Instances For

def Semantics.Modality.BiasedPQ.evidentialPossibility (f : EvidentialBiasFlavor) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) :

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

Equations

Semantics.Modality.BiasedPQ.evidentialPossibility f p w = Semantics.Modality.Kratzer.possibility f.contextBase f.stereotypical p w

Instances For

theorem Semantics.Modality.BiasedPQ.evidentialBias_duality (f : EvidentialBiasFlavor) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) :

(evidentialNecessity f p w == !evidentialPossibility f (fun (w' : Attitudes.Intensional.World) => !p w') w) = true

□_ev satisfies modal duality.

def Semantics.Modality.BiasedPQ.innerBias (f : EvidentialBiasFlavor) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) :

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

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

Equations

Semantics.Modality.BiasedPQ.innerBias f p w = Semantics.Modality.BiasedPQ.evidentialNecessity f (fun (w' : Semantics.Attitudes.Intensional.World) => !p w') w

Instances For

def Semantics.Modality.BiasedPQ.medialBias (f : EvidentialBiasFlavor) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) :

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

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

Equations

Semantics.Modality.BiasedPQ.medialBias f p w = !Semantics.Modality.BiasedPQ.evidentialNecessity f p w

Instances For

theorem Semantics.Modality.BiasedPQ.inner_entails_medial (f : EvidentialBiasFlavor) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hSerial : (Kratzer.bestWorlds f.contextBase f.stereotypical w).length > 0) (hInner : innerBias f p w = true) :

medialBias f p w = true

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

def Semantics.Modality.BiasedPQ.falsumFocusRequirement :

Core.InformationStructure.DiscourseStatus

Outer negation (FALSUM) is obligatorily focused (Staňková 2026 §3.2, §4).

FALSUM targets discourse polarity — whether p is or is not in the CG. Focus on FALSUM generates Rooth alternatives on polarity.

The focus semantic value of FALSUM: {λw[p ∉ CG], λw[p ∈ CG]}.

Equations

Semantics.Modality.BiasedPQ.falsumFocusRequirement = Core.InformationStructure.DiscourseStatus.focused

Instances For

def Semantics.Modality.BiasedPQ.falsumAlternatives (cg : Core.CommonGround.BContextSet Attitudes.Intensional.World) (p : BProp Attitudes.Intensional.World) :

List (Attitudes.Intensional.World → Prop)

FALSUM generates exactly two alternatives (polarity contrast).

Equations

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

Instances For

theorem Semantics.Modality.BiasedPQ.falsum_binary_alternatives (cg : Core.CommonGround.BContextSet Attitudes.Intensional.World) (p : BProp Attitudes.Intensional.World) :

(falsumAlternatives cg p).length = 2

inductive Semantics.Modality.BiasedPQ.EvidentialBiasStrength :

Strength of evidential bias associated with a negation scope configuration.

This bridges Romero's two-dimensional bias typology to Staňková's three-way Czech distinction:

Inner neg → strong contextual evidence bias (must be ¬p)
Medial neg → weak contextual evidence bias (doesn't have to be p)
Outer neg (FALSUM) → original speaker bias, no □_ev involvement

Instances For

instance Semantics.Modality.BiasedPQ.instDecidableEqEvidentialBiasStrength :

DecidableEq EvidentialBiasStrength

Equations

Semantics.Modality.BiasedPQ.instDecidableEqEvidentialBiasStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Modality.BiasedPQ.instBEqEvidentialBiasStrength :

BEq EvidentialBiasStrength

Equations

Semantics.Modality.BiasedPQ.instBEqEvidentialBiasStrength = { beq := Semantics.Modality.BiasedPQ.instBEqEvidentialBiasStrength.beq }

def Semantics.Modality.BiasedPQ.instBEqEvidentialBiasStrength.beq :

EvidentialBiasStrength → EvidentialBiasStrength → Bool

Equations

Semantics.Modality.BiasedPQ.instBEqEvidentialBiasStrength.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Semantics.Modality.BiasedPQ.instReprEvidentialBiasStrength :

Repr EvidentialBiasStrength

Equations

Semantics.Modality.BiasedPQ.instReprEvidentialBiasStrength = { reprPrec := Semantics.Modality.BiasedPQ.instReprEvidentialBiasStrength.repr }

def Semantics.Modality.BiasedPQ.instReprEvidentialBiasStrength.repr :

EvidentialBiasStrength → ℕ → Std.Format

Equations

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

Instances For