[BN20] — Numeral semantics: the type-shift landscape

[BN20] survey the semantics of bare numerals: three views — numerals as number-denoting (type d, their (18)), as cardinality modifiers (⟨e,t⟩, their (11)), and as degree quantifiers (⟨⟨d,t⟩,t⟩, [Ken15], their (43)) — and argue the views are related by type-shifts and operators, "end[ing] up with equivalent empirical coverage". This file formalises the equivalences the survey itself contributes:

• their (23): the number view composed with MANY (their (22)) is the modifier meaning — many_number;
• their (25): CARD — an operator the authors define themselves, "for illustration of the equivalence of the modifier and number views" — maps the modifier meaning back to the number meaning — card_numModifier;
• their (49)–(50): [Par87]'s BE/IOTA lower [Ken15]'s exactly degree quantifier to the number meaning — BE_kennedy and iota_BE_kennedy, on the Partee-triangle substrate (Semantics/Composition/TypeShifting.lean);
• their (52)–(54): the survey's own proposal, "fill[ing] in an empty slot in the available types of numeral semantic analyses" — an at least degree quantifier (their (52), which is exactly the Montague lift of the number view) together with a MAX operator (their (53)) that recovers Kennedy's exactly quantifier — MAX_lift_eq_kennedy — while keeping the lower-bound meaning basic (their argument from the polarity profile of "zero", [bylinina-nouwen-2018]).

Degrees are modelled as ℕ; max(P) is mathlib's IsGreatest; pluralities are Finset ℕ with # as Finset.card. The survey's other threads — exhaustification (§5, deferring to [Spe13]), the Heim–Kennedy generalization, lower-bound semantics ([Hor72], atLeastMeaning in Semantics/Numerals/Basic.lean) — live with their primary anchors.

The number and modifier views (their (11), (18), (22)–(25))

Pluralities are finite sets of atoms; # is cardinality.

def BylininaNouwen2020.numModifier (n : ℕ) : Finset ℕ → Prop

The modifier view (their (11)): ⟦twelveₘ⟧ = λx. #x = 12.

Equations

• BylininaNouwen2020.numModifier n x = (x.card = n)

def BylininaNouwen2020.MANY (d : ℕ) : Finset ℕ → Prop

The counting operator MANY (their (22)): ⟦MANY⟧ = λd λx. #x = d.

Equations

• BylininaNouwen2020.MANY d x = (x.card = d)

theorem BylininaNouwen2020.many_number (n : ℕ) : MANY n = numModifier n

Their (23): ⟦twelveₙ MANY⟧ = ⟦twelveₘ⟧ — the number view composed with MANY is definitionally the modifier meaning.

def BylininaNouwen2020.CARD (P : Finset ℕ → Prop) : ℕ → Prop

The survey's own CARD operator (their (24)): ⟦CARD⟧ = λP ιd. ∀x[P(x) → #x = d], rendered as the relation "d is the degree CARD(P) denotes" — the ι-presupposition is the existence-and- uniqueness conjunct.

Equations

• BylininaNouwen2020.CARD P d = ((∃ (x : Finset ℕ), P x) ∧ ∀ (x : Finset ℕ), P x → x.card = d)

theorem BylininaNouwen2020.card_numModifier (n : ℕ) : CARD (numModifier n) = Semantics.Composition.TypeShifting.ident n

Their (25): CARD(⟦twelveₘ⟧) = ⟦twelveₙ⟧ — CARD maps the modifier meaning back to the number meaning (ident n is the singleton property of the degree n).

The degree-quantifier view (their (43), (47)–(50))

[Ken15]'s exactly numeral: the degree properties whose maximal value is n. max(P) = n is mathlib's IsGreatest P n.

def BylininaNouwen2020.kennedyNum (n : ℕ) : (ℕ → Prop) → Prop

Kennedy's degree quantifier (their (43)): ⟦twelve⟧ = λP. max(P) = 12.

Equations

• BylininaNouwen2020.kennedyNum n P = IsGreatest {d : ℕ | P d} n

theorem BylininaNouwen2020.BE_kennedy (n : ℕ) : Semantics.Composition.TypeShifting.BE (kennedyNum n) = Semantics.Composition.TypeShifting.ident n

Their (49): BE(⟦twelve⟧) = {12} — [Par87]'s BE lowers Kennedy's quantifier to the singleton degree property.

theorem BylininaNouwen2020.iota_BE_kennedy [DecidableEq ℕ] (domain : List ℕ) (n : ℕ) (hmem : n ∈ domain) (hnd : domain.Nodup) : Semantics.Composition.TypeShifting.iota domain (Semantics.Composition.TypeShifting.BE (kennedyNum n)) = some n

Their (50): IOTA(BE(⟦twelve⟧)) = 12 — the BE/IOTA chain recovers the number meaning, via the substrate's iota_ident roundtrip.

The survey's proposal: at-least quantifier + MAX (their (52)–(54))

theorem BylininaNouwen2020.lowerBounded_eq_lift (n : ℕ) : (fun (P : ℕ → Prop) => P n) = Semantics.Composition.TypeShifting.lift n

The survey's at least degree quantifier (their (52)): ⟦twelve⟧ = λP. P(12) — exactly the Montague lift of the number view.

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

The survey's MAX operator (their (53)): ⟦MAX⟧ = λD λP. max(P) ∈ ∩D.

Equations

• BylininaNouwen2020.MAX D P = ∃ (m : ℕ), IsGreatest {d : ℕ | P d} m ∧ ∀ (Q : ℕ → Prop), D Q → Q m

theorem BylininaNouwen2020.MAX_lift_eq_kennedy (n : ℕ) : MAX (Semantics.Composition.TypeShifting.lift n) = kennedyNum n

Their (54): ⟦MAX twelve⟧ on the at least quantifier is Kennedy's exactly quantifier — the survey's account keeps the lower-bound meaning basic and derives the exactly reading by MAX, preserving the Heim–Kennedy scope explanation.

theorem BylininaNouwen2020.lift_ne_kennedy (n : ℕ) : Semantics.Composition.TypeShifting.lift n ≠ kennedyNum n

The lower-bound and exactly quantifiers genuinely differ before MAX applies (witness P = {n, n+1}): MAX does real work.