Halpert & Hammerly 2026: Reconciling Animacy and Noun Class in Bantu

@cite{halpert-hammerly-2026}

Halpert, Claire & Hammerly, Christopher. 2026. Reconciling animacy and noun class in Bantu. Glossa: a journal of general linguistics 11(1). 1--25.

Core claims

1. Core Noun Class Hypothesis (19): All Bantu nouns are underlyingly specified for one of three core noun classes based on features [±Animate] and [±Human] from @cite{hammerly-2023}'s containment hierarchy: HUMAN [+Anim, +Hum] ≈ cl 1/2, NON-HUMAN ANIMATE [+Anim, −Hum] ≈ cl 9/10, INANIMATE [−Anim, −Hum] ≈ cl 7/8.

2. Containment unification: Person features [±Author, ±Participant] and animacy features [±Human, ±Animate] are part of the same containment hierarchy (3)–(4): [Auth] ⊂ [Part] ⊂ [Hum] ⊂ [Anim].

3. Final vowels (22): Core noun class is morphophonologically encoded by the nominalizing final vowel: n[+Anim, +Hum] ↔ -i, n[_, −Hum] ↔ -o.

4. nP stacking (26): A secondary n wraps the core nP, creating mismatches between the class prefix (secondary) and the core noun class (accessible to agreement).

5. Probe articulation (29): Cross-Bantu variation in animacy effects follows from probe sensitivity — flat φ-probes target n_secondary (Zulu), while probes relativized to [+Animate] search past n_secondary to n_core (Swahili).

Empirical phenomena

• Alternative agreement / anti-agreement in Lubukusu (8)–(9)
• Animacy override in Chiyao (11)–(12), Swahili (13)
• Object doubling conditioned by animacy in Nyaturu (14)
• Agreement convergence with conjoined nouns in Xhosa (18)

Relationship to Carstens 2026

@cite{halpert-hammerly-2026} and @cite{carstens-2026} converge on nP stacking and the three-way core noun class split, but differ on the theoretical grounding: H&H derive core classes from @cite{hammerly-2023}'s containment-type features [±Animate, ±Human] and propose final vowels as their morphophonological locus. Carstens rejects a grammaticalized animacy hierarchy (fn. 12). The AnimacyFeatures type in Bantu/Params.lean formalizes H&H's feature system; SemanticCore (shared with Carstens) is derived from it via AnimacyFeatures.toCoreClass.

Integration

• AnimacyFeatures instantiates Features.PhiFeatures (same PrivativePair as person features), connecting person and animacy containment
• AnimacyFeatures.toAnimacyLevel bridges to the Features.Prominence hierarchy used throughout the codebase
• impossible_human_inanimate_without_animal proves the conflation impossibility predicted by containment
• AnimacyFeatures.toGenderFeature bridges to @cite{kramer-2015}'s GenderFeature type on the n-head
• Cross-references: Carstens2026.lean (convergence data), Kramer2020.lean (n-head typology)

structure HalpertHammerly2026.ProminenceFeatures : Type

The full prominence hierarchy from @cite{hammerly-2023} (3): [Auth] ⊂ [Part] ⊂ [Hum] ⊂ [Anim] ⊂ [Agent] ⊂ [Indiv] ⊂ φ.

This structure encodes the four innermost features. Person features [±Author, ±Participant] are nested inside animacy features [±Human, ±Animate].

• isAnimate : Bool
• isHuman : Bool
• hasParticipant : Bool
• hasAuthor : Bool

@[implicit_reducible]

instance HalpertHammerly2026.instDecidableEqProminenceFeatures : DecidableEq ProminenceFeatures

Equations

• HalpertHammerly2026.instDecidableEqProminenceFeatures = HalpertHammerly2026.instDecidableEqProminenceFeatures.decEq

def HalpertHammerly2026.instDecidableEqProminenceFeatures.decEq (x✝ x✝¹ : ProminenceFeatures) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance HalpertHammerly2026.instReprProminenceFeatures : Repr ProminenceFeatures

Equations

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

def HalpertHammerly2026.instReprProminenceFeatures.repr : ProminenceFeatures → ℕ → Std.Format

Equations

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

def HalpertHammerly2026.ProminenceFeatures.wellFormed (pf : ProminenceFeatures) : Bool

Well-formedness enforces the full containment chain: [+Author] → [+Participant] → [+Human] → [+Animate].

Equations

• pf.wellFormed = ((!pf.hasAuthor || pf.hasParticipant) && (!pf.hasParticipant || pf.isHuman) && (!pf.isHuman || pf.isAnimate))

