German gender

This file defines the three German genders and the suffixes that fix the gender of a noun. German has three controller genders, the masculine, the feminine and the neuter. The determiners and the adjectives distinguish them in the singular and not in the plural, and German.Determiners records that evidence. A noun's gender follows its meaning for many nouns denoting persons and animals, and its ending for many others. Of the endings Durrell tabulates, -heit ~ -keit, -schaft and -ung make a noun feminine and the diminutives -chen and -lein make it neuter, and for these five he gives no exception. The diminutives do so whatever the sex of the referent: Mädchen 'girl' and Fräulein 'young lady' are neuter, like Bübchen 'little boy'. Determiners and adjectives agree with that gender, relative pronouns almost always do, and personal pronouns often follow the sex of the referent instead, especially in speech.

Main definitions

• German.Gender.Value: the three genders.
• German.Gender.Suffix, German.Gender.Suffix.gender: the suffixes that fix the gender of the nouns they end, and the gender each fixes.
• German.Gender.Suffix.noun: a noun ending in such a suffix, whose gender is the suffix's.

References

• [Dur11]

inductive German.Gender.Value : Type

German has three controller genders.

• masc : Value
• fem : Value
• neut : Value

@[instance_reducible]

instance German.Gender.instDecidableEqValue : DecidableEq Value

Equations

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

@[instance_reducible]

instance German.Gender.instReprValue : Repr Value

Equations

• German.Gender.instReprValue = { reprPrec := German.Gender.instReprValue.repr }

def German.Gender.instReprValue.repr : Value → ℕ → Std.Format

Equations

• German.Gender.instReprValue.repr German.Gender.Value.masc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "German.Gender.Value.masc")).group prec✝
• German.Gender.instReprValue.repr German.Gender.Value.fem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "German.Gender.Value.fem")).group prec✝
• German.Gender.instReprValue.repr German.Gender.Value.neut prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "German.Gender.Value.neut")).group prec✝

@[instance_reducible]

instance German.Gender.instFintypeValue : Fintype Value

Equations

• German.Gender.instFintypeValue = { elems := { val := ↑German.Gender.Value.enumList, nodup := German.Gender.Value.enumList_nodup }, complete := German.Gender.instFintypeValue._proof_1 }

def German.Gender.Value.toLabel : Value → Gender

Each German gender bears the comparative label of the same name.

Equations

• German.Gender.Value.masc.toLabel = Gender.masculine
• German.Gender.Value.fem.toLabel = Gender.feminine
• German.Gender.Value.neut.toLabel = Gender.neuter

inductive German.Gender.Suffix : Type

The suffixes that fix the gender of every noun they end.

• heit : Suffix
• keit : Suffix
• schaft : Suffix
• ung : Suffix
• chen : Suffix
• lein : Suffix

@[instance_reducible]

instance German.Gender.instDecidableEqSuffix : DecidableEq Suffix

Equations

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

@[instance_reducible]

instance German.Gender.instReprSuffix : Repr Suffix

Equations

• German.Gender.instReprSuffix = { reprPrec := German.Gender.instReprSuffix.repr }

def German.Gender.instReprSuffix.repr : Suffix → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• German.Gender.instReprSuffix.repr German.Gender.Suffix.heit prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "German.Gender.Suffix.heit")).group prec✝
• German.Gender.instReprSuffix.repr German.Gender.Suffix.keit prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "German.Gender.Suffix.keit")).group prec✝
• German.Gender.instReprSuffix.repr German.Gender.Suffix.ung prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "German.Gender.Suffix.ung")).group prec✝
• German.Gender.instReprSuffix.repr German.Gender.Suffix.chen prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "German.Gender.Suffix.chen")).group prec✝
• German.Gender.instReprSuffix.repr German.Gender.Suffix.lein prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "German.Gender.Suffix.lein")).group prec✝

@[instance_reducible]

instance German.Gender.instFintypeSuffix : Fintype Suffix

Equations

