German Derivational Gender: -schaft and related suffixes

[Kra20] [Kra15]

German is a 3-gender language (masculine, feminine, neuter) where certain derivational suffixes deterministically assign gender:

• -schaft → always feminine: Freundschaft, Gesellschaft, Wissenschaft
• -heit, -keit → always feminine: Freiheit, Möglichkeit
• -ung → always feminine: Zeitung, Bildung
• -chen, -lein → always neuter: Mädchen, Büchlein

Theory-neutral data layer

The Fragment carries one empirical field per suffix: assignedGender, the deterministic gender output. No isNaturalGender field — derivational suffixes always assign arbitrary gender (the suffix is the locus of the gender feature, not the root's semantic content). The [Kra15] structural analysis (each suffix IS a categorizing head n with a fixed gender feature: -schaft = n u[+FEM], -chen = plain n) is a projection that lives in Studies/.

The empirical content captured here is the morphological override: Mädchen 'girl' is neuter despite its semantic referent being female, because the diminutive suffix -chen fixes the gender. This is diagnostic for any theory in which suffixes can override semantics.

structure German.Gender.DerivationalSuffix : Type

A German derivational suffix that deterministically assigns gender. Theory-neutral: carries the empirical gender output, not a DM categorizing head.

• form : String
• assignedGender : Gender

  Gender this suffix always assigns, regardless of the base.

@[implicit_reducible]

instance German.Gender.instDecidableEqDerivationalSuffix : DecidableEq DerivationalSuffix

Equations

• German.Gender.instDecidableEqDerivationalSuffix = German.Gender.instDecidableEqDerivationalSuffix.decEq

def German.Gender.instDecidableEqDerivationalSuffix.decEq (x✝ x✝¹ : DerivationalSuffix) : Decidable (x✝ = x✝¹)

Equations

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

def German.Gender.instReprDerivationalSuffix.repr : DerivationalSuffix → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance German.Gender.instReprDerivationalSuffix : Repr DerivationalSuffix

Equations

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

def German.Gender.schaft : DerivationalSuffix

Equations

• German.Gender.schaft = { form := "-schaft", assignedGender := Gender.feminine }

def German.Gender.heit : DerivationalSuffix

Equations

• German.Gender.heit = { form := "-heit", assignedGender := Gender.feminine }

def German.Gender.keit : DerivationalSuffix

Equations

• German.Gender.keit = { form := "-keit", assignedGender := Gender.feminine }

def German.Gender.ung : DerivationalSuffix

Equations

• German.Gender.ung = { form := "-ung", assignedGender := Gender.feminine }

def German.Gender.chen : DerivationalSuffix

Equations

• German.Gender.chen = { form := "-chen", assignedGender := Gender.neuter }

def German.Gender.lein : DerivationalSuffix

Equations

• German.Gender.lein = { form := "-lein", assignedGender := Gender.neuter }

structure German.Gender.DerivedNoun : Type

A German noun derived via a gender-assigning suffix. The noun's surface gender is the suffix's assignedGender (suffix overrides base semantics, e.g. Mädchen).

• form : String
• gloss : String
• suffix : DerivationalSuffix

def German.Gender.instDecidableEqDerivedNoun.decEq (x✝ x✝¹ : DerivedNoun) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance German.Gender.instDecidableEqDerivedNoun : DecidableEq DerivedNoun

Equations

• German.Gender.instDecidableEqDerivedNoun = German.Gender.instDecidableEqDerivedNoun.decEq

def German.Gender.instReprDerivedNoun.repr : DerivedNoun → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance German.Gender.instReprDerivedNoun : Repr DerivedNoun

Equations

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

@[reducible, inline]

abbrev German.Gender.DerivedNoun.gender (n : DerivedNoun) : Gender

Equations

• n.gender = n.suffix.assignedGender

def German.Gender.freundschaft : DerivedNoun

Equations

• German.Gender.freundschaft = { form := "Freundschaft", gloss := "friendship", suffix := German.Gender.schaft }

def German.Gender.gesellschaft : DerivedNoun

Equations

• German.Gender.gesellschaft = { form := "Gesellschaft", gloss := "society", suffix := German.Gender.schaft }

def German.Gender.wissenschaft : DerivedNoun

Equations

• German.Gender.wissenschaft = { form := "Wissenschaft", gloss := "science", suffix := German.Gender.schaft }

def German.Gender.meisterschaft : DerivedNoun

Equations

• German.Gender.meisterschaft = { form := "Meisterschaft", gloss := "championship", suffix := German.Gender.schaft }

def German.Gender.freiheit : DerivedNoun

Equations

• German.Gender.freiheit = { form := "Freiheit", gloss := "freedom", suffix := German.Gender.heit }

def German.Gender.moeglichkeit : DerivedNoun

Equations

• German.Gender.moeglichkeit = { form := "Möglichkeit", gloss := "possibility", suffix := German.Gender.keit }

def German.Gender.zeitung : DerivedNoun

Equations

• German.Gender.zeitung = { form := "Zeitung", gloss := "newspaper", suffix := German.Gender.ung }

def German.Gender.bildung : DerivedNoun

Equations

• German.Gender.bildung = { form := "Bildung", gloss := "education", suffix := German.Gender.ung }

def German.Gender.maedchen : DerivedNoun

Equations

• German.Gender.maedchen = { form := "Mädchen", gloss := "girl", suffix := German.Gender.chen }

def German.Gender.buechlein : DerivedNoun

Equations

• German.Gender.buechlein = { form := "Büchlein", gloss := "booklet", suffix := German.Gender.lein }

def German.Gender.allDerived : List DerivedNoun

Equations

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

theorem German.Gender.feminine_suffixes_assign_feminine : ([freundschaft, gesellschaft, wissenschaft, meisterschaft, freiheit, moeglichkeit, zeitung, bildung].all fun (x : DerivedNoun) => x.gender == Gender.feminine) = true

All -schaft, -heit, -keit, -ung derived nouns surface as feminine — the suffix deterministically assigns feminine. Stated directly over assignedGender (no DM intermediary).

theorem German.Gender.diminutive_suffixes_assign_neuter : chen.assignedGender = Gender.neuter ∧ lein.assignedGender = Gender.neuter

-chen and -lein derived nouns surface as neuter.

theorem German.Gender.maedchen_neuter_override : maedchen.gender = Gender.neuter ∧ maedchen.gloss = "girl"

Mädchen override: Mädchen 'girl' is neuter despite its semantic referent being female. The diminutive suffix -chen overrides the natural-gender expectation — empirical fact that any theory must account for. The DM-specific analysis (suffix IS the n head, plain n → neuter via 3-gender VI) lives in Studies/Kramer2020.lean.