Corbett (1991): Gender — typology of noun-class systems

[Cor91] [Cor13] [DH13a] [Dix72]

Greville Corbett. Gender. Cambridge University Press, 1991. Plus [Cor13]'s WALS Chs 30, 31, 32.

This study file holds the 22-language exemplar sample and Corbett's cross-linguistic generalisations over it. The per-language records (Profile) live here — per-language paper-specific data belongs in the study file that consumes it, not in Fragments. The WALS chapter values are stored explicitly per language and grounded against Data.WALS.F30A/F31A/F32A by the *_wals_grounded theorems; the Ch 30 bin is derived from the controller-gender count (Profile.genderCount), so bin/count consistency holds by construction.

Deviations from earlier revisions

• The former GenderProfile substrate (fromWALS smart constructor with silent fallbacks, stored count + bin + consistency predicates) was dissolved into this file 2026-06-10.
• The former IsCanonicalGender predicate was renamed IsPrototypicalSexBased: "canonical gender" is [CF16], whose Canonical Gender Principle makes purely semantic assignment canonical — the prototypical Indo-European mixed-assignment cell this predicate picks out is non-canonical in their sense.
• The former Dyirbal basis-override ("Corbett 1991 treats Dyirbal as non-sex-based") was dropped as unverifiable against the monograph: ch. 2 presents Dyirbal classes I/II as organised around male/female humans, which is WALS's sex-based criterion. The non-sex-based reading is Dixon/Lakoff framing and belongs to a study anchored on them.

Sample composition

22 languages spanning all five WALS Ch 30 values: no gender (Mandarin, Japanese, Turkish, Finnish, Korean, Quechua), 2 genders (French, Spanish, Hindi-Urdu, Irish, Hebrew, Hausa), 3 genders (German, Russian, Latin, Romanian, and — as a pronominal system — English), 4 genders (Dyirbal, Archi), 5+ noun classes (Swahili, Zulu, Fula).

Substrate: semantic bases and per-language profiles

inductive Corbett1991.SemanticBasis : Type

Semantic dimensions that can underlie gender / noun-class assignment. Editorial five-way cut over [Cor91]'s assignment discussion; consumed by [Kra20]'s Semantic Core Generalization.

• sex : SemanticBasis
• animacy : SemanticBasis
• humanness : SemanticBasis
• shape : SemanticBasis
• rationality : SemanticBasis

@[implicit_reducible]

instance Corbett1991.instDecidableEqSemanticBasis : DecidableEq SemanticBasis

Equations

• Corbett1991.instDecidableEqSemanticBasis x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Corbett1991.instBEqSemanticBasis : BEq SemanticBasis

Equations

• Corbett1991.instBEqSemanticBasis = { beq := Corbett1991.instBEqSemanticBasis.beq }

def Corbett1991.instBEqSemanticBasis.beq : SemanticBasis → SemanticBasis → Bool

Equations

• Corbett1991.instBEqSemanticBasis.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Corbett1991.instReprSemanticBasis.repr : SemanticBasis → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Corbett1991.instReprSemanticBasis : Repr SemanticBasis

Equations

• Corbett1991.instReprSemanticBasis = { reprPrec := Corbett1991.instReprSemanticBasis.repr }

structure Corbett1991.Profile : Type

A language's gender record for this study: the controller-gender count ([Cor91]'s ch. 6 counting — Swahili has 7 genders over ~15 traditional classes; Fula ~20), the WALS Ch 31/32 codings stored explicitly (grounded against Data.WALS below), agreement-target inventory, semantic bases, and the comparative-label bridge for sex-based systems.

• name : String
• iso639 : String
• rawCount : ℕ

  Controller genders ([Cor91] ch. 6): sets of nouns taking the same agreements, with singular/plural pairings counted once.

• basis : Data.WALS.F31A.GenderBasis

  WALS Ch 31 value ([Cor13]).

• assignment : Data.WALS.F32A.SystemsOfGenderAssignment

  WALS Ch 32 value ([Cor13]).

