Degree comparison

import Linglib.Semantics.Degree.Comparison · namespace Degree

A Comparison is one of the five ways a measured value can relate to a threshold, =, ≥, >, ≤ and <, kept as data so that numerals, measure phrases and comparatives can share it. It selects an order interval, and the entities a measure μ sends into that interval form the preimage μ ⁻¹' c.interval n. A comparison is strict when its threshold lies outside the interval, and as a modifier of degree sets it is extensive exactly when not strict. Reversing the scale exchanges its two sides, and an order embedding preserves it when the threshold moves along. Maximality on a scale is the greatest or least member of a set, the two exchanged by reversing the scale.

Implementation notes

Strictness belongs to the comparison and not to its interval: over the integers fewer than 11 and at most 10 select the same numbers. maxOnScale returns a member of its set, so on a dense scale an open interval has no maximum at its open end; mathlib's IsLUB and IsGLB are the versions that do not require membership.

References

Kennedy 2015, A "de-Fregean" semantics (and neo-Gricean pragmatics) for modified and unmodified numerals formalized
Kennedy 2007, Vagueness and Grammar: The Semantics of Relative and Absolute Gradable Adjectives formalized
Nouwen 2010, Two kinds of modified numerals
Geurts & Nouwen 2007, ‘At least’ et al.: The semantics of scalar modifiers
Rett 2015a, Measure Phrase Equatives and Modified Numerals formalized
Rett 2020a, Eliminating EARLIEST formalized
Rett 2026, Semantic Ambivalence and Expletive Negation formalized
Uegaki & Sudo 2019, The hope-wh puzzle formalized

Declarations

A comparison is the ordering relation a degree modifier draws between a measured value and a threshold. The bare and modified numerals of Kennedy 2015 differ only in this relation (73), as the comparative and equative of Rett 2015a (33) do.

inductive Comparison L45–59

Type

eq : Comparison
The relation μ x = n of a bare numeral (73a).
ge : Comparison
The relation μ x ≥ n of at least n (42a).
gt : Comparison
The relation μ x > n of more than n (41a).
le : Comparison
The relation μ x ≤ n of at most n (42b).
lt : Comparison
The relation μ x < n of fewer than n (41b).

Derives DecidableEq, Repr, Inhabited.

Instances Degree.instMulActionPolarityComparison

Used by Comparison.IsStrict, Comparison.Rel, Comparison.interval, Comparison.mem_interval, Comparison.decidableRel, Comparison.decidableMemInterval, Comparison.self_mem_interval_iff, Comparison.modifier, Comparison.modifier_singleton, Comparison.isExtensive_modifier_iff, Comparison.disjoint_modifier_singleton_iff, Comparison.ordConnected_interval, Comparison.dual, Comparison.dual_dual, Comparison.rel_dual, Comparison.interval_dual, Comparison.rel_map_iff, Comparison.preimage_interval, Comparison.interval_injective, Comparison.preimage_interval_eq_iff, Comparison.forall_preimage_interval_eq_iff, maxOnScale, mem_maxOnScale_dual

Used in Semantics/Degree/Antonymy, Semantics/Degree/Quantifier, Semantics/Quantification/Numerals/Basic, AloniVanOrmondt2023, BumfordRett2021 and 8 more

L65–71

L73–75

L81–84

The order interval a comparison selects is {n}, [n, ∞), (n, ∞), (-∞, n] or (-∞, n).

def Comparison.interval L86–87

{α : Type u_1} [Preorder α] (c : Comparison) (n : α) :

Set α

c.interval n = {a : α | c.Rel a n}

Built from ,

Used by Comparison.interval_eq, Comparison.interval_ge, Comparison.interval_gt, Comparison.interval_le, Comparison.interval_lt, Comparison.mem_interval, Comparison.decidableMemInterval, Comparison.self_mem_interval_iff, Comparison.modifier, Comparison.modifier_singleton, Comparison.ordConnected_interval, Comparison.interval_dual, Comparison.preimage_interval, Comparison.interval_injective, Comparison.preimage_interval_eq_iff, Comparison.forall_preimage_interval_eq_iff

Used in Semantics/Quantification/Numerals/Basic, AloniVanOrmondt2023, BeltramaSoltBurnett2023, BylininaNouwen2020, CohenKrifka2014 and 13 more

A comparison keeps its threshold exactly when it is not strict, the inclusive and exclusive orderings of Kennedy 2015 (4).

@[simp] theorem Comparison.self_mem_interval_iff L118–121

{α : Type u_1} [Preorder α] (c : Comparison) (n : α) :

n ∈ c.interval n ↔ ¬c.IsStrict

Built from , ,

Comparisons as modifiers

A comparison is a modifier of degree sets acting pointwise through its interval, so the modified numeral is the modifier applied to the bare numeral's two-sided meaning: at least is the upward closure, at most the downward closure and exactly the identity. The two halves of Kennedy 2015 (4) are then properties of the modifier, extensive when the comparison is inclusive and disjoint from each singleton when it is strict.

theorem Comparison.isExtensive_modifier_iff L146–150

{α : Type u_1} [Preorder α] [Nonempty α] (c : Comparison) :

c.modifier.IsExtensive ↔ ¬c.IsStrict

Built from , ,

L152–156

L160–164

The antonymous comparison

Polar antonyms measure the same degrees under inverse orderings, an observation Kennedy 2007 traces to Sapir. Its note 29 leaves open whether degrees are points, as they are here, or intervals.

The dual comparison exchanges its arguments, so a is taller than b exactly when b is shorter than a, Kennedy 2007 (60).

theorem Comparison.rel_dual L195–198

{α : Type u_1} [Preorder α] (c : Comparison) (a b : α) :

c.dual.Rel a b ↔ c.Rel b a

Built from , ,

L200–203

Change of scale

L213–215

An order embedding of the scale pulls the interval at f n back to the interval at n, so a comparison is invariant when its threshold moves along with the measure.

theorem Comparison.preimage_interval L217–221

{α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (f : α ↪o β) (c : Comparison) (n : α) :

⇑f ⁻¹' c.interval (f n) = c.interval n

Built from ,

L229–232

L234–239

L241–246

Threshold significance

Uegaki & Sudo 2019 take a gradable expression whose interpretation depends on a threshold to presuppose that some member of the comparison class exceeds it, since a threshold above the whole class draws no distinction in the class.

L264–267

L269–271

Scale-sensitive maximality

What counts as maximal depends on the ordering of the scale, so the same operator picks the latest time of a clause under after and the earliest under before.

L284–288

Maximality on the dual comparison is maximality on the reversed scale, "the same relation involved in each, just applied to reverse scales" (Rett 2026 n. 13).

theorem mem_maxOnScale_dual L290–294

{α : Type u_2} [Preorder α] {X : Set α} {x : α} (c : Comparison) :

x ∈ maxOnScale c.dual X ↔ OrderDual.toDual x ∈ maxOnScale c (⇑OrderDual.ofDual ⁻¹' X)

Built from , ,

theorem mem_maxOnScale_gt L302–304

{α : Type u_2} [PartialOrder α] {X : Set α} {x : α} :

x ∈ maxOnScale Comparison.gt X ↔ IsGreatest X x

Built from

theorem mem_maxOnScale_lt L306–307

{α : Type u_2} [PartialOrder α] {X : Set α} {x : α} :

x ∈ maxOnScale Comparison.lt X ↔ IsLeast X x

Built from