Kramer 2020: Grammatical Gender — A Close Look at Gender Assignment

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

Formalizes the core contributions of @cite{kramer-2020}, a review article that sharpens and extends @cite{kramer-2015}'s structural approach to gender assignment. Three main results:

1. The Semantic Core Generalization (ex. 2/28): every language with grammatical gender assigns gender semantically to at least some nouns, based on animacy, humanness, and/or social gender/biological sex.

2. Lexical vs structural gender assignment (§3): a comparison of @cite{harris-1991}'s lexical rules with @cite{kramer-2015}'s structural n-based approach, identifying three phenomena that differentiate them: phonological assignment (§3.3.1), hybrid nouns (§3.3.2), and the Semantic Core (§3.3.3).

3. Cross-linguistic variation in arbitrary assignment (Table 2): remainder nouns vary along two dimensions — same vs different gender(s), recycled vs novel vs both.

Integration

• Typology ↔ DM bridge: SemanticBasis.toGenderDimension connects the typological SemanticBasis (from Phenomena/Gender/Typology.lean) to the DM GenderDimension (from Theories/Morphology/DM/Categorizer.lean), making explicit that the semantic core properties are the same things parameterized as feature dimensions in the structural approach.

• DM → Minimalism bridge: GenderFeature.toGramFeature (in Categorizer.lean) maps DM gender features to Minimalist GramFeature, with interpretable gender → valued and uninterpretable → unvalued.

• Semantic Core verified: semantic_core_holds proves the generalization over the existing 21-language sample from Typology.lean.

The typological SemanticBasis and the DM GenderDimension describe the same underlying distinction from different perspectives: typology asks what semantic property organizes the system, while DM asks what binary feature sits on n. @cite{kramer-2020} makes this connection explicit by analyzing sex-based systems as [±FEM] or [±MASC], and animacy-based systems as [±ANIM].

The mapping is partial in two ways:

1. SemanticBasis.shape and .rationality have no standard DM feature dimension (no [±SHAPE] or [±RATIONAL] in the literature).

2. SemanticBasis.humanness maps to .anim because @cite{kramer-2015} does not posit a [±HUMAN] dimension — the closest is [±ANIM]. This is a limitation of the current DM feature inventory, not a claim that humanness is a subset of animacy (e.g. Akɔɔse distinguishes human vs nonhuman, which is orthogonal to animate vs inanimate).

def Phenomena.Gender.Typology.SemanticBasis.isCore : SemanticBasis → Bool

Whether a SemanticBasis falls within the semantic core.

@cite{kramer-2020} ex. 3 identifies three core properties; shape and rationality are additional semantic bases (§2.2.1) that go beyond the core but never constitute the only basis for a gender system.

Equations

• Phenomena.Gender.Typology.SemanticBasis.sex.isCore = true
• Phenomena.Gender.Typology.SemanticBasis.animacy.isCore = true
• Phenomena.Gender.Typology.SemanticBasis.humanness.isCore = true
• Phenomena.Gender.Typology.SemanticBasis.shape.isCore = false
• Phenomena.Gender.Typology.SemanticBasis.rationality.isCore = false

def Phenomena.Gender.Typology.GenderProfile.satisfiesSemanticCore (p : GenderProfile) : Bool

The Semantic Core Generalization: a gender profile satisfies it iff it either has no gender system, or at least one of its semantic bases falls within the core {animacy, humanness, social gender/sex}.

Equations

• p.satisfiesSemanticCore = (p.genderCount == Phenomena.Gender.Typology.GenderCount.none || p.semanticBases.any Phenomena.Gender.Typology.SemanticBasis.isCore)

def Phenomena.Gender.Typology.SemanticBasis.toGenderDimension : SemanticBasis → Option Morphology.DM.GenderDimension

Map a typological semantic basis to its corresponding DM gender dimension, when one exists. (@cite{kramer-2020} §3)

The .humanness → .anim mapping reflects a gap in @cite{kramer-2015}'s feature inventory: no [±HUMAN] dimension is posited, so humanness-based systems are approximated by [±ANIM].

Equations

• Phenomena.Gender.Typology.SemanticBasis.sex.toGenderDimension = some Morphology.DM.GenderDimension.fem
• Phenomena.Gender.Typology.SemanticBasis.animacy.toGenderDimension = some Morphology.DM.GenderDimension.anim
• Phenomena.Gender.Typology.SemanticBasis.humanness.toGenderDimension = some Morphology.DM.GenderDimension.anim
• Phenomena.Gender.Typology.SemanticBasis.shape.toGenderDimension = none
• Phenomena.Gender.Typology.SemanticBasis.rationality.toGenderDimension = none

def Morphology.DM.GenderDimension.toSemanticBasis : GenderDimension → Phenomena.Gender.Typology.SemanticBasis

Inverse direction: map a DM gender dimension to its typological basis. (@cite{kramer-2020} §3)

Equations

• Morphology.DM.GenderDimension.fem.toSemanticBasis = Phenomena.Gender.Typology.SemanticBasis.sex
• Morphology.DM.GenderDimension.masc.toSemanticBasis = Phenomena.Gender.Typology.SemanticBasis.sex
• Morphology.DM.GenderDimension.anim.toSemanticBasis = Phenomena.Gender.Typology.SemanticBasis.animacy

theorem Phenomena.Gender.Studies.Kramer2020.semantic_core_holds : (Typology.allProfiles.all fun (x : Typology.GenderProfile) => x.satisfiesSemanticCore) = true

Semantic Core Generalization (@cite{kramer-2020} ex. 2/28): every language in the sample satisfies the semantic core.

theorem Phenomena.Gender.Studies.Kramer2020.no_gender_without_core : (Typology.allProfiles.all fun (p : Typology.GenderProfile) => if (p.genderCount != Typology.GenderCount.none) = true then p.semanticBases.any Typology.SemanticBasis.isCore else true) = true

No language has gender without at least one core semantic basis.

theorem Phenomena.Gender.Studies.Kramer2020.core_properties_have_dimensions : Typology.SemanticBasis.sex.toGenderDimension.isSome = true ∧ Typology.SemanticBasis.animacy.toGenderDimension.isSome = true ∧ Typology.SemanticBasis.humanness.toGenderDimension.isSome = true

Core semantic properties correspond to DM feature dimensions: every core basis has a toGenderDimension target.

theorem Phenomena.Gender.Studies.Kramer2020.noncore_properties_no_dimension : Typology.SemanticBasis.shape.toGenderDimension.isNone = true ∧ Typology.SemanticBasis.rationality.toGenderDimension.isNone = true

Non-core properties lack a standard DM dimension.

theorem Phenomena.Gender.Studies.Kramer2020.roundtrip_sex_fem : Typology.SemanticBasis.sex.toGenderDimension = some Morphology.DM.GenderDimension.fem

Round-trip: .sex → .fem (the default parameterization).

theorem Phenomena.Gender.Studies.Kramer2020.roundtrip_anim : Morphology.DM.GenderDimension.anim.toSemanticBasis.toGenderDimension = some Morphology.DM.GenderDimension.anim

Round-trip: .anim → .animacy → .anim.

inductive Phenomena.Gender.Studies.Kramer2020.RemainderGenderSource : Type

Whether remainder nouns use recycled genders, novel genders, or both. (@cite{kramer-2020} Table 2)

• recycled : RemainderGenderSource
• novel : RemainderGenderSource
• both : RemainderGenderSource

instance Phenomena.Gender.Studies.Kramer2020.instDecidableEqRemainderGenderSource : DecidableEq RemainderGenderSource

Equations

• Phenomena.Gender.Studies.Kramer2020.instDecidableEqRemainderGenderSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Gender.Studies.Kramer2020.instBEqRemainderGenderSource.beq : RemainderGenderSource → RemainderGenderSource → Bool

Equations

• Phenomena.Gender.Studies.Kramer2020.instBEqRemainderGenderSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Gender.Studies.Kramer2020.instBEqRemainderGenderSource : BEq RemainderGenderSource

Equations

• Phenomena.Gender.Studies.Kramer2020.instBEqRemainderGenderSource = { beq := Phenomena.Gender.Studies.Kramer2020.instBEqRemainderGenderSource.beq }

