Serbian Question Particles

@cite{simik-2024}

Lexical entries for Serbian interrogative particles.

Particles

Particle	Gloss	Layer	Bias
da li	neutral PQ	CP	none
zar	RAZVE (mirative)	PerspP	+evidential

Cross-Module Connections

• SlavicPQStrategies.serbian: PQ strategy profile (da li + verb movement)
• SlavicPQStrategies.zar: bias particle data (outerNeg/innerNeg)
• Bridge theorems in SlavicPQStrategies (Phenomena imports Fragments)

structure Fragments.Serbian.QuestionParticles.QParticleEntry : Type

A Serbian interrogative particle entry.

• form : String
• gloss : String
• layer : Semantics.Questions.QParticleLayer
• polarOk : Bool
• declOk : Bool
• whOk : Bool
• requiresEvidentialBias : Bool
• requiresEpistemicBias : Bool

instance Fragments.Serbian.QuestionParticles.instReprQParticleEntry : Repr QParticleEntry

Equations

• Fragments.Serbian.QuestionParticles.instReprQParticleEntry = { reprPrec := Fragments.Serbian.QuestionParticles.instReprQParticleEntry.repr }

def Fragments.Serbian.QuestionParticles.instReprQParticleEntry.repr : QParticleEntry → Nat → Std.Format

Equations

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

instance Fragments.Serbian.QuestionParticles.instDecidableEqQParticleEntry : DecidableEq QParticleEntry

Equations

• Fragments.Serbian.QuestionParticles.instDecidableEqQParticleEntry = Fragments.Serbian.QuestionParticles.instDecidableEqQParticleEntry.decEq

def Fragments.Serbian.QuestionParticles.instDecidableEqQParticleEntry.decEq (x✝ x✝¹ : QParticleEntry) : Decidable (x✝ = x✝¹)

Equations

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

instance Fragments.Serbian.QuestionParticles.instBEqQParticleEntry : BEq QParticleEntry

Equations

• Fragments.Serbian.QuestionParticles.instBEqQParticleEntry = { beq := Fragments.Serbian.QuestionParticles.instBEqQParticleEntry.beq }

def Fragments.Serbian.QuestionParticles.instBEqQParticleEntry.beq : QParticleEntry → QParticleEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Serbian.QuestionParticles.instBEqQParticleEntry.beq x✝¹ x✝ = false

def Fragments.Serbian.QuestionParticles.daLi : QParticleEntry

da li — default PQ particle combination (@cite{simik-2024} ex. 31). Particle + verb movement. Neutral baseline.

Equations

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

def Fragments.Serbian.QuestionParticles.zar_ : QParticleEntry

zar — mirative/dubitative particle (RAZVE family, @cite{simik-2024} §4.2.4). Compatible with both outer and inner negation (like Russian razve).

Equations

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

def Fragments.Serbian.QuestionParticles.allQuestionParticles : List QParticleEntry

Equations

• Fragments.Serbian.QuestionParticles.allQuestionParticles = [Fragments.Serbian.QuestionParticles.daLi, Fragments.Serbian.QuestionParticles.zar_]

theorem Fragments.Serbian.QuestionParticles.daLi_neutral : daLi.requiresEvidentialBias = false ∧ daLi.requiresEpistemicBias = false

theorem Fragments.Serbian.QuestionParticles.zar_evidential : zar_.requiresEvidentialBias = true

theorem Fragments.Serbian.QuestionParticles.bias_contrast : daLi.requiresEvidentialBias = false ∧ zar_.requiresEvidentialBias = true

da li and zar form a neutral/evidential contrast.