inductive Fragments.English.NumeralModifiers.ModifierType : Type

Semantic type of a numeral modifier.

Modifiers can be:

• Tolerance-based: "around n" = λx. |n-x| ≤ y (with hidden tolerance y)
• Interval-based: "between a b" = λx. a ≤ x ≤ b
• Exactifier: "exactly n" = λx. x = n
• Bound-setting: "at least n", "more than n", etc.

• tolerance : ModifierType
• interval : ModifierType
• exactifier : ModifierType
• bound : ModifierType
• approximator : ModifierType

def Fragments.English.NumeralModifiers.instReprModifierType.repr : ModifierType → ℕ → Std.Format

Equations

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

instance Fragments.English.NumeralModifiers.instReprModifierType : Repr ModifierType

Equations

• Fragments.English.NumeralModifiers.instReprModifierType = { reprPrec := Fragments.English.NumeralModifiers.instReprModifierType.repr }

instance Fragments.English.NumeralModifiers.instDecidableEqModifierType : DecidableEq ModifierType

Equations

• Fragments.English.NumeralModifiers.instDecidableEqModifierType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.English.NumeralModifiers.instBEqModifierType.beq : ModifierType → ModifierType → Bool

Equations

• Fragments.English.NumeralModifiers.instBEqModifierType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.English.NumeralModifiers.instBEqModifierType : BEq ModifierType

Equations

• Fragments.English.NumeralModifiers.instBEqModifierType = { beq := Fragments.English.NumeralModifiers.instBEqModifierType.beq }

inductive Fragments.English.NumeralModifiers.PragmaticFunction : Type

Pragmatic function of a numeral modifier.

Following Égré et al. (2023): modifiers signal the shape of the speaker's private distribution over the true value.

• peakedSignal : PragmaticFunction
• flatSignal : PragmaticFunction
• pointSignal : PragmaticFunction
• boundSignal : PragmaticFunction

instance Fragments.English.NumeralModifiers.instReprPragmaticFunction : Repr PragmaticFunction

Equations

• Fragments.English.NumeralModifiers.instReprPragmaticFunction = { reprPrec := Fragments.English.NumeralModifiers.instReprPragmaticFunction.repr }

def Fragments.English.NumeralModifiers.instReprPragmaticFunction.repr : PragmaticFunction → ℕ → Std.Format

Equations

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

instance Fragments.English.NumeralModifiers.instDecidableEqPragmaticFunction : DecidableEq PragmaticFunction

Equations

• Fragments.English.NumeralModifiers.instDecidableEqPragmaticFunction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.English.NumeralModifiers.instBEqPragmaticFunction.beq : PragmaticFunction → PragmaticFunction → Bool

Equations

• Fragments.English.NumeralModifiers.instBEqPragmaticFunction.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.English.NumeralModifiers.instBEqPragmaticFunction : BEq PragmaticFunction

Equations

• Fragments.English.NumeralModifiers.instBEqPragmaticFunction = { beq := Fragments.English.NumeralModifiers.instBEqPragmaticFunction.beq }

inductive Fragments.English.NumeralModifiers.EvaluativeValence : Type

Evaluative valence of a bound-setting modifier.

Distinguishes modifiers with the same truth conditions but different framing:

• "at most 100" (negative valence) → reversed framing (endorsed more in negative contexts)
• "up to 100" (positive valence) → standard framing (endorsed more in positive contexts)

• positive : EvaluativeValence
• negative : EvaluativeValence
• neutral : EvaluativeValence

def Fragments.English.NumeralModifiers.instReprEvaluativeValence.repr : EvaluativeValence → ℕ → Std.Format

Equations

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

instance Fragments.English.NumeralModifiers.instReprEvaluativeValence : Repr EvaluativeValence

Equations

• Fragments.English.NumeralModifiers.instReprEvaluativeValence = { reprPrec := Fragments.English.NumeralModifiers.instReprEvaluativeValence.repr }

instance Fragments.English.NumeralModifiers.instDecidableEqEvaluativeValence : DecidableEq EvaluativeValence

Equations

• Fragments.English.NumeralModifiers.instDecidableEqEvaluativeValence x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.English.NumeralModifiers.instBEqEvaluativeValence.beq : EvaluativeValence → EvaluativeValence → Bool

Equations

• Fragments.English.NumeralModifiers.instBEqEvaluativeValence.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.English.NumeralModifiers.instBEqEvaluativeValence : BEq EvaluativeValence

