Negative concord: n-word + concord typology

[Gia00] [vdAVA16]

Lightweight, Fragment-importable types for negative concord: the item-level n-word status, the NC subtype, and the clausal-position parameter the strict/non-strict contrast turns on.

Kept separate from Typology/Negation.lean (the WALS-based negation survey) so that Typology/PolarityItem.lean and Fragment lexicons can import the n-word classification without pulling in the WALS datapoint files. Negation.lean imports this file to bridge the item-level status to its language-level WALS 115A NegIndefiniteStrategy (NegIndefiniteStrategy.hasNegativeConcord / .admits).

Main declarations

• NWordStatus — n-word / negative-quantifier / NPI (item-level).
• NegConcordSubtype — strict / non-strict / negative-spread.
• NWordPosition + NegConcordSubtype.nmRequired — the strict/non-strict contrast, derived from the type.

inductive Features.NegativeConcord.NWordStatus : Type

Item-level status of a negation-sensitive indefinite: the n-word vs negative-quantifier vs NPI trichotomy. [Gia00] gives the minimal, deliberately theory-neutral definition — n-words "occur in NC structures and can be associated with negative meaning" — and stresses their heterogeneity. The internal semantics is contested (negative existential vs polarity-sensitive universal vs an NPI licensed by a null negation); this enum records only the distributional class, which [vdAVA16] take as the basis of the NC typology. Lets a strict-NC n-word (Russian никто, Italian nessuno) be classified honestly rather than borrowing a strong-NPI slot in Semantics.Polarity.

• nWord : NWordStatus

  N-word: occurs in negative-concord structures (Romance nessuno, Slavic никто, Greek típota, Hungarian semmi); licenses a negative fragment answer ("Nothing.") yet typically co-occurs with a clausal negation marker.

• negQuantifier : NWordStatus

  Inherently negative quantifier: negates on its own with no concord; two stack to double negation. English nobody, German niemand.

• npi : NWordStatus

  Negative-polarity item: non-negative, licensed by (not contributing) negation, occurs across a wider range of contexts (questions, conditionals, comparatives). English anybody.

@[implicit_reducible]

instance Features.NegativeConcord.instDecidableEqNWordStatus : DecidableEq NWordStatus

Equations

• Features.NegativeConcord.instDecidableEqNWordStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.NegativeConcord.instBEqNWordStatus.beq : NWordStatus → NWordStatus → Bool

Equations

• Features.NegativeConcord.instBEqNWordStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Features.NegativeConcord.instBEqNWordStatus : BEq NWordStatus

Equations

• Features.NegativeConcord.instBEqNWordStatus = { beq := Features.NegativeConcord.instBEqNWordStatus.beq }

@[implicit_reducible]

instance Features.NegativeConcord.instReprNWordStatus : Repr NWordStatus

Equations

• Features.NegativeConcord.instReprNWordStatus = { reprPrec := Features.NegativeConcord.instReprNWordStatus.repr }

def Features.NegativeConcord.instReprNWordStatus.repr : NWordStatus → Nat → Std.Format

Equations

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

inductive Features.NegativeConcord.NegConcordSubtype : Type

Subtype of negative concord ([vdAVA16]; [Gia00]). strict keeps the clausal negation marker regardless of n-word position (Greek, Hungarian, Slavic); nonStrict drops it when the n-word is preverbal but requires it postverbally (Italian, Spanish, Portuguese); negativeSpread has several n-words share one negation with no clausal marker at all (French personne n'a rien dit). [vdAVA16] find strict far more frequent than nonStrict, and nonStrict itself heterogeneous — not cleanly a single category.

• strict : NegConcordSubtype
• nonStrict : NegConcordSubtype
• negativeSpread : NegConcordSubtype

@[implicit_reducible]

instance Features.NegativeConcord.instDecidableEqNegConcordSubtype : DecidableEq NegConcordSubtype

Equations

• Features.NegativeConcord.instDecidableEqNegConcordSubtype x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Features.NegativeConcord.instBEqNegConcordSubtype : BEq NegConcordSubtype

Equations

• Features.NegativeConcord.instBEqNegConcordSubtype = { beq := Features.NegativeConcord.instBEqNegConcordSubtype.beq }

def Features.NegativeConcord.instBEqNegConcordSubtype.beq : NegConcordSubtype → NegConcordSubtype → Bool

Equations

• Features.NegativeConcord.instBEqNegConcordSubtype.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Features.NegativeConcord.instReprNegConcordSubtype : Repr NegConcordSubtype

Equations

• Features.NegativeConcord.instReprNegConcordSubtype = { reprPrec := Features.NegativeConcord.instReprNegConcordSubtype.repr }

def Features.NegativeConcord.instReprNegConcordSubtype.repr : NegConcordSubtype → Nat → Std.Format

Equations

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

inductive Features.NegativeConcord.NWordPosition : Type

Position of an n-word relative to the finite verb — the parameter the strict vs non-strict contrast turns on.

• preverbal : NWordPosition
• postverbal : NWordPosition

@[implicit_reducible]

instance Features.NegativeConcord.instDecidableEqNWordPosition : DecidableEq NWordPosition

Equations

• Features.NegativeConcord.instDecidableEqNWordPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Features.NegativeConcord.instBEqNWordPosition.beq : NWordPosition → NWordPosition → Bool

Equations

• Features.NegativeConcord.instBEqNWordPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Features.NegativeConcord.instBEqNWordPosition : BEq NWordPosition

Equations

• Features.NegativeConcord.instBEqNWordPosition = { beq := Features.NegativeConcord.instBEqNWordPosition.beq }

@[implicit_reducible]

instance Features.NegativeConcord.instReprNWordPosition : Repr NWordPosition

Equations

• Features.NegativeConcord.instReprNWordPosition = { reprPrec := Features.NegativeConcord.instReprNWordPosition.repr }

def Features.NegativeConcord.instReprNWordPosition.repr : NWordPosition → Nat → Std.Format

Equations

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

def Features.NegativeConcord.NegConcordSubtype.nmRequired : NegConcordSubtype → NWordPosition → Bool

Whether a clausal negation marker is required, given the NC subtype and the n-word's position ([Gia00]: strict NC keeps the marker regardless of position; non-strict drops it for a preverbal n-word but requires it postverbally; negative spread has no clausal marker). The strict/non-strict contrast falls out of the type.

Equations

• Features.NegativeConcord.NegConcordSubtype.strict.nmRequired x✝ = true
• Features.NegativeConcord.NegConcordSubtype.nonStrict.nmRequired Features.NegativeConcord.NWordPosition.preverbal = false
• Features.NegativeConcord.NegConcordSubtype.nonStrict.nmRequired Features.NegativeConcord.NWordPosition.postverbal = true
• Features.NegativeConcord.NegConcordSubtype.negativeSpread.nmRequired x✝ = false

theorem Features.NegativeConcord.strict_nonstrict_contrast : NegConcordSubtype.strict.nmRequired NWordPosition.preverbal = true ∧ NegConcordSubtype.nonStrict.nmRequired NWordPosition.preverbal = false ∧ NegConcordSubtype.nonStrict.nmRequired NWordPosition.postverbal = true

The strict vs non-strict contrast: both require the marker postverbally, but only strict requires it preverbally ([Gia00]).