Šimík (2024): Polar Question Semantics and Bias in Slavic

[Sim24] [BD20] [Day25] [ER23]

Šimík's cross-Slavic survey of polar-question particles classifies each particle by its left-peripheral layer in the [BD20] / [Day25] cartography [SAP [PerspP [CP ...]]].

The fragments in Fragments/{Russian,Bulgarian,Ukrainian,Polish, Slovenian,Serbian,Macedonian}/QuestionParticles.lean carry only theory-neutral lexical primitives (form, position, distribution). This study file overlays [Sim24]'s layer assignments and bias classification (evidentialRequirement) and proves the Slavic generalization that the neutral PQ-particle of each surveyed language sits at CP, while the biased mirative particles (the cross-Slavic RAZVE family) sit at PerspP.

Particle layer assignments

Language	Particle	Layer
Russian	li	CP
Russian	razve	PerspP
Bulgarian	li	CP
Bulgarian	nima	PerspP
Ukrainian	čy	CP
Ukrainian	xiba	PerspP
Polish	czy	CP
Polish	czyżby	PerspP
Slovenian	ali	CP
Serbian	da li	CP
Serbian	zar	PerspP
Macedonian	dali	CP

The Slavic data is the empirical anchor for the cross-linguistic claim that the cartography in [Day25] extends beyond Hindi-Urdu and Japanese to a much wider typological range.

The file also records [Sim24] §4.1's typology of default (unbiased) PQ strategies across ten Slavic languages (PQProfile).

Layer assignment for each Slavic Q-particle.

Each def records Šimík's classification of a Fragment particle. The _ argument is unused because the layer assignment is a theoretical overlay on the particle, not a computed property of its lexical fields.

def Simik2024.russianLi_layer : Particle → Features.QParticleLayer

Equations

• Simik2024.russianLi_layer x✝ = Features.QParticleLayer.cp

def Simik2024.russianRazve_layer : Particle → Features.QParticleLayer

Equations

• Simik2024.russianRazve_layer x✝ = Features.QParticleLayer.perspP

def Simik2024.bulgarianLi_layer : Particle → Features.QParticleLayer

Equations

• Simik2024.bulgarianLi_layer x✝ = Features.QParticleLayer.cp

def Simik2024.bulgarianNima_layer : Particle → Features.QParticleLayer

Equations

• Simik2024.bulgarianNima_layer x✝ = Features.QParticleLayer.perspP

def Simik2024.ukrainianCy_layer : Particle → Features.QParticleLayer

Equations

• Simik2024.ukrainianCy_layer x✝ = Features.QParticleLayer.cp

def Simik2024.ukrainianXiba_layer : Particle → Features.QParticleLayer

Equations

• Simik2024.ukrainianXiba_layer x✝ = Features.QParticleLayer.perspP

def Simik2024.polishCzy_layer : Particle → Features.QParticleLayer

Equations

• Simik2024.polishCzy_layer x✝ = Features.QParticleLayer.cp

def Simik2024.polishCzyzby_layer : Particle → Features.QParticleLayer

Equations

• Simik2024.polishCzyzby_layer x✝ = Features.QParticleLayer.perspP

def Simik2024.slovenianAli_layer : Particle → Features.QParticleLayer

Equations

• Simik2024.slovenianAli_layer x✝ = Features.QParticleLayer.cp

def Simik2024.serbianDaLi_layer : Particle → Features.QParticleLayer

Equations

• Simik2024.serbianDaLi_layer x✝ = Features.QParticleLayer.cp

def Simik2024.serbianZar_layer : Particle → Features.QParticleLayer

Equations

• Simik2024.serbianZar_layer x✝ = Features.QParticleLayer.perspP

def Simik2024.macedonianDali_layer : Particle → Features.QParticleLayer

Equations

• Simik2024.macedonianDali_layer x✝ = Features.QParticleLayer.cp

Cross-Slavic generalizations

theorem Simik2024.neutral_PQ_particles_are_CP : russianLi_layer Russian.QuestionParticles.li = Features.QParticleLayer.cp ∧ bulgarianLi_layer Bulgarian.QuestionParticles.li = Features.QParticleLayer.cp ∧ ukrainianCy_layer Ukrainian.QuestionParticles.cy = Features.QParticleLayer.cp ∧ polishCzy_layer Polish.QuestionParticles.czy = Features.QParticleLayer.cp ∧ slovenianAli_layer Slovenian.QuestionParticles.ali = Features.QParticleLayer.cp ∧ serbianDaLi_layer Serbian.QuestionParticles.daLi = Features.QParticleLayer.cp ∧ macedonianDali_layer Macedonian.QuestionParticles.dali = Features.QParticleLayer.cp

