Kramer (2020): Grammatical Gender: A Close Look at Gender Assignment Across Languages

This file formalizes the review's account of how nouns are sorted into genders. Every gender system assigns gender to some nouns by animacy, humanness, or social gender/biological sex, the semantic core generalization, and the remainder nouns take one gender or several, recycled from the core or novel, in every combination (Table 2). Russian's remainder follows declension class up to the Class III exceptions, and Hausa's feminine remainder ends in -ā, a correlation that fails in the other direction. Against these facts the review sets the lexical rules of [Har91] beside the gender-on-n analysis of [Kra15] for Spanish: the two agree on Spanish, but a lexical entry holds one gender feature, so hybrid nouns call for a second structural source, and the thesis of radical interpretability derives the semantic core from the structural account alone.

Implementation notes

The semantic core generalization is checked over the assignment survey of Corbett1991, and the Spanish, Russian, and Hausa data are the Fragments' nouns rather than the review's tables; Remainder.spanish reads the split of Table 1 off the Fragment, and the two assignment accounts are compared on every noun of the Fragment's shape rather than on its list. The determiner items of (25) go through the library's Subset Principle, so el for [−fem] and for featureless n is a computation rather than a listing. The hybrid datum (27) is the one hand-typed example, since the Russian Fragment records only the morphological gender of vrač.

References

• [Kra20]
• [Cor91] — the assignment survey and the Russian declension rule
• [Har91] — lexical gender assignment
• [Kra15] — structural gender assignment

The semantic core (§1.2)

def Kramer2020.IsCore : Corbett1991.Criterion → Prop

The minimal properties of (3) are animacy, humanness, and social gender or biological sex.

Equations

• Kramer2020.IsCore Corbett1991.Criterion.animacy = True
• Kramer2020.IsCore Corbett1991.Criterion.humanness = True
• Kramer2020.IsCore Corbett1991.Criterion.sex = True
• Kramer2020.IsCore x✝ = False

@[instance_reducible]

instance Kramer2020.instDecidablePredCriterionIsCore : DecidablePred IsCore

Equations

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

def Kramer2020.SatisfiesSemanticCore (e : Corbett1991.SurveyEntry) : Prop

By the semantic core generalization (2), a language with gender assigns it to some nouns by a property of (3).

Equations

• Kramer2020.SatisfiesSemanticCore e = ∃ b ∈ e.criteria, Kramer2020.IsCore b

@[instance_reducible]

instance Kramer2020.instDecidablePredSurveyEntrySatisfiesSemanticCore : DecidablePred SatisfiesSemanticCore

Equations

• Kramer2020.instDecidablePredSurveyEntrySatisfiesSemanticCore x✝ = id inferInstance

theorem Kramer2020.semantic_core_holds (e : Corbett1991.SurveyEntry) : e ∈ Corbett1991.survey → SatisfiesSemanticCore e

Remainder nouns (§2.3.1)

structure Kramer2020.Remainder (G : Type u_1) : Type u_1

The genders a language assigns semantically and the genders of its remainder nouns.

• core : Finset G
• remainder : Finset G

def Kramer2020.Remainder.AllSame {G : Type u_1} (r : Remainder G) : Prop

The remainder nouns all take one gender.

Equations

• r.AllSame = (r.remainder.card = 1)

def Kramer2020.Remainder.Recycled {G : Type u_1} (r : Remainder G) : Prop

The remainder genders are recycled from the core.

Equations

• r.Recycled = (r.remainder ⊆ r.core)

def Kramer2020.Remainder.Novel {G : Type u_1} (r : Remainder G) : Prop

The remainder genders are novel.

Equations

• r.Novel = Disjoint r.remainder r.core

def Kramer2020.Remainder.Mixed {G : Type u_1} (r : Remainder G) : Prop

Recycled and novel genders both occur.

Equations

• r.Mixed = (¬r.Recycled ∧ ¬r.Novel)

@[instance_reducible]

instance Kramer2020.Remainder.instDecidableAllSame {G : Type u_1} (r : Remainder G) : Decidable r.AllSame

