Documentation

Studies.KennedyLevin2008

Kennedy and Levin (2008): Measure of Change #

This file formalizes Kennedy and Levin's account of variable telicity in degree achievements. Following Kennedy and McNally, a comparative such as wider than the carpet measures on the part of its adjective's scale from the comparative standard up, which Kennedy and Levin call a difference function. A degree achievement is built on a measure of change, the difference function at the degree its argument has when the event begins, applied when it ends. The scale of a measure of change always has a least degree and inherits any greatest degree of the adjective's scale, so Interpretive Economy admits a minimum standard for every degree achievement, giving the atelic comparative reading, and a maximum standard, giving the telic reading, exactly when the adjective's scale is closed above; the telic reading entails the atelic one and is preferred. Widen thus has no telic reading and never means become wide.

The account agrees with Hay, Kennedy and Levin's difference values on both readings and on completely and slightly, and differs on measure phrases, which require at least their degree of change here and exactly that degree there. The English fragment's degree achievements take the Vendler class that Interpretive Economy gives their base scales.

Implementation notes #

TODO #

References #

Difference functions (23)–(24) #

theorem KennedyLevin2008.comparative_iff {E : Type u_1} {δ : Type u_2} [LinearOrder δ] (μ : E → δ) (a b : E) :
⊥ < Set.projIci (μ b) (μ a) ↔ μ b < μ a

At the minimum standard, the difference function at b's degree holds of a exactly when a has more of the property than b ((23)–(24)).

theorem KennedyLevin2008.comparative_eq_top_iff {E : Type u_1} {δ : Type u_2} [LinearOrder δ] (μ : E → δ) (a b : E) [OrderTop δ] (h : μ b ≠ ⊤) :
Set.projIci (μ b) (μ a) = ⊤ ↔ μ a = ⊤

At a maximum standard, a comparative would hold exactly when the positive form does, unless the standard already has the greatest degree (fn. 16).

The measure of change and its readings (25)–(27) #

theorem KennedyLevin2008.admits_iff {α : Type u_1} {δ : Type u_2} {T : Type u_3} [LinearOrder δ] (m : α → T → δ) (x : α) (i : T) {s : Degree.PositiveStandard} :

Interpretive Economy admits the minimum standard on the scale of a measure of change, the maximum exactly when the adjective's scale has a greatest degree, and never the contextual standard (§7.3.3).

theorem KennedyLevin2008.admits_iff_of_noMaxOrder {α : Type u_1} {δ : Type u_2} {T : Type u_3} [LinearOrder δ] (m : α → T → δ) (x : α) (i : T) [NoMaxOrder δ] {s : Degree.PositiveStandard} :

Without a greatest degree only the minimum standard is admitted, so widen has no telic reading and does not mean become wide ((6)).

theorem KennedyLevin2008.defaultStandard_eq {α : Type u_1} {δ : Type u_2} {T : Type u_3} [LinearOrder δ] (m : α → T → δ) (x : α) (i : T) :

The preferred standard on the scale of a measure of change is the maximum when the adjective's scale has one, and the minimum otherwise.

theorem KennedyLevin2008.minStandard_iff {α : Type u_1} {δ : Type u_2} {T : Type u_3} [LinearOrder δ] (m : α → T → δ) (x : α) (i f : T) :
⊥ < Set.projIci (m x i) (m x f) ↔ m x i < m x f

The minimum-standard reading has the truth conditions of the comparative, the argument ending the event with more of the property than it began with ((27)).

theorem KennedyLevin2008.maxStandard_iff {α : Type u_1} {δ : Type u_2} {T : Type u_3} [LinearOrder δ] (m : α → T → δ) (x : α) (i f : T) [OrderTop δ] (h : m x i ≠ ⊤) :
Set.projIci (m x i) (m x f) = ⊤ ↔ m x f = ⊤

Unless the argument begins with the greatest degree, the maximum-standard reading holds exactly when it ends with that degree, as the positive form of the adjective requires ((27)).

