Hay, Kennedy and Levin (1999): Scalar Structure Underlies Telicity in "Degree Achievements"

This file formalizes Hay, Kennedy and Levin's analysis of degree achievements. The morpheme that forms the verb contributes an increase, true of an event when the affected argument's degree on the base adjective's scale at the end of the event is its degree at the start plus a difference value, and the predicate is telic exactly when the difference value is bounded, specifying a positive lower bound on the change. A bound can come from a measure phrase or completely, from significantly as against slightly, from the maximal value of a closed-range base adjective, or from a conventional value supplied by context. A bound that is only implicated can be cancelled and one supplied by overt material cannot, which is why an unmodified degree achievement takes both adverbials and one modified by completely only the in-adverbial. The paper's closed-range and open-range adjectives are checked against the scales of the English fragment.

Implementation notes

• Degrees form a densely ordered abelian group, whose addition extends the paper's degree addition (15), defined only when a summand is positive. The maximal scale value is a degree top rather than a top element, and density makes "some amount" and slightly unbounded.
• The readings of a description are its admissible difference values. Overt material fixes one; with none there is the literal "some amount" and, when a maximal or conventional value is salient, the bounded value it implicates. The in-adverbial and for-adverbial tests are read as the existence of a bounded and of an unbounded reading.
• The almost test and the causative component of transitive degree achievements are not modelled.

TODO

• The parallel with the mass–count distinction and the redefinition of the incremental theme as the difference value (§4.2), which want a shared substrate with Krifka's cumulativity.

References

• J. Hay, C. Kennedy and B. Levin, Scalar Structure Underlies Telicity in “Degree Achievements” (1999)
• C. Kennedy and L. McNally, Scale Structure, Degree Modification, and the Semantics of Gradable Predicates (2005)
• D. R. Dowty, Word Meaning and Montague Grammar (1979)
• M. Krifka, Nominal Reference, Temporal Constitution and Quantification in Event Semantics (1989)

The difference value (§2)

def HayKennedyLevin1999.Increase {α : Type u_1} {δ : Type u_2} {T : Type u_3} [Add δ] (φ : α → T → δ) (x : α) (d : δ) (t₀ t₁ : T) : Prop

Increase φ x d t₀ t₁ holds when x increases in φ-ness by the difference value d over an event that begins at t₀ and ends at t₁ ((16)).

Equations

• HayKennedyLevin1999.Increase φ x d t₀ t₁ = (φ x t₀ + d = φ x t₁)

def HayKennedyLevin1999.Describes {α : Type u_1} {δ : Type u_2} {T : Type u_3} [Add δ] (φ : α → T → δ) (x : α) (D : Set δ) (t₀ t₁ : T) : Prop

A description holds when x increases by some difference value in D, the positive degrees for (17a) and {5 inches} for (17b).

Equations

• HayKennedyLevin1999.Describes φ x D t₀ t₁ = ∃ d ∈ D, HayKennedyLevin1999.Increase φ x d t₀ t₁

theorem HayKennedyLevin1999.Increase.end_unique {α : Type u_1} {δ : Type u_2} {T : Type u_3} [Add δ] {φ : α → T → δ} {x : α} {d : δ} {t₀ t₁ t₂ : T} (h₁ : Increase φ x d t₀ t₁) (h₂ : Increase φ x d t₀ t₂) : φ x t₁ = φ x t₂

With the difference value given, the degree at the end of the event is determined by the degree at its start, the source of an identifiable endpoint (§3).

theorem HayKennedyLevin1999.describes_iff_sub_mem {α : Type u_1} {δ : Type u_2} {T : Type u_3} [AddCommGroup δ] {φ : α → T → δ} {x : α} {D : Set δ} {t₀ t₁ : T} : Describes φ x D t₀ t₁ ↔ φ x t₁ - φ x t₀ ∈ D

In a group a description holds exactly when the difference between the final and the initial degree is one of its difference values.

