Krifka (1998): The Origins of Telicity

Krifka treats telicity as a property of event predicates: a predicate is telic when no event it applies to has a proper part it also applies to that starts or ends at a different time (Aspect.IsTelic). For verbs of consumption and creation telicity follows from the transfer of part structure between object and event that a strictly incremental thematic relation performs, and for verbs of movement it follows from expansion, adjacency, and the source and goal of the path. Quantized predicates are telic but not conversely, and cumulative predicates that apply to two non-contemporaneous events are atelic.

Main results

• eat_apples_cum, eat_two_apples_qua: on a model of eat, eat apples is cumulative and eat two apples is quantized.
• isTelic_vp_of_seinc: expansion with mapping to objects makes the verb phrase of a quantized object telic.
• isTelic_sourceGoal: a movement with a specified source and goal is telic.
• Reading.not_isTelic_read: incrementality does not guarantee telicity, since re-reading the end of an article gives a reading with a non-final part that is also a reading.
• Movement: the paper's movement diagrams, checked against adjacency on a finite model.

Implementation notes

• The model of eat identifies an event with the apples it consumes, so its verb phrases are the object predicates themselves; the transfer from object to verb phrase is the general Aspect.vp_cum and Aspect.vp_qua.
• Temporal precedence is a parameter of the telicity notions. The paper's consequence of its event axioms that overlapping events never precede each other enters as NoPartPrecedes, which is all the proofs use.
• Overlap is Mereology.Overlap, relative to a possible null element. The paper's part structures have none, so the expansion theorems assume that the thematic relation never relates the null object.
• The source and goal conditions quantify the subpath and the subevent separately; the formalization ties them through the thematic relation, as the paper's telicity proof does.
• The measure adverbial (55) is formalized only through its part relation IsTemporalPart, without its presupposed universal clause over the parts of the witness e′.
• The strict-movement telicity claim of the paper does not follow from adjacency and mapping to objects alone (adjacency may be empty), and the tangentiality condition on sums of movements, the derived measure functions for movement and the changes in other dimensions are not formalized.
• In the finite model, the diagram's detour consists of the segments h and i; the paper's list of movements calls the second one j.

References

• [Kri98]

Measure adverbials

