Zimmermann (2008): Quantification in Hausa

This file formalizes the scopal and quantificational observations of [Zim08]'s chapter on the Hausa quantifier system in [Mat08a], whose inventory the fragment Hausa.Determiners types after [New00] and [Jag01]. Bare indefinite noun phrases always scope under negation, whether they follow or precede the negation marker, (11)–(14); the chapter's preferred account makes them predicates whose existential force comes from the verb, after van Geenhoven, so that negation over the verb yields a negative existential in either position (bareVerb, neg_bareVerb_iff, bare_no_wide_scope). The marked indefinite wani is an existential that is ambiguous under verb-phrase negation between the negative existential and the some-not reading, (69), which come apart on a three-passenger model (wani_wide_scope, wani_narrow_scope_false). The distributive universal koo+wh reads as a negative existential under verb-phrase negation, (73), and as a negative universal under sentence negation, (74): the first is the universal scoping over the negation (every_neg_iff_not_some), and the two readings differ on the model (kowWh_negation_readings_diverge). The collective universal duk takes a plural or mass argument, (85)–(86), combines with collective predicates that the distributive koo+wh rejects, (89)–(90) (duk_collective, not_every_collective), and yields the negative universal under either negation, (91) (neg_duk_iff).

Implementation notes

• The chapter leaves the choice among generalized-quantifier, indeterminate-pronoun and choice-function analyses of the class-B quantifiers open (§3.2.5); wani and koo+wh are read here as the generalized quantifiers GQ.some and every, the first of the three.
• A collective predicate is one that holds only of pluralities of at least two members; the distributive universal applies it member by member and so fails.
• The binding differences of §4.2.3 and the adverbial quantifiers of §6 are not represented.

References

• [Zim08]
• [Mat08a]
• [New00]
• [Jag01]

Bare indefinites under negation, §2.1.3

def Zimmermann2008.bareVerb {α : Type u_1} {E : Type u_2} (V : α → E → Prop) (P : α → Prop) (e : E) : Prop

A verb that forms a complex predicate with a bare indefinite argument: the existential force comes from the verb, λP λe. ∃x, P x ∧ V x e.

Equations

• Zimmermann2008.bareVerb V P e = ∃ (x : α), P x ∧ V x e

theorem Zimmermann2008.neg_bareVerb_iff {α : Type u_1} {E : Type u_2} (V : α → E → Prop) (P : α → Prop) (e : E) : ¬bareVerb V P e ↔ ∀ (x : α), P x → ¬V x e

Negation over the verb yields the negative existential, (14): no bare-indefinite reading scopes over negation, wherever the noun phrase sits.

A three-passenger domain

inductive Zimmermann2008.Faasinjee : Type

Three passengers, faasinjojî: Audù, Bàlki and Càdi.

• audu : Faasinjee
• balki : Faasinjee
• cadi : Faasinjee

@[instance_reducible]

instance Zimmermann2008.instDecidableEqFaasinjee : DecidableEq Faasinjee

Equations

• Zimmermann2008.instDecidableEqFaasinjee x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Zimmermann2008.instReprFaasinjee.repr : Faasinjee → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Zimmermann2008.instReprFaasinjee : Repr Faasinjee

Equations

• Zimmermann2008.instReprFaasinjee = { reprPrec := Zimmermann2008.instReprFaasinjee.repr }

@[instance_reducible]

instance Zimmermann2008.instFintypeFaasinjee : Fintype Faasinjee

Equations

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

def Zimmermann2008.Daura : Faasinjee → Prop

yā daurà wàndà 'buckled their seatbelt': Audù and Bàlki did, Càdi did not.

Equations

• Zimmermann2008.Daura Zimmermann2008.Faasinjee.audu = True
• Zimmermann2008.Daura Zimmermann2008.Faasinjee.balki = True
• Zimmermann2008.Daura Zimmermann2008.Faasinjee.cadi = False

@[instance_reducible]

instance Zimmermann2008.instDecidablePredFaasinjeeDaura : DecidablePred Daura

Equations

• Zimmermann2008.instDecidablePredFaasinjeeDaura Zimmermann2008.Faasinjee.audu = isTrue trivial
• Zimmermann2008.instDecidablePredFaasinjeeDaura Zimmermann2008.Faasinjee.balki = isTrue trivial
• Zimmermann2008.instDecidablePredFaasinjeeDaura Zimmermann2008.Faasinjee.cadi = isFalse Zimmermann2008.instDecidablePredFaasinjeeDaura._proof_1

