Unified Numeral Semantics

[Blo15] [CFS12] [Fox07] [GS13] [Hor72] [Ken15] [Hac00] [Lin83] [Par87] [Spe13]

The numeral surface forms ("three", "more than three", "at least three", "at most three", "fewer than three") are five Nat-instantiations of [Ken15]'s unified de-Fregean GQ λP. max{d | #P ≥ d} REL m, captured by Core.Order.Comparison.over. Each named meaning is the corresponding Core.Order.Comparison.{eq,gt,lt,ge,le}.over id specialization, and so inherits the scale infrastructure (maximal informativity, monotonicity, density) by construction.

The only theory disagreement is the bare-numeral semantics:

Theory	Bare "three"	bare semantics
Lower-bound	≥3	atLeastMeaning
Exact	=3	bareMeaning

Modified numerals are theory-independent — everyone agrees "more than 3" means > 3. The Class A / Class B distinction ([GN07], [Nou10]) reduces to whether the modifier's comparison keeps its interval endpoint; see Core.Order.Comparison.boundary_mem.

Sections

1. Modifier classification (Class A/B, Bound direction)
2. Numeral meaning functions (5 defs over Core.Order.Comparison.{...}.over id)
3. BareNumeral; Comparison interpretation (Entry.denoteUnder)
4. Alternative sets (Kennedy §4.1)
5. Class A/B corollaries, anti-Horn-scale corollaries
6. Type-shifting (Kennedy §3.1)
7. EXH–type-shift duality (Spector §6.2)
8. GQT bridge (Bylinina & Nouwen)

Precision/halo machinery lives in Numerals/Precision.lean.

inductive Semantics.Numerals.ModifierClass : Type

Class A (strict >, <) vs Class B (non-strict ≥, ≤) modified numerals — a descriptive split due to [Nou10].