Equations

• Fragments.English.NumeralModifiers.instBEqEvaluativeValence = { beq := Fragments.English.NumeralModifiers.instBEqEvaluativeValence.beq }

structure Fragments.English.NumeralModifiers.NumeralModifierEntry : Type

Lexical entry for a numeral modifier.

• form : String

  Surface form

• modType : ModifierType

  Modifier type

• pragFunction : PragmaticFunction

  Pragmatic function

• requiresRound : Bool

  Requires round numeral?

• isVague : Bool

  Is the modifier vague (tolerance-based)?

• conveysShape : Bool

  Does it convey shape information beyond support?

• soritesSusceptible : Bool

  Can it license sorites chains?

• boundDir : Option Semantics.Lexical.Numeral.BoundDirection

  Bound direction (for bound-setting modifiers)

• modClass : Option Semantics.Lexical.Numeral.ModifierClass

  Modifier class (for bound-setting modifiers)

• evaluativeValence : EvaluativeValence

  Evaluative valence (@cite{blok-2015} / @cite{claus-walch-2024})

• generatesIgnorance : Bool

  Does this modifier generate ignorance implicatures?

• notes : String

  Notes

instance Fragments.English.NumeralModifiers.instReprNumeralModifierEntry : Repr NumeralModifierEntry

Equations

• Fragments.English.NumeralModifiers.instReprNumeralModifierEntry = { reprPrec := Fragments.English.NumeralModifiers.instReprNumeralModifierEntry.repr }

def Fragments.English.NumeralModifiers.instReprNumeralModifierEntry.repr : NumeralModifierEntry → ℕ → Std.Format

Equations

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

instance Fragments.English.NumeralModifiers.instBEqNumeralModifierEntry : BEq NumeralModifierEntry

Equations

• Fragments.English.NumeralModifiers.instBEqNumeralModifierEntry = { beq := Fragments.English.NumeralModifiers.instBEqNumeralModifierEntry.beq }

def Fragments.English.NumeralModifiers.instBEqNumeralModifierEntry.beq : NumeralModifierEntry → NumeralModifierEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.English.NumeralModifiers.instBEqNumeralModifierEntry.beq x✝¹ x✝ = false

def Fragments.English.NumeralModifiers.about : NumeralModifierEntry

"about": tolerance-based approximation.

The most common English approximator. Used in BSB2022's stimuli: "about fifty minutes" vs "fifty minutes" vs "forty-nine minutes."

⟦about n⟧ = λy.λx. |n-x| ≤ y Pragmatically signals peaked private distribution centered on n.

Source: @cite{beltrama-solt-burnett-2023}

Equations

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

def Fragments.English.NumeralModifiers.around : NumeralModifierEntry

"around": tolerance-based approximation.

⟦around n⟧ = λy.λx. |n-x| ≤ y Pragmatically signals peaked private distribution centered on n.

Source: Égré et al. 2023

Equations

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

def Fragments.English.NumeralModifiers.approximately : NumeralModifierEntry

"approximately": explicit tolerance marker.

Similar to "around" but more formal register. Interacts with roundness: "approximately 100" natural, "approximately 99" marked.

Source: Phenomena/Gradability/Imprecision/Numerals.lean

Equations

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

def Fragments.English.NumeralModifiers.roughly : NumeralModifierEntry

"roughly": informal tolerance marker.

Behaves like "around" pragmatically.

Equations

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

def Fragments.English.NumeralModifiers.between : NumeralModifierEntry

"between... and...": interval specification.

⟦between a and b⟧ = λx. a ≤ x ≤ b Pragmatically signals flat distribution over [a,b]. Does NOT convey shape information (only support).

Source: Égré et al. 2023

Equations

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

def Fragments.English.NumeralModifiers.exactly : NumeralModifierEntry

"exactly": precision enforcer.

⟦exactly n⟧ = λx. x = n Removes imprecision. Point signal.

Source: Phenomena/Gradability/Imprecision/Numerals.lean (ExactlyModifierDatum)

Equations

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

def Fragments.English.NumeralModifiers.precisely : NumeralModifierEntry

"precisely": formal exactifier.

Behaves like "exactly" semantically.

Equations

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

def Fragments.English.NumeralModifiers.atLeast : NumeralModifierEntry

"at least n": Class B lower bound (max ≥ n).

Generates ignorance implicatures because compatible with the bare reading. Neutral evaluative valence.

