Documentation

Linglib.Theories.Semantics.Degree.Core

Degree Semantics: Core Infrastructure #

@cite{heim-2001} @cite{kennedy-2007} @cite{klein-1980} @cite{rett-2026} @cite{schwarzschild-2008} @cite{israel-2011} @cite{kennedy-mcnally-2005}

Shared types and interfaces for degree-based analyses of gradable expressions. This module defines the minimal GradablePredicate interface that all degree semantic frameworks (Kennedy, Heim, Klein, Schwarzschild, Rett) share, and the compositional DegP structure for degree phrase composition.

Design #

Every degree framework provides a measure function μ : Entity → Degree. They differ in how the degree argument is bound and how the standard of comparison is introduced:

Framework	Degree binding	Standard introduction
@cite{kennedy-2007}	Degree quantifier -er	Degree clause
@cite{heim-2001}	Sentential -er operator	λ-abstraction
@cite{klein-1980}	No degrees	Comparison class
Schwarzschild	Intervals on scale	Interval semantics
@cite{rett-2026}	Order-sensitive MAX	Scale-directional MAX

All frameworks except Klein posit degrees; this module provides the interface they share.

Connection to Core.Scale #

Core.Scale defines the algebraic infrastructure (boundedness, MAX, DirectedMeasure, degree/threshold types for computation). This module adds the linguistic interface: gradable predicates, DegP composition, and standard-of-comparison structure.

Relationship to Lexical.Adjective.Theory #

This module uses abstract types (Entity D : Type* with LinearOrder D) for framework-level theorems. Lexical.Adjective.Theory uses concrete Degree max (= Fin (max+1)) for computation in RSA models and Fragment entries. The two serve different clients: this module is imported by Degree/Frameworks/ and Degree/Comparative.lean; Adjective.Theory is imported by Fragments/English/ and Phenomena/Gradability/ bridges.

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, Rett) provides an instance. Klein's delineation approach does not use degrees, so it does not instantiate this interface.

The algebraic content (μ, boundedness, direction) comes from DirectedMeasure. GradablePredicate adds only the lexical identity.

The D parameter is the degree type (e.g., ℚ, Degree max, or an abstract LinearOrder).

boundedness : Boundedness
μ : Entity → D
direction : ScalePolarity
form : String
The adjective's lexical form (for identification)

Instances For

inductive Semantics.Degree.DegPType :

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: [DegP [Deg -er/as/est] [DegComplement than-clause]] Heim: [DegP [-er d₁ d₂]...] (sentential operator)

This type captures the framework-independent parts: what kind of comparison, and what standard type.

comparative : DegPType
equative : DegPType
superlative : DegPType
excessive : DegPType
sufficiency : DegPType

Instances For

instance Semantics.Degree.instDecidableEqDegPType :

DecidableEq DegPType

Equations

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

def Semantics.Degree.instBEqDegPType.beq :

DegPType → DegPType → Bool

Equations

Semantics.Degree.instBEqDegPType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Semantics.Degree.instBEqDegPType :

Equations

Semantics.Degree.instBEqDegPType = { beq := Semantics.Degree.instBEqDegPType.beq }

instance Semantics.Degree.instReprDegPType :

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.

Instances For

inductive Semantics.Degree.StandardType :

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

explicit : StandardType
contextual : StandardType
absolute : StandardType

Instances For

instance Semantics.Degree.instDecidableEqStandardType :

DecidableEq StandardType

Equations

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

instance Semantics.Degree.instBEqStandardType :

BEq StandardType

Equations

Semantics.Degree.instBEqStandardType = { beq := Semantics.Degree.instBEqStandardType.beq }

def Semantics.Degree.instBEqStandardType.beq :

StandardType → StandardType → Bool

Equations

Semantics.Degree.instBEqStandardType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

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.

Instances For

