German Negation Fragment

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

German expresses standard negation with the particle nicht, which appears after the finite verb in main clauses and before the non-finite verb at clause end. Negation is symmetric: adding nicht introduces no structural changes beyond the negation marker itself.

Examples

Affirmative	Negative
Ich singe 'I sing'	Ich singe nicht 'I don't sing'
Er hat gelesen 'He has read'	Er hat nicht gelesen 'He hasn't read'

Key properties

• No finiteness change: finite verb stays finite
• No TAM restrictions: all tenses/moods available under negation
• No paradigmatic gaps: the full inflectional paradigm is maintained
• Constituent negation nicht can also negate sub-constituents

def Fragments.German.Negation.negMarker : String

The German standard negation marker.

Equations

• Fragments.German.Negation.negMarker = "nicht"

def Fragments.German.Negation.negDeterminer : String

kein — negative determiner (fuses negation + indefinite article).

Equations

• Fragments.German.Negation.negDeterminer = "kein"

structure Fragments.German.Negation.NegExample : Type

A negation example showing symmetric structure.

• affirmative : String
• negative : String
• gloss : String
• tenseLabel : String

instance Fragments.German.Negation.instReprNegExample : Repr NegExample

Equations

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

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

Equations

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

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

Equations

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

instance Fragments.German.Negation.instBEqNegExample : BEq NegExample

Equations

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

def Fragments.German.Negation.present : NegExample

Present tense: Ich singe / Ich singe nicht.

Equations

• Fragments.German.Negation.present = { affirmative := "Ich singe", negative := "Ich singe nicht", gloss := "I sing / I sing NEG", tenseLabel := "present" }

def Fragments.German.Negation.presentPerfect : NegExample

Present perfect: Er hat gelesen / Er hat nicht gelesen.

Equations

• Fragments.German.Negation.presentPerfect = { affirmative := "Er hat gelesen", negative := "Er hat nicht gelesen", gloss := "He has read / He has NEG read", tenseLabel := "present perfect" }

def Fragments.German.Negation.preterite : NegExample

Preterite: Sie kam / Sie kam nicht.

Equations

• Fragments.German.Negation.preterite = { affirmative := "Sie kam", negative := "Sie kam nicht", gloss := "She came / She came NEG", tenseLabel := "preterite" }

def Fragments.German.Negation.subjunctiveII : NegExample

Subjunctive II: Er käme / Er käme nicht.

Equations

• Fragments.German.Negation.subjunctiveII = { affirmative := "Er käme", negative := "Er käme nicht", gloss := "He would.come / He would.come NEG", tenseLabel := "subjunctive II" }

def Fragments.German.Negation.future : NegExample

Future: Sie wird singen / Sie wird nicht singen.

Equations

• Fragments.German.Negation.future = { affirmative := "Sie wird singen", negative := "Sie wird nicht singen", gloss := "She will sing / She will NEG sing", tenseLabel := "future" }

def Fragments.German.Negation.allExamples : List NegExample

Equations

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

Verification

theorem Fragments.German.Negation.negMarker_is_nicht : negMarker = "nicht"

theorem Fragments.German.Negation.all_negative_contain_nicht : (allExamples.all fun (e : NegExample) => Fragments.German.Negation.hasSubstr✝ e.negative "nicht") = true

German negation is symmetric: the negative form is always the affirmative + nicht, with no structural change. We verify this by checking that each negative example contains nicht.

theorem Fragments.German.Negation.all_tenses_available : allExamples.length = 5

All five tenses are available under negation (no paradigmatic gaps).