Halpert and Hammerly (2026): Reconciling Animacy and Noun Class in Bantu

This file formalizes the Core Noun Class Hypothesis: every Bantu noun is specified for [±Animate, ±Human] on its nominalizing head, Kramer's gendered n, and so belongs to one of the core classes HUMAN, ANIMATE and INANIMATE, canonically classes 1/2, 9/10 and 7/8 (19), whatever class its prefix shows. The features are Hammerly's containment sets of ontological primitives ranked by prominence (1), so every category a specification denotes is order-convex, and no conflation in McGinnis's sense groups humans with natural forces to the exclusion of animals.

Class prefixes are secondary n's stacked over the core, as in Fuchs and van der Wal's diminutives, so a nominal is Carstens's stacked nominal over the core classes. Agreement depends on the probe (29): a flat probe finds the secondary n and agrees with the prefix class, as in Zulu, while a probe relativized to [+Animate] searches past it to the core, the animacy override of Chiyao and Swahili and the animate-only object marking of Nyaturu.

Main results

• category_ordConnected: every category is order-convex.
• agreement_flat, agreement_animateProbe: a flat probe agrees with the prefix class and a relativized one with the core.
• isikhohleli_agreement: isikhohleli 'coughing person' agrees in class 7 or class 1 by the probe.

Implementation notes

• A nominal has a secondary n only when its prefix class is a core class other than its core's; ofEntry is undefined for classes 3/4 and 5/6, whose features the paper leaves open.
• The fragment's semantic animacy stands in for the grammatical core, which the paper allows to be idiosyncratic.
• Agreement with conjoined subjects, (15) to (18), is recorded as data only.

References

• [HH26]
• [Ham23]
• [McG05]
• [FvdW22]
• [TTML18]
• [Car26]
• [Kra15]

Containment features, section 2

inductive HalpertHammerly2026.Primitive : Type

The ontological primitives of (1) and (3), most prominent first, which are the author I, the addressee U, other humans O, animals A, natural forces F, concrete things R, and abstract things S.

• author : Primitive
• addressee : Primitive
• human : Primitive
• animal : Primitive
• force : Primitive
• concrete : Primitive
• abstract : Primitive

@[instance_reducible]

instance HalpertHammerly2026.instDecidableEqPrimitive : DecidableEq Primitive

Equations

• HalpertHammerly2026.instDecidableEqPrimitive x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HalpertHammerly2026.instReprPrimitive : Repr Primitive

Equations

• HalpertHammerly2026.instReprPrimitive = { reprPrec := HalpertHammerly2026.instReprPrimitive.repr }

def HalpertHammerly2026.instReprPrimitive.repr : Primitive → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance HalpertHammerly2026.instFintypePrimitive : Fintype Primitive

Equations

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

def HalpertHammerly2026.Primitive.rank : Primitive → ℕ

Prominence rank, the author highest.

Equations

• HalpertHammerly2026.Primitive.author.rank = 0
• HalpertHammerly2026.Primitive.addressee.rank = 1
• HalpertHammerly2026.Primitive.human.rank = 2
• HalpertHammerly2026.Primitive.animal.rank = 3
• HalpertHammerly2026.Primitive.force.rank = 4
• HalpertHammerly2026.Primitive.concrete.rank = 5
• HalpertHammerly2026.Primitive.abstract.rank = 6

@[instance_reducible]

instance HalpertHammerly2026.Primitive.instLinearOrder : LinearOrder Primitive

The prominence order (1), author < addressee < human < animal < force < concrete < abstract.

Equations

• HalpertHammerly2026.Primitive.instLinearOrder = LinearOrder.lift' HalpertHammerly2026.Primitive.rank ⋯

@[reducible, inline]

abbrev HalpertHammerly2026.feature (p : Primitive) : Set Primitive

A feature of (3), the primitives at least as prominent as its cutoff. [Author] is feature .author, [Participant] feature .addressee, [Human] feature .human, [Animate] feature .animal, [Agent] feature .force, [Individuated] feature .concrete, and ɸ feature .abstract, each contained in the next.

