Unified Numeral Semantics

@cite{blok-2015} @cite{goodman-stuhlmuller-2013} @cite{horn-1972} @cite{kennedy-2015} @cite{hackl-2000} @cite{link-1983} @cite{spector-2013}

Consolidates numeral theory infrastructure into a single module. All numeral meanings (bare + modified) flow through maxMeaning. The only theory disagreement is the OrderingRel for bare numerals:

Theory	Bare "three"	bareRel
Lower-bound	≥3	.ge
Exact	=3	.eq

Modified numerals are theory-independent — everyone agrees "more than 3" means .gt.

Sections

1. Ordering relations and modifier classification
2. Unified meaning function (maxMeaning)
3. BareNumeral type and NumeralExpr
4. Alternative sets (Kennedy §4.1)
5. Class A/B theorems, anti-Horn-scale argument
6. Theory parameterization (NumeralTheory)
7. Theory instances (LowerBound, Exact)
8. Derived properties (ambiguity, monotonicity, RSA)
9. Comparison infrastructure and theorems
10. GQT bridge theorems
11. CumminsFranke bridge
12. Aliases
13. Verification

inductive Semantics.Lexical.Numeral.OrderingRel : Type

The 5 ordering relations used in Kennedy's maximality framework.

Each modified numeral selects one of these relations:

• .eq: bare numerals ("three" = max = 3)
• .gt: "more than" (max > 3)
• .lt: "fewer than" (max < 3)
• .ge: "at least" (max ≥ 3)
• .le: "at most" (max ≤ 3)

• eq : OrderingRel
• gt : OrderingRel
• lt : OrderingRel
• ge : OrderingRel
• le : OrderingRel

def Semantics.Lexical.Numeral.instReprOrderingRel.repr : OrderingRel → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Numeral.instReprOrderingRel : Repr OrderingRel

Equations

• Semantics.Lexical.Numeral.instReprOrderingRel = { reprPrec := Semantics.Lexical.Numeral.instReprOrderingRel.repr }

instance Semantics.Lexical.Numeral.instDecidableEqOrderingRel : DecidableEq OrderingRel

Equations

• Semantics.Lexical.Numeral.instDecidableEqOrderingRel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Lexical.Numeral.instBEqOrderingRel.beq : OrderingRel → OrderingRel → Bool

Equations

• Semantics.Lexical.Numeral.instBEqOrderingRel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Lexical.Numeral.instBEqOrderingRel : BEq OrderingRel

Equations

• Semantics.Lexical.Numeral.instBEqOrderingRel = { beq := Semantics.Lexical.Numeral.instBEqOrderingRel.beq }

inductive Semantics.Lexical.Numeral.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

• classA : ModifierClass
• classB : ModifierClass

instance Semantics.Lexical.Numeral.instReprModifierClass : Repr ModifierClass

Equations

• Semantics.Lexical.Numeral.instReprModifierClass = { reprPrec := Semantics.Lexical.Numeral.instReprModifierClass.repr }

def Semantics.Lexical.Numeral.instReprModifierClass.repr : ModifierClass → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Numeral.instDecidableEqModifierClass : DecidableEq ModifierClass

Equations

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

def Semantics.Lexical.Numeral.instBEqModifierClass.beq : ModifierClass → ModifierClass → Bool

Equations

• Semantics.Lexical.Numeral.instBEqModifierClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Lexical.Numeral.instBEqModifierClass : BEq ModifierClass

Equations

• Semantics.Lexical.Numeral.instBEqModifierClass = { beq := Semantics.Lexical.Numeral.instBEqModifierClass.beq }

inductive Semantics.Lexical.Numeral.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.Lexical.Numeral.instReprBoundDirection.repr : BoundDirection → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Numeral.instReprBoundDirection : Repr BoundDirection

Equations

• Semantics.Lexical.Numeral.instReprBoundDirection = { reprPrec := Semantics.Lexical.Numeral.instReprBoundDirection.repr }

instance Semantics.Lexical.Numeral.instDecidableEqBoundDirection : DecidableEq BoundDirection

Equations

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

def Semantics.Lexical.Numeral.instBEqBoundDirection.beq : BoundDirection → BoundDirection → Bool

Equations

• Semantics.Lexical.Numeral.instBEqBoundDirection.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Lexical.Numeral.instBEqBoundDirection : BEq BoundDirection

Equations

• Semantics.Lexical.Numeral.instBEqBoundDirection = { beq := Semantics.Lexical.Numeral.instBEqBoundDirection.beq }

def Semantics.Lexical.Numeral.modifierClassOf : OrderingRel → ModifierClass

Derive the modifier class from an ordering relation.

Equations

• Semantics.Lexical.Numeral.modifierClassOf Semantics.Lexical.Numeral.OrderingRel.eq = Semantics.Lexical.Numeral.ModifierClass.classB
• Semantics.Lexical.Numeral.modifierClassOf Semantics.Lexical.Numeral.OrderingRel.gt = Semantics.Lexical.Numeral.ModifierClass.classA
• Semantics.Lexical.Numeral.modifierClassOf Semantics.Lexical.Numeral.OrderingRel.lt = Semantics.Lexical.Numeral.ModifierClass.classA
• Semantics.Lexical.Numeral.modifierClassOf Semantics.Lexical.Numeral.OrderingRel.ge = Semantics.Lexical.Numeral.ModifierClass.classB
• Semantics.Lexical.Numeral.modifierClassOf Semantics.Lexical.Numeral.OrderingRel.le = Semantics.Lexical.Numeral.ModifierClass.classB

def Semantics.Lexical.Numeral.boundDirectionOf : OrderingRel → BoundDirection

Derive bound direction from an ordering relation.

Equations

• Semantics.Lexical.Numeral.boundDirectionOf Semantics.Lexical.Numeral.OrderingRel.eq = Semantics.Lexical.Numeral.BoundDirection.lower
• Semantics.Lexical.Numeral.boundDirectionOf Semantics.Lexical.Numeral.OrderingRel.gt = Semantics.Lexical.Numeral.BoundDirection.lower
• Semantics.Lexical.Numeral.boundDirectionOf Semantics.Lexical.Numeral.OrderingRel.lt = Semantics.Lexical.Numeral.BoundDirection.upper
• Semantics.Lexical.Numeral.boundDirectionOf Semantics.Lexical.Numeral.OrderingRel.ge = Semantics.Lexical.Numeral.BoundDirection.lower
• Semantics.Lexical.Numeral.boundDirectionOf Semantics.Lexical.Numeral.OrderingRel.le = Semantics.Lexical.Numeral.BoundDirection.upper

def Semantics.Lexical.Numeral.maxMeaning (rel : OrderingRel) (m n : ℕ) : Bool

The unified meaning function for all numeral expressions.

maxMeaning rel m n is true iff cardinality n stands in relation rel to threshold m. This captures Kennedy'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.

