Polar Question Bias — vocabulary

[romero-2024] [romero-han-2004] [ladd-1981] [BG00]

Theory-neutral vocabulary for polar question bias, shared by lexical fragments and the theory layer. Polar questions come in three forms — PosQ, LoNQ, HiNQ — sensitive to two independent bias dimensions: original speaker bias (the speaker's prior epistemic lean) and contextual evidence bias (evidence available in the current discourse).

This file carries only the directional enums and the form/bias compatibility tables, so that Fragment lexical entries can record which bias a particle requires without importing modal machinery; VERUM semantics with modal frames lives study-side (Studies/RomeroHan2004.lean).

Main definitions

• PQForm — the three polar-question forms.
• OriginalBias, ContextualEvidence — the two directional bias dimensions.
• EvidentialBiasStrength — strength of contextual-evidence bias by negation scope.
• originalBiasOK, evidenceBiasOK — Romero's compatibility tables.

inductive Question.PQForm : Type

The three polar question forms ([romero-2024] §1).

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.

@[instance_reducible]

instance Question.instDecidableEqPQForm : DecidableEq PQForm

Equations

• Question.instDecidableEqPQForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Question.instReprPQForm.repr : PQForm → ℕ → Std.Format

Equations

• Question.instReprPQForm.repr Question.PQForm.PosQ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Question.PQForm.PosQ")).group prec✝
• Question.instReprPQForm.repr Question.PQForm.LoNQ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Question.PQForm.LoNQ")).group prec✝
• Question.instReprPQForm.repr Question.PQForm.HiNQ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Question.PQForm.HiNQ")).group prec✝

@[instance_reducible]

instance Question.instReprPQForm : Repr PQForm

Equations

• Question.instReprPQForm = { reprPrec := Question.instReprPQForm.repr }

@[instance_reducible]

instance Question.instFintypePQForm : Fintype PQForm

Equations

• Question.instFintypePQForm = { elems := { val := ↑Question.PQForm.enumList, nodup := Question.PQForm.enumList_nodup }, complete := Question.instFintypePQForm._proof_1 }

inductive Question.OriginalBias : Type

Original speaker bias: belief or expectation that p is true, based on the speaker's epistemic state prior to the current situation and exchange.

• forP : OriginalBias

  Speaker originally expected/believed p.

• neutral : OriginalBias

  Speaker had no prior expectation about p.

• againstP : OriginalBias

  Speaker originally expected/believed ¬p.

@[instance_reducible]

instance Question.instDecidableEqOriginalBias : DecidableEq OriginalBias

Equations

• Question.instDecidableEqOriginalBias x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Question.instReprOriginalBias.repr : OriginalBias → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Question.instReprOriginalBias : Repr OriginalBias

Equations

• Question.instReprOriginalBias = { reprPrec := Question.instReprOriginalBias.repr }

inductive Question.ContextualEvidence : Type

Contextual evidence bias ([BG00]): expectation about p induced by evidence available in the current discourse situation. A felicity condition on rising declaratives and a bias dimension for polar questions.

• forP : ContextualEvidence

  Current context provides evidence for p.

• neutral : ContextualEvidence

  No contextual evidence either way.

• againstP : ContextualEvidence

  Current context provides evidence against p.

@[instance_reducible]

instance Question.instDecidableEqContextualEvidence : DecidableEq ContextualEvidence

Equations

• Question.instDecidableEqContextualEvidence x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Question.instReprContextualEvidence : Repr ContextualEvidence

Equations

• Question.instReprContextualEvidence = { reprPrec := Question.instReprContextualEvidence.repr }

def Question.instReprContextualEvidence.repr : ContextualEvidence → ℕ → Std.Format

Equations

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

inductive Question.EvidentialBiasStrength : Type

Strength of contextual-evidence bias associated with a negation scope, bridging Romero's typology to Staňková's three-way Czech distinction: inner negation → strong (□_ev(¬p)), medial → weak (¬□_ev(p)), outer (FALSUM) → no □_ev involvement.

• strong : EvidentialBiasStrength

  Inner: □_ev(¬p).

• weak : EvidentialBiasStrength

  Medial: ¬□_ev(p).

• none_ : EvidentialBiasStrength

  Outer: FALSUM, not □_ev-based.

@[instance_reducible]

instance Question.instDecidableEqEvidentialBiasStrength : DecidableEq EvidentialBiasStrength

Equations

• Question.instDecidableEqEvidentialBiasStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Question.instReprEvidentialBiasStrength.repr : EvidentialBiasStrength → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Question.instReprEvidentialBiasStrength : Repr EvidentialBiasStrength

Equations

• Question.instReprEvidentialBiasStrength = { reprPrec := Question.instReprEvidentialBiasStrength.repr }

def Question.originalBiasOK : PQForm → OriginalBias → Bool

Original speaker bias conditions on PQ forms ([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

• Question.originalBiasOK Question.PQForm.PosQ Question.OriginalBias.forP = true
• Question.originalBiasOK Question.PQForm.PosQ Question.OriginalBias.neutral = true
• Question.originalBiasOK Question.PQForm.PosQ Question.OriginalBias.againstP = true
• Question.originalBiasOK Question.PQForm.LoNQ Question.OriginalBias.forP = true
• Question.originalBiasOK Question.PQForm.LoNQ Question.OriginalBias.neutral = true
• Question.originalBiasOK Question.PQForm.LoNQ Question.OriginalBias.againstP = false
• Question.originalBiasOK Question.PQForm.HiNQ Question.OriginalBias.forP = true
• Question.originalBiasOK Question.PQForm.HiNQ Question.OriginalBias.neutral = false
• Question.originalBiasOK Question.PQForm.HiNQ Question.OriginalBias.againstP = false

theorem Question.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 ([ladd-1981], [romero-han-2004]).

theorem Question.posQ_neutral_ok : originalBiasOK PQForm.PosQ OriginalBias.neutral = true

PosQs can be used in neutral contexts.

theorem Question.loNQ_neutral_ok : originalBiasOK PQForm.LoNQ OriginalBias.neutral = true

LoNQs can be neutral.

def Question.evidenceBiasOK : PQForm → ContextualEvidence → Bool

Contextual evidence bias conditions on PQ forms ([romero-2024] Table 2, [BG00]).

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

Equations

• Question.evidenceBiasOK Question.PQForm.PosQ Question.ContextualEvidence.forP = true
• Question.evidenceBiasOK Question.PQForm.PosQ Question.ContextualEvidence.neutral = true
• Question.evidenceBiasOK Question.PQForm.PosQ Question.ContextualEvidence.againstP = false
• Question.evidenceBiasOK Question.PQForm.LoNQ Question.ContextualEvidence.forP = false
• Question.evidenceBiasOK Question.PQForm.LoNQ Question.ContextualEvidence.neutral = false
• Question.evidenceBiasOK Question.PQForm.LoNQ Question.ContextualEvidence.againstP = true
• Question.evidenceBiasOK Question.PQForm.HiNQ Question.ContextualEvidence.forP = false
• Question.evidenceBiasOK Question.PQForm.HiNQ Question.ContextualEvidence.neutral = true
• Question.evidenceBiasOK Question.PQForm.HiNQ Question.ContextualEvidence.againstP = true

theorem Question.loNQ_requires_evidence_against_p : evidenceBiasOK PQForm.LoNQ ContextualEvidence.forP = false ∧ evidenceBiasOK PQForm.LoNQ ContextualEvidence.neutral = false ∧ evidenceBiasOK PQForm.LoNQ ContextualEvidence.againstP = true

LoNQs require contextual evidence against p ([BG00]).

theorem Question.hiNQ_evidence_against_ok : evidenceBiasOK PQForm.HiNQ ContextualEvidence.againstP = true

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

theorem Question.hiNQ_evidence_neutral_ok : evidenceBiasOK PQForm.HiNQ ContextualEvidence.neutral = true

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