de Swart and Sag (2002): Negation and Negative Concord in Romance

De Swart and Sag take the French n-words personne, rien and aucun N to be negative quantifiers and derive the two readings of a clause with two of them from two ways of composing quantifiers. Iteration, ordinary function application, puts one in the scope of the other and gives the double negation reading; resumption absorbs both into one quantifier over pairs and gives the concord reading. Only anti-additive quantifiers resume, which no is and few is not. Sentential negation is anti-additive too, a quantifier of type 0 that binds no variable, so it can join a resumption and is then semantically empty; standard French keeps pas out of resumption, so pas with an n-word reads only as a double negation.

Main results

• reading_iteration_iff, reading_resumption_iff: the double negation reading of two n-words is every·some and the concord reading is no·some.
• reading_resumption_and_not_iteration: the two readings differ.
• isAntiAdditive_no, not_isAntiAdditive_few: no is anti-additive and few is not.
• mem_aucun_and_isAntiAdditive_iff: of the readings of aucun, the anti-additive one is no.
• negReading_iteration_iff: negation iterated over an n-word gives the existential.

Implementation notes

• Resumption is binary, Quantifier.Polyadic.resume; the ternary and quaternary chains of the paper's (15) and (16) are not formalized.
• The HPSG retrieval of §4 is represented by its outcome, the Mode in which the stored quantifiers compose.

References

• [dSS02]
• [PW06]
• [vdW97]

inductive DeSwartSag2002.Mode : Type

Retrieval composes two n-words by iteration, function application, or by resumption into a single quantifier over pairs ((29)).

• iteration : Mode
• resumption : Mode

@[instance_reducible]

instance DeSwartSag2002.instDecidableEqMode : DecidableEq Mode

Equations

• DeSwartSag2002.instDecidableEqMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance DeSwartSag2002.instReprMode : Repr Mode

Equations

• DeSwartSag2002.instReprMode = { reprPrec := DeSwartSag2002.instReprMode.repr }

def DeSwartSag2002.instReprMode.repr : Mode → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance DeSwartSag2002.instFintypeMode : Fintype Mode

Equations

• DeSwartSag2002.instFintypeMode = { elems := { val := ↑DeSwartSag2002.Mode.enumList, nodup := DeSwartSag2002.Mode.enumList_nodup }, complete := DeSwartSag2002.instFintypeMode._proof_1 }

def DeSwartSag2002.reading {α : Type u} [Fintype α] : Mode → (α → Prop) → (α → Prop) → (α → α → Prop) → Prop

The reading of a clause whose two arguments are n-words with restrictors A and B and whose verb denotes R, as Personne n'aime personne ((13), (14)).

Equations

• DeSwartSag2002.reading DeSwartSag2002.Mode.iteration x✝² x✝¹ x✝ = Quantifier.Polyadic.iterate Quantifier.GQ.no Quantifier.GQ.no x✝² x✝¹ x✝
• DeSwartSag2002.reading DeSwartSag2002.Mode.resumption x✝² x✝¹ x✝ = Quantifier.Polyadic.resume Quantifier.GQ.Family.no x✝² x✝¹ x✝

theorem DeSwartSag2002.reading_iteration_iff {α : Type u} [Fintype α] {A B : α → Prop} {R : α → α → Prop} : reading Mode.iteration A B R ↔ Quantifier.Polyadic.iterate Quantifier.GQ.every Quantifier.GQ.some A B R

The double negation reading, ¬∃x¬∃y R(x, y) ((13)), is every·some, as the gloss of (33b) has it: everyone loves the son of someone.

theorem DeSwartSag2002.reading_resumption_iff {α : Type u} [Fintype α] {A B : α → Prop} {R : α → α → Prop} : reading Mode.resumption A B R ↔ Quantifier.Polyadic.iterate Quantifier.GQ.no Quantifier.GQ.some A B R

The concord reading, ¬∃x∃y R(x, y) ((14)), is no·some ((17)).

theorem DeSwartSag2002.reading_resumption_and_not_iteration : (reading Mode.resumption (fun (x : Fin 1) => True) (fun (x : Fin 1) => True) fun (x x_1 : Fin 1) => False) ∧ ¬reading Mode.iteration (fun (x : Fin 1) => True) (fun (x : Fin 1) => True) fun (x x_1 : Fin 1) => False

The two readings differ: of one individual who loves no one, Personne n'aime personne is true on its concord reading and false on its double negation reading.

Anti-additivity

Concord is restricted to anti-additive quantifiers such as personne 'no one', to the exclusion of the merely downward-entailing peu 'few'. Negation is anti-additive as well (NaturalLogic.isAntiAdditive_compl).

theorem DeSwartSag2002.isAntiAdditive_no {α : Type u} (A : α → Prop) : NaturalLogic.IsAntiAdditive (Quantifier.GQ.no A)

No is anti-additive in its scope: none of A is in S ∪ S' iff none is in S and none in S'.

theorem DeSwartSag2002.not_isAntiAdditive_few : ¬NaturalLogic.IsAntiAdditive (Quantifier.GQ.few fun (x : Fin 3) => True)

Few is downward-entailing (Quantifier.GQ.scopeAntitone_few) but not anti-additive: of three individuals, few are 0 and few are 1, but not few are 0 or 1.

theorem DeSwartSag2002.not_isAntiAdditive_some : ¬NaturalLogic.IsAntiAdditive (Quantifier.GQ.some fun (x : PUnit.{u + 1}) => True)

Some is not anti-additive: of one individual, some is in ⊤ ∪ ⊥ but none is in ⊥.

theorem DeSwartSag2002.mem_aucun_and_isAntiAdditive_iff {d : Quantifier.GQ.Family} : (d ∈ Semantics.Denotes.denote French.Determiners.QuantityWord.aucun ∧ ∀ (β : Type u) [inst : Fintype β] (A : β → Prop), NaturalLogic.IsAntiAdditive (d β A)) ↔ d = Quantifier.GQ.Family.no

Of the readings of aucun, the one that is anti-additive on every finite domain, as a concord item must be, is the negative quantifier.

Negation as a quantifier of type 0

A negator binds no variable, so when it joins the resumption of n-words it leaves the resumptive quantifier unchanged: in concord, negation is semantically empty (§6.1). The same holds of sans 'without' (§6.2).

def DeSwartSag2002.negReading {α : Type u} : Mode → (α → Prop) → (α → Prop) → Prop

The reading of a negator with one n-word: negation iterated over the n-word, or absorbed into its resumption.

Equations

• DeSwartSag2002.negReading DeSwartSag2002.Mode.iteration x✝¹ x✝ = ¬Quantifier.GQ.no x✝¹ x✝
• DeSwartSag2002.negReading DeSwartSag2002.Mode.resumption x✝¹ x✝ = Quantifier.GQ.no x✝¹ x✝

theorem DeSwartSag2002.negReading_iteration_iff {α : Type u} {A S : α → Prop} : negReading Mode.iteration A S ↔ Quantifier.GQ.some A S

Negation iterated over an n-word gives the existential, the only reading of standard French Il ne va pas nulle part 'he goes somewhere' ((36a)), since constraint (40) keeps pas out of resumption.

theorem DeSwartSag2002.negReading_resumption_iff {α : Type u} {A S : α → Prop} : negReading Mode.resumption A S ↔ Quantifier.GQ.no A S

Absorbed into the n-word's resumption, the negator adds nothing, as sans in Anne est partie sans rien dire 'Anne left without saying anything' ((56)).