Gradable adjectives

Adjective-specific degree semantics, layered on the syntactic Adjective (Syntax/Category/Adjective): the GradableAdjective lexeme with its derived Kennedy classification, the two-threshold model for contrary antonyms, and multidimensional binding ([sassoon-2013]).

Main definitions

• GradableAdjective — a syntactic Adjective refined with the degree-semantic layer; scaleType, standard, and adjectiveClass are derived views.
• ThresholdPair — the two thresholds of a contrary antonym pair, with a gap.
• InformationalStrength — the weak/strong distinction ([AG24a]).
• DimensionBindingType — how a multidimensional adjective binds its dimensions.

The finite degree carrier Bounded, its Threshold, and the threshold semantics (positiveMeaning, negativeMeaning) live in Semantics/Degree/Discrete. The intersective/subsective/privative classification lives in Semantics/Modification/Classification.lean.

Standards and Interpretive Economy ([kennedy-2007])

Absorbed from the retired Standard.lean: the classification of gradable adjectives by scale structure and the derivation of standard type from boundedness. Interpretive Economy ([kennedy-2007] eq. (66)) maximises the contribution of conventional meaning: a scale with an endpoint rules out the contextual standard; a totally closed scale admits both endpoint standards (Boundedness.Admits) with the maximum as the pragmatically preferred default (Boundedness.defaultStandard).

Classification carriers

inductive Degree.PositiveStandard : Type

Positive form standard: how the contextual threshold is determined. For open scales, the standard is the contextual norm ([kennedy-2007]); for closed scales, it is the relevant endpoint fixed by Interpretive Economy.

• contextual : PositiveStandard

  Open-scale: θ = norm relative to comparison class.

• minEndpoint : PositiveStandard

  Lower-bounded: θ = minimum (e.g., "bent", "wet").

• maxEndpoint : PositiveStandard

  Upper-bounded / closed: θ = maximum (e.g., "full", "dry").

• functional : PositiveStandard

  Necessity standard: θ = minimum value for pursuit ([Bel25]).

@[instance_reducible]

instance Degree.instDecidableEqPositiveStandard : DecidableEq PositiveStandard

Equations

• Degree.instDecidableEqPositiveStandard x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Degree.instReprPositiveStandard : Repr PositiveStandard

Equations

• Degree.instReprPositiveStandard = { reprPrec := Degree.instReprPositiveStandard.repr }

def Degree.instReprPositiveStandard.repr : PositiveStandard → ℕ → Std.Format

Equations

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

def Degree.PositiveStandard.RequiresComparisonClass : PositiveStandard → Prop

Whether the positive standard depends on contextual domain information.

[kennedy-2007] argues the comparison class is not a semantic argument of pos (contra [klein-1980]), replacing it with the standard-fixing function s: ⟦pos⟧ = λg.λx. g(x) ≥ s(g). For relative (open-scale) adjectives, s still requires contextual domain information; for absolute (closed-scale) adjectives the standard comes from scale endpoints via Interpretive Economy.

Equations

• Degree.PositiveStandard.contextual.RequiresComparisonClass = True
• Degree.PositiveStandard.minEndpoint.RequiresComparisonClass = False
• Degree.PositiveStandard.maxEndpoint.RequiresComparisonClass = False
• Degree.PositiveStandard.functional.RequiresComparisonClass = True

@[instance_reducible]

instance Degree.instDecidablePredPositiveStandardRequiresComparisonClass : DecidablePred PositiveStandard.RequiresComparisonClass

Equations

• Degree.instDecidablePredPositiveStandardRequiresComparisonClass Degree.PositiveStandard.contextual = isTrue Degree.instDecidablePredPositiveStandardRequiresComparisonClass._proof_1
• Degree.instDecidablePredPositiveStandardRequiresComparisonClass Degree.PositiveStandard.minEndpoint = isFalse Degree.instDecidablePredPositiveStandardRequiresComparisonClass._proof_2
• Degree.instDecidablePredPositiveStandardRequiresComparisonClass Degree.PositiveStandard.maxEndpoint = isFalse Degree.instDecidablePredPositiveStandardRequiresComparisonClass._proof_3
• Degree.instDecidablePredPositiveStandardRequiresComparisonClass Degree.PositiveStandard.functional = isTrue Degree.instDecidablePredPositiveStandardRequiresComparisonClass._proof_4

inductive Degree.AdjectiveClass : Type

