Documentation

Linglib.Semantics.Quantification.Numerals.Basic

Numeral meanings #

This file collects what is specific to numerals over the degree comparisons of Semantics/Degree/Comparison.lean. A bare numeral and its four modifications, more than, fewer than, at least and at most, are the five comparisons of Degree.Comparison: in Kennedy's de-Fregean semantics the form with relation REL and number m is true of a degree property whose greatest degree stands in REL to m. On counts the form denotes the interval c.interval m, and on worlds measured by μ the set μ ⁻¹' c.interval m, so the forms have no names of their own here. The meanings of the modified forms are common ground. Accounts differ on the bare numeral, which has the two-sided meaning Comparison.eq.interval m for Kennedy and the lower-bounded meaning Comparison.ge.interval m in the tradition of Horn, each account deriving the other reading. Exhaustifying the lower-bounded meaning against the scale of higher numerals gives the two-sided one, and Kennedy's type lowering, existential closure over the two-sided meaning at the degrees above, takes it to the lower-bounded one.

Main definitions #

Numerals.ModifierClass, Numerals.ModifierKind: Nouwen's two classes of numeral modifier and the constructions modifiers are built on, with ModifierKind.modifierClass.
Numerals.NumeralModifier: a numeral modifier as a lexical item, its form, kind and readings, each reading a Modifier (Set ℕ) of sets of amounts.
Numerals.exhNumeral: the lower-bounded meaning exhaustified against the next numeral.

Main results #

Numerals.exhNumeral_eq: the exhaustified lower-bounded meaning is the two-sided one.
Numerals.mem_exhNumeral_iff_exhAgainst: exhaustifying against the next numeral is exhaustifying against the whole scale.

References #

Numeral modifiers #

inductive Numerals.ModifierClass :

The two classes of numeral modifiers of [Nou10]. A Class A modifier relates the numeral to a definite amount, so a hexagon has fewer than 11 sides is a weak truth. A Class B modifier places a bound on a range of amounts, so a hexagon has at most 10 sides is odd and the modifier conveys that the speaker does not know the amount.

[Ken15] reduces the split to the ordering the modifier expresses, exclusive for Class A and inclusive for Class B (Degree.Comparison.boundary_mem), and derives the ignorance as an implicature. The categorical pattern is contested, since [SBH12] show that at most and up to dissociate, [CCDR22] find the ignorance contrast graded and dependent on the question under discussion, and [Eng18] derives the inferences of comparative numerals from granularity.

classA : ModifierClass
classB : ModifierClass

Instances For

def Numerals.instReprModifierClass.repr :

ModifierClass → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Numerals.instReprModifierClass :

Repr ModifierClass

Equations

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

@[instance_reducible]

instance Numerals.instDecidableEqModifierClass :

DecidableEq ModifierClass

Equations

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

inductive Numerals.ModifierKind :

The kinds of numeral modifier in [Nou10]'s survey, by the construction the modifier is built on.

comparative : ModifierKind
A comparative, such as more than or fewer than.
superlative : ModifierKind
A superlative, such as at least or at most.
locative : ModifierKind
A locative preposition, such as over or under.
directional : ModifierKind
A directional preposition, such as up to or from.
adverbial : ModifierKind
An adverb of minimality or maximality, such as minimally or maximally.

Instances For

@[instance_reducible]

instance Numerals.instReprModifierKind :

Repr ModifierKind

Equations

Numerals.instReprModifierKind = { reprPrec := Numerals.instReprModifierKind.repr }

def Numerals.instReprModifierKind.repr :

ModifierKind → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance Numerals.instDecidableEqModifierKind :

DecidableEq ModifierKind

Equations

Numerals.instDecidableEqModifierKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Numerals.ModifierKind.modifierClass :

ModifierKind → ModifierClass

The class of each kind. The comparatives are [Nou10]'s model of Class A and the superlatives and the adverbs of Class B, and the prepositional modifiers follow their spatial use, a locative preposition giving a Class A modifier and a directional one a Class B modifier.

Equations

Instances For

structure Numerals.NumeralModifier :

A numeral modifier, an expression that combines with a numeral to bound, fix or approximate the amount it names.

form : String
The surface form.
kind : Option ModifierKind
The construction the modifier is built on, none for the exactifiers and approximators, which [Nou10]'s survey does not cover.
readings : Set (Modifier (Set ℕ))
The readings the literature makes available, each a modifier of sets of amounts that sends the bare numeral's two-sided meaning {n} to the amounts verifying the modified numeral.

Instances For

@[instance_reducible]

instance Numerals.NumeralModifier.instDenotesSetModifierNat :

Semantics.Denotes NumeralModifier (Set (Modifier (Set ℕ)))

A numeral modifier denotes its readings.

Equations

Numerals.NumeralModifier.instDenotesSetModifierNat = { denote := Numerals.NumeralModifier.readings }

@[simp]

theorem Numerals.NumeralModifier.denote_eq_readings (w : NumeralModifier) :

Semantics.Denotes.denote w = w.readings

def Numerals.NumeralModifier.modifierClass (w : NumeralModifier) :

Option ModifierClass

The class of a bound-setting modifier, read off its kind.

Equations

w.modifierClass = Option.map (fun (x : Numerals.ModifierKind) => x.modifierClass) w.kind

Instances For

def Numerals.NumeralModifier.ofComparison (form : String) (kind : Option ModifierKind) (c : Degree.Comparison) :

NumeralModifier

The numeral modifier with the one reading of a comparison, as a bound-setting modifier or an exactifier has.

Equations

Numerals.NumeralModifier.ofComparison form kind c = { form := form, kind := kind, readings := {c.modifier} }

Instances For

@[simp]

theorem Numerals.NumeralModifier.kind_ofComparison {form : String} {kind : Option ModifierKind} {c : Degree.Comparison} :

(ofComparison form kind c).kind = kind

@[simp]

theorem Numerals.NumeralModifier.readings_ofComparison {form : String} {kind : Option ModifierKind} {c : Degree.Comparison} :

(ofComparison form kind c).readings = {c.modifier}

Exhaustification #

On the account of [CFS12] that [Spe13a] discusses, the bare numeral has the lower-bounded meaning and its two-sided reading comes from a covert exhaustivity operator, which asserts at least m and denies at least m + 1. [Ken15] runs the derivation the other way, lowering the two-sided meaning to the lower-bounded one.

def Numerals.exhNumeral (m : ℕ) :

Set ℕ

The lower-bounded meaning of m exhaustified against the next numeral.

Equations

Numerals.exhNumeral m = Degree.Comparison.ge.interval m \ Degree.Comparison.ge.interval (m + 1)

Instances For

theorem Numerals.exhNumeral_eq (m : ℕ) :

exhNumeral m = Degree.Comparison.eq.interval m

The exhaustified lower-bounded meaning is the two-sided meaning.

@[instance_reducible]

instance Numerals.instDecidablePredNatMemSetExhNumeral {m : ℕ} :

DecidablePred fun (x : ℕ) => x ∈ exhNumeral m

Equations

Numerals.instDecidablePredNatMemSetExhNumeral n = decidable_of_iff (n = m) ⋯

theorem Numerals.mem_exhNumeral_iff_exhAgainst {m n : ℕ} :

n ∈ exhNumeral m ↔ Exhaustification.exhAgainst (fun (x1 x2 : ℕ) => x1 < x2) (fun (k : ℕ) => n ∈ Degree.Comparison.ge.interval (m + k)) 0

Exhaustifying against the next numeral is exhaustifying against the whole scale of higher numerals, which is an entailment chain (Exhaustification.exhAgainst_lt_iff_succ).