instance Phenomena.Gender.Studies.Kramer2020.instReprRemainderGenderSource : Repr RemainderGenderSource

Equations

• Phenomena.Gender.Studies.Kramer2020.instReprRemainderGenderSource = { reprPrec := Phenomena.Gender.Studies.Kramer2020.instReprRemainderGenderSource.repr }

def Phenomena.Gender.Studies.Kramer2020.instReprRemainderGenderSource.repr : RemainderGenderSource → ℕ → Std.Format

Equations

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

structure Phenomena.Gender.Studies.Kramer2020.RemainderPattern : Type

How remainder nouns (those not assigned gender by the semantic core) are distributed across genders (@cite{kramer-2020} Table 2).

Two independent parameters:

1. Are all remainder nouns in the same gender, or spread across genders?
2. Is the remainder gender recycled, novel, or a mix of both?

• sameGender : Bool

  Are all remainder nouns assigned to a single gender?

• genderSource : RemainderGenderSource

  Source of the remainder gender(s).

def Phenomena.Gender.Studies.Kramer2020.instDecidableEqRemainderPattern.decEq (x✝ x✝¹ : RemainderPattern) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Gender.Studies.Kramer2020.instDecidableEqRemainderPattern : DecidableEq RemainderPattern

Equations

• Phenomena.Gender.Studies.Kramer2020.instDecidableEqRemainderPattern = Phenomena.Gender.Studies.Kramer2020.instDecidableEqRemainderPattern.decEq

instance Phenomena.Gender.Studies.Kramer2020.instBEqRemainderPattern : BEq RemainderPattern

Equations

• Phenomena.Gender.Studies.Kramer2020.instBEqRemainderPattern = { beq := Phenomena.Gender.Studies.Kramer2020.instBEqRemainderPattern.beq }

def Phenomena.Gender.Studies.Kramer2020.instBEqRemainderPattern.beq : RemainderPattern → RemainderPattern → Bool

Equations

