Russian Negation Fragment

@cite{miestamo-2005} @cite{dryer-haspelmath-2013}

Russian expresses standard negation with the preverbal particle не (ne). Negation is symmetric: adding не introduces no structural changes — no finiteness change, no TAM restrictions, no paradigmatic gaps.

Negative concord (Ch 115)

Russian has obligatory negative concord (WALS: co-occur):

• Никто не пришёл 'Nobody NEG came' = 'Nobody came'
• Ничего не видел 'Nothing NEG saw' = '(I) saw nothing'

N-words (ни- series) always co-occur with predicate negation не.

def Fragments.Russian.Negation.negMarker : String

The standard negation particle.

Equations

• Fragments.Russian.Negation.negMarker = "не"

structure Fragments.Russian.Negation.NegExample : Type

A Russian negation example.

• affirmative : String
• negative : String
• glossAff : String
• glossNeg : String
• tenseLabel : String

def Fragments.Russian.Negation.instReprNegExample.repr : NegExample → Nat → Std.Format

Equations

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

instance Fragments.Russian.Negation.instReprNegExample : Repr NegExample

Equations

• Fragments.Russian.Negation.instReprNegExample = { reprPrec := Fragments.Russian.Negation.instReprNegExample.repr }

def Fragments.Russian.Negation.instBEqNegExample.beq : NegExample → NegExample → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Russian.Negation.instBEqNegExample.beq x✝¹ x✝ = false

instance Fragments.Russian.Negation.instBEqNegExample : BEq NegExample

Equations

• Fragments.Russian.Negation.instBEqNegExample = { beq := Fragments.Russian.Negation.instBEqNegExample.beq }

def Fragments.Russian.Negation.present : NegExample

Present tense.

Equations

• Fragments.Russian.Negation.present = { affirmative := "Он ест", negative := "Он не ест", glossAff := "3SG eat.PRS", glossNeg := "3SG NEG eat.PRS", tenseLabel := "present" }

def Fragments.Russian.Negation.past : NegExample

Past tense.

Equations

• Fragments.Russian.Negation.past = { affirmative := "Он ел", negative := "Он не ел", glossAff := "3SG eat.PST.M", glossNeg := "3SG NEG eat.PST.M", tenseLabel := "past" }

def Fragments.Russian.Negation.future : NegExample

Future (periphrastic).

Equations

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

def Fragments.Russian.Negation.imperative : NegExample

Imperative.

Equations

• Fragments.Russian.Negation.imperative = { affirmative := "Ешь!", negative := "Не ешь!", glossAff := "eat.IMP.2SG", glossNeg := "NEG eat.IMP.2SG", tenseLabel := "imperative" }

def Fragments.Russian.Negation.allExamples : List NegExample

Equations

• Fragments.Russian.Negation.allExamples = [Fragments.Russian.Negation.present, Fragments.Russian.Negation.past, Fragments.Russian.Negation.future, Fragments.Russian.Negation.imperative]

structure Fragments.Russian.Negation.NegConcordExample : Type

A negative concord example.

• sentence : String
• translation : String
• nword : String
• nwordGloss : String

instance Fragments.Russian.Negation.instReprNegConcordExample : Repr NegConcordExample

Equations

• Fragments.Russian.Negation.instReprNegConcordExample = { reprPrec := Fragments.Russian.Negation.instReprNegConcordExample.repr }

def Fragments.Russian.Negation.instReprNegConcordExample.repr : NegConcordExample → Nat → Std.Format

Equations

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

def Fragments.Russian.Negation.instBEqNegConcordExample.beq : NegConcordExample → NegConcordExample → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Russian.Negation.instBEqNegConcordExample.beq x✝¹ x✝ = false

instance Fragments.Russian.Negation.instBEqNegConcordExample : BEq NegConcordExample

Equations

• Fragments.Russian.Negation.instBEqNegConcordExample = { beq := Fragments.Russian.Negation.instBEqNegConcordExample.beq }

def Fragments.Russian.Negation.nikto : NegConcordExample

Никто не пришёл — obligatory negative concord.

Equations

• Fragments.Russian.Negation.nikto = { sentence := "Никто не пришёл", translation := "Nobody came", nword := "никто", nwordGloss := "nobody" }

def Fragments.Russian.Negation.nichego : NegConcordExample

Ничего не видел — obligatory negative concord.

Equations

• Fragments.Russian.Negation.nichego = { sentence := "Ничего не видел", translation := "(I) saw nothing", nword := "ничего", nwordGloss := "nothing.GEN" }

def Fragments.Russian.Negation.nikogda : NegConcordExample

Никогда не приходил — obligatory negative concord.

Equations

• Fragments.Russian.Negation.nikogda = { sentence := "Никогда не приходил", translation := "(He) never came", nword := "никогда", nwordGloss := "never" }

def Fragments.Russian.Negation.allConcordExamples : List NegConcordExample

Equations

• Fragments.Russian.Negation.allConcordExamples = [Fragments.Russian.Negation.nikto, Fragments.Russian.Negation.nichego, Fragments.Russian.Negation.nikogda]

Verification

theorem Fragments.Russian.Negation.negMarker_is_ne : negMarker = "не"

theorem Fragments.Russian.Negation.all_examples_count : allExamples.length = 4

theorem Fragments.Russian.Negation.all_negative_contain_ne : (allExamples.all fun (e : NegExample) => Fragments.Russian.Negation.hasSubstr✝ e.negative "не" || Fragments.Russian.Negation.hasSubstr✝¹ e.negative "Не") = true

All negative examples contain не (or sentence-initial Не).

theorem Fragments.Russian.Negation.all_concord_contain_ne : (allConcordExamples.all fun (e : NegConcordExample) => Fragments.Russian.Negation.hasSubstr✝ e.sentence "не") = true

All negative concord examples contain не alongside the n-word.

theorem Fragments.Russian.Negation.all_nwords_ni_prefix : (allConcordExamples.all fun (e : NegConcordExample) => e.nword.startsWith "ни") = true

All n-words begin with ни-.