German Negation Fragment

@cite{miestamo-2005} @cite{haspelmath-2013} @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.nicht : Typology.Negation.NegMarkerEntry

nicht — German's standard negation particle. Attaches to the VP at clause-final position; surfaces after the finite verb in V2 main clauses (Ich singe nicht) and before the non-finite verb in periphrastic constructions (Er hat nicht gelesen). The V2/SOV alternation is why WALS Ch 143A classifies German as .type1Type2 (mixed NegV / VNeg) rather than a single position; the position field uses .other to flag this.

Equations

• Fragments.German.Negation.nicht = { form := "nicht", morphemeType := Typology.Negation.NegMorphemeType.particle, position := Typology.Negation.NegMarkerPosition.other }

def Fragments.German.Negation.negDeterminer : String

kein — negative determiner (fuses negation + indefinite article). Lives here as a lexical fact about German negation morphology; the morphosyntactic analysis of NQ-type negative quantifiers in non-NC languages is a separate axis from the operator.

Equations

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

def Fragments.German.Negation.negationSystem : Typology.Negation.NegationSystem

The German negation system: a single particle. The Fragment-side joint consumed by Phenomena/Negation/Studies/Dryer2013.lean.

Equations

• Fragments.German.Negation.negationSystem = Typology.Negation.NegationSystem.ofISO "deu" [Fragments.German.Negation.nicht]

structure Fragments.German.Negation.NegExample : Type

A negation example showing symmetric structure.

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

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

Equations

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

@[implicit_reducible]

instance Fragments.German.Negation.instReprNegExample : Repr NegExample

Equations

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

@[implicit_reducible]

instance Fragments.German.Negation.instBEqNegExample : BEq NegExample

Equations

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

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

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.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).

def Fragments.German.Negation.negationProfile : Typology.Negation.NegationProfile

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

Equations

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