At the cardinality level, maxMeaning.eq also plays the role of @cite{bylinina-nouwen-2020} MANY operator: MANY(n) = λcard. card = n. A proper MANY over plural individuals awaits mereological infrastructure; at the Nat abstraction the two are definitionally equal.

Equations

• Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.eq m n = (n == m)
• Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.gt m n = decide (n > m)
• Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.lt m n = decide (n < m)
• Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.ge m n = decide (n ≥ m)
• Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.le m n = decide (n ≤ m)

@[reducible, inline]

abbrev Semantics.Lexical.Numeral.bareMeaning (m n : ℕ) : Bool

Bare numeral meaning: max = m (exact cardinality).

Equations

• Semantics.Lexical.Numeral.bareMeaning m n = Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.eq m n

@[reducible, inline]

abbrev Semantics.Lexical.Numeral.moreThanMeaning (m n : ℕ) : Bool

"More than m": max > m.

Equations

• Semantics.Lexical.Numeral.moreThanMeaning m n = Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.gt m n

@[reducible, inline]

abbrev Semantics.Lexical.Numeral.fewerThanMeaning (m n : ℕ) : Bool

"Fewer than m": max < m.

Equations

• Semantics.Lexical.Numeral.fewerThanMeaning m n = Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.lt m n

@[reducible, inline]

abbrev Semantics.Lexical.Numeral.atLeastMeaning (m n : ℕ) : Bool

"At least m": max ≥ m.

Equations

• Semantics.Lexical.Numeral.atLeastMeaning m n = Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.ge m n

@[reducible, inline]

abbrev Semantics.Lexical.Numeral.atMostMeaning (m n : ℕ) : Bool

"At most m": max ≤ m.

Equations

• Semantics.Lexical.Numeral.atMostMeaning m n = Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.le m n

inductive Semantics.Lexical.Numeral.BareNumeral : Type

Bare numeral utterances (one through five).

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

instance Semantics.Lexical.Numeral.instDecidableEqBareNumeral : DecidableEq BareNumeral

Equations

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

instance Semantics.Lexical.Numeral.instBEqBareNumeral : BEq BareNumeral

Equations

• Semantics.Lexical.Numeral.instBEqBareNumeral = { beq := Semantics.Lexical.Numeral.instBEqBareNumeral.beq }

def Semantics.Lexical.Numeral.instBEqBareNumeral.beq : BareNumeral → BareNumeral → Bool

Equations

• Semantics.Lexical.Numeral.instBEqBareNumeral.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Lexical.Numeral.instReprBareNumeral : Repr BareNumeral

Equations

• Semantics.Lexical.Numeral.instReprBareNumeral = { reprPrec := Semantics.Lexical.Numeral.instReprBareNumeral.repr }

def Semantics.Lexical.Numeral.instReprBareNumeral.repr : BareNumeral → ℕ → Std.Format

Equations

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

def Semantics.Lexical.Numeral.instInhabitedBareNumeral.default : BareNumeral

Equations

• Semantics.Lexical.Numeral.instInhabitedBareNumeral.default = Semantics.Lexical.Numeral.BareNumeral.one

instance Semantics.Lexical.Numeral.instInhabitedBareNumeral : Inhabited BareNumeral

Equations

• Semantics.Lexical.Numeral.instInhabitedBareNumeral = { default := Semantics.Lexical.Numeral.instInhabitedBareNumeral.default }

def Semantics.Lexical.Numeral.BareNumeral.toNat : BareNumeral → ℕ

Convert BareNumeral to its numeric value.

Equations

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

instance Semantics.Lexical.Numeral.instToStringBareNumeral : ToString BareNumeral

Equations

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

inductive Semantics.Lexical.Numeral.NumeralExpr : Type

A numeral expression: either a bare numeral or a modified numeral.

• bare (n : ℕ) : NumeralExpr
• modified (rel : OrderingRel) (n : ℕ) : NumeralExpr

instance Semantics.Lexical.Numeral.instReprNumeralExpr : Repr NumeralExpr

Equations

• Semantics.Lexical.Numeral.instReprNumeralExpr = { reprPrec := Semantics.Lexical.Numeral.instReprNumeralExpr.repr }

def Semantics.Lexical.Numeral.instReprNumeralExpr.repr : NumeralExpr → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Numeral.instDecidableEqNumeralExpr : DecidableEq NumeralExpr

Equations

• Semantics.Lexical.Numeral.instDecidableEqNumeralExpr = Semantics.Lexical.Numeral.instDecidableEqNumeralExpr.decEq

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

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Lexical.Numeral.instDecidableEqNumeralExpr.decEq (Semantics.Lexical.Numeral.NumeralExpr.bare n) (Semantics.Lexical.Numeral.NumeralExpr.modified rel n_1) = isFalse ⋯
• Semantics.Lexical.Numeral.instDecidableEqNumeralExpr.decEq (Semantics.Lexical.Numeral.NumeralExpr.modified rel n) (Semantics.Lexical.Numeral.NumeralExpr.bare n_1) = isFalse ⋯

def Semantics.Lexical.Numeral.instBEqNumeralExpr.beq : NumeralExpr → NumeralExpr → Bool

Equations

• Semantics.Lexical.Numeral.instBEqNumeralExpr.beq (Semantics.Lexical.Numeral.NumeralExpr.bare a) (Semantics.Lexical.Numeral.NumeralExpr.bare b) = (a == b)
• Semantics.Lexical.Numeral.instBEqNumeralExpr.beq (Semantics.Lexical.Numeral.NumeralExpr.modified a a_1) (Semantics.Lexical.Numeral.NumeralExpr.modified b b_1) = (a == b && a_1 == b_1)
• Semantics.Lexical.Numeral.instBEqNumeralExpr.beq x✝¹ x✝ = false

instance Semantics.Lexical.Numeral.instBEqNumeralExpr : BEq NumeralExpr

Equations

• Semantics.Lexical.Numeral.instBEqNumeralExpr = { beq := Semantics.Lexical.Numeral.instBEqNumeralExpr.beq }

def Semantics.Lexical.Numeral.NumeralExpr.meaning (bareRel : OrderingRel) : NumeralExpr → ℕ → Bool

Meaning of a numeral expression, parameterized by the bare-numeral theory.

Equations

• Semantics.Lexical.Numeral.NumeralExpr.meaning bareRel (Semantics.Lexical.Numeral.NumeralExpr.bare m) x✝ = Semantics.Lexical.Numeral.maxMeaning bareRel m x✝
• Semantics.Lexical.Numeral.NumeralExpr.meaning bareRel (Semantics.Lexical.Numeral.NumeralExpr.modified rel m) x✝ = Semantics.Lexical.Numeral.maxMeaning rel m x✝

inductive Semantics.Lexical.Numeral.NumeralAlternative : Type

A numeral alternative in Kennedy's framework.

Instead of the traditional Horn scale ⟨1, 2, 3,...⟩, the relevant alternatives for numeral n are:

{bare n, more than n, at least n} (lower-bound direction) {bare n, fewer than n, at most n} (upper-bound direction)