Equations

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

def Fragments.English.NumeralModifiers.atMost : NumeralModifierEntry

"at most n": Class B upper bound (max ≤ n).

Generates ignorance implicatures. NEGATIVE evaluative valence: "at most" is endorsed more in negative contexts. @cite{claus-walch-2024} show this produces reversed framing effects.

Equations

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

def Fragments.English.NumeralModifiers.moreThan : NumeralModifierEntry

"more than n": Class A lower bound (max > n).

Does NOT generate ignorance implicatures (excludes the bare-numeral world). Neutral evaluative valence.

Equations

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

def Fragments.English.NumeralModifiers.fewerThan : NumeralModifierEntry

"fewer than n": Class A upper bound (max < n).

Does NOT generate ignorance implicatures (excludes the bare-numeral world). Neutral evaluative valence.

Equations

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

def Fragments.English.NumeralModifiers.upTo : NumeralModifierEntry

"up to n": Class B upper bound (max ≤ n).

Same truth conditions as "at most n", but POSITIVE evaluative valence. @cite{claus-walch-2024} show "up to" follows standard framing (endorsed more in positive contexts), unlike "at most".

Equations

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

def Fragments.English.NumeralModifiers.fromOn : NumeralModifierEntry

"from n on": Class B lower bound (max ≥ n).

Positive evaluative valence: invites positive evaluation of the quantity. Generates ignorance implicatures (compatible with bare reading).

Equations

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

def Fragments.English.NumeralModifiers.almost : NumeralModifierEntry

"almost": proximal approximation with polar exclusion.

⟦almost n⟧ = λx. close(x, n) ∧ ¬(x = n) [or ¬(x ≥ n) under LB]

Unlike tolerance modifiers ("around"), "almost" EXCLUDES the target value (the polar component). @cite{nouwen-2006} decomposes "almost" into proximal (close to p) and polar (¬p) components. This creates a key LB/BL divergence:

• Under LB: "almost three" = close to 3 AND <3 → only values below 3
• Under BL: "almost three" = close to 3 AND ≠3 → values above OR below 3

The empirical asymmetry (below only) is argued by @cite{penka-2006} to favor LB. @cite{nouwen-2006} shows that polar orientation is in general context-dependent (e.g., "almost that warm" vs "almost that cold" orient in opposite directions depending on the scale).

Source: @cite{penka-2006} "Almost there: The meaning of almost"; @cite{nouwen-2006} "Remarks on the Polar Orientation of Almost".

Equations

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

def Fragments.English.NumeralModifiers.nearly : NumeralModifierEntry

"nearly": synonym of "almost" with slight register difference.

Same proximal + polar semantics as "almost".

Equations

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

structure Fragments.English.NumeralModifiers.ModifierScale : Type

Informativity scale for numeral modifiers.

Ordered by how much information about the true value they convey: exactly > around > between

"Exactly" gives the most information (point), "around" gives shape, "between" gives only support.

• stronger : NumeralModifierEntry

  More informative (stronger)

• weaker : NumeralModifierEntry

  Less informative (weaker)

• isScalarPair : Bool

  Scalar relation holds

instance Fragments.English.NumeralModifiers.instReprModifierScale : Repr ModifierScale

Equations

• Fragments.English.NumeralModifiers.instReprModifierScale = { reprPrec := Fragments.English.NumeralModifiers.instReprModifierScale.repr }

def Fragments.English.NumeralModifiers.instReprModifierScale.repr : ModifierScale → ℕ → Std.Format

Equations

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

def Fragments.English.NumeralModifiers.exactlyAroundScale : ModifierScale

"Exactly" is more informative than "around"

Equations

• Fragments.English.NumeralModifiers.exactlyAroundScale = { stronger := Fragments.English.NumeralModifiers.exactly, weaker := Fragments.English.NumeralModifiers.around, isScalarPair := true }

def Fragments.English.NumeralModifiers.aroundBetweenScale : ModifierScale

"Around" is more informative than "between" (conveys shape)

Equations

• Fragments.English.NumeralModifiers.aroundBetweenScale = { stronger := Fragments.English.NumeralModifiers.around, weaker := Fragments.English.NumeralModifiers.between, isScalarPair := true }

def Fragments.English.NumeralModifiers.toleranceModifiers : List NumeralModifierEntry

Equations

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

def Fragments.English.NumeralModifiers.intervalModifiers : List NumeralModifierEntry

