Zarma-Sonrai: Negation and Expletive Negation Markers

[JK21]

Zarma-Sonrai (ISO 639-3: dje) is a Songhay language mainly spoken in the southwestern border area of Niger. It had not been documented for expletive negation (EN) prior to [JK21].

Standard Negation

Zarma-Sonrai distinguishes two standard negation markers by aspect:

• si : imperfective negation (IPFV.NEG)
• mana / batu : perfective negation (PFV.NEG)

Expletive Negation

EN negators vary by trigger class, mirroring the aspect-based split:

Trigger class	EN negator	Gloss	Aspect
FEAR	si	IPFV.NEG	imperfective
AVOID	si	IPFV.NEG	imperfective
DENY	si	IPFV.NEG	imperfective
DELAY	batu	PFV.NEG	perfective
BEFORE	mana	PFV.NEG	perfective
CANNOT WAIT	si + batu	IPFV+PFV	mixed

The choice of EN negator correlates with the aspectual properties of the complement clause, not with the trigger class itself.

Notable Absences

• WITHOUT: expressed as "q not p" (analytic, not triggering EN)
• TOO…TO: expressed as "too…so that…not" (collocation, not EN)
• MORE THAN: attested (with da 'than'), but EN data limited

Standard negation

def ZarmaSonrai.Negation.si : Syntax.Negation.NegMarkerEntry

si — imperfective negation marker. Aspect-conditioned alternation with perfective mana/batu. Parallel to Mandarin's bù/méi split.

Equations

• ZarmaSonrai.Negation.si = { form := "si", morphemeType := Syntax.Negation.NegMorphemeType.particle, position := Syntax.Negation.NegMarkerPosition.preverbal }

def ZarmaSonrai.Negation.mana : Syntax.Negation.NegMarkerEntry

mana — perfective negation marker (one of two variants).

Equations

• ZarmaSonrai.Negation.mana = { form := "mana", morphemeType := Syntax.Negation.NegMorphemeType.particle, position := Syntax.Negation.NegMarkerPosition.preverbal }

def ZarmaSonrai.Negation.batu : Syntax.Negation.NegMarkerEntry

batu — perfective negation marker (second variant; also surfaces as a verb 'wait/delay').

Equations

• ZarmaSonrai.Negation.batu = { form := "batu", morphemeType := Syntax.Negation.NegMorphemeType.particle, position := Syntax.Negation.NegMarkerPosition.preverbal }

def ZarmaSonrai.Negation.negationSystem : Syntax.Negation.NegationSystem

The Zarma-Sonrai negation system: three aspect-conditioned markers. si (imperfective) listed first per ordering convention; the two perfective variants follow. The Fragment-side joint consumed by Studies/Dryer2013Negation.lean.

Equations

• ZarmaSonrai.Negation.negationSystem = Syntax.Negation.NegationSystem.ofISO "dje" [ZarmaSonrai.Negation.si, ZarmaSonrai.Negation.mana, ZarmaSonrai.Negation.batu]

def ZarmaSonrai.Negation.ipfvNeg : String

Legacy String accessors (used by enNegatorForAspect in this file).

Equations

• ZarmaSonrai.Negation.ipfvNeg = ZarmaSonrai.Negation.si.form

def ZarmaSonrai.Negation.pfvNeg : String

Equations

• ZarmaSonrai.Negation.pfvNeg = ZarmaSonrai.Negation.mana.form

def ZarmaSonrai.Negation.pfvNeg2 : String

Equations

• ZarmaSonrai.Negation.pfvNeg2 = ZarmaSonrai.Negation.batu.form

inductive ZarmaSonrai.Negation.ENAspect : Type

Aspect governs expletive negation marker choice.

• ipfv : ENAspect
• pfv : ENAspect

@[implicit_reducible]

instance ZarmaSonrai.Negation.instDecidableEqENAspect : DecidableEq ENAspect

Equations

• ZarmaSonrai.Negation.instDecidableEqENAspect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ZarmaSonrai.Negation.instReprENAspect.repr : ENAspect → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ZarmaSonrai.Negation.instReprENAspect : Repr ENAspect

Equations

• ZarmaSonrai.Negation.instReprENAspect = { reprPrec := ZarmaSonrai.Negation.instReprENAspect.repr }

Expletive negation markers

structure ZarmaSonrai.Negation.ENNegator : Type

An expletive negation marker used in a specific trigger context.

• form : String

  The negator form

• aspect : ENAspect

  Aspectual context

• isStandardNeg : Bool

  Whether this is a standard negation marker

def ZarmaSonrai.Negation.instReprENNegator.repr : ENNegator → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ZarmaSonrai.Negation.instReprENNegator : Repr ENNegator

Equations

