Bylinina and Nouwen (2018): On zero and semantic plurality

This file formalizes the argument of Bylinina and Nouwen that zero is a numeral, not a negative quantifier like no, and that its semantics needs an empty plurality. A numeral contributes a cardinality, ∃x[#x = n ∧ A(x) ∧ B(x)], with an at least reading ((20)–(28)). With Link's pluralization * ((29)), which excludes the sum of the empty set, zero A B is a contradiction ((36)); with the full lattice × ((30)), which has the empty plurality ⊥, it is a tautology ((37), (39)), and exhaustifying it against the higher numerals gives no A B ((40)).

The polarity of zero follows from the split between the two meanings. Weak negative polarity items need their environment non-trivially downward entailing, downward and not upward entailing, in the meaning below the exhaustivity operator, and strong items in the meaning above it as well ((53)). Below the operator zero A B is a tautology, downward and upward entailing at once, so zero licenses neither kind of item ((54)), while few licenses weak items only ((48)) and no both. An analysis with a basic exactly meaning has no such split: Kennedy's degree quantifier zero, λP. max(P) = 0, is no A B under × ((73)) and never true under * ((72)), and as no it licenses both kinds of item (Section 6.3).

The empty plurality is needed elsewhere: under × a downward monotone degree quantifier such as fewer than ten is downward monotone in its scope, under * it is not ((65), (66)). On scope the two analyses agree (Section 6.2): exhaustifying the lower bound at a site and raising Kennedy's quantifier to that site give the same reading, so the split-scope reading (77b) of every student read zero books, which the sentence lacks ((78)), is blocked only for the degree quantifier, by the Heim-Kennedy generalization ((80)).

Main results

• exhAgainst_zero_iff_no, zero_mem_countDegrees: exhaustified zero is no, and the unexhaustified zero is a tautology.
• not_licenses_zero, rows_predicted: zero licenses no polarity item, few weak ones only and no both, as the paper's judgments have it.
• kennedyZero_eq_nobody: Kennedy's zero is the context of no.
• antitone_maxIn_countDegrees, not_antitone_maxIn_countDegrees_sdiff: fewer than ten is downward monotone with × and not with *.
• countDegrees_plural_eq_Iic_comp: a count's measured degree property is that of its pluralities under ×.

Implementation notes

• Pluralities are the finite sets of atoms, and plural Z is Mereology.FullAlgClosure of the singletons of Z, the full lattice ×Z; without the empty sum it is Link's *Z, Mereology.AlgClosure of them (plural_sdiff_empty). A distributive predicate B holds of a plurality that is in plural B.
• Degrees are natural numbers; Kennedy's numeral is Degree.MaxIn {n} and its two scopes are Degree.LowScope and Degree.HighScope. Exhaustification against the higher numerals is Exhaustification.exhAgainst (· < ·).
• Licensing is the library's: zero is a scalar PolarityItem.Licenser, and every item needs the meaning below the exhaustivity operator non-trivially downward entailing. For strong items the library asks Zwarts's anti-additivity of the meaning above it where (53) asks for non-trivial downward entailment; zero fails the first condition, so the two agree on it.

TODO

The tag-question and neg-inversion contrasts (Section 2), the existential operator E for bare plurals ((58)), plural definites with ⊥ ((60)–(64)), and the stipulation max(∅) = 0 that would let the de-Fregean analysis do without ⊥ (Section 6.1) are not formalized.

References

• [BN18]
• [Lin83]
• [Gaj11]
• [Lah98]
• [Ken15]
• [Hei00]

Pluralities and numerals

def BylininaNouwen2018.plural {α : Type u_1} [DecidableEq α] (Z : Set α) : Set (Finset α)

The pluralities of members of Z, the full closure ×Z of its singletons ((30)), are the sums ⊔X of the subsets X ⊆ Z, the empty sum ⊥ among them.

Equations

• BylininaNouwen2018.plural Z = {x : Finset α | Mereology.FullAlgClosure (fun (x : Finset α) => x ∈ (fun (x : α) => {x}) '' Z) x}

@[simp]

theorem BylininaNouwen2018.mem_plural {α : Type u_1} [DecidableEq α] {Z : Set α} {x : Finset α} : x ∈ plural Z ↔ ↑x ⊆ Z

theorem BylininaNouwen2018.plural_sdiff_empty {α : Type u_1} [DecidableEq α] (Z : Set α) : plural Z \ {∅} = {x : Finset α | Mereology.AlgClosure (fun (x : Finset α) => x ∈ (fun (x : α) => {x}) '' Z) x}

Without the empty sum ×Z is Link's *Z ((29)).

theorem BylininaNouwen2018.plural_inter {α : Type u_1} [DecidableEq α] (A B : Set α) : plural A ∩ plural B = plural (A ∩ B)

def BylininaNouwen2018.countDegrees {α : Type u_1} [DecidableEq α] (A : Set α) (C : Set (Finset α)) : Set ℕ

The degree property λi. ∃x[#x = i ∧ A(x) ∧ C(x)] of the pluralities of members of A that are C, which a numeral n holds of at its lower bound ((27)) and Kennedy's numeral quantifies over ((71)).

Equations

• BylininaNouwen2018.countDegrees A C = Finset.card '' (BylininaNouwen2018.plural A ∩ C)

theorem BylininaNouwen2018.isLowerSet_countDegrees_plural {α : Type u_1} [DecidableEq α] (A B : Set α) : IsLowerSet (countDegrees A (plural B))

With a distributive predicate the degree property is a lower set, so the numeral has an at least reading ((20), (22)).

theorem BylininaNouwen2018.countDegrees_singleton {α : Type u_1} [DecidableEq α] {A : Set α} {s : Finset α} (hs : ↑s ⊆ A) : countDegrees A {s} = {s.card}

With a collective predicate true of the plurality s alone, the degree property holds at #s alone, so the numeral has no at least reading.

theorem BylininaNouwen2018.countDegrees_plural_eq_Iic {α : Type u_1} [DecidableEq α] {A B : Set α} (h : (A ∩ B).Finite) : countDegrees A (plural B) = Set.Iic (A ∩ B).ncard

With finitely many members of A ∩ B the degree property under × is {0, …, n} for their number n ((73)), the measured degree property of Degree.LowScope.

Zero

Under * the at least zero is a contradiction and under × a tautology; exhaustification against the higher numerals turns the tautology into no.

theorem BylininaNouwen2018.zero_notMem_countDegrees_sdiff {α : Type u_1} [DecidableEq α] (A B : Set α) : 0 ∉ countDegrees A (plural B \ {∅})

Under *, zero A B is a contradiction ((36)).

theorem BylininaNouwen2018.zero_mem_countDegrees {α : Type u_1} [DecidableEq α] (A B : Set α) : 0 ∈ countDegrees A (plural B)

Under ×, zero A B is a tautology ((37), (39)).

theorem BylininaNouwen2018.maxIn_singleton_iff_exhAgainst {D : Type u_2} [LinearOrder D] {P : Set D} {n : D} : Degree.MaxIn {n} P ↔ Exhaustification.exhAgainst (fun (x1 x2 : D) => x1 < x2) (fun (x : D) => x ∈ P) n

Kennedy's quantifier holds of a degree property when the lower bound, exhaustified against the higher numerals, does: both say that n is its greatest degree.

theorem BylininaNouwen2018.maxIn_zero_countDegrees_iff {α : Type u_1} [DecidableEq α] {A B : Set α} : Degree.MaxIn {0} (countDegrees A (plural B)) ↔ Quantifier.GQ.no A B

Under ×, Kennedy's zero A B is no A B ((73)).

theorem BylininaNouwen2018.not_maxIn_zero_countDegrees_sdiff {α : Type u_1} [DecidableEq α] (A B : Set α) : ¬Degree.MaxIn {0} (countDegrees A (plural B \ {∅}))

Under *, Kennedy's zero A B is never true ((72)), since the degree property lacks 0.

theorem BylininaNouwen2018.exhAgainst_zero_iff_no {α : Type u_1} [DecidableEq α] {A B : Set α} : Exhaustification.exhAgainst (fun (x1 x2 : ℕ) => x1 < x2) (fun (x : ℕ) => x ∈ countDegrees A (plural B)) 0 ↔ Quantifier.GQ.no A B

Exhaustified zero A B is no A B ((40)).

Negative polarity items

Zero is a scalar licenser, the at least numeral below the exhaustivity operator and the numeral exhaustified against the higher numerals above it, so the library's licensing applies to it as stated in (53).

def BylininaNouwen2018.zero : PolarityItem.Licenser

Zero NP over a restrictor, the at least numeral and its exhaustification against the higher numerals ((39), (40)).

Equations

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

theorem BylininaNouwen2018.exhaustified_zero : zero.exhaustified = PolarityItem.LicensingContext.nobody.licenser

Above the exhaustivity operator zero is no, non-trivially downward entailing ((54a)).

theorem BylininaNouwen2018.isStrawsonUE_zero : zero.IsStrawsonUE

Below it zero is a tautology, downward and upward entailing at once ((54b)).

@[simp]

theorem BylininaNouwen2018.not_licenses_zero (e : PolarityItem) : ¬zero.Licenses e

So zero licenses no negative polarity item, weak or strong.

@[instance_reducible]

instance BylininaNouwen2018.instDecidablePredPolarityItemLicensesZero : DecidablePred zero.Licenses

Equations

• BylininaNouwen2018.instDecidablePredPolarityItemLicensesZero e = isFalse ⋯

def BylininaNouwen2018.kennedyZero : PolarityItem.Licenser

Kennedy's zero, with its exactly meaning basic and so no exhaustivity operator to split its meaning.

Equations

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

theorem BylininaNouwen2018.kennedyZero_eq_nobody : kennedyZero = PolarityItem.LicensingContext.nobody.licenser

Kennedy's zero is no ((73)), so it licenses what no licenses, strong items included, against (13), (15) and (16) (Section 6.3).

inductive BylininaNouwen2018.Licenser : Type

The paper's licensers.

• no : Licenser
• few : Licenser
• zero : Licenser

@[instance_reducible]

instance BylininaNouwen2018.instDecidableEqLicenser : DecidableEq Licenser

Equations

• BylininaNouwen2018.instDecidableEqLicenser x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def BylininaNouwen2018.instReprLicenser.repr : Licenser → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BylininaNouwen2018.instReprLicenser : Repr Licenser

Equations

• BylininaNouwen2018.instReprLicenser = { reprPrec := BylininaNouwen2018.instReprLicenser.repr }

noncomputable def BylininaNouwen2018.Licenser.denote : Licenser → PolarityItem.Licenser

The library's operator for each licenser.

Equations

• BylininaNouwen2018.Licenser.no.denote = PolarityItem.LicensingContext.nobody.licenser
• BylininaNouwen2018.Licenser.few.denote = PolarityItem.LicensingContext.few.licenser
• BylininaNouwen2018.Licenser.zero.denote = BylininaNouwen2018.zero

@[instance_reducible]

instance BylininaNouwen2018.instDecidablePredPolarityItemLicensesDenote (L : Licenser) : DecidablePred L.denote.Licenses

Equations

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

structure BylininaNouwen2018.Row : Type

A sentence of the paper records its licenser, its polarity item as an entry of the English fragment, and the judgment.

• licenser : Licenser
• item : PolarityItem
• judgment : Judgment

def BylininaNouwen2018.Row.ofDatum (ex : Datum) : List Row

A sentence gives a row for each of its polarity items, as entries of the English fragment.

Equations

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

def BylininaNouwen2018.rows : List Row

Equations

• BylininaNouwen2018.rows = List.flatMap BylininaNouwen2018.Row.ofDatum BylininaNouwen2018.Examples.all

theorem BylininaNouwen2018.rows_predicted (r : Row) : r ∈ rows → (r.judgment = Judgment.acceptable ↔ r.licenser.denote.Licenses r.item)

Every judgment is the library's verdict, a sentence being acceptable exactly when its licenser licenses its item.

Downward monotone degree quantifiers

A degree quantifier at a lower set, fewer than ten or at most ten, is downward monotone in its scope under ×, since 0 keeps the degree property nonempty, and not under * ((65), (66)).

theorem BylininaNouwen2018.antitone_maxIn_countDegrees {α : Type u_1} [DecidableEq α] {U : Set ℕ} (hU : IsLowerSet U) {A : Set α} (hA : A.Finite) : Antitone fun (B : Set α) => Degree.MaxIn U (countDegrees A (plural B))

theorem BylininaNouwen2018.not_antitone_maxIn_countDegrees_sdiff : ¬Antitone fun (B : Set Unit) => Degree.MaxIn (Set.Iio 10) (countDegrees Set.univ (plural B \ {∅}))

Under *, fewer than ten students passed is false when no student passed.

Scope

Exhaustifying the lower bound at a site and raising Kennedy's quantifier to that site give the same reading ((75), (76)), whatever degree property the scope abstracts, so the analyses differ only in the sites they reach.

theorem BylininaNouwen2018.exhAgainst_iff_highScope {ι : Type u_2} {Q : Quantifier.NP ι} {P : ι → Set ℕ} {n : ℕ} : Exhaustification.exhAgainst (fun (x1 x2 : ℕ) => x1 < x2) (fun (m : ℕ) => Q fun (x : ι) => m ∈ P x) n ↔ Degree.HighScope (Degree.MaxIn {n}) Q P

Exhaustification above Q is the numeral raised over Q.

theorem BylininaNouwen2018.exhAgainst_iff_lowScope {ι : Type u_2} {Q : Quantifier.NP ι} {P : ι → Set ℕ} {n : ℕ} : (Q fun (x : ι) => Exhaustification.exhAgainst (fun (x1 x2 : ℕ) => x1 < x2) (fun (x_1 : ℕ) => x_1 ∈ P x) n) ↔ Degree.LowScope (Degree.MaxIn {n}) Q P

Exhaustification below Q is the numeral in situ under Q.

theorem BylininaNouwen2018.countDegrees_plural_eq_Iic_comp {α : Type u_1} [DecidableEq α] {ι : Type u_2} {A : Set α} {B : ι → Set α} (h : ∀ (i : ι), (A ∩ B i).Finite) : (fun (i : ι) => countDegrees A (plural (B i))) = Set.Iic ∘ fun (i : ι) => (A ∩ B i).ncard

A count's measured degree property is that of its full pluralities. With finitely many members of each A ∩ B i, the pluralities of A that are B i have the degrees Iic of their number, so Degree.LowScope and Degree.HighScope at Iic ∘ the count are the readings of the plural model.

theorem BylininaNouwen2018.highScope_every_not_lowScope : Degree.HighScope (Degree.MaxIn {0}) (Quantifier.GQ.every fun (x : Fin 2) => True) (Set.Iic ∘ fun (i : Fin 2) => 4 * ↑i) ∧ ¬Degree.LowScope (Degree.MaxIn {0}) (Quantifier.GQ.every fun (x : Fin 2) => True) (Set.Iic ∘ fun (i : Fin 2) => 4 * ↑i)

Over every student the split-scope reading (77b), that not every student read a book, is true when one student read none and another four, while the reading (77a), that every student read none, is false: the continuation (78) separates them.