Telicity

Krifka treats telicity as a property of event predicates: a predicate is telic when every part of one of its events that it also applies to is both an initial and a final part of that event. Quantized predicates are telic though not conversely, and cumulative or divisive predicates that apply to events with successive parts are not. Telicity originates in the thematic relation. A relation is strictly incremental when the parts of the object and of the event correspond one to one, as for the object of eat, and incremental when it is the closure of such a relation under sums, which admits the backups of read the article. The reference properties of the object carry over to the verb phrase: cumulativity along a summative relation, and quantization along a relation with unique participants that maps to subobjects. For a thematic function these are a sum homomorphism and an injective one, so drink milk is cumulative and drink two liters of milk quantized.

Main definitions

• IsTelic: every part of an event of the predicate that the predicate applies to is an initial and a final part of it.
• SINC, INC: strict incrementality and incrementality of a thematic relation.
• Incrementality.Holds: the property an incrementality class of Aspect/Defs.lean names.
• VP: the verb phrase of a relation and an object predicate.

Main results

• isTelic_of_qua, exists_isTelic_not_qua: quantized predicates are telic, not conversely.
• not_isTelic_of_cum, not_isTelic_of_div: cumulative and divisive predicates with successive events or parts are not telic.
• SINC.inc_of_sum, INC.sum: a summative strictly incremental relation is incremental, and an incremental relation is summative.
• vp_cum, vp_qua: cumulativity and quantization carry over from the object to the verb phrase; vp_cum_graph and vp_qua_graph are the cases of a thematic function.

Implementation notes

Temporal precedence is a parameter of the telicity notions. The proofs use only that parts of an event neither precede nor follow it, NoPartPrecedes, which follows from Krifka's axiom that overlapping events do not precede each other (noPartPrecedes_of_overlap). A final part is an initial part under the converse precedence, so results about final parts are transported.

References

• [Kri89], [Kri98], [CK16]

Telicity by initial and final parts