def HayKennedyLevin1999.IsBounded {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] (D : Set δ) : Prop

A set of difference values is bounded when it has a positive lower bound. Once that much change has happened the truth conditions are met, so the event has an endpoint and the predicate is telic (§3.1).

Equations

• HayKennedyLevin1999.IsBounded D = ∃ (b : δ), 0 < b ∧ b ∈ lowerBounds D

def HayKennedyLevin1999.someAmount {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] : Set δ

The implicit difference value "some amount" is any positive degree ((9a)).

Equations

• HayKennedyLevin1999.someAmount = Set.Ioi 0

def HayKennedyLevin1999.measurePhrase {δ : Type u_2} (m : δ) : Set δ

A measure phrase fixes the difference value at exactly its degree m ((18)).

Equations

• HayKennedyLevin1999.measurePhrase m = {m}

def HayKennedyLevin1999.completely {δ : Type u_2} [AddCommGroup δ] (top i : δ) : Set δ

Completely fixes the difference value at the change that takes the initial degree i to the scale's maximal value top ((21)).

Equations

• HayKennedyLevin1999.completely top i = {top - i}

def HayKennedyLevin1999.significantly {δ : Type u_2} [LinearOrder δ] (s : δ) : Set δ

Significantly, a monotone increasing modifier, admits the difference values of at least the contextual standard s ((23)).

Equations

• HayKennedyLevin1999.significantly s = Set.Ici s

def HayKennedyLevin1999.slightly {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] (s : δ) : Set δ

Slightly, a monotone decreasing modifier, admits the positive difference values of at most s, since part of a slight increase is a slight increase ((24)).

Equations

• HayKennedyLevin1999.slightly s = Set.Ioc 0 s

theorem HayKennedyLevin1999.isBounded_measurePhrase {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] {m : δ} (hm : 0 < m) : IsBounded (measurePhrase m)

theorem HayKennedyLevin1999.isBounded_completely {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] [IsOrderedAddMonoid δ] {top i : δ} (hi : i < top) : IsBounded (completely top i)

theorem HayKennedyLevin1999.isBounded_significantly {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] {s : δ} (hs : 0 < s) : IsBounded (significantly s)

theorem HayKennedyLevin1999.not_isBounded_of_forall {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] {D : Set δ} (h : ∀ (b : δ), 0 < b → ∃ d ∈ D, d < b) : ¬IsBounded D

A difference value that admits arbitrarily small positive changes specifies no bound.

theorem HayKennedyLevin1999.not_isBounded_slightly {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] [DenselyOrdered δ] {s : δ} (hs : 0 < s) : ¬IsBounded (slightly s)

theorem HayKennedyLevin1999.not_isBounded_someAmount {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] [DenselyOrdered δ] : ¬IsBounded someAmount

Readings (§3.2–§3.4)

inductive HayKennedyLevin1999.Modifier (δ : Type u_4) : Type u_4

A modifier is the overt material that can fix a difference value.

• none {δ : Type u_4} : Modifier δ
• measure {δ : Type u_4} (m : δ) : Modifier δ
• completely {δ : Type u_4} : Modifier δ
• significantly {δ : Type u_4} (s : δ) : Modifier δ
• slightly {δ : Type u_4} (s : δ) : Modifier δ

structure HayKennedyLevin1999.Context (δ : Type u_4) : Type u_4

A context supplies what can bound the difference value when nothing overt does, the maximal value of a closed-range base adjective's scale (§3.2) or a conventional maximum for the affected object (§3.3).

• scaleMax : Option δ
• conventionalMax : Option δ

def HayKennedyLevin1999.Context.bound {δ : Type u_2} (c : Context δ) : Option δ

The salient bound of a context is its scale maximum if there is one, and otherwise its conventional maximum.

Equations

• c.bound = (c.scaleMax <|> c.conventionalMax)

def HayKennedyLevin1999.readings {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] (c : Context δ) (i : δ) : Modifier δ → Set (Set δ)

