Scale boundedness

import Linglib.Semantics.Degree.Boundedness · namespace Degree

This file defines Degree.Boundedness, the classification of scales by the endpoints they have, for which Kennedy and McNally and, independently, Rotstein and Winter gave evidence from degree modifiers. A boundedness is the endpoint profile of an order, and Boundedness.ofOrder D reads it off D from the existence of a least and a greatest element, so that a scale's tag is a fact about its degrees. The tag is what a lexical entry stores, since a record field cannot hold an OrderTop instance.

The negative member of an antonym pair measures on the same degrees in the reverse order, and Boundedness.dual is that operation on tags. The file also defines the standards of the positive form and Kennedy's Interpretive Economy, which selects among them by the tag. A standard is an upper set of degrees, and the positive form of a measure at it is the preimage of the standard. Kennedy's standards are the degrees above the least, those from the greatest and those above a contextual threshold. Interpretive Economy uses a standard the scale itself fixes when there is one. Where an automorphism carries any degree between the endpoints to any other, the standards every automorphism fixes are the trivial ones and the endpoint ones, so a scale with an endpoint rules out the contextual standard. A difference function, which measures on the ray above a degree, always has the minimum standard, and at it the positive form is a comparative.

Main definitions

Boundedness: the four endpoint profiles, with the predicates HasMin and HasMax.
Boundedness.ofOrder: the boundedness of an order.
Boundedness.dual, Boundedness.withMin, Boundedness.withMax: the ends exchanged, and a least or greatest degree adjoined.
Boundedness.DegreeShape: the canonical linear order of each boundedness.
Degree.IsInvariant: a standard every automorphism of the degrees maps to itself.
PositiveStandard, PositiveStandard.standards: the kinds of standard of the positive form, and the standards of each kind on a scale.
Boundedness.Admits, Boundedness.defaultStandard: the standards Interpretive Economy admits on a scale, and the one it prefers.
EndpointModifier, Boundedness.Licenses: maximizers and minimizers, licensed by an endpoint.

Main statements

Boundedness.ofOrder_degreeShape: every boundedness is that of a linear order.
Degree.isInvariant_iff_of_exists_orderIso: where an automorphism carries any degree between the endpoints to any other, the invariant standards are the trivial and the endpoint ones.
Boundedness.admits_contextual: the contextual standard is admitted exactly on an open scale.
PositiveStandard.requiresComparisonClass_iff, PositiveStandard.complementary_iff: the scale fixes exactly the endpoint standards, and only the minimum and the maximum are complementary.
preimage_projIci_comp_Ioi_bot: a comparative is the positive form of a difference function at the minimum standard.

Implementation notes

Kennedy states Interpretive Economy as maximizing the contribution of conventional meaning ((66)). Reading the standards a scale contributes as those fixed by every automorphism of its degrees is this library's. It makes the admissibility of each standard a theorem about the canonical scale of each tag, the integers with the endpoints adjoined, on which a shift carries any degree between the endpoints to any other. The preference for the maximum on a totally closed scale is Kennedy's and stays a stipulation (defaultStandard).

References

Declarations

Which endpoints a scale has (Kennedy & McNally 2005 (23), Kennedy 2007 (59)). Open scales may further approach a value without reaching it or be unbounded (Kennedy 2007 fn. 28); the tag does not record that.

inductive Boundedness L92–100

Type

open_ : Boundedness
lowerClosed : Boundedness
upperClosed : Boundedness
closed : Boundedness

Derives DecidableEq, Repr, Fintype.

Instances Degree.instMulActionPolarityBoundedness

Used by Boundedness.HasMin, Boundedness.HasMax, Boundedness.ext_iff, Boundedness.ext, Boundedness.eq_upperClosed_iff, Boundedness.ofOrder, Boundedness.dual, Boundedness.hasMin_dual, Boundedness.hasMax_dual, Boundedness.dual_dual, Boundedness.withMin, Boundedness.withMax, Boundedness.hasMin_withMin, Boundedness.hasMax_withMin, Boundedness.hasMax_withMax, Boundedness.hasMin_withMax, Boundedness.dual_withMin, Boundedness.dual_withMax, Boundedness.DegreeShape, Boundedness.instLinearOrderDegreeShape, Boundedness.ofOrder_degreeShape, Boundedness.exists_isBot_degreeShape, Boundedness.exists_isTop_degreeShape, Boundedness.exists_not_isBot_not_isTop, Boundedness.exists_orderIso_degreeShape, Boundedness.isInvariant_degreeShape_iff, Boundedness.Admits, Boundedness.admits_contextual, Boundedness.admits_minEndpoint, Boundedness.admits_maxEndpoint, Boundedness.not_admits_necessity, Boundedness.not_admits_extreme, Boundedness.instDecidableAdmits, Boundedness.not_admits_contextual_of_ne_open, Boundedness.defaultStandard, Boundedness.admits_defaultStandard, Boundedness.defaultStandard_eq_maxEndpoint_iff, Boundedness.complementary_defaultStandard_dual_iff, Boundedness.IsRelative, Boundedness.admits_withMin_iff, Boundedness.defaultStandard_withMin, Boundedness.Licenses, instDecidablePredEndpointModifierLicenses, Boundedness.licenses_maximizer, Boundedness.licenses_minimizer

