Cross-Slavic Polar Question Strategies

@cite{esipova-romero-2023} @cite{simik-2024}

Typology of default (unbiased) polar question strategies across Slavic languages, based on @cite{simik-2024} §4.1. Slavic languages show rich variation in how they form PQs, using word order alternations, clause-initial particles, verb-attached particles, and combinations thereof.

Key Findings

1. Verb movement languages (Czech, Slovak, Upper Sorbian): InterPPQ (verb-initial positive) is the default unbiased PQ.
2. Particle languages (Bulgarian, Russian): verb-attached li introduces the default PQ.
3. Clause-initial particle languages (Ukrainian, Polish): čy/czy is obligatory in PQs.
4. Some languages use multiple strategies (Serbian: da li, je li; Slovenian: ali; Macedonian: dali).

Architecture

Profile particle fields and BiasParticle form fields are derived from Fragment entries (Phenomena imports Fragments, not vice versa). This ensures single-source-of-truth: changing a particle form in the Fragment automatically propagates here.

inductive Phenomena.Questions.SlavicPQStrategies.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).

instance Phenomena.Questions.SlavicPQStrategies.instDecidableEqPQStrategy : DecidableEq PQStrategy

Equations

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

instance Phenomena.Questions.SlavicPQStrategies.instBEqPQStrategy : BEq PQStrategy

Equations

• Phenomena.Questions.SlavicPQStrategies.instBEqPQStrategy = { beq := Phenomena.Questions.SlavicPQStrategies.instBEqPQStrategy.beq }

def Phenomena.Questions.SlavicPQStrategies.instBEqPQStrategy.beq : PQStrategy → PQStrategy → Bool

Equations

• Phenomena.Questions.SlavicPQStrategies.instBEqPQStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Questions.SlavicPQStrategies.instReprPQStrategy.repr : PQStrategy → Nat → Std.Format

Equations

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

instance Phenomena.Questions.SlavicPQStrategies.instReprPQStrategy : Repr PQStrategy

Equations

• Phenomena.Questions.SlavicPQStrategies.instReprPQStrategy = { reprPrec := Phenomena.Questions.SlavicPQStrategies.instReprPQStrategy.repr }

inductive Phenomena.Questions.SlavicPQStrategies.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.

instance Phenomena.Questions.SlavicPQStrategies.instDecidableEqDeclPQAvailability : DecidableEq DeclPQAvailability

Equations

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

instance Phenomena.Questions.SlavicPQStrategies.instBEqDeclPQAvailability : BEq DeclPQAvailability

Equations

• Phenomena.Questions.SlavicPQStrategies.instBEqDeclPQAvailability = { beq := Phenomena.Questions.SlavicPQStrategies.instBEqDeclPQAvailability.beq }

def Phenomena.Questions.SlavicPQStrategies.instBEqDeclPQAvailability.beq : DeclPQAvailability → DeclPQAvailability → Bool

Equations

• Phenomena.Questions.SlavicPQStrategies.instBEqDeclPQAvailability.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Questions.SlavicPQStrategies.instReprDeclPQAvailability : Repr DeclPQAvailability

Equations

• Phenomena.Questions.SlavicPQStrategies.instReprDeclPQAvailability = { reprPrec := Phenomena.Questions.SlavicPQStrategies.instReprDeclPQAvailability.repr }

def Phenomena.Questions.SlavicPQStrategies.instReprDeclPQAvailability.repr : DeclPQAvailability → Nat → Std.Format

Equations

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

structure Phenomena.Questions.SlavicPQStrategies.SlavicPQProfile : Type

A Slavic language's PQ 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

• exampleNum : Option String

  Example number from

instance Phenomena.Questions.SlavicPQStrategies.instReprSlavicPQProfile : Repr SlavicPQProfile

Equations

• Phenomena.Questions.SlavicPQStrategies.instReprSlavicPQProfile = { reprPrec := Phenomena.Questions.SlavicPQStrategies.instReprSlavicPQProfile.repr }

def Phenomena.Questions.SlavicPQStrategies.instReprSlavicPQProfile.repr : SlavicPQProfile → Nat → Std.Format

Equations

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

