Grubic, Renans, and Duah (2019): Focus, Exhaustivity and Existence in Akan, Ga and Ngamo

Grubic, Renans and Duah analyse the marked focus/background constructions of Akan, Ga and Ngamo (section 8), whose data, the rows of Data.Examples.GrubicRenansDuah2019, they collect in sections 5 and 6. In none of the three is the exhaustive inference asserted: negating the construction targets the prejacent, so an additive continuation loses its antecedent, where negating overt only, the substrate's Focus.Particles.only, keeps it. The Akan nà and Ga ni constructions are clefts that assert the prejacent and presuppose conditional exhaustivity, that if the prejacent holds no other alternative does, together with existence. The Ngamo =i/ye construction only presupposes that its background is salient.

Main results

• negated_only_licenses_also, negated_cleft_notMem: negating only keeps an antecedent for also, negating a marked construction does not.
• cleft_neg_of_alt, cleft_exhaustive, cleft_existence: the conditional exhaustivity of the cleft projects through negation, cannot be cancelled, and comes with existence.
• marked_exhaustivity_cancellable, marked_of_not_exists: the Ngamo construction's exhaustive inference is a cancellable implicature, and it carries no existence presupposition.

Implementation notes

Constructions are trivalent propositions over an arbitrary set of alternatives containing the prejacent, so the theorems are general rather than checked on a two-world model. The background of (78) is the existential closure of the alternatives, and its salience an abstract predicate on propositions. Section 4's contrast finding, which the paper concludes is pragmatic rather than conventional, and section 7's argument that salience is not givenness are not formalized.

References

• [GRD19]
• [EK98]

noncomputable def GrubicRenansDuah2019.cleft {W : Type u_1} (alts : Set (Set W)) (p : Set W) : W → SignType

The Akan nà and Ga ni constructions, (75) and (76), assert the prejacent and presuppose conditional exhaustivity together with existence.

Equations

• GrubicRenansDuah2019.cleft alts p = {w : W | (w ∈ p → w ∈ Exhaustification.excludes alts p) ∧ w ∈ ⋃₀ alts}.indicator fun (w : W) => SignType.ofProp (w ∈ p)

noncomputable def GrubicRenansDuah2019.marked {W : Type u_1} (alts : Set (Set W)) (p : Set W) (salient : Set W → Prop) : W → SignType

The Ngamo =i/ye construction (78) asserts the prejacent and presupposes the salience of the background, the existential closure of the alternatives.

Equations

• GrubicRenansDuah2019.marked alts p salient = {_w : W | salient (⋃₀ alts)}.indicator fun (w : W) => SignType.ofProp (w ∈ p)

The exhaustive inference is not asserted, section 5.2.1

theorem GrubicRenansDuah2019.negated_only_licenses_also {W : Type u_1} (alts : Set (Set W)) (p : Set W) {w : W} (h : -Focus.Particles.only (fun (x1 x2 : Set W) => x1 ⊆ x2) alts p w = 1) : w ∈ p ∧ ∃ q ∈ alts, ¬p ⊆ q ∧ w ∈ q

Negating overt only keeps the prejacent and denies exhaustivity, so some alternative the prejacent does not entail holds and also has its antecedent, (36b) and (37b).

theorem GrubicRenansDuah2019.negated_cleft_notMem {W : Type u_1} (alts : Set (Set W)) (p : Set W) {w : W} (h : -cleft alts p w = 1) : w ∉ p

Negating a marked construction targets the prejacent, so also lacks its antecedent, (36a) to (38a).

Implicature in Ngamo, presupposition in Akan and Ga, section 5.2.2

theorem GrubicRenansDuah2019.marked_exhaustivity_cancellable {W : Type u_1} (alts : Set (Set W)) (p : Set W) {salient : Set W → Prop} {q : Set W} {w : W} (hs : salient (⋃₀ alts)) (hq : q ∈ alts) (hne : ¬p ⊆ q) (hw : w ∈ p ∩ q) : marked alts p salient w = 1 ∧ w ∉ Exhaustification.excludes alts p

The Ngamo construction is satisfied, presupposition included, at a world where an alternative the prejacent does not entail holds too, so its exhaustive inference is cancellable ((42) and (45)).

theorem GrubicRenansDuah2019.cleft_exhaustive {W : Type u_1} (alts : Set (Set W)) (p : Set W) {w : W} (h : cleft alts p w = 1) : w ∈ Exhaustification.excludes alts p

The cleft, wherever it is defined and true, is exhaustive ((43), (44) and (77)); a further true alternative makes it undefined, so it cannot answer a mention-some question, (49) and (50).

theorem GrubicRenansDuah2019.cleft_neg_of_alt {W : Type u_1} (alts : Set (Set W)) (p : Set W) {q : Set W} {w : W} (hq : q ∈ alts) (hw : w ∈ q) (hp : w ∉ p) : -cleft alts p w = 1

The conditional presupposition projects, (54). A negated cleft is defined and true at a world where the prejacent fails and another alternative holds, so it wasn't Fred she invited is compatible with her inviting Peter and Paul.

Existence, section 6

theorem GrubicRenansDuah2019.cleft_existence {W : Type u_1} (alts : Set (Set W)) (p : Set W) {w : W} (h : cleft alts p w ≠ 0) : w ∈ ⋃₀ alts

The cleft presupposes that some alternative holds, so a focused negative quantifier clashes with it ((60) and (61)).

theorem GrubicRenansDuah2019.marked_of_not_exists {W : Type u_1} (alts : Set (Set W)) (p : Set W) {salient : Set W → Prop} (hs : salient (⋃₀ alts)) {w : W} : w ∉ ⋃₀ alts → marked alts p salient w ≠ 0

The Ngamo construction is defined at a world where no alternative holds, so it carries no existence presupposition (59).