• Phenomena.Gender.Studies.Kramer2020.instBEqRemainderPattern.beq { sameGender := a, genderSource := a_1 } { sameGender := b, genderSource := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Gender.Studies.Kramer2020.instBEqRemainderPattern.beq x✝¹ x✝ = false

def Phenomena.Gender.Studies.Kramer2020.instReprRemainderPattern.repr : RemainderPattern → ℕ → Std.Format

Equations

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

instance Phenomena.Gender.Studies.Kramer2020.instReprRemainderPattern : Repr RemainderPattern

Equations

• Phenomena.Gender.Studies.Kramer2020.instReprRemainderPattern = { reprPrec := Phenomena.Gender.Studies.Kramer2020.instReprRemainderPattern.repr }

def Phenomena.Gender.Studies.Kramer2020.dieri : RemainderPattern

Dieri (Pama-Nyungan): all remainder nouns are masculine (= same gender used for male humans). Same gender, recycled. (@cite{kramer-2020} Table 2)

Equations

• Phenomena.Gender.Studies.Kramer2020.dieri = { sameGender := true, genderSource := Phenomena.Gender.Studies.Kramer2020.RemainderGenderSource.recycled }

def Phenomena.Gender.Studies.Kramer2020.tamil : RemainderPattern

Tamil (Dravidian): remainder nouns go to neuter — a novel gender not used for the male/female semantic core. Same gender, novel. (@cite{kramer-2020} Table 2; Asher 1982)

Equations

• Phenomena.Gender.Studies.Kramer2020.tamil = { sameGender := true, genderSource := Phenomena.Gender.Studies.Kramer2020.RemainderGenderSource.novel }

def Phenomena.Gender.Studies.Kramer2020.spanishRemainder : RemainderPattern

Spanish: remainder nouns are split arbitrarily across masculine and feminine — both recycled genders. Different genders, recycled. (@cite{kramer-2020} Table 1, Table 2; @cite{harris-1991})

Equations

• Phenomena.Gender.Studies.Kramer2020.spanishRemainder = { sameGender := false, genderSource := Phenomena.Gender.Studies.Kramer2020.RemainderGenderSource.recycled }

def Phenomena.Gender.Studies.Kramer2020.akoose : RemainderPattern

Akɔɔse (Niger-Congo: Bantu): remainder nouns spread across at least 7 noun classes — novel genders. Different genders, novel. (@cite{kramer-2020} Table 2; Hedinger 2008)

Equations

• Phenomena.Gender.Studies.Kramer2020.akoose = { sameGender := false, genderSource := Phenomena.Gender.Studies.Kramer2020.RemainderGenderSource.novel }

def Phenomena.Gender.Studies.Kramer2020.blackfoot : RemainderPattern

Blackfoot (Algic: Algonquian): inanimate nouns are assigned either a novel inanimate gender or a recycled animate gender. Different genders, both recycled and novel. (@cite{kramer-2020} Table 2; Frantz 2017)

Equations

• Phenomena.Gender.Studies.Kramer2020.blackfoot = { sameGender := false, genderSource := Phenomena.Gender.Studies.Kramer2020.RemainderGenderSource.both }

theorem Phenomena.Gender.Studies.Kramer2020.table2_all_cells : dieri ≠ tamil ∧ dieri ≠ spanishRemainder ∧ dieri ≠ akoose ∧ dieri ≠ blackfoot ∧ tamil ≠ spanishRemainder ∧ tamil ≠ akoose ∧ tamil ≠ blackfoot ∧ spanishRemainder ≠ akoose ∧ spanishRemainder ≠ blackfoot ∧ akoose ≠ blackfoot

All five attested cells of Table 2 are distinct patterns.

@cite{kramer-2020} §3.2 contrasts two theoretical approaches:

Lexical (@cite{harris-1991}): gender assigned via lexical rules that map semantic features (e.g. [FEMALE]) to grammatical gender features (e.g. [F]). Each noun is listed with its gender feature in the lexicon. Gender is a property of the lexical entry.

Structural (@cite{kramer-2015}): gender is a phi-feature on the categorizing head n. A root combines with an n bearing gender features via syntactic Merge. Gender is a property of the syntactic structure.

Three phenomena differentiate them (§3.3):

1. Phonological gender assignment
2. Hybrid nouns (e.g. Russian vrač)
3. The Semantic Core Generalization

structure Phenomena.Gender.Studies.Kramer2020.LexicalGenderRule : Type

A lexical gender rule: maps a semantic feature to a grammatical gender feature in a specified context. (@cite{harris-1991})

The semanticBasis identifies which semantic property triggers the rule; targetDimension identifies which DM gender dimension is assigned; context describes the conditioning environment.

• semanticBasis : Typology.SemanticBasis

  Semantic trigger (e.g. sex → social gender triggers the rule)

• targetDimension : Morphology.DM.GenderDimension

  DM gender dimension assigned (e.g. fem)

• context : Typology.SemanticBasis

  Context restriction (e.g. humanness)

def Phenomena.Gender.Studies.Kramer2020.instDecidableEqLexicalGenderRule.decEq (x✝ x✝¹ : LexicalGenderRule) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Gender.Studies.Kramer2020.instDecidableEqLexicalGenderRule : DecidableEq LexicalGenderRule

Equations

• Phenomena.Gender.Studies.Kramer2020.instDecidableEqLexicalGenderRule = Phenomena.Gender.Studies.Kramer2020.instDecidableEqLexicalGenderRule.decEq

instance Phenomena.Gender.Studies.Kramer2020.instBEqLexicalGenderRule : BEq LexicalGenderRule

Equations

• Phenomena.Gender.Studies.Kramer2020.instBEqLexicalGenderRule = { beq := Phenomena.Gender.Studies.Kramer2020.instBEqLexicalGenderRule.beq }

def Phenomena.Gender.Studies.Kramer2020.instBEqLexicalGenderRule.beq : LexicalGenderRule → LexicalGenderRule → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Gender.Studies.Kramer2020.instBEqLexicalGenderRule.beq x✝¹ x✝ = false

instance Phenomena.Gender.Studies.Kramer2020.instReprLexicalGenderRule : Repr LexicalGenderRule

Equations

• Phenomena.Gender.Studies.Kramer2020.instReprLexicalGenderRule = { reprPrec := Phenomena.Gender.Studies.Kramer2020.instReprLexicalGenderRule.repr }

def Phenomena.Gender.Studies.Kramer2020.instReprLexicalGenderRule.repr : LexicalGenderRule → ℕ → Std.Format

Equations

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

def Phenomena.Gender.Studies.Kramer2020.harrisHumanGenderRule : LexicalGenderRule

Harris's Human Gender rule for Spanish: [FEMALE] → [F] / __ [HUMAN] The semantic feature [FEMALE] triggers assignment of the grammatical gender feature [F] (feminine) in the context of [HUMAN] nouns. (@cite{harris-1991}; @cite{kramer-2020} ex. 23)

Equations

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

theorem Phenomena.Gender.Studies.Kramer2020.harris_rule_uses_core_bases : harrisHumanGenderRule.semanticBasis.isCore = true ∧ harrisHumanGenderRule.context.isCore = true

Harris's rule connects two core semantic bases: assignment is triggered by social gender/sex and conditioned on humanness.

inductive Phenomena.Gender.Studies.Kramer2020.DiagnosticStatus : Type

The status of a diagnostic phenomenon for a theoretical approach. @cite{kramer-2020} §3.3 argues that some phenomena are genuinely diagnostic while others are inconclusive.

• handled : DiagnosticStatus
• problematic : DiagnosticStatus
• inconclusive : DiagnosticStatus

instance Phenomena.Gender.Studies.Kramer2020.instDecidableEqDiagnosticStatus : DecidableEq DiagnosticStatus

Equations

• Phenomena.Gender.Studies.Kramer2020.instDecidableEqDiagnosticStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Gender.Studies.Kramer2020.instBEqDiagnosticStatus : BEq DiagnosticStatus

Equations

• Phenomena.Gender.Studies.Kramer2020.instBEqDiagnosticStatus = { beq := Phenomena.Gender.Studies.Kramer2020.instBEqDiagnosticStatus.beq }

def Phenomena.Gender.Studies.Kramer2020.instBEqDiagnosticStatus.beq : DiagnosticStatus → DiagnosticStatus → Bool

Equations

• Phenomena.Gender.Studies.Kramer2020.instBEqDiagnosticStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Gender.Studies.Kramer2020.instReprDiagnosticStatus.repr : DiagnosticStatus → ℕ → Std.Format

Equations

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

instance Phenomena.Gender.Studies.Kramer2020.instReprDiagnosticStatus : Repr DiagnosticStatus

Equations

• Phenomena.Gender.Studies.Kramer2020.instReprDiagnosticStatus = { reprPrec := Phenomena.Gender.Studies.Kramer2020.instReprDiagnosticStatus.repr }

structure Phenomena.Gender.Studies.Kramer2020.ApproachCapabilities : Type

A gender assignment approach, characterized by how it handles each of the three diagnostic phenomena from §3.3.

• phonologicalAssignment : DiagnosticStatus

  §3.3.1: phonological gender assignment

• hybridAgreement : DiagnosticStatus

  §3.3.2: hybrid nouns (simultaneous dual agreement)

• predictsSemanticCore : DiagnosticStatus

  §3.3.3: the Semantic Core Generalization

instance Phenomena.Gender.Studies.Kramer2020.instDecidableEqApproachCapabilities : DecidableEq ApproachCapabilities

Equations

• Phenomena.Gender.Studies.Kramer2020.instDecidableEqApproachCapabilities = Phenomena.Gender.Studies.Kramer2020.instDecidableEqApproachCapabilities.decEq

def Phenomena.Gender.Studies.Kramer2020.instDecidableEqApproachCapabilities.decEq (x✝ x✝¹ : ApproachCapabilities) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Gender.Studies.Kramer2020.instBEqApproachCapabilities : BEq ApproachCapabilities

Equations

• Phenomena.Gender.Studies.Kramer2020.instBEqApproachCapabilities = { beq := Phenomena.Gender.Studies.Kramer2020.instBEqApproachCapabilities.beq }

def Phenomena.Gender.Studies.Kramer2020.instBEqApproachCapabilities.beq : ApproachCapabilities → ApproachCapabilities → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Gender.Studies.Kramer2020.instBEqApproachCapabilities.beq x✝¹ x✝ = false

def Phenomena.Gender.Studies.Kramer2020.instReprApproachCapabilities.repr : ApproachCapabilities → ℕ → Std.Format

Equations

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

instance Phenomena.Gender.Studies.Kramer2020.instReprApproachCapabilities : Repr ApproachCapabilities

Equations

• Phenomena.Gender.Studies.Kramer2020.instReprApproachCapabilities = { reprPrec := Phenomena.Gender.Studies.Kramer2020.instReprApproachCapabilities.repr }

def Phenomena.Gender.Studies.Kramer2020.lexicalApproach : ApproachCapabilities

The lexical approach (@cite{harris-1991}).

• Phonological assignment: handled (lexical rules can reference phonology), but @cite{kramer-2020} §3.3.1 argues the phenomenon may not exist — Hausa -ā is morphophonological realization, not assignment.
• Hybrid agreement: problematic — a lexical entry has one gender feature; a single entry cannot be both [M] and [F] (@cite{kramer-2020} §3.3.2)
• Semantic Core: problematic — nothing prevents a language from having only arbitrary gender rules without any semantic connection (@cite{kramer-2020} §3.3.3)

Equations

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

def Phenomena.Gender.Studies.Kramer2020.structuralApproach : ApproachCapabilities

The structural approach (@cite{kramer-2015}).

• Phonological assignment: inconclusive — syntax cannot see phonology, but @cite{kramer-2020} §3.3.1 argues the phenomenon is better analyzed as morphophonological realization of a gender feature on n, so the structural approach is not genuinely challenged.
• Hybrid agreement: handled — a root can combine with different n heads, or a social-gender projection can override morphosyntactic gender (@cite{kramer-2020} §3.3.2)
• Semantic Core: handled — via the Thesis of Radical Interpretability: if a language has gender features, at least some must be interpretable, which forces semantic assignment for at least some nouns (@cite{kramer-2020} §3.3.3)

Equations

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

theorem Phenomena.Gender.Studies.Kramer2020.approaches_differ : lexicalApproach.phonologicalAssignment ≠ structuralApproach.phonologicalAssignment ∧ lexicalApproach.hybridAgreement ≠ structuralApproach.hybridAgreement ∧ lexicalApproach.predictsSemanticCore ≠ structuralApproach.predictsSemanticCore

The approaches differ on all three diagnostic phenomena.

theorem Phenomena.Gender.Studies.Kramer2020.structural_edge : structuralApproach.hybridAgreement = DiagnosticStatus.handled ∧ structuralApproach.predictsSemanticCore = DiagnosticStatus.handled ∧ lexicalApproach.hybridAgreement = DiagnosticStatus.problematic ∧ lexicalApproach.predictsSemanticCore = DiagnosticStatus.problematic

The structural approach handles 2 of the 3 diagnostic phenomena; the lexical approach handles 1. Phonological assignment is inconclusive for both (the structural approach because syntax can't see phonology; the lexical approach because Kramer argues the phenomenon doesn't exist as described). This is the basis for @cite{kramer-2020} §3.4's conclusion that "structural gender assignment has a slight edge."

def Phenomena.Gender.Studies.Kramer2020.radicalInterpretability (features : List Morphology.DM.GenderFeature) : Prop

Radical Interpretability (Brody 1997; Pesetsky & Torrego 2001, 2007): each syntactic feature must receive a semantic interpretation in some syntactic location.

In formal terms: if a feature F has an uninterpretable instantiation in a language, then F also has an interpretable instantiation in that language. The converse need not hold.

Equations

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

theorem Phenomena.Gender.Studies.Kramer2020.amharic_radical_interpretability : radicalInterpretability [{ interp := Morphology.DM.Interpretability.i, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.pos } }, { interp := Morphology.DM.Interpretability.i, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.neg } }, { interp := Morphology.DM.Interpretability.u, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.pos } }]

Amharic's n types satisfy Radical Interpretability: the uninterpretable u[+FEM] is accompanied by interpretable i[+FEM] and i[−FEM] in the same dimension.