The admissible difference values of a description whose argument starts at degree i are the one that overt material fixes or, with none, the literal "some amount" and, when a bound is salient, the value the most informative interpretation implicates.

Equations

• HayKennedyLevin1999.readings c i HayKennedyLevin1999.Modifier.none = {HayKennedyLevin1999.someAmount} ∪ (Option.map (fun (m : δ) => {HayKennedyLevin1999.completely m i}) c.bound).getD ∅
• HayKennedyLevin1999.readings c i (HayKennedyLevin1999.Modifier.measure m) = {HayKennedyLevin1999.measurePhrase m}
• HayKennedyLevin1999.readings c i HayKennedyLevin1999.Modifier.completely = (Option.map (fun (m : δ) => {HayKennedyLevin1999.completely m i}) c.scaleMax).getD ∅
• HayKennedyLevin1999.readings c i (HayKennedyLevin1999.Modifier.significantly s) = {HayKennedyLevin1999.significantly s}
• HayKennedyLevin1999.readings c i (HayKennedyLevin1999.Modifier.slightly s) = {HayKennedyLevin1999.slightly s}

def HayKennedyLevin1999.HasTelic {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] (c : Context δ) (i : δ) (m : Modifier δ) : Prop

A description has a telic reading, which an in-adverbial needs, when one of its admissible difference values is bounded.

Equations

• HayKennedyLevin1999.HasTelic c i m = ∃ D ∈ HayKennedyLevin1999.readings c i m, HayKennedyLevin1999.IsBounded D

def HayKennedyLevin1999.HasAtelic {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] (c : Context δ) (i : δ) (m : Modifier δ) : Prop

A description has an atelic reading, which a for-adverbial needs, when one of its admissible difference values is unbounded.

Equations

• HayKennedyLevin1999.HasAtelic c i m = ∃ D ∈ HayKennedyLevin1999.readings c i m, ¬HayKennedyLevin1999.IsBounded D

theorem HayKennedyLevin1999.hasTelic_measure {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] {c : Context δ} {i m : δ} (hm : 0 < m) : HasTelic c i (Modifier.measure m)

A measure phrase makes the predicate telic, whatever the base adjective ((18)–(20)).

theorem HayKennedyLevin1999.not_hasAtelic_measure {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] {c : Context δ} {i m : δ} (hm : 0 < m) : ¬HasAtelic c i (Modifier.measure m)

theorem HayKennedyLevin1999.hasTelic_completely {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] {c : Context δ} {i : δ} [IsOrderedAddMonoid δ] {top : δ} (hc : c.scaleMax = some top) (hi : i < top) : HasTelic c i Modifier.completely

Completely makes the predicate telic and leaves no atelic reading ((21)–(22), (35)).

theorem HayKennedyLevin1999.not_hasAtelic_completely {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] {c : Context δ} {i : δ} [IsOrderedAddMonoid δ] {top : δ} (hc : c.scaleMax = some top) (hi : i < top) : ¬HasAtelic c i Modifier.completely

theorem HayKennedyLevin1999.readings_completely_open {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] {c : Context δ} {i : δ} (hc : c.scaleMax = none) : readings c i Modifier.completely = ∅

Completely has no reading on an open-range base ((25b)).

theorem HayKennedyLevin1999.hasTelic_significantly {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] {c : Context δ} {i s : δ} (hs : 0 < s) : HasTelic c i (Modifier.significantly s)

Significantly makes the predicate telic ((23)).

theorem HayKennedyLevin1999.hasAtelic_slightly {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] {c : Context δ} {i : δ} [DenselyOrdered δ] {s : δ} (hs : 0 < s) : HasAtelic c i (Modifier.slightly s)

Slightly leaves the predicate atelic ((24)).

theorem HayKennedyLevin1999.not_hasTelic_slightly {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] {c : Context δ} {i : δ} [DenselyOrdered δ] {s : δ} (hs : 0 < s) : ¬HasTelic c i (Modifier.slightly s)

