Bylinina and Nouwen (2020): Numeral semantics

This file formalizes the survey of numeral meanings by Bylinina and Nouwen. Once the determiner view is set aside, a bare numeral has been taken to denote a predicate counting the atoms of a plurality, λx. #x = n, a number n, or a quantifier over degree properties, Kennedy's λP. max(P) = n, and operators relate the three: the counting operator MANY takes the number to the predicate ((22), (23)), the survey's CARD takes the predicate back ((24), (25)), and Partee's BE and IOTA lower the quantifier to the number ((47)–(50)). Lowering forgets the upper bound, so the lowered numeral, interpreted in situ, has an at least reading.

The views differ in where the exactly reading comes from. On the predicate and number views a numeral with a distributive predicate is lower-bounded ((29)) and an exhaustivity operator strengthens it ((32), (34)); on Kennedy's view the numeral is doubly bounded and takes scope by QR ((43)–(46)). At each scope site the two coincide, as Bylinina and Nouwen (2018) observed for zero: exhaustifying the lower bound against the higher numerals says that the numeral is the greatest degree of the property abstracted there, which is what Kennedy's quantifier says of it. Above a possibility modal both give the strong reading (36-b), Kennedy's (46), and above some students both give (39), a reading the sentence is reported to lack (fn. 9 flags the judgement). The accounts differ in which sites they reach: the Heim-Kennedy generalization (42) keeps degree operators below nominal quantifiers, and nothing keeps a propositional EXH there.

The survey's proposal keeps the quantifier type and the lower bound: the numeral is the Montague lift of the number ((52)), and an operator MAX turns it into Kennedy's quantifier ((53), (54)). At the numeral's landing site MAX is exhaustification, so the strengthening moves with the numeral and obeys (42). The lower bound has to be basic because of zero ((51)), the argument of Bylinina and Nouwen (2018): Kennedy's zero A B is no A B and licenses the negative polarity items that zero does not, while with MAX apart from the numeral zero is a tautology below MAX and no above it, and licenses none.

Main results

• exhAgainst_poss_iff_highScope: the exhaustified possibility reading of Spector is Kennedy's (46).
• lowScope_some_not_highScope: over some students the high reading (39) is strictly stronger.
• MAX_individual_iff_exhAgainst: MAX of the lifted number is exhaustification at its site.
• not_licenses_zeroWithMAX: with MAX, zero licenses no negative polarity item.

Implementation notes

• Degrees are natural numbers, a degree property is a Set ℕ and a degree quantifier a predicate on them. Kennedy's numeral is the substrate's Degree.MaxIn {n}, and its scope relative to a modal or nominal quantifier Q over a count μ is Degree.LowScope or Degree.HighScope.
• Pluralities, degree properties and licensing are those of BylininaNouwen2018: the finite sets of atoms, with the empty plurality, so plural Z is the full lattice ×Z and Link's *Z ((12)) its nonempty part. The lower bound (29) is isLowerSet_countDegrees_plural, and its failure with a collective predicate (fn. 8) countDegrees_singleton.
• EXH is Exhaustification.exhAgainst (· < ·), denying every higher numeral, which on those lower sets are the stronger alternatives of (32).

TODO

The determiner view (Section 2) and the Dutch hoeven data (26)–(28) are not formalized.

References

• [BN20]
• [BN18]
• [Ken15]
• [Par87]
• [Spe13a]
• [Hei00]
• [Lin83]

The modifier and number views

The modifier meaning of a numeral is the counting operator at its number, so the two views differ only in whether the counting is built into the numeral or supplied by an operator.

def BylininaNouwen2020.MANY {α : Type u_1} (d : ℕ) : Set (Finset α)

MANY d is the property of pluralities with d atoms, λx. #x = d ((22)).

Equations

• BylininaNouwen2020.MANY d = Finset.card ⁻¹' {d}

theorem BylininaNouwen2020.mem_MANY {α : Type u_1} {d : ℕ} {x : Finset α} : x ∈ MANY d ↔ x.card = d

noncomputable def BylininaNouwen2020.CARD {α : Type u_1} (P : Set (Finset α)) : Option ℕ

