van der Auwera and Van Alsenoy (2016): On the Typology of Negative Concord

This file formalizes [vdAVA16], a typology of negative concord, a semantically single negation expressed both by a clausal negator and by a negative indefinite, (1), over a variety sample of 179 languages. A negative indefinite is an indefinite whose dominant use is negation, as against a negatively polar or a neutral indefinite, Indefinite, and a language's way of negating with an indefinite is one of Kahrel's five strategies, Strategy. The paper's first claim is that negative concord is not frequent: the impression that it is rests on [Has97]'s deliberately wide notion of negative indefinite, so that the co-occurrence value of WALS 115A, [Has13b], covers the neutral and polar strategies as well as concord, toWALS, toWALS_eq_predicateNegationAlsoPresent_iff. The second claim is that strict concord is far more frequent than non-strict, and that non-strict concord is not one pattern but many. A concord system records, for a negative indefinite before and after the finite verb, whether the clausal negator is absent, optional or obligatory, or the position unavailable, Marking and System, the paper's formulas (19), (26), (28), (30), (32), (36), (38), (39): strict concord is obligatory marking in both positions, IsStrict, and non-strict concord is concord that is not strict, IsNonStrict. [Jes17]'s Negative Early principle, that the clausal negator appears first where the negative indefinite comes late, orders the two positions, NegativeEarly, and the four subtypes of Table 9 are exactly the non-strict systems with both positions available that respect it, nonStrict_negativeEarly_iff. The diachrony of Table 6 from Latin to modern Slavic is a chain on the strictness scale, stages_isChain, each stage respecting Negative Early, negativeEarly_of_mem_stages, whereas Catalan moves from strict to the Spanish subtype, the other way along the scale, informalCatalan_lt_formalCatalan.

Implementation notes

The strictness scale orders the markings absent, optional, obligatory, and a system is a pair of optional markings, the asterisk of the paper's formulas being none; Georgian's immediate precedence, (36), Welsh's compound verbs, (43), and Yiddish's emphatic omission, (45), are recorded as rows, since they parametrize concord by something other than the position relative to the finite verb. The frequencies of Tables 1 to 3, the areal distribution, and the morpho-syntactic composition of Table 4 are reported in the paper and not formalized. The examples are the rows of Data.Examples.VanDerAuweraVanAlsenoy2016.

References

• [vdAVA16]
• [Has97]
• [Has13b]
• [Kah96]
• [Gia98]
• [Jes17]
• [dS10]

Indefinites and strategies

inductive VanDerAuweraVanAlsenoy2016.Indefinite : Type

The indefinite used in a negative clause, by its dominant use: neutral, at home in positive and negative contexts alike, negatively polar, licensed by negation among other contexts, or negative, used predominantly for negation.

• neutral : Indefinite
• negativelyPolar : Indefinite
• negative : Indefinite

@[instance_reducible]

instance VanDerAuweraVanAlsenoy2016.instDecidableEqIndefinite : DecidableEq Indefinite

Equations

• VanDerAuweraVanAlsenoy2016.instDecidableEqIndefinite x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance VanDerAuweraVanAlsenoy2016.instReprIndefinite : Repr Indefinite

Equations

• VanDerAuweraVanAlsenoy2016.instReprIndefinite = { reprPrec := VanDerAuweraVanAlsenoy2016.instReprIndefinite.repr }

def VanDerAuweraVanAlsenoy2016.instReprIndefinite.repr : Indefinite → ℕ → Std.Format

Equations

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

inductive VanDerAuweraVanAlsenoy2016.Strategy : Type

[Kah96]'s strategies for a single negation with an indefinite, Table 1: a verbal negator with a neutral or a negatively polar indefinite, a negative indefinite alone, negative concord, and another construction such as a negative existential.

• verbalNegatorNeutral : Strategy
• verbalNegatorPolar : Strategy
• negativeIndefiniteAlone : Strategy
• concord : Strategy
• other : Strategy

@[instance_reducible]

instance VanDerAuweraVanAlsenoy2016.instDecidableEqStrategy : DecidableEq Strategy

Equations

• VanDerAuweraVanAlsenoy2016.instDecidableEqStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance VanDerAuweraVanAlsenoy2016.instReprStrategy : Repr Strategy

Equations

• VanDerAuweraVanAlsenoy2016.instReprStrategy = { reprPrec := VanDerAuweraVanAlsenoy2016.instReprStrategy.repr }

