Zeijlstra (2004): Sentential Negation and Negative Concord

Zeijlstra derives negative concord from syntactic agreement. Each negative element carries a negative feature, interpretable [iNEG] or uninterpretable [uNEG], and an element carrying [uNEG] must be checked by a c-commanding element carrying [iNEG]. In concord languages the n-words carry [uNEG] and are non-negative indefinites; the operator that checks them is negation with existential closure, which binds their variables. A clause whose highest negative element carries [uNEG] has a covert operator above it. Languages differ in the feature of the negative marker: [uNEG] in strict concord languages such as Czech and [iNEG] in non-strict ones such as Italian, while in double negation languages such as Standard Dutch every negative element carries [iNEG] and n-words are negative quantifiers.

In Czech the n-word means the same before and after the negated verb, while an Italian n-word before non yields double negation. The concord reading of two n-words is de Swart and Sag's resumption of no, which Zeijlstra reduces to an iteration; the two analyses differ not on the truth conditions of concord but on whether a concord language has the double negation reading as well.

Main results

• meaning_of_forall_u: in a strict concord language every negative clause has one negation, wherever its marker and n-words stand.
• meaning_marker_nword, meaning_nword_marker: Italian non before an n-word gives concord and after it double negation.
• meaning_concord_iff_resumption, meaning_dn_iff_iteration: concord is de Swart and Sag's resumption and double negation their iteration.
• mem_nessuno_and_scopeMonotone_iff: of the readings of an n-word, Zeijlstra's is the non-negative one.

Implementation notes

• A clause is its negative elements in c-command order over a nucleus that takes the individuals its n-words introduce; movement, Multiple Agree and phases are represented by that order. An n-word's variable is closed by the nearest [iNEG] element above it, and since only n-words and [uNEG] markers intervene, closing it in place is equivalent.
• Example numbers are those of chapter 8 unless marked.
• The summary of §8.1.4 assigns the markers of strict and non-strict concord the opposite features; the derivations of §§8.1.1–8.1.2 fix them as here.

References

• [Zei04]
• [dSS02]

inductive Zeijlstra2004.Feature : Type

A negative feature is interpretable, [iNEG], or uninterpretable, [uNEG].

• i : Feature
• u : Feature

@[instance_reducible]

instance Zeijlstra2004.instDecidableEqFeature : DecidableEq Feature

Equations

• Zeijlstra2004.instDecidableEqFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Zeijlstra2004.instReprFeature : Repr Feature

Equations

• Zeijlstra2004.instReprFeature = { reprPrec := Zeijlstra2004.instReprFeature.repr }

def Zeijlstra2004.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

• Zeijlstra2004.instReprFeature.repr Zeijlstra2004.Feature.i prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Zeijlstra2004.Feature.i")).group prec✝
• Zeijlstra2004.instReprFeature.repr Zeijlstra2004.Feature.u prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Zeijlstra2004.Feature.u")).group prec✝

inductive Zeijlstra2004.NegElement (α : Type u) : Type u

A negative element of a clause is a negative marker or an n-word with its restrictor, each carrying a negative feature.

• marker {α : Type u} (f : Feature) : NegElement α
• nword {α : Type u} (f : Feature) (A : α → Prop) : NegElement α

def Zeijlstra2004.NegElement.feature {α : Type u} : NegElement α → Feature

The negative feature of an element.

Equations

• (Zeijlstra2004.NegElement.marker f).feature = f
• (Zeijlstra2004.NegElement.nword f A).feature = f

def Zeijlstra2004.NegElement.isNword {α : Type u} : NegElement α → Bool

Whether an element is an n-word.

Equations

• (Zeijlstra2004.NegElement.marker f).isNword = false
• (Zeijlstra2004.NegElement.nword f A).isNword = true

def Zeijlstra2004.interp {α : Type u} : List (NegElement α) → (List α → Prop) → Prop

The interpretation of negative elements in c-command order over a nucleus that takes the individuals the n-words introduce. A marker carrying [iNEG] is negation and one carrying [uNEG] is empty; an n-word carrying [uNEG] is an indefinite, existentially closed, and one carrying [iNEG] a negative quantifier.

Equations

• Zeijlstra2004.interp [] x✝ = x✝ []
• Zeijlstra2004.interp (Zeijlstra2004.NegElement.marker Zeijlstra2004.Feature.i :: es) x✝ = ¬Zeijlstra2004.interp es x✝
• Zeijlstra2004.interp (Zeijlstra2004.NegElement.marker Zeijlstra2004.Feature.u :: es) x✝ = Zeijlstra2004.interp es x✝
• Zeijlstra2004.interp (Zeijlstra2004.NegElement.nword Zeijlstra2004.Feature.u A :: es) x✝ = Quantifier.GQ.some A fun (x : α) => Zeijlstra2004.interp es fun (xs : List α) => x✝ (x :: xs)
• Zeijlstra2004.interp (Zeijlstra2004.NegElement.nword Zeijlstra2004.Feature.i A :: es) x✝ = Quantifier.GQ.no A fun (x : α) => Zeijlstra2004.interp es fun (xs : List α) => x✝ (x :: xs)

def Zeijlstra2004.meaning {α : Type u} (es : List (NegElement α)) (P : List α → Prop) : Prop

The meaning of a clause. When its highest negative element carries [uNEG], a covert operator above it checks the feature and contributes negation.

Equations