• German.Gender.instFintypeSuffix = { elems := { val := ↑German.Gender.Suffix.enumList, nodup := German.Gender.Suffix.enumList_nodup }, complete := German.Gender.instFintypeSuffix._proof_1 }

def German.Gender.Suffix.form : Suffix → String

s.form is the written form of the suffix s.

Equations

• German.Gender.Suffix.heit.form = "-heit"
• German.Gender.Suffix.keit.form = "-keit"
• German.Gender.Suffix.schaft.form = "-schaft"
• German.Gender.Suffix.ung.form = "-ung"
• German.Gender.Suffix.chen.form = "-chen"
• German.Gender.Suffix.lein.form = "-lein"

def German.Gender.Suffix.gender : Suffix → Value

The suffixes -heit ~ -keit, -schaft and -ung fix the feminine, and the diminutives -chen and -lein the neuter.

Equations

• German.Gender.Suffix.heit.gender = German.Gender.Value.fem
• German.Gender.Suffix.keit.gender = German.Gender.Value.fem
• German.Gender.Suffix.schaft.gender = German.Gender.Value.fem
• German.Gender.Suffix.ung.gender = German.Gender.Value.fem
• German.Gender.Suffix.chen.gender = German.Gender.Value.neut
• German.Gender.Suffix.lein.gender = German.Gender.Value.neut

def German.Gender.Suffix.noun (s : Suffix) (form gloss : String) (naturalGender : Option Gender := none) : GenderedNoun Value

s.noun form gloss is the noun form 'gloss' ending in the suffix s, and its gender is the one s fixes.

Equations

• s.noun form gloss naturalGender = { form := form, gloss := gloss, gender := s.gender, naturalGender := naturalGender }

theorem German.Gender.Suffix.isNaturalGender_noun_iff (s : Suffix) (form gloss : String) (g : Gender) : GenderedNoun.IsNaturalGender Value.toLabel (s.noun form gloss (some g)) ↔ g = s.gender.toLabel

A noun ending in a gender-fixing suffix has natural gender just when its referents' gender is the one the suffix fixes.

Nouns

def German.Gender.krankheit : GenderedNoun Value

Krankheit 'illness' is a noun in -heit.

Equations

• German.Gender.krankheit = German.Gender.Suffix.heit.noun "Krankheit" "illness"

def German.Gender.herrschaft : GenderedNoun Value

Herrschaft 'rule' is a noun in -schaft.

Equations

• German.Gender.herrschaft = German.Gender.Suffix.schaft.noun "Herrschaft" "rule"

def German.Gender.bedeutung : GenderedNoun Value

Bedeutung 'meaning' is a noun in -ung.

Equations

• German.Gender.bedeutung = German.Gender.Suffix.ung.noun "Bedeutung" "meaning"

def German.Gender.buechlein : GenderedNoun Value

Büchlein 'little book' is a noun in -lein.

Equations

• German.Gender.buechlein = German.Gender.Suffix.lein.noun "Büchlein" "little book"

def German.Gender.maedchen : GenderedNoun Value

Mädchen 'girl' is neuter, though its referents are female.

Equations

• German.Gender.maedchen = German.Gender.Suffix.chen.noun "Mädchen" "girl" (some Gender.feminine)

def German.Gender.fraeulein : GenderedNoun Value

Fräulein 'young lady' is neuter, though its referents are female.

Equations

• German.Gender.fraeulein = German.Gender.Suffix.lein.noun "Fräulein" "young lady" (some Gender.feminine)

def German.Gender.buebchen : GenderedNoun Value

Bübchen 'little boy' is neuter, though its referents are male.

Equations

• German.Gender.buebchen = German.Gender.Suffix.chen.noun "Bübchen" "little boy" (some Gender.masculine)

theorem German.Gender.not_isNaturalGender_diminutive : ¬GenderedNoun.IsNaturalGender Value.toLabel maedchen ∧ ¬GenderedNoun.IsNaturalGender Value.toLabel fraeulein ∧ ¬GenderedNoun.IsNaturalGender Value.toLabel buebchen

The diminutives denoting persons are neuter whatever the sex of the referent.