Numeral Embedding Semantics

@cite{bylinina-nouwen-2020} @cite{coppock-beaver-2014} @cite{gajewski-2007} @cite{horn-1972} @cite{kaufmann-2012} @cite{kennedy-2015} @cite{meier-2003} @cite{musolino-2004} @cite{nouwen-2006} @cite{penka-2006} @cite{solt-waldon-2019} @cite{kiparsky-kiparsky-1970} @cite{heim-2000}

Formal predictions of lower-bound vs exact numeral theories under embedding: negation, modals, "exactly" modification, conditionals, exhaustification, approximators ("almost"), focus particles ("only"), and QUD-convexity.

The theories agree on bare numerals at the numeral's own cardinality but diverge sharply in embedded environments. All embedding functions are parameterized by NumeralTheory so divergence theorems compare LowerBound vs Exact directly.

Key Results

Embedding	LowerBound	Exact	Diverge?
¬(three) at 4	false (4≥3, so ¬ fails)	true (4≠3)	✓
◇(two) at [3]	true (3≥2)	false (3≠2)	✓
□(three) at [3,4]	true (both ≥3)	false (4≠3)	✓
exactly(three)	informative	redundant	✓
almost(three) at 4	false (polar blocks)	true (4≠3, proximal)	✓
¬(three) convexity	convex (<3)	non-convex (≠3)	✓
EXH(two) at 2	true (≥2 ∧ ¬≥3)	true (=2)	✗ (convergence)

def Semantics.Lexical.Numeral.BareNumeral.succ : BareNumeral → Option BareNumeral

Next-higher BareNumeral (for computing scalar alternatives).

Equations

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

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

Negation: ¬(numeral meaning).

"John doesn't have three children"

• LB: ¬(n ≥ 3) = n < 3
• BL: ¬(n = 3) = n ≠ 3

Equations

• Semantics.Lexical.Numeral.negatedMeaning T w n = !T.meaning w n

def Semantics.Lexical.Numeral.possibilityMeaning (T : NumeralTheory) (w : BareNumeral) (accessible : List ℕ) : Bool

Modal possibility: ∃ accessible world where numeral holds.

"You are allowed to eat two biscuits"

Equations

• Semantics.Lexical.Numeral.possibilityMeaning T w accessible = accessible.any (T.meaning w)

def Semantics.Lexical.Numeral.necessityMeaning (T : NumeralTheory) (w : BareNumeral) (accessible : List ℕ) : Bool

Modal necessity: ∀ accessible worlds, numeral holds.

"You must read three books"

Equations

• Semantics.Lexical.Numeral.necessityMeaning T w accessible = accessible.all (T.meaning w)

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

"Exactly" modification: always exact regardless of base theory.

"John has exactly three children" — always means =n.

Equations

• Semantics.Lexical.Numeral.exactlyMeaning w n = Semantics.Lexical.Numeral.maxMeaning Semantics.Lexical.Numeral.OrderingRel.eq w.toNat n

def Semantics.Lexical.Numeral.conditionalMeaning (T : NumeralTheory) (w : BareNumeral) (n : ℕ) (consequent : ℕ → Bool) : Bool

Conditional antecedent: material conditional with numeral in restrictor.

"If you have three children, you qualify" Conditional is true when antecedent is false OR consequent is true.

Equations

• Semantics.Lexical.Numeral.conditionalMeaning T w n consequent = (!T.meaning w n || consequent n)

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

Exhaustivity operator: strengthens meaning by negating the next stronger alternative.

Under LB: EXH(≥n) = ≥n ∧ ¬(≥(n+1)) = =n Under BL: EXH(=n) = =n (vacuous, since =n already excludes n+1)

Equations

• Semantics.Lexical.Numeral.exh T w n = (T.meaning w n && match w.succ with | some w' => !T.meaning w' n | none => true)

def Semantics.Lexical.Numeral.exhUnderPossibility (T : NumeralTheory) (w : BareNumeral) (accessible : List ℕ) : Bool

EXH-under-◇: ◇(EXH(numeral)) — exhaustification below the modal.

"It's possible to eat exactly two..."

Equations

• Semantics.Lexical.Numeral.exhUnderPossibility T w accessible = accessible.any (Semantics.Lexical.Numeral.exh T w)

def Semantics.Lexical.Numeral.exhOverPossibility (T : NumeralTheory) (w : BareNumeral) (accessible : List ℕ) : Bool

EXH-over-◇: EXH(◇(numeral)) — exhaustification above the modal.