def VanDerAuweraVanAlsenoy2016.instReprStrategy.repr : Strategy → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance VanDerAuweraVanAlsenoy2016.instFintypeStrategy : Fintype Strategy

Equations

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

def VanDerAuweraVanAlsenoy2016.Strategy.indefinite : Strategy → Option Indefinite

The indefinite each strategy uses, if any.

Equations

• VanDerAuweraVanAlsenoy2016.Strategy.verbalNegatorNeutral.indefinite = some VanDerAuweraVanAlsenoy2016.Indefinite.neutral
• VanDerAuweraVanAlsenoy2016.Strategy.verbalNegatorPolar.indefinite = some VanDerAuweraVanAlsenoy2016.Indefinite.negativelyPolar
• VanDerAuweraVanAlsenoy2016.Strategy.negativeIndefiniteAlone.indefinite = some VanDerAuweraVanAlsenoy2016.Indefinite.negative
• VanDerAuweraVanAlsenoy2016.Strategy.concord.indefinite = some VanDerAuweraVanAlsenoy2016.Indefinite.negative
• VanDerAuweraVanAlsenoy2016.Strategy.other.indefinite = none

def VanDerAuweraVanAlsenoy2016.Strategy.toWALS : Strategy → Data.WALS.F115A.NegativeIndefiniteType

The WALS 115A value a strategy falls under: [Has13b]'s co-occurrence of predicate negation with a negative indefinite, in the wide sense of [Has97], covers every strategy with a verbal negator.

Equations

• VanDerAuweraVanAlsenoy2016.Strategy.verbalNegatorNeutral.toWALS = Data.WALS.F115A.NegativeIndefiniteType.predicateNegationAlsoPresent
• VanDerAuweraVanAlsenoy2016.Strategy.verbalNegatorPolar.toWALS = Data.WALS.F115A.NegativeIndefiniteType.predicateNegationAlsoPresent
• VanDerAuweraVanAlsenoy2016.Strategy.concord.toWALS = Data.WALS.F115A.NegativeIndefiniteType.predicateNegationAlsoPresent
• VanDerAuweraVanAlsenoy2016.Strategy.negativeIndefiniteAlone.toWALS = Data.WALS.F115A.NegativeIndefiniteType.noPredicateNegation
• VanDerAuweraVanAlsenoy2016.Strategy.other.toWALS = Data.WALS.F115A.NegativeIndefiniteType.negativeExistentialConstruction

theorem VanDerAuweraVanAlsenoy2016.toWALS_eq_predicateNegationAlsoPresent_iff (s : Strategy) : s.toWALS = Data.WALS.F115A.NegativeIndefiniteType.predicateNegationAlsoPresent ↔ s = Strategy.verbalNegatorNeutral ∨ s = Strategy.verbalNegatorPolar ∨ s = Strategy.concord

WALS co-occurrence is not negative concord: it is any strategy with a verbal negator, so the frequency of the WALS value does not measure the frequency of concord.

Strict and non-strict negative concord

inductive VanDerAuweraVanAlsenoy2016.Marking : Type

Whether the clausal negator accompanies a negative indefinite in a position: absent, the formula V, optional, (N) V, or obligatory, N V; the strictness scale.

• absent : Marking
• optional : Marking
• obligatory : Marking

@[instance_reducible]

instance VanDerAuweraVanAlsenoy2016.instDecidableEqMarking : DecidableEq Marking

Equations

• VanDerAuweraVanAlsenoy2016.instDecidableEqMarking x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def VanDerAuweraVanAlsenoy2016.instReprMarking.repr : Marking → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance VanDerAuweraVanAlsenoy2016.instReprMarking : Repr Marking

Equations

• VanDerAuweraVanAlsenoy2016.instReprMarking = { reprPrec := VanDerAuweraVanAlsenoy2016.instReprMarking.repr }

@[instance_reducible]

instance VanDerAuweraVanAlsenoy2016.instFintypeMarking : Fintype Marking

Equations

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

def VanDerAuweraVanAlsenoy2016.Marking.rank : Marking → Fin 3

The position of a marking on the strictness scale.

Equations

• VanDerAuweraVanAlsenoy2016.Marking.absent.rank = 0
• VanDerAuweraVanAlsenoy2016.Marking.optional.rank = 1
• VanDerAuweraVanAlsenoy2016.Marking.obligatory.rank = 2

@[instance_reducible]

instance VanDerAuweraVanAlsenoy2016.instLinearOrderMarking : LinearOrder Marking

Equations