• bare (n : ℕ) : NumeralAlternative
• modified (rel : OrderingRel) (n : ℕ) : NumeralAlternative

instance Semantics.Lexical.Numeral.instReprNumeralAlternative : Repr NumeralAlternative

Equations

• Semantics.Lexical.Numeral.instReprNumeralAlternative = { reprPrec := Semantics.Lexical.Numeral.instReprNumeralAlternative.repr }

def Semantics.Lexical.Numeral.instReprNumeralAlternative.repr : NumeralAlternative → ℕ → Std.Format

Equations

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

def Semantics.Lexical.Numeral.instDecidableEqNumeralAlternative.decEq (x✝ x✝¹ : NumeralAlternative) : Decidable (x✝ = x✝¹)

Equations

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

instance Semantics.Lexical.Numeral.instDecidableEqNumeralAlternative : DecidableEq NumeralAlternative

Equations

• Semantics.Lexical.Numeral.instDecidableEqNumeralAlternative = Semantics.Lexical.Numeral.instDecidableEqNumeralAlternative.decEq

def Semantics.Lexical.Numeral.instBEqNumeralAlternative.beq : NumeralAlternative → NumeralAlternative → Bool

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Lexical.Numeral.instBEqNumeralAlternative.beq (Semantics.Lexical.Numeral.NumeralAlternative.bare a) (Semantics.Lexical.Numeral.NumeralAlternative.bare b) = (a == b)
• Semantics.Lexical.Numeral.instBEqNumeralAlternative.beq x✝¹ x✝ = false

instance Semantics.Lexical.Numeral.instBEqNumeralAlternative : BEq NumeralAlternative

Equations

• Semantics.Lexical.Numeral.instBEqNumeralAlternative = { beq := Semantics.Lexical.Numeral.instBEqNumeralAlternative.beq }

def Semantics.Lexical.Numeral.lowerAlternatives (n : ℕ) : List NumeralAlternative

Lower-bound alternative set.

Equations

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

def Semantics.Lexical.Numeral.upperAlternatives (n : ℕ) : List NumeralAlternative

Upper-bound alternative set.

Equations

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

def Semantics.Lexical.Numeral.NumeralAlternative.meaning : NumeralAlternative → ℕ → Bool

Get the meaning of a numeral alternative.

Equations

• (Semantics.Lexical.Numeral.NumeralAlternative.bare a).meaning = Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.eq a
• (Semantics.Lexical.Numeral.NumeralAlternative.modified a a_1).meaning = Semantics.Lexical.Numeral.maxMeaning a a_1

theorem Semantics.Lexical.Numeral.classA_gt_excludes_bare (m : ℕ) : maxMeaning OrderingRel.gt m m = false

Class A modifiers EXCLUDE the bare-numeral world.

theorem Semantics.Lexical.Numeral.classA_lt_excludes_bare (m : ℕ) : maxMeaning OrderingRel.lt m m = false

theorem Semantics.Lexical.Numeral.classB_ge_includes_bare (m : ℕ) : maxMeaning OrderingRel.ge m m = true

Class B modifiers INCLUDE the bare-numeral world.

theorem Semantics.Lexical.Numeral.classB_le_includes_bare (m : ℕ) : maxMeaning OrderingRel.le m m = true

theorem Semantics.Lexical.Numeral.classB_entailed_by_bare (m n : ℕ) : bareMeaning m n = true → atLeastMeaning m n = true

Bare numeral entails "at least n" (Class B ≥).

theorem Semantics.Lexical.Numeral.classA_not_entailed_by_bare (m : ℕ) : bareMeaning m m = true ∧ moreThanMeaning m m = false

Bare numeral does NOT entail "more than n" (Class A >).

theorem Semantics.Lexical.Numeral.bare_not_monotonic : bareMeaning 3 3 = true ∧ bareMeaning 2 3 = false

Exact bare numerals are NOT monotonic.

theorem Semantics.Lexical.Numeral.numerals_not_horn_scalar : (bareMeaning 3 3 = true ∧ bareMeaning 2 3 = false) ∧ bareMeaning 2 2 = true ∧ bareMeaning 3 2 = false

Bare numerals do not form a traditional Horn scale.

theorem Semantics.Lexical.Numeral.atLeast_strictly_weaker_than_bare : (bareMeaning 3 3 = true ∧ atLeastMeaning 3 3 = true) ∧ atLeastMeaning 3 4 = true ∧ bareMeaning 3 4 = false

"At least n" is strictly weaker than "bare n" (under bilateral semantics).

theorem Semantics.Lexical.Numeral.moreThan_disjoint_from_bare : (bareMeaning 3 3 = true ∧ moreThanMeaning 3 3 = false) ∧ bareMeaning 3 4 = false ∧ moreThanMeaning 3 4 = true

"More than n" and "bare n" have disjoint denotations.

def Semantics.Lexical.Numeral.standardNumWords : List BareNumeral

Standard list of numeral utterances for RSA scenarios.

Equations

• Semantics.Lexical.Numeral.standardNumWords = [Semantics.Lexical.Numeral.BareNumeral.one, Semantics.Lexical.Numeral.BareNumeral.two, Semantics.Lexical.Numeral.BareNumeral.three]

def Semantics.Lexical.Numeral.standardWorlds : List ℕ

Standard list of world states (cardinalities 0-3).

Equations

• Semantics.Lexical.Numeral.standardWorlds = [0, 1, 2, 3]

structure Semantics.Lexical.Numeral.NumeralTheory : Type

A semantic theory for number words.

Each theory specifies a bareRel — the ordering relation for bare numerals. All meanings are derived via maxMeaning:

• Bare numeral meaning: maxMeaning T.bareRel w.toNat n
• Modified numeral meaning: maxMeaning rel m n (theory-independent)

• name : String

  Name of the theory

• citation : String

  Academic citation

• bareRel : OrderingRel

  The key parameter: which ordering relation for bare numerals

• utterances : List BareNumeral

  Utterances to consider (default: one, two, three)

• worlds : List ℕ

  World states to consider (default: 0, 1, 2, 3)

inductive Semantics.Lexical.Numeral.DerivationalDirection : Type

Derivational direction for the at-least/exactly relationship (@cite{bylinina-nouwen-2020} §5–6).

The four views on numeral semantics differ in which reading is basic:

• exactFromAtLeast: base meaning is at-least (≥n), exact derived via EXH or scalar implicature. Corresponds to LowerBound / @cite{horn-1972} / the modifier–number view.
• atLeastFromExact: base meaning is exact (=n), at-least derived via type-shift or relaxing maximality. Corresponds to Exact / @cite{kennedy-2015} / the degree quantifier view.

• exactFromAtLeast : DerivationalDirection
• atLeastFromExact : DerivationalDirection

instance Semantics.Lexical.Numeral.instDecidableEqDerivationalDirection : DecidableEq DerivationalDirection

Equations

