Degree Semantics: Type Definitions

Pure type definitions for degree-based analyses of gradable expressions @cite{heim-2001} @cite{kennedy-2007} @cite{schwarzschild-2008} @cite{beltrama-2025}. Positive-form semantics is in Basic.lean; Kennedy 2007's interpretive economy classification is in Kennedy.lean. Klein-style delineation @cite{klein-1980} has no measure function and lives in Theories/Semantics/Gradability/Delineation.lean.

Main definitions

• GradablePredicate — measure-function interface extending DirectedMeasure
• DegPType, StandardType — DegP compositional taxonomy
• ModifierDirection — amplifier / downtoner axis
• AdjectivalConstruction — surface-construction type for evaluativity
• PositiveStandard, AdjectiveClass — Kennedy-style classification carriers

structure Semantics.Degree.GradablePredicate (Entity : Type u_1) (D : Type u_2) [LinearOrder D] extends Core.Scale.DirectedMeasure D Entity : Type (max u_1 u_2)

Minimal interface for a gradable predicate: a measure function mapping entities to degrees on a scale with known boundedness.

Extends DirectedMeasure D Entity with a lexical form field. Every degree framework (Kennedy, Heim, Schwarzschild) provides an instance; Klein's delineation approach does not use degrees and so does not instantiate this interface (see Gradability/Delineation.lean).

• boundedness : Boundedness
• μ : Entity → D
• direction : ScalePolarity
• form : String

  The adjective's lexical form (for identification).

inductive Semantics.Degree.DegPType : Type

The compositional structure of a Degree Phrase (DegP).

In all degree frameworks, DegP is the syntactic locus where degree comparison happens. The internal structure varies — Kennedy posits [DegP [Deg -er/as/est] [DegComplement than-clause]], Heim posits a sentential -er operator — but the framework-independent taxonomy is captured here.

• comparative : DegPType

  -er / more.

• equative : DegPType

  as...as.

• superlative : DegPType

  -est / most.

• excessive : DegPType

  too.

• sufficiency : DegPType

  enough.

@[implicit_reducible]

instance Semantics.Degree.instDecidableEqDegPType : DecidableEq DegPType

Equations

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

@[implicit_reducible]

instance Semantics.Degree.instReprDegPType : Repr DegPType

Equations

• Semantics.Degree.instReprDegPType = { reprPrec := Semantics.Degree.instReprDegPType.repr }

def Semantics.Degree.instReprDegPType.repr : DegPType → ℕ → Std.Format

Equations

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

inductive Semantics.Degree.StandardType : Type

The standard of comparison: what the degree is compared to.

• explicit : StandardType

  "taller than Bill" — explicit standard.

• contextual : StandardType

  "tall" — contextually determined standard.

• absolute : StandardType

  "full" — scale endpoint as standard.

@[implicit_reducible]

instance Semantics.Degree.instDecidableEqStandardType : DecidableEq StandardType

Equations

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

@[implicit_reducible]

instance Semantics.Degree.instReprStandardType : Repr StandardType

Equations

• Semantics.Degree.instReprStandardType = { reprPrec := Semantics.Degree.instReprStandardType.repr }

def Semantics.Degree.instReprStandardType.repr : StandardType → ℕ → Std.Format

Equations

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

inductive Semantics.Degree.ModifierDirection : Type

Degree modifier direction — the same axis as NPI scalar direction. Lexical instantiations of named modifiers (slightly, very, quite, etc.) live in consuming Studies files (e.g. Phenomena/Politeness/Studies/MachinoEtAl2025.lean for the AmE/BrE quite contrast).

• amplifier : ModifierDirection

  very, extremely — raises the threshold.

• downtoner : ModifierDirection

  slightly, kind of — lowers the threshold.

@[implicit_reducible]

instance Semantics.Degree.instDecidableEqModifierDirection : DecidableEq ModifierDirection

Equations

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

def Semantics.Degree.instReprModifierDirection.repr : ModifierDirection → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Degree.instReprModifierDirection : Repr ModifierDirection

Equations

• Semantics.Degree.instReprModifierDirection = { reprPrec := Semantics.Degree.instReprModifierDirection.repr }

inductive Semantics.Degree.AdjectivalConstruction : Type

Degree construction type. Used by evaluativity analyses to track which surface constructions trigger evaluative readings.

• positive : AdjectivalConstruction

  "Kim is tall" — unmarked form.

• comparative : AdjectivalConstruction

  "Kim is taller than Sam".

• equative : AdjectivalConstruction

  "Kim is as tall as Sam".

• measurePhrase : AdjectivalConstruction

  "Kim is 6 feet tall" — explicit measure phrase.

• degreeQuestion : AdjectivalConstruction

  "How tall is Kim?".

def Semantics.Degree.instReprAdjectivalConstruction.repr : AdjectivalConstruction → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Degree.instReprAdjectivalConstruction : Repr AdjectivalConstruction

Equations

• Semantics.Degree.instReprAdjectivalConstruction = { reprPrec := Semantics.Degree.instReprAdjectivalConstruction.repr }

@[implicit_reducible]

instance Semantics.Degree.instDecidableEqAdjectivalConstruction : DecidableEq AdjectivalConstruction

Equations

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

@[implicit_reducible]

instance Semantics.Degree.instToStringAdjectivalConstruction : ToString AdjectivalConstruction

User-facing rendering, distinct from Repr (which prefixes the namespace). Consumed by Studies files that string-interpolate construction names into diagnostic messages — see e.g. Phenomena/Gradability/Studies/Rett2015Implicature.lean.

Equations

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

inductive Semantics.Degree.PositiveStandard : Type

Positive form standard: how the contextual threshold is determined. For open scales, the standard is the contextual norm (@cite{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 (@cite{beltrama-2025}).

@[implicit_reducible]

instance Semantics.Degree.instDecidableEqPositiveStandard : DecidableEq PositiveStandard

Equations

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

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

Equations

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

@[implicit_reducible]

instance Semantics.Degree.instReprPositiveStandard : Repr PositiveStandard

Equations

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

def Semantics.Degree.PositiveStandard.RequiresComparisonClass : PositiveStandard → Prop

Whether the positive standard depends on contextual domain information.

@cite{kennedy-2007} argues the comparison class is not a semantic argument of pos (contra @cite{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

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

@[implicit_reducible]

instance Semantics.Degree.instDecidablePredPositiveStandardRequiresComparisonClass : DecidablePred PositiveStandard.RequiresComparisonClass

Equations

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

inductive Semantics.Degree.AdjectiveClass : Type

Kennedy's adjective classification by scale structure and standard type @cite{kennedy-2007} @cite{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 (@cite{beltrama-2025}).

• nonGradable : AdjectiveClass

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

@[implicit_reducible]

instance Semantics.Degree.instReprAdjectiveClass : Repr AdjectiveClass

Equations

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

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

Equations

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

@[implicit_reducible]

instance Semantics.Degree.instDecidableEqAdjectiveClass : DecidableEq AdjectiveClass

Equations

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

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

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

Equations

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

@[implicit_reducible]

instance Semantics.Degree.instDecidablePredAdjectiveClassIsRelative : DecidablePred AdjectiveClass.IsRelative

Equations

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