Equations

• Fragments.English.NumeralModifiers.intervalModifiers = [Fragments.English.NumeralModifiers.between]

def Fragments.English.NumeralModifiers.exactifiers : List NumeralModifierEntry

Equations

• Fragments.English.NumeralModifiers.exactifiers = [Fragments.English.NumeralModifiers.exactly, Fragments.English.NumeralModifiers.precisely]

def Fragments.English.NumeralModifiers.boundModifiers : List NumeralModifierEntry

Equations

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

def Fragments.English.NumeralModifiers.classAModifiers : List NumeralModifierEntry

Equations

• Fragments.English.NumeralModifiers.classAModifiers = [Fragments.English.NumeralModifiers.moreThan, Fragments.English.NumeralModifiers.fewerThan]

def Fragments.English.NumeralModifiers.classBModifiers : List NumeralModifierEntry

Equations

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

def Fragments.English.NumeralModifiers.approximatorModifiers : List NumeralModifierEntry

Equations

• Fragments.English.NumeralModifiers.approximatorModifiers = [Fragments.English.NumeralModifiers.almost, Fragments.English.NumeralModifiers.nearly]

def Fragments.English.NumeralModifiers.allModifiers : List NumeralModifierEntry

Equations

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

def Fragments.English.NumeralModifiers.modifierScales : List ModifierScale

Equations

• Fragments.English.NumeralModifiers.modifierScales = [Fragments.English.NumeralModifiers.exactlyAroundScale, Fragments.English.NumeralModifiers.aroundBetweenScale]

theorem Fragments.English.NumeralModifiers.tolerance_modifiers_convey_shape : (toleranceModifiers.all fun (x : NumeralModifierEntry) => x.conveysShape) = true

All tolerance modifiers convey shape information.

theorem Fragments.English.NumeralModifiers.non_tolerance_no_shape : ((intervalModifiers ++ exactifiers).all fun (x : NumeralModifierEntry) => x.conveysShape == false) = true

No interval or exact modifiers convey shape information.

theorem Fragments.English.NumeralModifiers.only_tolerance_sorites : (toleranceModifiers.all fun (x : NumeralModifierEntry) => x.soritesSusceptible) = true ∧ ((intervalModifiers ++ exactifiers).all fun (x : NumeralModifierEntry) => x.soritesSusceptible == false) = true

Only tolerance modifiers are sorites-susceptible.

theorem Fragments.English.NumeralModifiers.classB_all_generate_ignorance : (classBModifiers.all fun (x : NumeralModifierEntry) => x.generatesIgnorance) = true

All Class B modifiers generate ignorance implicatures.

theorem Fragments.English.NumeralModifiers.classA_no_ignorance : (classAModifiers.all fun (x : NumeralModifierEntry) => x.generatesIgnorance == false) = true

No Class A modifiers generate ignorance implicatures.

theorem Fragments.English.NumeralModifiers.atMost_upTo_differ_only_in_valence : atMost.modType = upTo.modType ∧ atMost.modClass = upTo.modClass ∧ atMost.boundDir = upTo.boundDir ∧ atMost.evaluativeValence ≠ upTo.evaluativeValence

"at most" and "up to" differ only in evaluative valence.

Same modType, modClass, boundDir, but different evaluativeValence. This is the key @cite{blok-2015} / @cite{claus-walch-2024} observation.

theorem Fragments.English.NumeralModifiers.bound_modifiers_all_bound : (boundModifiers.all fun (x : NumeralModifierEntry) => x.modType == ModifierType.bound) = true

All bound modifiers are classified as bound type.

theorem Fragments.English.NumeralModifiers.bound_modifiers_not_vague : (boundModifiers.all fun (x : NumeralModifierEntry) => x.isVague == false) = true

No bound modifiers are vague.

theorem Fragments.English.NumeralModifiers.approximators_not_sorites : (approximatorModifiers.all fun (x : NumeralModifierEntry) => x.soritesSusceptible == false) = true

Approximators are not sorites-susceptible (unlike tolerance modifiers).

theorem Fragments.English.NumeralModifiers.approximators_distinct_from_tolerance : (approximatorModifiers.all fun (x : NumeralModifierEntry) => x.modType == ModifierType.approximator) = true ∧ (toleranceModifiers.all fun (x : NumeralModifierEntry) => x.modType == ModifierType.tolerance) = true

Approximators have polar exclusion (distinguished from tolerance modifiers by type).