Beavers (2011): On Affectedness

This file formalizes Beavers's analysis of affectedness as specificity about scalar change. A predicate relates its theme to a scale, and how strongly it affects the theme is how much it says about where the theme ends up on that scale. Change is an increase from a contextually given source to a later goal, following Hay, Kennedy and Levin, so the soup cooled 5 degrees effects a quantized change, the soup cooled a non-quantized one, and both entail that the soup changed. The telic reading that Kennedy and Levin derive for a degree achievement on a scale closed above is a quantized change to the maximum, and the atelic reading a non-quantized change.

Each degree of affectedness is an existential generalization of the one above it, so the entailments a predicate has about its theme form one of four sets. These are exactly the four contentful thematic roles of patienthood in Beavers's earlier work, each the entailment set of some predicate.

Implementation notes

• A scale s indexes a measure function m s. An event's result on s is where its theme ends, provided the theme started at the contextual source b and ended higher, which is SOURCE and GOAL (48) with the increase of (43).
• The goal of the measure-phrase reading is b + n, fixed only relative to the contextual source, whereas Beavers's exemplars of quantized change such as break have a lexical goal.
• Hay, Kennedy and Levin judge broaden the investigation significantly telic, since its difference value has a lower bound (HayKennedyLevin1999.isBounded_significantly). A lower-bounded change is non-quantized, and the diagnostics of (63) count only quantized change as telic. The two papers define telicity differently, as a bounded difference value and as a predicate that describes no proper part of its events.

TODO

• Derive the telicity of quantized change, the first row of (63), from the Figure/Path Relation (53), with scales as Krifka's paths (Krifka1998.isTelic_sourceGoal).
• The remaining diagnostics of (63)–(66) and the result-phrase data of §5.

References

• J. Beavers, On Affectedness (2011)
• J. Hay, C. Kennedy and B. Levin, Scalar Structure Underlies Telicity in “Degree Achievements” (1999)
• C. Kennedy and B. Levin, Measure of Change: The Adjectival Core of Degree Achievements (2008)
• J. Beavers, The structure of lexical meaning: Why semantics really matters (2010)

Scalar change (§4.1)

def Beavers2011.Result {α : Type u_1} {S : Type u_2} {D : Type u_3} {T : Type u_4} {E : Type u_5} [LinearOrder T] [Event.TemporalTrace E T] [LinearOrder D] (m : S → α → T → D) (b : D) (x : α) (s : S) (g : D) (e : E) : Prop

Result m b x s g e holds when the theme x starts the event e at the contextual source b on the scale s and ends it at the higher goal g, the result relation of (48).

Equations

• Beavers2011.Result m b x s g e = (m s x (Event.τ e).toProd.1 = b ∧ b < g ∧ m s x (Event.τ e).toProd.2 = g)

theorem Beavers2011.exists_lt_of_nonQuantizedChange {α : Type u_1} {S : Type u_2} {D : Type u_3} {T : Type u_4} {E : Type u_5} [LinearOrder T] [Event.TemporalTrace E T] [LinearOrder D] {m : S → α → T → D} {b : D} {θ : α → S → E → Prop} {φ : α → E → Prop} (h : ArgumentStructure.NonQuantizedChange θ (Result m b) φ) {x : α} {e : E} (hx : φ x e) : ∃ (s : S), θ x s e ∧ m s x (Event.τ e).toProd.1 < m s x (Event.τ e).toProd.2

A non-quantized change entails that the theme ends the event with more of the property than it began with, so that the soup cooled 5 degrees, but nothing is different about it is contradictory ((59)).

theorem Beavers2011.snd_eq_of_quantizedChange {α : Type u_1} {S : Type u_2} {D : Type u_3} {T : Type u_4} {E : Type u_5} [LinearOrder T] [Event.TemporalTrace E T] [LinearOrder D] {m : S → α → T → D} {b : D} {θ : α → S → E → Prop} {φ : α → E → Prop} {s₀ : S} {g : D} (hθ : ∀ (x : α) (s : S) (e : E), θ x s e → s = s₀) (h : ArgumentStructure.QuantizedChange θ (Result m b) φ g) {x : α} {e : E} (hx : φ x e) : m s₀ x (Event.τ e).toProd.2 = g

On a predicate whose only scale is s₀, a quantized change to g ends every event at g.