Kennedy's adjective classification by scale structure and standard type [kennedy-2007] [kennedy-mcnally-2005], plus a nonGradable case for adjectives outside the degree-based fragment.

• relativeGradable : AdjectiveClass

  Standard varies with comparison class — tall, expensive, big.

• absoluteMaximum : AdjectiveClass

  Threshold fixed at scale maximum — full, straight, closed, dry.

• absoluteMinimum : AdjectiveClass

  Threshold fixed at scale minimum — wet, bent, open, dirty.

• mildlyPositive : AdjectiveClass

  Necessity-relative threshold — decent, acceptable ([Bel25]).

• nonGradable : AdjectiveClass

  Non-gradable: no degree argument, no scale — atomic, prime, deceased, pregnant. Outside the degree-based system; consumers that classify a general adjective should map non-gradables here rather than coercing them into a gradable class.

def Degree.instReprAdjectiveClass.repr : AdjectiveClass → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Degree.instReprAdjectiveClass : Repr AdjectiveClass

Equations

• Degree.instReprAdjectiveClass = { reprPrec := Degree.instReprAdjectiveClass.repr }

@[instance_reducible]

instance Degree.instDecidableEqAdjectiveClass : DecidableEq AdjectiveClass

Equations

• Degree.instDecidableEqAdjectiveClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Degree.AdjectiveClass.IsRelative (c : AdjectiveClass) : Prop

Coarse two-way classification: relative vs absolute. Collapses absoluteMaximum and absoluteMinimum.

Equations

• c.IsRelative = (c = Degree.AdjectiveClass.relativeGradable)

@[instance_reducible]

instance Degree.instDecidablePredAdjectiveClassIsRelative : DecidablePred AdjectiveClass.IsRelative

Equations

• Degree.instDecidablePredAdjectiveClassIsRelative c = decEq c Degree.AdjectiveClass.relativeGradable

def Degree.Boundedness.Admits (b : Boundedness) : PositiveStandard → Prop

The positive-form standards Interpretive Economy admits for a scale ([kennedy-2007] §4.2–§4.3): a maximal degree stands out on a scale with a maximum and a non-minimal degree on one with a minimum, so an endpoint standard is available exactly where the scale has that endpoint; the contextual standard, which context must supply, survives IE (66) only on a totally open scale. A totally closed scale therefore admits both endpoints ((67)–(68)).

Equations

• b.Admits Degree.PositiveStandard.contextual = (b = Degree.Boundedness.open_)
• b.Admits Degree.PositiveStandard.minEndpoint = b.HasMin
• b.Admits Degree.PositiveStandard.maxEndpoint = b.HasMax
• b.Admits Degree.PositiveStandard.functional = False

@[instance_reducible]

instance Degree.instDecidableAdmits (b : Boundedness) (s : PositiveStandard) : Decidable (b.Admits s)

Equations

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

def Degree.Boundedness.defaultStandard : Boundedness → PositiveStandard

The out-of-context default standard, Interpretive Economy plus a strengthening preference: where one standard is admitted it is forced, and a totally closed scale takes the maximum (a maximum standard entails a minimum one).

Equations

• Degree.Boundedness.open_.defaultStandard = Degree.PositiveStandard.contextual
• Degree.Boundedness.lowerBounded.defaultStandard = Degree.PositiveStandard.minEndpoint
• Degree.Boundedness.upperBounded.defaultStandard = Degree.PositiveStandard.maxEndpoint
• Degree.Boundedness.closed.defaultStandard = Degree.PositiveStandard.maxEndpoint

theorem Degree.Boundedness.admits_defaultStandard (b : Boundedness) : b.Admits b.defaultStandard

The default standard is always admitted.

theorem Degree.Boundedness.closed_admits_minEndpoint : closed.Admits PositiveStandard.minEndpoint

A totally closed scale admits the minimum standard as well as the default maximum ([kennedy-2007] (67)–(68)).

theorem Degree.Boundedness.closed_admits_maxEndpoint : closed.Admits PositiveStandard.maxEndpoint

theorem Degree.Boundedness.not_admits_contextual_of_ne_open {b : Boundedness} (h : b ≠ open_) : ¬b.Admits PositiveStandard.contextual

Interpretive Economy rules out the contextual standard whenever the scale has an endpoint.

def Degree.Boundedness.IsRelative (b : Boundedness) : Prop

A scale is relative iff its default standard needs a comparison class, i.e. iff it is open (tall, expensive, big).

Equations

• b.IsRelative = b.defaultStandard.RequiresComparisonClass