• Zeijlstra2004.meaning es P = if Option.map Zeijlstra2004.NegElement.feature es.head? = some Zeijlstra2004.Feature.u then ¬Zeijlstra2004.interp es P else Zeijlstra2004.interp es P

Strict concord

theorem Zeijlstra2004.interp_filter_isNword {α : Type u} {es : List (NegElement α)} (hu : ∀ e ∈ es, e.feature = Feature.u) (P : List α → Prop) : interp es P ↔ interp (List.filter NegElement.isNword es) P

With every feature uninterpretable, the markers contribute nothing.

theorem Zeijlstra2004.meaning_of_forall_u {α : Type u} {es : List (NegElement α)} (hne : es ≠ []) (hu : ∀ e ∈ es, e.feature = Feature.u) (P : List α → Prop) : meaning es P ↔ ¬interp (List.filter NegElement.isNword es) P

In a strict concord language, where markers and n-words carry [uNEG], every negative clause has the single negation of the covert operator over its n-words, wherever the marker stands: Czech Nevolá nikdo ((20)) and Nikdo nevolá ((23)) both mean 'nobody is calling'.

Non-strict concord and double negation

theorem Zeijlstra2004.meaning_marker_nword {α : Type u} {A : α → Prop} {P : List α → Prop} : meaning [NegElement.marker Feature.i, NegElement.nword Feature.u A] P ↔ Quantifier.GQ.no A fun (x : α) => P [x]

Italian Non ha telefonato nessuno 'nobody called' ((63)): non carries [iNEG] and checks the n-word below it.

theorem Zeijlstra2004.meaning_nword_marker {α : Type u} {A : α → Prop} {P : List α → Prop} : meaning [NegElement.nword Feature.u A, NegElement.marker Feature.i] P ↔ Quantifier.GQ.every A fun (x : α) => P [x]

Italian Nessuno non ha telefonato 'nobody didn't call' ((36b) of chapter 7): the n-word above non needs the covert operator, and non negates again, so the concord reading 'nobody called' is out ((66)).

theorem Zeijlstra2004.meaning_dn_nword_marker {α : Type u} {A : α → Prop} {P : List α → Prop} : meaning [NegElement.nword Feature.i A, NegElement.marker Feature.i] P ↔ Quantifier.GQ.every A fun (x : α) => P [x]

Standard Dutch Niemand loopt niet 'everybody walks' ((84)): both negative elements carry [iNEG].

Comparison with de Swart and Sag

theorem Zeijlstra2004.meaning_concord_iff_resumption {α : Type u} [Fintype α] {A B : α → Prop} {P : List α → Prop} : meaning [NegElement.nword Feature.u A, NegElement.nword Feature.u B] P ↔ DeSwartSag2002.reading DeSwartSag2002.Mode.resumption A B fun (x y : α) => P [x, y]

The concord reading of two n-words under the covert operator, Italian Nessuno ha telefonato a nessuno 'nobody called anybody' ((68)), is de Swart and Sag's resumption of no; Zeijlstra's objection that this resumption reduces to an iteration ((29) of chapter 7) is Quantifier.Polyadic.resume_no_iff.

theorem Zeijlstra2004.meaning_dn_iff_iteration {α : Type u} [Fintype α] {A B : α → Prop} {P : List α → Prop} : meaning [NegElement.nword Feature.i A, NegElement.nword Feature.i B] P ↔ DeSwartSag2002.reading DeSwartSag2002.Mode.iteration A B fun (x y : α) => P [x, y]

Two n-words carrying [iNEG] in a double negation language give de Swart and Sag's iteration of no.

theorem Zeijlstra2004.meaning_concord_and_not_iteration : (meaning [NegElement.nword Feature.u fun (x : Fin 1) => True, NegElement.nword Feature.u fun (x : Fin 1) => True] fun (x : List (Fin 1)) => False) ∧ ¬DeSwartSag2002.reading DeSwartSag2002.Mode.iteration (fun (x : Fin 1) => True) (fun (x : Fin 1) => True) fun (x x_1 : Fin 1) => False

Unlike de Swart and Sag's, Zeijlstra's analysis gives a concord clause with two n-words no double negation reading: of one individual who called no one, its meaning holds and the iteration of no fails.

The readings of n-words

N-words are non-negative indefinites, so of the readings the fragments list for an n-word, Zeijlstra's is the one that is upward monotone in its scope.

theorem Zeijlstra2004.not_scopeMonotone_no : ¬Quantifier.GQ.no.ScopeMonotone

No is not upward monotone in its scope: of one individual, none is in ⊥ but one is in ⊤.

theorem Zeijlstra2004.mem_nessuno_and_scopeMonotone_iff {d : Quantifier.GQ.Family} : (d ∈ Semantics.Denotes.denote Italian.Determiners.QuantityWord.nessuno ∧ ∀ (β : Type u) [inst : Fintype β], (d β).ScopeMonotone) ↔ d = Quantifier.GQ.Family.some

Of the readings of Italian nessuno, the one upward monotone in its scope on every finite domain is the indefinite.

theorem Zeijlstra2004.mem_zadny_and_scopeMonotone_iff {d : Quantifier.GQ.Family} : (d ∈ Semantics.Denotes.denote Czech.Determiners.QuantityWord.zadny ∧ ∀ (β : Type u) [inst : Fintype β], (d β).ScopeMonotone) ↔ d = Quantifier.GQ.Family.some

Of the readings of Czech žádný, the one upward monotone in its scope on every finite domain is the indefinite.