Gradable adjectives

Adjective-specific degree semantics, layered on the syntactic Adjective (Syntax/Adjective): the GradableAdjective lexeme with its derived Kennedy classification, the two-threshold model for contrary antonyms, multidimensional binding ([Sas13]), and the bridge from a concrete Degree scale to the abstract DirectedMeasure.

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.
• adjMeasure — a GradableAdjective read as a DirectedMeasure over a scale.

Core degree types (Degree, Threshold) live in Core.MeasurementScale; the threshold semantics (positiveMeaning, negativeMeaning) in Semantics/Degree/Basic. The intersective/subsective/privative classification lives in Classification.lean.

Two-threshold model for contrary antonyms

structure Semantics.Gradability.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 : Degree.Threshold max
• neg : Degree.Threshold max

@[implicit_reducible]

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

Equations

• Semantics.Gradability.instReprThresholdPair = { reprPrec := Semantics.Gradability.instReprThresholdPair.repr }

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

Equations

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

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

Equations

• Semantics.Gradability.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 ⋯

@[implicit_reducible]

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

Equations

• Semantics.Gradability.instDecidableEqThresholdPair = Semantics.Gradability.instDecidableEqThresholdPair.decEq

@[implicit_reducible]

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

Equations

• Semantics.Gradability.instBEqThresholdPair = { beq := Semantics.Gradability.instBEqThresholdPair.beq }

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

Equations

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

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 Semantics.Gradability.contradictoryNeg {max : ℕ} (d : Degree.Degree max) (θ : Degree.Threshold max) : Prop

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

Equations

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

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

Equations

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

Antonym relations

@[reducible, inline]

abbrev Semantics.Gradability.AntonymRelation : Type

The relation between a positive form and its antonym.

Equations

• Semantics.Gradability.AntonymRelation = Features.NegationType

Informational strength

inductive Semantics.Gradability.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

def Semantics.Gradability.instReprInformationalStrength.repr : InformationalStrength → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Gradability.instReprInformationalStrength : Repr InformationalStrength

Equations

• Semantics.Gradability.instReprInformationalStrength = { reprPrec := Semantics.Gradability.instReprInformationalStrength.repr }

@[implicit_reducible]

instance Semantics.Gradability.instDecidableEqInformationalStrength : DecidableEq InformationalStrength

Equations

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

The gradable adjective

inductive Semantics.Gradability.SpatialConfigType : Type

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

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

@[implicit_reducible]

instance Semantics.Gradability.instDecidableEqSpatialConfigType : DecidableEq SpatialConfigType

Equations

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

def Semantics.Gradability.instReprSpatialConfigType.repr : SpatialConfigType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Gradability.instReprSpatialConfigType : Repr SpatialConfigType

Equations

• Semantics.Gradability.instReprSpatialConfigType = { reprPrec := Semantics.Gradability.instReprSpatialConfigType.repr }

structure Semantics.Gradability.GradableAdjectiveextends Adjective : Type

A gradable adjective: the syntactic Adjective (Syntax/Adjective) refined with the degree-semantic layer that becomes relevant in this module — the Kennedy standardOverride, and the lexical-semantic facets antonymRelation, resultative spatialConfigType ([Lev26]), 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 Semantics.Gradability.Dimension
• isLowerEndpoint : Bool
• comparison : ComparisonFacet
• antonymForm : Option String
• standardOverride : Option Degree.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 ([Lev26]).

• 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.

def Semantics.Gradability.instReprGradableAdjective.repr : GradableAdjective → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Gradability.instReprGradableAdjective : Repr GradableAdjective

Equations

• Semantics.Gradability.instReprGradableAdjective = { reprPrec := Semantics.Gradability.instReprGradableAdjective.repr }

def Semantics.Gradability.GradableAdjective.scaleType (g : GradableAdjective) : Core.Order.Boundedness

The scale's intrinsic shape — read off the dimension key, not stored (.open_ for a non-gradable, which has no scale).

Equations

• g.scaleType = (Option.map Semantics.Gradability.Dimension.boundedness g.dimension).getD Core.Order.Boundedness.open_

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