• agreementTargets : List Agreement.AgreementTarget

  Targets where gender agreement surfaces. An inventory, not the Agreement Hierarchy itself (which is a monotonicity claim about hybrid nouns; not yet formalized).

• semanticBases : List SemanticBasis

  Semantic dimensions organising the system.

• attestedGenders : List Gender

  Comparative-label bridge for systems the masculine/feminine/neuter/common vocabulary covers; [] for noun-class systems (Bantu, Dyirbal).

def Corbett1991.instReprProfile.repr : Profile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Corbett1991.instReprProfile : Repr Profile

Equations

• Corbett1991.instReprProfile = { reprPrec := Corbett1991.instReprProfile.repr }

@[implicit_reducible]

instance Corbett1991.instDecidableEqProfile : DecidableEq Profile

Equations

• Corbett1991.instDecidableEqProfile = Corbett1991.instDecidableEqProfile.decEq

def Corbett1991.instDecidableEqProfile.decEq (x✝ x✝¹ : Profile) : Decidable (x✝ = x✝¹)

Equations

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

def Corbett1991.Profile.genderCount (p : Profile) : Data.WALS.F30A.GenderCount

WALS Ch 30 bin, derived from the controller-gender count. A count of 1 maps to .none: one agreement pattern for all nouns is the absence of a system, not a one-gender system ([Kra15]'s two-class minimum; cf. Gender.System's Nontrivial convention).

Equations

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

def Corbett1991.Profile.HasAgreement (p : Profile) : Prop

Whether the language has any gender agreement.

Equations

• p.HasAgreement = (p.agreementTargets ≠ [])

@[implicit_reducible]

instance Corbett1991.Profile.instDecidablePredHasAgreement : DecidablePred HasAgreement

Equations

• p.instDecidablePredHasAgreement = inferInstance

def Corbett1991.Profile.IsNounClassSystem (p : Profile) : Prop

"Noun class" system: 5+ controller genders per [Cor91]'s conventional cut.

Equations

• p.IsNounClassSystem = (p.rawCount ≥ 5)

@[implicit_reducible]

instance Corbett1991.Profile.instDecidablePredIsNounClassSystem : DecidablePred IsNounClassSystem

Equations

• p.instDecidablePredIsNounClassSystem = inferInstance

def Corbett1991.Profile.IsCoherent (p : Profile) : Prop

Internal coherence: a no-gender language has no-gender WALS codings and no agreement targets; a gendered one has gendered codings.

Equations

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

@[implicit_reducible]

instance Corbett1991.Profile.instDecidablePredIsCoherent : DecidablePred IsCoherent

Equations

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

def Corbett1991.Profile.IsPrototypicalSexBased (p : Profile) : Prop

Prototypical European-style gender system: sex-based, 2 or 3 genders, semantic + formal assignment.

Not [CF16]'s canonical gender: their Canonical Gender Principle makes purely semantic assignment canonical, so this mixed-assignment cell is non-canonical in their sense. The predicate picks out the prototypical Indo-European configuration.

Equations

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

@[implicit_reducible]

instance Corbett1991.Profile.instDecidablePredIsPrototypicalSexBased : DecidablePred IsPrototypicalSexBased

Equations

• p.instDecidablePredIsPrototypicalSexBased = inferInstance

WALS grounding predicates

The stored Ch 30/31/32 values agree with Data.WALS wherever WALS covers the language; for WALS-silent languages (Fula, Irish, Latin, Romanian) the predicates hold vacuously and the stored value is this file's commitment.

def Corbett1991.Profile.CountGrounded (p : Profile) : Prop

Derived Ch 30 bin agrees with WALS F30A where covered.

Equations

• p.CountGrounded = ∀ d ∈ Data.WALS.F30A.lookupISO p.iso639, d.value = p.genderCount

def Corbett1991.Profile.BasisGrounded (p : Profile) : Prop

Stored Ch 31 basis agrees with WALS F31A where covered.

