German Verbal Prefix and Particle Verbs

@cite{ludeling-2001} @cite{dendikken-1995}

Lexical entries for German verbs with prefixes — both separable particle verbs (scheidbar zusammengesetzte Verben, e.g. anrufen) and inseparable prefix verbs (ver-, be-, ent-, zer-). The distinction is the major morphosyntactic split in the German verbal system: separable verbs split under V2 (er ruft Maria an) and trigger ge- insertion in the past participle (angerufen) and zu insertion in the zu-infinitive (anzurufen); inseparable prefix verbs never split, lack ge- in the participle (verstanden, not *geverstanden), and place zu before the whole word in the zu-infinitive (zu verstehen).

@cite{dendikken-1995}'s SC analysis (book ch. 2) takes German particle verbs as one of the major Germanic test cases for the ergative-particle / SC-head proposal.

Main definitions

• GermanAffixClass — separable vs inseparable.
• GermanVerbalAffixEntry — a single entry.
• inventory — eight canonical entries (5 separable, 3 inseparable).

Main results

• inventory_citation_concat — every entry's citationForm is affix ++ stem (holds for both classes).
• IsSeparable predicate with decidable instance.

inductive Fragments.German.VerbParticles.GermanAffixClass : Type

German affix class: separable particles split under V2 and trigger ge-/-zu- insertion; inseparable prefixes never split.

• separable : GermanAffixClass
• inseparable : GermanAffixClass

@[implicit_reducible]

instance Fragments.German.VerbParticles.instDecidableEqGermanAffixClass : DecidableEq GermanAffixClass

Equations

• Fragments.German.VerbParticles.instDecidableEqGermanAffixClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Fragments.German.VerbParticles.GermanVerbalAffixEntry : Type

A German prefixed-verb entry: separable particle verb or inseparable prefix verb. Records both the past participle (with or without ge- insertion) and the zu-infinitive (concatenated or space-separated) for the morphological diagnostics.

• citationForm : String

  Citation infinitive (affix + stem concatenated).

• stem : String

  Bare verb stem.

• affix : String

  The affix (separable particle or inseparable prefix).

• affixClass : GermanAffixClass

  Affix class.

• pastParticiple : String

  Past participle. Separable: ge- between affix and stem (angerufen). Inseparable: bare verb participle, no ge- (verstanden).

• zuInfinitive : String

  zu-infinitive. Separable: zu concatenated between affix and stem (anzurufen, one word). Inseparable: zu as separate word before the citation form (zu verstehen).

• gloss : String

  English gloss.

def Fragments.German.VerbParticles.IsSeparable (e : GermanVerbalAffixEntry) : Prop

An entry's affix is separable.

Equations

• Fragments.German.VerbParticles.IsSeparable e = (e.affixClass = Fragments.German.VerbParticles.GermanAffixClass.separable)

@[implicit_reducible]

instance Fragments.German.VerbParticles.instDecidablePredGermanVerbalAffixEntryIsSeparable : DecidablePred IsSeparable

Equations

• Fragments.German.VerbParticles.instDecidablePredGermanVerbalAffixEntryIsSeparable e = decEq e.affixClass Fragments.German.VerbParticles.GermanAffixClass.separable

Separable particle verbs

def Fragments.German.VerbParticles.anrufen : GermanVerbalAffixEntry

anrufen 'phone, call up'. Separable an-; pp angerufen; zu-inf anzurufen.

Equations

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

def Fragments.German.VerbParticles.aufmachen : GermanVerbalAffixEntry

aufmachen 'open'. Separable auf-; pp aufgemacht; zu-inf aufzumachen.

Equations

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

def Fragments.German.VerbParticles.einschalten : GermanVerbalAffixEntry

einschalten 'switch on'. Separable ein-; pp eingeschaltet; zu-inf einzuschalten.

Equations

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

def Fragments.German.VerbParticles.abfahren : GermanVerbalAffixEntry

abfahren 'depart'. Separable ab-; pp abgefahren; zu-inf abzufahren.

Equations

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

def Fragments.German.VerbParticles.mitkommen : GermanVerbalAffixEntry

mitkommen 'come along'. Separable mit-; pp mitgekommen; zu-inf mitzukommen.

Equations

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

Inseparable prefix verbs

def Fragments.German.VerbParticles.verstehen : GermanVerbalAffixEntry

verstehen 'understand'. Inseparable ver-; pp verstanden (no ge-); zu-inf zu verstehen (separated).

Equations

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

def Fragments.German.VerbParticles.bezahlen : GermanVerbalAffixEntry

bezahlen 'pay'. Inseparable be-; pp bezahlt (no ge-); zu-inf zu bezahlen (separated).

Equations

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

def Fragments.German.VerbParticles.entkommen : GermanVerbalAffixEntry

entkommen 'escape'. Inseparable ent-; pp entkommen (no ge-); zu-inf zu entkommen (separated).

Equations

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

def Fragments.German.VerbParticles.inventory : List GermanVerbalAffixEntry

The canonical inventory: 5 separable + 3 inseparable.

Equations

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

Properties

def Fragments.German.VerbParticles.IsCitationConcat (e : GermanVerbalAffixEntry) : Prop

An entry's citationForm is the literal concatenation of its affix and stem. Holds for both separable and inseparable classes; the morphological diagnostics live in the past participle and zu-infinitive shapes (separable inserts ge-/-zu- between affix and stem; inseparable does neither).

Equations

• Fragments.German.VerbParticles.IsCitationConcat e = (e.citationForm = e.affix ++ e.stem)

@[implicit_reducible]

instance Fragments.German.VerbParticles.instDecidablePredGermanVerbalAffixEntryIsCitationConcat : DecidablePred IsCitationConcat

Equations

• Fragments.German.VerbParticles.instDecidablePredGermanVerbalAffixEntryIsCitationConcat e = decEq e.citationForm (e.affix ++ e.stem)

theorem Fragments.German.VerbParticles.inventory_citation_concat (e : GermanVerbalAffixEntry) (he : e ∈ inventory) : IsCitationConcat e

Every inventory entry's citation form is the concatenation of its affix and stem.