theorem Beavers2011.not_quantizedChange_of_snd_ne {α : Type u_1} {S : Type u_2} {D : Type u_3} {T : Type u_4} {E : Type u_5} [LinearOrder T] [Event.TemporalTrace E T] [LinearOrder D] {m : S → α → T → D} {b : D} {θ : α → S → E → Prop} {φ : α → E → Prop} {s₀ : S} (hθ : ∀ (x : α) (s : S) (e : E), θ x s e → s = s₀) {x x' : α} {e e' : E} (hx : φ x e) (hx' : φ x' e') (hne : m s₀ x (Event.τ e).toProd.2 ≠ m s₀ x' (Event.τ e').toProd.2) : ¬∃ (g : D), ArgumentStructure.QuantizedChange θ (Result m b) φ g

A predicate on the single scale s₀ with two events that end at different goals effects no quantized change, since a quantized change fixes one goal for all its events (p. 357).

Quantized and non-quantized change as difference values ((58))

theorem Beavers2011.quantizedChange_iff_describes_measurePhrase {α : Type u_1} {S : Type u_2} {D : Type u_3} {T : Type u_4} {E : Type u_5} [LinearOrder T] [Event.TemporalTrace E T] [AddCommGroup D] [LinearOrder D] [IsOrderedAddMonoid D] {m : S → α → T → D} {b : D} {s₀ : S} {φ : α → E → Prop} {n : D} (hn : 0 < n) : ArgumentStructure.QuantizedChange (fun (x : α) (s : S) (x_1 : E) => s = s₀) (Result m b) φ (b + n) ↔ ∀ (x : α) (e : E), φ x e → m s₀ x (Event.τ e).toProd.1 = b ∧ HayKennedyLevin1999.Describes (m s₀) x (HayKennedyLevin1999.measurePhrase n) (Event.τ e).toProd.1 (Event.τ e).toProd.2

On a predicate whose scale is s₀, a quantized change to b + n for a positive n is the reading of [HKL99] with the measure phrase n from the source b, as in the soup cooled 5 degrees ((58a)).

theorem Beavers2011.nonQuantizedChange_iff_describes_someAmount {α : Type u_1} {S : Type u_2} {D : Type u_3} {T : Type u_4} {E : Type u_5} [LinearOrder T] [Event.TemporalTrace E T] [AddCommGroup D] [LinearOrder D] [IsOrderedAddMonoid D] {m : S → α → T → D} {b : D} {s₀ : S} {φ : α → E → Prop} : ArgumentStructure.NonQuantizedChange (fun (x : α) (s : S) (x_1 : E) => s = s₀) (Result m b) φ ↔ ∀ (x : α) (e : E), φ x e → m s₀ x (Event.τ e).toProd.1 = b ∧ HayKennedyLevin1999.Describes (m s₀) x HayKennedyLevin1999.someAmount (Event.τ e).toProd.1 (Event.τ e).toProd.2

On a predicate whose scale is s₀, a non-quantized change is the reading of [HKL99] with the difference value "some amount" from the source b, as in the soup cooled ((58b)).

Degree achievements ((60a), (60b))

theorem Beavers2011.quantizedChange_top_of_maxStandard {α : Type u_1} {S : Type u_2} {D : Type u_3} {T : Type u_4} {E : Type u_5} [LinearOrder T] [Event.TemporalTrace E T] [LinearOrder D] {m : S → α → T → D} {b : D} {s₀ : S} {φ : α → E → Prop} [OrderTop D] (hb : b ≠ ⊤) (h : ∀ (x : α) (e : E), φ x e → m s₀ x (Event.τ e).toProd.1 = b ∧ Set.projIci (m s₀ x (Event.τ e).toProd.1) (m s₀ x (Event.τ e).toProd.2) = ⊤) : ArgumentStructure.QuantizedChange (fun (x : α) (s : S) (x_1 : E) => s = s₀) (Result m b) φ ⊤

From a source below the maximum, the telic reading of a degree achievement on a scale closed above, on which the theme reaches the maximum ([KL08]), is a quantized change to ⊤, as for straighten.

theorem Beavers2011.nonQuantizedChange_of_minStandard {α : Type u_1} {S : Type u_2} {D : Type u_3} {T : Type u_4} {E : Type u_5} [LinearOrder T] [Event.TemporalTrace E T] [LinearOrder D] {m : S → α → T → D} {b : D} {s₀ : S} {φ : α → E → Prop} (h : ∀ (x : α) (e : E), φ x e → m s₀ x (Event.τ e).toProd.1 = b ∧ ⊥ < Set.projIci (m s₀ x (Event.τ e).toProd.1) (m s₀ x (Event.τ e).toProd.2)) : ArgumentStructure.NonQuantizedChange (fun (x : α) (s : S) (x_1 : E) => s = s₀) (Result m b) φ

The atelic reading of a degree achievement, on which the theme ends above where it began ([KL08]), is a non-quantized change, as for widen or cool.

The contentful roles of [Bea10]

def Beavers2011.role {α : Type u_6} {S : Type u_7} {G : Type u_8} {β : Type u_9} (θ : α → S → β → Prop) (R : α → S → G → β → Prop) (φ : α → β → Prop) : Set ArgumentStructure.AffectednessEntailment

The patient role of a predicate is the set of affectedness entailments it has about its theme ([Bea10] (65)).

Equations

• Beavers2011.role θ R φ = {e : ArgumentStructure.AffectednessEntailment | ArgumentStructure.AffectednessDegree.Holds θ R φ ↑e}

theorem Beavers2011.isLowerSet_role {α : Type u_6} {S : Type u_7} {G : Type u_8} {β : Type u_9} {θ : α → S → β → Prop} {R : α → S → G → β → Prop} {φ : α → β → Prop} : IsLowerSet (role θ R φ)

Every predicate's role is contentful, closed under entailment, since each degree entails the weaker ones ([Bea10] (67)).

theorem Beavers2011.role_eq_entailments_iff {α : Type u_6} {S : Type u_7} {G : Type u_8} {β : Type u_9} {θ : α → S → β → Prop} {R : α → S → G → β → Prop} {φ : α → β → Prop} {d : ArgumentStructure.AffectednessDegree} : role θ R φ = ↑(ArgumentStructure.AffectednessDegree.entailments d) ↔ ∀ (e : ArgumentStructure.AffectednessEntailment), ArgumentStructure.AffectednessDegree.Holds θ R φ ↑e ↔ ↑e ≤ d

A predicate has the role that [Bea10] names by the degree d exactly when its entailments are those at most as strong as d.

theorem Beavers2011.exists_role_eq_iff (s : Set ArgumentStructure.AffectednessEntailment) : (∃ (θ : Unit → Unit → Bool → Prop) (R : Unit → Unit → Bool → Bool → Prop) (φ : Unit → Bool → Prop), role θ R φ = s) ↔ IsLowerSet s

A set of affectedness entailments is the role of some predicate exactly when it is contentful, as the objects of see, hit, cut and eat illustrate ([Bea10] (66)–(67)).