Used in Semantics/Degree/Adjective, Semantics/Degree/Antonymy, Semantics/Degree/Gradability, Semantics/Degree/Scale, Syntax/Category/Verb/Defs and 5 more

Endpoints

The scale has a minimum.

def Boundedness.HasMin L106–109

Boundedness → Prop

Boundedness.lowerClosed.HasMin = True
Boundedness.closed.HasMin = True
Boundedness.open_.HasMin = False
Boundedness.upperClosed.HasMin = False

Built from

Used by Boundedness.instDecidablePredHasMin, Boundedness.ext_iff, Boundedness.ext, Boundedness.eq_upperClosed_iff, Boundedness.hasMin_ofOrder, Boundedness.hasMin_ofOrder_of_orderBot, Boundedness.not_hasMin_ofOrder, Boundedness.hasMin_dual, Boundedness.hasMax_dual, Boundedness.hasMin_withMin, Boundedness.hasMin_withMax, Boundedness.exists_isBot_degreeShape, Boundedness.admits_minEndpoint, Boundedness.instDecidableAdmits, Boundedness.Licenses, Boundedness.licenses_minimizer

The scale has a maximum.

def Boundedness.HasMax L111–114

Boundedness → Prop

Boundedness.upperClosed.HasMax = True
Boundedness.closed.HasMax = True
Boundedness.open_.HasMax = False
Boundedness.lowerClosed.HasMax = False

Built from

Used by Boundedness.instDecidablePredHasMax, Boundedness.ext_iff, Boundedness.ext, Boundedness.eq_upperClosed_iff, Boundedness.hasMax_ofOrder, Boundedness.hasMax_ofOrder_of_orderTop, Boundedness.not_hasMax_ofOrder, Boundedness.hasMin_dual, Boundedness.hasMax_dual, Boundedness.hasMax_withMin, Boundedness.hasMax_withMax, Boundedness.exists_isTop_degreeShape, Boundedness.admits_maxEndpoint, Boundedness.instDecidableAdmits, Boundedness.defaultStandard_eq_maxEndpoint_iff, Boundedness.admits_withMin_iff, Boundedness.defaultStandard_withMin, Boundedness.Licenses, Boundedness.licenses_maximizer

Used in Semantics/Degree/Scale, HayKennedyLevin1999, KennedyLevin2008, Morzycki2009, SauerlandStateva2011

The boundedness of an order

The boundedness of an order records which of a least and a greatest element it has.

Boundedness.ofOrder L137–140

noncomputable def Degree.Boundedness.ofOrder (D : Type u_2) [LE D] :

Boundedness

The definition is too large to print here; read it in the source.

Built from

Used by Boundedness.hasMin_ofOrder, Boundedness.hasMax_ofOrder, Boundedness.hasMin_ofOrder_of_orderBot, Boundedness.hasMax_ofOrder_of_orderTop, Boundedness.not_hasMin_ofOrder, Boundedness.not_hasMax_ofOrder, Boundedness.ofOrder_orderDual, Boundedness.ofOrder_Ici, Boundedness.ofOrder_Iic, Boundedness.ofOrder_Icc, Boundedness.ofOrder_Ioo, Boundedness.ofOrder_Ioc, Boundedness.ofOrder_degreeShape

Used in Grano2026, KennedyLevin2008, Koev2026, Lassiter2017, Morzycki2009 and 1 more

The ends exchanged

The dual of a boundedness exchanges its ends, giving the scale of the antonym (Kennedy 2007 (60)).

def Boundedness.dual L173–179

Boundedness → Boundedness

Boundedness.open_.dual = Boundedness.open_
Boundedness.lowerClosed.dual = Boundedness.upperClosed
Boundedness.upperClosed.dual = Boundedness.lowerClosed
Boundedness.closed.dual = Boundedness.closed

Built from

