Akan (Kwa) Determiners

@cite{zimmermann-2026} @cite{owusu-2022} @cite{bombi-2018} @cite{philipp-2022}

Fragment entries for the Akan (Kwa, Niger-Congo) determiner system, covering definiteness markers, indefinites, and universal quantifiers.

Definiteness

Akan has an overt DEF-marker nó whose analysis is disputed:

Analysis	Source	DefPresupType
Strong (familiarity)	@cite{schwarz-2013}	familiarity
Weak (uniqueness)	@cite{bombi-2018}	uniqueness
Demonstrative	@cite{owusu-2022}	familiarity + ¬uniq

All analyses agree that bare NPs (without nó) can receive definite readings in Akan, making Akan a WeakArticleStrategy.bareNominal language. The bare NP handles uniqueness-based definiteness covertly, while nó overtly marks familiarity.

Key empirical facts (@cite{owusu-2022}, @cite{zimmermann-2026} §3.1):

• nó is infelicitous with globally unique NPs (ewia 'sun') → ¬uniqueness
• nó requires a discourse-familiar antecedent → familiarity
• nó is obligatory in larger-situation contexts (ex. 4a) → previous reference

Indefiniteness

Akan bí is analysed as a skolemized choice function by @cite{owusu-2022}, explaining its obligatory wide scope under negation. Hausa wani/wata by contrast is an ∃-quantifier with flexible scope. This contrast provides cross-linguistic evidence for the choice function vs ∃-quantifier distinction that English alone cannot disambiguate.

Universal Quantification

Akan bi-ara shows flexible interpretation: universal (✓every), NPI (✓nobody), and free choice (✓any), depending on structural context. @cite{philipp-2022} proposes a structural ambiguity account via the alternative-sensitive scalar operator ara.

inductive Fragments.Akan.Determiners.NoAnalysis : Type

Analysis options for Akan nó, reflecting the current debate. @cite{zimmermann-2026} §3.1 surveys all three positions.

• strong : NoAnalysis
• weak : NoAnalysis
• demonstrative : NoAnalysis

@[implicit_reducible]

instance Fragments.Akan.Determiners.instDecidableEqNoAnalysis : DecidableEq NoAnalysis

Equations

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

def Fragments.Akan.Determiners.instReprNoAnalysis.repr : NoAnalysis → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Akan.Determiners.instReprNoAnalysis : Repr NoAnalysis

Equations

• Fragments.Akan.Determiners.instReprNoAnalysis = { reprPrec := Fragments.Akan.Determiners.instReprNoAnalysis.repr }

def Fragments.Akan.Determiners.NoAnalysis.toPresupType : NoAnalysis → Features.Definiteness.DefPresupType

Each analysis predicts a different presupposition type.

Equations

• Fragments.Akan.Determiners.NoAnalysis.strong.toPresupType = Features.Definiteness.DefPresupType.familiarity
• Fragments.Akan.Determiners.NoAnalysis.weak.toPresupType = Features.Definiteness.DefPresupType.uniqueness
• Fragments.Akan.Determiners.NoAnalysis.demonstrative.toPresupType = Features.Definiteness.DefPresupType.familiarity

def Fragments.Akan.Determiners.preferredAnalysis : NoAnalysis

Bombi's (2018) uniqueness-based analysis captures the most empirical data: it explains why nó occurs on non-uniquely-referring NPs (in familiarity contexts where uniqueness is evaluated against the context of a preceding clause), the different distribution of nó and demonstrative saa...nó, and the non-occurrence on proper names. @cite{zimmermann-2026} §3.1 concludes Bombi's analysis fares better than Owusu's demonstrative analysis.

Equations

• Fragments.Akan.Determiners.preferredAnalysis = Fragments.Akan.Determiners.NoAnalysis.weak

def Fragments.Akan.Determiners.noSem {E : Type} (dc : Semantics.Definiteness.DiscourseContext E) (restrictor scope : E → Bool) : Core.Presupposition.PrProp Unit

⟦nó⟧ under the familiarity analysis: presupposes a unique salient discourse referent matching the restrictor.

Built from the canonical presupOfReferent combinator with russellIotaList over the discourse-salient domain — familiarity is encoded as domain restriction (searching dc.salient instead of the full domain).

Under Bombi's preferred uniqueness analysis, the same denotation applies but evaluated against a discourse-restricted situation rather than the full evaluation world.

Equations

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

inductive Fragments.Akan.Determiners.BareNPReading : Type

Akan bare NP interpretation depends on context:

• Globally unique NPs (ewia 'sun'): definite reading without nó → covert uniqueness-based iota
• Non-singleton-denoting NPs: indefinite / ∃-quantifier reading → covert ∃ or type-shift