"It's possible to eat at-least-two but NOT possible to eat at-least-three" Captures Bylinina & Nouwen's (35)/(36) scope distinction.

Equations

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

theorem Semantics.Lexical.Numeral.negation_divergence_above : negatedMeaning LowerBound BareNumeral.three 4 = false ∧ negatedMeaning Exact BareNumeral.three 4 = true

Core negation divergence: above the numeral.

"John doesn't have three children" in world with 4 children:

• LB: ¬(4 ≥ 3) = false (4 is at-least-3, so negation fails)
• BL: ¬(4 = 3) = true (4 is not-exactly-3, so negation succeeds)

theorem Semantics.Lexical.Numeral.negation_agreement_below : negatedMeaning LowerBound BareNumeral.three 2 = true ∧ negatedMeaning Exact BareNumeral.three 2 = true

Negation agreement below the numeral.

Both theories agree: "doesn't have three" is true for someone with 2.

theorem Semantics.Lexical.Numeral.negation_agreement_at : negatedMeaning LowerBound BareNumeral.three 3 = false ∧ negatedMeaning Exact BareNumeral.three 3 = false

Negation agreement at the numeral.

Both theories agree: "doesn't have three" is false for someone with exactly 3.

theorem Semantics.Lexical.Numeral.entailment_reversal_under_negation : (LowerBound.meaning BareNumeral.three 4 = true ∧ Exact.meaning BareNumeral.three 4 = false) ∧ negatedMeaning LowerBound BareNumeral.three 4 = false ∧ negatedMeaning Exact BareNumeral.three 4 = true

Entailment reversal under negation.

In isolation: BL entails LB (=3 → ≥3). Under negation: ¬(≥3) entails ¬(=3) but not vice versa. World 4 witnesses the asymmetry.

theorem Semantics.Lexical.Numeral.exactly_redundant_exact (w : BareNumeral) (n : ℕ) : exactlyMeaning w n = Exact.meaning w n

"Exactly" is redundant under Exact: "exactly three" = "three" (BL).

Both reduce to maxMeaning.eq — definitionally equal.

theorem Semantics.Lexical.Numeral.exactly_informative_lowerBound : LowerBound.meaning BareNumeral.three 4 = true ∧ exactlyMeaning BareNumeral.three 4 = false

"Exactly" is informative under LowerBound: restricts ≥3 to =3.

At world 4: LB says "three" is true (4 ≥ 3), but "exactly three" is false (4 ≠ 3).

theorem Semantics.Lexical.Numeral.exactly_full_comparison : (LowerBound.meaning BareNumeral.three 3 = true ∧ exactlyMeaning BareNumeral.three 3 = true) ∧ (LowerBound.meaning BareNumeral.three 4 = true ∧ exactlyMeaning BareNumeral.three 4 = false) ∧ Exact.meaning BareNumeral.three 4 = false ∧ exactlyMeaning BareNumeral.three 4 = false

Full "exactly" comparison: agrees at n, diverges above under LB.

theorem Semantics.Lexical.Numeral.modal_possibility_divergence : possibilityMeaning LowerBound BareNumeral.two [3] = true ∧ possibilityMeaning Exact BareNumeral.two [3] = false

Modal possibility: LB is satisfiable by more worlds.

"You are allowed to eat two biscuits" with only world 3 accessible:

• LB: ◇(≥2) at [3] = true (3 ≥ 2)
• BL: ◇(=2) at [3] = false (3 ≠ 2)

theorem Semantics.Lexical.Numeral.modal_necessity_divergence : necessityMeaning LowerBound BareNumeral.three [3, 4] = true ∧ necessityMeaning Exact BareNumeral.three [3, 4] = false

Modal necessity: BL is harder to satisfy.

"You must read three books" with accessible worlds [3, 4]:

• LB: □(≥3) = true (3 ≥ 3 ∧ 4 ≥ 3)
• BL: □(=3) = false (4 ≠ 3)

theorem Semantics.Lexical.Numeral.modal_necessity_agreement_exact : necessityMeaning LowerBound BareNumeral.three [3] = true ∧ necessityMeaning Exact BareNumeral.three [3] = true

Modal necessity agreement: when all worlds match exactly.

theorem Semantics.Lexical.Numeral.conditional_restrictor_divergence : LowerBound.meaning BareNumeral.three 4 = true ∧ Exact.meaning BareNumeral.three 4 = false

Conditional antecedent divergence.