• ZarmaSonrai.Negation.instReprENNegator = { reprPrec := ZarmaSonrai.Negation.instReprENNegator.repr }

@[implicit_reducible]

instance ZarmaSonrai.Negation.instDecidableEqENNegator : DecidableEq ENNegator

Equations

• ZarmaSonrai.Negation.instDecidableEqENNegator = ZarmaSonrai.Negation.instDecidableEqENNegator.decEq

def ZarmaSonrai.Negation.instDecidableEqENNegator.decEq (x✝ x✝¹ : ENNegator) : Decidable (x✝ = x✝¹)

Equations

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

def ZarmaSonrai.Negation.enIpfv : ENNegator

Imperfective EN negator: si.

Equations

• ZarmaSonrai.Negation.enIpfv = { form := "si", aspect := ZarmaSonrai.Negation.ENAspect.ipfv, isStandardNeg := true }

def ZarmaSonrai.Negation.enPfv : ENNegator

Perfective EN negator: batu.

Equations

• ZarmaSonrai.Negation.enPfv = { form := "batu", aspect := ZarmaSonrai.Negation.ENAspect.pfv, isStandardNeg := true }

theorem ZarmaSonrai.Negation.en_negators_are_standard : enIpfv.isStandardNeg = true ∧ enPfv.isStandardNeg = true

Both EN negators are standard negation markers — Zarma-Sonrai does not have a dedicated expletive negator (unlike French ne).

Trigger-specific examples

structure ZarmaSonrai.Negation.ENExample : Type

A glossed EN example from Zarma-Sonrai.

• triggerClass : String
• triggerForm : String
• triggerGloss : String
• sentence : String
• gloss : String
• translation : String
• enNegator : String
• enAspect : ENAspect

@[implicit_reducible]

instance ZarmaSonrai.Negation.instReprENExample : Repr ENExample

Equations

• ZarmaSonrai.Negation.instReprENExample = { reprPrec := ZarmaSonrai.Negation.instReprENExample.repr }

def ZarmaSonrai.Negation.instReprENExample.repr : ENExample → ℕ → Std.Format

Equations

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

def ZarmaSonrai.Negation.delayExample : ENExample

DELAY trigger: batu 'delay' ([JK21], ex. 22).

Equations

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

def ZarmaSonrai.Negation.cannotWaitExample : ENExample

CANNOT WAIT trigger: si batu 'cannot wait' ([JK21], Table 5, ex. 25).

Equations

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

def ZarmaSonrai.Negation.hideExample : ENExample

HIDE trigger: tugu 'hide'. Zarma-Sonrai example ([JK21], §6.1.3, ex. 20).

N.B. The negator sinda ('not.have') is a copular/possessive negative, not the imperfective marker si or perfective mana/batu. It falls outside the aspect-based EN negator selection system formalized in enNegatorForAspect. The .ipfv classification here is approximate.

Equations

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

def ZarmaSonrai.Negation.allExamples : List ENExample

Equations

• ZarmaSonrai.Negation.allExamples = [ZarmaSonrai.Negation.delayExample, ZarmaSonrai.Negation.cannotWaitExample, ZarmaSonrai.Negation.hideExample]

Aspect-based negator selection

def ZarmaSonrai.Negation.enNegatorForAspect : ENAspect → String

The EN negator is determined by the aspectual properties of the complement clause, not by the trigger class. This is a general property of Zarma-Sonrai negation, not specific to EN.

Equations

• ZarmaSonrai.Negation.enNegatorForAspect ZarmaSonrai.Negation.ENAspect.ipfv = ZarmaSonrai.Negation.ipfvNeg
• ZarmaSonrai.Negation.enNegatorForAspect ZarmaSonrai.Negation.ENAspect.pfv = ZarmaSonrai.Negation.pfvNeg2

theorem ZarmaSonrai.Negation.fear_uses_ipfv_neg : enNegatorForAspect ENAspect.ipfv = "si"

theorem ZarmaSonrai.Negation.delay_uses_pfv_neg : enNegatorForAspect ENAspect.pfv = "batu"

def ZarmaSonrai.Negation.withoutBlocked : Semantics.Negation.ENBlockingReason

Why WITHOUT and TOO…TO do not trigger EN in Zarma-Sonrai.

WITHOUT is expressed analytically as "q not p" and TOO…TO as "too…so that…not" — in both cases, the negation is a necessary part of the meaning, not expletive ([JK21], §7).

Equations

• ZarmaSonrai.Negation.withoutBlocked = Semantics.Negation.ENBlockingReason.analyticNegation

def ZarmaSonrai.Negation.tooToBlocked : Semantics.Negation.ENBlockingReason

Equations

• ZarmaSonrai.Negation.tooToBlocked = Semantics.Negation.ENBlockingReason.analyticNegation