theorem Phenomena.Gender.Studies.Kramer2020.spanish_radical_interpretability : radicalInterpretability [{ interp := Morphology.DM.Interpretability.i, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.pos } }, { interp := Morphology.DM.Interpretability.i, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.neg } }, { interp := Morphology.DM.Interpretability.u, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.pos } }]

Spanish's n types (Set 1) satisfy Radical Interpretability: u[+FEM] is accompanied by i[+FEM] in the same dimension.

theorem Phenomena.Gender.Studies.Kramer2020.russian_radical_interpretability : radicalInterpretability [{ interp := Morphology.DM.Interpretability.i, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.pos } }, { interp := Morphology.DM.Interpretability.i, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.neg } }, { interp := Morphology.DM.Interpretability.u, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.pos } }, { interp := Morphology.DM.Interpretability.u, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.neg } }]

Russian's n types (5-n) satisfy Radical Interpretability: both u[+FEM] and u[−FEM] are paired with i[+FEM] and i[−FEM].

theorem Phenomena.Gender.Studies.Kramer2020.no_purely_arbitrary_under_ri (features : List Morphology.DM.GenderFeature) (hRI : radicalInterpretability features) (hNonempty : ∃ gf ∈ features, True) (hAllU : ∀ gf ∈ features, gf.interp = Morphology.DM.Interpretability.u) : False

The Semantic Core follows from Radical Interpretability + structural assignment: if a language has any gender feature (even uninterpretable), it must have an interpretable one in the same dimension, which forces at least some nouns to be assigned gender semantically.

Contrapositively: a language with only uninterpretable gender (pure arbitrary assignment, no semantic core) violates Radical Interpretability.

theorem Phenomena.Gender.Studies.Kramer2020.ri_implies_interpretable_exists (features : List Morphology.DM.GenderFeature) (hRI : radicalInterpretability features) (hNonempty : ∃ gf ∈ features, True) : ∃ gf ∈ features, gf.interp = Morphology.DM.Interpretability.i

Positive direction of the RI → Semantic Core derivation: if a language has gender features and satisfies Radical Interpretability, then it has at least one interpretable gender feature (which, being interpretable, forces semantic gender assignment for at least some nouns). (@cite{kramer-2020} §3.3.3)

structure Phenomena.Gender.Studies.Kramer2020.SameRootNominal : Type

Same-root nominals: nouns that can be assigned different grammatical genders depending on the social gender of their referent. (@cite{kramer-2020} §2.2.3; @cite{kramer-2015}; @cite{corbett-1991})

In the structural approach, the root itself is ungendered; gender depends on which n head it merges with. Same-root nominals combine with alternative n heads depending on the referent.

Examples: Amharic hakim 'doctor' (ex. 13), Spanish estudiante 'student', Greek odigós 'driver'.

• form : String

  The noun form

• language : String

  Language

• possibleNHeads : List Morphology.DM.CatHead

  Possible gender assignments (> 1 for same-root nominals)

instance Phenomena.Gender.Studies.Kramer2020.instReprSameRootNominal : Repr SameRootNominal

Equations

• Phenomena.Gender.Studies.Kramer2020.instReprSameRootNominal = { reprPrec := Phenomena.Gender.Studies.Kramer2020.instReprSameRootNominal.repr }

def Phenomena.Gender.Studies.Kramer2020.instReprSameRootNominal.repr : SameRootNominal → ℕ → Std.Format

Equations

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

def Phenomena.Gender.Studies.Kramer2020.SameRootNominal.isSameRoot (n : SameRootNominal) : Bool

Whether this is a genuine same-root nominal (multiple n options).

Equations

• n.isSameRoot = decide (n.possibleNHeads.length > 1)

def Phenomena.Gender.Studies.Kramer2020.amharicHakim : SameRootNominal

Amharic hakim 'doctor': combines with either i[+FEM] or i[−FEM] depending on the referent. (@cite{kramer-2020} ex. 13)

Equations

• Phenomena.Gender.Studies.Kramer2020.amharicHakim = { form := "hakim", language := "Amharic", possibleNHeads := [Morphology.DM.CatHead.n_iFem, Morphology.DM.CatHead.n_iMasc] }

theorem Phenomena.Gender.Studies.Kramer2020.hakim_is_same_root : amharicHakim.isSameRoot = true

theorem Phenomena.Gender.Studies.Kramer2020.same_root_two_n_heads : amharicHakim.possibleNHeads.length = 2

Same-root nominals pose a challenge for lexical approaches: a single lexical entry cannot carry both [M] and [F]. The structural approach handles them by allowing the same root to merge with different n heads.

theorem Phenomena.Gender.Studies.Kramer2020.hakim_distinct_genders : Morphology.DM.CatHead.n_iFem ≠ Morphology.DM.CatHead.n_iMasc

The two n heads for hakim are distinct gender features.

Hybrid nouns are distinct from same-root nominals. Where same-root nominals alternate gender depending on the referent (Amharic hakim is EITHER masculine OR feminine), hybrid nouns trigger BOTH genders SIMULTANEOUSLY on different agreement targets in the same sentence.

@cite{kramer-2020} ex. 16/27: Russian vrač 'doctor' očen' xoroš-aja glavn-yj vrač very good-F head-M doctor 'a very good head doctor'

Here xoroš-aja shows feminine agreement and glavn-yj shows masculine agreement with the SAME noun vrač in the SAME clause.

@cite{kramer-2020} §3.3.2 argues this is problematic for lexical approaches (a lexical entry has one gender feature) but handled by structural approaches (a social-gender projection can coexist with morphosyntactic gender on n).

structure Phenomena.Gender.Studies.Kramer2020.HybridNoun : Type

A hybrid noun: a single lexical item that triggers different genders on different agreement targets simultaneously. (@cite{kramer-2020} §2.2.3, §3.3.2; @cite{corbett-1991})

• form : String

  The noun form

• language : String

  Language

• morphGender : Morphology.DM.GenderVal

  Morphosyntactic gender (from n head)

• semGender : Morphology.DM.GenderVal

  Semantic gender (from social-gender projection, triggered by referent)

• distinct : self.morphGender ≠ self.semGender

  The two genders must differ for hybrid agreement to arise.

def Phenomena.Gender.Studies.Kramer2020.instReprHybridNoun.repr : HybridNoun → ℕ → Std.Format

Equations

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

instance Phenomena.Gender.Studies.Kramer2020.instReprHybridNoun : Repr HybridNoun

Equations

• Phenomena.Gender.Studies.Kramer2020.instReprHybridNoun = { reprPrec := Phenomena.Gender.Studies.Kramer2020.instReprHybridNoun.repr }

def Phenomena.Gender.Studies.Kramer2020.russianVrac : HybridNoun

Russian vrač 'doctor': morphologically masculine (from n), but can trigger feminine agreement when referring to a female doctor. (@cite{kramer-2020} ex. 15-16/27; @cite{corbett-1991})

Equations

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

theorem Phenomena.Gender.Studies.Kramer2020.hybrid_nouns_favor_structural : structuralApproach.hybridAgreement = DiagnosticStatus.handled ∧ lexicalApproach.hybridAgreement = DiagnosticStatus.problematic

Hybrid nouns are problematic for lexical approaches: a lexical entry can bear only one gender feature, but hybrid nouns need two genders simultaneously. The structural approach handles this via separate projections for morphosyntactic and social gender. (@cite{kramer-2020} §3.3.2)

structure Phenomena.Gender.Studies.Kramer2020.NInventory : Type

An inventory of n heads for a language, with the number of surface genders that result from VI (@cite{kramer-2015} Chs 5-7).

The key insight: surface gender count is determined by VI rules, not directly by the n inventory. Two languages can have the SAME set of n heads but different numbers of surface genders (e.g., Dieri 2 vs Mangarayi 3).

• language : String
• nHeads : List Morphology.DM.CatHead
• surfaceGenders : ℕ

instance Phenomena.Gender.Studies.Kramer2020.instReprNInventory : Repr NInventory

Equations

• Phenomena.Gender.Studies.Kramer2020.instReprNInventory = { reprPrec := Phenomena.Gender.Studies.Kramer2020.instReprNInventory.repr }

def Phenomena.Gender.Studies.Kramer2020.instReprNInventory.repr : NInventory → ℕ → Std.Format

Equations

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