Equations

• r.instDecidableAllSame = { decide := r.remainder.card.beq 1, reflects_decide := ⋯ }

@[instance_reducible]

instance Kramer2020.Remainder.instDecidableRecycledOfDecidableEq {G : Type u_1} (r : Remainder G) [DecidableEq G] : Decidable r.Recycled

Equations

• r.instDecidableRecycledOfDecidableEq = { decide := decide (∀ a ∈ r.remainder.val.attach, (fun (x : G) (a : x ∈ r.remainder) => x ∈ r.core) ↑a ⋯), reflects_decide := ⋯ }

@[instance_reducible]

instance Kramer2020.Remainder.instDecidableNovelOfDecidableEq {G : Type u_1} (r : Remainder G) [DecidableEq G] : Decidable r.Novel

Equations

• r.instDecidableNovelOfDecidableEq = { decide := decide (∀ ⦃a : G⦄, a ∈ r.remainder → a ∉ r.core), reflects_decide := ⋯ }

@[instance_reducible]

instance Kramer2020.Remainder.instDecidableMixedOfDecidableEq {G : Type u_1} (r : Remainder G) [DecidableEq G] : Decidable r.Mixed

Equations

• r.instDecidableMixedOfDecidableEq = { decide := decide ¬r.Recycled && decide ¬r.Novel, reflects_decide := ⋯ }

theorem Kramer2020.Remainder.not_mixed_of_allSame {G : Type u_1} (r : Remainder G) (h : r.AllSame) : ¬r.Mixed

The cell of Table 2 marked not applicable is empty, since a single remainder gender is recycled or novel but not both.

def Kramer2020.Remainder.ofNouns {N : Type u_2} (nouns : List N) (natural : N → Bool) (gender : N → Gender) : Remainder Gender

The core and remainder genders of a lexicon with a natural-gender field.

Equations

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

def Kramer2020.Remainder.dieri : Remainder Gender

Dieri makes female humans feminine and male humans and every other noun masculine.

Equations

• Kramer2020.Remainder.dieri = { core := {Gender.masculine, Gender.feminine}, remainder := {Gender.masculine} }

def Kramer2020.Remainder.tamil : Remainder Gender

Tamil has Dieri's core and puts the remainder in a novel neuter.

Equations

• Kramer2020.Remainder.tamil = { core := {Gender.masculine, Gender.feminine}, remainder := {Gender.neuter} }

def Kramer2020.Remainder.spanish : Remainder Gender

Spanish splits the remainder arbitrarily over both core genders (Table 1), as the Fragment records.

Equations

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

def Kramer2020.Remainder.blackfoot : Remainder Gender

Blackfoot makes animates animate and puts inanimates in a novel inanimate gender or the recycled animate one.

Equations

• Kramer2020.Remainder.blackfoot = { core := {Gender.animate}, remainder := {Gender.animate, Gender.inanimate} }

theorem Kramer2020.Remainder.table2 : dieri.AllSame ∧ dieri.Recycled ∧ tamil.AllSame ∧ tamil.Novel ∧ ¬spanish.AllSame ∧ spanish.Recycled ∧ ¬blackfoot.AllSame ∧ blackfoot.Mixed

Table 2 has one remainder gender recycled (Dieri) or novel (Tamil), and different remainder genders recycled (Spanish) or both (Blackfoot).

theorem Kramer2020.Remainder.akoose_cell (r : Remainder ℕ) (hcore : r.core = {1}) (hcard : 7 ≤ r.remainder.card) (h : 1 ∉ r.remainder) : ¬r.AllSame ∧ r.Novel

Akɔɔse has the human gender as its core and at least seven other remainder genders, so its remainder takes different, novel genders.

Declension class in Russian (§2.3.2)

def Kramer2020.declensionGender : Russian.Gender.DeclClass → Gender

[Cor91]'s assignment for the Russian remainder (18) makes Class I masculine, Class II or III feminine, and all others neuter.

Equations

