Hausa Determiners

@cite{zimmermann-2008} @cite{zimmermann-2014} @cite{zimmermann-2026}

Fragment entries for the Hausa (Chadic, West Africa) determiner system, covering universal quantifiers and indefinite markers.

Universal Quantification

Hausa has a 2-form UQ system (@cite{zimmermann-2008}):

Form	Type	Complement	Reading
koo-wane	[+dist]	SG count without DEF	each
duk(a)	[−dist]	DEF PL count + mass	all

The koo-quantifier shows phi-agreement with the NP and combines only with bare SG count NPs. The duka-expressions do not agree and select for definite plural NPs and mass NPs.

This maps to the Haslinger et al. Q_∀ + ONE decomposition:

• koo-wane = Q_∀[ONE_∅] (distributive, non-overlapping complement)
• duk(a) = bare Q_∀ (non-distributive, CUM complement)

Indefiniteness

Hausa has two indefinite strategies:

Form	Analysis	Scope potential
wani/wata	∃-quantifier	Wide + narrow
bare NP	covert ∃	Narrow only

wani/wata can take exceptional wide scope, even out of relative clauses (@cite{zimmermann-2014}), motivating an analysis as either a contextually bound choice function variable or an ∃-quantifier with singleton restriction (@cite{schwarzschild-2002}).

@cite{zimmermann-2008} @cite{zimmermann-2014} analyse wani/wata as ∃-quantifiers, in complementary distribution with the distributive universal koo-wane/koo-wace.

inductive Fragments.Hausa.Determiners.HausaUQ : Type

Hausa has a 2-form universal quantifier system: koo-wane (distributive) vs duk(a) (non-distributive). @cite{zimmermann-2008}, confirmed by @cite{zimmermann-2026} §4.1.

• koo : HausaUQ
• duk : HausaUQ

@[implicit_reducible]

instance Fragments.Hausa.Determiners.instDecidableEqHausaUQ : DecidableEq HausaUQ

Equations

• Fragments.Hausa.Determiners.instDecidableEqHausaUQ x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Hausa.Determiners.instReprHausaUQ : Repr HausaUQ

Equations

• Fragments.Hausa.Determiners.instReprHausaUQ = { reprPrec := Fragments.Hausa.Determiners.instReprHausaUQ.repr }

def Fragments.Hausa.Determiners.instReprHausaUQ.repr : HausaUQ → ℕ → Std.Format

Equations

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

def Fragments.Hausa.Determiners.HausaUQ.takesSGCount : HausaUQ → Bool

koo shows phi-agreement and takes bare SG count NPs. duk does not agree and takes DEF PL/mass NPs.

Equations

• Fragments.Hausa.Determiners.HausaUQ.koo.takesSGCount = true
• Fragments.Hausa.Determiners.HausaUQ.duk.takesSGCount = false

def Fragments.Hausa.Determiners.HausaUQ.takesDEFPlural : HausaUQ → Bool

Equations

• Fragments.Hausa.Determiners.HausaUQ.koo.takesDEFPlural = false
• Fragments.Hausa.Determiners.HausaUQ.duk.takesDEFPlural = true

def Fragments.Hausa.Determiners.HausaUQ.isDistributive : HausaUQ → Bool

The koo/duk split instantiates the DNG (@cite{haslinger-etal-2025-nllt}): same Q_∀, different complement structure.

Equations

• Fragments.Hausa.Determiners.HausaUQ.koo.isDistributive = true
• Fragments.Hausa.Determiners.HausaUQ.duk.isDistributive = false

def Fragments.Hausa.Determiners.kooSem {α : Type u_1} [PartialOrder α] (P Q : α → Prop) : Prop

⟦koo-wane⟧ = Q_∀[ONE_∅]: distributive universal.

koo-wane distributes over the individual atoms of the SG NP denotation. Because it selects for SG count NPs (atoms only), ONE_∅ (non-overlap) is automatically satisfied.

Equivalent to English every in the Haslinger et al. decomposition. @cite{zimmermann-2008}.

Equations