def Phenomena.Gender.Studies.Kramer2020.NInventory.hasArbitraryGender (inv : NInventory) : Bool

Does this inventory include any arbitrary (uninterpretable) gender?

Equations

• inv.hasArbitraryGender = inv.nHeads.any fun (ch : Morphology.DM.CatHead) => match ch.phi.gender with | some gf => gf.isArbitrary | none => false

def Phenomena.Gender.Studies.Kramer2020.NInventory.purelySemanticGender (inv : NInventory) : Bool

Is this a purely semantic gender system (no u-features)?

Equations

• inv.purelySemanticGender = !inv.hasArbitraryGender

def Phenomena.Gender.Studies.Kramer2020.dieriNs : NInventory

Equations

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

def Phenomena.Gender.Studies.Kramer2020.mangarayiNs : NInventory

Equations

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

def Phenomena.Gender.Studies.Kramer2020.amharicNs : NInventory

Equations

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

def Phenomena.Gender.Studies.Kramer2020.spanishNs : NInventory

Equations

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

def Phenomena.Gender.Studies.Kramer2020.maaNs : NInventory

Equations

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

def Phenomena.Gender.Studies.Kramer2020.lealaoNs : NInventory

Equations

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

def Phenomena.Gender.Studies.Kramer2020.ojibweNs : NInventory

Equations

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

def Phenomena.Gender.Studies.Kramer2020.lavukaleveNs : NInventory

Equations

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

theorem Phenomena.Gender.Studies.Kramer2020.same_ns_different_genders : dieriNs.nHeads = mangarayiNs.nHeads ∧ dieriNs.surfaceGenders ≠ mangarayiNs.surfaceGenders

Same n inventory, different surface genders: Dieri (2) vs Mangarayi (3). This demonstrates that surface gender count depends on VI, not the inventory itself.

theorem Phenomena.Gender.Studies.Kramer2020.set1_shared : amharicNs.nHeads = spanishNs.nHeads

Set 1 languages share the same n inventory (@cite{kramer-2015} Ch 6).

theorem Phenomena.Gender.Studies.Kramer2020.dieri_purely_semantic : dieriNs.purelySemanticGender = true

3-n languages have purely semantic gender (no u-features). (@cite{kramer-2015} Ch 5)

theorem Phenomena.Gender.Studies.Kramer2020.lealao_purely_semantic : lealaoNs.purelySemanticGender = true

Lealao Chinantec is also purely semantic (animacy-based, Ch 5).

theorem Phenomena.Gender.Studies.Kramer2020.ojibwe_has_uAnim : ojibweNs.hasArbitraryGender = true

Ojibwe is a 4-n animacy language with arbitrary animate assignment (u[+ANIM]). (@cite{kramer-2015} Ch 6, §6.4)

theorem Phenomena.Gender.Studies.Kramer2020.ojibwe_four_ns : ojibweNs.nHeads.length = 4

Ojibwe has the same structure as Set 1 sex-based languages (Amharic, Spanish) but in the animacy dimension: i[+ANIM], i[−ANIM], plain n, u[+ANIM].

theorem Phenomena.Gender.Studies.Kramer2020.lavukaleve_maximal : lavukaleveNs.nHeads.length = 5

Lavukaleve is maximal: 5 n heads (both u[+FEM] and u[−FEM]).

theorem Phenomena.Gender.Studies.Kramer2020.more_ns_same_genders : amharicNs.nHeads.length > dieriNs.nHeads.length ∧ amharicNs.surfaceGenders = dieriNs.surfaceGenders

More n heads does not entail more surface genders: Amharic has 4 ns but only 2 surface genders.

theorem Phenomena.Gender.Studies.Kramer2020.hombre_natural_masculine : Fragments.Spanish.Gender.hombre.nHead.phi.gender = some { interp := Morphology.DM.Interpretability.i, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.neg } }

Derive from fragment: hombre 'man' has natural masculine gender (i[−FEM]).

theorem Phenomena.Gender.Studies.Kramer2020.mujer_natural_feminine : Fragments.Spanish.Gender.mujer.nHead.phi.gender = some { interp := Morphology.DM.Interpretability.i, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.pos } }

Derive from fragment: mujer 'woman' has natural feminine gender (i[+FEM]).

theorem Phenomena.Gender.Studies.Kramer2020.mesa_arbitrary_feminine : Fragments.Spanish.Gender.mesa.nHead.phi.gender = some { interp := Morphology.DM.Interpretability.u, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.pos } }

Derive from fragment: mesa 'table' has arbitrary feminine gender (u[+FEM]).

theorem Phenomena.Gender.Studies.Kramer2020.libro_default_masculine : Fragments.Spanish.Gender.libro.nHead.phi.gender = none

Derive from fragment: libro 'book' has default masculine (plain n).

def Phenomena.Gender.Studies.Kramer2020.spanishSameRoot (e : Fragments.Spanish.Gender.SameRootEntry) : SameRootNominal

Bridge: convert a Spanish SameRootEntry to the cross-linguistic SameRootNominal type.

Equations

• Phenomena.Gender.Studies.Kramer2020.spanishSameRoot e = { form := e.form, language := "Spanish", possibleNHeads := e.possibleNHeads }

theorem Phenomena.Gender.Studies.Kramer2020.soldado_is_same_root : Fragments.Spanish.Gender.soldado.mascHead ≠ Fragments.Spanish.Gender.soldado.femHead

Spanish soldado 'soldier' as a same-root nominal: the root √SOLDAD can combine with i[+FEM] or i[−FEM].

theorem Phenomena.Gender.Studies.Kramer2020.spanish_same_roots_genuine : (spanishSameRoot Fragments.Spanish.Gender.soldado).isSameRoot = true ∧ (spanishSameRoot Fragments.Spanish.Gender.estudiante).isSameRoot = true ∧ (spanishSameRoot Fragments.Spanish.Gender.artista).isSameRoot = true

Spanish same-root nominals are genuine same-root nominals (they have two possible n heads).

theorem Phenomena.Gender.Studies.Kramer2020.spanish_four_n_types : spanishNs.nHeads.length = 4

Spanish has the full Set 1 inventory: 4 n types.

theorem Phenomena.Gender.Studies.Kramer2020.fragment_covers_inventory : (Fragments.Spanish.Gender.allNouns.any fun (x : Fragments.Spanish.Gender.SpanishNoun) => x.nHead == Morphology.DM.CatHead.n_iFem) = true ∧ (Fragments.Spanish.Gender.allNouns.any fun (x : Fragments.Spanish.Gender.SpanishNoun) => x.nHead == Morphology.DM.CatHead.n_iMasc) = true ∧ (Fragments.Spanish.Gender.allNouns.any fun (x : Fragments.Spanish.Gender.SpanishNoun) => x.nHead == Morphology.DM.CatHead.n_uFem) = true ∧ (Fragments.Spanish.Gender.allNouns.any fun (x : Fragments.Spanish.Gender.SpanishNoun) => x.nHead == Morphology.DM.CatHead.n_plain) = true

The fragment inventory covers all four n-types from the NInventory.

@cite{kramer-2015} §3.4 identifies four classes of roots, distinguished by which n heads they are licensed to combine with:

1. Female-denoting roots (√WOMAN, √QUEEN): semantic licensing (List 3) requires n i[+FEM]. The Encyclopedia entry only provides a denotation in the context of an n head bearing [+FEM].
2. Male-denoting roots (√MAN, √KING): semantic licensing requires n i[−FEM].
3. Arbitrarily feminine roots (√TABLE, √CHAIR): PF licensing (List 2) requires n u[+FEM]. A VI rule specifies the exponent in the context of [+FEM] on n.
4. Default roots (√BOOK, √CAR): no licensing requirement. Combine with plain n (the elsewhere case).

This classification generates the licensing tables found in Tables 3.1 (Amharic, 3 ns) and 6.2 (Spanish, 4 ns).

inductive Phenomena.Gender.Studies.Kramer2020.RootClass : Type

Root classes from @cite{kramer-2015} §3.4, parameterized by which n head the root is licensed to combine with.