Truth-conditionally the split is the reflexive/irreflexive boundary behavior: Class A EXCLUDES the bare-numeral world, Class B INCLUDES it (Class B iff the comparison's interval keeps its endpoint; see Core.Order.Comparison.boundary_mem). The further claim that this predicts a categorical ignorance-implicature pattern (Class B carries ignorance, Class A not) is contested: [SBH12] show at most and up to dissociate (so "Class B" is not one class), and [CCDR22] find the ignorance contrast graded and QUD-dependent rather than categorical; [Eng18] derives comparative-numeral inferences from granularity scales rather than from the strict/non-strict relation type.

Truth-conditionally the split is Core.Order.Comparison.boundary_mem (the non-strict comparison's interval keeps its endpoint).

• classA : ModifierClass
• classB : ModifierClass

def Semantics.Numerals.instReprModifierClass.repr : ModifierClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Numerals.instReprModifierClass : Repr ModifierClass

Equations

• Semantics.Numerals.instReprModifierClass = { reprPrec := Semantics.Numerals.instReprModifierClass.repr }

@[implicit_reducible]

instance Semantics.Numerals.instDecidableEqModifierClass : DecidableEq ModifierClass

Equations

• Semantics.Numerals.instDecidableEqModifierClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Semantics.Numerals.BoundDirection : Type

Upper vs lower bound direction.

• .upper: constrains from above (at most, fewer than)
• .lower: constrains from below (at least, more than)

• upper : BoundDirection
• lower : BoundDirection

def Semantics.Numerals.instReprBoundDirection.repr : BoundDirection → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Numerals.instReprBoundDirection : Repr BoundDirection

Equations

• Semantics.Numerals.instReprBoundDirection = { reprPrec := Semantics.Numerals.instReprBoundDirection.repr }

@[implicit_reducible]

instance Semantics.Numerals.instDecidableEqBoundDirection : DecidableEq BoundDirection

Equations

• Semantics.Numerals.instDecidableEqBoundDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

Five named meanings — one per surface form. Each is the id-instantiation of the corresponding Core.Order.Comparison.over degree property. They capture [Ken15]'s

⟦modifier m⟧ = λP. max{d | #P ≥ d} REL m

where n plays the role of max{d | #P ≥ d} and m is the numeral. bareMeaning is the exact (Kennedy) reading; the lower-bound (Horn) reading of bare numerals is atLeastMeaning. Grounding in Comparison.over makes the density predictions (geOver_downMono, moreThan_noMaxInf, atLeast_hasMaxInf, etc.) hold by construction.

def Semantics.Numerals.bareMeaning : ℕ → ℕ → Prop

Bare numeral meaning (exact reading): n = m.

Equations

• Semantics.Numerals.bareMeaning m n = (n ∈ Core.Order.Comparison.eq.over id m)

def Semantics.Numerals.moreThanMeaning : ℕ → ℕ → Prop

"More than m": n > m.

Equations

• Semantics.Numerals.moreThanMeaning m n = (n ∈ Core.Order.Comparison.gt.over id m)

def Semantics.Numerals.fewerThanMeaning : ℕ → ℕ → Prop

"Fewer than m": n < m.

Equations

• Semantics.Numerals.fewerThanMeaning m n = (n ∈ Core.Order.Comparison.lt.over id m)

def Semantics.Numerals.atLeastMeaning : ℕ → ℕ → Prop

"At least m": n ≥ m.

Equations

• Semantics.Numerals.atLeastMeaning m n = (n ∈ Core.Order.Comparison.ge.over id m)

def Semantics.Numerals.atMostMeaning : ℕ → ℕ → Prop

"At most m": n ≤ m.

Equations

• Semantics.Numerals.atMostMeaning m n = (n ∈ Core.Order.Comparison.le.over id m)

@[simp]

theorem Semantics.Numerals.bareMeaning_def (m n : ℕ) : bareMeaning m n ↔ n = m

@[simp]

theorem Semantics.Numerals.moreThanMeaning_def (m n : ℕ) : moreThanMeaning m n ↔ n > m

@[simp]

theorem Semantics.Numerals.fewerThanMeaning_def (m n : ℕ) : fewerThanMeaning m n ↔ n < m

@[simp]

theorem Semantics.Numerals.atLeastMeaning_def (m n : ℕ) : atLeastMeaning m n ↔ n ≥ m

@[simp]

theorem Semantics.Numerals.atMostMeaning_def (m n : ℕ) : atMostMeaning m n ↔ n ≤ m

@[implicit_reducible]

instance Semantics.Numerals.instDecidableBareMeaning (m n : ℕ) : Decidable (bareMeaning m n)

Equations

• Semantics.Numerals.instDecidableBareMeaning m n = Semantics.Numerals.instDecidableBareMeaning._aux_1 m n

@[implicit_reducible]

instance Semantics.Numerals.instDecidableMoreThanMeaning (m n : ℕ) : Decidable (moreThanMeaning m n)

Equations

• Semantics.Numerals.instDecidableMoreThanMeaning m n = Semantics.Numerals.instDecidableMoreThanMeaning._aux_1 m n

@[implicit_reducible]

instance Semantics.Numerals.instDecidableFewerThanMeaning (m n : ℕ) : Decidable (fewerThanMeaning m n)

Equations

• Semantics.Numerals.instDecidableFewerThanMeaning m n = Semantics.Numerals.instDecidableFewerThanMeaning._aux_1 m n

@[implicit_reducible]

instance Semantics.Numerals.instDecidableAtLeastMeaning (m n : ℕ) : Decidable (atLeastMeaning m n)

Equations

• Semantics.Numerals.instDecidableAtLeastMeaning m n = Semantics.Numerals.instDecidableAtLeastMeaning._aux_1 m n

@[implicit_reducible]

instance Semantics.Numerals.instDecidableAtMostMeaning (m n : ℕ) : Decidable (atMostMeaning m n)

Equations

• Semantics.Numerals.instDecidableAtMostMeaning m n = Semantics.Numerals.instDecidableAtMostMeaning._aux_1 m n

inductive Semantics.Numerals.BareNumeral : Type

Bare numeral utterances (one through five).

• one : BareNumeral
• two : BareNumeral
• three : BareNumeral
• four : BareNumeral
• five : BareNumeral

@[implicit_reducible]

instance Semantics.Numerals.instDecidableEqBareNumeral : DecidableEq BareNumeral

Equations

• Semantics.Numerals.instDecidableEqBareNumeral x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Numerals.instReprBareNumeral : Repr BareNumeral

Equations

• Semantics.Numerals.instReprBareNumeral = { reprPrec := Semantics.Numerals.instReprBareNumeral.repr }

def Semantics.Numerals.instReprBareNumeral.repr : BareNumeral → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Numerals.instInhabitedBareNumeral : Inhabited BareNumeral

Equations

• Semantics.Numerals.instInhabitedBareNumeral = { default := Semantics.Numerals.instInhabitedBareNumeral.default }

def Semantics.Numerals.BareNumeral.toNat : BareNumeral → ℕ

Convert BareNumeral to its numeric value.

Equations

• Semantics.Numerals.BareNumeral.one.toNat = 1
• Semantics.Numerals.BareNumeral.two.toNat = 2
• Semantics.Numerals.BareNumeral.three.toNat = 3
• Semantics.Numerals.BareNumeral.four.toNat = 4
• Semantics.Numerals.BareNumeral.five.toNat = 5

def Semantics.Numerals.BareNumeral.succ : BareNumeral → Option BareNumeral

Next-higher BareNumeral (for computing scalar alternatives).

Equations

• Semantics.Numerals.BareNumeral.one.succ = some Semantics.Numerals.BareNumeral.two
• Semantics.Numerals.BareNumeral.two.succ = some Semantics.Numerals.BareNumeral.three
• Semantics.Numerals.BareNumeral.three.succ = some Semantics.Numerals.BareNumeral.four
• Semantics.Numerals.BareNumeral.four.succ = some Semantics.Numerals.BareNumeral.five
• Semantics.Numerals.BareNumeral.five.succ = none

@[implicit_reducible]

instance Semantics.Numerals.instToStringBareNumeral : ToString BareNumeral

Equations

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

The five numeral forms are the five Core.Order.Comparisons applied to an argument; the object lives in Typology/Numeral/Basic.lean. Here we give the semantics: the order relation each comparison names, and the theory-choice meaning.

def Numeral.Entry.denoteUnder (e : Entry) (bare : ℕ → ℕ → Prop) : ℕ → Prop

Denotation of a numeral word e: the predicate over cardinalities it is true of, under a choice of bare-numeral semantics (bareMeaning exact vs. atLeastMeaning lower-bound — only the bare .eq form consults bare; the four modified forms are theory-independent Comparison.over denotations). A method on the numeral object, mirroring PersonalPronoun.denote.

Equations

• e.denoteUnder bare = match (motive := Core.Order.Comparison → ℕ → Prop) e.comparison with | Core.Order.Comparison.eq => bare e.argument | c => fun (n : ℕ) => n ∈ c.over id e.argument

@[implicit_reducible]

instance Semantics.Numerals.instDecidableDenoteUnder (e : Numeral.Entry) (bare : ℕ → ℕ → Prop) [(m n : ℕ) → Decidable (bare m n)] (n : ℕ) : Decidable (e.denoteUnder bare n)

Equations

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

theorem Numeral.Entry.denoteUnder_boundary (e : Entry) (bare : ℕ → ℕ → Prop) (h : e.comparison ≠ Core.Order.Comparison.eq) : e.denoteUnder bare e.argument ↔ e.argument ∈ e.comparison.interval e.argument

The bare-world meaning of a modified numeral word (comparison ≠ .eq) is endpoint membership in the comparison's interval — connecting meaning to the interval form.

def Semantics.Numerals.kennedyAlternatives : List Core.Order.Comparison

[Ken15]'s single alternative set — the five numeral forms (bare plus four modifications) as Core.Order.Comparisons. The point is anti-Horn-scale: there is no fixed scale direction. The Class A / Class B split is read off asymmetric entailment (cf. classA_excludes_bare_world, classB_includes_bare_world), not from membership in a pre-split sublist.

Equations

• Semantics.Numerals.kennedyAlternatives = [Core.Order.Comparison.eq, Core.Order.Comparison.gt, Core.Order.Comparison.lt, Core.Order.Comparison.ge, Core.Order.Comparison.le]

Class A/B is the central typological generalization ([GN07], [Nou10]): strict modifiers (>, <) exclude the bare-numeral world; non-strict modifiers (≥, ≤) include it. Both theorems below are now corollaries of Core.Order.Comparison.boundary_mem (Class A/B = whether the comparison's interval is closed at its endpoint) via meaning_boundary.

theorem Semantics.Numerals.classA_excludes_bare_world (e : Numeral.Entry) (bare : ℕ → ℕ → Prop) (h : e.comparison.isStrict) : ¬e.denoteUnder bare e.argument

Class A excludes the bare-numeral world (universal). A strict comparison (>, <) fails at the boundary n = m, regardless of which bare-numeral semantics is chosen. Corollary of boundary_mem.

theorem Semantics.Numerals.classB_includes_bare_world (e : Numeral.Entry) (bare : ℕ → ℕ → Prop) (h : ¬e.comparison.isStrict) (hne : e.comparison ≠ Core.Order.Comparison.eq) : e.denoteUnder bare e.argument

Class B includes the bare-numeral world (universal). A non-strict modifier (≥, ≤) holds at the boundary n = m, regardless of which bare-numeral semantics is chosen. Corollary of boundary_mem.

theorem Semantics.Numerals.classB_entailed_by_bare (m n : ℕ) : bareMeaning m n → atLeastMeaning m n

Bare numeral pointwise entails "at least m" — the id-specialization of Degree.eqOver_imp_geOver.

theorem Semantics.Numerals.bare_not_upward_monotone : ¬∀ (m m' n : ℕ), m ≤ m' → bareMeaning m n → bareMeaning m' n

Exact bare numerals are not upward-monotone: the id-specialization of Degree.eqOver_not_upward_monotone (witness d = 3, d' = 4).

theorem Semantics.Numerals.bare_not_downward_monotone : ¬∀ (m m' n : ℕ), m' ≤ m → bareMeaning m n → bareMeaning m' n

Bare numerals are not downward-monotone either, so they fail the Horn-scale criterion in both directions. The id-specialization of Degree.eqOver_not_downward_monotone.

theorem Semantics.Numerals.atLeast_strictly_weaker_than_bare (m : ℕ) : atLeastMeaning m (m + 1) ∧ ¬bareMeaning m (m + 1)

"At least m" is strictly weaker than "bare m" — the id-specialization of Degree.geOver_strictly_weaker_than_eqOver (witness d' = m+1).

theorem Semantics.Numerals.moreThan_disjoint_from_bare (m n : ℕ) : ¬(bareMeaning m n ∧ moreThanMeaning m n)

"More than m" and "bare m" have disjoint denotations — the id-specialization of Degree.gtOver_disjoint_eqOver.

De-Fregean type-shifting: exact → lower-bound

The general operation Degree.typeLower (∃ d' ≥ d, exact d' w) and its collapse typeLower_eqOver_iff (existentially lowering Comparison.eq.over μ yields Comparison.ge.over μ) live in Semantics/Degree/Predicate.lean. Numerals are the id-instantiation: typeLower bareMeaning m n ↔ atLeastMeaning m n follows by definitional unfolding (bareMeaning ≡ Comparison.eq.over id, atLeastMeaning ≡ Comparison.ge.over id).

The general theorem Degree.distinct_no_universal_witness rules out the alternative universal-closure reading of Partee's iota.

theorem Semantics.Numerals.typeLower_bareMeaning_iff (m n : ℕ) : Degree.typeLower bareMeaning m n ↔ atLeastMeaning m n

The numeral instantiation of Degree.typeLower_eqOver_iff.

EXH and type-shifting are inverses

[Spe13] (§6.2) presents an approach (from [CFS12]) where the exact reading of bare numerals arises from a covert exhaustivity operator: EXH(≥n) = ≥n ∧ ¬(≥n+1) = (=n). [Ken15] proposes the reverse: the lower-bound reading arises from type-shifting the exact meaning: typeShift(=n) = (≥n).

Both directions are general theorems on ℕ — the duality is not a spot-check, it follows from the linear order. For RSA the pair {exact, lower-bound} is what matters; type-shifting is preferable to EXH because it is independently motivated (Partee's universal), parameter-free, and grammatically always available (no insertion-site stipulation). The two halves of the duality are exhNumeral_iff_bare (EXH(≥n) = (=n)) and typeLower_bareMeaning_iff (typeShift(=n) = (≥n)).

def Semantics.Numerals.exhNumeral (m n : ℕ) : Prop

Scalar exhaustification for numerals: "at least m AND NOT at least m+1" — i.e., "exactly m".

Equations

• Semantics.Numerals.exhNumeral m n = (Semantics.Numerals.atLeastMeaning m n ∧ ¬Semantics.Numerals.atLeastMeaning (m + 1) n)

@[implicit_reducible]

instance Semantics.Numerals.instDecidableExhNumeral (m n : ℕ) : Decidable (exhNumeral m n)

Equations

• Semantics.Numerals.instDecidableExhNumeral m n = Semantics.Numerals.instDecidableExhNumeral._aux_1 m n

theorem Semantics.Numerals.exhNumeral_iff_bare (m n : ℕ) : exhNumeral m n ↔ bareMeaning m n

EXH(lower-bound) = exact (general). Exhaustifying the lower-bound meaning produces the exact meaning at every world.

theorem Semantics.Numerals.exhNumeral_eq_exhChain (m n : ℕ) : exhNumeral m n ↔ Exhaustification.exhChain (fun (k : ℕ) => atLeastMeaning (m + k)) 0 n

exhNumeral is chain-exhaustification against the full Horn scale of stronger numerals (Exhaustification.exhChain): the scale is an entailment chain, so negating the next-stronger alternative negates them all (Exhaustification.exhChain_iff_succ).

The GQT numeral quantifiers in Quantifier.lean (exactly_n_sem, at_least_n_sem, at_most_n_sem) compute the same truth values as the named numeral meanings applied to the intersection cardinality. This connects B&N's quantifier view (type ⟨⟨e,t⟩,⟨e,t⟩,t⟩) to the Kennedy maximality view (type ⟨d,t⟩).

theorem Semantics.Numerals.gqt_atLeast_agrees {α : Type u_1} [Fintype α] (n : ℕ) (R S : α → Prop) : Quantification.at_least_n_sem n R S ↔ atLeastMeaning n (Quantification.count fun (x : α) => R x ∧ S x)

GQT "at least n" agrees with atLeastMeaning on intersection cardinality.

theorem Semantics.Numerals.gqt_atMost_agrees {α : Type u_1} [Fintype α] (n : ℕ) (R S : α → Prop) : Quantification.at_most_n_sem n R S ↔ atMostMeaning n (Quantification.count fun (x : α) => R x ∧ S x)

GQT "at most n" agrees with atMostMeaning on intersection cardinality.

theorem Semantics.Numerals.gqt_exactly_agrees {α : Type u_1} [Fintype α] (n : ℕ) (R S : α → Prop) : Quantification.exactly_n_sem n R S ↔ bareMeaning n (Quantification.count fun (x : α) => R x ∧ S x)

GQT "exactly n" agrees with bareMeaning on intersection cardinality.

Denotation of the Numeral object

The lexical numeral object (Core.Order.Comparison, Numeral.Entry) is owned by Typology/Numeral/Basic.lean; this section is the semantics side — it imports that object and provides its Comparison.over denotation, mirroring how Semantics/Reference/PronounDenotation.lean denotes the PersonalPronoun object. The denotation is by construction a Core.Order.Comparison.over, so every lemma about Comparison.over transfers to every numeral entry. Entry.denoteUnder (the cardinal, theory-parameterized reading) is in Section 3.

def Numeral.Entry.denote {E : Type u_1} {α : Type u_2} [LinearOrder α] (e : Entry) (μ : E → α) (m : α) : E → Prop

Denotation of a numeral entry against a measure μ : E → α and a magnitude m: [Ken15]'s de-Fregean GQ λx. REL (μ x) m. The measure and magnitude are supplied compositionally; bare cardinals take μ = id, α = ℕ.

Equations

• e.denote μ m = e.comparison.over μ m

def Numeral.Entry.denoteCard (e : Entry) : ℕ → Prop

Bare cardinal denotation: count with μ = id and the entry's own argument.

Equations

• e.denoteCard = e.denote id e.argument

theorem Semantics.Numerals.denoteCard_eq_bareMeaning (e : Numeral.Entry) (h : e.comparison = Core.Order.Comparison.eq) : e.denoteCard = bareMeaning e.argument

The bare-comparison cardinal recovers bareMeaning (definitionally).

theorem Semantics.Numerals.denoteCard_eq_atLeastMeaning (e : Numeral.Entry) (h : e.comparison = Core.Order.Comparison.ge) : e.denoteCard = atLeastMeaning e.argument

The "at least" cardinal recovers atLeastMeaning.

theorem Semantics.Numerals.denote_at_boundary {E : Type u_1} {α : Type u_2} [LinearOrder α] (e : Numeral.Entry) (μ : E → α) (m : α) {x : E} (h : μ x = m) : e.denote μ m x ↔ ¬e.comparison.isStrict

Class A/B boundary behaviour, free for every numeral entry. At an entity whose measure equals the magnitude, the numeral holds iff its comparison is non-strict (bare =, Class B ≥/≤) and fails for the strict Class A comparisons (>/<). Inherited from Comparison.over, no per-entry proof.