Degree Achievements

@cite{kennedy-levin-2008}

@cite{kennedy-levin-2008} show that degree achievements (rust, cool, widen, increase) have variable telicity determined by the boundedness of the underlying adjectival scale:

• Closed-scale adjectives (clean, full, straight) → telic degree achievements
• Open-scale adjectives (long, wide, cool) → atelic degree achievements

A degree achievement V derived from adjective A has a measure of change function mΔ(e) = d(result(e)) - d(init(e)) on A's scale. Telicity = whether mΔ is bounded: if A's scale has a maximum, mΔ is bounded → telic (accomplishment); if A's scale is open, mΔ is unbounded → atelic (activity).

This module derives VendlerClass from Boundedness, connecting to the existing LicensingPipeline infrastructure in Core/Scales/Scale.lean.

• Kennedy, C. & Levin, B. (2007). Measure of change: The adjectival core of degree achievements. In L. McNally & C. Kennedy (eds.), Adjectives and Adverbs, 156–182. OUP.

structure Features.DegreeAchievement.DegreeAchievementScale : Type

A degree achievement's base scale structure.

The key claim: the telicity of a degree achievement verb is determined by the boundedness of the scale inherited from the base adjective. Scales with a maximum (closed, upper-bounded) yield telic VPs; scales without a maximum (open, lower-bounded) yield atelic VPs.

• scaleBoundedness : Core.Scale.Boundedness

  The adjectival base's scale boundedness.

• dimension : String

  The dimension of change (height, temperature, fullness,...).

• baseAdjective : Option String

  Citation form of the base adjective (if deadjectival).

def Features.DegreeAchievement.instReprDegreeAchievementScale.repr : DegreeAchievementScale → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.DegreeAchievement.instReprDegreeAchievementScale : Repr DegreeAchievementScale

Equations

• Features.DegreeAchievement.instReprDegreeAchievementScale = { reprPrec := Features.DegreeAchievement.instReprDegreeAchievementScale.repr }

@[implicit_reducible]

instance Features.DegreeAchievement.instBEqDegreeAchievementScale : BEq DegreeAchievementScale

Equations

• Features.DegreeAchievement.instBEqDegreeAchievementScale = { beq := Features.DegreeAchievement.instBEqDegreeAchievementScale.beq }

def Features.DegreeAchievement.instBEqDegreeAchievementScale.beq : DegreeAchievementScale → DegreeAchievementScale → Bool

Equations

• One or more equations did not get rendered due to their size.
• Features.DegreeAchievement.instBEqDegreeAchievementScale.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Features.DegreeAchievement.instInhabitedDegreeAchievementScale : Inhabited DegreeAchievementScale

Equations

• Features.DegreeAchievement.instInhabitedDegreeAchievementScale = { default := { scaleBoundedness := Core.Scale.Boundedness.open_, dimension := "" } }

def Features.DegreeAchievement.DegreeAchievementScale.defaultTelicity (s : DegreeAchievementScale) : Telicity

Derive default telicity from scale boundedness (@cite{kennedy-levin-2008} Thm 1). Scales with a maximum → telic; scales without → atelic.

The mapping follows Boundedness.hasMax:

• .closed (has max) → .telic
• .upperBounded (has max) → .telic
• .open_ (no max) → .atelic
• .lowerBounded (no max) → .atelic

Equations

• s.defaultTelicity = if s.scaleBoundedness.hasMax = true then Features.Telicity.telic else Features.Telicity.atelic

def Features.DegreeAchievement.DegreeAchievementScale.defaultVendlerClass (s : DegreeAchievementScale) : VendlerClass

Derive default VendlerClass from scale boundedness. All degree achievements are dynamic and durative, so: telic → accomplishment, atelic → activity.

Equations

• s.defaultVendlerClass = if s.scaleBoundedness.hasMax = true then Features.VendlerClass.accomplishment else Features.VendlerClass.activity

theorem Features.DegreeAchievement.closed_scale_telic (d : String) (a : Option String) : { scaleBoundedness := Core.Scale.Boundedness.closed, dimension := d, baseAdjective := a }.defaultTelicity = Telicity.telic

Closed scaleBoundedness → telic.

theorem Features.DegreeAchievement.open_scale_atelic (d : String) (a : Option String) : { scaleBoundedness := Core.Scale.Boundedness.open_, dimension := d, baseAdjective := a }.defaultTelicity = Telicity.atelic

Open scaleBoundedness → atelic.

theorem Features.DegreeAchievement.upperBounded_telic (d : String) (a : Option String) : { scaleBoundedness := Core.Scale.Boundedness.upperBounded, dimension := d, baseAdjective := a }.defaultTelicity = Telicity.telic

Upper-bounded → telic (has max → bounded mΔ).

theorem Features.DegreeAchievement.lowerBounded_atelic (d : String) (a : Option String) : { scaleBoundedness := Core.Scale.Boundedness.lowerBounded, dimension := d, baseAdjective := a }.defaultTelicity = Telicity.atelic

Lower-bounded → atelic (no max → unbounded mΔ).

theorem Features.DegreeAchievement.closed_scale_accomplishment (d : String) (a : Option String) : { scaleBoundedness := Core.Scale.Boundedness.closed, dimension := d, baseAdjective := a }.defaultVendlerClass = VendlerClass.accomplishment

Closed scaleBoundedness → accomplishment.

theorem Features.DegreeAchievement.open_scale_activity (d : String) (a : Option String) : { scaleBoundedness := Core.Scale.Boundedness.open_, dimension := d, baseAdjective := a }.defaultVendlerClass = VendlerClass.activity

Open scaleBoundedness → activity.

theorem Features.DegreeAchievement.default_vendler_is_dynamic (s : DegreeAchievementScale) : s.defaultVendlerClass = VendlerClass.accomplishment ∨ s.defaultVendlerClass = VendlerClass.activity

defaultVendlerClass always returns.accomplishment or.activity — degree achievements are always dynamic and durative.

theorem Features.DegreeAchievement.telicity_vendler_agree (s : DegreeAchievementScale) : s.defaultVendlerClass.telicity = s.defaultTelicity

defaultTelicity agrees with the telicity of defaultVendlerClass.

@[implicit_reducible]

instance Features.DegreeAchievement.instLicensingPipelineDegreeAchievementScale : Core.Scale.LicensingPipeline DegreeAchievementScale

LicensingPipeline instance for DegreeAchievementScale: maps through scaleBoundedness directly. hasMax → closed, else open.

Equations

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