Used by Boundedness.hasMin_dual, Boundedness.hasMax_dual, Boundedness.dual_involutive, Boundedness.dual_dual, Boundedness.ofOrder_orderDual, Boundedness.dual_withMin, Boundedness.dual_withMax, Boundedness.complementary_defaultStandard_dual_iff

Used in Semantics/Degree/Antonymy, Koev2026

An endpoint adjoined

b.withMin is b with a least degree adjoined, the shape of a ray Set.Ici a.

def Boundedness.withMin L199–202

Boundedness → Boundedness

Boundedness.open_.withMin = Boundedness.lowerClosed
Boundedness.lowerClosed.withMin = Boundedness.lowerClosed
Boundedness.upperClosed.withMin = Boundedness.closed
Boundedness.closed.withMin = Boundedness.closed

Built from

Used by Boundedness.hasMin_withMin, Boundedness.hasMax_withMin, Boundedness.dual_withMin, Boundedness.dual_withMax, Boundedness.ofOrder_Ici, Boundedness.admits_withMin_iff, Boundedness.defaultStandard_withMin

Used in Semantics/Degree/Scale

b.withMax is b with a greatest degree adjoined, the shape of a ray Set.Iic a.

def Boundedness.withMax L204–207

Boundedness → Boundedness

Boundedness.open_.withMax = Boundedness.upperClosed
Boundedness.upperClosed.withMax = Boundedness.upperClosed
Boundedness.lowerClosed.withMax = Boundedness.closed
Boundedness.closed.withMax = Boundedness.closed

Built from

Used by Boundedness.hasMax_withMax, Boundedness.hasMin_withMax, Boundedness.dual_withMin, Boundedness.dual_withMax, Boundedness.ofOrder_Iic

A linear order of each shape

b.DegreeShape is the integers with the endpoints of b adjoined, a linear order of each boundedness.

@[reducible, inline] abbrev Boundedness.DegreeShape L262–268

Boundedness → Type

Boundedness.open_.DegreeShape = ℤ
Boundedness.lowerClosed.DegreeShape = WithBot ℤ
Boundedness.upperClosed.DegreeShape = WithTop ℤ
Boundedness.closed.DegreeShape = WithTop (WithBot ℤ)

Built from

Used by Boundedness.instLinearOrderDegreeShape, Boundedness.ofOrder_degreeShape, Boundedness.exists_isBot_degreeShape, Boundedness.exists_isTop_degreeShape, Boundedness.exists_not_isBot_not_isTop, Boundedness.exists_orderIso_degreeShape, Boundedness.isInvariant_degreeShape_iff, Boundedness.Admits

Used in Semantics/Degree/Scale

L270–271

Every boundedness is that of a linear order, since DegreeShape is a section of ofOrder.

@[simp] theorem Boundedness.ofOrder_degreeShape L273–282

(b : Boundedness) :

ofOrder b.DegreeShape = b

Built from , ,

Invariant standards

A standard of a scale is an upper set of its degrees, and the positive form at it holds of what the measure places in it, so that a stronger standard, a smaller upper set, entails a weaker one. A standard is invariant when the order alone singles it out, every automorphism of the degrees mapping it to itself. All degrees and none are invariant, as are the degrees above a least one and those from a greatest one, and where any degree between the endpoints is carried to any other by an automorphism, as on the canonical scales, these are all.

A standard is invariant when every order automorphism of the degrees maps it to itself.

def IsInvariant L344–345

{D : Type u_1} [Preorder D] (U : UpperSet D) :

Prop

IsInvariant U = ∀ (f : D ≃o D), (UpperSet.map f) U = U

Used by isInvariant_bot, isInvariant_top, isInvariant_Ioi_of_isBot, isInvariant_Ici_of_isTop, IsInvariant.apply_mem, isInvariant_iff_of_exists_orderIso, forall_isInvariant_iff_of_exists_orderIso, Boundedness.isInvariant_degreeShape_iff, PositiveStandard.RequiresComparisonClass, Boundedness.Admits

Where an automorphism carries any degree strictly between the endpoints to any other, the invariant standards are the trivial ones and the endpoint ones.

theorem isInvariant_iff_of_exists_orderIso L369–411

{D : Type u_1} [LinearOrder D] {U : UpperSet D} (hI : ∃ (x : D), ¬IsBot x ∧ ¬IsTop x) (h : ∀ (x y : D), ¬IsBot x → ¬IsTop x → ¬IsBot y → ¬IsTop y → ∃ (f : D ≃o D), f x = y) :