def Phenomena.Questions.SlavicPQStrategies.instBEqSlavicPQProfile.beq : SlavicPQProfile → SlavicPQProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Questions.SlavicPQStrategies.instBEqSlavicPQProfile.beq x✝¹ x✝ = false

instance Phenomena.Questions.SlavicPQStrategies.instBEqSlavicPQProfile : BEq SlavicPQProfile

Equations

• Phenomena.Questions.SlavicPQStrategies.instBEqSlavicPQProfile = { beq := Phenomena.Questions.SlavicPQStrategies.instBEqSlavicPQProfile.beq }

def Phenomena.Questions.SlavicPQStrategies.czech : SlavicPQProfile

Czech: verb-initial (VSO) with rising/falling intonation. No overt PQ particle. Default = InterPPQ (ex. 25).

Equations

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

def Phenomena.Questions.SlavicPQStrategies.slovak : SlavicPQProfile

Slovak: verb-initial, parallel to Czech (ex. 26).

Equations

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

def Phenomena.Questions.SlavicPQStrategies.upperSorbian : SlavicPQProfile

Upper Sorbian: verb-initial (ex. 27).

Equations

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

def Phenomena.Questions.SlavicPQStrategies.slovenian : SlavicPQProfile

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

Equations

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

def Phenomena.Questions.SlavicPQStrategies.ukrainian : SlavicPQProfile

Ukrainian: clause-initial čy (obligatory) (ex. 29).

Equations

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

def Phenomena.Questions.SlavicPQStrategies.polish : SlavicPQProfile

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

Equations

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

def Phenomena.Questions.SlavicPQStrategies.serbian : SlavicPQProfile

Serbian: da (+ li) is the default strategy (ex. 31). Serbian has the richest PQ repertoire among Slavic languages (Todorović 2023).

Equations

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

def Phenomena.Questions.SlavicPQStrategies.macedonian : SlavicPQProfile

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

Equations

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

def Phenomena.Questions.SlavicPQStrategies.bulgarian : SlavicPQProfile

Bulgarian: verb-attached li (ex. 33). li encliticizes onto the focused constituent.

Equations

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

def Phenomena.Questions.SlavicPQStrategies.russian : SlavicPQProfile

Russian: verb-attached li (formal) or IntonPQ (default). li-PQs are rare in spoken Russian — IntonPQs dominate (Onoeva & Staňková, to appear: only 6/500 were liPQs). IntonPQs are arguably unbiased (§4.2.3).

Equations

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

def Phenomena.Questions.SlavicPQStrategies.allProfiles : List SlavicPQProfile

Equations

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

def Phenomena.Questions.SlavicPQStrategies.verbMovementLanguages : List SlavicPQProfile

Languages using verb movement as default PQ strategy. These are the languages without an overt question particle in default PQs (fn. 45).

Equations

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

def Phenomena.Questions.SlavicPQStrategies.particleLanguages : List SlavicPQProfile

Languages using a clause-initial particle.

Equations

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

theorem Phenomena.Questions.SlavicPQStrategies.verbMovement_implies_declPQ : (verbMovementLanguages.all fun (x : SlavicPQProfile) => x.declPQ == DeclPQAvailability.available) = true

Verb movement languages all have DeclPQs available.

def Phenomena.Questions.SlavicPQStrategies.liFamily : List SlavicPQProfile

The li family of particles spans Bulgarian, Russian, and (as da li) Serbian. These trace back to proto-Slavic li (§4.2.1).

Equations

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

structure Phenomena.Questions.SlavicPQStrategies.BiasParticle : Type

The razve family: cross-Slavic particles specialized for expressing mirative/dubitative bias in PQs. These indicate surprise at or doubt about the evidence (§4.2.4).

Russian razve, Ukrainian and Belarusian xiba, Polish czyż(by), Bulgarian nima, Czech copak/cožpak/snad, Serbian zar.

The form field is derived from Fragment entries where available.

• language : String
• form : String
• gloss : String
• outerNeg : Bool

  Compatible with outer (FALSUM) negation?

• innerNeg : Bool

  Compatible with inner (VERUM ¬p) negation?

def Phenomena.Questions.SlavicPQStrategies.instReprBiasParticle.repr : BiasParticle → Nat → Std.Format

Equations

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

instance Phenomena.Questions.SlavicPQStrategies.instReprBiasParticle : Repr BiasParticle