"If you have three children, you qualify" — does having 4 children trigger it?

• LB: 4 ≥ 3 = true, so antecedent holds
• BL: 4 = 3 = false, so antecedent fails (conditional vacuously true)

theorem Semantics.Lexical.Numeral.restrictor_domain_differs : (LowerBound.meaning BareNumeral.three 3 = true ∧ LowerBound.meaning BareNumeral.three 4 = true) ∧ Exact.meaning BareNumeral.three 3 = true ∧ Exact.meaning BareNumeral.three 4 = false

Universal restrictor: different domains.

"Every student who read three books passed"

• LB restrictor includes {3, 4, 5,...}
• BL restrictor includes only {3}

theorem Semantics.Lexical.Numeral.exh_strengthens_lowerBound : exh LowerBound BareNumeral.two 2 = true ∧ exh LowerBound BareNumeral.two 3 = false

EXH strengthens LowerBound: ≥n → =n.

EXH("two" under LB) at world 2 = true, at world 3 = false.

theorem Semantics.Lexical.Numeral.exh_vacuous_exact : exh Exact BareNumeral.two 1 = Exact.meaning BareNumeral.two 1 ∧ exh Exact BareNumeral.two 2 = Exact.meaning BareNumeral.two 2 ∧ exh Exact BareNumeral.two 3 = Exact.meaning BareNumeral.two 3

EXH is vacuous under Exact: =n is already exact.

exh(BL, "two", n) = BL.meaning("two", n) for n ∈ {1, 2, 3}.

theorem Semantics.Lexical.Numeral.exh_convergence : exh LowerBound BareNumeral.two 1 = exh Exact BareNumeral.two 1 ∧ exh LowerBound BareNumeral.two 2 = exh Exact BareNumeral.two 2 ∧ exh LowerBound BareNumeral.two 3 = exh Exact BareNumeral.two 3

After EXH, both theories converge: EXH(LB) = EXH(BL) = =n.

This is the key result: pragmatic strengthening under LB converges to the BL bare-numeral meaning.

theorem Semantics.Lexical.Numeral.exh_scope_diverges_lowerBound : exhUnderPossibility LowerBound BareNumeral.two [2, 3] = true ∧ exhOverPossibility LowerBound BareNumeral.two [2, 3] = false

EXH-under-◇ vs EXH-over-◇ diverge under LB with worlds [2, 3].

"You are allowed to eat two biscuits":

• EXH-under-◇: ◇(EXH(≥2)) = ◇(=2) — possible to eat exactly 2 → true
• EXH-over-◇: EXH(◇(≥2)) = ◇(≥2) ∧ ¬◇(≥3) — false (world 3 makes ◇(≥3) true)

theorem Semantics.Lexical.Numeral.exh_scope_agrees_restricted : exhUnderPossibility LowerBound BareNumeral.two [2] = true ∧ exhOverPossibility LowerBound BareNumeral.two [2] = true

Under restricted access [2], EXH scope doesn't matter for LB.

theorem Semantics.Lexical.Numeral.exh_scope_diverges_exact : exhUnderPossibility Exact BareNumeral.two [2, 3] = true ∧ exhOverPossibility Exact BareNumeral.two [2, 3] = false

EXH-scope divergence under BL with worlds [2, 3].

• EXH-under-◇: ◇(EXH(=2)) = ◇(=2) — true (world 2)
• EXH-over-◇: EXH(◇(=2)) = ◇(=2) ∧ ¬◇(=3) — false (world 3 exists)

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

Proximity to numeral value: within distance 1.

Equations

• Semantics.Lexical.Numeral.isProximal m n = (n + 1 == m || n == m || n == m + 1)

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

"Almost n": proximal to n but the numeral's meaning is false. Proximal/polar decomposition from @cite{nouwen-2006}.

Under LB: close to n AND ¬(≥n) → only values below n Under BL: close to n AND ¬(=n) → values above OR below n

The LB/BL divergence argument is from @cite{penka-2006}. @cite{nouwen-2006} shows that polar orientation is context-dependent in general (e.g., "almost that warm" vs "almost that cold" orient in opposite directions).

Equations

• Semantics.Lexical.Numeral.almostMeaning T w n = (Semantics.Lexical.Numeral.isProximal w.toNat n && !T.meaning w n)

theorem Semantics.Lexical.Numeral.almost_diverges_above : almostMeaning LowerBound BareNumeral.three 4 = false ∧ almostMeaning Exact BareNumeral.three 4 = true