@cite{owusu-2022}, @cite{philipp-2022}. Akan is classified as WeakArticleStrategy.bareNominal in Features/Definiteness.lean.

• definite : BareNPReading
• indefinite : BareNPReading

@[implicit_reducible]

instance Fragments.Akan.Determiners.instDecidableEqBareNPReading : DecidableEq BareNPReading

Equations

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

def Fragments.Akan.Determiners.instReprBareNPReading.repr : BareNPReading → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Akan.Determiners.instReprBareNPReading : Repr BareNPReading

Equations

• Fragments.Akan.Determiners.instReprBareNPReading = { reprPrec := Fragments.Akan.Determiners.instReprBareNPReading.repr }

def Fragments.Akan.Determiners.bareNPIndefType : Semantics.Quantification.ChoiceFunction.IndefType

When a bare NP gets an indefinite reading, it is a covert ∃-quantifier — hence narrow scope only.

Equations

• Fragments.Akan.Determiners.bareNPIndefType = Semantics.Quantification.ChoiceFunction.IndefType.existential

def Fragments.Akan.Determiners.biIndefType : Semantics.Quantification.ChoiceFunction.IndefType

bí is analysed as a choice function, not an ∃-quantifier. @cite{owusu-2022}, following @cite{mirrazi-2024}.

Equations

• Fragments.Akan.Determiners.biIndefType = Semantics.Quantification.ChoiceFunction.IndefType.choiceFunction

def Fragments.Akan.Determiners.biSem (S : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

⟦bí⟧ = λs.λP. CH(f_s). f_s(P(s))

@cite{owusu-2022} analyses bí as denoting a skolemized choice function with individual and world/situation indices.

The choice function f_s selects a single individual of type e from the set of P-individuals in situation s. The key consequence: since negation is not an intensional operator, it cannot shift the situation argument, so bí-NPs always take wide scope over negation.

⟦Me-n-ni fish bí⟧ = ¬eat(speaker, f_s(fish)) = 'I don't eat a certain (kind of) fish' (∃ > ¬) ≠ 'I don't eat any fish' (*¬ > ∃)

@cite{zimmermann-2026} §3.3 exx. (15–16).

Equations

• Fragments.Akan.Determiners.biSem S E = Semantics.Quantification.ChoiceFunction.SkolemCF S E

inductive Fragments.Akan.Determiners.BiaraReading : Type

bi-ara exhibits flexible surface interpretations depending on its structural environment. @cite{philipp-2022} proposes that the three readings arise from different structural combinations of the INDEF marker bí and the alternative-sensitive scalar operator ara:

• INDEF + ara at NP level → universal (✓every)
• INDEF + ara at clause level → NPI (nobody) / FC (any)

@cite{zimmermann-2026} §4.1.2 ex. (27).

• universal : BiaraReading
• npi : BiaraReading
• freeChoice : BiaraReading

@[implicit_reducible]

instance Fragments.Akan.Determiners.instDecidableEqBiaraReading : DecidableEq BiaraReading

Equations

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

def Fragments.Akan.Determiners.instReprBiaraReading.repr : BiaraReading → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Akan.Determiners.instReprBiaraReading : Repr BiaraReading

Equations

• Fragments.Akan.Determiners.instReprBiaraReading = { reprPrec := Fragments.Akan.Determiners.instReprBiaraReading.repr }

theorem Fragments.Akan.Determiners.bi_is_cf : biIndefType = Semantics.Quantification.ChoiceFunction.IndefType.choiceFunction

bí is a choice function indefinite. @cite{owusu-2022}, @cite{zimmermann-2026} §3.3 ex. (15).

theorem Fragments.Akan.Determiners.bareNP_is_existential : bareNPIndefType = Semantics.Quantification.ChoiceFunction.IndefType.existential

Bare NPs are ∃-quantifier indefinites.

theorem Fragments.Akan.Determiners.strong_presup_familiarity : NoAnalysis.strong.toPresupType = Features.Definiteness.DefPresupType.familiarity

Strong analysis of nó predicts familiarity presupposition. @cite{schwarz-2013}.

theorem Fragments.Akan.Determiners.demonstrative_presup_familiarity : NoAnalysis.demonstrative.toPresupType = Features.Definiteness.DefPresupType.familiarity

Demonstrative analysis of nó also predicts familiarity. @cite{owusu-2022}.

def Fragments.Akan.Determiners.akanArticleStrategy : Features.Definiteness.WeakArticleStrategy

Akan's article system: overt DEF marker (nó) for familiarity, bare NP for uniqueness-based definiteness. This is the reverse of English (one overt form for both) and German (two overt forms). @cite{schwarz-2013}, @cite{zimmermann-2026} §3.1.

Equations

• Fragments.Akan.Determiners.akanArticleStrategy = Features.Definiteness.WeakArticleStrategy.bareNominal