Surface Gender

@cite{corbett-1991} @cite{kramer-2020}

Descriptive (atheoretical) classification of surface gender values attested cross-linguistically. This type records the observable gender of a noun — what agreement class it triggers — without committing to the mechanism of gender assignment.

The distinction between sex-based systems (masculine/feminine/neuter) and animacy-based systems (animate/inanimate) follows @cite{corbett-1991}'s WALS Chapter 31. @cite{kramer-2020} argues that these surface categories arise from a single underlying mechanism (phi-features on the nominalizing head n), parameterized by feature dimension; that analysis lives in Morphology.DM.Categorizer.

For languages with many noun classes (Bantu, Mixtec), the fragment retains its own fine-grained Gender type and provides a bridge to SurfaceGender via a .primary function.

inductive Features.SurfaceGender : Type

Surface gender categories attested cross-linguistically.

These are the descriptive labels a grammar assigns to nouns based on agreement patterns. For the structural analysis, see Morphology.DM.GenderFeature.

• masculine : SurfaceGender

  Masculine: male humans/higher animates; default in many sex-based systems.

• feminine : SurfaceGender

  Feminine: female humans/higher animates; marked in many sex-based systems.

• neuter : SurfaceGender

  Neuter: neither masculine nor feminine; inanimate default in 3-gender systems.

• common : SurfaceGender

  Common: merged masculine + feminine (Swedish, Danish).

• animate : SurfaceGender

  Animate: animate referents in animacy-based systems (Teop, Algonquian).

• inanimate : SurfaceGender

  Inanimate: inanimate referents in animacy-based systems.

@[implicit_reducible]

instance Features.instDecidableEqSurfaceGender : DecidableEq SurfaceGender

Equations

• Features.instDecidableEqSurfaceGender x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.instReprSurfaceGender.repr : SurfaceGender → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.instReprSurfaceGender : Repr SurfaceGender

Equations

• Features.instReprSurfaceGender = { reprPrec := Features.instReprSurfaceGender.repr }

@[implicit_reducible]

instance Features.instInhabitedSurfaceGender : Inhabited SurfaceGender

Equations

• Features.instInhabitedSurfaceGender = { default := Features.instInhabitedSurfaceGender.default }

def Features.instInhabitedSurfaceGender.default : SurfaceGender

Equations

• Features.instInhabitedSurfaceGender.default = Features.SurfaceGender.masculine

@[implicit_reducible]

instance Features.instBEqSurfaceGender : BEq SurfaceGender

Equations

• Features.instBEqSurfaceGender = { beq := Features.instBEqSurfaceGender.beq }

def Features.instBEqSurfaceGender.beq : SurfaceGender → SurfaceGender → Bool

Equations

• Features.instBEqSurfaceGender.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Features.SurfaceGender.toUDGender : SurfaceGender → Option UD.Gender

Map surface gender to Universal Dependencies gender where a natural correspondence exists. Animacy-based genders have no standard UD equivalent.

Equations

• Features.SurfaceGender.masculine.toUDGender = some UD.Gender.Masc
• Features.SurfaceGender.feminine.toUDGender = some UD.Gender.Fem
• Features.SurfaceGender.neuter.toUDGender = some UD.Gender.Neut
• Features.SurfaceGender.common.toUDGender = some UD.Gender.Com
• Features.SurfaceGender.animate.toUDGender = none
• Features.SurfaceGender.inanimate.toUDGender = none

def Features.SurfaceGender.ofUDGender : UD.Gender → SurfaceGender

Inverse: map UD gender to surface gender. Total (every UD gender has a surface gender equivalent).

Equations

• Features.SurfaceGender.ofUDGender UD.Gender.Masc = Features.SurfaceGender.masculine
• Features.SurfaceGender.ofUDGender UD.Gender.Fem = Features.SurfaceGender.feminine
• Features.SurfaceGender.ofUDGender UD.Gender.Neut = Features.SurfaceGender.neuter
• Features.SurfaceGender.ofUDGender UD.Gender.Com = Features.SurfaceGender.common

theorem Features.SurfaceGender.roundtrip_ud (g : UD.Gender) : (ofUDGender g).toUDGender = some g

Round-trip: UD → Surface → UD is the identity.

Gender Features (@cite{sauerland-2003})

Binary feature decomposition of sex-based gender:

• [±feminine]: whether the referent triggers feminine agreement. Feminine and neuter are [+feminine]; masculine is [−feminine].
• [±neuter]: whether the referent triggers neuter agreement. Only neuter is [+neuter]; feminine and masculine are [−neuter].

These features form a containment hierarchy: [+neuter] → [+feminine]. This is a feature-geometric claim from @cite{sauerland-2003} §6, not a natural-kind claim: neuter is the most specified gender (like singular for number, 1st for person), and masculine is the least specified (like plural, 3rd).