The neutral polar-question particle of every surveyed Slavic language sits at CP. Which particle counts as neutral is Šimík's classification, recorded below as evidentialRequirement.

theorem Simik2024.razve_family_is_PerspP : russianRazve_layer Russian.QuestionParticles.razve_ = Features.QParticleLayer.perspP ∧ bulgarianNima_layer Bulgarian.QuestionParticles.nima = Features.QParticleLayer.perspP ∧ ukrainianXiba_layer Ukrainian.QuestionParticles.xiba = Features.QParticleLayer.perspP ∧ polishCzyzby_layer Polish.QuestionParticles.czyzby = Features.QParticleLayer.perspP ∧ serbianZar_layer Serbian.QuestionParticles.zar_ = Features.QParticleLayer.perspP

The cross-Slavic RAZVE family — the mirative/dubitative particles that signal conflict between speaker's prior epistemic state and incoming contextual evidence — uniformly sits at PerspP.

def Simik2024.razveFamily : List Particle

The cross-Slavic RAZVE family as a list. Šimík's bias classification (§4.2): these require contextual evidence for p (evidentialRequirement), while the neutral PQ particles impose no bias requirement. The layer assignments above correlate — RAZVE = PerspP, neutral = CP — which is Šimík's analysis, not a lexical fact, so both classifications live here rather than on the fragment entries.

Equations

• Simik2024.razveFamily = [Russian.QuestionParticles.razve_, Bulgarian.QuestionParticles.nima, Ukrainian.QuestionParticles.xiba, Polish.QuestionParticles.czyzby, Serbian.QuestionParticles.zar_]

def Simik2024.evidentialRequirement (p : Particle) : Option Semantics.Questions.Bias.ContextualEvidence

Evidential requirement per Šimík: .forP for the RAZVE family, none for the neutral particles.

Equations

• Simik2024.evidentialRequirement p = if p ∈ Simik2024.razveFamily then some Semantics.Questions.Bias.ContextualEvidence.forP else none

Default PQ strategies

[Sim24] §4.1's typology of default (unbiased) polar-question strategies across ten Slavic languages. particle fields are derived from Fragment entries.

inductive Simik2024.PQStrategy : Type

How a language formally encodes its default (unbiased) polar question.

• verbMovement : PQStrategy

  Verb movement to clause-initial position (subject–verb inversion).

• clauseInitialParticle : PQStrategy

  Clause-initial question particle.

• verbAttachedParticle : PQStrategy

  Particle attached to the verb (or focused constituent).

• particlePlusMovement : PQStrategy

  Combination of particle + verb movement.

• intonationOnly : PQStrategy

  Intonation only (no overt morphosyntactic marking).

@[implicit_reducible]

instance Simik2024.instDecidableEqPQStrategy : DecidableEq PQStrategy

Equations

• Simik2024.instDecidableEqPQStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Simik2024.instReprPQStrategy : Repr PQStrategy

Equations

• Simik2024.instReprPQStrategy = { reprPrec := Simik2024.instReprPQStrategy.repr }

def Simik2024.instReprPQStrategy.repr : PQStrategy → ℕ → Std.Format

Equations

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

inductive Simik2024.DeclPQAvailability : Type

Whether the language permits declarative PQs (DeclPQs) as a separate strategy from interrogative PQs.

• available : DeclPQAvailability

  DeclPQs available and convey evidential bias.

• unavailable : DeclPQAvailability

  DeclPQs not available as a distinct strategy.

• marginal : DeclPQAvailability

  DeclPQs marginal or register-restricted.

@[implicit_reducible]

instance Simik2024.instDecidableEqDeclPQAvailability : DecidableEq DeclPQAvailability

Equations

• Simik2024.instDecidableEqDeclPQAvailability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Simik2024.instReprDeclPQAvailability : Repr DeclPQAvailability

Equations

• Simik2024.instReprDeclPQAvailability = { reprPrec := Simik2024.instReprDeclPQAvailability.repr }

def Simik2024.instReprDeclPQAvailability.repr : DeclPQAvailability → ℕ → Std.Format

Equations

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

structure Simik2024.PQProfile : Type

A Slavic language's default polar-question strategy profile.

• language : String

  Language name.

• code : String

  ISO 639-1 or 639-3 code.

• defaultStrategy : PQStrategy

  Default (unbiased) PQ strategy.

• particle : Option String

  Particle form (if applicable), derived from Fragment entries where possible.

• declPQ : DeclPQAvailability

  Whether DeclPQs are available.

• negationTriggersBias : Bool

  Whether adding negation triggers epistemic bias.