Equations

• HalpertHammerly2026.feature p = Set.Iic p

def HalpertHammerly2026.value (p : Primitive) : Bool → Set Primitive

A bivalent value of a feature, the feature itself or its complement.

Equations

• HalpertHammerly2026.value p true = HalpertHammerly2026.feature p
• HalpertHammerly2026.value p false = (HalpertHammerly2026.feature p)ᶜ

theorem HalpertHammerly2026.value_ordConnected (p : Primitive) (b : Bool) : (value p b).OrdConnected

@[reducible, inline]

abbrev HalpertHammerly2026.Spec : Type

A specification, the value, if any, of each feature.

Equations

• HalpertHammerly2026.Spec = (HalpertHammerly2026.Primitive → Option Bool)

def HalpertHammerly2026.category (s : Spec) : Set Primitive

The category a specification defines, the intersection of the values it specifies ((4), (5)); a feature left unspecified is conflated.

Equations

• HalpertHammerly2026.category s = ⋂ (p : HalpertHammerly2026.Primitive), ⋂ b ∈ s p, HalpertHammerly2026.value p b

theorem HalpertHammerly2026.mem_category {s : Spec} {x : Primitive} : x ∈ category s ↔ ∀ (p : Primitive) (b : Bool), s p = some b → (x ≤ p ↔ b = true)

theorem HalpertHammerly2026.category_ordConnected (s : Spec) : (category s).OrdConnected

Feature-definable categories are order-convex.

theorem HalpertHammerly2026.animal_mem_category {s : Spec} (h₁ : Primitive.human ∈ category s) (h₂ : Primitive.force ∈ category s) : Primitive.animal ∈ category s

No category encompasses non-interlocutor humans and natural forces to the exclusion of animals, the impossible conflation of section 2.

def HalpertHammerly2026.contrast (p : Primitive) : Spec

The full specification singling out a primitive (4), positive on every feature at or above it and negative on every feature below it.

Equations

• HalpertHammerly2026.contrast p q = some (decide (p ≤ q))

theorem HalpertHammerly2026.category_contrast (p : Primitive) : category (contrast p) = {p}

At the limit each primitive defines its own category, the leaves of the contrastive hierarchy (4).

Core noun classes, (19) and (22)

inductive HalpertHammerly2026.AnimacyFeature : Type

The bivalent features [±Animate, ±Human] of a Bantu nominalizing head (19), [+Human] entailing [+Animate].

• animate : AnimacyFeature
• human : AnimacyFeature

@[instance_reducible]

instance HalpertHammerly2026.instDecidableEqAnimacyFeature : DecidableEq AnimacyFeature

Equations

• HalpertHammerly2026.instDecidableEqAnimacyFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def HalpertHammerly2026.instReprAnimacyFeature.repr : AnimacyFeature → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance HalpertHammerly2026.instReprAnimacyFeature : Repr AnimacyFeature

Equations

• HalpertHammerly2026.instReprAnimacyFeature = { reprPrec := HalpertHammerly2026.instReprAnimacyFeature.repr }

@[instance_reducible]

instance HalpertHammerly2026.instFintypeAnimacyFeature : Fintype AnimacyFeature

Equations

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

def HalpertHammerly2026.AnimacyFeature.rank : AnimacyFeature → Fin 2

Position on the dependency chain, animate below human.

Equations

• HalpertHammerly2026.AnimacyFeature.animate.rank = 0
• HalpertHammerly2026.AnimacyFeature.human.rank = 1

@[instance_reducible]

instance HalpertHammerly2026.instLinearOrderAnimacyFeature : LinearOrder AnimacyFeature

Equations

• HalpertHammerly2026.instLinearOrderAnimacyFeature = LinearOrder.lift' HalpertHammerly2026.AnimacyFeature.rank HalpertHammerly2026.instLinearOrderAnimacyFeature._proof_1

@[reducible, inline]

abbrev HalpertHammerly2026.AnimacyFeatures : Type

The features of a nominalizing head, its positive ones.

Equations

• HalpertHammerly2026.AnimacyFeatures = Finset HalpertHammerly2026.AnimacyFeature