• Fragments.Hausa.Determiners.kooSem P Q = Semantics.Quantification.ONEModifiers.everyPresup P Q

def Fragments.Hausa.Determiners.dukSem {α : Type u_1} [PartialOrder α] (P Q : α → Prop) : Prop

⟦duk(a)⟧ = bare Q_∀: non-distributive universal.

duk(a) applies the scope predicate to the maximal element of the DEF PL/mass NP denotation (the sum of all individuals).

Equivalent to English all in the Haslinger et al. decomposition. @cite{zimmermann-2008}.

Equations

• Fragments.Hausa.Determiners.dukSem P Q = Semantics.Quantification.UnifiedUniversal.QForall P Q

inductive Fragments.Hausa.Determiners.HausaIndef : Type

Hausa indefinite marker type: bare NP vs wani/wata-marked.

Both are ∃-quantifiers (@cite{zimmermann-2014}). The difference is that wani is an overt ∃ that can QR, while bare NPs have a covert ∃ that is locally bound.

• bare : HausaIndef
• wani : HausaIndef

@[implicit_reducible]

instance Fragments.Hausa.Determiners.instDecidableEqHausaIndef : DecidableEq HausaIndef

Equations

• Fragments.Hausa.Determiners.instDecidableEqHausaIndef x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Hausa.Determiners.instReprHausaIndef : Repr HausaIndef

Equations

• Fragments.Hausa.Determiners.instReprHausaIndef = { reprPrec := Fragments.Hausa.Determiners.instReprHausaIndef.repr }

def Fragments.Hausa.Determiners.instReprHausaIndef.repr : HausaIndef → ℕ → Std.Format

Equations

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

def Fragments.Hausa.Determiners.HausaIndef.indefType : HausaIndef → Semantics.Quantification.ChoiceFunction.IndefType

Both Hausa indefinite strategies use ∃-quantification, not choice functions. @cite{zimmermann-2014}.

Equations

• Fragments.Hausa.Determiners.HausaIndef.bare.indefType = Semantics.Quantification.ChoiceFunction.IndefType.existential
• Fragments.Hausa.Determiners.HausaIndef.wani.indefType = Semantics.Quantification.ChoiceFunction.IndefType.existential

def Fragments.Hausa.Determiners.HausaIndef.isMarkedIndefinite : HausaIndef → Bool

wani/wata satisfies Matthewson's diagnostics for marked indefinites: occurrence in existential sentences, introduction of new discourse referents, serving as antecedents for sluicing. @cite{matthewson-1999}, @cite{zimmermann-2026} §3.3 ex. (12).

Equations

• Fragments.Hausa.Determiners.HausaIndef.bare.isMarkedIndefinite = false
• Fragments.Hausa.Determiners.HausaIndef.wani.isMarkedIndefinite = true

theorem Fragments.Hausa.Determiners.koo_is_distributive : HausaUQ.koo.isDistributive = true

koo-wane is distributive: its complement must be non-overlapping.

theorem Fragments.Hausa.Determiners.duk_is_nondistributive : HausaUQ.duk.isDistributive = false

duk(a) is non-distributive: it applies to the maximal sum.

theorem Fragments.Hausa.Determiners.koo_takes_sg_count : HausaUQ.koo.takesSGCount = true

koo selects SG count NPs (atoms). @cite{zimmermann-2008}, @cite{haslinger-etal-2025-nllt}.

theorem Fragments.Hausa.Determiners.duk_takes_def_plural : HausaUQ.duk.takesDEFPlural = true

duk selects DEF PL/mass NPs. @cite{zimmermann-2008}, @cite{haslinger-etal-2025-nllt}.

theorem Fragments.Hausa.Determiners.bare_is_existential : HausaIndef.bare.indefType = Semantics.Quantification.ChoiceFunction.IndefType.existential

Bare NPs are ∃-quantifier indefinites. @cite{zimmermann-2014}.

theorem Fragments.Hausa.Determiners.wani_is_existential : HausaIndef.wani.indefType = Semantics.Quantification.ChoiceFunction.IndefType.existential

wani/wata are ∃-quantifier indefinites. @cite{zimmermann-2014}.