@[implicit_reducible]

instance Simik2024.instReprPQProfile : Repr PQProfile

Equations

• Simik2024.instReprPQProfile = { reprPrec := Simik2024.instReprPQProfile.repr }

def Simik2024.instReprPQProfile.repr : PQProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Simik2024.instBEqPQProfile : BEq PQProfile

Equations

• Simik2024.instBEqPQProfile = { beq := Simik2024.instBEqPQProfile.beq }

def Simik2024.instBEqPQProfile.beq : PQProfile → PQProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Simik2024.instBEqPQProfile.beq x✝¹ x✝ = false

def Simik2024.czech : PQProfile

Czech: verb-initial (VSO) with rising/falling intonation. No overt PQ particle; the default is InterPPQ.

Equations

• Simik2024.czech = { language := "Czech", code := "cs", defaultStrategy := Simik2024.PQStrategy.verbMovement, declPQ := Simik2024.DeclPQAvailability.available }

def Simik2024.slovak : PQProfile

Slovak: verb-initial, parallel to Czech.

Equations

• Simik2024.slovak = { language := "Slovak", code := "sk", defaultStrategy := Simik2024.PQStrategy.verbMovement, declPQ := Simik2024.DeclPQAvailability.available }

def Simik2024.upperSorbian : PQProfile

Upper Sorbian: verb-initial.

Equations

• Simik2024.upperSorbian = { language := "Upper Sorbian", code := "hsb", defaultStrategy := Simik2024.PQStrategy.verbMovement, declPQ := Simik2024.DeclPQAvailability.available }

def Simik2024.slovenian : PQProfile

Slovenian: clause-initial ali (optionally) + verb movement. ali is reported as incompatible with DeclPQs.

Equations

• Simik2024.slovenian = { language := "Slovenian", code := "sl", defaultStrategy := Simik2024.PQStrategy.clauseInitialParticle, particle := some Slovenian.QuestionParticles.ali.form }

def Simik2024.ukrainian : PQProfile

Ukrainian: clause-initial čy (obligatory).

Equations

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

def Simik2024.polish : PQProfile

Polish: clause-initial czy (obligatory in default PQ). Verb-initial PQs are possible but unacceptable in quiz scenarios.

Equations

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

def Simik2024.serbian : PQProfile

Serbian: da (+ li) is the default strategy. Serbian has the richest PQ repertoire among Slavic languages (see [Sim24]).

Equations

• Simik2024.serbian = { language := "Serbian", code := "sr", defaultStrategy := Simik2024.PQStrategy.particlePlusMovement, particle := some Serbian.QuestionParticles.daLi.form }

def Simik2024.macedonian : PQProfile

Macedonian: dali (clause-initial) for default PQs. dali can introduce negative PQs without triggering bias, unlike Bulgarian li.

Equations

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

def Simik2024.bulgarian : PQProfile

Bulgarian: verb-attached li, encliticizing onto the focused constituent. DeclPQs are colloquial only.

Equations

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

def Simik2024.russian : PQProfile

Russian: verb-attached li (formal) or IntonPQ (default). li-PQs are rare in spoken Russian — IntonPQs dominate and are arguably unbiased (see [Sim24]).

Equations

• Simik2024.russian = { language := "Russian", code := "ru", defaultStrategy := Simik2024.PQStrategy.intonationOnly, particle := some Russian.QuestionParticles.li.form }

def Simik2024.allProfiles : List PQProfile

All ten surveyed Slavic PQ profiles.

Equations

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

def Simik2024.verbMovementLanguages : List PQProfile

Languages using verb movement as default PQ strategy — the languages without an overt question particle in default PQs.

Equations

• Simik2024.verbMovementLanguages = List.filter (fun (x : Simik2024.PQProfile) => x.defaultStrategy == Simik2024.PQStrategy.verbMovement) Simik2024.allProfiles

def Simik2024.particleLanguages : List PQProfile

Languages using a clause-initial particle.

Equations

• Simik2024.particleLanguages = List.filter (fun (x : Simik2024.PQProfile) => x.defaultStrategy == Simik2024.PQStrategy.clauseInitialParticle) Simik2024.allProfiles

theorem Simik2024.verbMovement_implies_declPQ : (verbMovementLanguages.all fun (x : PQProfile) => x.declPQ == DeclPQAvailability.available) = true

Verb movement languages all have DeclPQs available.

theorem Simik2024.dali_negation_unbiased : bulgarian.negationTriggersBias = true ∧ macedonian.negationTriggersBias = false

Macedonian dali introduces negative PQs without triggering epistemic bias, unlike Bulgarian li.