@[reducible, inline]

abbrev HalpertHammerly2026.AnimacyFeatures.WellFormed (af : AnimacyFeatures) : Prop

A specification is coherent when [+Human] entails [+Animate] (footnote 10).

Equations

• af.WellFormed = IsLowerSet ↑af

def HalpertHammerly2026.AnimacyFeatures.spec (af : AnimacyFeatures) : Spec

The features as a specification of the [Animate] and [Human] features of (3).

Equations

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

theorem HalpertHammerly2026.AnimacyFeatures.category_spec_eq_empty_iff (af : AnimacyFeatures) : category af.spec = ∅ ↔ ¬af.WellFormed

The incoherent combination is the one denoting no primitive at all.

@[reducible, inline]

abbrev HalpertHammerly2026.Core : Type

A core noun class (19), a coherent specification of [±Animate, ±Human].

Equations

• HalpertHammerly2026.Core = { af : HalpertHammerly2026.AnimacyFeatures // af.WellFormed }

def HalpertHammerly2026.Core.human : Core

HUMAN, [+Animate, +Human].

Equations

• HalpertHammerly2026.Core.human = ⟨{HalpertHammerly2026.AnimacyFeature.animate, HalpertHammerly2026.AnimacyFeature.human}, HalpertHammerly2026.Core.human._proof_1⟩

def HalpertHammerly2026.Core.animal : Core

ANIMATE, [+Animate, −Human].

Equations

• HalpertHammerly2026.Core.animal = ⟨{HalpertHammerly2026.AnimacyFeature.animate}, HalpertHammerly2026.Core.animal._proof_1⟩

def HalpertHammerly2026.Core.inanimate : Core

INANIMATE, [−Animate, −Human].

Equations

• HalpertHammerly2026.Core.inanimate = ⟨∅, HalpertHammerly2026.Core.inanimate._proof_1⟩

theorem HalpertHammerly2026.Core.category_spec_human : category (↑human).spec = Set.Iic Primitive.human

HUMAN denotes every primitive down to the local persons, so the class contains the speech-act participants, the containment behind their reduction to class 1/2 ((8), (10)).

theorem HalpertHammerly2026.Core.category_spec_inanimate : category (↑inanimate).spec = Set.Ioi Primitive.animal

INANIMATE is the conflation of natural forces, concrete things, and abstract things, the GENERIC INANIMATE of (5).

def HalpertHammerly2026.Core.ofAnimacy : Reference.Animacy → Core

The core class of a referent of a given animacy.

Equations

• HalpertHammerly2026.Core.ofAnimacy Reference.Animacy.human = HalpertHammerly2026.Core.human
• HalpertHammerly2026.Core.ofAnimacy Reference.Animacy.animate = HalpertHammerly2026.Core.animal
• HalpertHammerly2026.Core.ofAnimacy Reference.Animacy.inanimate = HalpertHammerly2026.Core.inanimate

def HalpertHammerly2026.Core.gender (c : Core) : Xhosa.Gender

In Xhosa (19), HUMAN is class 1/2, ANIMATE class 9/10, and INANIMATE class 7/8.

Equations

• c.gender = if HalpertHammerly2026.AnimacyFeature.human ∈ ↑c then Xhosa.Gender.genderA else if HalpertHammerly2026.AnimacyFeature.animate ∈ ↑c then Xhosa.Gender.genderE else Xhosa.Gender.genderD

def HalpertHammerly2026.Core.ofGender (g : Xhosa.Gender) : Option Core

The core class of a gender, read off the semantic core the fragment records for it; none for a purely formal gender.

Equations

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

theorem HalpertHammerly2026.Core.ofGender_gender (c : Core) : ofGender c.gender = some c

The classes of (19) agree with the fragment's semantic cores, the gender a core class is spelled out in bearing that core.

theorem HalpertHammerly2026.Core.gender_eq_of_ofGender {g : Xhosa.Gender} {c : Core} (h : ofGender g = some c) : c.gender = g

inductive HalpertHammerly2026.Core.FinalVowel : Type

The nominalizing final vowels (22).

• i : FinalVowel
• o : FinalVowel

@[instance_reducible]

instance HalpertHammerly2026.Core.instDecidableEqFinalVowel : DecidableEq FinalVowel

Equations

• HalpertHammerly2026.Core.instDecidableEqFinalVowel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HalpertHammerly2026.Core.instReprFinalVowel : Repr FinalVowel

Equations

• HalpertHammerly2026.Core.instReprFinalVowel = { reprPrec := HalpertHammerly2026.Core.instReprFinalVowel.repr }

def HalpertHammerly2026.Core.instReprFinalVowel.repr : FinalVowel → ℕ → Std.Format

Equations

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

def HalpertHammerly2026.Core.finalVowel (c : Core) : FinalVowel

By (22) the core n is spelled out as -i when [+Human] and as -o otherwise.

Equations

• c.finalVowel = if HalpertHammerly2026.AnimacyFeature.human ∈ ↑c then HalpertHammerly2026.Core.FinalVowel.i else HalpertHammerly2026.Core.FinalVowel.o

theorem HalpertHammerly2026.Core.finalVowel_eq_i_iff (c : Core) : c.finalVowel = FinalVowel.i ↔ c.gender = Xhosa.Gender.genderA

At the core, -i is exactly class 1/2, so the 73% of Chichewa -i nouns in class 1 reported in section 4.1 are the aligned nominals and the rest are stacked.

theorem HalpertHammerly2026.Core.eq_of_factorsThrough_animate {β : Type u_1} {f : Core → β} (hf : Function.FactorsThrough f fun (x : Core) => decide (AnimacyFeature.animate ∈ ↑x)) : f human = f animal

An exponent conditioned on [±Animate] alone, as Swahili's class 1/2 agreement under animacy override (13), treats humans and animals alike, the GENERIC ANIMATE conflation of (5).

theorem HalpertHammerly2026.Core.not_factorsThrough_gender : ¬Function.FactorsThrough gender fun (x : Core) => decide (AnimacyFeature.animate ∈ ↑x)

Xhosa's core genders distinguish [±Human] within [+Animate].

def HalpertHammerly2026.Core.pluralSubjPrefix (c : Core) : String

The plural subject marker of a core class's gender.

Equations

• c.pluralSubjPrefix = c.gender.pluralClass.subjPrefix

theorem HalpertHammerly2026.Core.pluralSubjPrefix_factorsThrough : Function.FactorsThrough pluralSubjPrefix fun (x : Core) => decide (AnimacyFeature.human ∈ ↑x)

Xhosa's class 8 and class 10 subject markers are both zi- (footnote 7), since the plural marker is conditioned on [±Human] alone and ANIMATE and INANIMATE share it.

Local persons

def HalpertHammerly2026.personSpec (pf : Person.Features) : Spec

The person features [±Participant, ±Author] as a specification of (3).

Equations

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

theorem HalpertHammerly2026.category_personSpec_subset {pf : Person.Features} (h : Person.Feature.participant ∈ pf) : category (personSpec pf) ⊆ category (↑Core.human).spec

Local persons are a more highly specified subset of HUMAN (section 3.2). A participant's category lies inside the core class, so a probe for class 1/2 finds them, as Lubukusu alternative agreement (8) and Zulu person reduction (10) show.

Stacked nominals, (26) to (29)

A nominal is [Car26]'s stacked nominal over the core classes: the core n beneath an optional secondary n with a class feature of its own ((27), (28)). An aligned noun's secondary n bears none and is spelled out by the core.

def HalpertHammerly2026.prefixGender (n : Carstens2026.Nominal Core) : Xhosa.Gender

The class prefix, the allomorph of the outermost n (27).

Equations

• HalpertHammerly2026.prefixGender n = n.visible.gender

def HalpertHammerly2026.ofEntry (e : Xhosa.Noun) : Option (Carstens2026.Nominal Core)

The nominal of a Xhosa noun (28), with the core from the entity denoted and a secondary n bearing the features of the noun's gender when that is a core class other than the core's. It is undefined for the genders whose features the paper leaves open.

Equations

• HalpertHammerly2026.ofEntry e = Option.map (Carstens2026.Nominal.stack (HalpertHammerly2026.Core.ofAnimacy e.animacy)) (HalpertHammerly2026.Core.ofGender e.gender)

theorem HalpertHammerly2026.prefixGender_eq_gender {e : Xhosa.Noun} {n : Carstens2026.Nominal Core} (h : ofEntry e = some n) : prefixGender n = e.gender

The prefix class of a nominal is the noun's gender.

theorem HalpertHammerly2026.ofEntry_isikhohleli : ofEntry Xhosa.Nouns.isikhohleli = some { core := Core.human, outer := some Core.inanimate }

In (28) isikhohleli 'coughing person' is a human core under a class 7 secondary n, its final vowel the animate -i and its prefix class 7.

theorem HalpertHammerly2026.ofEntry_aligned : ofEntry Xhosa.Nouns.umkhohleli = some { core := Core.human } ∧ ofEntry Xhosa.Nouns.isikhohlela = some { core := Core.inanimate }

In (27a) and (27c) umkhohleli 'coughing person' and isikhohlela 'phlegm' are aligned, the prefix class the core's own.

def HalpertHammerly2026.flat : Minimalist.Probe Core

The flat ɸ probe of (29a), to which any n is visible.

Equations

• HalpertHammerly2026.flat = Minimalist.Probe.indiscriminate

def HalpertHammerly2026.animateProbe : Minimalist.Probe Core

The ɸ probe of (29b), relativized to [+Animate].

Equations

• HalpertHammerly2026.animateProbe = Minimalist.Probe.relativized fun (x : HalpertHammerly2026.Core) => decide (HalpertHammerly2026.AnimacyFeature.animate ∈ ↑x)

def HalpertHammerly2026.agreement (p : Minimalist.Probe Core) (n : Carstens2026.Nominal Core) : Option Xhosa.Gender

The gender a probe agrees in, the allomorph of the n it finds searching from the top.

Equations

• HalpertHammerly2026.agreement p n = Option.map HalpertHammerly2026.Core.gender (p.search n.genders.reverse)

theorem HalpertHammerly2026.agreement_flat (n : Carstens2026.Nominal Core) : agreement flat n = some (prefixGender n)

In Zulu a flat probe finds the outermost n, so agreement tracks the prefix class (29a).

theorem HalpertHammerly2026.animateProbe_search {n : Carstens2026.Nominal Core} (hc : AnimacyFeature.animate ∈ ↑n.core) (hs : ∀ s ∈ n.outer, AnimacyFeature.animate ∉ ↑s) : animateProbe.search n.genders.reverse = some n.core

In Swahili, with an inanimate secondary n over an animate core as in (28), the relativized probe searches past the secondary n to the core (29b).

theorem HalpertHammerly2026.agreement_animateProbe {n : Carstens2026.Nominal Core} (hc : AnimacyFeature.animate ∈ ↑n.core) (hs : ∀ s ∈ n.outer, AnimacyFeature.animate ∉ ↑s) : agreement animateProbe n = some n.core.gender

Under animacy override ((11), (13)) the relativized probe agrees with the core class.

theorem HalpertHammerly2026.animateProbe_outcome (c : Core) : animateProbe.outcome { core := c }.genders.reverse = Minimalist.Probe.Outcome.valued ↔ AnimacyFeature.animate ∈ ↑c

In Nyaturu object doubling (14) an object probe relativized to [+Animate] is valued by an aligned noun iff its core is animate, so an inanimate object leaves it unvalued and no object marker surfaces.

theorem HalpertHammerly2026.isikhohleli_agreement : (ofEntry Xhosa.Nouns.isikhohleli).bind (agreement flat) = some Xhosa.Gender.genderD ∧ (ofEntry Xhosa.Nouns.isikhohleli).bind (agreement animateProbe) = some Xhosa.Gender.genderA

By (28) and (29) isikhohleli agrees in class 7 with a flat probe and in class 1 with the relativized one.