The effective positive standard: the default from (scale shape, pole), overridable by standardOverride. This is the quantity the old scaleType field conflated — it separates wet (closed + lower ⇒ min) from dry (closed + upper ⇒ max), and lets good (open shape) take a contextual standard rather than a bogus bound. ([Ken07]'s Interpretive Economy on the open/singly-bounded cases.)

Equations

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

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

Kennedy's adjective class — derived from standard, not stored; .nonGradable exactly when there is no dimension ([Ken07], [KMcN05]).

Equations

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

def Semantics.Gradability.GradableAdjective.IsRelative (g : GradableAdjective) : Prop

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

Equations

• g.IsRelative = g.adjectiveClass.IsRelative

@[implicit_reducible]

instance Semantics.Gradability.GradableAdjective.instDecidableIsRelative (g : GradableAdjective) : Decidable g.IsRelative

Equations

• g.instDecidableIsRelative = id inferInstance

Multidimensional adjectives ([Sas13])

inductive Semantics.Gradability.DimensionBindingType : Type

How a multidimensional adjective binds its dimensions ([Sas13]).

• 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

@[implicit_reducible]

instance Semantics.Gradability.instReprDimensionBindingType : Repr DimensionBindingType

Equations

• Semantics.Gradability.instReprDimensionBindingType = { reprPrec := Semantics.Gradability.instReprDimensionBindingType.repr }

def Semantics.Gradability.instReprDimensionBindingType.repr : DimensionBindingType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Gradability.instDecidableEqDimensionBindingType : DecidableEq DimensionBindingType

Equations

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

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

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

Equations

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

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

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

Equations

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

theorem Semantics.Gradability.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 [Sas13]'s Hypothesis 2 — under a negation theory of antonymy, if the positive form is conjunctive, the negative antonym (its negation) is disjunctive.

theorem Semantics.Gradability.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 Semantics.Gradability.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

• Semantics.Gradability.DimensionBindingType.conjunctive.negate = Semantics.Gradability.DimensionBindingType.disjunctive
• Semantics.Gradability.DimensionBindingType.disjunctive.negate = Semantics.Gradability.DimensionBindingType.conjunctive
• Semantics.Gradability.DimensionBindingType.mixed.negate = Semantics.Gradability.DimensionBindingType.mixed

theorem Semantics.Gradability.negate_involutive (b : DimensionBindingType) : b.negate.negate = b

def Semantics.Gradability.predictedBinding : Degree.PositiveStandard → DimensionBindingType

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

Equations

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

Marginality scales ([DJ26])

structure Semantics.Gradability.GradableMLScale (α : Type u_1) [LinearOrder α] (W : Type u_2) extends Degree.DirectedMeasure α W : Type (max u_1 u_2)

• boundedness : Boundedness
• μ : W → α
• direction : Core.Order.ScalePolarity
• ml : MLScale α

def Semantics.Gradability.marginalityPositive {α : Type u_1} [LinearOrder α] (ml : MLScale α) (norm degree : α) : Prop

Equations

• Semantics.Gradability.marginalityPositive ml norm degree = ml.L norm degree

theorem Semantics.Gradability.marginality_entails_standard {α : Type u_1} [LinearOrder α] (ml : MLScale α) (norm degree : α) (h : marginalityPositive ml norm degree) : norm < degree

Degree–DirectedMeasure bridge

Degree max has LinearOrder and BoundedOrder (from Core.MeasurementScale), so the abstract theorems in MeasurementScale.lean apply directly to concrete RSA degree computations.

def Semantics.Gradability.adjMeasure {max : ℕ} {W : Type u_1} (μ : W → Degree.Degree max) (entry : GradableAdjective) : Degree.DirectedMeasure (Degree.Degree max) W

Equations

• Semantics.Gradability.adjMeasure μ entry = Degree.DirectedMeasure.adjective μ entry.scaleType

theorem Semantics.Gradability.closedAdj_licensed {max : ℕ} {W : Type u_1} (μ : W → Degree.Degree max) (entry : GradableAdjective) (h : entry.scaleType = Core.Order.Boundedness.closed) : (adjMeasure μ entry).IsLicensed

theorem Semantics.Gradability.openAdj_blocked {max : ℕ} {W : Type u_1} (μ : W → Degree.Degree max) (entry : GradableAdjective) (h : entry.scaleType = Core.Order.Boundedness.open_) : ¬(adjMeasure μ entry).IsLicensed

theorem Semantics.Gradability.degree_nontrivial {max : ℕ} (h : 1 ≤ max) : ∃ (x : Degree.Degree max), x ≠ ⊤

theorem Semantics.Gradability.degree_admits_optimum {max : ℕ} (h : 1 ≤ max) : ∃ (P : Degree.Degree max → Prop), (∀ (x y : Degree.Degree max), x ≤ y → P x → P y) ∧ ¬∀ (x y : Degree.Degree max), P x ↔ P y

theorem Semantics.Gradability.degree_measure_is_id {max : ℕ} {W : Type u_1} (μ : W → Degree.Degree max) : (Degree.DirectedMeasure.numeral μ).μ = μ