def HalpertHammerly2026.ProminenceFeatures.personFeatures (pf : ProminenceFeatures) : Features.Person.Features

Extract the person projection.

Equations

• pf.personFeatures = { hasParticipant := pf.hasParticipant, hasAuthor := pf.hasAuthor }

def HalpertHammerly2026.ProminenceFeatures.animacyFeatures (pf : ProminenceFeatures) : Fragments.Bantu.AnimacyFeatures

Extract the animacy projection.

Equations

• pf.animacyFeatures = { isAnimate := pf.isAnimate, isHuman := pf.isHuman }

theorem HalpertHammerly2026.participant_implies_human (pf : ProminenceFeatures) (hw : pf.wellFormed = true) (hp : pf.hasParticipant = true) : pf.isHuman = true

The containment chain predicts: speech-act participants are human. [+Participant] → [+Human] (@cite{halpert-hammerly-2026} (3)–(4)).

theorem HalpertHammerly2026.participant_implies_animate (pf : ProminenceFeatures) (hw : pf.wellFormed = true) (hp : pf.hasParticipant = true) : pf.isAnimate = true

The containment chain predicts: speech-act participants are animate. [+Participant] → [+Human] → [+Animate].

theorem HalpertHammerly2026.first_person_is_human_animate (pf : ProminenceFeatures) : pf.wellFormed = true → pf.hasAuthor = true → pf.isHuman = true ∧ pf.isAnimate = true

First person is necessarily human and animate.

theorem HalpertHammerly2026.person_animacy_same_structure : (Features.PhiFeatures.toPair Features.Person.first).wellFormed = true ∧ (Features.PhiFeatures.toPair Fragments.Bantu.AnimacyFeatures.human).wellFormed = true ∧ (Features.PhiFeatures.toPair Features.Person.third).wellFormed = true ∧ (Features.PhiFeatures.toPair Fragments.Bantu.AnimacyFeatures.inanimate).wellFormed = true

Person and animacy features share the PrivativePair structure. Both Features.Person.Features and AnimacyFeatures are PhiFeatures instances — the same three-cell, no-four-way-distinction architecture. This is not a coincidence: they are fragments of the same containment hierarchy (@cite{hammerly-2023}).

theorem HalpertHammerly2026.core_noun_class_hypothesis : Fragments.Bantu.AnimacyFeatures.human.toCoreClass = Fragments.Bantu.SemanticCore.human ∧ Fragments.Bantu.AnimacyFeatures.animal.toCoreClass = Fragments.Bantu.SemanticCore.animal ∧ Fragments.Bantu.AnimacyFeatures.inanimate.toCoreClass = Fragments.Bantu.SemanticCore.inanimate

The Core Noun Class Hypothesis (19): the three well-formed feature combinations map exactly to the three core classes.

theorem HalpertHammerly2026.xhosa_core_classes : Option.map Fragments.Bantu.SemanticCore.toFeatures Fragments.Xhosa.Gender.genderA.status.core = some Fragments.Bantu.AnimacyFeatures.human ∧ Option.map Fragments.Bantu.SemanticCore.toFeatures Fragments.Xhosa.Gender.genderD.status.core = some Fragments.Bantu.AnimacyFeatures.inanimate ∧ Option.map Fragments.Bantu.SemanticCore.toFeatures Fragments.Xhosa.Gender.genderE.status.core = some Fragments.Bantu.AnimacyFeatures.animal

The feature decomposition of Xhosa's three interpretable genders matches H&H's core noun class features.

theorem HalpertHammerly2026.xhosa_no_core : Fragments.Xhosa.Gender.genderB.status.core = none ∧ Fragments.Xhosa.Gender.genderC.status.core = none

Xhosa's uninterpretable genders have no core feature decomposition.

theorem HalpertHammerly2026.core_classes_match_prominence : Fragments.Bantu.AnimacyFeatures.human.toAnimacyLevel = Features.Prominence.AnimacyLevel.human ∧ Fragments.Bantu.AnimacyFeatures.animal.toAnimacyLevel = Features.Prominence.AnimacyLevel.animate ∧ Fragments.Bantu.AnimacyFeatures.inanimate.toAnimacyLevel = Features.Prominence.AnimacyLevel.inanimate