theorem Zimmermann2008.bare_no_wide_scope : ¬¬bareVerb (fun (x : Faasinjee) (x_1 : Unit) => Daura x) (fun (x : Faasinjee) => True) () ∧ ∃ (x : Faasinjee), ¬Daura x

The bare-indefinite reading of passengers didn't buckle is false on the model, while the some-not reading a wide-scope indefinite would give is true: the readings the chapter separates in (13) are distinct.

The class-B quantifiers, §3.2

theorem Zimmermann2008.wani_wide_scope : Quantifier.GQ.some (fun (x : Faasinjee) => True) fun (x : Faasinjee) => ¬Daura x

The wide-scope reading of wani faasinjèe bài daurà wàndà ba, some passenger did not buckle their seatbelt, (69ii): Càdi is the witness.

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

The negative existential reading, no passenger buckled their seatbelt, (69i), fails: Audù did.

theorem Zimmermann2008.wani_ambiguity_witness : (Quantifier.GQ.some (fun (x : Faasinjee) => True) fun (x : Faasinjee) => ¬Daura x) ∧ ¬¬∃ (x : Faasinjee), Daura x

The two readings of wani under verb-phrase negation come apart on the model, (69).

theorem Zimmermann2008.every_neg_iff_not_some {α : Type u_1} (R S : α → Prop) : (Quantifier.GQ.every R fun (x : α) => ¬S x) ↔ ¬Quantifier.GQ.some R S

The universal over the negation is the negative existential: koo+wh under verb-phrase negation, (73), I saw no one.

theorem Zimmermann2008.kowWh_negation_readings_diverge : ¬Quantifier.GQ.every (fun (x : Faasinjee) => True) Daura ∧ ¬Quantifier.GQ.every (fun (x : Faasinjee) => True) fun (x : Faasinjee) => ¬Daura x

The negative existential of (73) and the negative universal of (74) differ on the model: not every passenger buckled, yet it is false that none did.

The two universals, §4

def Zimmermann2008.kowWhSem {α : Type u_1} (R S : α → Prop) : Prop

The distributive universal koo+wh: the generalized quantifier every over a predicate of individuals.

Equations

• Zimmermann2008.kowWhSem R S = Quantifier.GQ.every R S

def Zimmermann2008.dukSem {α : Type u_1} (R : Finset α) (S : Finset α → Prop) : Prop

The collective universal duk: its plural or mass argument, (85)–(86), is a plurality, and the predicate applies to the plurality as a whole.

Equations

• Zimmermann2008.dukSem R S = S R

def Zimmermann2008.Collective {α : Type u_1} (S : Finset α → Prop) : Prop

A collective predicate such as tàaru 'gather' or keewàyee 'surround' holds only of pluralities with at least two members.

Equations

• Zimmermann2008.Collective S = ∀ (s : Finset α), S s → 2 ≤ s.card

theorem Zimmermann2008.duk_collective {α : Type u_1} {R : Finset α} {S : Finset α → Prop} (h : S R) : dukSem R S

Duk combines with a collective predicate, (90): the students gathered as a group.

theorem Zimmermann2008.not_every_collective {α : Type u_1} {R : Finset α} {S : Finset α → Prop} (hS : Collective S) (hR : R.Nonempty) : ¬kowWhSem (fun (x : α) => x ∈ R) fun (x : α) => S {x}

Koo+wh cannot combine with a collective predicate, (89): applying it member by member asks each singleton to gather, which no collective predicate allows.

theorem Zimmermann2008.neg_duk_iff {α : Type u_1} (R : Finset α) (P : α → Prop) : (¬dukSem R fun (s : Finset α) => ∀ x ∈ s, P x) ↔ ¬Quantifier.GQ.every (fun (x : α) => x ∈ R) P

Duk under negation is the negative universal not all, (91), under verb-phrase and sentence negation alike: for a distributive predicate, not every member satisfies it.

theorem Zimmermann2008.kowWh_daura_false : ¬kowWhSem (fun (x : Faasinjee) => True) Daura

Kōwānè faasinjèe yā daurà wàndà 'every passenger buckled their seatbelt' is false on the model: Càdi did not.