@[instance_reducible]

instance Degree.instDecidablePredBoundednessIsRelative : DecidablePred Boundedness.IsRelative

Equations

• Degree.instDecidablePredBoundednessIsRelative b = Degree.instDecidablePredBoundednessIsRelative._aux_1 b

Two-threshold model for contrary antonyms

structure Degree.ThresholdPair (max : ℕ) : Type

The two thresholds of a contrary antonym pair (happy/unhappy): pos for the positive form (true when degree > pos) and neg for the negative form (true when degree < neg). When neg < pos a gap region [neg, pos] — "neither" — lies between them; that strict inequality is taken as a hypothesis where a gap is needed (contrary_gap_exists, gap_nonempty), not stored as an invariant.

• pos : Threshold max
• neg : Threshold max

def Degree.instReprThresholdPair.repr {max✝ : ℕ} : ThresholdPair max✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Degree.instReprThresholdPair {max✝ : ℕ} : Repr (ThresholdPair max✝)

Equations

• Degree.instReprThresholdPair = { reprPrec := Degree.instReprThresholdPair.repr }

@[instance_reducible]

instance Degree.instDecidableEqThresholdPair {max✝ : ℕ} : DecidableEq (ThresholdPair max✝)

Equations

• Degree.instDecidableEqThresholdPair = Degree.instDecidableEqThresholdPair.decEq

def Degree.instDecidableEqThresholdPair.decEq {max✝ : ℕ} (x✝ x✝¹ : ThresholdPair max✝) : Decidable (x✝ = x✝¹)

Equations

