Carstens (2026): The grammar of gender

In Xhosa, conjoined singulars of genders 1/2, 7/8 and 9/10 take gender-matching plural agreement, while those of 3/4 and 5/6, like mismatched conjuncts, take the semantic agreement of class 2 for humans and class 8 for the rest. Carstens reads the split as interpretability. Every Bantu nominal is a stacked nP, a core n bearing a semantic gender (i[human], i[animal] and i[inanimate] in Xhosa, i[human] and i[non-human] in Shona) under the n that fixes its class. Following Adamson and Anagnostopoulou, only interpretable gender features percolate to &P, where they are intersected, so a u-gender contributes nothing; the arbitrary members of an interpretable gender carry a bare i[entity] flavor and still match.

Two grammars read the intersection: Highest Wins takes the shared visible gender and Best Semantic Match the shared core, the source of the minority choices. Where neither matches, the conjunction is ineffable. In Shona six of the eight genders are uninterpretable, so matching agreement is the exception.

Implementation notes

• A nominal is a core gender under an optional outer gender. The visible gender's feature carries the interpretability of its n and resolves by Minimalist.Coordination.resolve, so u-genders drop out by the substrate's percolation; the cores resolve as interpretable.
• A noun's core is the gender whose n bears the flavor of what it denotes, read off the fragment's animacy and the genders' status; its outer layer is its own gender.
• The rows carry the example sentences with the classes they accept and reject, and the Table 13 counts on one example per cell. Single-conjunct agreement, the choices offered in at most 5% of cases and Taraldsen et al.'s Tables 4 and 6, which the paper sets aside, are not encoded, nor is the comparison with Halpert and Hammerly's binary features in §8.

References

• [Car26]
• [AA25]
• [Kra15]
• [TTML18]
• [HH26]

def Carstens2026.interpretability : Bantu.GenderStatus → Minimalist.Interpretability

Whether the n of a gender carries a feature that percolates to &P, (13) and (77b).

Equations

• Carstens2026.interpretability (Bantu.GenderStatus.interpretable a) = Minimalist.Interpretability.interpretable
• Carstens2026.interpretability Bantu.GenderStatus.uninterpretable = Minimalist.Interpretability.uninterpretable

Nominals and the two grammars (§4–§5)

structure Carstens2026.Nominal (G : Type u_3) : Type u_3

A Bantu nominal is a core nP of the gender that carries the semantic flavor of what it denotes, wrapped, when its visible class belongs to another gender, in an outer nP of that gender, (10) and (72)–(73).

• core : G
• outer : Option G

@[instance_reducible]

instance Carstens2026.instDecidableEqNominal {G✝ : Type u_3} [DecidableEq G✝] : DecidableEq (Nominal G✝)

Equations

• Carstens2026.instDecidableEqNominal = Carstens2026.instDecidableEqNominal.decEq

def Carstens2026.instDecidableEqNominal.decEq {G✝ : Type u_3} [DecidableEq G✝] (x✝ x✝¹ : Nominal G✝) : Decidable (x✝ = x✝¹)

Equations

