Czech Negation Fragment

[Mie05] [Has13b] [DH13a]

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 Czech.Negation.ne : Syntax.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

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

def Czech.Negation.negationSystem : Syntax.Negation.NegationSystem

The Czech negation system: a single verbal prefix.

Equations

• Czech.Negation.negationSystem = Syntax.Negation.NegationSystem.ofISO "ces" [Czech.Negation.ne]

def Czech.Negation.negPrefix : String

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

Equations

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

structure Czech.Negation.NegExample : Type

A Czech negation example.

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

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

Equations

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

@[instance_reducible]

instance Czech.Negation.instReprNegExample : Repr NegExample

Equations

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

@[instance_reducible]

instance Czech.Negation.instBEqNegExample : BEq NegExample

Equations

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

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

Equations

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

def Czech.Negation.present : NegExample

Present tense: jí → nejí.

Equations

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

def Czech.Negation.past : NegExample

Past tense: jedl → nejedl.

Equations

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

def Czech.Negation.future : NegExample

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

Equations

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

Conditional: jedl by → nejedl by.

Equations

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

def Czech.Negation.allExamples : List NegExample

Equations

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

structure Czech.Negation.NegConcordExample : Type

A negative concord example.

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

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

Equations

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

@[instance_reducible]

instance Czech.Negation.instReprNegConcordExample : Repr NegConcordExample

Equations

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

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

Equations

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

@[instance_reducible]

instance Czech.Negation.instBEqNegConcordExample : BEq NegConcordExample

Equations

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

def Czech.Negation.nikdo : NegConcordExample

Nikdo nepřišel — obligatory negative concord.

Equations

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

def Czech.Negation.nic : NegConcordExample

Nic neviděl — obligatory negative concord.

Equations

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

def Czech.Negation.nikdy : NegConcordExample

Nikdy nepřišel — obligatory negative concord.

Equations

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

def Czech.Negation.allConcordExamples : List NegConcordExample

Equations

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

Verification

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