• VanDerAuweraVanAlsenoy2016.instLinearOrderMarking = LinearOrder.lift' VanDerAuweraVanAlsenoy2016.Marking.rank VanDerAuweraVanAlsenoy2016.instLinearOrderMarking._proof_1

structure VanDerAuweraVanAlsenoy2016.System : Type

A negative concord system: the marking of a preverbal and of a postverbal negative indefinite, none when the position is unavailable, the asterisk of the formulas.

• preverbal : Option Marking
• postverbal : Option Marking

def VanDerAuweraVanAlsenoy2016.instDecidableEqSystem.decEq (x✝ x✝¹ : System) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance VanDerAuweraVanAlsenoy2016.instDecidableEqSystem : DecidableEq System

Equations

• VanDerAuweraVanAlsenoy2016.instDecidableEqSystem = VanDerAuweraVanAlsenoy2016.instDecidableEqSystem.decEq

@[instance_reducible]

instance VanDerAuweraVanAlsenoy2016.instReprSystem : Repr System

Equations

• VanDerAuweraVanAlsenoy2016.instReprSystem = { reprPrec := VanDerAuweraVanAlsenoy2016.instReprSystem.repr }

def VanDerAuweraVanAlsenoy2016.instReprSystem.repr : System → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev VanDerAuweraVanAlsenoy2016.Pattern : Type

A pattern with both positions available, the systems of Tables 6 and 9.

Equations

• VanDerAuweraVanAlsenoy2016.Pattern = (VanDerAuweraVanAlsenoy2016.Marking × VanDerAuweraVanAlsenoy2016.Marking)

def VanDerAuweraVanAlsenoy2016.Pattern.toSystem (p : Pattern) : System

The system of a pattern.

Equations

• p.toSystem = { preverbal := some p.1, postverbal := some p.2 }

def VanDerAuweraVanAlsenoy2016.System.HasConcord (s : System) : Prop

Concord is available in some construction.

Equations

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

def VanDerAuweraVanAlsenoy2016.System.IsStrict (s : System) : Prop

Strict negative concord: the clausal negator is obligatory whatever the position of the negative indefinite, (14).

Equations

• s.IsStrict = (s.preverbal = some VanDerAuweraVanAlsenoy2016.Marking.obligatory ∧ s.postverbal = some VanDerAuweraVanAlsenoy2016.Marking.obligatory)

def VanDerAuweraVanAlsenoy2016.System.IsNonStrict (s : System) : Prop

Non-strict negative concord: concord in some construction but not in all, (15).

Equations

• s.IsNonStrict = (s.HasConcord ∧ ¬s.IsStrict)

@[instance_reducible]

instance VanDerAuweraVanAlsenoy2016.instDecidableHasConcord (s : System) : Decidable s.HasConcord

Equations

• VanDerAuweraVanAlsenoy2016.instDecidableHasConcord s = id inferInstance

@[instance_reducible]

instance VanDerAuweraVanAlsenoy2016.instDecidableIsStrict (s : System) : Decidable s.IsStrict

Equations

• VanDerAuweraVanAlsenoy2016.instDecidableIsStrict s = id inferInstance

@[instance_reducible]

instance VanDerAuweraVanAlsenoy2016.instDecidableIsNonStrict (s : System) : Decidable s.IsNonStrict

Equations

• VanDerAuweraVanAlsenoy2016.instDecidableIsNonStrict s = id inferInstance

theorem VanDerAuweraVanAlsenoy2016.System.IsStrict.hasConcord {s : System} (h : s.IsStrict) : s.HasConcord

def VanDerAuweraVanAlsenoy2016.Pattern.NegativeEarly (p : Pattern) : Prop

The Negative Early principle: a postverbal negative indefinite, which leaves the negation late, calls for the clausal negator at least as much as a preverbal one.

Equations

• p.NegativeEarly = (p.1 ≤ p.2)

@[instance_reducible]

instance VanDerAuweraVanAlsenoy2016.instDecidablePredPatternNegativeEarly : DecidablePred Pattern.NegativeEarly

Equations

• VanDerAuweraVanAlsenoy2016.instDecidablePredPatternNegativeEarly p = { decide := (↑p.1.rank).ble ↑p.2.rank, reflects_decide := ⋯ }

def VanDerAuweraVanAlsenoy2016.spanish : Pattern

(19): the Spanish subtype, no negator with a preverbal negative indefinite and an obligatory one with a postverbal one.

Equations

• VanDerAuweraVanAlsenoy2016.spanish = (VanDerAuweraVanAlsenoy2016.Marking.absent, VanDerAuweraVanAlsenoy2016.Marking.obligatory)

