Unified Numeral Semantics

@cite{blok-2015} @cite{chierchia-fox-spector-2012} @cite{fox-2007} @cite{goodman-stuhlmuller-2013} @cite{horn-1972} @cite{kennedy-2015} @cite{hackl-2000} @cite{link-1983} @cite{partee-1987} @cite{spector-2013}

The numeral surface forms ("three", "more than three", "at least three", "at most three", "fewer than three") are five Nat-instantiations of @cite{kennedy-2015}'s unified de-Fregean GQ λP. max{d | #P ≥ d} REL m, captured in Core.Scale.relationalGQ. Each named meaning is the corresponding Core.Scale.{...}Deg 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 (@cite{geurts-nouwen-2007}, @cite{nouwen-2010}) reduces to reflexivity vs irreflexivity of the modifier's underlying relation; see Core.Scale.relationalGQ_refl_at_boundary and Core.Scale.relationalGQ_irrefl_at_boundary.

Sections

1. Modifier classification (Class A/B, Bound direction)
2. Numeral meaning functions (5 defs over Core.Scale.{...}Deg id)
3. BareNumeral and NumeralExpr
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)

The HasDegree-based numeral predicates and CardinalityDegree instance live in Numerals/Degree.lean; precision/halo machinery lives in Numerals/Precision.lean.

inductive Semantics.Numerals.ModifierClass : Type

Class A (strict) vs Class B (non-strict) modified numerals.

The distinction predicts ignorance implicature patterns:

• Class A (>, <): EXCLUDE the bare-numeral world → no ignorance
• Class B (≥, ≤): INCLUDE the bare-numeral world → ignorance

Structurally: Class B iff the underlying relation is reflexive (Std.Refl), Class A iff irreflexive (Std.Irrefl); see Core.Scale.relationalGQ_refl_at_boundary.

• classA : ModifierClass
• classB : ModifierClass

@[implicit_reducible]

instance Semantics.Numerals.instReprModifierClass : Repr ModifierClass

Equations

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

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.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.Scale degree property. They capture @cite{kennedy-2015}'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 Core.Scale makes the density predictions (atLeastDeg_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 = Core.Scale.eqDeg id

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

"More than m": n > m.

Equations

• Semantics.Numerals.moreThanMeaning = Core.Scale.moreThanDeg id

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

"Fewer than m": n < m.

Equations

• Semantics.Numerals.fewerThanMeaning = Core.Scale.lessThanDeg id

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

"At least m": n ≥ m.

Equations

• Semantics.Numerals.atLeastMeaning = Core.Scale.atLeastDeg id

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

"At most m": n ≤ m.

Equations

• Semantics.Numerals.atMostMeaning = Core.Scale.atMostDeg id