theorem KennedyLevin2008.minStandard_of_maxStandard {α : Type u_1} {δ : Type u_2} {T : Type u_3} [LinearOrder δ] (m : α → T → δ) (x : α) (i f : T) [OrderTop δ] (h : m x i ≠ ⊤) (hmax : Set.projIci (m x i) (m x f) = ⊤) :
⊥ < Set.projIci (m x i) (m x f)

Unless the argument begins with the greatest degree, the telic reading entails the atelic one.

Measure phrases and degree modifiers (32)–(34) #

theorem KennedyLevin2008.minStandard_iff_describes_someAmount {α : Type u_1} {δ : Type u_2} {T : Type u_3} [AddCommGroup δ] [LinearOrder δ] [IsOrderedAddMonoid δ] (m : α → T → δ) (x : α) (i f : T) :
⊥ < Set.projIci (m x i) (m x f) ↔ HayKennedyLevin1999.Describes m x HayKennedyLevin1999.someAmount i f

The minimum-standard reading is the reading of [HKL99] with the difference value "some amount".

theorem KennedyLevin2008.maxStandard_iff_describes_completely {α : Type u_1} {δ : Type u_2} {T : Type u_3} [AddCommGroup δ] [LinearOrder δ] (m : α → T → δ) (x : α) (i f : T) {top : δ} (h : m x i < top) :
↑(Set.projIci (m x i) (m x f)) = top ↔ HayKennedyLevin1999.Describes m x (HayKennedyLevin1999.completely top (m x i)) i f

Against a maximal degree top above the initial degree, the maximum-standard reading, which completely also gives ((34a)), is the reading of [HKL99] with completely.

theorem KennedyLevin2008.slightly_iff_describes_slightly {α : Type u_1} {δ : Type u_2} {T : Type u_3} [AddCommGroup δ] [LinearOrder δ] [IsOrderedAddMonoid δ] (m : α → T → δ) (x : α) (i f : T) (s : ↑(Set.Ici (m x i))) :
⊥ < Set.projIci (m x i) (m x f) ∧ Set.projIci (m x i) (m x f) ≤ s ↔ HayKennedyLevin1999.Describes m x (HayKennedyLevin1999.slightly (↑s - m x i)) i f

Slightly, a positive change up to a small degree s ((34b)), is the reading of [HKL99] with slightly.

theorem KennedyLevin2008.measurePhrase_iff {α : Type u_1} {δ : Type u_2} {T : Type u_3} [AddCommGroup δ] [LinearOrder δ] [IsOrderedAddMonoid δ] (m : α → T → δ) (x : α) (i f : T) {n : δ} (hn : 0 < n) :
n ≤ ↑(Set.projIci (m x i) (m x f)) - m x i ↔ HayKennedyLevin1999.Describes m x (Set.Ici n) i f

For a positive degree n, the amount of change is at least n, as a measure phrase requires ((32)–(33)), exactly when the event is described by the difference values of at least n.

theorem KennedyLevin2008.le_of_describes_measurePhrase {α : Type u_1} {δ : Type u_2} {T : Type u_3} [AddCommGroup δ] [LinearOrder δ] [IsOrderedAddMonoid δ] (m : α → T → δ) (x : α) (i f : T) {n : δ} (hn : 0 < n) (h : HayKennedyLevin1999.Describes m x (HayKennedyLevin1999.measurePhrase n) i f) :
n ≤ ↑(Set.projIci (m x i) (m x f)) - m x i

The exact difference value that [HKL99] give a measure phrase entails the at-least reading.

The English degree achievements #

For any measure function into a dimension's degrees, a degree achievement on the dimension is by default an accomplishment when the preferred standard on the scale of its measure of change is the maximum, and an activity otherwise.

daVerbs lists the fragment's degree achievements.

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

    Every degree achievement's Vendler class is the default of its base scale.

    The adjective–verb pairs of the fragment are clean, dry, straight, flat and open with closed scales, and long, wide, cool and warm with open ones.

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

      A degree achievement measures on its adjective's scale.

      A degree achievement takes in X exactly when its scale is closed above, and for X otherwise ((1), (6)).

      On the fragment, bend, boil, clean, dry, straighten, flatten and open take in X, and rust, increase, lengthen, widen, cool and warm take for X.