CARD P is the number of atoms every plurality in P has, ιd. ∀x[P(x) → #x = d] ((24)).

Equations

• BylininaNouwen2020.CARD P = Reference.iota fun (d : ℕ) => ∀ x ∈ P, x.card = d

theorem BylininaNouwen2020.CARD_MANY {α : Type u_1} {n : ℕ} (hn : ∃ (x : Finset α), x.card = n) : CARD (MANY n) = some n

CARD recovers the number a modifier meaning counts ((25)), given a plurality of that size.

theorem BylininaNouwen2020.MANY_injective_iff {α : Type u_1} : Function.Injective MANY ↔ Infinite α

Numbers as classes of equinumerous pluralities ((17)) are faithful exactly when there are pluralities of every size: on a finite domain every numeral beyond its size denotes the empty property.

Exhaustification and degree quantifiers

Exhaustifying the lower bound at a site and raising Kennedy's quantifier there give the same reading (BylininaNouwen2018.exhAgainst_iff_highScope, BylininaNouwen2018.exhAgainst_iff_lowScope), so the accounts differ only in the sites available to them.

theorem BylininaNouwen2020.exhAgainst_poss_iff_highScope {n : ℕ} {W : Type u_2} {R : W → Prop} {count : W → ℕ} : Exhaustification.exhAgainst (fun (x1 x2 : ℕ) => x1 < x2) (fun (m : ℕ) => Spector2013.poss (count '' {w : W | R w}) (Degree.Comparison.ge.interval m)) n ↔ Degree.HighScope (Degree.MaxIn {n}) (Quantifier.GQ.some R) (Set.Iic ∘ count)

Spector's wide-scope exhaustification over a possibility modal, the reading (36-b), is Kennedy's numeral raised over the modal ((46)).

theorem BylininaNouwen2020.poss_eq_iff_lowScope {n : ℕ} {W : Type u_2} {R : W → Prop} {count : W → ℕ} : Spector2013.poss (count '' {w : W | R w}) (Degree.Comparison.eq.interval n) ↔ Degree.LowScope (Degree.MaxIn {n}) (Quantifier.GQ.some R) (Set.Iic ∘ count)

The exactly reading under the possibility modal, (36-a), is Kennedy's numeral in situ.

theorem BylininaNouwen2020.lowScope_some_not_highScope (n : ℕ) : Degree.LowScope (Degree.MaxIn {n}) (Quantifier.GQ.some fun (x : Fin 2) => True) (Set.Iic ∘ fun (i : Fin 2) => n + ↑i) ∧ ¬Degree.HighScope (Degree.MaxIn {n}) (Quantifier.GQ.some fun (x : Fin 2) => True) (Set.Iic ∘ fun (i : Fin 2) => n + ↑i)

Over some students the high reading (39) is strictly stronger than the low one. It entails the low one (Degree.lowScope_some_of_highScope), and a student answering n questions with another answering n + 1 makes the low reading true and (39) false.

Lowering

BE and IOTA take Kennedy's quantifier to the number as they take the lift of an entity to the entity ((48)–(50)), and send it where they send the lower-bound quantifier.

theorem BylininaNouwen2020.BE_maxIn_singleton (n : ℕ) : Quantifier.NP.BE (Degree.MaxIn {n}) = Quantifier.NP.ident n

BE lowers the exactly-reading quantifier to the singleton of its number ((49)).

theorem BylininaNouwen2020.BE_maxIn_singleton_eq_BE_individual (n : ℕ) : Quantifier.NP.BE (Degree.MaxIn {n}) = Quantifier.NP.BE (Quantifier.NP.individual n)

Lowering forgets the upper bound, since BE sends the exactly-reading quantifier where it sends the lower-bound one.

theorem BylininaNouwen2020.iota_BE_maxIn_singleton (n : ℕ) : Reference.iota (Quantifier.NP.BE (Degree.MaxIn {n})) = some n

IOTA(BE(twelve)) = 12 ((50)), as IOTA(BE(λP.P(Mary))) = Mary ((48)).

theorem BylininaNouwen2020.maxIn_singleton_injective : Function.Injective fun (n : ℕ) => Degree.MaxIn {n}

The exactly-reading quantifier determines the numeral, since lowering recovers it.

The survey's proposal

The empty slot in the type landscape is a lower-bound degree quantifier, the Montague lift individual n of the number ((52)), from which MAX derives the exactly reading ((53), (54)).

def BylininaNouwen2020.MAX (D : Set (Set ℕ)) : Set ℕ → Prop

MAX D holds of the degree properties whose maximum lies in every member of D, as in λD λP. max(P) ∈ ∩D ((53)).

Equations

• BylininaNouwen2020.MAX D = Degree.MaxIn (⋂₀ D)

theorem BylininaNouwen2020.MAX_individual (n : ℕ) : MAX (Quantifier.NP.individual n) = Degree.MaxIn {n}

MAX takes the lower-bound quantifier to Kennedy's ((54)), since the properties containing n intersect to {n}.

theorem BylininaNouwen2020.MAX_individual_iff_exhAgainst {n : ℕ} {P : Set ℕ} : MAX (Quantifier.NP.individual n) P ↔ Exhaustification.exhAgainst (fun (x1 x2 : ℕ) => x1 < x2) (fun (x : ℕ) => Quantifier.NP.individual x P) n

At its landing site MAX of the lower-bound quantifier is its exhaustification against the higher numerals, a strengthening that moves with the numeral.

theorem BylininaNouwen2020.maxIn_singleton_lt_individual (n : ℕ) : Degree.MaxIn {n} < Quantifier.NP.individual n

The exactly-reading quantifier is strictly stronger than the lower-bound one, so MAX does work: {n, n + 1} contains n without n being its greatest element.

theorem BylininaNouwen2020.MAX_individual_zero_iff {α : Type u_1} [DecidableEq α] {A B : Set α} : MAX (Quantifier.NP.individual 0) (BylininaNouwen2018.countDegrees A (BylininaNouwen2018.plural B)) ↔ Quantifier.GQ.no A B

MAX of the lower-bound zero A B is Kennedy's zero A B, which is no A B ((51)).

def BylininaNouwen2020.zeroWithMAX : PolarityItem.Licenser

With MAX apart from the numeral, zero is a scalar licenser, the lower-bound numeral below MAX and its MAX above it.

Equations

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

theorem BylininaNouwen2020.zeroWithMAX_eq_zero : zeroWithMAX = BylininaNouwen2018.zero

It is the zero of [BN18], since MAX is exhaustification at its site.

theorem BylininaNouwen2020.not_licenses_zeroWithMAX (e : PolarityItem) : ¬zeroWithMAX.Licenses e

So it licenses no negative polarity item, where Kennedy's zero is no and licenses both (BylininaNouwen2018.kennedyZero_eq_nobody).