def Semantics.Degree.positiveSem {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (θ : D) (x : Entity) :

The positive (unmarked) form of a gradable adjective: "Kim is tall" is true iff μ(Kim) exceeds a contextual standard θ.

This is the common core across Kennedy and Heim:

Kennedy: ⟦tall⟧ = λd.λx. height(x) ≥ d, with θ = pos(tall)
Heim: ⟦tall⟧ = λx. height(x) ≥ θ_c

Klein's approach is different: "tall" is true relative to a comparison class, with no degree parameter.

Equations

Semantics.Degree.positiveSem μ θ x = (μ x ≥ θ)

Instances For

def Semantics.Degree.positiveFromScale {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [BoundedOrder D] (μ : Entity → D) (b : Core.Scale.Boundedness) (x : Entity) :

The positive form with standard derived from scale structure. @cite{kennedy-2007}: for closed-scale adjectives, the standard IS the scale endpoint (minimum or maximum); for open-scale adjectives, it's contextually determined.

Equations

Semantics.Degree.positiveFromScale μ Core.Scale.Boundedness.closed x = (μ x = ⊤)
Semantics.Degree.positiveFromScale μ Core.Scale.Boundedness.upperBounded x = (μ x = ⊤)
Semantics.Degree.positiveFromScale μ Core.Scale.Boundedness.lowerBounded x = (μ x > ⊥)
Semantics.Degree.positiveFromScale μ Core.Scale.Boundedness.open_ x = True

Instances For

Computational (Bool) versions of threshold comparison using concrete Degree max types. Moved from Lexical.Adjective.Theory — these are general degree operations, not adjective-specific.

def Semantics.Degree.positiveMeaning {max : ℕ} (d : Core.Scale.Degree max) (t : Core.Scale.Threshold max) :

Positive form: degree > threshold

Equations

Semantics.Degree.positiveMeaning d t = decide ({ value := t.value.castSucc } < d)

Instances For

def Semantics.Degree.negativeMeaning {max : ℕ} (d : Core.Scale.Degree max) (t : Core.Scale.Threshold max) :

Negative form: degree < threshold

Equations

Semantics.Degree.negativeMeaning d t = decide (d < { value := t.value.castSucc })

Instances For

def Semantics.Degree.antonymMeaning {max : ℕ} (d : Core.Scale.Degree max) (t : Core.Scale.Threshold max) :

Antonym reverses the comparison

Equations

Semantics.Degree.antonymMeaning d t = decide (d ≤ { value := t.value.castSucc })

Instances For

theorem Semantics.Degree.positiveMeaning_monotone {max : ℕ} (d : Core.Scale.Degree max) (θ_weak θ_strong : Core.Scale.Threshold max) (h_ord : θ_weak ≤ θ_strong) (h_strong : positiveMeaning d θ_strong = true) :

positiveMeaning d θ_weak = true

Monotonicity of positiveMeaning in the threshold: a higher threshold is informationally stronger. If d > θ_strong and θ_weak ≤ θ_strong, then d > θ_weak. This grounds the InformationalStrength distinction between weak adjectives (lower θ) and strong adjectives (higher θ).

inductive Semantics.Degree.ModifierDirection :

Degree modifier direction — same axis as NPI scalar direction.

amplifier : ModifierDirection
downtoner : ModifierDirection

Instances For

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.instBEqModifierDirection.beq :

ModifierDirection → ModifierDirection → Bool

Equations

Semantics.Degree.instBEqModifierDirection.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Semantics.Degree.instBEqModifierDirection :

BEq ModifierDirection

Equations

Semantics.Degree.instBEqModifierDirection = { beq := Semantics.Degree.instBEqModifierDirection.beq }

def Semantics.Degree.instReprModifierDirection.repr :

ModifierDirection → ℕ → Std.Format

Equations

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

Instances For

instance Semantics.Degree.instReprModifierDirection :

Repr ModifierDirection

Equations

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

structure Semantics.Degree.DegreeModifier (max : ℕ) :

A degree modifier that shifts the threshold of a gradable predicate.

form : String
direction : ModifierDirection
shift : Fin (max + 1)
rank : ℕ

Instances For

def Semantics.Degree.instReprDegreeModifier.repr {max✝ : ℕ} :

DegreeModifier max✝ → ℕ → Std.Format

Equations

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

Instances For

instance Semantics.Degree.instReprDegreeModifier {max✝ : ℕ} :

Repr (DegreeModifier max✝)

Equations

Semantics.Degree.instReprDegreeModifier = { reprPrec := Semantics.Degree.instReprDegreeModifier.repr }

def Semantics.Degree.DegreeModifier.applyToThreshold {max : ℕ} (m : DegreeModifier max) (θ : Core.Scale.Threshold max) :

Core.Scale.Threshold max

Apply a modifier to a threshold.

Equations

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

Instances For

def Semantics.Degree.modifiedMeaning {max : ℕ} (m : DegreeModifier max) (d : Core.Scale.Degree max) (θ : Core.Scale.Threshold max) :

A modified gradable predicate: degree(x) > M(θ).

Equations

Semantics.Degree.modifiedMeaning m d θ = Semantics.Degree.positiveMeaning d (m.applyToThreshold θ)

Instances For

def Semantics.Degree.slightly (max : ℕ) (h : 1 ≤ max := by omega) :

DegreeModifier max

"slightly" — minimal downtoner

Equations

Semantics.Degree.slightly max h = { form := "slightly", direction := Semantics.Degree.ModifierDirection.downtoner, shift := ⟨1, ⋯⟩, rank := 1 }

Instances For

def Semantics.Degree.kindOf (max : ℕ) (h : 2 ≤ max := by omega) :

DegreeModifier max

"kind of" — moderate downtoner

Equations

Semantics.Degree.kindOf max h = { form := "kind of", direction := Semantics.Degree.ModifierDirection.downtoner, shift := ⟨2, ⋯⟩, rank := 2 }

Instances For

def Semantics.Degree.quite (max : ℕ) (h : 1 ≤ max := by omega) :

DegreeModifier max

"quite" — amplifier (AmE reading).

Equations

Semantics.Degree.quite max h = { form := "quite", direction := Semantics.Degree.ModifierDirection.amplifier, shift := ⟨1, ⋯⟩, rank := 1 }

Instances For

def Semantics.Degree.very (max : ℕ) (h : 2 ≤ max := by omega) :

DegreeModifier max

"very" — strong amplifier

Equations

Semantics.Degree.very max h = { form := "very", direction := Semantics.Degree.ModifierDirection.amplifier, shift := ⟨2, ⋯⟩, rank := 2 }

Instances For

def Semantics.Degree.extremely (max : ℕ) (h : 3 ≤ max := by omega) :

DegreeModifier max

"extremely" — maximal amplifier

Equations

Semantics.Degree.extremely max h = { form := "extremely", direction := Semantics.Degree.ModifierDirection.amplifier, shift := ⟨3, ⋯⟩, rank := 3 }

Instances For

inductive Semantics.Degree.AdjectivalConstruction :

Degree construction type (positive, comparative, equative, etc.). Used by evaluativity analyses to track which constructions trigger evaluative readings.

Instances For

instance Semantics.Degree.instReprAdjectivalConstruction :

Repr AdjectivalConstruction

Equations

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

def Semantics.Degree.instReprAdjectivalConstruction.repr :

AdjectivalConstruction → ℕ → Std.Format

Equations

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

Instances For

instance Semantics.Degree.instDecidableEqAdjectivalConstruction :

DecidableEq AdjectivalConstruction

Equations

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

def Semantics.Degree.instBEqAdjectivalConstruction.beq :

AdjectivalConstruction → AdjectivalConstruction → Bool

Equations

Semantics.Degree.instBEqAdjectivalConstruction.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Semantics.Degree.instBEqAdjectivalConstruction :

BEq AdjectivalConstruction

Equations

Semantics.Degree.instBEqAdjectivalConstruction = { beq := Semantics.Degree.instBEqAdjectivalConstruction.beq }

instance Semantics.Degree.instToStringAdjectivalConstruction :

ToString AdjectivalConstruction

Equations

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

inductive Semantics.Degree.PositiveStandard :

Positive form standard: how the contextual threshold is determined. @cite{kennedy-2007}: for open scales, the standard is the contextual norm; for closed scales, it's the relevant endpoint.

contextual : PositiveStandard
minEndpoint : PositiveStandard
maxEndpoint : PositiveStandard
functional : PositiveStandard

Instances For

instance Semantics.Degree.instDecidableEqPositiveStandard :

DecidableEq PositiveStandard

Equations

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

instance Semantics.Degree.instBEqPositiveStandard :

BEq PositiveStandard

Equations

Semantics.Degree.instBEqPositiveStandard = { beq := Semantics.Degree.instBEqPositiveStandard.beq }

def Semantics.Degree.instBEqPositiveStandard.beq :

PositiveStandard → PositiveStandard → Bool

Equations

Semantics.Degree.instBEqPositiveStandard.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Semantics.Degree.instReprPositiveStandard :

Repr PositiveStandard

Equations

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

def Semantics.Degree.instReprPositiveStandard.repr :

PositiveStandard → ℕ → Std.Format

Equations

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

Instances For

def Semantics.Degree.interpretiveEconomy (b : Core.Scale.Boundedness) :

PositiveStandard

Interpretive Economy determines the standard from scale structure. When a scale has an endpoint, Interpretive Economy requires using it as the standard (more informative than contextual norm).

Equations

Instances For

def Semantics.Degree.isClassA (b : Core.Scale.Boundedness) :

@cite{kennedy-2007}'s relative vs. absolute adjective distinction. Kennedy uses "relative" and "absolute"; we label them Class A/B for brevity.

Class A (= Kennedy's "relative"): open scale, contextual standard determined by the standard-fixing function s. "tall", "expensive", "heavy"
Class B (= Kennedy's "absolute"): closed scale, endpoint standard fixed by Interpretive Economy. "full", "empty", "straight", "bent"

The class is determined entirely by scale boundedness (§4.2, p. 32-35). Kennedy argues (§2.3, p. 16) that comparison classes are descriptively real but not semantic arguments of pos — they influence the standard through contextual domain restriction, not as constituents of the logical form (contra @cite{klein-1980}).

Equations

Instances For

def Semantics.Degree.isClassB (b : Core.Scale.Boundedness) :

Equations

Semantics.Degree.isClassB b = !Semantics.Degree.isClassA b

Instances For

theorem Semantics.Degree.classA_contextual :

interpretiveEconomy Core.Scale.Boundedness.open_ = PositiveStandard.contextual

Class A adjectives have contextual standards.

theorem Semantics.Degree.classB_endpoint :

interpretiveEconomy Core.Scale.Boundedness.closed = PositiveStandard.maxEndpoint

Class B adjectives (closed scale) have endpoint standards.

def Semantics.Degree.PositiveStandard.requiresComparisonClass :

PositiveStandard → Bool

Whether the positive standard depends on contextual domain information.

@cite{kennedy-2007} argues (§2.3, p. 16) that the comparison class "is not the crucial feature on which we should be basing an account of the semantic properties of vague predicates" — it is NOT a semantic argument of pos (contra @cite{klein-1980}). Instead, Kennedy replaces it with the standard-fixing function s (eq 27): ⟦pos⟧ = λg.λx. g(x) ≥ s(g).

Nevertheless, for relative (open-scale) adjectives, s still requires contextual domain information — "the distribution of objects in some domain (a comparison class)" (p. 42). For absolute (closed-scale) adjectives, the standard comes from scale endpoints via Interpretive Economy, with no contextual domain needed.

true for .contextual (standard depends on contextual domain), false for .minEndpoint / .maxEndpoint (standard is a scale bound).

Equations

Instances For

theorem Semantics.Degree.classA_requires_cc :

(interpretiveEconomy Core.Scale.Boundedness.open_).requiresComparisonClass = true

Relative (Class A) adjectives need contextual domain information: open scale → contextual s → domain-dependent.

theorem Semantics.Degree.classB_no_cc (b : Core.Scale.Boundedness) (h : isClassA b = false) :

(interpretiveEconomy b).requiresComparisonClass = false

Absolute (Class B) adjectives do NOT need contextual domain information: bounded scale → endpoint standard → domain-independent.

theorem Semantics.Degree.scale_determines_cc_sensitivity (b : Core.Scale.Boundedness) :

isClassA b = (interpretiveEconomy b).requiresComparisonClass

The full chain: isClassA ↔ requiresComparisonClass after Interpretive Economy. Scale structure determines everything.

inductive Semantics.Degree.AdjectiveClass :

Kennedy's adjective classification based on scale structure and standard type.

The key distinction:

Relative Gradable Adjectives (RGA): Standard varies with comparison class Examples: tall, expensive, big, old
Absolute Gradable Adjectives (AGA): Standard fixed by scale structure
- Maximum standard: full, straight, closed, dry
- Minimum standard: wet, bent, open, dirty

Source: @cite{kennedy-2007}, @cite{kennedy-mcnally-2005}

relativeGradable : AdjectiveClass
absoluteMaximum : AdjectiveClass
absoluteMinimum : AdjectiveClass
mildlyPositive : AdjectiveClass

Instances For

def Semantics.Degree.instReprAdjectiveClass.repr :

AdjectiveClass → ℕ → Std.Format

Equations

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

Instances For

instance Semantics.Degree.instReprAdjectiveClass :

Repr AdjectiveClass

Equations

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

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.instBEqAdjectiveClass.beq :

AdjectiveClass → AdjectiveClass → Bool

Equations

Semantics.Degree.instBEqAdjectiveClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Semantics.Degree.instBEqAdjectiveClass :

BEq AdjectiveClass

Equations

Semantics.Degree.instBEqAdjectiveClass = { beq := Semantics.Degree.instBEqAdjectiveClass.beq }

def Semantics.Degree.AdjectiveClass.isRelative :

AdjectiveClass → Bool

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

Equations

Instances For