IsInvariant U ↔ U = ⊥ ∨ U = ⊤ ∨ (∃ (m : D), IsBot m ∧ U = UpperSet.Ioi m) ∨ ∃ (m : D), IsTop m ∧ U = UpperSet.Ici m

Built from

L413–428

L432–435

Standards and Interpretive Economy

The positive form of a gradable predicate at a standard U is the preimage μ ⁻¹' U of the standard under its measure, true of what the measure places in the standard. Kennedy's standards are the degrees above the least, Set.Ioi ⊥, as for wet and bent; those from the greatest, Set.Ici ⊤, as for dry and full; and those above a contextual threshold θ, Set.Ioi θ, as for tall. When the least degree is below the greatest, the maximum standard is stronger than the minimum (UpperSet.Ioi_le_Ici), and the minimum standard is the weakest nontrivial one, covering the standard every degree meets (UpperSet.Ici_covBy_Ioi). Interpretive Economy maximizes the contribution of conventional meaning, so a scale with an endpoint rules out the contextual standard, and a totally closed scale admits both endpoint standards and prefers the maximum.

A positive standard is the kind of threshold the positive form compares a degree with, a contextual norm on an open scale and an endpoint on a closed one (Kennedy 2007), or a standard an adjective fixes lexically outside that choice.

inductive PositiveStandard L450–465

Type

contextual : PositiveStandard
The norm of a comparison class, as for tall.
minEndpoint : PositiveStandard
The minimum of the scale, as for bent and wet.
maxEndpoint : PositiveStandard
The maximum of the scale, as for full and dry.
necessity : PositiveStandard
The minimum degree for pursuit (Beltrama 2025).
extreme : PositiveStandard
A standard beyond that of the weak adjective on the same pole, as for gigantic and pristine (Morzycki 2012).

Derives DecidableEq, Repr.

Used by PositiveStandard.standards, PositiveStandard.RequiresComparisonClass, PositiveStandard.requiresComparisonClass_iff, PositiveStandard.Complementary, PositiveStandard.complementary_iff, Boundedness.Admits, Boundedness.instDecidableAdmits, Boundedness.defaultStandard, Boundedness.admits_withMin_iff

Used in Fragments/Adyghe/Clause, Fragments/Dutch/Verbs, Fragments/English/Verbs/Basic, Fragments/Finnish/Verbs, Fragments/German/Verbs and 19 more

The standards of a kind on a scale. A minimum standard is the set of degrees above a least degree and a maximum standard the set from a greatest one; a contextual, necessity or extreme standard is a threshold, the degrees above or from some degree, which the context or the lexicon fixes and the scale does not.

def PositiveStandard.standards L467–476

(s : PositiveStandard) (D : Type u_1) [Preorder D] :

Set (UpperSet D)

Equations

PositiveStandard.minEndpoint.standards D = {U : UpperSet D | ∃ (m : D), IsBot m ∧ U = UpperSet.Ioi m}
PositiveStandard.maxEndpoint.standards D = {U : UpperSet D | ∃ (m : D), IsTop m ∧ U = UpperSet.Ici m}
PositiveStandard.contextual.standards D = {U : UpperSet D | ∃ (θ : D), U = UpperSet.Ioi θ ∨ U = UpperSet.Ici θ}
PositiveStandard.necessity.standards D = {U : UpperSet D | ∃ (θ : D), U = UpperSet.Ioi θ ∨ U = UpperSet.Ici θ}
PositiveStandard.extreme.standards D = {U : UpperSet D | ∃ (θ : D), U = UpperSet.Ioi θ ∨ U = UpperSet.Ici θ}

Built from

Used by PositiveStandard.RequiresComparisonClass, PositiveStandard.Complementary, Boundedness.Admits

Used in Semantics/Modality/Basic

L480–487

The scale fixes exactly the endpoint standards.

theorem PositiveStandard.requiresComparisonClass_iff L489–506

{s : PositiveStandard} :

s.RequiresComparisonClass ↔ s ≠ minEndpoint ∧ s ≠ maxEndpoint

Built from ,

L508–509

L511–517

Only the minimum and the maximum standards are complementary: any other pair leaves a gap or an overlap on some scale.

theorem PositiveStandard.complementary_iff L519–561

{s t : PositiveStandard} :

s.Complementary t ↔ s = minEndpoint ∧ t = maxEndpoint ∨ s = maxEndpoint ∧ t = minEndpoint

Built from ,

L563

Difference functions

The difference function of a measure μ at a degree d is Set.projIci d ∘ μ, which measures on the ray above d and sends every degree at or below d to d, the derived zero. The ray has a least degree (Boundedness.ofOrder_Ici), so Interpretive Economy admits the minimum standard for a difference function, giving the truth conditions of a comparative with standard d, and the maximum standard exactly when the scale of μ has one.