theorem HayKennedyLevin1999.hasTelic_of_bound {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] {c : Context δ} {i : δ} [IsOrderedAddMonoid δ] {b : δ} (hb : c.bound = some b) (hi : i < b) : HasTelic c i Modifier.none

With a salient bound, from a closed-range base or from convention, an unmodified degree achievement has a telic reading ((26), (28), (34a)).

theorem HayKennedyLevin1999.hasAtelic_none {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] {c : Context δ} {i : δ} [DenselyOrdered δ] : HasAtelic c i Modifier.none

The literal reading is always available, so the implicated bound can be cancelled and the for-adverbial is felicitous ((32), (34b)).

theorem HayKennedyLevin1999.not_hasTelic_none {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] {c : Context δ} {i : δ} [DenselyOrdered δ] (hb : c.bound = none) : ¬HasTelic c i Modifier.none

Without a salient bound an unmodified degree achievement has only the atelic reading ((27), (30), (31)).

Cancellability (§3.3, (32)–(33))

theorem HayKennedyLevin1999.completely_not_cancellable {α : Type u_1} {δ : Type u_2} {T : Type u_3} [AddCommGroup δ] [LinearOrder δ] {φ : α → T → δ} {x : α} {top : δ} {t₀ t₁ : T} (h : Describes φ x (completely top (φ x t₀)) t₀ t₁) : ¬φ x t₁ < top

A bound supplied by overt material cannot be cancelled, so a rope straightened completely is completely straight ((33)).

theorem HayKennedyLevin1999.someAmount_cancellable {δ : Type u_2} [AddCommGroup δ] [LinearOrder δ] [IsOrderedAddMonoid δ] [DenselyOrdered δ] {i top : δ} (hi : i < top) : ∃ (φ : Unit → Bool → δ), Describes φ () someAmount false true ∧ φ () true < top

A bound that is only implicated can be cancelled, the literal "some amount" being consistent with the maximal value not having been reached ((32)).

The English degree achievements (§3.2, (25))

def HayKennedyLevin1999.closedRange : List Degree.GradableAdjective

The closed-range adjectives the paper names are straight, empty and dry ((25a)), and flat.

Equations

• HayKennedyLevin1999.closedRange = [English.Adjectives.straight, English.Adjectives.empty, English.Adjectives.dry, English.Adjectives.flat]

def HayKennedyLevin1999.openRange : List Degree.GradableAdjective

The open-range adjectives the paper names are long, wide and short ((25b)).

Equations

• HayKennedyLevin1999.openRange = [English.Adjectives.long, English.Adjectives.wide, English.Adjectives.short]

theorem HayKennedyLevin1999.fragment_range : (∀ a ∈ closedRange, a.boundedness.HasMax) ∧ ∀ a ∈ openRange, ¬a.boundedness.HasMax

The fragment's adjectives agree with the paper's classification, a closed-range adjective having a scale with a maximum and an open-range one a scale without.

theorem HayKennedyLevin1999.fragment_verbs : (∀ v ∈ [English.Verbs.straighten, English.Verbs.dry, English.Verbs.flatten], ∃ b ∈ v.changeScale, b.HasMax) ∧ ∀ v ∈ [English.Verbs.lengthen, English.Verbs.widen], ∃ b ∈ v.changeScale, ¬b.HasMax

The fragment's degree achievements measure change on scales of the same kind as their base adjectives, straighten, dry and flatten on a scale with a maximum and lengthen and widen on one without.

theorem HayKennedyLevin1999.defaultTelicity_iff (d : Degree.ScalarDimension) (i top : ℚ) (hi : i < top) : d.defaultTelicity = Aspect.Telicity.telic ↔ HasTelic { scaleMax := if d.boundedness.HasMax then some top else none, conventionalMax := none } i Modifier.none

The default telicity the fragment derives for a degree achievement is the telicity of the unmodified reading in a context whose only salient bound is the scale's maximum, when it has one.