The first four classes are from Tables 3.1/6.2 (3-n and Set 1 4-n systems). arbitraryMasc extends the typology to 5-n systems (Russian, Lavukaleve) and Set 2 4-n systems (Maa, Wari'), where u[−FEM] is also attested.

• femaleReferent : RootClass
• maleReferent : RootClass
• arbitraryFem : RootClass
• arbitraryMasc : RootClass
• default : RootClass

instance Phenomena.Gender.Studies.Kramer2020.instDecidableEqRootClass : DecidableEq RootClass

Equations

• Phenomena.Gender.Studies.Kramer2020.instDecidableEqRootClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Gender.Studies.Kramer2020.instBEqRootClass.beq : RootClass → RootClass → Bool

Equations

• Phenomena.Gender.Studies.Kramer2020.instBEqRootClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Gender.Studies.Kramer2020.instBEqRootClass : BEq RootClass

Equations

• Phenomena.Gender.Studies.Kramer2020.instBEqRootClass = { beq := Phenomena.Gender.Studies.Kramer2020.instBEqRootClass.beq }

instance Phenomena.Gender.Studies.Kramer2020.instReprRootClass : Repr RootClass

Equations

• Phenomena.Gender.Studies.Kramer2020.instReprRootClass = { reprPrec := Phenomena.Gender.Studies.Kramer2020.instReprRootClass.repr }

def Phenomena.Gender.Studies.Kramer2020.instReprRootClass.repr : RootClass → ℕ → Std.Format

Equations

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

def Phenomena.Gender.Studies.Kramer2020.RootClass.licensedNHead : RootClass → Morphology.DM.CatHead

The n head each root class is licensed to combine with.

Equations

• Phenomena.Gender.Studies.Kramer2020.RootClass.femaleReferent.licensedNHead = Morphology.DM.CatHead.n_iFem
• Phenomena.Gender.Studies.Kramer2020.RootClass.maleReferent.licensedNHead = Morphology.DM.CatHead.n_iMasc
• Phenomena.Gender.Studies.Kramer2020.RootClass.arbitraryFem.licensedNHead = Morphology.DM.CatHead.n_uFem
• Phenomena.Gender.Studies.Kramer2020.RootClass.arbitraryMasc.licensedNHead = Morphology.DM.CatHead.n_uNegFem
• Phenomena.Gender.Studies.Kramer2020.RootClass.default.licensedNHead = Morphology.DM.CatHead.n_plain

def Phenomena.Gender.Studies.Kramer2020.RootClass.licensing : RootClass → Morphology.DM.LicensingType

The licensing type for each root class.

Equations

• Phenomena.Gender.Studies.Kramer2020.RootClass.femaleReferent.licensing = Morphology.DM.LicensingType.semantic
• Phenomena.Gender.Studies.Kramer2020.RootClass.maleReferent.licensing = Morphology.DM.LicensingType.semantic
• Phenomena.Gender.Studies.Kramer2020.RootClass.arbitraryFem.licensing = Morphology.DM.LicensingType.arbitrary
• Phenomena.Gender.Studies.Kramer2020.RootClass.arbitraryMasc.licensing = Morphology.DM.LicensingType.arbitrary
• Phenomena.Gender.Studies.Kramer2020.RootClass.default.licensing = Morphology.DM.LicensingType.arbitrary

theorem Phenomena.Gender.Studies.Kramer2020.natural_roots_semantic : RootClass.femaleReferent.licensing = Morphology.DM.LicensingType.semantic ∧ RootClass.maleReferent.licensing = Morphology.DM.LicensingType.semantic

Natural-gender roots are semantically licensed.

theorem Phenomena.Gender.Studies.Kramer2020.arbitrary_roots_pf : RootClass.arbitraryFem.licensing = Morphology.DM.LicensingType.arbitrary ∧ RootClass.arbitraryMasc.licensing = Morphology.DM.LicensingType.arbitrary ∧ RootClass.default.licensing = Morphology.DM.LicensingType.arbitrary

Arbitrary and default roots are PF-licensed.

theorem Phenomena.Gender.Studies.Kramer2020.root_classes_distinct_n : RootClass.femaleReferent.licensedNHead ≠ RootClass.maleReferent.licensedNHead ∧ RootClass.femaleReferent.licensedNHead ≠ RootClass.arbitraryFem.licensedNHead ∧ RootClass.femaleReferent.licensedNHead ≠ RootClass.arbitraryMasc.licensedNHead ∧ RootClass.femaleReferent.licensedNHead ≠ RootClass.default.licensedNHead ∧ RootClass.maleReferent.licensedNHead ≠ RootClass.arbitraryFem.licensedNHead ∧ RootClass.maleReferent.licensedNHead ≠ RootClass.arbitraryMasc.licensedNHead ∧ RootClass.maleReferent.licensedNHead ≠ RootClass.default.licensedNHead ∧ RootClass.arbitraryFem.licensedNHead ≠ RootClass.arbitraryMasc.licensedNHead ∧ RootClass.arbitraryFem.licensedNHead ≠ RootClass.default.licensedNHead ∧ RootClass.arbitraryMasc.licensedNHead ≠ RootClass.default.licensedNHead

Each root class maps to a distinct n head.

theorem Phenomena.Gender.Studies.Kramer2020.spanish_licensing_mujer : Fragments.Spanish.Gender.mujer.nHead = RootClass.femaleReferent.licensedNHead

Verify that the Spanish fragment's nouns match their expected root classes. Each noun's nHead should equal the licensed n head for its root class.

theorem Phenomena.Gender.Studies.Kramer2020.spanish_licensing_hombre : Fragments.Spanish.Gender.hombre.nHead = RootClass.maleReferent.licensedNHead

theorem Phenomena.Gender.Studies.Kramer2020.spanish_licensing_mesa : Fragments.Spanish.Gender.mesa.nHead = RootClass.arbitraryFem.licensedNHead

theorem Phenomena.Gender.Studies.Kramer2020.spanish_licensing_libro : Fragments.Spanish.Gender.libro.nHead = RootClass.default.licensedNHead

theorem Phenomena.Gender.Studies.Kramer2020.licensing_bridge_femaleReferent : (Morphology.DM.CatHead.n_iFem.phi.gender.get ⋯).licensingType = RootClass.femaleReferent.licensing

Bridge: the licensing type of a root class agrees with the licensing type derived from its n head's gender feature. For gendered root classes, the GenderFeature.licensingType (defined in Categorizer.lean) produces the same result as RootClass.licensing.

theorem Phenomena.Gender.Studies.Kramer2020.licensing_bridge_maleReferent : (Morphology.DM.CatHead.n_iMasc.phi.gender.get ⋯).licensingType = RootClass.maleReferent.licensing

theorem Phenomena.Gender.Studies.Kramer2020.licensing_bridge_arbitraryFem : (Morphology.DM.CatHead.n_uFem.phi.gender.get ⋯).licensingType = RootClass.arbitraryFem.licensing

theorem Phenomena.Gender.Studies.Kramer2020.licensing_bridge_arbitraryMasc : (Morphology.DM.CatHead.n_uNegFem.phi.gender.get ⋯).licensingType = RootClass.arbitraryMasc.licensing

theorem Phenomena.Gender.Studies.Kramer2020.russian_licensing_otec : Fragments.Russian.Gender.otec.nHead = RootClass.maleReferent.licensedNHead

Russian fragment nouns match their root classes.

theorem Phenomena.Gender.Studies.Kramer2020.russian_licensing_mat' : Fragments.Russian.Gender.mat'.nHead = RootClass.femaleReferent.licensedNHead

theorem Phenomena.Gender.Studies.Kramer2020.russian_licensing_zakon : Fragments.Russian.Gender.zakon.nHead = RootClass.arbitraryMasc.licensedNHead

theorem Phenomena.Gender.Studies.Kramer2020.russian_licensing_škola : Fragments.Russian.Gender.škola.nHead = RootClass.arbitraryFem.licensedNHead

theorem Phenomena.Gender.Studies.Kramer2020.russian_licensing_vino : Fragments.Russian.Gender.vino.nHead = RootClass.default.licensedNHead

theorem Phenomena.Gender.Studies.Kramer2020.persona_exception : Fragments.Spanish.Gender.persona.nHead = RootClass.arbitraryFem.licensedNHead ∧ Fragments.Spanish.Gender.persona.gloss = "person"

persona is human-denoting but has u[+FEM] (arbitrary feminine), not i[+FEM] (natural feminine). This is the key exception to the pattern that human-denoting nouns get interpretable gender features. (@cite{kramer-2020} §3.2, p. 59; @cite{kramer-2015} §6.2)

In root-class terms: persona's root is licensed as arbitraryFem despite denoting humans — its root is only licensed to combine with n u[+FEM], never n i[+FEM] or n i[−FEM].

The NInventory (from the DM analysis of n heads, @cite{kramer-2015}) and the GenderProfile (from WALS typology, @cite{corbett-2013}) describe the same languages from different theoretical perspectives. The key bridge: the NInventory.surfaceGenders count should match GenderProfile.rawGenderCount for the same language.

theorem Phenomena.Gender.Studies.Kramer2020.spanish_ninventory_matches_profile : spanishNs.surfaceGenders = Typology.spanish.rawGenderCount

Spanish: the DM n-inventory predicts the same number of surface genders as the WALS typological profile.

theorem Phenomena.Gender.Studies.Kramer2020.spanish_surface_genders_consistent : Typology.GenderCount.two.contains spanishNs.surfaceGenders = true

Spanish surface genders are consistent with the WALS gender count bin.

theorem Phenomena.Gender.Studies.Kramer2020.spanish_structural_vs_surface : spanishNs.nHeads.length > spanishNs.surfaceGenders

For Spanish, the n-inventory has 4 structural heads mapping to 2 surface genders — a many-to-one mapping mediated by VI (@cite{kramer-2015} Ch 6). This is the central insight: structural richness (4 n types) does not imply surface richness (only 2 genders).

theorem Phenomena.Gender.Studies.Kramer2020.spanish_assignment_consistent : spanishNs.hasArbitraryGender = true ∧ Typology.spanish.assignment = Typology.AssignmentSystem.semanticAndFormal

NInventory ↔ AssignmentSystem bridge: having arbitrary (u) features in the n-inventory corresponds to semanticAndFormal assignment in the WALS typology. 3-n languages with no u-features are semanticOnly. (@cite{kramer-2020} §2.3; @cite{corbett-2013} Ch 32)

In Set 1 languages (Spanish, Amharic), masculine is the DEFAULT gender: nouns with plain n (no gender feature) surface as masculine. The derivation:

1. The root combines with plain n (no gender feature on n).
2. At PF, Vocabulary Insertion looks for a matching exponent.
3. The [+FEM] exponent requires [+FEM] on n — it does NOT match.
4. The elsewhere/default exponent (masculine) is inserted.

In Set 2 languages (Maa, Wari'), the same logic yields feminine as default:

1. The root combines with plain n (no gender feature on n).
2. The [−FEM] exponent requires [−FEM] on n — it does NOT match.
3. The elsewhere/default exponent (feminine) is inserted.

The polarity of the u-feature determines which gender is arbitrary vs default.

inductive Phenomena.Gender.Studies.Kramer2020.SurfaceGender : Type

Derive the surface gender for Set 1 Spanish: plain n has no [+FEM], so the [+FEM] VI rule does not match, yielding default masculine.

• masculine : SurfaceGender
• feminine : SurfaceGender

instance Phenomena.Gender.Studies.Kramer2020.instDecidableEqSurfaceGender : DecidableEq SurfaceGender

Equations

• Phenomena.Gender.Studies.Kramer2020.instDecidableEqSurfaceGender x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Gender.Studies.Kramer2020.instBEqSurfaceGender : BEq SurfaceGender

Equations

• Phenomena.Gender.Studies.Kramer2020.instBEqSurfaceGender = { beq := Phenomena.Gender.Studies.Kramer2020.instBEqSurfaceGender.beq }

def Phenomena.Gender.Studies.Kramer2020.instBEqSurfaceGender.beq : SurfaceGender → SurfaceGender → Bool

Equations

• Phenomena.Gender.Studies.Kramer2020.instBEqSurfaceGender.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Gender.Studies.Kramer2020.instReprSurfaceGender.repr : SurfaceGender → ℕ → Std.Format

Equations

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

instance Phenomena.Gender.Studies.Kramer2020.instReprSurfaceGender : Repr SurfaceGender

Equations

• Phenomena.Gender.Studies.Kramer2020.instReprSurfaceGender = { reprPrec := Phenomena.Gender.Studies.Kramer2020.instReprSurfaceGender.repr }

def Phenomena.Gender.Studies.Kramer2020.set1SurfaceGender (ch : Morphology.DM.CatHead) : SurfaceGender

Set 1 default gender derivation: if n has no [+FEM] feature, the default VI rule inserts masculine. If n has [+FEM] (interpretable or uninterpretable), VI inserts feminine. (@cite{kramer-2015} §6.2; @cite{kramer-2020} §3)

Equations

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

def Phenomena.Gender.Studies.Kramer2020.set2SurfaceGender (ch : Morphology.DM.CatHead) : SurfaceGender

Set 2 default gender derivation: if n has no [−FEM] feature, the default VI rule inserts feminine. If n has [−FEM] (interpretable or uninterpretable), VI inserts masculine. (@cite{kramer-2015} §6.3)

Equations

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

theorem Phenomena.Gender.Studies.Kramer2020.set1_plain_n_masculine : set1SurfaceGender Morphology.DM.CatHead.n_plain = SurfaceGender.masculine

Plain n → masculine (the default).

theorem Phenomena.Gender.Studies.Kramer2020.set1_iFem_feminine : set1SurfaceGender Morphology.DM.CatHead.n_iFem = SurfaceGender.feminine

i[+FEM] → feminine (natural female).

theorem Phenomena.Gender.Studies.Kramer2020.set1_iMasc_masculine : set1SurfaceGender Morphology.DM.CatHead.n_iMasc = SurfaceGender.masculine

i[−FEM] → masculine (natural male).

theorem Phenomena.Gender.Studies.Kramer2020.set1_uFem_feminine : set1SurfaceGender Morphology.DM.CatHead.n_uFem = SurfaceGender.feminine

u[+FEM] → feminine (arbitrary feminine).

theorem Phenomena.Gender.Studies.Kramer2020.set2_plain_n_feminine : set2SurfaceGender Morphology.DM.CatHead.n_plain = SurfaceGender.feminine

Plain n → feminine (the default in Set 2).

theorem Phenomena.Gender.Studies.Kramer2020.set2_uNegFem_masculine : set2SurfaceGender Morphology.DM.CatHead.n_uNegFem = SurfaceGender.masculine

u[−FEM] → masculine (arbitrary masculine in Set 2).

theorem Phenomena.Gender.Studies.Kramer2020.set2_iMasc_masculine : set2SurfaceGender Morphology.DM.CatHead.n_iMasc = SurfaceGender.masculine

i[−FEM] → masculine (natural male, same in both sets).

theorem Phenomena.Gender.Studies.Kramer2020.set2_iFem_feminine : set2SurfaceGender Morphology.DM.CatHead.n_iFem = SurfaceGender.feminine

i[+FEM] → feminine (natural female, same in both sets).

theorem Phenomena.Gender.Studies.Kramer2020.set1_set2_default_contrast : set1SurfaceGender Morphology.DM.CatHead.n_plain ≠ set2SurfaceGender Morphology.DM.CatHead.n_plain

The Set 1 ↔ Set 2 contrast: plain n defaults to OPPOSITE genders.

theorem Phenomena.Gender.Studies.Kramer2020.spanish_derivation_chain : set1SurfaceGender Fragments.Spanish.Gender.mujer.nHead = SurfaceGender.feminine ∧ set1SurfaceGender Fragments.Spanish.Gender.hombre.nHead = SurfaceGender.masculine ∧ set1SurfaceGender Fragments.Spanish.Gender.mesa.nHead = SurfaceGender.feminine ∧ set1SurfaceGender Fragments.Spanish.Gender.libro.nHead = SurfaceGender.masculine ∧ set1SurfaceGender Fragments.Spanish.Gender.persona.nHead = SurfaceGender.feminine ∧ set1SurfaceGender Fragments.Spanish.Gender.ángel.nHead = SurfaceGender.masculine

Verify the full derivation chain for Spanish fragment nouns: the surface gender computed from each noun's CatHead matches the expected gender assignment.

theorem Phenomena.Gender.Studies.Kramer2020.fixed_gender_from_n_head : set1SurfaceGender Fragments.Spanish.Gender.persona.nHead = SurfaceGender.feminine ∧ set1SurfaceGender Fragments.Spanish.Gender.ángel.nHead = SurfaceGender.masculine

Fixed-gender nouns: persona surfaces as feminine despite denoting persons of any sex; ángel surfaces as masculine. The derivation chain correctly predicts this from their n heads.

Russian is a 5-n language with 3 surface genders — the same inventory as Lavukaleve, supporting @cite{kramer-2015}'s prediction that n-inventory size and surface gender count are independent (mediated by VI).

def Phenomena.Gender.Studies.Kramer2020.russianNs : NInventory

Equations

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

theorem Phenomena.Gender.Studies.Kramer2020.russian_lavukaleve_same_ns : russianNs.nHeads = lavukaleveNs.nHeads

Russian and Lavukaleve share the same n-inventory (5 heads).

theorem Phenomena.Gender.Studies.Kramer2020.russian_lavukaleve_same_surface : russianNs.surfaceGenders = lavukaleveNs.surfaceGenders

Both have 3 surface genders despite the 5-n inventory.

theorem Phenomena.Gender.Studies.Kramer2020.russian_structural_vs_surface : russianNs.nHeads.length > russianNs.surfaceGenders

Russian has 5 structural heads mapping to 3 surface genders.

theorem Phenomena.Gender.Studies.Kramer2020.russian_ninventory_matches_profile : russianNs.surfaceGenders = Typology.russian.rawGenderCount

Russian: the DM n-inventory predicts the same number of surface genders as the WALS typological profile.

theorem Phenomena.Gender.Studies.Kramer2020.russian_surface_genders_consistent : Typology.GenderCount.three.contains russianNs.surfaceGenders = true

Russian n-inventory matches the WALS gender count bin.

theorem Phenomena.Gender.Studies.Kramer2020.russian_assignment_consistent : russianNs.hasArbitraryGender = true ∧ Typology.russian.assignment = Typology.AssignmentSystem.semanticAndFormal

Russian has u-features → semanticAndFormal assignment, consistent with the WALS profile.

theorem Phenomena.Gender.Studies.Kramer2020.vrač_morph_masculine : Fragments.Russian.Gender.vrač.nHead.phi.gender = some { interp := Morphology.DM.Interpretability.u, val := { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.neg } }

Fragment-derived: vrač has morphological masculine (u[−FEM]).

theorem Phenomena.Gender.Studies.Kramer2020.vrač_matches_hybrid : russianVrac.morphGender = { dim := Morphology.DM.GenderDimension.fem, pol := Morphology.DM.Polarity.neg } ∧ Fragments.Russian.Gender.vrač.nHead.phi.gender = some { interp := Morphology.DM.Interpretability.u, val := russianVrac.morphGender }

vrač is a hybrid noun: its morphological gender (u[−FEM] = masculine) differs from the semantic gender triggered by a female referent ([+FEM]). This matches the russianVrac definition from §7.

theorem Phenomena.Gender.Studies.Kramer2020.zakon_fragment_masculine : Fragments.Russian.Gender.surfaceGender Fragments.Russian.Gender.zakon.nHead = Fragments.Russian.Gender.SurfaceGender.masculine

Fragment-derived: zakon (Class I) surfaces as masculine.

theorem Phenomena.Gender.Studies.Kramer2020.vino_fragment_neuter : Fragments.Russian.Gender.surfaceGender Fragments.Russian.Gender.vino.nHead = Fragments.Russian.Gender.SurfaceGender.neuter

Fragment-derived: vino (default) surfaces as neuter.

theorem Phenomena.Gender.Studies.Kramer2020.russian_fragment_covers_inventory : (Fragments.Russian.Gender.allNouns.any fun (x : Fragments.Russian.Gender.RussianNoun) => x.nHead == Morphology.DM.CatHead.n_iFem) = true ∧ (Fragments.Russian.Gender.allNouns.any fun (x : Fragments.Russian.Gender.RussianNoun) => x.nHead == Morphology.DM.CatHead.n_iMasc) = true ∧ (Fragments.Russian.Gender.allNouns.any fun (x : Fragments.Russian.Gender.RussianNoun) => x.nHead == Morphology.DM.CatHead.n_uFem) = true ∧ (Fragments.Russian.Gender.allNouns.any fun (x : Fragments.Russian.Gender.RussianNoun) => x.nHead == Morphology.DM.CatHead.n_uNegFem) = true ∧ (Fragments.Russian.Gender.allNouns.any fun (x : Fragments.Russian.Gender.RussianNoun) => x.nHead == Morphology.DM.CatHead.n_plain) = true

Fragment-derived: Russian has all 5 n-types in its lexicon.

The NInventory.surfaceGenders field is currently stipulated. Here we derive the surface gender count from VI rules applied to each n-head, verifying that the computed count matches the stipulated count.

The key VI patterns from @cite{kramer-2015}:

• Set 1 (Spanish, Amharic): [+FEM] → feminine, else → masculine (2)
• Set 2 (Maa): [−FEM] → masculine, else → feminine (2)
• 3-gender (Russian, Mangarayi, Lavukaleve): [+FEM] → fem, [−FEM] → masc, no feature → neuter (3)

def Phenomena.Gender.Studies.Kramer2020.NInventory.computeSurfaceGenders (inv : NInventory) (viMap : Morphology.DM.CatHead → ℕ) : ℕ

A VI gender-class assignment: maps each n-head to a surface gender class (encoded as Nat). Two n-heads yielding the same Nat surface as the same gender.

Equations

• inv.computeSurfaceGenders viMap = (List.map viMap inv.nHeads).eraseDups.length

def Phenomena.Gender.Studies.Kramer2020.viSet1 (ch : Morphology.DM.CatHead) : ℕ

Set 1 VI: [+FEM] → 0 (feminine), everything else → 1 (masculine).

Equations

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

def Phenomena.Gender.Studies.Kramer2020.viSet2 (ch : Morphology.DM.CatHead) : ℕ

Set 2 VI: [−FEM] → 1 (masculine), everything else → 0 (feminine).

Equations

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

def Phenomena.Gender.Studies.Kramer2020.viThreeGender (ch : Morphology.DM.CatHead) : ℕ

3-gender VI: [+FEM] → 0, [−FEM] → 1, no feature → 2.

Equations

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

theorem Phenomena.Gender.Studies.Kramer2020.spanish_vi_derived : spanishNs.computeSurfaceGenders viSet1 = spanishNs.surfaceGenders

theorem Phenomena.Gender.Studies.Kramer2020.amharic_vi_derived : amharicNs.computeSurfaceGenders viSet1 = amharicNs.surfaceGenders

theorem Phenomena.Gender.Studies.Kramer2020.maa_vi_derived : maaNs.computeSurfaceGenders viSet2 = maaNs.surfaceGenders

theorem Phenomena.Gender.Studies.Kramer2020.russian_vi_derived : russianNs.computeSurfaceGenders viThreeGender = russianNs.surfaceGenders

theorem Phenomena.Gender.Studies.Kramer2020.mangarayi_vi_derived : mangarayiNs.computeSurfaceGenders viThreeGender = mangarayiNs.surfaceGenders

theorem Phenomena.Gender.Studies.Kramer2020.lavukaleve_vi_derived : lavukaleveNs.computeSurfaceGenders viThreeGender = lavukaleveNs.surfaceGenders

theorem Phenomena.Gender.Studies.Kramer2020.dieri_vi_derived : dieriNs.computeSurfaceGenders viSet1 = dieriNs.surfaceGenders

Dieri: same 3-n inventory as Mangarayi but 2 surface genders under Set 1 VI (where plain n → masculine, not neuter).

theorem Phenomena.Gender.Studies.Kramer2020.dieri_mangarayi_vi_contrast : dieriNs.nHeads = mangarayiNs.nHeads ∧ dieriNs.computeSurfaceGenders viSet1 ≠ mangarayiNs.computeSurfaceGenders viThreeGender

The Dieri vs Mangarayi contrast: same n-heads, different VI → different surface gender counts. This is now DERIVED, not stipulated.