• Kramer2020.declensionGender Russian.Gender.DeclClass.I = Gender.masculine
• Kramer2020.declensionGender Russian.Gender.DeclClass.II = Gender.feminine
• Kramer2020.declensionGender Russian.Gender.DeclClass.III = Gender.feminine
• Kramer2020.declensionGender Russian.Gender.DeclClass.IV = Gender.neuter

theorem Kramer2020.declension_exceptions : List.filter (fun (n : Russian.Gender.Noun) => decide (Option.map declensionGender n.declClass ≠ some n.gender.toLabel)) Russian.Gender.remainderNouns = [Russian.Gender.znamja, Russian.Gender.put']

(18) misassigns exactly the Class III nouns of (19), neuter znamja and masculine put'.

The final vowel in Hausa (§2.3.2, §3.3.1)

def Kramer2020.phonologicalRule (n : Hausa.Noun) : Gender

The disputed rule (26) makes a noun in -ā feminine and any other masculine.

Equations

• Kramer2020.phonologicalRule n = if n.EndsInAa then Gender.feminine else Gender.masculine

theorem Kramer2020.phonologicalRule_kada : phonologicalRule Hausa.kada ≠ Hausa.kada.gender

In (22e) kadā̀ 'crocodile' ends in -ā and is masculine, so (26) is false.

theorem Kramer2020.feminine_remainder_aa (n : Hausa.Noun) : n ∈ Hausa.allNouns → ¬GenderedNoun.IsNaturalGender id n → n.gender = Gender.feminine → n.EndsInAa

In its valid direction, every feminine noun outside the semantic core ends in -ā.

Lexical gender assignment (§3.2)

structure Kramer2020.LexicalEntry : Type

A lexical entry in [Har91]'s system bears the semantic features [human] and [female] and the gender feature [f].

• human : Bool
• female : Bool
• f : Bool

@[instance_reducible]

instance Kramer2020.instDecidableEqLexicalEntry : DecidableEq LexicalEntry

Equations

• Kramer2020.instDecidableEqLexicalEntry = Kramer2020.instDecidableEqLexicalEntry.decEq

def Kramer2020.instDecidableEqLexicalEntry.decEq (x✝ x✝¹ : LexicalEntry) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Kramer2020.instReprLexicalEntry : Repr LexicalEntry

Equations

• Kramer2020.instReprLexicalEntry = { reprPrec := Kramer2020.instReprLexicalEntry.repr }

def Kramer2020.instReprLexicalEntry.repr : LexicalEntry → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Kramer2020.instFintypeLexicalEntry : Fintype LexicalEntry

Equations

• Kramer2020.instFintypeLexicalEntry = Fintype.ofEquiv ((_ : Bool) × (_ : Bool) × Bool) Kramer2020.LexicalEntry.proxyTypeEquiv

def Kramer2020.LexicalEntry.humanCloning (e : LexicalEntry) : List LexicalEntry

Human Cloning (Figure 1) doubles a [human] entry into a [male] and a [female] entry.

Equations

• e.humanCloning = if e.human = true then [{ human := e.human, female := false, f := e.f }, { human := e.human, female := true, f := e.f }] else [e]

def Kramer2020.LexicalEntry.humanGender (e : LexicalEntry) : LexicalEntry

The Human Gender rule (23) is [female] → [f] / __ [human].

Equations

• e.humanGender = { human := e.human, female := e.female, f := e.f || e.human && e.female }

def Kramer2020.LexicalEntry.gender (e : LexicalEntry) : Gender

Agreement is feminine with [f] and masculine by default.

Equations

• e.gender = if e.f = true then Gender.feminine else Gender.masculine

def Kramer2020.lexicalEntry (n : Spanish.Gender.Noun) : LexicalEntry

A Fragment noun's lexical entry has [human] for the natural-gender nouns (higher animals honoris causa), [female] for the female-denoting ones, and a listed [f] for the arbitrarily feminine remainder.

Equations

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

theorem Kramer2020.lexical_faithful (n : Spanish.Gender.Noun) : (lexicalEntry n).humanGender.gender = n.gender.toLabel

The lexical account recovers the gender of every noun of the Fragment's shape.

theorem Kramer2020.persona_cloned_feminine : List.map (fun (x : LexicalEntry) => x.humanGender.gender) { human := true, female := false, f := true }.humanCloning = [Gender.feminine, Gender.feminine]

persona, listed with [f], stays feminine under Human Cloning.

Structural gender assignment (§3.2)

def Kramer2020.spanishHeads : List DistributedMorphology.Categorizer.Head

The four n's of (24).

Equations

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

def Kramer2020.nHead (n : Spanish.Gender.Noun) : DistributedMorphology.Categorizer.Head

A Fragment noun's n bears interpretable gender for the natural-gender nouns and u[+fem] for the arbitrarily feminine remainder, persona among them, and is plain otherwise.

Equations

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

theorem Kramer2020.nHead_mem_spanishHeads (n : Spanish.Gender.Noun) : nHead n ∈ spanishHeads

inductive Kramer2020.DetFeature : Type

A definite determiner bears [d], [def], and the gender it acquires by agreement.

• d : DetFeature
• definite : DetFeature
• gender (v : DistributedMorphology.GenderValue) : DetFeature

@[instance_reducible]

instance Kramer2020.instDecidableEqDetFeature : DecidableEq DetFeature

Equations

• Kramer2020.instDecidableEqDetFeature = Kramer2020.instDecidableEqDetFeature.decEq

def Kramer2020.instDecidableEqDetFeature.decEq (x✝ x✝¹ : DetFeature) : Decidable (x✝ = x✝¹)

Equations

• Kramer2020.instDecidableEqDetFeature.decEq Kramer2020.DetFeature.d Kramer2020.DetFeature.d = isTrue ⋯
• Kramer2020.instDecidableEqDetFeature.decEq Kramer2020.DetFeature.d Kramer2020.DetFeature.definite = isFalse Kramer2020.instDecidableEqDetFeature.decEq._proof_3
• Kramer2020.instDecidableEqDetFeature.decEq Kramer2020.DetFeature.d (Kramer2020.DetFeature.gender v) = isFalse ⋯
• Kramer2020.instDecidableEqDetFeature.decEq Kramer2020.DetFeature.definite Kramer2020.DetFeature.d = isFalse Kramer2020.instDecidableEqDetFeature.decEq._proof_5
• Kramer2020.instDecidableEqDetFeature.decEq Kramer2020.DetFeature.definite Kramer2020.DetFeature.definite = isTrue ⋯
• Kramer2020.instDecidableEqDetFeature.decEq Kramer2020.DetFeature.definite (Kramer2020.DetFeature.gender v) = isFalse ⋯
• Kramer2020.instDecidableEqDetFeature.decEq (Kramer2020.DetFeature.gender v) Kramer2020.DetFeature.d = isFalse ⋯
• Kramer2020.instDecidableEqDetFeature.decEq (Kramer2020.DetFeature.gender v) Kramer2020.DetFeature.definite = isFalse ⋯
• Kramer2020.instDecidableEqDetFeature.decEq (Kramer2020.DetFeature.gender a) (Kramer2020.DetFeature.gender b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Kramer2020.instReprDetFeature.repr : DetFeature → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Kramer2020.instReprDetFeature.repr Kramer2020.DetFeature.d prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Kramer2020.DetFeature.d")).group prec✝

@[instance_reducible]

instance Kramer2020.instReprDetFeature : Repr DetFeature

Equations

• Kramer2020.instReprDetFeature = { reprPrec := Kramer2020.instReprDetFeature.repr }

def Kramer2020.determinerFeatures (ch : DistributedMorphology.Categorizer.Head) : List DetFeature

What the determiner carries after agreeing with a head.

Equations

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

def Kramer2020.determiners : List (DistributedMorphology.VocabularyItem DetFeature String)

Of the Spanish definite determiners (25), la carries [+fem] and el is underspecified.

Equations

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

def Kramer2020.determiner (ch : DistributedMorphology.Categorizer.Head) : Option String

The determiner a head takes, by the Subset Principle.

Equations

• Kramer2020.determiner ch = DistributedMorphology.subsetPrinciple Kramer2020.determiners ↑(Kramer2020.determinerFeatures ch)

theorem Kramer2020.determiner_iMasc_eq_plain : determiner DistributedMorphology.Categorizer.Head.n_iMasc = some "el" ∧ determiner DistributedMorphology.Categorizer.Head.n_plain = some "el"

A determiner with [−fem] and one with no gender feature both take el: la carries a feature neither bears.

theorem Kramer2020.determiner_iFem_eq_uFem : determiner DistributedMorphology.Categorizer.Head.n_iFem = some "la" ∧ determiner DistributedMorphology.Categorizer.Head.n_uFem = some "la"

Natural and arbitrary feminine share la, since both bear [+fem].

def Kramer2020.expectedDeterminer : Spanish.Gender.Value → String

The determiner a gender value calls for.

Equations

• Kramer2020.expectedDeterminer Spanish.Gender.Value.fem = "la"
• Kramer2020.expectedDeterminer Spanish.Gender.Value.masc = "el"

theorem Kramer2020.structural_faithful (n : Spanish.Gender.Noun) : determiner (nHead n) = some (expectedDeterminer n.gender)

The structural account recovers the gender of every noun of the Fragment's shape.

theorem Kramer2020.lexical_eq_structural (n : Spanish.Gender.Noun) : (lexicalEntry n).humanGender.gender = Gender.feminine ↔ determiner (nHead n) = some "la"

On Spanish the two accounts agree (§3.3), noun by noun.

Hybrid nouns (§3.3.2)

def Kramer2020.hybridTargets : List (String × Gender)

In (27) the agreement targets of vrač 'doctor', the Fragment's morphologically masculine Class I noun, take both genders in one phrase.

Equations

• Kramer2020.hybridTargets = [("xoroš-aja", Gender.feminine), ("glavn-yj", Gender.masculine)]

theorem Kramer2020.no_lexical_hybrid {targets : List (String × Gender)} (hf : ∃ t ∈ targets, t.2 = Gender.feminine) (hm : ∃ t ∈ targets, t.2 = Gender.masculine) : ¬∃ (e : LexicalEntry), ∀ t ∈ targets, t.2 = e.gender

No lexical entry fits agreement targets of both genders, since an entry has one gender; the structural account adds a second source of gender features above n.

theorem Kramer2020.lexical_no_hybrid : ¬∃ (e : LexicalEntry), ∀ t ∈ hybridTargets, t.2 = e.gender

(27) is such a case.

Radical interpretability and the semantic core (§3.3.3)

def Kramer2020.RadicallyInterpretable (fs : List DistributedMorphology.GenderFeature) : Prop

The thesis of radical interpretability (29) requires of a language's gender features that an uninterpretable instantiation of a dimension imply an interpretable one.

Equations

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

@[instance_reducible]

instance Kramer2020.instDecidableRadicallyInterpretable (fs : List DistributedMorphology.GenderFeature) : Decidable (RadicallyInterpretable fs)

Equations

• Kramer2020.instDecidableRadicallyInterpretable fs = id inferInstance

theorem Kramer2020.spanish_radicallyInterpretable : RadicallyInterpretable (List.filterMap (fun (x : DistributedMorphology.Categorizer.Head) => x.gender) spanishHeads)

theorem Kramer2020.exists_interpretable {fs : List DistributedMorphology.GenderFeature} (h : RadicallyInterpretable fs) (hne : fs ≠ []) : ∃ gf ∈ fs, gf.interp = Minimalist.Interpretability.interpretable

Under radical interpretability a language with gender features has an interpretable one, so some nouns are gendered semantically: the semantic core, from the structural account.

theorem Kramer2020.lexical_allows_arbitrary_only : ∃ (L : List LexicalEntry), (∀ e ∈ L, e.human = false) ∧ (∃ e ∈ L, e.gender = Gender.feminine) ∧ ∃ e ∈ L, e.gender = Gender.masculine

The lexical account excludes nothing, since a lexicon whose two agreement classes track no semantic feature is well formed, though no such language is attested.