The three well-formed combinations yield the three gender values:

• neuter: [+feminine, +neuter] — maximal (presupposes inanimate)
• feminine: [+feminine, −neuter] — intermediate (presupposes female)
• masculine: [−feminine, −neuter] — minimal (vacuous/default)

This parallels person [±author] ⊂ [±participant] and number [±atomic] ⊂ [±minimal]. All three are instances of PhiFeatures.

For the morphosyntactic (DM) analysis, see Morphology.DM.Categorizer.GenderFeature.

structure Features.Gender.Features : Type

Binary gender features: [±feminine, ±neuter].

These two features suffice for the three-way gender distinction:

• neuter: [+feminine, +neuter]
• feminine: [+feminine, −neuter]
• masculine: [−feminine, −neuter]

The fourth combination [−feminine, +neuter] is ill-formed: a neuter entity necessarily triggers feminine agreement ([+neuter] → [+feminine] in the feature geometry).

• isFeminine : Bool

  [+feminine]: referent triggers feminine (or neuter) agreement.

• isNeuter : Bool

  [+neuter]: referent triggers neuter agreement.

def Features.Gender.instDecidableEqFeatures.decEq (x✝ x✝¹ : Features) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Features.Gender.instDecidableEqFeatures : DecidableEq Features

Equations

• Features.Gender.instDecidableEqFeatures = Features.Gender.instDecidableEqFeatures.decEq

def Features.Gender.instReprFeatures.repr : Features → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Gender.instReprFeatures : Repr Features

Equations

• Features.Gender.instReprFeatures = { reprPrec := Features.Gender.instReprFeatures.repr }

def Features.Gender.Features.wellFormed (gf : Features) : Bool

Well-formedness: [+neuter] → [+feminine]. Neuter entails feminine in the feature geometry.

Equations

• gf.wellFormed = (!gf.isNeuter || gf.isFeminine)

def Features.Gender.neuterF : Features

Neuter features: [+feminine, +neuter].

Equations

• Features.Gender.neuterF = { isFeminine := true, isNeuter := true }

def Features.Gender.feminineF : Features

Feminine features: [+feminine, −neuter].

Equations

• Features.Gender.feminineF = { isFeminine := true, isNeuter := false }

def Features.Gender.masculineF : Features

Masculine features: [−feminine, −neuter].

Equations

• Features.Gender.masculineF = { isFeminine := false, isNeuter := false }

@[implicit_reducible]

instance Features.Gender.instPhiFeaturesFeatures : PhiFeatures Features

Gender features are a PhiFeatures instance: outer = isFeminine, inner = isNeuter.

The containment [+neuter] → [+feminine] maps to PrivativePair's [+inner] → [+outer], unifying the structure with person and number. All shared properties are inherited by construction.

Equations

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

@[simp]

theorem Features.Gender.neuter_is_maximal : PhiFeatures.toPair neuterF = PrivativePair.maximal

The three canonical gender values map to the three PrivativePair cells.

@[simp]

theorem Features.Gender.feminine_is_intermediate : PhiFeatures.toPair feminineF = PrivativePair.intermediate

@[simp]

theorem Features.Gender.masculine_is_minimal : PhiFeatures.toPair masculineF = PrivativePair.minimal

theorem Features.Gender.no_fourth_gender (a b c d : Features) : a.wellFormed = true → b.wellFormed = true → c.wellFormed = true → d.wellFormed = true → a ≠ b → a ≠ c → a ≠ d → b ≠ c → b ≠ d → c ≠ d → False

No 4-way gender distinction (inherited from PhiFeatures).

@[simp]

theorem Features.Gender.neuter_wellFormed : neuterF.wellFormed = true

@[simp]

theorem Features.Gender.feminine_wellFormed : feminineF.wellFormed = true

@[simp]

theorem Features.Gender.masculine_wellFormed : masculineF.wellFormed = true

theorem Features.Gender.illFormed_only : { isFeminine := false, isNeuter := true }.wellFormed = false

The ill-formed combination [−feminine, +neuter] is the only combination that violates well-formedness.

theorem Features.Gender.exactly_three_wellFormed : (List.filter Features.wellFormed [{ isFeminine := true, isNeuter := true }, { isFeminine := true, isNeuter := false }, { isFeminine := false, isNeuter := true }, { isFeminine := false, isNeuter := false }]).length = 3

There are exactly 3 well-formed feature combinations (= 3 genders).

theorem Features.Gender.neuter_implies_feminine (f : Features) (hw : f.wellFormed = true) : f.isNeuter = true → f.isFeminine = true

Containment: [+neuter] → [+feminine] for all well-formed features.

def Features.Gender.Features.toSurfaceGender : Features → Option SurfaceGender

Map gender features to the descriptive SurfaceGender type.

Equations