The positive form of a difference function at the minimum standard is the comparative with standard d (Kennedy & McNally 2005, Kennedy & Levin 2008 (24)).

theorem preimage_projIci_comp_Ioi_bot L578–582

{α : Type u_1} {D : Type u_2} [LinearOrder D] {μ : α → D} {d : D} :

Set.projIci d ∘ μ ⁻¹' Set.Ioi ⊥ = μ ⁻¹' Set.Ioi d

L584–590

Interpretive Economy computes truth conditions from conventional meaning where it can, allowing a contextual standard only where conventional meaning is insufficient (Kennedy 2007 (66)). The standards a scale itself fixes are those every automorphism of its degrees fixes, and the endpoint standards are among them (isInvariant_Ioi_of_isBot), so a scale admits an endpoint standard where it has a standard of that kind, and the contextual standard only where it fixes no standard but the trivial ones. The lexical necessity and extreme standards it never admits. On the canonical scales the endpoint standards are the only nontrivial invariant ones (isInvariant_degreeShape_iff).

def Boundedness.Admits L596–609

(b : Boundedness) :

PositiveStandard → Prop

b.Admits PositiveStandard.contextual = ∀ (U : UpperSet b.DegreeShape), IsInvariant U → U = ⊥ ∨ U = ⊤
b.Admits PositiveStandard.minEndpoint = (PositiveStandard.minEndpoint.standards b.DegreeShape).Nonempty
b.Admits PositiveStandard.maxEndpoint = (PositiveStandard.maxEndpoint.standards b.DegreeShape).Nonempty
b.Admits PositiveStandard.necessity = False
b.Admits PositiveStandard.extreme = False

Built from , , , ,

Used by Boundedness.admits_contextual, Boundedness.admits_minEndpoint, Boundedness.admits_maxEndpoint, Boundedness.not_admits_necessity, Boundedness.not_admits_extreme, Boundedness.instDecidableAdmits, Boundedness.not_admits_contextual_of_ne_open, Boundedness.admits_defaultStandard, Boundedness.admits_withMin_iff

Used in Semantics/Degree/Adjective, Semantics/Degree/Gradability, Grano2026, Kennedy2007, KennedyLevin2008 and 2 more

The contextual standard is admitted exactly on a totally open scale, since a scale with an endpoint fixes the endpoint standard (Kennedy 2007 (66)).

@[simp] theorem Boundedness.admits_contextual L611–617

{b : Boundedness} :

b.Admits PositiveStandard.contextual ↔ b = open_

Built from ,

The default standard of a scale is the one Interpretive Economy forces where it admits only one, and the maximum on a totally closed scale, since a maximum standard entails a minimum one.

def Boundedness.defaultStandard L642–648

Boundedness → PositiveStandard

Boundedness.open_.defaultStandard = PositiveStandard.contextual
Boundedness.lowerClosed.defaultStandard = PositiveStandard.minEndpoint
Boundedness.upperClosed.defaultStandard = PositiveStandard.maxEndpoint
Boundedness.closed.defaultStandard = PositiveStandard.maxEndpoint

Built from ,

Used by Boundedness.admits_defaultStandard, Boundedness.defaultStandard_eq_maxEndpoint_iff, Boundedness.complementary_defaultStandard_dual_iff, Boundedness.IsRelative, Boundedness.defaultStandard_withMin

Used in Semantics/Degree/Gradability, Semantics/Degree/Scale, KennedyLevin2008, Koev2026

Endpoint modifiers

An endpoint modifier is a degree modifier that refers to an endpoint of the scale, a maximizer such as completely or fully, or a minimizer such as slightly or partially (Kennedy & McNally 2005, Kennedy 2007 (61)).

inductive EndpointModifier L687–693

Type

maximizer : EndpointModifier
minimizer : EndpointModifier

Derives DecidableEq, Repr.

Used by Boundedness.Licenses

Used in Kennedy2007, Koev2026, Lassiter2017

A scale licenses an endpoint modifier when it has the endpoint the modifier picks out.

def Boundedness.Licenses L695–698

(b : Boundedness) :

EndpointModifier → Prop

b.Licenses EndpointModifier.maximizer = b.HasMax
b.Licenses EndpointModifier.minimizer = b.HasMin

Built from , , ,

Used by instDecidablePredEndpointModifierLicenses, Boundedness.licenses_maximizer, Boundedness.licenses_minimizer

Used in Kennedy2007, Lassiter2017

L700–702

L704–705

L707–708