def Aspect.IsInitialPart {β : Type u_1} [PartialOrder β] (precedes : β → β → Prop) (e' e : β) : Prop

An initial part of an event is a part that no part of the event precedes.

Equations

• Aspect.IsInitialPart precedes e' e = (e' ≤ e ∧ ¬∃ e'' ≤ e, precedes e'' e')

@[reducible, inline]

abbrev Aspect.IsFinalPart {β : Type u_1} [PartialOrder β] (precedes : β → β → Prop) (e' e : β) : Prop

A final part of an event is a part that no part of the event follows, an initial part under the converse precedence.

Equations

• Aspect.IsFinalPart precedes e' e = Aspect.IsInitialPart (flip precedes) e' e

def Aspect.IsTelic {β : Type u_1} [PartialOrder β] (precedes : β → β → Prop) (P : β → Prop) : Prop

A predicate is telic when every P-part of a P-event is an initial and a final part of it.

Equations

• Aspect.IsTelic precedes P = ∀ (e e' : β), P e → P e' → e' ≤ e → Aspect.IsInitialPart precedes e' e ∧ Aspect.IsFinalPart precedes e' e

def Aspect.NoPartPrecedes {β : Type u_1} [PartialOrder β] (precedes : β → β → Prop) : Prop

Parts of an event neither precede nor follow it.

Equations

• Aspect.NoPartPrecedes precedes = ∀ (a b : β), a ≤ b → ¬precedes a b ∧ ¬precedes b a

theorem Aspect.NoPartPrecedes.flip {β : Type u_1} [PartialOrder β] {precedes : β → β → Prop} (h : NoPartPrecedes precedes) : NoPartPrecedes (_root_.flip precedes)

theorem Aspect.noPartPrecedes_of_overlap {β : Type u_1} [PartialOrder β] {precedes : β → β → Prop} [NoBotOrder β] (h : ∀ (a b : β), Mereology.Overlap a b → ¬precedes a b) : NoPartPrecedes precedes

Parts of an event neither precede nor follow it if overlapping events do not precede each other ([Kri98] (35)) and no event is null.

theorem Aspect.isInitialPart_self {β : Type u_1} [PartialOrder β] {precedes : β → β → Prop} (h : NoPartPrecedes precedes) (e : β) : IsInitialPart precedes e e

theorem Aspect.isFinalPart_self {β : Type u_1} [PartialOrder β] {precedes : β → β → Prop} (h : NoPartPrecedes precedes) (e : β) : IsFinalPart precedes e e

theorem Aspect.IsTelic.flip {β : Type u_1} [PartialOrder β] {precedes : β → β → Prop} {P : β → Prop} (h : IsTelic precedes P) : IsTelic (_root_.flip precedes) P

A predicate telic for a precedence is telic for its converse.

theorem Aspect.isTelic_of_qua {β : Type u_1} [PartialOrder β] {precedes : β → β → Prop} (h : NoPartPrecedes precedes) {P : β → Prop} (hP : Mereology.QUA P) : IsTelic precedes P

Quantized predicates are telic.

theorem Aspect.isTelic_of_not_precedes {β : Type u_1} [PartialOrder β] {precedes : β → β → Prop} (h : ∀ (a b : β), ¬precedes a b) (P : β → Prop) : IsTelic precedes P

Among contemporaneous events every predicate is telic.

theorem Aspect.exists_isTelic_not_qua : ∃ (P : Bool → Prop), IsTelic (fun (x x_1 : Bool) => False) P ∧ ¬Mereology.QUA P

A telic predicate need not be quantized, as the predicate true of every event running from three to four is not on two such events one part of the other.

theorem Aspect.not_isTelic_of_cum {β : Type u_1} [SemilatticeSup β] {precedes : β → β → Prop} {P : β → Prop} (hP : Mereology.CUM P) {e e' e'' : β} (he : P e) (he' : P e') (h'' : e'' ≤ e) (hp : precedes e' e'') : ¬IsTelic precedes P

A cumulative predicate true of two events, a part of one following the other, is not telic.

theorem Aspect.not_isTelic_of_div {β : Type u_1} [PartialOrder β] {precedes : β → β → Prop} {P : β → Prop} (hP : Mereology.DIV P) {e e' e'' : β} (he : P e) (h' : e' ≤ e) (h'' : e'' ≤ e) (hp : precedes e' e'') : ¬IsTelic precedes P

A divisive predicate true of an event with a part preceding another part is not telic, as the divisive reference of activities makes them atelic ([CK16]).

Incremental relations

structure Aspect.SINC {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) : Prop

A relation is strictly incremental when a part of a related object is related to exactly one part of the event and conversely, and some related pair has related proper parts, so the relation is not confined to atoms.

• ue : Mereology.UE θ
• uo : Mereology.UO θ
• extended : ∃ (x : α) (y : α) (e : β) (e' : β), y < x ∧ e' < e ∧ θ x e ∧ θ y e'

  Some related pair has related proper parts.

theorem Aspect.SINC.mse {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (h : SINC θ) : Mereology.MSE θ

theorem Aspect.SINC.mso {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (h : SINC θ) : Mereology.MSO θ

theorem Aspect.SINC.me {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (h : SINC θ) : Mereology.ME θ

theorem Aspect.SINC.mo {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (h : SINC θ) : Mereology.MO θ

def Aspect.INC {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) : Prop

A relation is incremental when it is the closure of some strictly incremental relation under sums.

Equations

• Aspect.INC θ = ∃ (θ' : α → β → Prop), Aspect.SINC θ' ∧ ∀ (x : α) (e : β), θ x e ↔ Mereology.AlgClosure (Function.uncurry θ') (x, e)

theorem Aspect.SINC.inc_of_sum {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (h : SINC θ) (hs : Mereology.SUM θ) : INC θ

A summative strictly incremental relation is incremental, being its own closure.

theorem Aspect.INC.sum {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (h : INC θ) : Mereology.SUM θ

An incremental relation is summative, being a closure under sums.

def Aspect.Incrementality.Holds {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] : Incrementality → (α → β → Prop) → Prop

The property of a thematic relation that an incrementality class names. A verb is classed by the strongest that its theme relation has.

Equations

• Aspect.Incrementality.strict.Holds x✝ = Aspect.SINC x✝
• Aspect.Incrementality.incremental.Holds x✝ = Aspect.INC x✝
• Aspect.Incrementality.cumulative.Holds x✝ = Mereology.SUM x✝

theorem Aspect.Incrementality.Holds.cumulative {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (h : Incrementality.incremental.Holds θ) : Incrementality.cumulative.Holds θ

The incremental class is included in the cumulative one.

theorem Aspect.Incrementality.Holds.incremental {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (h : strict.Holds θ) (hs : Mereology.SUM θ) : Incrementality.incremental.Holds θ

A summative relation of the strict class is of the incremental class.

The verb phrase

def Aspect.VP {α : Type u_1} {β : Type u_2} (θ : α → β → Prop) (OBJ : α → Prop) : β → Prop

The verb phrase of a relation and an object predicate holds of the events with some object of the predicate.

Equations

• Aspect.VP θ OBJ e = ∃ (y : α), OBJ y ∧ θ y e

theorem Aspect.vp_cum {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} {OBJ : α → Prop} (hθ : Mereology.SUM θ) (hObj : Mereology.CUM OBJ) : Mereology.CUM (VP θ OBJ)

A summative relation carries cumulativity from the object to the verb phrase.

theorem Aspect.vp_qua {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} {OBJ : α → Prop} (hU : Mereology.UP θ) (hm : Mereology.MSO θ) (hObj : Mereology.QUA OBJ) : Mereology.QUA (VP θ OBJ)

Uniqueness of participants and mapping to subobjects carry quantization from the object to the verb phrase, since the object of a proper subevent is a proper part of the object.

theorem Aspect.vp_eq {α : Type u_1} {β : Type u_2} (θ : α → β → Prop) (y : α) : (VP θ fun (x : α) => x = y) = θ y

The verb phrase of a particular object is the object's event predicate.

theorem Aspect.vp_graph {α : Type u_1} {β : Type u_2} (f : β → α) (OBJ : α → Prop) : VP (fun (x1 : α) (x2 : β) => x1 = f x2) OBJ = OBJ ∘ f

The verb phrase along a thematic function is the object predicate pulled back along it.

theorem Aspect.vp_cum_graph {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {OBJ : α → Prop} {F : Type u_3} [FunLike F β α] [SupHomClass F β α] (f : F) (hObj : Mereology.CUM OBJ) : Mereology.CUM (VP (fun (x1 : α) (x2 : β) => x1 = f x2) OBJ)

A cumulative object predicate along a sum homomorphism gives a cumulative verb phrase, so drink milk is cumulative ([CK16]).

theorem Aspect.vp_qua_graph {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {OBJ : α → Prop} {F : Type u_3} [FunLike F β α] [SupHomClass F β α] (f : F) (hf : Function.Injective ⇑f) (hObj : Mereology.QUA OBJ) : Mereology.QUA (VP (fun (x1 : α) (x2 : β) => x1 = f x2) OBJ)

A quantized object predicate along an injective sum homomorphism gives a quantized verb phrase, so drink two liters of milk is quantized ([CK16]). The homomorphism places the participant of a proper subevent below the whole participant, and injectivity makes it a proper part.