[Zim26]: African Lambdas I — The Nominal Domain

[Zim26] §3.3's comparative claim about marked indefinites: Akan bí and Hausa wani/wata are near-identical in distribution but differ in one decisive respect — under negation wani-NPs scope freely (ex. (13), from [Zim14]) while bí-NPs must outscope negation (ex. (15)). The review concludes the two markers need contrasting analyses — (16a) skolemized choice function for bí ([Owu22], after [Kra98b] and [Mir24]) vs (16b) ∃-quantifier for wani ([Zim08]; cf. [Sch02]) — and that the two-way African comparison discriminates between CF- and ∃-analyses of indefinites where comparison with English alone cannot.

Main declarations

• Akan.Determiners.Indefinite.z2026IndefType, Hausa.Indefinite.z2026IndefType — the review's (16) classification over the two Fragment inventories, discharging the substrate IndefType contrast.
• Zimmermann2026.wani_scopings_diverge — (13): the ∃-analysis' two scopings are truth-conditionally distinct on [Zim08]'s passenger model.
• Zimmermann2026.bi_reading_not_narrow — (15): the CF reading is not the ¬ > ∃ reading on [Owu22]'s two-person model.
• Zimmermann2026.bi_negation_construals_collapse — the review's "negation is not an intensional operator" gloss: extensionality of negation collapses the situation pronoun's bound/free construals.

Implementation notes

Review-anchor discipline: only the comparison the review itself draws is formalized here — the (16) classification and the (13)/(15) scope divergence. The per-language analyses are consumed from their primary sources' formalizations: Studies/Zimmermann2008 (Hausa model, wani_wide_scope, wani_narrow_scope_false) and Studies/Owusu2022 (Akan model, skolemDenot, bi_wide_scope_witnessed, someone_sang).

Todo

• Ga ko (∃-bound CF) vs kome (contextually bound CF) and the no-student datum unattested with English indefinites (§3.3 ex. (17)).
• Bare NPs: obligatory narrow scope in both languages; covert-∃ availability under [Chi98]-style blocking by the overt markers (§3.3–§3.4).
• DEF–INDEF co-occurrence bí nó via [Par87] type-shift of the CF output (§3.4 ex. (18)).
• The DEF-marking landscape of §3.1 (uniqueness ι, familiar nó, demonstrative analyses) — the [Sch13] / [Bom18] / [Owu22] rivalry on the shared Akan entries.

def Akan.Determiners.Indefinite.z2026IndefType : Indefinite → Option Quantification.ChoiceFunction.IndefType

[Zim26] (16a)'s classification of the Akan inventory: bí denotes a skolemized choice function ([Owu22]); bare NPs (obligatory narrow scope) are outside the (16) classification.

Equations

• Akan.Determiners.Indefinite.bi.z2026IndefType = some Quantification.ChoiceFunction.IndefType.choiceFunction
• Akan.Determiners.Indefinite.bare.z2026IndefType = none

def Hausa.Indefinite.z2026IndefType : Indefinite → Option Quantification.ChoiceFunction.IndefType

[Zim26] (16b)'s classification of the Hausa inventory: wani/wata denotes an ∃-quantifier ([Zim08], [Zim14]); bare NPs (obligatory narrow scope) are outside the (16) classification.

Equations

• Hausa.Indefinite.wani.z2026IndefType = some Quantification.ChoiceFunction.IndefType.existential
• Hausa.Indefinite.bare.z2026IndefType = none

theorem Zimmermann2026.wani_scopings_diverge : ¬((¬∃ (x : Zimmermann2008.Faasinjee), Zimmermann2008.Daura x) ↔ Quantification.some_sem (fun (x : Zimmermann2008.Faasinjee) => True) fun (x : Zimmermann2008.Faasinjee) => ¬Zimmermann2008.Daura x)

(13): under the ∃-analysis (16b), the two scopings of wani under negation are truth-conditionally distinct — on [Zim08]'s passenger model the ∃ > ¬ reading holds while ¬ > ∃ fails, so the scopal flexibility of wani is empirically detectable.

theorem Zimmermann2026.bi_reading_not_narrow (d : Intensional.Intension Unit (Owusu2022.Onipa → Prop) → Owusu2022.Onipa) : d ∈ Owusu2022.skolemDenot Owusu2022.preferAma () Akan.Determiners.Indefinite.bi → ¬((¬∃ (x : Owusu2022.Onipa), Owusu2022.ToDwom x) ↔ ¬Owusu2022.ToDwom (d (Intensional.Intension.rigid fun (x : Owusu2022.Onipa) => True)))

(15): the CF analysis (16a) assigns bí under negation a reading distinct from ¬ > ∃ — on [Owu22]'s two-person model the CF reading is true while ¬ > ∃ is false. The interpretive gap that selects (16a) over (16b) for bí.

theorem Zimmermann2026.bi_negation_construals_collapse {S : Type u_1} {E : Type u_2} (f : Quantification.ChoiceFunction.SkolemCF S E) (s₀ : S) (P : Intensional.Intension S (E → Prop)) (VP : E → S → Prop) : (fun (p : S → Prop) (s : S) => ¬p s) (fun (s : S) => VP (f.applyIntensionAt Intensional.SitVarStatus.SitVarStatus.bound s s₀ P) s) s₀ ↔ (fun (p : S → Prop) (s : S) => ¬p s) (fun (s : S) => VP (f.applyIntensionAt Intensional.SitVarStatus.SitVarStatus.free s s₀ P) s) s₀

The review's negation gloss, formalized: "as negation is not an intensional operator, the situational skolem argument of the choice function cannot be shifted away from the actual resource situation … resulting in wide scope only". Pointwise negation is extensional (Intensional.IsExtensionalAt.neg), so by the substrate's bound_free_collapse the bound and free construals of bí's situation pronoun coincide under negation — for any CF and restrictor; the wide (free) construal is the only reading. Situation quantifiers separate the construals (bound_free_diverge_box), so the collapse is negation's extensionality at work, not a triviality.