Equations

• Phenomena.Questions.SlavicPQStrategies.instReprBiasParticle = { reprPrec := Phenomena.Questions.SlavicPQStrategies.instReprBiasParticle.repr }

def Phenomena.Questions.SlavicPQStrategies.instBEqBiasParticle.beq : BiasParticle → BiasParticle → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Questions.SlavicPQStrategies.instBEqBiasParticle.beq x✝¹ x✝ = false

instance Phenomena.Questions.SlavicPQStrategies.instBEqBiasParticle : BEq BiasParticle

Equations

• Phenomena.Questions.SlavicPQStrategies.instBEqBiasParticle = { beq := Phenomena.Questions.SlavicPQStrategies.instBEqBiasParticle.beq }

def Phenomena.Questions.SlavicPQStrategies.razve : BiasParticle

Equations

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

def Phenomena.Questions.SlavicPQStrategies.nahodou : BiasParticle

Equations

• Phenomena.Questions.SlavicPQStrategies.nahodou = { language := "Czech", form := "náhodou", gloss := "by.chance", outerNeg := true, innerNeg := false }

def Phenomena.Questions.SlavicPQStrategies.copak : BiasParticle

Equations

• Phenomena.Questions.SlavicPQStrategies.copak = { language := "Czech", form := "copak", gloss := "RAZVE.CZ", outerNeg := true, innerNeg := true }

def Phenomena.Questions.SlavicPQStrategies.zar : BiasParticle

Equations

• Phenomena.Questions.SlavicPQStrategies.zar = { language := "Serbian", form := Fragments.Serbian.QuestionParticles.zar_.form, gloss := "RAZVE.SR", outerNeg := true, innerNeg := true }

theorem Phenomena.Questions.SlavicPQStrategies.razve_both_negations : razve.outerNeg = true ∧ razve.innerNeg = true

Russian razve is compatible with both inner and outer negation. It stays constant across VERUM and FALSUM because both involve a conflict between epistemic and evidential bias.

theorem Phenomena.Questions.SlavicPQStrategies.nahodou_outer_only : nahodou.outerNeg = true ∧ nahodou.innerNeg = false

Czech náhodou is restricted to outer negation only, unlike razve (@cite{stankova-2025}, §5).

theorem Phenomena.Questions.SlavicPQStrategies.razve_nahodou_differ : razve.innerNeg ≠ nahodou.innerNeg

razve and náhodou differ in inner negation compatibility, despite both being ordering source modifiers. This reflects different selectional requirements: razve is compatible with both VERUM and FALSUM, while náhodou only modifies FALSUM's epistemic possibility component.

These theorems verify empirical generalizations directly against Fragment lexical data. Because profile/BiasParticle fields derive from Fragments, there are no separate "bridge" theorems — the connection is by construction.

theorem Phenomena.Questions.SlavicPQStrategies.razve_family_all_evidential : Fragments.Russian.QuestionParticles.razve_.requiresEvidentialBias = true ∧ Fragments.Ukrainian.QuestionParticles.xiba.requiresEvidentialBias = true ∧ Fragments.Polish.QuestionParticles.czyzby.requiresEvidentialBias = true ∧ Fragments.Bulgarian.QuestionParticles.nima.requiresEvidentialBias = true ∧ Fragments.Serbian.QuestionParticles.zar_.requiresEvidentialBias = true

All RAZVE-family Fragment entries require evidential bias.

theorem Phenomena.Questions.SlavicPQStrategies.neutral_particles_no_evidential : Fragments.Russian.QuestionParticles.li.requiresEvidentialBias = false ∧ Fragments.Ukrainian.QuestionParticles.cy.requiresEvidentialBias = false ∧ Fragments.Polish.QuestionParticles.czy.requiresEvidentialBias = false ∧ Fragments.Bulgarian.QuestionParticles.li.requiresEvidentialBias = false ∧ Fragments.Serbian.QuestionParticles.daLi.requiresEvidentialBias = false ∧ Fragments.Slovenian.QuestionParticles.ali.requiresEvidentialBias = false ∧ Fragments.Macedonian.QuestionParticles.dali.requiresEvidentialBias = false

All neutral PQ Fragment entries do NOT require evidential bias.