Zarma-Sonrai: Negation and Expletive Negation Markers

@cite{jin-koenig-2021}

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 @cite{jin-koenig-2021}.

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

def Fragments.ZarmaSonrai.Negation.ipfvNeg : String

Negation marker for imperfective aspect contexts.

Equations

• Fragments.ZarmaSonrai.Negation.ipfvNeg = "si"

def Fragments.ZarmaSonrai.Negation.pfvNeg : String

Negation marker for perfective aspect contexts (variant 1).

Equations

• Fragments.ZarmaSonrai.Negation.pfvNeg = "mana"

def Fragments.ZarmaSonrai.Negation.pfvNeg2 : String

Negation marker for perfective aspect contexts (variant 2).

Equations

• Fragments.ZarmaSonrai.Negation.pfvNeg2 = "batu"

inductive Fragments.ZarmaSonrai.Negation.ENAspect : Type

Aspect governs expletive negation marker choice.

• ipfv : ENAspect
• pfv : ENAspect

instance Fragments.ZarmaSonrai.Negation.instDecidableEqENAspect : DecidableEq ENAspect

Equations

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

def Fragments.ZarmaSonrai.Negation.instBEqENAspect.beq : ENAspect → ENAspect → Bool

Equations

• Fragments.ZarmaSonrai.Negation.instBEqENAspect.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.ZarmaSonrai.Negation.instBEqENAspect : BEq ENAspect

Equations

• Fragments.ZarmaSonrai.Negation.instBEqENAspect = { beq := Fragments.ZarmaSonrai.Negation.instBEqENAspect.beq }

def Fragments.ZarmaSonrai.Negation.instReprENAspect.repr : ENAspect → Nat → Std.Format

Equations

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

instance Fragments.ZarmaSonrai.Negation.instReprENAspect : Repr ENAspect

Equations

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

structure Fragments.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

instance Fragments.ZarmaSonrai.Negation.instReprENNegator : Repr ENNegator

Equations

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

def Fragments.ZarmaSonrai.Negation.instReprENNegator.repr : ENNegator → Nat → Std.Format

Equations

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

def Fragments.ZarmaSonrai.Negation.instBEqENNegator.beq : ENNegator → ENNegator → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.ZarmaSonrai.Negation.instBEqENNegator.beq x✝¹ x✝ = false

instance Fragments.ZarmaSonrai.Negation.instBEqENNegator : BEq ENNegator

Equations

• Fragments.ZarmaSonrai.Negation.instBEqENNegator = { beq := Fragments.ZarmaSonrai.Negation.instBEqENNegator.beq }

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

Equations

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

instance Fragments.ZarmaSonrai.Negation.instDecidableEqENNegator : DecidableEq ENNegator

Equations

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

def Fragments.ZarmaSonrai.Negation.enIpfv : ENNegator

Imperfective EN negator: si.

Equations

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

def Fragments.ZarmaSonrai.Negation.enPfv : ENNegator

Perfective EN negator: batu.

Equations

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

theorem Fragments.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).

structure Fragments.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

instance Fragments.ZarmaSonrai.Negation.instReprENExample : Repr ENExample

Equations

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

def Fragments.ZarmaSonrai.Negation.instReprENExample.repr : ENExample → Nat → Std.Format

Equations

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

def Fragments.ZarmaSonrai.Negation.delayExample : ENExample

DELAY trigger: batu 'delay' (@cite{jin-koenig-2021}, ex. 22).

Equations

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

def Fragments.ZarmaSonrai.Negation.cannotWaitExample : ENExample

CANNOT WAIT trigger: si batu 'cannot wait' (@cite{jin-koenig-2021}, Table 5, ex. 25).

Equations

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

def Fragments.ZarmaSonrai.Negation.hideExample : ENExample

HIDE trigger: tugu 'hide'. Zarma-Sonrai example (@cite{jin-koenig-2021}, §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 Fragments.ZarmaSonrai.Negation.allExamples : List ENExample

Equations

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

def Fragments.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

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

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

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

def Fragments.ZarmaSonrai.Negation.withoutBlocked : Core.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 (@cite{jin-koenig-2021}, §7).

Equations

• Fragments.ZarmaSonrai.Negation.withoutBlocked = Core.ENBlockingReason.analyticNegation

def Fragments.ZarmaSonrai.Negation.tooToBlocked : Core.ENBlockingReason

Equations

• Fragments.ZarmaSonrai.Negation.tooToBlocked = Core.ENBlockingReason.analyticNegation