Czech Negation Fragment

@cite{miestamo-2005} @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 (ni- series) always co-occur with the ne- prefix on the verb.

def Fragments.Czech.Negation.negPrefix : String

The standard negation prefix.

Equations

• Fragments.Czech.Negation.negPrefix = "ne-"

structure Fragments.Czech.Negation.NegExample : Type

A Czech negation example.

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

instance Fragments.Czech.Negation.instReprNegExample : Repr NegExample

Equations

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

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

Equations

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

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

Equations

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

instance Fragments.Czech.Negation.instBEqNegExample : BEq NegExample

Equations

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

def Fragments.Czech.Negation.present : NegExample

Present tense: jí → nejí.

Equations

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

def Fragments.Czech.Negation.past : NegExample

Past tense: jedl → nejedl.

Equations

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

def Fragments.Czech.Negation.future : NegExample

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

Equations

• Fragments.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.Czech.Negation.conditional : NegExample

Conditional: jedl by → nejedl by.

Equations

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

def Fragments.Czech.Negation.allExamples : List NegExample

Equations

• Fragments.Czech.Negation.allExamples = [Fragments.Czech.Negation.present, Fragments.Czech.Negation.past, Fragments.Czech.Negation.future, Fragments.Czech.Negation.conditional]

structure Fragments.Czech.Negation.NegConcordExample : Type

A negative concord example.

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

instance Fragments.Czech.Negation.instReprNegConcordExample : Repr NegConcordExample

Equations

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

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

Equations

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

instance Fragments.Czech.Negation.instBEqNegConcordExample : BEq NegConcordExample

Equations

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

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

Equations

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

def Fragments.Czech.Negation.nikdo : NegConcordExample

Nikdo nepřišel — obligatory negative concord.

Equations

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

def Fragments.Czech.Negation.nic : NegConcordExample

Nic neviděl — obligatory negative concord.

Equations

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

def Fragments.Czech.Negation.nikdy : NegConcordExample

Nikdy nepřišel — obligatory negative concord.

Equations

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

def Fragments.Czech.Negation.allConcordExamples : List NegConcordExample

Equations

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

Verification

theorem Fragments.Czech.Negation.negPrefix_is_ne : negPrefix = "ne-"

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

theorem Fragments.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.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.Czech.Negation.all_nwords_ni_prefix : (allConcordExamples.all fun (e : NegConcordExample) => e.nword.startsWith "ni") = true

All n-words begin with ni-.