@[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.

def Semantics.Numerals.instInhabitedBareNumeral.default : BareNumeral

Equations

• Semantics.Numerals.instInhabitedBareNumeral.default = Semantics.Numerals.BareNumeral.one

@[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.

inductive Semantics.Numerals.NumeralExpr : Type

A numeral expression: a bare numeral or one of the four modifications. Used both as a surface form and (via kennedyAlternatives) as an element of Kennedy's single alternative set.

• bare (n : ℕ) : NumeralExpr
• atLeast (n : ℕ) : NumeralExpr
• moreThan (n : ℕ) : NumeralExpr
• atMost (n : ℕ) : NumeralExpr
• fewerThan (n : ℕ) : NumeralExpr

@[implicit_reducible]

instance Semantics.Numerals.instReprNumeralExpr : Repr NumeralExpr

Equations

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

def Semantics.Numerals.instReprNumeralExpr.repr : NumeralExpr → ℕ → Std.Format

Equations

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

def Semantics.Numerals.instDecidableEqNumeralExpr.decEq (x✝ x✝¹ : NumeralExpr) : Decidable (x✝ = x✝¹)

Equations

• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.bare a) (Semantics.Numerals.NumeralExpr.bare b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.bare n) (Semantics.Numerals.NumeralExpr.atLeast n_1) = isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.bare n) (Semantics.Numerals.NumeralExpr.moreThan n_1) = isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.bare n) (Semantics.Numerals.NumeralExpr.atMost n_1) = isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.bare n) (Semantics.Numerals.NumeralExpr.fewerThan n_1) = isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.atLeast n) (Semantics.Numerals.NumeralExpr.bare n_1) = isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.atLeast a) (Semantics.Numerals.NumeralExpr.atLeast b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.atLeast n) (Semantics.Numerals.NumeralExpr.moreThan n_1) = isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.atLeast n) (Semantics.Numerals.NumeralExpr.atMost n_1) = isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.atLeast n) (Semantics.Numerals.NumeralExpr.fewerThan n_1) = isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.moreThan n) (Semantics.Numerals.NumeralExpr.bare n_1) = isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.moreThan n) (Semantics.Numerals.NumeralExpr.atLeast n_1) = isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.moreThan a) (Semantics.Numerals.NumeralExpr.moreThan b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.moreThan n) (Semantics.Numerals.NumeralExpr.atMost n_1) = isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.moreThan n) (Semantics.Numerals.NumeralExpr.fewerThan n_1) = isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.atMost n) (Semantics.Numerals.NumeralExpr.bare n_1) = isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.atMost n) (Semantics.Numerals.NumeralExpr.atLeast n_1) = isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.atMost n) (Semantics.Numerals.NumeralExpr.moreThan n_1) = isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.atMost a) (Semantics.Numerals.NumeralExpr.atMost b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.atMost n) (Semantics.Numerals.NumeralExpr.fewerThan n_1) = isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.fewerThan n) (Semantics.Numerals.NumeralExpr.bare n_1) = isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.fewerThan n) (Semantics.Numerals.NumeralExpr.atLeast n_1) = isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.fewerThan n) (Semantics.Numerals.NumeralExpr.moreThan n_1) = isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.fewerThan n) (Semantics.Numerals.NumeralExpr.atMost n_1) = isFalse ⋯
• Semantics.Numerals.instDecidableEqNumeralExpr.decEq (Semantics.Numerals.NumeralExpr.fewerThan a) (Semantics.Numerals.NumeralExpr.fewerThan b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Numerals.instDecidableEqNumeralExpr : DecidableEq NumeralExpr

Equations

• Semantics.Numerals.instDecidableEqNumeralExpr = Semantics.Numerals.instDecidableEqNumeralExpr.decEq

def Semantics.Numerals.NumeralExpr.argument : NumeralExpr → ℕ

The numeric argument: the m in "more than m", "exactly m", etc.

Equations

• (Semantics.Numerals.NumeralExpr.bare a).argument = a
• (Semantics.Numerals.NumeralExpr.atLeast a).argument = a
• (Semantics.Numerals.NumeralExpr.moreThan a).argument = a
• (Semantics.Numerals.NumeralExpr.atMost a).argument = a
• (Semantics.Numerals.NumeralExpr.fewerThan a).argument = a

def Semantics.Numerals.NumeralExpr.modifierClass : NumeralExpr → Option ModifierClass

Strict (Class A) vs. non-strict (Class B) classification per @cite{geurts-nouwen-2007} / @cite{nouwen-2010}. Bare numerals carry no modifier and return none.

Equations

• (Semantics.Numerals.NumeralExpr.bare n).modifierClass = none
• (Semantics.Numerals.NumeralExpr.moreThan n).modifierClass = some Semantics.Numerals.ModifierClass.classA
• (Semantics.Numerals.NumeralExpr.fewerThan n).modifierClass = some Semantics.Numerals.ModifierClass.classA
• (Semantics.Numerals.NumeralExpr.atLeast n).modifierClass = some Semantics.Numerals.ModifierClass.classB
• (Semantics.Numerals.NumeralExpr.atMost n).modifierClass = some Semantics.Numerals.ModifierClass.classB

def Semantics.Numerals.NumeralExpr.boundDirection : NumeralExpr → Option BoundDirection

Lower-bound vs. upper-bound modifier direction. Bare numerals return none.

Equations

• (Semantics.Numerals.NumeralExpr.bare a).boundDirection = none
• (Semantics.Numerals.NumeralExpr.atLeast a).boundDirection = some Semantics.Numerals.BoundDirection.lower
• (Semantics.Numerals.NumeralExpr.moreThan a).boundDirection = some Semantics.Numerals.BoundDirection.lower
• (Semantics.Numerals.NumeralExpr.atMost a).boundDirection = some Semantics.Numerals.BoundDirection.upper
• (Semantics.Numerals.NumeralExpr.fewerThan a).boundDirection = some Semantics.Numerals.BoundDirection.upper

def Semantics.Numerals.NumeralExpr.meaning (bare : ℕ → ℕ → Prop) : NumeralExpr → ℕ → Prop

Meaning of a numeral expression, parameterized by the bare-numeral semantics (theory choice: Kennedy bareMeaning or Horn atLeastMeaning).

Equations

• Semantics.Numerals.NumeralExpr.meaning bare (Semantics.Numerals.NumeralExpr.bare m) x✝ = bare m x✝
• Semantics.Numerals.NumeralExpr.meaning bare (Semantics.Numerals.NumeralExpr.atLeast m) x✝ = Semantics.Numerals.atLeastMeaning m x✝
• Semantics.Numerals.NumeralExpr.meaning bare (Semantics.Numerals.NumeralExpr.moreThan m) x✝ = Semantics.Numerals.moreThanMeaning m x✝
• Semantics.Numerals.NumeralExpr.meaning bare (Semantics.Numerals.NumeralExpr.atMost m) x✝ = Semantics.Numerals.atMostMeaning m x✝
• Semantics.Numerals.NumeralExpr.meaning bare (Semantics.Numerals.NumeralExpr.fewerThan m) x✝ = Semantics.Numerals.fewerThanMeaning m x✝

@[implicit_reducible]

instance Semantics.Numerals.instDecidableMeaning (bare : ℕ → ℕ → Prop) [(m n : ℕ) → Decidable (bare m n)] (e : NumeralExpr) (n : ℕ) : Decidable (NumeralExpr.meaning bare e n)

Equations

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

def Semantics.Numerals.kennedyAlternatives (n : ℕ) : List NumeralExpr

@cite{kennedy-2015}'s single alternative set for numeral n — bare plus all four surface modifications. 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

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

Class A/B is the central typological generalization (@cite{geurts-nouwen-2007}, @cite{nouwen-2010}): strict modifiers (>, <) exclude the bare-numeral world; non-strict modifiers (≥, ≤) include it. The classification is derived from NumeralExpr.modifierClass; the inclusion/exclusion theorems below apply the corresponding general lemmas Core.Scale.relationalGQ_irrefl_at_boundary and Core.Scale.relationalGQ_refl_at_boundary, instantiated at μ = id.

theorem Semantics.Numerals.classA_excludes_bare_world (bare : ℕ → ℕ → Prop) (e : NumeralExpr) (h : e.modifierClass = some ModifierClass.classA) : ¬NumeralExpr.meaning bare e e.argument

Class A excludes the bare-numeral world (universal). For every e : NumeralExpr whose modifier class is A, the meaning fails at n = e.argument, regardless of which bare-numeral semantics is chosen.

Each non-vacuous branch delegates to Core.Scale.relationalGQ_irrefl_at_boundary at μ = id.

theorem Semantics.Numerals.classB_includes_bare_world (bare : ℕ → ℕ → Prop) (e : NumeralExpr) (h : e.modifierClass = some ModifierClass.classB) : NumeralExpr.meaning bare e e.argument

Class B includes the bare-numeral world (universal). For every e : NumeralExpr whose modifier class is B, the meaning holds at n = e.argument, regardless of which bare-numeral semantics is chosen.

Each non-vacuous branch delegates to Core.Scale.relationalGQ_refl_at_boundary at μ = id.

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 Core.Scale.eqDeg_imp_atLeastDeg.

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 Core.Scale.eqDeg_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 Core.Scale.eqDeg_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 Core.Scale.atLeastDeg_strictly_weaker_than_eqDeg (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 Core.Scale.moreThanDeg_disjoint_eqDeg.

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

The general operation Core.Scale.typeLower (∃ d' ≥ d, exact d' w) and its collapse typeLower_eqDeg_iff : typeLower (eqDeg μ) d w ↔ atLeastDeg μ d w live in Core/Scales/Scale.lean. Numerals are the id-instantiation: typeLower bareMeaning m n ↔ atLeastMeaning m n follows by definitional unfolding (bareMeaning ≡ eqDeg id, atLeastMeaning ≡ atLeastDeg id).

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

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

The numeral instantiation of Core.Scale.typeLower_eqDeg_iff.

EXH and type-shifting are inverses

@cite{spector-2013} (§6.2) presents an approach (from @cite{chierchia-fox-spector-2012}) where the exact reading of bare numerals arises from a covert exhaustivity operator: EXH(≥n) = ≥n ∧ ¬(≥n+1) = (=n). @cite{kennedy-2015} 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.

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 (m : Core.Logic.Intensional.Frame) [Fintype m.Entity] (n : ℕ) (R S : m.Entity → Prop) : Quantification.Quantifier.at_least_n_sem m n R S ↔ atLeastMeaning n (Quantification.Quantifier.count fun (x : m.Entity) => R x ∧ S x)

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

theorem Semantics.Numerals.gqt_atMost_agrees (m : Core.Logic.Intensional.Frame) [Fintype m.Entity] (n : ℕ) (R S : m.Entity → Prop) : Quantification.Quantifier.at_most_n_sem m n R S ↔ atMostMeaning n (Quantification.Quantifier.count fun (x : m.Entity) => R x ∧ S x)

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

theorem Semantics.Numerals.gqt_exactly_agrees (m : Core.Logic.Intensional.Frame) [Fintype m.Entity] (n : ℕ) (R S : m.Entity → Prop) : Quantification.Quantifier.exactly_n_sem m n R S ↔ bareMeaning n (Quantification.Quantifier.count fun (x : m.Entity) => R x ∧ S x)

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