• Degree.instDecidableEqThresholdPair.decEq { pos := a, neg := a_1 } { pos := b, neg := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Degree.instBEqThresholdPair.beq {max✝ : ℕ} : ThresholdPair max✝ → ThresholdPair max✝ → Bool

Equations

• Degree.instBEqThresholdPair.beq { pos := a, neg := a_1 } { pos := b, neg := b_1 } = (a == b && a_1 == b_1)
• Degree.instBEqThresholdPair.beq x✝¹ x✝ = false

@[instance_reducible]

instance Degree.instBEqThresholdPair {max✝ : ℕ} : BEq (ThresholdPair max✝)

Equations

• Degree.instBEqThresholdPair = { beq := Degree.instBEqThresholdPair.beq }

Negation semantics

The two-threshold model for contrary antonyms: the general threshold semantics of Semantics/Degree/Basic (positiveMeaning/negativeMeaning/notPositiveMeaning) read through a ThresholdPair's two poles.

@[reducible, inline]

abbrev Degree.contradictoryNeg {max : ℕ} (d : Bounded max) (θ : Threshold max) : Prop

Contradictory negation not happy — d ≤ θ (Degree.notPositiveMeaning).

Equations

• Degree.contradictoryNeg d θ = Degree.notPositiveMeaning d θ

@[reducible, inline]

abbrev Degree.contraryNeg {max : ℕ} (d : Bounded max) (θ_neg : Threshold max) : Prop

Contrary negation unhappy — d < θ_neg (Degree.negativeMeaning).

Equations

• Degree.contraryNeg d θ_neg = Degree.negativeMeaning d θ_neg

@[reducible, inline]

abbrev Degree.inGapRegion {max : ℕ} (d : Bounded max) (tp : ThresholdPair max) : Prop

The gap region: d is neither positive nor negative (neg ≤ d ≤ pos).

Equations

• Degree.inGapRegion d tp = ({ value := tp.neg.value.castSucc } ≤ d ∧ d ≤ { value := tp.pos.value.castSucc })

@[reducible, inline]

abbrev Degree.positiveMeaning' {max : ℕ} (d : Bounded max) (tp : ThresholdPair max) : Prop

Positive form happy at the pair's upper threshold — d > pos.

Equations

• Degree.positiveMeaning' d tp = Degree.positiveMeaning d tp.pos

@[reducible, inline]

abbrev Degree.contraryNegMeaning {max : ℕ} (d : Bounded max) (tp : ThresholdPair max) : Prop

Negative form unhappy at the pair's lower threshold — d < neg.

Equations

• Degree.contraryNegMeaning d tp = Degree.negativeMeaning d tp.neg

@[reducible, inline]

abbrev Degree.notContraryNegMeaning {max : ℕ} (d : Bounded max) (tp : ThresholdPair max) : Prop

not unhappy — the complement of the negative form (neg ≤ d).

Equations

• Degree.notContraryNegMeaning d tp = ({ value := tp.neg.value.castSucc } ≤ d)

Antonym relations

@[reducible, inline]

abbrev Degree.AntonymRelation : Type

The relation between a positive form and its antonym.

Equations

• Degree.AntonymRelation = Features.NegationType

Informational strength

inductive Degree.InformationalStrength : Type

Informational strength of a gradable adjective within its scale.

Weak adjectives (e.g., "large", "clean") occupy a broader region of the scale. Strong adjectives (e.g., "gigantic", "pristine") occupy a narrower, more extreme region.

A strong adjective entails its weak counterpart on the same pole: "x is gigantic" ⟹ "x is large", but not vice versa.

This distinction is orthogonal to scale structure (relative vs absolute) and polarity (positive vs negative).

Source: [AG24a], [Hor72]

• weak : InformationalStrength
• strong : InformationalStrength

@[instance_reducible]

instance Degree.instReprInformationalStrength : Repr InformationalStrength

Equations

• Degree.instReprInformationalStrength = { reprPrec := Degree.instReprInformationalStrength.repr }

def Degree.instReprInformationalStrength.repr : InformationalStrength → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Degree.instDecidableEqInformationalStrength : DecidableEq InformationalStrength

Equations

• Degree.instDecidableEqInformationalStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

The gradable adjective

inductive Degree.SpatialConfigType : Type

Spatial configuration type for adjectives in resultative constructions ([levin-2026]). Only adjectives describing spatially instantiated states license intr-push open resultatives.

• barrierConfig : SpatialConfigType
• unattachment : SpatialConfigType
• surfaceOrient : SpatialConfigType

@[instance_reducible]

instance Degree.instDecidableEqSpatialConfigType : DecidableEq SpatialConfigType

Equations

• Degree.instDecidableEqSpatialConfigType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Degree.instReprSpatialConfigType.repr : SpatialConfigType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Degree.instReprSpatialConfigType : Repr SpatialConfigType

Equations

• Degree.instReprSpatialConfigType = { reprPrec := Degree.instReprSpatialConfigType.repr }

structure Degree.GradableAdjectiveextends Adjective : Type

A gradable adjective: the syntactic Adjective (Syntax/Category/Adjective) refined with the degree-semantic layer that becomes relevant in this module — the Kennedy standardOverride, and the lexical-semantic facets antonymRelation, resultative spatialConfigType ([levin-2026]), and evaluativeValence ([Nou24]). The scale shape (scaleType), positive standard, and Kennedy adjectiveClass are derived views below — the fix for the old stored scaleType that conflated scale shape with pole (wet/dry share one closed .wetness scale, differing only in pole).

• form : String
• script : Option String
• dimension : Option Features.ScalarDimension
• polarity : Option Degree.ScalePolarity
• comparison : ComparisonFacet
• antonymForm : Option String
• standardOverride : Option PositiveStandard

  Override the Kennedy default standard (the good/MPA residual: an open-shape scale that nonetheless takes a functional/contextual standard, [Bel25]). none = take the derived default.

• antonymRelation : Option AntonymRelation

  Lexical antonym's logical relation (contrary vs contradictory).

• spatialConfigType : Option SpatialConfigType

  Resultative spatial-configuration class ([levin-2026]).

• evaluativeValence : Option Features.EvaluativeValence

  Evaluative valence of the adjective, when applicable. Determines intensifier degree class ([Nou24]): negative-evaluative bases yield H-degree intensifiers, positive-evaluative bases yield M-degree intensifiers.

@[instance_reducible]

instance Degree.instReprGradableAdjective : Repr GradableAdjective

Equations

• Degree.instReprGradableAdjective = { reprPrec := Degree.instReprGradableAdjective.repr }

def Degree.instReprGradableAdjective.repr : GradableAdjective → ℕ → Std.Format

Equations

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

def Degree.GradableAdjective.scaleType (g : GradableAdjective) : Boundedness

The scale the adjective measures on: its dimension's, dualized for the negative member of an antonym pair (.open_ for a non-gradable, which has no scale).

Equations

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

def Degree.GradableAdjective.standard (g : GradableAdjective) : PositiveStandard

The positive standard: the scale's default, unless overridden (the good/MPA residual).

Equations

• g.standard = g.standardOverride.getD g.scaleType.defaultStandard

theorem Degree.GradableAdjective.admits_standard (g : GradableAdjective) (h : g.standardOverride = none) : g.scaleType.Admits g.standard

An override-free entry's standard is one its scale admits.

def Degree.GradableAdjective.adjectiveClass (g : GradableAdjective) : AdjectiveClass

Kennedy's adjective class — derived from standard, not stored; .nonGradable exactly when there is no dimension ([kennedy-2007], [kennedy-mcnally-2005]).

Equations

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

def Degree.GradableAdjective.IsRelative (g : GradableAdjective) : Prop

Comparison-class dependence — the relative/absolute distinction, derived.

Equations

• g.IsRelative = g.adjectiveClass.IsRelative

@[instance_reducible]

instance Degree.GradableAdjective.instDecidableIsRelative (g : GradableAdjective) : Decidable g.IsRelative

Equations

• g.instDecidableIsRelative = id inferInstance

Multidimensional adjectives ([sassoon-2013])

inductive Degree.DimensionBindingType : Type

How a multidimensional adjective binds its dimensions ([sassoon-2013]).

• conjunctive: entity must meet standard in ALL dimensions (e.g., healthy)
• disjunctive: entity must meet standard in SOME dimension (e.g., sick)
• mixed: context determines ∀ vs ∃ (e.g., intelligent)

• conjunctive : DimensionBindingType
• disjunctive : DimensionBindingType
• mixed : DimensionBindingType

@[instance_reducible]

instance Degree.instReprDimensionBindingType : Repr DimensionBindingType

Equations

• Degree.instReprDimensionBindingType = { reprPrec := Degree.instReprDimensionBindingType.repr }

def Degree.instReprDimensionBindingType.repr : DimensionBindingType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Degree.instDecidableEqDimensionBindingType : DecidableEq DimensionBindingType

Equations

• Degree.instDecidableEqDimensionBindingType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Degree.conjunctiveBinding {α : Type u_1} (dims : List (α → Bool)) (x : α) : Bool

Conjunctive binding: ∀Q ∈ DIM(P,c). Q(x).

Equations

• Degree.conjunctiveBinding dims x = dims.all fun (x_1 : α → Bool) => x_1 x

def Degree.disjunctiveBinding {α : Type u_1} (dims : List (α → Bool)) (x : α) : Bool

Disjunctive binding: ∃Q ∈ DIM(P,c). Q(x).

Equations

• Degree.disjunctiveBinding dims x = dims.any fun (x_1 : α → Bool) => x_1 x

theorem Degree.deMorgan_conjunctive_disjunctive {α : Type u_1} (dims : List (α → Bool)) (x : α) : (!conjunctiveBinding dims x) = disjunctiveBinding (List.map (fun (d : α → Bool) (a : α) => !d a) dims) x

De Morgan: negating conjunctive binding yields disjunctive binding over negated dimension predicates. This is the formal core of [sassoon-2013]'s Hypothesis 2 — under a negation theory of antonymy, if the positive form is conjunctive, the negative antonym (its negation) is disjunctive.

theorem Degree.deMorgan_disjunctive_conjunctive {α : Type u_1} (dims : List (α → Bool)) (x : α) : (!disjunctiveBinding dims x) = conjunctiveBinding (List.map (fun (d : α → Bool) (a : α) => !d a) dims) x

def Degree.DimensionBindingType.negate : DimensionBindingType → DimensionBindingType

The predicted binding type for a negative antonym, given its positive counterpart's binding type. Follows from De Morgan under the negation theory of antonymy.

Equations

• Degree.DimensionBindingType.conjunctive.negate = Degree.DimensionBindingType.disjunctive
• Degree.DimensionBindingType.disjunctive.negate = Degree.DimensionBindingType.conjunctive
• Degree.DimensionBindingType.mixed.negate = Degree.DimensionBindingType.mixed

theorem Degree.negate_involutive (b : DimensionBindingType) : b.negate.negate = b

def Degree.predictedBinding : PositiveStandard → DimensionBindingType

[sassoon-2013] Hypothesis 3: standard type predicts binding type. Total (max standard) → conjunctive, partial (min standard) → disjunctive, relative (contextual) → mixed.

Equations

• Degree.predictedBinding Degree.PositiveStandard.maxEndpoint = Degree.DimensionBindingType.conjunctive
• Degree.predictedBinding Degree.PositiveStandard.minEndpoint = Degree.DimensionBindingType.disjunctive
• Degree.predictedBinding Degree.PositiveStandard.contextual = Degree.DimensionBindingType.mixed
• Degree.predictedBinding Degree.PositiveStandard.functional = Degree.DimensionBindingType.mixed