• Carstens2026.instDecidableEqNominal.decEq { core := a, outer := a_1 } { core := b, outer := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Carstens2026.instReprNominal {G✝ : Type u_3} [Repr G✝] : Repr (Nominal G✝)

Equations

• Carstens2026.instReprNominal = { reprPrec := Carstens2026.instReprNominal.repr }

def Carstens2026.instReprNominal.repr {G✝ : Type u_3} [Repr G✝] : Nominal G✝ → ℕ → Std.Format

Equations

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

def Carstens2026.Nominal.visible {G : Type u_1} (n : Nominal G) : G

The visible gender, the outer layer's or the core's.

Equations

• n.visible = n.outer.getD n.core

def Carstens2026.Nominal.genders {G : Type u_1} (n : Nominal G) : List G

The genders of the nominal's n's, innermost first.

Equations

• n.genders = n.core :: n.outer.toList

theorem Carstens2026.Nominal.visible_eq_agreeingGender {G : Type u_1} (n : Nominal G) (r : DistributedMorphology.Root) (d : G) : n.visible = DistributedMorphology.agreeingGender some d ({ root := r, heads := n.genders }.lastCycle fun (x : G) => True) ∧ n.visible = DistributedMorphology.agreeingGender some d n.genders.reverse

The visible gender is the agreeing gender of the Highest Gender Hypothesis, the gender a probe finds in the last cycle of the nominal; since every n bears a gender, a probe searching every n finds it too.

def Carstens2026.Nominal.visibleBundle {G : Type u_1} (status : G → Bantu.GenderStatus) (n : Nominal G) : Minimalist.Coordination.Bundle G

The visible gender's feature as percolation sees it, annotated with the interpretability of the gender's n.

Equations

• Carstens2026.Nominal.visibleBundle status n = Minimalist.Coordination.Bundle.single n.visible (Carstens2026.interpretability (status n.visible))

def Carstens2026.Nominal.coreBundle {G : Type u_1} (n : Nominal G) : Minimalist.Coordination.Bundle G

The core's feature, always interpretable.

Equations

• n.coreBundle = Minimalist.Coordination.Bundle.single n.core Minimalist.Interpretability.interpretable

def Carstens2026.Nominal.stack {G : Type u_1} [DecidableEq G] (c g : G) : Nominal G

The nominal of a noun of gender g over the core c, an outer nP of gender g stacked above the core unless the two coincide, (72)–(73).

Equations

• Carstens2026.Nominal.stack c g = { core := c, outer := if g = c then none else some g }

@[simp]

theorem Carstens2026.Nominal.visible_stack {G : Type u_1} [DecidableEq G] (c g : G) : (stack c g).visible = g

def Carstens2026.highestWins {G : Type u_1} {C : Type u_2} (status : G → Bantu.GenderStatus) (pluralClass : G → C) [DecidableEq G] (a b : Nominal G) : Option C

Highest Wins (79), where the visible genders percolate and intersect, the shared gender valuing its plural class.

Equations

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

def Carstens2026.bestSemanticMatch {G : Type u_1} {C : Type u_2} (pluralClass : G → C) [DecidableEq G] (a b : Nominal G) : Option C

Best Semantic Match (80), where the cores intersect, a total match of gender with flavor, the shared core valuing its plural class.

Equations

• Carstens2026.bestSemanticMatch pluralClass a b = if a.core ∈ Minimalist.Coordination.resolve a.coreBundle b.coreBundle then some (pluralClass a.core) else none

def Carstens2026.Values {G : Type u_1} {C : Type u_2} (status : G → Bantu.GenderStatus) (pluralClass : G → C) [DecidableEq G] (a b : Nominal G) (c : C) : Prop

c values plural agreement on &P under one of the two grammars (§5.1).

Equations

• Carstens2026.Values status pluralClass a b c = (Carstens2026.highestWins status pluralClass a b = some c ∨ Carstens2026.bestSemanticMatch pluralClass a b = some c)

@[instance_reducible]

instance Carstens2026.instDecidableValuesOfDecidableEq {G : Type u_1} {C : Type u_2} (status : G → Bantu.GenderStatus) (pluralClass : G → C) [DecidableEq G] (a b : Nominal G) [DecidableEq C] (c : C) : Decidable (Values status pluralClass a b c)

Equations

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

theorem Carstens2026.highestWins_eq {G : Type u_1} {C : Type u_2} (status : G → Bantu.GenderStatus) (pluralClass : G → C) [DecidableEq G] {a b : Nominal G} : highestWins status pluralClass a b = if interpretability (status a.visible) = Minimalist.Interpretability.interpretable ∧ a.visible = b.visible then some (pluralClass a.visible) else none

theorem Carstens2026.bestSemanticMatch_eq {G : Type u_1} {C : Type u_2} (pluralClass : G → C) [DecidableEq G] {a b : Nominal G} : bestSemanticMatch pluralClass a b = if a.core = b.core then some (pluralClass a.core) else none

theorem Carstens2026.matching_iff {G : Type u_1} {C : Type u_2} (status : G → Bantu.GenderStatus) (pluralClass : G → C) [DecidableEq G] {a b : Nominal G} (h : a.visible = b.visible) : highestWins status pluralClass a b = some (pluralClass a.visible) ↔ interpretability (status a.visible) = Minimalist.Interpretability.interpretable

Uniform conjuncts pair with gender-matching plural agreement exactly when their gender is interpretable, (52a–b) and (54).

theorem Carstens2026.values_iff_of_uninterpretable {G : Type u_1} {C : Type u_2} (status : G → Bantu.GenderStatus) (pluralClass : G → C) [DecidableEq G] {a b : Nominal G} (hu : interpretability (status a.visible) = Minimalist.Interpretability.uninterpretable) (c : C) : Values status pluralClass a b c ↔ bestSemanticMatch pluralClass a b = some c

A u-gender stacked above a core is ignored, the cores alone valuing agreement (77).

theorem Carstens2026.two_grammars {G : Type u_1} {C : Type u_2} (status : G → Bantu.GenderStatus) (pluralClass : G → C) [DecidableEq G] {a : Nominal G} {g : G} (ho : a.outer = some g) (hi : interpretability (status g) = Minimalist.Interpretability.interpretable) : highestWins status pluralClass a a = some (pluralClass g) ∧ bestSemanticMatch pluralClass a a = some (pluralClass a.core)

An arbitrary member of an interpretable gender stacked above a core carries both i-genders to &P, uniform conjuncts match twice, and the two grammars value the visible and the core plural respectively, (78)–(80).

theorem Carstens2026.highestWins_eq_bestSemanticMatch {G : Type u_1} {C : Type u_2} (status : G → Bantu.GenderStatus) (pluralClass : G → C) [DecidableEq G] {a b : Nominal G} (ha : a.outer = none) (hb : b.outer = none) (hi : interpretability (status a.core) = Minimalist.Interpretability.interpretable) : highestWins status pluralClass a b = bestSemanticMatch pluralClass a b

Single-layer conjuncts of an interpretable gender give the two grammars nothing to disagree about.

theorem Carstens2026.not_values {G : Type u_1} {C : Type u_2} (status : G → Bantu.GenderStatus) (pluralClass : G → C) [DecidableEq G] {a b : Nominal G} (hv : a.visible ≠ b.visible) (hc : a.core ≠ b.core) (c : C) : ¬Values status pluralClass a b c

With neither the visible genders nor the cores matching, no class values agreement and the conjunction is ineffable, (91)–(92) and (111)–(112).

Xhosa (71)–(73)

def Carstens2026.xhosaFlavor : Reference.Animacy → Bantu.SemanticCore

The flavor of what a Xhosa noun denotes, [human], [animal] or [inanimate] (71).

Equations

• Carstens2026.xhosaFlavor Reference.Animacy.human = Bantu.SemanticCore.human
• Carstens2026.xhosaFlavor Reference.Animacy.animate = Bantu.SemanticCore.animal
• Carstens2026.xhosaFlavor Reference.Animacy.inanimate = Bantu.SemanticCore.inanimate

theorem Carstens2026.xhosaFlavor_existsUnique (a : Reference.Animacy) : ∃! g : Xhosa.Gender, g.status = Bantu.GenderStatus.interpretable (xhosaFlavor a)

Each flavor is borne by exactly one gender, A [human], E [animal] and D [inanimate] (71).

def Carstens2026.xhosaCore (a : Reference.Animacy) : Xhosa.Gender

The core of a noun, the gender whose n bears the flavor of what it denotes.

Equations

• Carstens2026.xhosaCore a = Fintype.choose (fun (a_1 : Xhosa.Gender) => a_1.status = Bantu.GenderStatus.interpretable (Carstens2026.xhosaFlavor a)) ⋯

def Carstens2026.xhosaNominal (n : Xhosa.Noun) : Nominal Xhosa.Gender

A noun's nominal, its core from what it denotes and its gender stacked above, (72)–(73).

Equations

• Carstens2026.xhosaNominal n = Carstens2026.Nominal.stack (Carstens2026.xhosaCore n.animacy) n.gender

Shona (§3.5, §5.2)

def Carstens2026.shonaFlavor : Reference.Animacy → Bantu.SemanticCore

The flavor of what a Shona noun denotes, [human] or [non-human] (§5.2).

Equations

• Carstens2026.shonaFlavor Reference.Animacy.human = Bantu.SemanticCore.human
• Carstens2026.shonaFlavor x✝ = Bantu.SemanticCore.nonhuman

theorem Carstens2026.shonaFlavor_existsUnique (a : Reference.Animacy) : ∃! g : Shona.Gender, g.status = Bantu.GenderStatus.interpretable (shonaFlavor a)

Each flavor is borne by exactly one gender, A [human] and D [non-human].

def Carstens2026.shonaCore (a : Reference.Animacy) : Shona.Gender

The core of a noun, the gender whose n bears the flavor of what it denotes.

Equations

• Carstens2026.shonaCore a = Fintype.choose (fun (a_1 : Shona.Gender) => a_1.status = Bantu.GenderStatus.interpretable (Carstens2026.shonaFlavor a)) ⋯

def Carstens2026.shonaNominal (n : Shona.Noun) : Nominal Shona.Gender

A Shona noun's nominal, where a diminutive's u-gender 12/13 stacks above its core (98).

Equations

• Carstens2026.shonaNominal n = Carstens2026.Nominal.stack (Carstens2026.shonaCore n.animacy) n.gender

The rows

def Carstens2026.rows (glottocode : String) : List Datum

The rows of one language.

Equations

• Carstens2026.rows glottocode = List.filter (fun (x : Datum) => decide (x.language = glottocode)) Carstens2026.Examples.all

def Carstens2026.xhosaClassOf : String → Option Xhosa.NounClass

The Xhosa plural class a row's class number names.

Equations

• Carstens2026.xhosaClassOf "2" = some Xhosa.NounClass.cl2
• Carstens2026.xhosaClassOf "4" = some Xhosa.NounClass.cl4
• Carstens2026.xhosaClassOf "6" = some Xhosa.NounClass.cl6
• Carstens2026.xhosaClassOf "8" = some Xhosa.NounClass.cl8
• Carstens2026.xhosaClassOf "10" = some Xhosa.NounClass.cl10
• Carstens2026.xhosaClassOf x✝ = none

def Carstens2026.shonaClassOf : String → Option Shona.NounClass

The Shona plural class a row's class number names.

Equations

• Carstens2026.shonaClassOf "2" = some Shona.NounClass.cl2
• Carstens2026.shonaClassOf "4" = some Shona.NounClass.cl4
• Carstens2026.shonaClassOf "6" = some Shona.NounClass.cl6
• Carstens2026.shonaClassOf "8" = some Shona.NounClass.cl8
• Carstens2026.shonaClassOf "10" = some Shona.NounClass.cl10
• Carstens2026.shonaClassOf "13" = some Shona.NounClass.cl13
• Carstens2026.shonaClassOf x✝ = none

def Carstens2026.conjuncts {G : Type u_1} {N : Type u_3} (nouns : List N) (form : N → String) (nominal : N → Nominal G) (e : Datum) : Option (Nominal G × Nominal G)

A row's conjuncts, the nominals of the nouns it names.

Equations

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

def Carstens2026.Predicts {G : Type u_1} {C : Type u_2} [DecidableEq G] (status : G → Bantu.GenderStatus) (pluralClass : G → C) (classOf : String → Option C) (p : Nominal G × Nominal G) (e : Datum) : Prop

The two grammars predict a row on the conjuncts p when every class it accepts values agreement under one of them and no class it rejects does.

Equations

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

@[instance_reducible]

instance Carstens2026.instDecidablePredictsOfDecidableEq {G : Type u_1} {C : Type u_2} [DecidableEq G] (status : G → Bantu.GenderStatus) (pluralClass : G → C) (classOf : String → Option C) [DecidableEq C] (p : Nominal G × Nominal G) (e : Datum) : Decidable (Predicts status pluralClass classOf p e)

Equations

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

theorem Carstens2026.xhosa_rows (e : Datum) : e ∈ rows "xhos1239" → ∃ p ∈ conjuncts Xhosa.Nouns.all (fun (x : Xhosa.Noun) => x.form) xhosaNominal e, Predicts Xhosa.Gender.status Xhosa.Gender.pluralClass xhosaClassOf p e

The Xhosa rows are predicted, (6)–(9), (37)–(49), (55), (81)–(91) and (111).

theorem Carstens2026.shona_rows (e : Datum) : e ∈ rows "shon1251" → ∃ p ∈ conjuncts Shona.Nouns.all (fun (x : Shona.Noun) => x.form) shonaNominal e, Predicts Shona.Gender.status Shona.Gender.pluralClass shonaClassOf p e

The Shona rows are predicted, matching agreement confined to 1/2 and 7/8, (58)–(68).

theorem Carstens2026.table13 (e : Datum) : e ∈ rows "xhos1239" → ∀ m ∈ e.nat? "matching", ∀ d ∈ e.nat? "default", ∀ p ∈ conjuncts Xhosa.Nouns.all (fun (x : Xhosa.Noun) => x.form) xhosaNominal e, d ≤ m ↔ interpretability p.1.visible.status = Minimalist.Interpretability.interpretable

Gender-matching agreement is chosen at least as often as default exactly in the cells whose gender is interpretable, Table 13 and (52a–b).

Taraldsen et al.'s reading (§3.2.3)

theorem Carstens2026.taraldsen_split (g : Xhosa.Gender) : interpretability g.status = Minimalist.Interpretability.interpretable ↔ TaraldsenEtAl2018.SharesClassifierN (TaraldsenEtAl2018.xhosaSg g) (TaraldsenEtAl2018.xhosaPl g)

The same failures read structurally by [TTML18]. The genders whose singular and plural prefixes share one classifier N are exactly the interpretable genders, the paper's diagnostic and their partition of the Xhosa data coinciding.