German Negation Fragment

[Mie05] [Has13b] [DH13a]

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 German.Negation.nicht : Syntax.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

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

def 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

• German.Negation.negDeterminer = "kein"

def German.Negation.negationSystem : Syntax.Negation.NegationSystem

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

Equations

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

structure German.Negation.NegExample : Type

A negation example showing symmetric structure.

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

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

Equations

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

@[implicit_reducible]

instance German.Negation.instReprNegExample : Repr NegExample

Equations

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

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

Equations

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

@[implicit_reducible]

instance German.Negation.instBEqNegExample : BEq NegExample

Equations

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

def German.Negation.present : NegExample

Present tense: Ich singe / Ich singe nicht.

Equations

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

def German.Negation.presentPerfect : NegExample

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

Equations

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

def German.Negation.preterite : NegExample

Preterite: Sie kam / Sie kam nicht.

Equations

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

def German.Negation.subjunctiveII : NegExample

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

Equations

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

def German.Negation.future : NegExample

Future: Sie wird singen / Sie wird nicht singen.

Equations

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

def German.Negation.allExamples : List NegExample

Equations

• German.Negation.allExamples = [German.Negation.present, German.Negation.presentPerfect, German.Negation.preterite, German.Negation.subjunctiveII, German.Negation.future]

Verification

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

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

def German.Negation.negationProfile : Syntax.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.