def VanDerAuweraVanAlsenoy2016.brabanticDutch : Pattern

(30): Belgian Brabantic Dutch, an optional negator with a postverbal negative indefinite.

Equations

• VanDerAuweraVanAlsenoy2016.brabanticDutch = (VanDerAuweraVanAlsenoy2016.Marking.absent, VanDerAuweraVanAlsenoy2016.Marking.optional)

def VanDerAuweraVanAlsenoy2016.french : Pattern

(32): French and African American English, the negator optional in both positions.

Equations

• VanDerAuweraVanAlsenoy2016.french = (VanDerAuweraVanAlsenoy2016.Marking.optional, VanDerAuweraVanAlsenoy2016.Marking.optional)

def VanDerAuweraVanAlsenoy2016.olderSlavic : Pattern

(28): older Slavic and Catalan, the negator optional preverbally and obligatory postverbally.

Equations

• VanDerAuweraVanAlsenoy2016.olderSlavic = (VanDerAuweraVanAlsenoy2016.Marking.optional, VanDerAuweraVanAlsenoy2016.Marking.obligatory)

def VanDerAuweraVanAlsenoy2016.nonStrictSubtypes : List Pattern

Table 9: the non-strict subtypes with both positions available.

Equations

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

theorem VanDerAuweraVanAlsenoy2016.nonStrict_negativeEarly_iff (p : Pattern) : p.toSystem.IsNonStrict ∧ p.NegativeEarly ↔ p ∈ nonStrictSubtypes

Table 9 is exactly the non-strict patterns respecting Negative Early.

def VanDerAuweraVanAlsenoy2016.stages : List Pattern

Table 6: the diachrony from Latin, with negative indefinites alone, through older Romance, Spanish and older Slavic to modern Slavic and Romanian, with strict concord.

Equations

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

theorem VanDerAuweraVanAlsenoy2016.stages_isChain : List.IsChain (fun (x1 x2 : Pattern) => x1 ≤ x2) stages

The diachrony ascends the strictness scale in both positions.

theorem VanDerAuweraVanAlsenoy2016.negativeEarly_of_mem_stages (p : Pattern) : p ∈ stages → p.NegativeEarly

Every stage respects Negative Early: the verbal negator appears with the postverbal negative indefinite before it appears with the preverbal one.

def VanDerAuweraVanAlsenoy2016.informalCatalan : Pattern

(29): informal Catalan has the Spanish subtype, formal Catalan strict concord.

Equations

• VanDerAuweraVanAlsenoy2016.informalCatalan = VanDerAuweraVanAlsenoy2016.spanish

def VanDerAuweraVanAlsenoy2016.formalCatalan : Pattern

Equations

• VanDerAuweraVanAlsenoy2016.formalCatalan = (VanDerAuweraVanAlsenoy2016.Marking.obligatory, VanDerAuweraVanAlsenoy2016.Marking.obligatory)

theorem VanDerAuweraVanAlsenoy2016.informalCatalan_lt_formalCatalan : informalCatalan ≤ formalCatalan ∧ informalCatalan ≠ formalCatalan

Catalan is changing from strict to Spanish-style concord, down the strictness scale: the diachrony has no single direction.

Systems with an unavailable position

def VanDerAuweraVanAlsenoy2016.icelandic : System

(26): Icelandic neinn, no preverbal position and obligatory concord postverbally.

Equations

• VanDerAuweraVanAlsenoy2016.icelandic = { preverbal := none, postverbal := some VanDerAuweraVanAlsenoy2016.Marking.obligatory }

def VanDerAuweraVanAlsenoy2016.welsh : System

(39): Welsh, no preverbal position and optional concord postverbally.

Equations

• VanDerAuweraVanAlsenoy2016.welsh = { preverbal := none, postverbal := some VanDerAuweraVanAlsenoy2016.Marking.optional }

def VanDerAuweraVanAlsenoy2016.westernArmenian : System

(38): Western Armenian, optional concord preverbally and no postverbal position.

Equations

• VanDerAuweraVanAlsenoy2016.westernArmenian = { preverbal := some VanDerAuweraVanAlsenoy2016.Marking.optional, postverbal := none }

theorem VanDerAuweraVanAlsenoy2016.isNonStrict_table8 : icelandic.IsNonStrict ∧ welsh.IsNonStrict ∧ westernArmenian.IsNonStrict

Table 8: the subtypes with one position unavailable are non-strict, concord depending on word order even where it is obligatory.