German pronouns

This file defines the German personal pronouns, the reflexive sich and the reciprocal einander, and the case paradigms of the interrogative pronouns wer 'who' and was 'what', which also head free relatives.

The second person distinguishes the familiar du and ihr from the polite level, with the single form Sie. Sie takes the third person plural series for agreement and reflexive binding (sich, not dich or euch) while denoting the addressee alone or with others, so its person is third and its referential categories are those of du and ihr together. wer declines for the four German cases; was has one form for the nominative and the accusative and no dative.

Main definitions

• German.Pronouns.pronouns — the personal pronoun inventory
• German.Pronouns.addresseeSg, German.Pronouns.addresseePl — the pronouns of address at each grade
• German.Pronouns.sich, German.Pronouns.einander — the reflexive and the reciprocal pronoun
• German.Pronouns.wer, German.Pronouns.was — the interrogative paradigms, a form for each case

Main results

• German.Pronouns.addresseeSg_eq_sie_formal_iff, German.Pronouns.addressee_number, German.Pronouns.sie_formal_referential — Sie is the pronoun of the polite grade, which does not distinguish one addressee from several, and it denotes what the two familiar forms denote together
• German.Pronouns.wer_isSome, German.Pronouns.was_isSome_iff — wer has a form in every case, was in every case but the dative

References

• L. J. Adamson and S. Zompì, Polite pronouns and the PCC (2025)
• M. Dalrymple and R. M. Kaplan, Feature indeterminacy and feature resolution (2000)
• N. Evans, Reciprocal Constructions: Towards a Structural Typology (2008)
• V. Gast and F. Haas, On Reciprocal and Reflexive Uses of Anaphors in German and Other European Languages (2008)

inductive German.Grade : Type

The honorific grades of German pronouns, lowest first.

• familiar : Grade

  The familiar grade, du and ihr.

• polite : Grade

  The polite grade, Sie.

@[instance_reducible]

instance German.instDecidableEqGrade : DecidableEq Grade

Equations

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

@[instance_reducible]

instance German.instFintypeGrade : Fintype Grade

Equations

• German.instFintypeGrade = { elems := { val := ↑German.Grade.enumList, nodup := German.Grade.enumList_nodup }, complete := German.instFintypeGrade._proof_1 }

def German.instReprGrade.repr : Grade → ℕ → Std.Format

Equations

• German.instReprGrade.repr German.Grade.familiar prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "German.Grade.familiar")).group prec✝
• German.instReprGrade.repr German.Grade.polite prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "German.Grade.polite")).group prec✝

@[instance_reducible]

instance German.instReprGrade : Repr Grade

Equations

• German.instReprGrade = { reprPrec := German.instReprGrade.repr }

@[instance_reducible]

instance German.instLinearOrderGrade : LinearOrder Grade

Equations

• German.instLinearOrderGrade = LinearOrder.lift' German.Grade.ctorIdx German.instLinearOrderGrade._proof_1

Personal pronouns

def German.Pronouns.ich : PersonalPronoun

The first person singular ich.

Equations

• German.Pronouns.ich = { form := "ich", person := some Person.first, number := some Number.singular }

def German.Pronouns.du : PersonalPronoun

The familiar second person singular du.

Equations

• German.Pronouns.du = { form := "du", person := some Person.second, number := some Number.singular }

def German.Pronouns.sie_formal : PersonalPronoun

The polite second person Sie, for one or several addressees. Its agreement person and number are those of the third person plural; it denotes the addressee alone or with others ([AZ25a]).

Equations

• German.Pronouns.sie_formal = { form := "Sie", person := some Person.third, number := some Number.plural, referential := {Person.Category.addressee, Person.Category.addresseeOthers} }

def German.Pronouns.er : PersonalPronoun

The third person singular masculine er.

Equations

• German.Pronouns.er = { form := "er", person := some Person.third, number := some Number.singular, gender := some Gender.masculine }

def German.Pronouns.sie_sg : PersonalPronoun

The third person singular feminine sie.

Equations

• German.Pronouns.sie_sg = { form := "sie", person := some Person.third, number := some Number.singular, gender := some Gender.feminine }

def German.Pronouns.es : PersonalPronoun

The third person singular neuter es.