"Almost three" diverges above: LB excludes 4, BL includes 4.

Under LB: 4 ≥ 3 so the polar component blocks it. Under BL: 4 ≠ 3 and 4 is proximal to 3, so "almost three" holds.

theorem Semantics.Lexical.Numeral.almost_asymmetry : (almostMeaning LowerBound BareNumeral.three 2 = true ∧ almostMeaning Exact BareNumeral.three 2 = true) ∧ almostMeaning LowerBound BareNumeral.three 4 = false ∧ almostMeaning Exact BareNumeral.three 4 = true

Full "almost" asymmetry: both agree on 2, diverge on 4.

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

"Only n" with numeral in focus: assertion + exclusion of stronger alternatives.

Truth-conditionally equivalent to EXH on the numeral meaning.

Equations

• Semantics.Lexical.Numeral.onlyMeaning T w n = Semantics.Lexical.Numeral.exh T w n

theorem Semantics.Lexical.Numeral.only_eq_exh (T : NumeralTheory) (w : BareNumeral) (n : ℕ) : onlyMeaning T w n = exh T w n

"Only" on numerals is truth-conditionally equivalent to EXH.

theorem Semantics.Lexical.Numeral.only_informative_lowerBound : LowerBound.meaning BareNumeral.three 4 = true ∧ onlyMeaning LowerBound BareNumeral.three 4 = false ∧ Exact.meaning BareNumeral.three 4 = false ∧ onlyMeaning Exact BareNumeral.three 4 = false

"Only" is truth-conditionally informative under LB, vacuous under BL.

"Only three students passed":

• Under LB: "three" at 4 is true (4≥3), but "only three" at 4 is false → informative
• Under BL: "three" at 4 is already false (4≠3), "only three" also false → vacuous

def Semantics.Lexical.Numeral.extendedWorlds : List ℕ

Worlds 0 through 5 for extended embedding tests.

Equations

• Semantics.Lexical.Numeral.extendedWorlds = [0, 1, 2, 3, 4, 5]

def Semantics.Lexical.Numeral.isConvex (worlds : List ℕ) (f : ℕ → Bool) : Bool

Convexity: the set of true values on sorted worlds has no internal gaps.

For every pair of true values a < c, all intermediate b must also be true. Non-convex denotations are predicted to be infelicitous in neutral QUD contexts.

Equations

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

theorem Semantics.Lexical.Numeral.negation_convexity_divergence : isConvex extendedWorlds (negatedMeaning LowerBound BareNumeral.three) = true ∧ isConvex extendedWorlds (negatedMeaning Exact BareNumeral.three) = false

Negation convexity divergence.

¬(≥3) on [0.5] = {0,1,2} — convex (no gaps). ¬(=3) on [0.5] = {0,1,2,4,5} — non-convex (gap at 3).

BL correctly predicts "She doesn't have 40 sheep" is infelicitous in neutral context (non-convex answer). LB incorrectly predicts felicity.

def Semantics.Lexical.Numeral.exhUnderNominalQ (T : NumeralTheory) (w : BareNumeral) (individuals : List ℕ) : Bool

EXH scoped under a nominal quantifier (∃): each individual is exhaustified.

"Some students answered exactly three questions" Under LB: ∃x[student(x) ∧ EXH(≥3)(answers(x))] = some student answered exactly 3. This is the WEAK reading — per-student exhaustification.

Equations

• Semantics.Lexical.Numeral.exhUnderNominalQ T w individuals = individuals.any (Semantics.Lexical.Numeral.exh T w)

def Semantics.Lexical.Numeral.exhOverNominalQ (T : NumeralTheory) (w : BareNumeral) (individuals : List ℕ) : Bool

EXH scoped over a nominal quantifier (∃): exhaustifies the existential claim.

"Some students answered exactly three questions" — strong reading: EXH(∃x[student(x) ∧ ≥3(answers(x))]) = some answered ≥3 AND none answered ≥4. Heim-Kennedy BLOCKS this reading for numerals.

Equations

• Semantics.Lexical.Numeral.exhOverNominalQ T w individuals = (individuals.any (T.meaning w) && match w.succ with | some w' => !individuals.any (T.meaning w') | none => true)

theorem Semantics.Lexical.Numeral.heimKennedy_nominal_blocked : exhUnderNominalQ LowerBound BareNumeral.three [3, 4] = true ∧ exhOverNominalQ LowerBound BareNumeral.three [3, 4] = false