def Krifka1998.IsTemporalPart {β : Type u_2} {T : Type u_3} [PartialOrder β] [PartialOrder T] (τ : β → T) (e' e : β) : Prop

e' is a temporal part of e, in the part relation of a temporal measure (55), if it is part of e and e has a part whose runtime does not overlap the runtime of e'.

Equations

• Krifka1998.IsTemporalPart τ e' e = (e' ≤ e ∧ ∃ e'' ≤ e, ¬Mereology.Overlap (τ e') (τ e''))

theorem Krifka1998.IsTemporalPart.le {β : Type u_2} {T : Type u_3} [PartialOrder β] [PartialOrder T] {τ : β → T} {e' e : β} (h : IsTemporalPart τ e' e) : e' ≤ e

theorem Krifka1998.IsTemporalPart.ne {β : Type u_2} {T : Type u_3} [PartialOrder β] [PartialOrder T] {τ : β → T} {e' e : β} (hτ : Monotone τ) (h : IsTemporalPart τ e' e) (h₀ : ∀ e'' ≤ e, ¬IsBot (τ e'')) : e' ≠ e

A temporal part with a non-null runtime is a proper part.

Eating apples

def Krifka1998.eat (x e : Finset (Fin 3)) : Prop

In a model of eat with three apples, an eating event is identified with the apples it consumes.

Equations

• Krifka1998.eat x e = (x = e)

theorem Krifka1998.eat_sinc : Aspect.SINC eat

The object relation of eat is strictly incremental and summative, with unique participants.

theorem Krifka1998.eat_sum : Mereology.SUM eat

theorem Krifka1998.eat_up : Mereology.UP eat

theorem Krifka1998.eat_apples_cum : Mereology.CUM (Aspect.VP eat Finset.Nonempty)

eat apples is cumulative, since the bare plural is cumulative and eat is summative.

theorem Krifka1998.eat_two_apples_qua : Mereology.QUA (Aspect.VP eat fun (x : Finset (Fin 3)) => x.card = 2)

eat two apples is quantized, since a measure phrase is quantized and eat is strictly incremental.

theorem Krifka1998.qua_vp_eq {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (h : Aspect.SINC θ) (y : α) : Mereology.QUA (Aspect.VP θ fun (x : α) => x = y)

With a particular object, as in eat it, a strictly incremental verb phrase is quantized.

Incrementality without telicity (§3.6)

An article has two paragraphs, read by the events 0, 1 and 2, the last two both reading the second paragraph. A strict reading reads each paragraph of its object once, and read is the closure of strict reading under sums, which is incremental but lets the reader go back.

def Krifka1998.Reading.paragraph (i : Fin 3) : Fin 2

Event 0 reads the first paragraph, and events 1 and 2 both read the second.

Equations

• Krifka1998.Reading.paragraph i = if i = 0 then 0 else 1

def Krifka1998.Reading.readOnce (x : Finset (Fin 2)) (e : Finset (Fin 3)) : Prop

An event is a strict reading of some paragraphs if it reads each of them exactly once.

Equations

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

@[instance_reducible]

instance Krifka1998.Reading.instDecidableRelFinsetFinOfNatNatReadOnce : DecidableRel readOnce

Equations

• Krifka1998.Reading.instDecidableRelFinsetFinOfNatNatReadOnce x✝¹ x✝ = id inferInstance

theorem Krifka1998.Reading.readOnce_sinc : Aspect.SINC readOnce

def Krifka1998.Reading.read (x : Finset (Fin 2)) (e : Finset (Fin 3)) : Prop

Reading is the closure of strict reading under sums.

Equations

• Krifka1998.Reading.read x e = Mereology.AlgClosure (Function.uncurry Krifka1998.Reading.readOnce) (x, e)

theorem Krifka1998.Reading.read_inc : Aspect.INC read

def Krifka1998.Reading.precedes (a b : Finset (Fin 3)) : Prop

An event precedes another if all its times are earlier.

Equations

• Krifka1998.Reading.precedes a b = ∀ i ∈ a, ∀ j ∈ b, i < j

@[instance_reducible]

instance Krifka1998.Reading.instDecidableRelFinsetFinOfNatNatPrecedes : DecidableRel precedes

Equations

• Krifka1998.Reading.instDecidableRelFinsetFinOfNatNatPrecedes x✝¹ x✝ = id inferInstance

theorem Krifka1998.Reading.not_isTelic_read : ¬Aspect.IsTelic precedes (read Finset.univ)

Read the article is not telic, since the strict reading {0, 1} is a part of the reading {0, 1, 2} that the re-reading {2} follows.

Telicity by expansion

def Krifka1998.EXP {α : Type u_1} {β : Type u_2} [SemilatticeSup α] (precedes : β → β → Prop) (θ : α → β → Prop) : Prop

A relation is expansive if the objects of temporally ordered events do not overlap.

Equations

• Krifka1998.EXP precedes θ = ∀ (x y : α) (e e' : β), θ x e → θ y e' → precedes e e' → ¬Mereology.Overlap x y

def Krifka1998.SEINC {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (precedes : β → β → Prop) (θ : α → β → Prop) : Prop

A relation is strictly expansive incremental if it is expansive and maps to objects.

Equations

• Krifka1998.SEINC precedes θ = (Krifka1998.EXP precedes θ ∧ Mereology.MO θ)

theorem Krifka1998.isInitialPart_of_seinc {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {precedes : β → β → Prop} {θ : α → β → Prop} (h : SEINC precedes θ) (h₀ : ∀ (x : α) (e : β), θ x e → ¬IsBot x) {x : α} {e e' : β} (hx : θ x e) (hx' : θ x e') (hle : e' ≤ e) : Aspect.IsInitialPart precedes e' e

Under a strictly expansive incremental relation, an object's events are initial parts of each other.

theorem Krifka1998.isFinalPart_of_seinc {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {precedes : β → β → Prop} {θ : α → β → Prop} (h : SEINC precedes θ) (h₀ : ∀ (x : α) (e : β), θ x e → ¬IsBot x) {x : α} {e e' : β} (hx : θ x e) (hx' : θ x e') (hle : e' ≤ e) : Aspect.IsFinalPart precedes e' e

Under a strictly expansive incremental relation, an object's events are final parts of each other.

theorem Krifka1998.isTelic_of_seinc {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {precedes : β → β → Prop} {θ : α → β → Prop} (h : SEINC precedes θ) (h₀ : ∀ (x : α) (e : β), θ x e → ¬IsBot x) (x : α) : Aspect.IsTelic precedes (θ x)

The events of a fixed object under a strictly expansive incremental relation form a telic predicate.

theorem Krifka1998.isTelic_vp_of_seinc {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {precedes : β → β → Prop} {θ : α → β → Prop} (h : SEINC precedes θ) (h₀ : ∀ (x : α) (e : β), θ x e → ¬IsBot x) (hUP : Mereology.UP θ) {OBJ : α → Prop} (hOBJ : Mereology.QUA OBJ) : Aspect.IsTelic precedes (Aspect.VP θ OBJ)

The verb phrase of a quantized object under a strictly expansive incremental relation with unique participants is telic, as eat two apples is.

Movement relations

def Krifka1998.ADJ {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (adjα : α → α → Prop) (adjβ : β → β → Prop) (θ : α → β → Prop) : Prop

A relation has the adjacency property if two subevents of a movement are temporally adjacent iff their paths are spatially adjacent.

Equations

• Krifka1998.ADJ adjα adjβ θ = ∀ (x : α) (e : β) (y z : α) (e' e'' : β), θ x e → e' ≤ e → e'' ≤ e → y ≤ x → z ≤ x → θ y e' → θ z e'' → (adjβ e' e'' ↔ adjα y z)

def Krifka1998.SMR {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (adjα : α → α → Prop) (adjβ : β → β → Prop) (isPath : α → Prop) (θ : α → β → Prop) : Prop

A strict movement relation has the adjacency property, maps to objects, and takes paths as objects.

Equations

• Krifka1998.SMR adjα adjβ isPath θ = (Krifka1998.ADJ adjα adjβ θ ∧ Mereology.MO θ ∧ ∀ (x : α) (e : β), θ x e → isPath x)

inductive Krifka1998.PrecedenceClosure {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (precedes : β → β → Prop) (θ' : α → β → Prop) : α → β → Prop

The closure of a relation under sums of temporally ordered events.

• base {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {precedes : β → β → Prop} {θ' : α → β → Prop} {x : α} {e : β} : θ' x e → PrecedenceClosure precedes θ' x e
• sum {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {precedes : β → β → Prop} {θ' : α → β → Prop} {x₁ x₂ : α} {e₁ e₂ : β} : PrecedenceClosure precedes θ' x₁ e₁ → PrecedenceClosure precedes θ' x₂ e₂ → precedes e₁ e₂ → PrecedenceClosure precedes θ' (x₁ ⊔ x₂) (e₁ ⊔ e₂)

def Krifka1998.MR {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (adjα : α → α → Prop) (adjβ precedes : β → β → Prop) (isPath : α → Prop) (θ : α → β → Prop) : Prop

A movement relation (71) is the closure of a strict movement relation under sums of temporally ordered events.

Equations

• Krifka1998.MR adjα adjβ precedes isPath θ = ∃ (θ' : α → β → Prop), Krifka1998.SMR adjα adjβ isPath θ' ∧ ∀ (x : α) (e : β), θ x e ↔ Krifka1998.PrecedenceClosure precedes θ' x e

def Krifka1998.Source {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (adjα : α → α → Prop) (precedes : β → β → Prop) (θ : α → β → Prop) (y x : α) (e : β) : Prop

The subpaths of a movement adjacent to y are the paths of its initial parts.

Equations

• Krifka1998.Source adjα precedes θ y x e = ∀ (x' : α) (e' : β), θ x' e' → x' ≤ x → e' ≤ e → (adjα x' y ↔ Aspect.IsInitialPart precedes e' e)

def Krifka1998.Goal {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (adjα : α → α → Prop) (precedes : β → β → Prop) (θ : α → β → Prop) (y x : α) (e : β) : Prop

The subpaths of a movement adjacent to y are the paths of its final parts.

Equations

• Krifka1998.Goal adjα precedes θ y x e = ∀ (x' : α) (e' : β), θ x' e' → x' ≤ x → e' ≤ e → (adjα x' y ↔ Aspect.IsFinalPart precedes e' e)

theorem Krifka1998.mr_of_smr {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {adjα : α → α → Prop} {adjβ precedes : β → β → Prop} {isPath : α → Prop} {θ : α → β → Prop} (h : SMR adjα adjβ isPath θ) (hClosed : ∀ (x₁ x₂ : α) (e₁ e₂ : β), θ x₁ e₁ → θ x₂ e₂ → precedes e₁ e₂ → θ (x₁ ⊔ x₂) (e₁ ⊔ e₂)) : MR adjα adjβ precedes isPath θ

A strict movement relation closed under sums of temporally ordered events is a movement relation.

theorem Krifka1998.isTelic_sourceGoal {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {adjα : α → α → Prop} {precedes : β → β → Prop} {θ : α → β → Prop} (hax : Aspect.NoPartPrecedes precedes) (hMO : Mereology.MO θ) (hUP : Mereology.UP θ) (u v : α) : Aspect.IsTelic precedes fun (e : β) => ∃ (x : α), θ x e ∧ Source adjα precedes θ u x e ∧ Goal adjα precedes θ v x e

A movement with a specified source and goal is telic under mapping to objects and uniqueness of participants, as walk from the university to the capitol is.

The movement diagrams

inductive Krifka1998.Seg : Type

The path segments of the paper's diagram run from a to g in a line, with h and i a detour from c to f.

• a : Seg
• b : Seg
• c : Seg
• d : Seg
• e : Seg
• f : Seg
• g : Seg
• h : Seg
• i : Seg

@[instance_reducible]

instance Krifka1998.instDecidableEqSeg : DecidableEq Seg

Equations

• Krifka1998.instDecidableEqSeg x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Krifka1998.Seg.edges : List (Seg × Seg)

The adjacent pairs of segments.

Equations

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

def Krifka1998.Seg.adj (s t : Seg) : Prop

Adjacency of segments.

Equations

• s.adj t = ((s, t) ∈ Krifka1998.Seg.edges ∨ (t, s) ∈ Krifka1998.Seg.edges)

@[instance_reducible]

instance Krifka1998.instDecidableAdj (s t : Seg) : Decidable (s.adj t)

Equations

• Krifka1998.instDecidableAdj s t = id inferInstance

def Krifka1998.pathAdj (x y : Finset Seg) : Prop

Two paths are adjacent if they are disjoint and have an adjacent pair of segments.

Equations

• Krifka1998.pathAdj x y = (Disjoint x y ∧ ∃ s ∈ x, ∃ t ∈ y, s.adj t)

def Krifka1998.eventAdj (e e' : Finset (Fin 7)) : Prop

Two events are adjacent if they are disjoint and have a consecutive pair of times.

Equations

• Krifka1998.eventAdj e e' = (Disjoint e e' ∧ ∃ i ∈ e, ∃ j ∈ e', ↑i + 1 = ↑j ∨ ↑j + 1 = ↑i)

@[instance_reducible]

instance Krifka1998.instDecidablePathAdj (x y : Finset Seg) : Decidable (pathAdj x y)

Equations

• Krifka1998.instDecidablePathAdj x y = id inferInstance

@[instance_reducible]

instance Krifka1998.instDecidableEventAdj (e e' : Finset (Fin 7)) : Decidable (eventAdj e e')

Equations

• Krifka1998.instDecidableEventAdj e e' = id inferInstance

def Krifka1998.support (L : List (Seg × Fin 7)) : List (Finset Seg × Finset (Fin 7))

A diagram relates its atomic movements and the whole movement.

Equations

• Krifka1998.support L = List.map (fun (p : Krifka1998.Seg × Fin 7) => ({p.1}, {p.2})) L ++ [((List.map Prod.fst L).toFinset, (List.map Prod.snd L).toFinset)]

def Krifka1998.Movement (L : List (Seg × Fin 7)) (x : Finset Seg) (e : Finset (Fin 7)) : Prop

The movement relation a diagram depicts.

Equations

• Krifka1998.Movement L x e = ((x, e) ∈ Krifka1998.support L)

@[instance_reducible]

instance Krifka1998.instDecidableMovement (L : List (Seg × Fin 7)) (x : Finset Seg) (e : Finset (Fin 7)) : Decidable (Movement L x e)

Equations

• Krifka1998.instDecidableMovement L x e = id inferInstance

def Krifka1998.walk : List (Seg × Fin 7)

A walk along a to f.

Equations

• Krifka1998.walk = [(Krifka1998.Seg.a, 0), (Krifka1998.Seg.b, 1), (Krifka1998.Seg.c, 2), (Krifka1998.Seg.d, 3), (Krifka1998.Seg.e, 4), (Krifka1998.Seg.f, 5)]

def Krifka1998.stopAndGo : List (Seg × Fin 7)

A stop-and-go movement pauses between c and d.

Equations

• Krifka1998.stopAndGo = [(Krifka1998.Seg.a, 0), (Krifka1998.Seg.b, 1), (Krifka1998.Seg.c, 2), (Krifka1998.Seg.d, 4), (Krifka1998.Seg.e, 5), (Krifka1998.Seg.f, 6)]

def Krifka1998.telekinesis : List (Seg × Fin 7)

Telekinesis moves from b straight to e.

Equations

• Krifka1998.telekinesis = [(Krifka1998.Seg.a, 0), (Krifka1998.Seg.b, 1), (Krifka1998.Seg.e, 2), (Krifka1998.Seg.f, 3)]

def Krifka1998.echternach : List (Seg × Fin 7)

An Echternach movement returns along c and b.

Equations

• Krifka1998.echternach = [(Krifka1998.Seg.a, 0), (Krifka1998.Seg.b, 1), (Krifka1998.Seg.c, 2), (Krifka1998.Seg.c, 3), (Krifka1998.Seg.b, 4)]

def Krifka1998.alcatraz : List (Seg × Fin 7)

An Alcatraz movement goes around the circle c, d, e, f, i, h.

Equations

• Krifka1998.alcatraz = [(Krifka1998.Seg.c, 0), (Krifka1998.Seg.d, 1), (Krifka1998.Seg.e, 2), (Krifka1998.Seg.f, 3), (Krifka1998.Seg.i, 4), (Krifka1998.Seg.h, 5)]

def Krifka1998.disconnected : List (Seg × Fin 7)

A movement along a disconnected path.

Equations

• Krifka1998.disconnected = [(Krifka1998.Seg.a, 0), (Krifka1998.Seg.b, 1), (Krifka1998.Seg.e, 4), (Krifka1998.Seg.f, 5)]

theorem Krifka1998.adj_walk : ADJ pathAdj eventAdj (Movement walk)

theorem Krifka1998.not_adj_stopAndGo : ¬ADJ pathAdj eventAdj (Movement stopAndGo)

theorem Krifka1998.not_adj_telekinesis : ¬ADJ pathAdj eventAdj (Movement telekinesis)

theorem Krifka1998.not_adj_echternach : ¬ADJ pathAdj eventAdj (Movement echternach)

theorem Krifka1998.not_adj_alcatraz : ¬ADJ pathAdj eventAdj (Movement alcatraz)

def Krifka1998.Connected (x : Finset Seg) : Prop

A set of segments is connected if no proper nonempty subset is closed under adjacency.

Equations

• Krifka1998.Connected x = ∀ y ∈ x.powerset, y.Nonempty → y ≠ x → ∃ s ∈ y, ∃ t ∈ x \ y, s.adj t

theorem Krifka1998.adj_disconnected : ADJ pathAdj eventAdj (Movement disconnected) ∧ ¬Connected {Seg.a, Seg.b, Seg.e, Seg.f}

The disconnected movement satisfies adjacency but its path is not connected.