Russian Negation Fragment

[Mie05] [Has13b] [DH13a]

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 of the ни- series always co-occur with predicate negation не. The lexical-reactive side — никто, ничего, никогда, кто-либо, etc. — lives in Fragments/Russian/PolarityItems.lean per the operator/lexical- reactive split documented in Core/Lexical/NegMarker.lean. The NegConcordExample data below illustrates the marker's NC behavior at the sentence level, which is operator-side typology consumed by Studies/Miestamo2005.lean.

def Russian.Negation.ne : Syntax.Negation.NegMarkerEntry

не — Russian's standard preverbal negation particle. A free word, syntactically immediately preverbal.

Equations

• Russian.Negation.ne = { form := "не", morphemeType := Syntax.Negation.NegMorphemeType.particle, position := Syntax.Negation.NegMarkerPosition.preverbal }

def Russian.Negation.negationSystem : Syntax.Negation.NegationSystem

The Russian negation system: a single preverbal particle.

Equations

• Russian.Negation.negationSystem = Syntax.Negation.NegationSystem.ofISO "rus" [Russian.Negation.ne]

structure Russian.Negation.NegExample : Type

A Russian negation example.

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

@[instance_reducible]

instance Russian.Negation.instReprNegExample : Repr NegExample

Equations

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

def Russian.Negation.instReprNegExample.repr : NegExample → ℕ → Std.Format

Equations

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

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

Equations

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

@[instance_reducible]

instance Russian.Negation.instBEqNegExample : BEq NegExample

Equations

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

def Russian.Negation.present : NegExample

Present tense.

Equations

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

def Russian.Negation.past : NegExample

Past tense.

Equations

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

def Russian.Negation.future : NegExample

Future (periphrastic).

Equations

• Russian.Negation.future = { affirmative := "Он будет есть", negative := "Он не будет есть", glossAff := "3SG will eat.INF", glossNeg := "3SG NEG will eat.INF", tenseLabel := "future" }

def Russian.Negation.imperative : NegExample

Imperative.

Equations

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

def Russian.Negation.allExamples : List NegExample

Equations

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

structure Russian.Negation.NegConcordExample : Type

A negative concord example.

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

def Russian.Negation.instReprNegConcordExample.repr : NegConcordExample → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Russian.Negation.instReprNegConcordExample : Repr NegConcordExample

Equations

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

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

Equations

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

@[instance_reducible]

instance Russian.Negation.instBEqNegConcordExample : BEq NegConcordExample

Equations

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

def Russian.Negation.nikto : NegConcordExample

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

Equations

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

def Russian.Negation.nichego : NegConcordExample

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

Equations

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

def Russian.Negation.nikogda : NegConcordExample

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

Equations

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

def Russian.Negation.allConcordExamples : List NegConcordExample

Equations

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

Verification

theorem Russian.Negation.ne_form : ne.form = "не"

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