Owusu (2022): the Akan indefinite bí

Owusu analyses the Akan indefinite bí as a choice function skolemized to a situation. Her entry (67) maps a situation s and a property P to f s (P s), presupposing that f s is a choice function. The function is free, fixed by the context as in Kratzer's analysis of a certain, and never existentially closed. A bí phrase scopes only above negation and, as a subject, above biara 'every', but as an object it also scopes below biara, while a bare noun scopes only below either. Owusu argues that closing the function freely, after Reinhart and Winter, derives the narrow reading under negation that bí lacks; that closing it only at the top, after Matthewson, derives no narrow reading of a conditional; and that the reading below biara is functional, the function's individual index being bound by the quantifier.

Main results

• closure_below_negation_iff: closing the function below negation, (50), gives the narrow reading.
• negation_narrow_iff: under negation the free function of (67) gives the narrow reading for every predicate only when the restrictor has a single member.
• closure_above_conditional_iff: closing the function at the top of a conditional gives the wide reading.
• wide_iff, functional_iff: (55), the readings with the individual index free and bound.
• ex57_free_iff, ex57_bound_iff, Scenario58.free, Scenario58.bound, Scenario58.not_narrow: both construals of (57) say that every student kept back one of their papers, which holds in the scenario (58) where the narrow reading fails.
• bi_not_narrow_under_negation, bare_narrow_under_negation, bi_narrow_under_every_iff, bare_narrow_under_every: the chapter's generalizations over its examples.

Implementation notes

• The presupposition of (67) is the type of f, a family S → ChoiceFunction E.
• The situation index and the individual index of (67) are taken one at a time, as the index type S.
• A construal holds in some context when some choice function makes it true.
• An example counts as a bí example when one of its words is the form of Akan.Determiners.bi.
• Owusu takes the world variable from a 2019 manuscript by Mirrazi; [Mir24] develops the analysis from the same example.

TODO

• The weak crossover asymmetry of (54)–(56), after [Chi01]: an index bound by biara in subject position would cross over it. It needs binding over syntax trees.
• The world variable of §3.3.3 in conditionals, (66), and under pɛ 'want', (65), with the existential entailment and substitution diagnostics of §3.2.3. The bound construal of (66b) is entailed by the narrow reading but is weaker than it unless the function picks an elder who comes wherever one does; the chapter does not discuss this.
• §3.4: bí nó, nó bí, and the ignorance inference of bí.
• The second chapter's analysis of nó.

References

• [Owu22]
• [Kra98b]
• [Rei97]
• [Win97]
• [Mat99]
• [Chi01]
• [Mir24]

Negation

theorem Owusu2022.closure_below_negation_iff {E : Type u_2} {N VP : E → Prop} (hN : ∃ (x : E), N x) : (¬∃ (f : Reference.ChoiceFunction E), VP (f N)) ↔ ¬Quantifier.GQ.some N VP

Closing the choice function below negation, as free existential closure must allow for (51), gives the narrow reading (50).

theorem Owusu2022.negation_narrow_iff {S : Type u_1} {E : Type u_2} (f : S → Reference.ChoiceFunction E) {s : S} {P : S → E → Prop} (hP : ∃ (x : E), P s x) : (∀ (VP : E → Prop), ¬VP ((f s) (P s)) ↔ ¬Quantifier.GQ.some (P s) VP) ↔ ∀ (x : E), P s x → x = (f s) (P s)

Under negation, the free function of (67) gives the narrow reading for every predicate exactly when its pick is the only member of the restrictor at the situation.

Conditionals

theorem Owusu2022.closure_above_conditional_iff {E : Type u_2} {N A : E → Prop} {p : Prop} (hN : ∃ (x : E), N x) : (∃ (f : Reference.ChoiceFunction E), A (f N) → p) ↔ ∃ (x : E), N x ∧ (A x → p)

Closing the choice function at the top of a conditional, as Matthewson's analysis does, gives the wide reading of (60), on which some member of the restrictor is such that the consequent holds if it satisfies the antecedent.

biara

theorem Owusu2022.wide_iff {E : Type u_2} {ι : Type u_3} {B : E → Prop} {R : ι → E → Prop} (hB : ∃ (x : E), B x) : (∃ (f : Reference.ChoiceFunction E), ∀ (z : ι), R z (f B)) ↔ Quantifier.GQ.some B fun (x : E) => ∀ (z : ι), R z x

With the individual index free, some function makes (55a) true exactly when one book was read by every woman.

theorem Owusu2022.functional_iff {E : Type u_2} {ι : Type u_3} {B : E → Prop} {R : ι → E → Prop} (hB : ∃ (x : E), B x) : (∃ (F : ι → Reference.ChoiceFunction E), ∀ (z : ι), R z ((F z) B)) ↔ ∀ (z : ι), Quantifier.GQ.some B (R z)

With the individual index bound by biara, some function makes (55b) true exactly when every woman read a book, the reading (24) glosses as every over the indefinite.

The scenario (57)–(58)

theorem Owusu2022.ex57_free_iff {E : Type u_2} {ι : Type u_3} {Wrote Submitted : ι → E → Prop} [Nonempty E] (hW : ∀ (x : ι), ∃ (y : E), Wrote x y) (hinj : Function.Injective Wrote) : (∃ (f : Reference.ChoiceFunction E), ∀ (x : ι), ¬Submitted x (f (Wrote x))) ↔ ∀ (x : ι), Quantifier.GQ.some (Wrote x) fun (x_1 : E) => ¬Submitted x x_1