Equations

• p.BasisGrounded = ∀ d ∈ Data.WALS.F31A.lookupISO p.iso639, d.value = p.basis

def Corbett1991.Profile.AssignmentGrounded (p : Profile) : Prop

Stored Ch 32 assignment agrees with WALS F32A where covered.

Equations

• p.AssignmentGrounded = ∀ d ∈ Data.WALS.F32A.lookupISO p.iso639, d.value = p.assignment

@[implicit_reducible]

instance Corbett1991.Profile.instDecidablePredCountGrounded : DecidablePred CountGrounded

Equations

• p.instDecidablePredCountGrounded = inferInstance

@[implicit_reducible]

instance Corbett1991.Profile.instDecidablePredBasisGrounded : DecidablePred BasisGrounded

Equations

• p.instDecidablePredBasisGrounded = inferInstance

@[implicit_reducible]

instance Corbett1991.Profile.instDecidablePredAssignmentGrounded : DecidablePred AssignmentGrounded

Equations

• p.instDecidablePredAssignmentGrounded = inferInstance

The 22-language exemplar sample

Public (not private): [Kra20] and [Car26] consume individual profiles.

def Corbett1991.english : Profile

Equations

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

def Corbett1991.mandarin : Profile

Equations

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

def Corbett1991.japanese : Profile

Equations

• Corbett1991.japanese = { name := "Japanese", iso639 := "jpn", rawCount := 0, basis := Data.WALS.F31A.GenderBasis.noGender, assignment := Data.WALS.F32A.SystemsOfGenderAssignment.noGender }

def Corbett1991.turkish : Profile

Equations

• Corbett1991.turkish = { name := "Turkish", iso639 := "tur", rawCount := 0, basis := Data.WALS.F31A.GenderBasis.noGender, assignment := Data.WALS.F32A.SystemsOfGenderAssignment.noGender }

def Corbett1991.finnish : Profile

Equations

• Corbett1991.finnish = { name := "Finnish", iso639 := "fin", rawCount := 0, basis := Data.WALS.F31A.GenderBasis.noGender, assignment := Data.WALS.F32A.SystemsOfGenderAssignment.noGender }

def Corbett1991.korean : Profile

Equations

• Corbett1991.korean = { name := "Korean", iso639 := "kor", rawCount := 0, basis := Data.WALS.F31A.GenderBasis.noGender, assignment := Data.WALS.F32A.SystemsOfGenderAssignment.noGender }

def Corbett1991.quechua : Profile

Equations

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

def Corbett1991.french : Profile

Equations

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

def Corbett1991.spanish : Profile

Equations

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

def Corbett1991.hindiUrdu : Profile

Equations

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

def Corbett1991.irish : Profile

Equations

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

def Corbett1991.hebrew : Profile

Equations

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

def Corbett1991.hausa : Profile

Equations

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

def Corbett1991.german : Profile

Equations

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

def Corbett1991.russian : Profile

Equations

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

def Corbett1991.latin : Profile

Equations

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

def Corbett1991.romanian : Profile

Equations

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

def Corbett1991.dyirbal : Profile

Equations

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

def Corbett1991.archi : Profile

Archi. The stored assignment is this file's [Cor91] commitment (semantic and formal: the monograph documents phonological and morphological correlates for the gender III/IV split -- UNVERIFIED: locate the passage), diverging from WALS F32A's semantic-only coding — see archi_corbett1991_vs_corbett2013.

Equations

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

def Corbett1991.swahili : Profile

Equations

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

def Corbett1991.zulu : Profile

Equations

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

def Corbett1991.fula : Profile

Equations

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

def Corbett1991.allProfiles : List Profile

All 22 language profiles in the Corbett 1991 sample.

Equations

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

WALS grounding

theorem Corbett1991.count_wals_grounded (p : Profile) : p ∈ allProfiles → p.CountGrounded

Every derived Ch 30 bin agrees with WALS F30A where covered.