Heim-Kennedy generalization: degree operators scope over modals but NOT over nominal quantifiers (@cite{heim-2000}, @cite{bylinina-nouwen-2020} §6, examples 40–41).

With individuals [3, 4] (one answered 3, one answered 4):

• Weak reading (EXH under ∃): true — the student with 3 answered exactly 3.
• Strong reading (EXH over ∃): false — blocked because someone answered 4 (≥4).

Contrast with the modal case (exh_scope_diverges_lowerBound), where BOTH EXH-under-◇ and EXH-over-◇ are available. The asymmetry is precisely what the degree quantifier analysis predicts via QR constraints.

theorem Semantics.Lexical.Numeral.modal_both_scopes_available : exhUnderPossibility LowerBound BareNumeral.two [2] = true ∧ exhOverPossibility LowerBound BareNumeral.two [2] = true

The modal case allows both scope configurations (contrast with Heim-Kennedy).

theorem Semantics.Lexical.Numeral.heimKennedy_vacuous_exact : exhUnderNominalQ Exact BareNumeral.three [3, 4] = true ∧ exhOverNominalQ Exact BareNumeral.three [3, 4] = false

Under Exact, Heim-Kennedy is vacuous: EXH adds nothing to =n, so neither scope yields a strong reading over nominal quantifiers.

theorem Semantics.Lexical.Numeral.imperative_compliance_divergence : LowerBound.meaning BareNumeral.three 5 = true ∧ Exact.meaning BareNumeral.three 5 = false

Imperative compliance divergence.

"Read three books!" — reading 5 books:

• LB: 5 ≥ 3 → compliant
• BL: 5 ≠ 3 → non-compliant

theorem Semantics.Lexical.Numeral.doubt_as_neg_raising : negatedMeaning LowerBound BareNumeral.three 4 = false ∧ negatedMeaning Exact BareNumeral.three 4 = true

Neg-raising "doubt" reduces to negation.

"I doubt three students passed" ≈ believe(¬(three passed)).

theorem Semantics.Lexical.Numeral.factive_presupposition_divergence : LowerBound.meaning BareNumeral.three 5 = true ∧ Exact.meaning BareNumeral.three 5 = false

Factive presupposition divergence.

"I'm surprised three students passed" presupposes the numeral meaning. At world 5: LB presupposition satisfied (5 ≥ 3), BL violated (5 ≠ 3).

theorem Semantics.Lexical.Numeral.degree_too_monotonicity : (LowerBound.meaning BareNumeral.three 3 = true ∧ LowerBound.meaning BareNumeral.three 4 = true) ∧ Exact.meaning BareNumeral.three 3 = true ∧ Exact.meaning BareNumeral.three 4 = false

Degree "too" monotonicity.

"Three is too many" — under LB, entails "four is too many" (both satisfy ≥3). Under BL, no such entailment (4 does not satisfy =3).

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

Acquisition prediction.

"Two horses jumped" when 3 jumped:

• LB: 3 ≥ 2 → should be accepted
• BL: 3 ≠ 2 → should be rejected Children reject, supporting BL.

structure Semantics.Lexical.Numeral.EmbeddingPrediction : Type

A prediction for a specific embedding environment.

• embedding : String
• lowerBoundResult : Bool
• exactResult : Bool

instance Semantics.Lexical.Numeral.instReprEmbeddingPrediction : Repr EmbeddingPrediction

Equations

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

def Semantics.Lexical.Numeral.instReprEmbeddingPrediction.repr : EmbeddingPrediction → ℕ → Std.Format

Equations

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

def Semantics.Lexical.Numeral.instBEqEmbeddingPrediction.beq : EmbeddingPrediction → EmbeddingPrediction → Bool

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Lexical.Numeral.instBEqEmbeddingPrediction.beq x✝¹ x✝ = false

instance Semantics.Lexical.Numeral.instBEqEmbeddingPrediction : BEq EmbeddingPrediction

Equations

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

def Semantics.Lexical.Numeral.EmbeddingPrediction.diverges (p : EmbeddingPrediction) : Bool

Do the theories diverge for this prediction?

Equations

• p.diverges = (p.lowerBoundResult != p.exactResult)

def Semantics.Lexical.Numeral.embeddingDivergences : List EmbeddingPrediction

Summary of key embedding divergence points.

Equations

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

theorem Semantics.Lexical.Numeral.divergence_point_count : (List.filter EmbeddingPrediction.diverges embeddingDivergences).length = 8

8 of 10 test points show theory divergence.