With the index free, some function makes (57a) true exactly when every student wrote a paper they did not submit, provided distinct students wrote distinct papers.

theorem Owusu2022.ex57_bound_iff {E : Type u_2} {ι : Type u_3} {Wrote Submitted : ι → E → Prop} (hW : ∀ (x : ι), ∃ (y : E), Wrote x y) : (∃ (F : ι → Reference.ChoiceFunction E), ∀ (x : ι), ¬Submitted x ((F x) (Wrote x))) ↔ ∀ (x : ι), Quantifier.GQ.some (Wrote x) fun (x_1 : E) => ¬Submitted x x_1

With the index bound by biara, some function makes (57b) true exactly when every student wrote a paper they did not submit.

inductive Owusu2022.Scenario58.Student : Type

The students of (58) are Alan, Bob and Carl.

• alan : Student
• bob : Student
• carl : Student

@[instance_reducible]

instance Owusu2022.Scenario58.instDecidableEqStudent : DecidableEq Student

Equations

• Owusu2022.Scenario58.instDecidableEqStudent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Owusu2022.Scenario58.instFintypeStudent : Fintype Student

Equations

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

@[instance_reducible]

instance Owusu2022.Scenario58.instInhabitedStudent : Inhabited Student

Equations

• Owusu2022.Scenario58.instInhabitedStudent = { default := Owusu2022.Scenario58.instInhabitedStudent.default }

@[reducible, inline]

abbrev Owusu2022.Scenario58.Paper : Type

Each student has three papers.

Equations

• Owusu2022.Scenario58.Paper = (Owusu2022.Scenario58.Student × Fin 3)

def Owusu2022.Scenario58.Wrote (x : Student) (p : Paper) : Prop

A student wrote their own three papers.

Equations

• Owusu2022.Scenario58.Wrote x p = (p.1 = x)

def Owusu2022.Scenario58.Submitted (x : Student) (p : Paper) : Prop

Each student submitted two of their papers, all but the last.

Equations

• Owusu2022.Scenario58.Submitted x p = (p.1 = x ∧ p.2 ≠ 2)

@[instance_reducible]

instance Owusu2022.Scenario58.instDecidableRelStudentPaperWrote : DecidableRel Wrote

Equations

• Owusu2022.Scenario58.instDecidableRelStudentPaperWrote x✝¹ x✝ = Owusu2022.Scenario58.instDecidableRelStudentPaperWrote._aux_1 x✝¹ x✝

@[instance_reducible]

instance Owusu2022.Scenario58.instDecidableRelStudentPaperSubmitted : DecidableRel Submitted

Equations

• Owusu2022.Scenario58.instDecidableRelStudentPaperSubmitted x✝¹ x✝ = { decide := decide (x✝.1 = x✝¹) && decide (x✝.2 ≠ 2), reflects_decide := ⋯ }

theorem Owusu2022.Scenario58.free : ∃ (f : Reference.ChoiceFunction Paper), ∀ (x : Student), ¬Submitted x (f (Wrote x))

In (58), some function makes (57a) true.

theorem Owusu2022.Scenario58.bound : ∃ (F : Student → Reference.ChoiceFunction Paper), ∀ (x : Student), ¬Submitted x ((F x) (Wrote x))

In (58), some function makes (57b) true.

theorem Owusu2022.Scenario58.not_narrow : ¬∀ (x : Student), ¬Quantifier.GQ.some (Wrote x) (Submitted x)

In (58) the narrow reading of (57), that no student submitted any paper they wrote, is false.

The examples

theorem Owusu2022.bi_not_narrow_under_negation (e : Datum) : e ∈ Examples.all → Akan.Determiners.bi.form ∈ e.surfaceTokens → e.feature? "operator" = some "negation" → List.lookup "narrow" e.readings ≠ some Judgment.acceptable

Under negation no bí example has the narrow reading, (21), (22) and (57).

theorem Owusu2022.bare_narrow_under_negation (e : Datum) : e ∈ Examples.all → Akan.Determiners.bi.form ∉ e.surfaceTokens → e.feature? "operator" = some "negation" → List.lookup "narrow" e.readings = some Judgment.acceptable ∧ List.lookup "wide" e.readings ≠ some Judgment.acceptable

Under negation the bare examples have the narrow reading and not the wide one, (29) and (30).

theorem Owusu2022.bi_narrow_under_every_iff (e : Datum) : e ∈ Examples.all → Akan.Determiners.bi.form ∈ e.surfaceTokens → e.feature? "operator" = some "every" → (List.lookup "narrow" e.readings = some Judgment.acceptable ↔ e.feature? "position" = some "object")

Under biara a bí example has the narrow reading exactly when it is the object, (23) and (24).

theorem Owusu2022.bare_narrow_under_every (e : Datum) : e ∈ Examples.all → Akan.Determiners.bi.form ∉ e.surfaceTokens → e.feature? "operator" = some "every" → List.lookup "narrow" e.readings = some Judgment.acceptable ∧ List.lookup "wide" e.readings = some Judgment.unacceptable

Under biara the bare examples have only the narrow reading, (31) and (32).