• { isFeminine := true, isNeuter := true }.toSurfaceGender = some Features.SurfaceGender.neuter
• { isFeminine := true, isNeuter := false }.toSurfaceGender = some Features.SurfaceGender.feminine
• { isFeminine := false, isNeuter := false }.toSurfaceGender = some Features.SurfaceGender.masculine
• { isFeminine := false, isNeuter := true }.toSurfaceGender = none

def Features.Gender.Features.fromSurfaceGender : SurfaceGender → Option Features

Map SurfaceGender to gender features (partial — only sex-based genders have feature equivalents).

Equations

• Features.Gender.Features.fromSurfaceGender Features.SurfaceGender.neuter = some Features.Gender.neuterF
• Features.Gender.Features.fromSurfaceGender Features.SurfaceGender.feminine = some Features.Gender.feminineF
• Features.Gender.Features.fromSurfaceGender Features.SurfaceGender.masculine = some Features.Gender.masculineF
• Features.Gender.Features.fromSurfaceGender x✝ = none

theorem Features.Gender.roundtrip_fromSG_toSG : ([neuterF, feminineF, masculineF].all fun (f : Features) => f.toSurfaceGender.bind Features.fromSurfaceGender == some f) = true

Round-trip: fromSurfaceGender ∘ toSurfaceGender = some for all well-formed features.

inductive Features.GenderInfo : Type

Gender knowledge state for a discourse referent.

Distinct from SurfaceGender, which describes the morphosyntactic agreement class a noun triggers. GenderInfo describes what the discourse participants know or assume about a referent's gender.

Motivated by @cite{arnold-2026}'s observation that singular they is licensed by two inversely correlated pragmatic conditions: one requiring an underspecified discourse representation (where gender is unknown or irrelevant), the other requiring knowledge that the referent's personal pronouns are they/them (where gender information is highly specific).

See also @cite{newman-1992} ("nonsolid" antecedents), @cite{newman-1998} (low individuation), and @cite{camilliere-etal-2021} (social distance as a proxy for discourse specificity).

• known : SurfaceGender → GenderInfo

  Gender is known to discourse participants and matches a morphosyntactic agreement class. Example: "my sister" → .known .feminine

• unspecified : GenderInfo

  Gender is unknown, irrelevant, or not elaborated in the discourse. Example: "every student", "someone", "the clerk" (in passing).

@[implicit_reducible]

instance Features.instDecidableEqGenderInfo : DecidableEq GenderInfo

Equations

• Features.instDecidableEqGenderInfo = Features.instDecidableEqGenderInfo.decEq

def Features.instDecidableEqGenderInfo.decEq (x✝ x✝¹ : GenderInfo) : Decidable (x✝ = x✝¹)

Equations

• Features.instDecidableEqGenderInfo.decEq (Features.GenderInfo.known a) (Features.GenderInfo.known b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Features.instDecidableEqGenderInfo.decEq (Features.GenderInfo.known a) Features.GenderInfo.unspecified = isFalse ⋯
• Features.instDecidableEqGenderInfo.decEq Features.GenderInfo.unspecified (Features.GenderInfo.known a) = isFalse ⋯
• Features.instDecidableEqGenderInfo.decEq Features.GenderInfo.unspecified Features.GenderInfo.unspecified = isTrue ⋯

def Features.instReprGenderInfo.repr : GenderInfo → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.instReprGenderInfo : Repr GenderInfo

Equations

• Features.instReprGenderInfo = { reprPrec := Features.instReprGenderInfo.repr }

@[implicit_reducible]

instance Features.instBEqGenderInfo : BEq GenderInfo

Equations

• Features.instBEqGenderInfo = { beq := Features.instBEqGenderInfo.beq }

def Features.instBEqGenderInfo.beq : GenderInfo → GenderInfo → Bool

Equations

• Features.instBEqGenderInfo.beq (Features.GenderInfo.known a) (Features.GenderInfo.known b) = (a == b)
• Features.instBEqGenderInfo.beq Features.GenderInfo.unspecified Features.GenderInfo.unspecified = true
• Features.instBEqGenderInfo.beq x✝¹ x✝ = false

def Features.SurfaceGender.toGenderInfo (g : SurfaceGender) : GenderInfo

Lift a surface gender to discourse-level knowledge.

Equations

• g.toGenderInfo = Features.GenderInfo.known g

def Features.GenderInfo.toSurfaceGender : GenderInfo → Option SurfaceGender

Extract the surface gender, if known.

Equations

• (Features.GenderInfo.known a).toSurfaceGender = some a
• Features.GenderInfo.unspecified.toSurfaceGender = none

theorem Features.GenderInfo.roundtrip_known (g : SurfaceGender) : g.toGenderInfo.toSurfaceGender = some g

Round-trip: known surface gender survives the coarsening.