Graded exhaustivity in Akan, Ga and Ngamo

Formalises [grubic-renans-duah-2019]: the exhaustive inference of a morphosyntactically marked focus construction is not asserted in any of the three languages — it is presupposed in Akan and Ga (cleft-like, with an existence presupposition) and merely conversationally implicated in Ngamo (whose marker contributes background salience, a definiteness component kept as prose here; their §7). The three analyses are three placements of exhaustivity across the two meaning dimensions: at-issue ([EK98]-style only-semantics, rejected for these constructions), ci (presupposed), or neither (implicated).

The §5.2.1 diagnostic — negation plus an additive continuation — is derived: negating overt only keeps the prejacent and negates exhaustivity, so also finds its anaphoric antecedent ((36b)/(37b)); negating the marked constructions targets the prejacent and removes it ((36a)/(37a), the #also judgments). Their §4 contrast findings (Akan/Ga contrastive, Ngamo felicitous all-new) connect to the Semantics.Focus.Use layer and are left as a TODO.

structure GrubicRenansDuah2019.CallWorld : Type

Who Njelu phoned ((36)).

• sama : Bool
• hawwa : Bool

@[implicit_reducible]

instance GrubicRenansDuah2019.instDecidableEqCallWorld : DecidableEq CallWorld

Equations

• GrubicRenansDuah2019.instDecidableEqCallWorld = GrubicRenansDuah2019.instDecidableEqCallWorld.decEq

def GrubicRenansDuah2019.instDecidableEqCallWorld.decEq (x✝ x✝¹ : CallWorld) : Decidable (x✝ = x✝¹)

Equations

• GrubicRenansDuah2019.instDecidableEqCallWorld.decEq { sama := a, hawwa := a_1 } { sama := b, hawwa := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def GrubicRenansDuah2019.instReprCallWorld.repr : CallWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance GrubicRenansDuah2019.instReprCallWorld : Repr CallWorld

Equations

• GrubicRenansDuah2019.instReprCallWorld = { reprPrec := GrubicRenansDuah2019.instReprCallWorld.repr }

def GrubicRenansDuah2019.calledSama : Set CallWorld

Equations

• GrubicRenansDuah2019.calledSama = {w : GrubicRenansDuah2019.CallWorld | w.sama = true}

def GrubicRenansDuah2019.calledHawwa : Set CallWorld

Equations

• GrubicRenansDuah2019.calledHawwa = {w : GrubicRenansDuah2019.CallWorld | w.hawwa = true}

def GrubicRenansDuah2019.alts : Semantics.Focus.Interpretation.PropFocusValue CallWorld

The alternative phoning propositions.

Equations

• GrubicRenansDuah2019.alts = {GrubicRenansDuah2019.calledSama, GrubicRenansDuah2019.calledHawwa}

def GrubicRenansDuah2019.exh : Set CallWorld

Exhaustivity of the prejacent over the alternatives — the strong-theory only condition.

Equations

• GrubicRenansDuah2019.exh = Semantics.Focus.onlyVia GrubicRenansDuah2019.alts GrubicRenansDuah2019.calledSama

def GrubicRenansDuah2019.existencePresup : Set CallWorld

Some alternative holds.

Equations

• GrubicRenansDuah2019.existencePresup = {w : GrubicRenansDuah2019.CallWorld | w ∈ GrubicRenansDuah2019.calledSama ∨ w ∈ GrubicRenansDuah2019.calledHawwa}

def GrubicRenansDuah2019.cleftLike : Pragmatics.Expressives.TwoDimProp CallWorld

The Akan/Ga marked construction: prejacent at issue; exhaustivity and existence presupposed (§5.2.3, §6).

Equations

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

def GrubicRenansDuah2019.backgroundMarked : Pragmatics.Expressives.TwoDimProp CallWorld

The Ngamo marked construction: prejacent at issue; no exhaustivity or existence presupposition (§5.2.2, §6.1).

Equations

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

def GrubicRenansDuah2019.onlyStyle : Pragmatics.Expressives.TwoDimProp CallWorld

Overt only ((36b)/(37b)): prejacent projects, exhaustivity is at issue.

Equations

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

theorem GrubicRenansDuah2019.negated_only_licenses_also (w : CallWorld) (hne : ¬onlyStyle.atIssue w) (hp : w ∈ calledSama) : w ∈ calledHawwa

Negating overt only licenses the additive continuation: with the prejacent projected and exhaustivity negated, some distinct alternative held — also has its antecedent ((36b)/(37b)).

theorem GrubicRenansDuah2019.negated_marked_blocks_also (w : CallWorld) (h : ¬cleftLike.atIssue w) : w ∉ calledSama

Negating the marked constructions targets the prejacent, removing the additive particle's antecedent — the #also judgments of (36a)/(37a). Exhaustivity is not asserted (§5.2.1), against a [EK98]-style only-semantics for these constructions.

theorem GrubicRenansDuah2019.ngamo_exhaustivity_cancellable : ∃ (w : CallWorld), backgroundMarked.atIssue w ∧ backgroundMarked.ci w ∧ w ∉ exh

Ngamo's exhaustive inference is cancellable — a conversational implicature (§5.2.2): the construction's full content is consistent with a non-exhaustive world.

theorem GrubicRenansDuah2019.cleft_exhaustivity_uncancellable : ¬∃ (w : CallWorld), cleftLike.atIssue w ∧ cleftLike.ci w ∧ w ∉ exh

Akan/Ga exhaustivity projects and cannot be cancelled — a presupposition (§5.2.3): no world satisfies the construction while falsifying exhaustivity.

theorem GrubicRenansDuah2019.existence_contrast : (∃ (w : CallWorld), backgroundMarked.ci w ∧ w ∉ existencePresup) ∧ ∀ (w : CallWorld), cleftLike.ci w → w ∈ existencePresup

Ngamo triggers no existence presupposition; Akan and Ga do (§6): the Ngamo construction is defined at a world where no alternative holds, the cleft-like one is not.