• Semantics.Lexical.Numeral.instDecidableEqDerivationalDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Lexical.Numeral.instBEqDerivationalDirection.beq : DerivationalDirection → DerivationalDirection → Bool

Equations

• Semantics.Lexical.Numeral.instBEqDerivationalDirection.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Lexical.Numeral.instBEqDerivationalDirection : BEq DerivationalDirection

Equations

• Semantics.Lexical.Numeral.instBEqDerivationalDirection = { beq := Semantics.Lexical.Numeral.instBEqDerivationalDirection.beq }

instance Semantics.Lexical.Numeral.instReprDerivationalDirection : Repr DerivationalDirection

Equations

• Semantics.Lexical.Numeral.instReprDerivationalDirection = { reprPrec := Semantics.Lexical.Numeral.instReprDerivationalDirection.repr }

def Semantics.Lexical.Numeral.instReprDerivationalDirection.repr : DerivationalDirection → ℕ → Std.Format

Equations

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

def Semantics.Lexical.Numeral.NumeralTheory.derivationalDirection (T : NumeralTheory) : DerivationalDirection

Derive the derivational direction from a theory's bareRel.

Equations

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

def Semantics.Lexical.Numeral.NumeralTheory.meaning (T : NumeralTheory) (w : BareNumeral) (n : ℕ) : Bool

Derived bare-numeral meaning from bareRel.

Equations

• T.meaning w n = Semantics.Lexical.Numeral.maxMeaning T.bareRel w.toNat n

def Semantics.Lexical.Numeral.NumeralTheory.exprMeaning (T : NumeralTheory) (e : NumeralExpr) (n : ℕ) : Bool

Derived meaning for general numeral expressions.

Equations

• T.exprMeaning e n = Semantics.Lexical.Numeral.NumeralExpr.meaning T.bareRel e n

def Semantics.Lexical.Numeral.LowerBound : NumeralTheory

Lower-bound numeral theory.

"Two" means ≥2. The exact interpretation emerges via scalar implicature.

Equations

• Semantics.Lexical.Numeral.LowerBound = { name := "Lower-bound", citation := "Horn 1972", bareRel := Semantics.Lexical.Numeral.OrderingRel.ge }

def Semantics.Lexical.Numeral.Exact : NumeralTheory

Exact numeral theory.

"Two" means =2 (via maximality). No RSA strengthening needed for bare numerals.

Equations

• Semantics.Lexical.Numeral.Exact = { name := "Exact", citation := "Kennedy 2015", bareRel := Semantics.Lexical.Numeral.OrderingRel.eq }

theorem Semantics.Lexical.Numeral.lowerBound_meaning_eq (w : BareNumeral) (n : ℕ) : LowerBound.meaning w n = maxMeaning OrderingRel.ge w.toNat n

Lower-bound meaning is maxMeaning.ge.

theorem Semantics.Lexical.Numeral.exact_meaning_eq (w : BareNumeral) (n : ℕ) : Exact.meaning w n = maxMeaning OrderingRel.eq w.toNat n

Exact meaning is maxMeaning.eq.

theorem Semantics.Lexical.Numeral.lowerBound_exactFromAtLeast : LowerBound.derivationalDirection = DerivationalDirection.exactFromAtLeast

Lower-bound derives exact from at-least (@cite{horn-1972}; @cite{bylinina-nouwen-2020} §5).

theorem Semantics.Lexical.Numeral.exact_atLeastFromExact : Exact.derivationalDirection = DerivationalDirection.atLeastFromExact

Exact derives at-least from exact (@cite{kennedy-2015}; @cite{bylinina-nouwen-2020} §6).

De-Fregean Type-Shifting: Exact → Lower-Bound

@cite{kennedy-2015} shows that the lower-bound meaning of bare numerals can be derived from the exact (de-Fregean) meaning via @cite{partee-1987}'s BE + iota type-shifting operations. The de-Fregean meaning max{n | D(n)} = m is basic; applying BE derives a property λn. n = m; applying iota and existential closure yields ∃x[P(x) ∧ #(x) = m], which is the one-sided (lower-bound) truth condition.

Key fact: maxMeaning.ge m n ↔ ∃ k ≥ m, maxMeaning.eq k n. The lower-bound reading says "the max is at least m", which holds iff there exists some k ≥ m such that the max is exactly k. This is the formal content of the type-shift.

def Semantics.Lexical.Numeral.typeLower (exact : ℕ → ℕ → Bool) (maxN m n : ℕ) : Bool

Type-lower the exact meaning to get the lower-bound meaning. Corresponds to Kennedy's derivation via BE + iota + existential closure. typeLower exact m n = true iff ∃ k ≥ m, exact k n = true. We compute this over a bounded range [m, maxN].

Equations

• Semantics.Lexical.Numeral.typeLower exact maxN m n = (List.range (maxN + 1)).any fun (k : ℕ) => decide (k ≥ m) && exact k n

theorem Semantics.Lexical.Numeral.lowerBound_from_exact_typeshift : (standardWorlds.all fun (n : ℕ) => [BareNumeral.one, BareNumeral.two, BareNumeral.three].all fun (w : BareNumeral) => LowerBound.meaning w n == typeLower (maxMeaning OrderingRel.eq) 3 w.toNat n) = true

The lower-bound theory is derivable from the exact theory via type-shifting. For each bare numeral and each standard world, the lower-bound meaning equals the type-lowered exact meaning. This formalizes @cite{kennedy-2015}'s claim that atLeastFromExact is not just a label but a derivational fact: maxMeaning.ge m n = typeLower (maxMeaning.eq) 3 m n for standard worlds.

theorem Semantics.Lexical.Numeral.typeLower_uniqueness (m n : ℕ) : (∃ k ≥ m, n = k) ↔ n ≥ m

Why this is the only type-shift: the equivalence ∃ k ≥ m, n = k ↔ n ≥ m is a tautology of linear orders on ℕ.

Partee's BE extracts singletons from the GQ; existential closure binds the degree variable; the result is uniquely determined by the linear order on degrees. No other Partee shift + closure mode produces a different reading:

• BE is the unique GQ→property lowering preserving content
• Universal closure would give ∀ k ≥ m, n = k, which is false for all n when there exist distinct k₁ ≥ m and k₂ ≥ m (i.e., always for m < maxN)
• The equivalence is a fact about ℕ, not a design choice

theorem Semantics.Lexical.Numeral.universal_closure_fails : ¬∃ (n : ℕ), ∀ k ≥ 2, k ≤ 3 → n = k

Universal closure fails: ∀ k ≥ m, n = k is unsatisfiable when there exist distinct k₁, k₂ ≥ m. This rules out the alternative to existential closure.

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) = ∃k≥n.(=k) = (≥n).

These are inverse operations on the same pair of meanings:

    exact ——typeShift——→ lower-bound
      ↑ |
      └────────EXH────────────┘

For RSA, only the pair {exact, lower-bound} matters — the listener marginalizes over both regardless of which is "basic". But type-shifting is preferable to EXH because:

1. Independently motivated: @cite{partee-1987} type-shifting applies to all NPs, not just numerals. It's part of the grammar regardless.
2. No free parameters: The lower-bound meaning is the unique output of type-shifting (proved: typeLower_uniqueness, universal_closure_fails). EXH requires specifying an alternative set.
3. No distribution problems: EXH must be stipulated as optionally present/absent at various syntactic positions. Type-shifted meanings are always grammatically available (Partee's universal).
4. Quality filter does the work: In RSA, the quality filter selects between type-shifted meanings based on the speaker's epistemic state. EXH insertion requires an additional mechanism for the listener to reason about.

def Semantics.Lexical.Numeral.exhNumeral (_maxN m n : ℕ) : Bool

Scalar exhaustification for numerals. exhNumeral m n = "the max count is at least m AND NOT at least m+1" = "the max count is exactly m". This is the EXH from @cite{spector-2013} (§6.2) applied to the numeral scalar alternative set {≥k : k is a numeral}.

Equations

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

theorem Semantics.Lexical.Numeral.exh_lowerBound_eq_exact : (standardWorlds.all fun (n : ℕ) => [BareNumeral.one, BareNumeral.two, BareNumeral.three].all fun (w : BareNumeral) => exhNumeral 3 w.toNat n == maxMeaning OrderingRel.eq w.toNat n) = true

EXH(lower-bound) = exact: Exhaustifying the lower-bound meaning produces the exact meaning. This is the forward direction of the duality.

theorem Semantics.Lexical.Numeral.typeShift_exact_eq_lowerBound : (standardWorlds.all fun (n : ℕ) => [BareNumeral.one, BareNumeral.two, BareNumeral.three].all fun (w : BareNumeral) => typeLower (maxMeaning OrderingRel.eq) 3 w.toNat n == maxMeaning OrderingRel.ge w.toNat n) = true

typeShift(exact) = lower-bound: Type-shifting the exact meaning produces the lower-bound meaning. This is the backward direction. (Already proved as lowerBound_from_exact_typeshift; restated for symmetry.)

theorem Semantics.Lexical.Numeral.exh_typeShift_roundtrip : (standardWorlds.all fun (n : ℕ) => [BareNumeral.one, BareNumeral.two, BareNumeral.three].all fun (w : BareNumeral) => exhNumeral 3 w.toNat n == maxMeaning OrderingRel.eq w.toNat n && typeLower (maxMeaning OrderingRel.eq) 3 w.toNat n == maxMeaning OrderingRel.ge w.toNat n) = true

The EXH–type-shift round-trip is the identity on exact meanings. typeShift(EXH(typeShift(exact))) = typeShift(exact) = lower-bound. Equivalently: starting from exact, type-shifting then exhaustifying recovers exact.

theorem Semantics.Lexical.Numeral.typeShift_subsumes_exh : (standardWorlds.all fun (n : ℕ) => [BareNumeral.one, BareNumeral.two, BareNumeral.three].all fun (w : BareNumeral) => maxMeaning OrderingRel.eq w.toNat n == maxMeaning OrderingRel.eq w.toNat n && typeLower (maxMeaning OrderingRel.eq) 3 w.toNat n == maxMeaning OrderingRel.ge w.toNat n && exhNumeral 3 w.toNat n == maxMeaning OrderingRel.eq w.toNat n && maxMeaning OrderingRel.ge w.toNat n == maxMeaning OrderingRel.ge w.toNat n) = true

EXH is redundant given type-shifting. The pair {exact, lower-bound} is obtainable from exact alone (via type-shifting) without EXH. Since type-shifting is independently motivated and produces the unique derived meaning (typeLower_uniqueness), EXH is not needed to generate the ambiguity that RSA marginalizes over.

Formally: the set of meanings available under Kennedy + type-shifting equals the set available under LB + EXH.

def Semantics.Lexical.Numeral.NumeralTheory.strongerThan (T : NumeralTheory) (w₁ w₂ : BareNumeral) : Prop

Strength ordering: w₁ is stronger than w₂ if w₁ entails w₂.

Equations

• T.strongerThan w₁ w₂ = ∀ (n : ℕ), T.meaning w₁ n = true → T.meaning w₂ n = true

def Semantics.Lexical.Numeral.NumeralTheory.isStrongerThan (T : NumeralTheory) (w₁ w₂ : BareNumeral) : Bool

Decidable strength comparison.

Equations

• T.isStrongerThan w₁ w₂ = T.worlds.all fun (n : ℕ) => !T.meaning w₁ n || T.meaning w₂ n

def Semantics.Lexical.Numeral.NumeralTheory.compatibleCount (T : NumeralTheory) (w : BareNumeral) : ℕ

Count worlds compatible with an utterance.

Equations

• T.compatibleCount w = (List.filter (T.meaning w) T.worlds).length

def Semantics.Lexical.Numeral.NumeralTheory.compatibleWorlds (T : NumeralTheory) (w : BareNumeral) : List ℕ

List of worlds compatible with an utterance.

Equations

• T.compatibleWorlds w = List.filter (T.meaning w) T.worlds

def Semantics.Lexical.Numeral.NumeralTheory.hasAmbiguity (T : NumeralTheory) (w : BareNumeral) : Bool

Is there semantic ambiguity for this utterance?

Equations

• T.hasAmbiguity w = decide (T.compatibleCount w > 1)

def Semantics.Lexical.Numeral.NumeralTheory.isMonotonic (T : NumeralTheory) : Prop

Monotonicity: larger numerals are stronger.

Equations

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

def Semantics.Lexical.Numeral.NumeralTheory.checkMonotonic (T : NumeralTheory) : Bool

Decidable monotonicity check.

Equations

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

def Semantics.Lexical.Numeral.NumeralTheory.isScalar (T : NumeralTheory) : Prop

A theory is scalar if numerals form a Horn scale.

Equations

• T.isScalar = (T.isMonotonic ∧ ∀ (w₁ w₂ : Semantics.Lexical.Numeral.BareNumeral), T.strongerThan w₁ w₂ → T.strongerThan w₂ w₁ → w₁ = w₂)

theorem Semantics.Lexical.Numeral.lowerBound_two_ambiguous : LowerBound.compatibleWorlds BareNumeral.two = [2, 3]

"two" is compatible with both 2 and 3 (ambiguity exists).

theorem Semantics.Lexical.Numeral.lowerBound_two_has_ambiguity : LowerBound.hasAmbiguity BareNumeral.two = true

Lower-bound has ambiguity for "two".

theorem Semantics.Lexical.Numeral.lowerBound_three_stronger_than_two : LowerBound.isStrongerThan BareNumeral.three BareNumeral.two = true

"three" entails "two" in lower-bound semantics.

theorem Semantics.Lexical.Numeral.lowerBound_two_stronger_than_one : LowerBound.isStrongerThan BareNumeral.two BareNumeral.one = true

"two" entails "one" in lower-bound semantics.

theorem Semantics.Lexical.Numeral.lowerBound_is_monotonic : LowerBound.checkMonotonic = true

Lower-bound semantics is monotonic.

theorem Semantics.Lexical.Numeral.lowerBound_one_count : LowerBound.compatibleCount BareNumeral.one = 3

theorem Semantics.Lexical.Numeral.lowerBound_two_count : LowerBound.compatibleCount BareNumeral.two = 2

theorem Semantics.Lexical.Numeral.lowerBound_three_count : LowerBound.compatibleCount BareNumeral.three = 1

theorem Semantics.Lexical.Numeral.exact_two_worlds : Exact.compatibleWorlds BareNumeral.two = [2]

"two" is compatible with only world 2 (exact meaning).

theorem Semantics.Lexical.Numeral.exact_no_ambiguity : Exact.hasAmbiguity BareNumeral.two = false

No ambiguity for bare numerals.

theorem Semantics.Lexical.Numeral.exact_differs_from_lowerBound : Exact.compatibleWorlds BareNumeral.two ≠ LowerBound.compatibleWorlds BareNumeral.two

Exact differs from LowerBound on bare numerals.

theorem Semantics.Lexical.Numeral.ambiguity_differs : LowerBound.hasAmbiguity BareNumeral.two = true ∧ Exact.hasAmbiguity BareNumeral.two = false

The key divergence: ambiguity.

theorem Semantics.Lexical.Numeral.exact_no_rsa_strengthening_needed : Exact.compatibleCount BareNumeral.two = 1

Under Exact, only one world compatible.

theorem Semantics.Lexical.Numeral.exact_not_monotonic : Exact.checkMonotonic = false

Exact is not monotonic.

theorem Semantics.Lexical.Numeral.exact_three_not_stronger : Exact.isStrongerThan BareNumeral.three BareNumeral.two = false

theorem Semantics.Lexical.Numeral.bare_numeral_summary : Exact.hasAmbiguity BareNumeral.two = false ∧ Exact.compatibleCount BareNumeral.two = 1 ∧ LowerBound.hasAmbiguity BareNumeral.two = true ∧ LowerBound.compatibleCount BareNumeral.two = 2

Summary: Exact vs LowerBound bare numerals.

def Semantics.Lexical.Numeral.theoriesAgreeAt (T₁ T₂ : NumeralTheory) (w : BareNumeral) (n : ℕ) : Bool

Do two theories agree on utterance w in world n?

Equations

• Semantics.Lexical.Numeral.theoriesAgreeAt T₁ T₂ w n = (T₁.meaning w n == T₂.meaning w n)

def Semantics.Lexical.Numeral.theoriesAgreeOn (T₁ T₂ : NumeralTheory) (w : BareNumeral) : Bool

Do two theories agree on utterance w across all worlds?

Equations

• Semantics.Lexical.Numeral.theoriesAgreeOn T₁ T₂ w = T₁.worlds.all fun (n : ℕ) => Semantics.Lexical.Numeral.theoriesAgreeAt T₁ T₂ w n

def Semantics.Lexical.Numeral.divergingWorlds (T₁ T₂ : NumeralTheory) (w : BareNumeral) : List ℕ

Find worlds where two theories diverge.

Equations

• Semantics.Lexical.Numeral.divergingWorlds T₁ T₂ w = List.filter (fun (n : ℕ) => !Semantics.Lexical.Numeral.theoriesAgreeAt T₁ T₂ w n) T₁.worlds

def Semantics.Lexical.Numeral.theoriesEquivalent (T₁ T₂ : NumeralTheory) : Bool

Do two theories agree on all utterances in all worlds?

Equations

• Semantics.Lexical.Numeral.theoriesEquivalent T₁ T₂ = T₁.utterances.all fun (w : Semantics.Lexical.Numeral.BareNumeral) => Semantics.Lexical.Numeral.theoriesAgreeOn T₁ T₂ w

def Semantics.Lexical.Numeral.hasMoreAmbiguity (T₁ T₂ : NumeralTheory) (w : BareNumeral) : Bool

Ambiguity difference.

Equations

• Semantics.Lexical.Numeral.hasMoreAmbiguity T₁ T₂ w = decide (T₁.compatibleCount w > T₂.compatibleCount w)

theorem Semantics.Lexical.Numeral.lowerBound_exact_differ_on_two : LowerBound.meaning BareNumeral.two 3 = true ∧ Exact.meaning BareNumeral.two 3 = false

theorem Semantics.Lexical.Numeral.divergence_at_three : divergingWorlds LowerBound Exact BareNumeral.two = [3]

theorem Semantics.Lexical.Numeral.agreement_at_two : theoriesAgreeAt LowerBound Exact BareNumeral.two 2 = true

theorem Semantics.Lexical.Numeral.theories_not_equivalent : theoriesEquivalent LowerBound Exact = false

theorem Semantics.Lexical.Numeral.lowerBound_more_ambiguous_two : hasMoreAmbiguity LowerBound Exact BareNumeral.two = true

theorem Semantics.Lexical.Numeral.ambiguity_count_differs : LowerBound.compatibleCount BareNumeral.two = 2 ∧ Exact.compatibleCount BareNumeral.two = 1

theorem Semantics.Lexical.Numeral.ambiguity_presence_differs : LowerBound.hasAmbiguity BareNumeral.two = true ∧ Exact.hasAmbiguity BareNumeral.two = false

theorem Semantics.Lexical.Numeral.monotonicity_differs : LowerBound.checkMonotonic = true ∧ Exact.checkMonotonic = false

theorem Semantics.Lexical.Numeral.only_lowerBound_supports_implicature : (LowerBound.compatibleCount BareNumeral.two > 1 ∧ LowerBound.isStrongerThan BareNumeral.three BareNumeral.two = true) ∧ Exact.compatibleCount BareNumeral.two = 1

theorem Semantics.Lexical.Numeral.lowerBound_consistent_with_cancellation : LowerBound.hasAmbiguity BareNumeral.two = true

theorem Semantics.Lexical.Numeral.exact_inconsistent_with_cancellation : Exact.hasAmbiguity BareNumeral.two = false

theorem Semantics.Lexical.Numeral.summary_comparison : (LowerBound.compatibleCount BareNumeral.two = 2 ∧ Exact.compatibleCount BareNumeral.two = 1) ∧ (LowerBound.checkMonotonic = true ∧ Exact.checkMonotonic = false) ∧ LowerBound.meaning BareNumeral.two 3 = true ∧ Exact.meaning BareNumeral.two 3 = false

theorem Semantics.Lexical.Numeral.classA_classB_diverge_on_bare_world : maxMeaning OrderingRel.gt 3 3 = false ∧ maxMeaning OrderingRel.ge 3 3 = true ∧ maxMeaning OrderingRel.lt 3 3 = false ∧ maxMeaning OrderingRel.le 3 3 = true

theorem Semantics.Lexical.Numeral.classB_strictly_weaker_than_bare : maxMeaning OrderingRel.ge 3 3 = true ∧ maxMeaning OrderingRel.ge 3 4 = true ∧ maxMeaning OrderingRel.eq 3 4 = false ∧ maxMeaning OrderingRel.gt 3 3 = false

theorem Semantics.Lexical.Numeral.bare_eq_exact_one (n : ℕ) : bareMeaning 1 n = Exact.meaning BareNumeral.one n

theorem Semantics.Lexical.Numeral.bare_eq_exact_two (n : ℕ) : bareMeaning 2 n = Exact.meaning BareNumeral.two n

theorem Semantics.Lexical.Numeral.bare_eq_exact_three (n : ℕ) : bareMeaning 3 n = Exact.meaning BareNumeral.three n

theorem Semantics.Lexical.Numeral.atLeast_eq_lowerBound_one (n : ℕ) : atLeastMeaning 1 n = LowerBound.meaning BareNumeral.one n

theorem Semantics.Lexical.Numeral.atLeast_eq_lowerBound_two (n : ℕ) : atLeastMeaning 2 n = LowerBound.meaning BareNumeral.two n

theorem Semantics.Lexical.Numeral.atLeast_eq_lowerBound_three (n : ℕ) : atLeastMeaning 3 n = LowerBound.meaning BareNumeral.three n

theorem Semantics.Lexical.Numeral.gqt_atLeast_agrees (m : Montague.Model) [Fintype m.Entity] (n : ℕ) (R S : m.Entity → Bool) : Determiner.Quantifier.at_least_n_sem m n R S = maxMeaning OrderingRel.ge n {x : m.Entity | R x = true ∧ S x = true}.card

GQT "at least n" agrees with maxMeaning.ge on intersection cardinality.

theorem Semantics.Lexical.Numeral.gqt_atMost_agrees (m : Montague.Model) [Fintype m.Entity] (n : ℕ) (R S : m.Entity → Bool) : Determiner.Quantifier.at_most_n_sem m n R S = maxMeaning OrderingRel.le n {x : m.Entity | R x = true ∧ S x = true}.card

GQT "at most n" agrees with maxMeaning.le on intersection cardinality.

theorem Semantics.Lexical.Numeral.gqt_exactly_agrees (m : Montague.Model) [Fintype m.Entity] (n : ℕ) (R S : m.Entity → Bool) : Determiner.Quantifier.exactly_n_sem m n R S = maxMeaning OrderingRel.eq n {x : m.Entity | R x = true ∧ S x = true}.card

GQT "exactly n" agrees with maxMeaning.eq on intersection cardinality.

theorem Semantics.Lexical.Numeral.moreThan_eq_cumminsFranke (m n : ℕ) : moreThanMeaning m n = decide (n > m)

"More than m" via maximality = n > m.

@[reducible, inline]

abbrev Semantics.Lexical.Numeral.Bilateral : NumeralTheory

Equations

• Semantics.Lexical.Numeral.Bilateral = Semantics.Lexical.Numeral.Exact

@[reducible, inline]

abbrev Semantics.Lexical.Numeral.DeFregean : NumeralTheory

Equations

• Semantics.Lexical.Numeral.DeFregean = Semantics.Lexical.Numeral.Exact

@[reducible, inline]

abbrev Semantics.Lexical.Numeral.NumWord : Type

Equations

• Semantics.Lexical.Numeral.NumWord = Semantics.Lexical.Numeral.BareNumeral

def Semantics.Lexical.Numeral.lowerBoundMeaning (w : BareNumeral) (n : ℕ) : Bool

Equations

• Semantics.Lexical.Numeral.lowerBoundMeaning w n = Semantics.Lexical.Numeral.LowerBound.meaning w n

def Semantics.Lexical.Numeral.bilateralMeaning (w : BareNumeral) (n : ℕ) : Bool

Equations

• Semantics.Lexical.Numeral.bilateralMeaning w n = Semantics.Lexical.Numeral.Exact.meaning w n

@[reducible, inline]

abbrev Semantics.Lexical.Numeral.deFregeanMeaning (w : BareNumeral) (n : ℕ) : Bool

Equations

• Semantics.Lexical.Numeral.deFregeanMeaning = Semantics.Lexical.Numeral.bilateralMeaning

@[reducible, inline]

abbrev Semantics.Lexical.Numeral.exactMeaning (w : BareNumeral) (n : ℕ) : Bool

Equations

• Semantics.Lexical.Numeral.exactMeaning = Semantics.Lexical.Numeral.bilateralMeaning

theorem Semantics.Lexical.Numeral.bare_exact_match : bareMeaning 3 3 = true

theorem Semantics.Lexical.Numeral.bare_rejects_lower : bareMeaning 3 2 = false

theorem Semantics.Lexical.Numeral.bare_rejects_higher : bareMeaning 3 4 = false

theorem Semantics.Lexical.Numeral.moreThan_above : moreThanMeaning 3 4 = true

theorem Semantics.Lexical.Numeral.moreThan_equal : moreThanMeaning 3 3 = false

theorem Semantics.Lexical.Numeral.fewerThan_below : fewerThanMeaning 3 2 = true

theorem Semantics.Lexical.Numeral.fewerThan_equal : fewerThanMeaning 3 3 = false

theorem Semantics.Lexical.Numeral.atLeast_equal : atLeastMeaning 3 3 = true

theorem Semantics.Lexical.Numeral.atLeast_above : atLeastMeaning 3 4 = true

theorem Semantics.Lexical.Numeral.atLeast_below : atLeastMeaning 3 2 = false

theorem Semantics.Lexical.Numeral.atMost_equal : atMostMeaning 3 3 = true

theorem Semantics.Lexical.Numeral.atMost_below : atMostMeaning 3 2 = true

theorem Semantics.Lexical.Numeral.atMost_above : atMostMeaning 3 4 = false

maxMeaning as ℕ-pullback of Core.Scale degree properties

maxMeaning computes over ℕ independently — it works, but the degree properties in Core.Scale (atLeastDeg, moreThanDeg, etc.) are the canonical scale-level definitions. These bridge theorems prove that maxMeaning is the Bool/decidable restriction of Core.Scale degree properties, connecting ℕ-level computation to scale-level definitions.

This means density predictions (moreThan_noMaxInf, atLeast_hasMaxInf) flow compositionally from Core.Scale through numeral semantics.

theorem Semantics.Lexical.Numeral.maxMeaning_ge_iff_atLeastDeg (m n : ℕ) : maxMeaning OrderingRel.ge m n = true ↔ Core.Scale.atLeastDeg id m n

maxMeaning.ge m n = true iff atLeastDeg id m n.

theorem Semantics.Lexical.Numeral.maxMeaning_gt_iff_moreThanDeg (m n : ℕ) : maxMeaning OrderingRel.gt m n = true ↔ Core.Scale.moreThanDeg id m n

maxMeaning.gt m n = true iff moreThanDeg id m n.

theorem Semantics.Lexical.Numeral.maxMeaning_eq_iff_eqDeg (m n : ℕ) : maxMeaning OrderingRel.eq m n = true ↔ Core.Scale.eqDeg id m n

maxMeaning.eq m n = true iff eqDeg id m n.

theorem Semantics.Lexical.Numeral.maxMeaning_le_iff_atMostDeg (m n : ℕ) : maxMeaning OrderingRel.le m n = true ↔ Core.Scale.atMostDeg id m n

maxMeaning.le m n = true iff atMostDeg id m n.

theorem Semantics.Lexical.Numeral.maxMeaning_lt_iff_lessThanDeg (m n : ℕ) : maxMeaning OrderingRel.lt m n = true ↔ Core.Scale.lessThanDeg id m n

maxMeaning.lt m n = true iff lessThanDeg id m n.

def Semantics.Lexical.Numeral.numeralExact {E : Type} [Core.Scale.HasDegree E] (stated : ℚ) (entity : E) : Bool

Literal/exact semantics for numeral expressions. "six feet" is true of x iff μ_height(x) = 183.

Equations

• Semantics.Lexical.Numeral.numeralExact stated entity = (Core.Scale.HasDegree.degree entity == stated)

def Semantics.Lexical.Numeral.numeralAtLeast {E : Type} [Core.Scale.HasDegree E] (threshold : ℚ) (entity : E) : Bool

"At least n" semantics (lower-bound reading).

Equations

• Semantics.Lexical.Numeral.numeralAtLeast threshold entity = decide (Core.Scale.HasDegree.degree entity ≥ threshold)

def Semantics.Lexical.Numeral.numeralApprox {E : Type} [Core.Scale.HasDegree E] (stated tolerance : ℚ) (entity : E) : Bool

Approximate match with tolerance (for vagueness/imprecision).

Equations

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

structure Semantics.Lexical.Numeral.MeasurePredicate (E : Type) : Type

A measure predicate maps entities to degrees along some dimension.

• dimension : String
• μ : E → ℚ

def Semantics.Lexical.Numeral.MeasurePredicate.fromHasDegree (E : Type) [Core.Scale.HasDegree E] (dim : String) : MeasurePredicate E

Construct a MeasurePredicate from a HasDegree instance

Equations

• Semantics.Lexical.Numeral.MeasurePredicate.fromHasDegree E dim = { dimension := dim, μ := Core.Scale.HasDegree.degree }

structure Semantics.Lexical.Numeral.DegreePhrase : Type

A degree phrase denotes a specific degree value. "1000 dollars" denotes the degree 1000 (in dollar units).

• value : ℚ
• unit : String

def Semantics.Lexical.Numeral.instReprDegreePhrase.repr : DegreePhrase → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Numeral.instReprDegreePhrase : Repr DegreePhrase

Equations

• Semantics.Lexical.Numeral.instReprDegreePhrase = { reprPrec := Semantics.Lexical.Numeral.instReprDegreePhrase.repr }

instance Semantics.Lexical.Numeral.instDecidableEqDegreePhrase : DecidableEq DegreePhrase

Equations

• Semantics.Lexical.Numeral.instDecidableEqDegreePhrase = Semantics.Lexical.Numeral.instDecidableEqDegreePhrase.decEq

def Semantics.Lexical.Numeral.instDecidableEqDegreePhrase.decEq (x✝ x✝¹ : DegreePhrase) : Decidable (x✝ = x✝¹)

Equations

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

def Semantics.Lexical.Numeral.instBEqDegreePhrase.beq : DegreePhrase → DegreePhrase → Bool

Equations

• Semantics.Lexical.Numeral.instBEqDegreePhrase.beq { value := a, unit := a_1 } { value := b, unit := b_1 } = (a == b && a_1 == b_1)
• Semantics.Lexical.Numeral.instBEqDegreePhrase.beq x✝¹ x✝ = false

instance Semantics.Lexical.Numeral.instBEqDegreePhrase : BEq DegreePhrase

Equations

• Semantics.Lexical.Numeral.instBEqDegreePhrase = { beq := Semantics.Lexical.Numeral.instBEqDegreePhrase.beq }

def Semantics.Lexical.Numeral.DegreePhrase.ofRat (n : ℚ) (unit : String := "") : DegreePhrase

Construct a degree phrase from a rational number

Equations

• Semantics.Lexical.Numeral.DegreePhrase.ofRat n unit = { value := n, unit := unit }

def Semantics.Lexical.Numeral.DegreePhrase.ofNat (n : ℕ) (unit : String := "") : DegreePhrase

Construct a degree phrase from a natural number

Equations

• Semantics.Lexical.Numeral.DegreePhrase.ofNat n unit = { value := ↑n, unit := unit }

def Semantics.Lexical.Numeral.measureSentence {E : Type} (pred : MeasurePredicate E) (entity : E) (deg : DegreePhrase) : Bool

Compositional semantics for measure sentences. ⟦X measure-pred degree-phrase⟧ = μ(X) = d

Equations

• Semantics.Lexical.Numeral.measureSentence pred entity deg = (pred.μ entity == deg.value)

def Semantics.Lexical.Numeral.measureSentence' {E : Type} [Core.Scale.HasDegree E] (entity : E) (deg : DegreePhrase) : Bool

Compositional semantics using HasDegree directly.

Equations

• Semantics.Lexical.Numeral.measureSentence' entity deg = (Core.Scale.HasDegree.degree entity == deg.value)

theorem Semantics.Lexical.Numeral.measureSentence_eq_numeralExact {E : Type} [Core.Scale.HasDegree E] (entity : E) (deg : DegreePhrase) : measureSentence' entity deg = numeralExact deg.value entity

The compositional measure sentence semantics equals the simple numeral check.

theorem Semantics.Lexical.Numeral.fromHasDegree_μ {E : Type} [Core.Scale.HasDegree E] (dim : String) : (MeasurePredicate.fromHasDegree E dim).μ = Core.Scale.HasDegree.degree

MeasurePredicate.fromHasDegree produces the HasDegree measure function.

theorem Semantics.Lexical.Numeral.measureSentence_fromHasDegree {E : Type} [Core.Scale.HasDegree E] (dim : String) (entity : E) (deg : DegreePhrase) : measureSentence (MeasurePredicate.fromHasDegree E dim) entity deg = numeralExact deg.value entity

Measure sentences compose correctly with HasDegree-derived predicates.

def Semantics.Lexical.Numeral.numeralWithPrecision {E : Type} [Core.Scale.HasDegree E] (stated : ℚ) (entity : E) (mode : Precision.PrecisionMode) (base : ℚ := 10) : Bool

Numeral semantics with precision mode. "1000 dollars" under exact mode: true iff cost = 1000 "1000 dollars" under approximate mode: true iff Round(cost) = 1000

Equations

• Semantics.Lexical.Numeral.numeralWithPrecision stated entity mode base = Semantics.Lexical.Numeral.Precision.matchesPrecision mode stated (Core.Scale.HasDegree.degree entity) base