The three core noun classes match the three animacy levels used throughout the codebase (bridging H&H's features to differential argument marking, Corbett/Smith-Stark scales, etc.).

inductive HalpertHammerly2026.LubukusuSM : Type

Lubukusu alternative agreement (8)–(9): local persons and class 1 nouns all trigger the same AA morpheme o- under A-bar extraction, while other classes (e.g. class 7) retain their standard SM.

This follows from containment: local persons have [+Participant], which entails [+Human] via the prominence hierarchy. Class 1 nouns have [+Human] directly. A probe targeting [+Human] treats them identically. Class 7 lacks [+Human] and so uses a different (unchanged) marker.

• a : LubukusuSM
• o : LubukusuSM
• sy : LubukusuSM

@[implicit_reducible]

instance HalpertHammerly2026.instDecidableEqLubukusuSM : DecidableEq LubukusuSM

Equations

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

def HalpertHammerly2026.instReprLubukusuSM.repr : LubukusuSM → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HalpertHammerly2026.instReprLubukusuSM : Repr LubukusuSM

Equations

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

structure HalpertHammerly2026.AAPattern : Type

Subject marker pair: declarative context vs A-bar extraction.

• declarative : LubukusuSM
• extraction : LubukusuSM

@[implicit_reducible]

instance HalpertHammerly2026.instDecidableEqAAPattern : DecidableEq AAPattern

Equations

• HalpertHammerly2026.instDecidableEqAAPattern = HalpertHammerly2026.instDecidableEqAAPattern.decEq

def HalpertHammerly2026.instDecidableEqAAPattern.decEq (x✝ x✝¹ : AAPattern) : Decidable (x✝ = x✝¹)

Equations

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

def HalpertHammerly2026.instReprAAPattern.repr : AAPattern → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance HalpertHammerly2026.instReprAAPattern : Repr AAPattern

Equations

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

def HalpertHammerly2026.lubukusu_class1 : AAPattern

Equations

• HalpertHammerly2026.lubukusu_class1 = { declarative := HalpertHammerly2026.LubukusuSM.a, extraction := HalpertHammerly2026.LubukusuSM.o }

def HalpertHammerly2026.lubukusu_local_person : AAPattern

Equations

• HalpertHammerly2026.lubukusu_local_person = { declarative := HalpertHammerly2026.LubukusuSM.a, extraction := HalpertHammerly2026.LubukusuSM.o }

def HalpertHammerly2026.lubukusu_class7 : AAPattern

Equations

• HalpertHammerly2026.lubukusu_class7 = { declarative := HalpertHammerly2026.LubukusuSM.sy, extraction := HalpertHammerly2026.LubukusuSM.sy }

theorem HalpertHammerly2026.aa_class1_eq_local : lubukusu_class1 = lubukusu_local_person

Class 1 and local persons share the AA pattern.

theorem HalpertHammerly2026.aa_class7_differs : lubukusu_class1 ≠ lubukusu_class7

Class 7 does NOT show alternative agreement (lacks [+Human]).

theorem HalpertHammerly2026.aa_structural_basis : (∀ (pf : ProminenceFeatures), pf.wellFormed = true → pf.hasParticipant = true → pf.animacyFeatures.isHuman = true) ∧ Fragments.Bantu.AnimacyFeatures.human.isHuman = true

Derivation: AA collapses class 1 and local persons BECAUSE both project [+Human] via PhiFeatures. Local persons have [+Participant], which entails [+Human] (person features are a subset of the animacy hierarchy). Class 1 has [+Human] directly. Both yield the same PrivativePair outer value.

This theorem shows the structural basis: well-formed participants must have [+Human], the same outer feature as class 1.

inductive HalpertHammerly2026.ProbeSensitivity : Type

Probe sensitivity determines whether agreement tracks n_core or n_secondary (@cite{halpert-hammerly-2026} (29)).

• flat: the probe targets the closest φ-features (n_secondary). Agreement always reflects the visible noun class.
• relativized: the probe bears [+Animate] and searches past n_secondary to find [+Animate] on n_core. Agreement reflects core noun class for animate nouns.

This is parameterized per grammatical function: a language may have a flat subject probe but a relativized object probe (Nyaturu).

• flat : ProbeSensitivity
• relativized : ProbeSensitivity

@[implicit_reducible]

instance HalpertHammerly2026.instDecidableEqProbeSensitivity : DecidableEq ProbeSensitivity

Equations

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

@[implicit_reducible]

instance HalpertHammerly2026.instReprProbeSensitivity : Repr ProbeSensitivity

Equations

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

def HalpertHammerly2026.instReprProbeSensitivity.repr : ProbeSensitivity → ℕ → Std.Format

Equations

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

def HalpertHammerly2026.agreementClass (probe : ProbeSensitivity) (stack : Fragments.Bantu.NPStack) : ℕ

Which agreement class surfaces for a given probe and nP stack. Flat probes always return the visible class; relativized probes return the core class when hasAnimateCore is true.

Equations

• HalpertHammerly2026.agreementClass HalpertHammerly2026.ProbeSensitivity.flat stack = stack.visibleClass
• HalpertHammerly2026.agreementClass HalpertHammerly2026.ProbeSensitivity.relativized stack = if stack.hasAnimateCore = true then stack.coreClass else stack.visibleClass

theorem HalpertHammerly2026.zulu_flat_class3_human : agreementClass ProbeSensitivity.flat Fragments.Xhosa.humanInClass3 = 3

Zulu (flat probe): a [human] noun in class 3 gets class 3 agreement.

theorem HalpertHammerly2026.swahili_relativized_human_override : agreementClass ProbeSensitivity.relativized { visibleClass := 7, coreClass := 1, status := Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human } = 1

Swahili (relativized probe): a [human] noun in class 7 gets class 1 agreement — animacy override. This is NOT separately stipulated; it FOLLOWS from agreementClass .relativized + hasAnimateCore.

theorem HalpertHammerly2026.swahili_relativized_animal_override : agreementClass ProbeSensitivity.relativized { visibleClass := 7, coreClass := 9, status := Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.animal } = 9

Swahili (relativized probe): an [animal] noun in class 7 ALSO gets core class agreement — animal override (GENERIC ANIMATE).

theorem HalpertHammerly2026.inanimate_no_override : agreementClass ProbeSensitivity.relativized { visibleClass := 5, coreClass := 7, status := Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.inanimate } = 5

Inanimate nouns are unaffected by relativized probes — probe finds no [+Animate] and falls back to visible class.

theorem HalpertHammerly2026.uninterpretable_always_visible (probe : ProbeSensitivity) (v c : ℕ) : agreementClass probe { visibleClass := v, coreClass := c, status := Fragments.Bantu.GenderStatus.uninterpretable } = v

Uninterpretable genders are always tracked by visible class regardless of probe type.

theorem HalpertHammerly2026.override_from_animate_core (stack : Fragments.Bantu.NPStack) (h : stack.hasAnimateCore = true) : agreementClass ProbeSensitivity.relativized stack = stack.coreClass

Animacy override is a consequence of probe articulation, not a separate parameter. When the core is [+Animate], a relativized probe returns the core class. When it isn't, the probe falls back to the visible class.

theorem HalpertHammerly2026.no_override_without_animate_core (stack : Fragments.Bantu.NPStack) (h : stack.hasAnimateCore = false) : agreementClass ProbeSensitivity.relativized stack = stack.visibleClass

theorem HalpertHammerly2026.convergence_human_to_sm2 : Fragments.Bantu.SemanticCore.human.defaultPluralClass = 2

The default plural agreement class for conjoined singulars is determined by the core noun class, not the visible class. Human conjuncts → SM2, non-human conjuncts → SM8/10. This follows from SemanticCore.defaultPluralClass.

theorem HalpertHammerly2026.convergence_animal_to_sm8 : Fragments.Bantu.SemanticCore.animal.defaultPluralClass = 8

theorem HalpertHammerly2026.convergence_inanimate_to_sm8 : Fragments.Bantu.SemanticCore.inanimate.defaultPluralClass = 8

theorem HalpertHammerly2026.xhosa_human_convergence : Fragments.Bantu.AnimacyFeatures.human.toCoreClass.defaultPluralClass = 2

Xhosa convergence (Table 18): human nouns in ANY class converge to SM2 because all human nouns share core noun class [+Animate, +Human].

theorem HalpertHammerly2026.xhosa_inanimate_convergence : Fragments.Bantu.AnimacyFeatures.inanimate.toCoreClass.defaultPluralClass = 8

Xhosa convergence (Table 18): inanimate nouns in any class converge to SM8 because they share core noun class [−Animate, −Human].

theorem HalpertHammerly2026.canonical_classes_show_expected : Fragments.Xhosa.humanCanonical.isCanonical = true ∧ Fragments.Xhosa.animalCanonical.isCanonical = true ∧ Fragments.Xhosa.humanInClass3.isCanonical = false ∧ Fragments.Xhosa.humanInClass5.isCanonical = false

Table 18 key insight: Classes 1, 7, 9 show EXPECTED agreement (their own plural class), not convergence. This is because these are the canonical classes for the three core noun classes — their visible class IS the core class (isCanonical = true).

Classes 3, 5 are non-canonical for all cores, so nouns in those classes show convergence to the core default instead.

theorem HalpertHammerly2026.noncanonical_converges_to_core : Fragments.Bantu.AnimacyFeatures.human.toCoreClass.defaultPluralClass = 2 ∧ Fragments.Bantu.AnimacyFeatures.human.toCoreClass.defaultPluralClass ≠ 4

Non-canonical nouns converge to core default, not to their visible class's plural. E.g. a [human] noun in class 3 converges to SM2 (core default for human), not SM4 (plural of class 3).

theorem HalpertHammerly2026.sm8_sm10_syncretism : Fragments.Xhosa.NounClass.cl8.subjPrefix = Fragments.Xhosa.NounClass.cl10.subjPrefix

The SM8/SM10 syncretism in Xhosa (both use zi-) follows from the fact that classes 8 and 10 share [−Human] — they differ only in [±Animate], which Xhosa's convergence is insensitive to in this context.

def HalpertHammerly2026.nyaturu_om_allowed (stack : Fragments.Bantu.NPStack) : Bool

Object doubling in Nyaturu (14): animate objects allow (or require) doubling with an object marker on the verb; inanimate objects disallow it. This uses the SAME predicate as animacy override — hasAnimateCore — applied to the object probe, confirming that both phenomena are instances of [+Animate]-relativized probing.

Equations

• HalpertHammerly2026.nyaturu_om_allowed stack = stack.hasAnimateCore

theorem HalpertHammerly2026.nyaturu_human_om : nyaturu_om_allowed { visibleClass := 1, coreClass := 1, status := Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human } = true

theorem HalpertHammerly2026.nyaturu_inanimate_no_om : nyaturu_om_allowed { visibleClass := 7, coreClass := 7, status := Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.inanimate } = false

theorem HalpertHammerly2026.om_and_override_share_predicate (stack : Fragments.Bantu.NPStack) : nyaturu_om_allowed stack = stack.hasAnimateCore ∧ (stack.hasAnimateCore = true → agreementClass ProbeSensitivity.relativized stack = stack.coreClass)

Object doubling and animacy override share the same structural basis: both depend on hasAnimateCore, confirming they are instances of the same [+Animate]-relativized probing mechanism.

def HalpertHammerly2026.toGenderFeature (af : Fragments.Bantu.AnimacyFeatures) : Morphology.DM.GenderFeature

Bridge from H&H's animacy features to @cite{kramer-2015}'s GenderFeature on the categorizing head n.

H&H's AnimacyFeatures encode core noun class via [±Animate, ±Human]. Kramer's framework uses GenderDimension.anim with interpretability. The bridge maps:

• [+Animate] (human or animal) → i[+ANIM] (interpretable animate)
• [−Animate] (inanimate) → i[−ANIM] (interpretable inanimate)

Both systems agree that the n-head bears gender features and that interpretability distinguishes natural from arbitrary gender.

Equations

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

theorem HalpertHammerly2026.human_is_iAnimPos : toGenderFeature Fragments.Bantu.AnimacyFeatures.human = HalpertHammerly2026.iAnimPos✝

theorem HalpertHammerly2026.inanimate_is_iAnimNeg : toGenderFeature Fragments.Bantu.AnimacyFeatures.inanimate = HalpertHammerly2026.iAnimNeg✝

theorem HalpertHammerly2026.core_features_are_interpretable : (toGenderFeature Fragments.Bantu.AnimacyFeatures.human).IsNatural ∧ (toGenderFeature Fragments.Bantu.AnimacyFeatures.animal).IsNatural ∧ (toGenderFeature Fragments.Bantu.AnimacyFeatures.inanimate).IsNatural

All core noun class features yield interpretable gender on n. This matches @cite{kramer-2015}'s prediction that natural gender is always interpretable, and connects H&H's claim that core noun class lives on n to Kramer's n-head architecture.

theorem HalpertHammerly2026.interpretability_alignment : (Fragments.Bantu.GenderStatus.interpretable Fragments.Bantu.SemanticCore.human).isInterpretable = true ∧ Fragments.Bantu.GenderStatus.uninterpretable.isInterpretable = false ∧ HalpertHammerly2026.iAnimPos✝.IsNatural ∧ { interp := Morphology.DM.Interpretability.u, val := { dim := Morphology.DM.GenderDimension.anim, pol := Morphology.DM.Polarity.pos } }.IsArbitrary

H&H's GenderStatus.uninterpretable corresponds to Kramer's arbitrary (u-feature) gender — both encode nouns whose gender is invisible at LF.