Czech Negation Fragment

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

Czech expresses standard negation with the verbal prefix ne-. Negation is symmetric: the prefix attaches directly to the verb with no structural change — no finiteness restriction, no TAM gaps.

Negative concord (Ch 115)

Czech has obligatory negative concord (WALS: co-occur), following the standard Slavic pattern:

• Nikdo nepřišel 'Nobody NEG.came' = 'Nobody came'
• Nic neviděl 'Nothing NEG.saw' = '(He) saw nothing'

N-words of the ni- series (nikdo, nic, nikdy, nikam) always co-occur with the ne- prefix on the verb. The lexeme entries live in the sibling Fragments/Czech/PolarityItems.lean per the operator/ lexical-reactive split documented in Core/Lexical/NegMarker.lean. The NegConcordExample data below illustrates the marker's interaction with the n-word system at the sentence level.

def Fragments.Slavic.Czech.Negation.ne : Typology.Negation.NegMarkerEntry

ne- — Czech's standard negation prefix. Attaches directly to the verb stem: nepřijde 'will not come', neviděl 'didn't see'. Symmetric across the paradigm.

Equations

• Fragments.Slavic.Czech.Negation.ne = { form := "ne-", morphemeType := Typology.Negation.NegMorphemeType.affix, position := Typology.Negation.NegMarkerPosition.preverbal }

def Fragments.Slavic.Czech.Negation.negationSystem : Typology.Negation.NegationSystem

The Czech negation system: a single verbal prefix. The Fragment-side joint consumed by Phenomena/Negation/Studies/Dryer2013.lean.

Equations

• Fragments.Slavic.Czech.Negation.negationSystem = Typology.Negation.NegationSystem.ofISO "ces" [Fragments.Slavic.Czech.Negation.ne]

def Fragments.Slavic.Czech.Negation.negPrefix : String

Legacy String accessor for the prefix. Kept for back-compat with Phenomena/Negation/Studies/Miestamo2005.lean. New consumers should use ne.form.

Equations

• Fragments.Slavic.Czech.Negation.negPrefix = Fragments.Slavic.Czech.Negation.ne.form

structure Fragments.Slavic.Czech.Negation.NegExample : Type

A Czech negation example.

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

@[implicit_reducible]

instance Fragments.Slavic.Czech.Negation.instReprNegExample : Repr NegExample

Equations

• Fragments.Slavic.Czech.Negation.instReprNegExample = { reprPrec := Fragments.Slavic.Czech.Negation.instReprNegExample.repr }

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

Equations

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

@[implicit_reducible]

instance Fragments.Slavic.Czech.Negation.instBEqNegExample : BEq NegExample

Equations

• Fragments.Slavic.Czech.Negation.instBEqNegExample = { beq := Fragments.Slavic.Czech.Negation.instBEqNegExample.beq }

def Fragments.Slavic.Czech.Negation.instBEqNegExample.beq : NegExample → NegExample → Bool

Equations

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

def Fragments.Slavic.Czech.Negation.present : NegExample

Present tense: jí → nejí.

Equations

• Fragments.Slavic.Czech.Negation.present = { affirmative := "Jí", negative := "Nejí", glossAff := "eat.3SG.PRS", glossNeg := "NEG.eat.3SG.PRS", tenseLabel := "present" }

def Fragments.Slavic.Czech.Negation.past : NegExample

Past tense: jedl → nejedl.

Equations

• Fragments.Slavic.Czech.Negation.past = { affirmative := "Jedl", negative := "Nejedl", glossAff := "eat.PST.M", glossNeg := "NEG.eat.PST.M", tenseLabel := "past" }

def Fragments.Slavic.Czech.Negation.future : NegExample

Future (periphrastic): bude jíst → nebude jíst.

Equations

• Fragments.Slavic.Czech.Negation.future = { affirmative := "Bude jíst", negative := "Nebude jíst", glossAff := "will.3SG eat.INF", glossNeg := "NEG.will.3SG eat.INF", tenseLabel := "future" }

def Fragments.Slavic.Czech.Negation.conditional : NegExample

Conditional: jedl by → nejedl by.

Equations

• Fragments.Slavic.Czech.Negation.conditional = { affirmative := "Jedl by", negative := "Nejedl by", glossAff := "eat.PST.M COND", glossNeg := "NEG.eat.PST.M COND", tenseLabel := "conditional" }

def Fragments.Slavic.Czech.Negation.allExamples : List NegExample

Equations

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

structure Fragments.Slavic.Czech.Negation.NegConcordExample : Type

A negative concord example.

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

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

Equations

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

@[implicit_reducible]

instance Fragments.Slavic.Czech.Negation.instReprNegConcordExample : Repr NegConcordExample

Equations

• Fragments.Slavic.Czech.Negation.instReprNegConcordExample = { reprPrec := Fragments.Slavic.Czech.Negation.instReprNegConcordExample.repr }

@[implicit_reducible]

instance Fragments.Slavic.Czech.Negation.instBEqNegConcordExample : BEq NegConcordExample

Equations

• Fragments.Slavic.Czech.Negation.instBEqNegConcordExample = { beq := Fragments.Slavic.Czech.Negation.instBEqNegConcordExample.beq }

def Fragments.Slavic.Czech.Negation.instBEqNegConcordExample.beq : NegConcordExample → NegConcordExample → Bool

Equations

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

def Fragments.Slavic.Czech.Negation.nikdo : NegConcordExample

Nikdo nepřišel — obligatory negative concord.

Equations

• Fragments.Slavic.Czech.Negation.nikdo = { sentence := "Nikdo nepřišel", translation := "Nobody came", nword := "nikdo", nwordGloss := "nobody" }

def Fragments.Slavic.Czech.Negation.nic : NegConcordExample

Nic neviděl — obligatory negative concord.

Equations

• Fragments.Slavic.Czech.Negation.nic = { sentence := "Nic neviděl", translation := "(He) saw nothing", nword := "nic", nwordGloss := "nothing" }

def Fragments.Slavic.Czech.Negation.nikdy : NegConcordExample

Nikdy nepřišel — obligatory negative concord.

Equations

• Fragments.Slavic.Czech.Negation.nikdy = { sentence := "Nikdy nepřišel", translation := "(He) never came", nword := "nikdy", nwordGloss := "never" }

def Fragments.Slavic.Czech.Negation.allConcordExamples : List NegConcordExample

Equations

• Fragments.Slavic.Czech.Negation.allConcordExamples = [Fragments.Slavic.Czech.Negation.nikdo, Fragments.Slavic.Czech.Negation.nic, Fragments.Slavic.Czech.Negation.nikdy]

Verification

theorem Fragments.Slavic.Czech.Negation.all_examples_count : allExamples.length = 4

theorem Fragments.Slavic.Czech.Negation.all_negative_start_ne : (allExamples.all fun (e : NegExample) => e.negative.startsWith "Ne") = true

All negative forms begin with Ne (prefix attached).

theorem Fragments.Slavic.Czech.Negation.all_concord_contain_ne : (allConcordExamples.all fun (e : NegConcordExample) => decide ((e.sentence.splitOn "ne").length > 1)) = true

All negative concord sentences contain a verb with ne- prefix.

theorem Fragments.Slavic.Czech.Negation.all_nwords_ni_prefix : (allConcordExamples.all fun (e : NegConcordExample) => e.nword.startsWith "ni") = true

All n-words begin with ni-.

def Fragments.Slavic.Czech.Negation.negationProfile : Typology.Negation.NegationProfile

Czech negation profile (WALS Ch 112-115 + Greco/JinKoenig fields).

Equations

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