Documentation

Linglib.Studies.Zimmermann2008

[Zim08]: Quantification in Hausa #

Selected formalization from Zimmermann's handbook chapter in [matthewson-2008], the first formal-semantic treatment of the Hausa quantifier system whose textbook description is given in [New00] and [Jag01]. The two reference grammars fix the inventory typed in Hausa; this file consumes those entries, states Zimmermann's predicted denotations, and checks their consequences on a small concrete model.

Main declarations #

Implementation notes #

z2008Denot extends the Fragment's UniversalQuantifier namespace with Zimmermann 2008's analytical bridge to substrate denotations. The denotation is paper-specific (Z2008 §3.2.5 leaves the choice open between GQ, indeterminate-pronoun, and choice-function); housing it on the Fragment type via the Studies file follows the project pattern of paper-specific methods on consensus typological entries. The denotation for kowWh is everyPresup (Q_∀ + ONE_∅); for duk it is bare QForall on a CUM lattice, but no concrete CUM-lattice model is exhibited here (see Todo).

References #

Todo #

source
def Hausa.UniversalQuantifier.z2008Denot {α : Type u_1} [PartialOrder α] :
UniversalQuantifier → (α → Prop) → (α → Prop) → Prop

[Zim08]'s predicted denotation for each Hausa universal entry, reframed via the [HHR+25] Q_∀ + ONE decomposition. kō-wh receives Q_∀ + ONE_∅ (atom-by-atom distributivity, Jaggar §9.5.1); DUK receives bare Q_∀ on a CUM restrictor (collective single-set scope, Jaggar §9.5.4).

Equations
Instances For

    A 3-passenger SG-count Hausa domain #

    Three passengers (faasinjojî [Jag01] §9.5.4 p.376) — Audù, Bàlki, Càdi — board a plane; Audù and Bàlki buckle their seatbelts, Càdi does not. The minimal SG-count atomic domain on which UniversalQuantifier.kowWh's atom-by-atom predication and Indefinite.wani's scope ambiguity under negation are observable.

    source
    inductive Zimmermann2008.Faasinjee :
    Type

    faasinjèe 'passenger'; faasinjojî PL. [Jag01] §9.5.4 p.376.

    Instances For
      source
      @[implicit_reducible]
      instance Zimmermann2008.instDecidableEqFaasinjee :
      DecidableEq Faasinjee
      Equations
      source
      def Zimmermann2008.instReprFaasinjee.repr :
      Faasinjee → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[implicit_reducible]
        instance Zimmermann2008.instReprFaasinjee :
        Repr Faasinjee
        Equations
        source
        @[implicit_reducible]
        instance Zimmermann2008.instPartialOrderFaasinjee :
        PartialOrder Faasinjee

        Flat order: every passenger is an atom; distinct passengers do not overlap.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        instance Zimmermann2008.instIsAtomicDomainFaasinjee :
        Mereology.IsAtomicDomain Faasinjee

        The flat Faasinjee order is an IsAtomicDomain; its atom/disjoint facts now derive from the shared Mereology machinery rather than bespoke proofs.

        source
        def Zimmermann2008.Daura :
        Faasinjee → Prop

        yā daurà wàndà 'buckled their seatbelt'.

        Equations
        Instances For
          source
          @[implicit_reducible]
          instance Zimmermann2008.instDecidablePredFaasinjeeDaura :
          DecidablePred Daura
          Equations

          Mereological structure #

          source
          theorem Zimmermann2008.atom_of_faasinjee (x : Faasinjee) :
          Mereology.Atom x
          source
          theorem Zimmermann2008.faasinjee_disjoint (x y : Faasinjee) (h : Mereology.Overlap x y) :
          x = y
          source
          theorem Zimmermann2008.faasinjee_ONE_empty :
          Quantification.ONEModifiers.ONE_empty fun (x : Faasinjee) => True

          ONE_empty holds of the universal faasinjèe predicate. This is the presupposition Z2008's kō-wh analysis (via Q_∀ + ONE_∅) places on its SG-count restrictor.

          UniversalQuantifier.kowWh distributivity (Jaggar §9.5.1, Z2008 §4.2.1) #

          source
          theorem Zimmermann2008.kowWh_daura_false :
          ¬Hausa.UniversalQuantifier.kowWh.z2008Denot (fun (x : Faasinjee) => True) Daura

          kōwānè faasinjèe yā daurà wàndà 'every passenger buckled their seatbelt' is false on this model: the kowWh-entry's denotation forces atom-by-atom predication (Jaggar p.370), and Càdi falsifies the scope.

          Indefinite.wani scope ambiguity under negation #

          (Jaggar §9.5.3, Z2008 §3.2.4 ex. 69)

          The marked indefinite wani faasinjèe bài daurà wàndà ba 'wani passenger didn't buckle their seatbelt' is ambiguous between the ¬∃ reading ('no passenger buckled', preferred) and the ∃¬ reading ('some passenger didn't buckle'). On the 3-passenger model the readings have different truth values: the ∃¬ reading is true (Càdi witnesses), the ¬∃ reading is false (Audù and Bàlki did buckle). Both readings are linguistically available; their truth values diverge on this scenario.

          source
          theorem Zimmermann2008.wani_wide_scope :
          Quantification.some_sem (fun (x : Faasinjee) => True) fun (x : Faasinjee) => ¬Daura x

          The wide-scope (∃¬) reading: ∃x. Faasinjèe(x) ∧ ¬Daura(x). Witnessed by Càdi.

          source
          theorem Zimmermann2008.wani_narrow_scope_false :
          ¬¬∃ (x : Faasinjee), Daura x

          The narrow-scope (¬∃) reading: ¬∃x. Faasinjèe(x) ∧ Daura(x). False on this model — Audù witnesses the negated existential.

          source
          theorem Zimmermann2008.wani_ambiguity_witness :
          (Quantification.some_sem (fun (x : Faasinjee) => True) fun (x : Faasinjee) => ¬Daura x) ∧ ¬¬∃ (x : Faasinjee), Daura x

          Indefinite.wani scope ambiguity, witnessed on a single model: the ∃¬ reading is true and the ¬∃ reading is false simultaneously. The empirical content of Z2008's ex. 69.