Equations

• German.Pronouns.es = { form := "es", person := some Person.third, number := some Number.singular, gender := some Gender.neuter }

def German.Pronouns.wir : PersonalPronoun

The first person plural wir.

Equations

• German.Pronouns.wir = { form := "wir", person := some Person.first, number := some Number.plural }

def German.Pronouns.ihr : PersonalPronoun

The familiar second person plural ihr.

Equations

• German.Pronouns.ihr = { form := "ihr", person := some Person.second, number := some Number.plural }

def German.Pronouns.sie_pl : PersonalPronoun

The third person plural sie.

Equations

• German.Pronouns.sie_pl = { form := "sie", person := some Person.third, number := some Number.plural }

def German.Pronouns.addresseeSg : Grade → PersonalPronoun

The pronoun for a single addressee at each grade.

Equations

• German.Pronouns.addresseeSg German.Grade.familiar = German.Pronouns.du
• German.Pronouns.addresseeSg German.Grade.polite = German.Pronouns.sie_formal

def German.Pronouns.addresseePl : Grade → PersonalPronoun

The pronoun for several addressees at each grade.

Equations

• German.Pronouns.addresseePl German.Grade.familiar = German.Pronouns.ihr
• German.Pronouns.addresseePl German.Grade.polite = German.Pronouns.sie_formal

def German.Pronouns.pronouns : Finset PersonalPronoun

The personal pronoun inventory.

Equations

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

theorem German.Pronouns.addresseeSg_eq_sie_formal_iff (g : Grade) : (addresseeSg g = sie_formal ↔ g = Grade.polite) ∧ (addresseePl g = sie_formal ↔ g = Grade.polite)

Sie is the pronoun of the polite grade and of no other, for one addressee or several.

theorem German.Pronouns.addressee_number : addresseeSg Grade.familiar ≠ addresseePl Grade.familiar ∧ addresseeSg Grade.polite = addresseePl Grade.polite

The familiar grade distinguishes one addressee from several, and the polite grade does not.

theorem German.Pronouns.sie_formal_referential : sie_formal.referential = du.referential ∪ ihr.referential

The polite form denotes exactly what the two familiar forms denote between them: Sie is number-neutral where the familiar level distinguishes du from ihr.

Reflexive and reciprocal pronouns

def German.Pronouns.sich : ReflexivePronoun

The third person reflexive sich, one form for both numbers and for the accusative and the dative; the first and second persons use their personal forms as reflexives. This is the pronominal sich of [GH08], a noun phrase that is only reflexive; the clitic sich of reciprocal and middle verbs is a marker in German.Reciprocals.

Equations

• German.Pronouns.sich = { form := "sich", person := some Person.third }

def German.Pronouns.einander : ReciprocalPronoun

The reciprocal einander 'each other', invariant for person, number and case. It fuses ein 'one' and ander 'other' ([GH08]) into a single word that also compounds with a preposition (an-einander, miteinander), the kind of fused bipartite form that [Eva08] classes with the reciprocal pronouns.

Equations

• German.Pronouns.einander = { form := "einander" }

Interrogative pronouns

The animate wer declines for the four German cases; the inanimate was has one form for the nominative and the accusative and no dative. Each paradigm is a partial map from case to form, so Morphology.formCells reads the cases a form realizes straight off it.

def German.Pronouns.wer : Case → Option String

The paradigm of wer 'who'.

Equations

• German.Pronouns.wer German.Case.nom = some "wer"
• German.Pronouns.wer German.Case.acc = some "wen"
• German.Pronouns.wer German.Case.dat = some "wem"
• German.Pronouns.wer German.Case.gen = some "wessen"

def German.Pronouns.was : Case → Option String

The paradigm of was 'what'.

Equations

• German.Pronouns.was German.Case.nom = some "was"
• German.Pronouns.was German.Case.acc = some "was"
• German.Pronouns.was German.Case.gen = some "wessen"
• German.Pronouns.was German.Case.dat = none

theorem German.Pronouns.wer_isSome (c : Case) : (wer c).isSome = true

wer has a form for every case.

theorem German.Pronouns.was_isSome_iff (c : Case) : (was c).isSome = true ↔ c ≠ Case.dat

was has a form for every case but the dative.