theorem Corbett1991.basis_wals_grounded (p : Profile) : p ∈ allProfiles → p.BasisGrounded

Every stored Ch 31 basis agrees with WALS F31A where covered.

theorem Corbett1991.assignment_wals_grounded (p : Profile) : p ∈ allProfiles → p.iso639 ≠ "aqc" → p.AssignmentGrounded

Every stored Ch 32 assignment agrees with WALS F32A where covered — except Archi, whose 1991-vs-2013 divergence is first-class below.

theorem Corbett1991.archi_corbett1991_vs_corbett2013 : archi.assignment = Data.WALS.F32A.SystemsOfGenderAssignment.semanticAndFormal ∧ ∀ d ∈ Data.WALS.F32A.lookupISO "aqc", d.value = Data.WALS.F32A.SystemsOfGenderAssignment.semantic

Corbett 1991 vs 2013: Archi. The 1991 monograph treats assignment as semantic and formal; the 2013 WALS chapter (F32A) codes Archi as semantic-only.

Sample-level structural sanity

theorem Corbett1991.all_coherent (p : Profile) : p ∈ allProfiles → p.IsCoherent

All profiles are internally coherent.

theorem Corbett1991.all_gender_counts_attested : (∃ p ∈ allProfiles, p.genderCount = Data.WALS.F30A.GenderCount.none) ∧ (∃ p ∈ allProfiles, p.genderCount = Data.WALS.F30A.GenderCount.two) ∧ (∃ p ∈ allProfiles, p.genderCount = Data.WALS.F30A.GenderCount.three) ∧ (∃ p ∈ allProfiles, p.genderCount = Data.WALS.F30A.GenderCount.four) ∧ ∃ p ∈ allProfiles, p.genderCount = Data.WALS.F30A.GenderCount.fiveOrMore

All five WALS Ch 30 values are attested.

theorem Corbett1991.all_bases_attested : (∃ p ∈ allProfiles, p.basis = Data.WALS.F31A.GenderBasis.noGender) ∧ (∃ p ∈ allProfiles, p.basis = Data.WALS.F31A.GenderBasis.sexBased) ∧ ∃ p ∈ allProfiles, p.basis = Data.WALS.F31A.GenderBasis.nonSexBased

All three Ch 31 values are attested.

theorem Corbett1991.all_assignments_attested : (∃ p ∈ allProfiles, p.assignment = Data.WALS.F32A.SystemsOfGenderAssignment.noGender) ∧ (∃ p ∈ allProfiles, p.assignment = Data.WALS.F32A.SystemsOfGenderAssignment.semantic) ∧ ∃ p ∈ allProfiles, p.assignment = Data.WALS.F32A.SystemsOfGenderAssignment.semanticAndFormal

All three Ch 32 values are attested.

Cross-linguistic generalisations

theorem Corbett1991.two_three_gender_all_sex_based (p : Profile) : p ∈ allProfiles → p.genderCount = Data.WALS.F30A.GenderCount.two ∨ p.genderCount = Data.WALS.F30A.GenderCount.three → p.basis = Data.WALS.F31A.GenderBasis.sexBased

All 2- and 3-gender systems in the sample are sex-based. Reflects the cross-linguistic pattern that small gender systems organise around sex.

theorem Corbett1991.no_purely_formal_in_sample (p : Profile) : p ∈ allProfiles → p.genderCount ≠ Data.WALS.F30A.GenderCount.none → p.assignment = Data.WALS.F32A.SystemsOfGenderAssignment.semantic ∨ p.assignment = Data.WALS.F32A.SystemsOfGenderAssignment.semanticAndFormal

[Cor91]'s key finding: no language assigns gender on a purely formal basis without any semantic core. In the sample, every gendered language has semantic assignment (alone or combined with formal).

theorem Corbett1991.gender_implies_agreement (p : Profile) : p ∈ allProfiles → (p.genderCount ≠ Data.WALS.F30A.GenderCount.none → p.HasAgreement) ∧ (p.genderCount = Data.WALS.F30A.GenderCount.none → ¬p.HasAgreement)

A gender system without any agreement is not a gender system — genders are precisely the categories that trigger agreement.

Agreement-target inventories

[Cor79] / [Cor91] ch. 8's Agreement Hierarchy has four positions: attributive > predicate > relative pronoun > personal pronoun. Verbal agreement (the substrate's .verb target, tested below) is subsumed under the predicate position in Corbett's scheme.

The theorems below are inventory observations on the sample — which targets mark gender at all. The hierarchy's actual content (monotone availability of semantic agreement along the positions) is formalized for number agreement in Studies/Corbett2000.lean (AgreementProfile.RespectsHierarchy, with British English committee as witness); the gender-side analogue for hybrid nouns like vrač needs per-target assignment on Gender.System.Assigned and is still open.

theorem Corbett1991.verb_agreement_implies_higher (p : Profile) : p ∈ allProfiles → Agreement.AgreementTarget.verb ∈ p.agreementTargets → Agreement.AgreementTarget.attributive ∈ p.agreementTargets ∨ Agreement.AgreementTarget.predicate ∈ p.agreementTargets ∨ Agreement.AgreementTarget.personalPronoun ∈ p.agreementTargets

Verb agreement implies higher-target agreement in the sample (none of the languages agree only on verbs).

theorem Corbett1991.no_verb_only_agreement (p : Profile) : p ∈ allProfiles → p.agreementTargets ≠ [Agreement.AgreementTarget.verb]

No language in the sample agrees only on verbs.

theorem Corbett1991.english_pronominal_gender : english.genderCount ≠ Data.WALS.F30A.GenderCount.none ∧ english.agreementTargets = [Agreement.AgreementTarget.personalPronoun]

English is the sample's pronominal gender system: it has gender (3 genders, he/she/it) but gender surfaces only on personal pronouns.

theorem Corbett1991.noun_class_rich_agreement (p : Profile) : p ∈ allProfiles → p.IsNounClassSystem → p.agreementTargets.length ≥ 4

Noun-class systems (5+) show agreement on more targets than smaller systems. In the sample, all noun-class systems agree on ≥4 of the 5 target types.

Basis × count interactions

theorem Corbett1991.non_sex_based_more_genders (p : Profile) : p ∈ allProfiles → p.basis = Data.WALS.F31A.GenderBasis.nonSexBased → p.rawCount ≥ 4

Non-sex-based systems in the sample have ≥4 genders. When gender is not organised around sex, the system tends to proliferate.

Prototypical sex-based systems

theorem Corbett1991.prototypical_sex_based_attested : french.IsPrototypicalSexBased ∧ spanish.IsPrototypicalSexBased ∧ german.IsPrototypicalSexBased ∧ russian.IsPrototypicalSexBased ∧ latin.IsPrototypicalSexBased ∧ romanian.IsPrototypicalSexBased ∧ hindiUrdu.IsPrototypicalSexBased

The European languages in the sample (and Hindi-Urdu) all instantiate the prototypical sex-based configuration. (See Profile.IsPrototypicalSexBased for why this is not [CF16]'s canonical gender.)

Gender bridge

theorem Corbett1991.surface_gender_bridge_populated (p : Profile) : p ∈ allProfiles → (p.genderCount = Data.WALS.F30A.GenderCount.two ∧ p.basis = Data.WALS.F31A.GenderBasis.sexBased → p.attestedGenders.length = 2) ∧ (p.genderCount = Data.WALS.F30A.GenderCount.three ∧ p.basis = Data.WALS.F31A.GenderBasis.sexBased → p.attestedGenders.length = 3)

Every 2- or 3-gender sex-based language in the sample exposes the appropriate Gender comparative labels via attestedGenders.

ISO code sanity (drift sentry)

theorem Corbett1991.iso_codes_unique : (List.map (fun (x : Profile) => x.iso639) allProfiles).eraseDups.length = allProfiles.length