Run times

[krifka-1989]

A clause denotes the set of intervals at which it holds, its run times (RunTimes). Statives denote a maximal interval with all its subintervals (stativeDenotation, a principal downset); accomplishments denote a singleton (accomplishmentDenotation); timeTrace projects an interval set to the time points it covers, and eventDenotation (Semantics/Events/Basic.lean) realises the patterns from neo-Davidsonian event predicates. The temporal-connective analyses that consume this carrier live in their studies (Anscombe1964, Karttunen1974, BeaverCondoravdi2003, Rett2020a, …).

@[reducible, inline]

abbrev Tense.RunTimes (T : Type u_2) [LinearOrder T] : Type u_2

A sentence denotes a set of temporal intervals — its "run-times".

Equations

• Tense.RunTimes T = Set (NonemptyInterval T)

def Tense.timeTrace {T : Type u_1} [LinearOrder T] (p : RunTimes T) : Set T

The time points contained in some interval of a denotation.

Equations

• Tense.timeTrace p = {t : T | ∃ i ∈ p, t ∈ i}

@[simp]

theorem Tense.mem_timeTrace {T : Type u_1} [LinearOrder T] {p : RunTimes T} {t : T} : t ∈ timeTrace p ↔ ∃ i ∈ p, t ∈ i

theorem Tense.timeTrace_image {T : Type u_1} [LinearOrder T] {α : Type u_2} (f : α → NonemptyInterval T) (s : Set α) : timeTrace (f '' s) = {t : T | ∃ a ∈ s, t ∈ f a}

@[simp]

theorem Tense.timeTrace_empty {T : Type u_1} [LinearOrder T] : timeTrace ∅ = ∅

@[simp]

theorem Tense.timeTrace_singleton {T : Type u_1} [LinearOrder T] (i : NonemptyInterval T) : timeTrace {i} = ↑i

@[simp]

theorem Tense.timeTrace_insert {T : Type u_1} [LinearOrder T] (i : NonemptyInterval T) (p : RunTimes T) : timeTrace (insert i p) = ↑i ∪ timeTrace p

theorem Tense.mem_timeTrace_pure {T : Type u_1} [LinearOrder T] {a t : T} : t ∈ timeTrace {NonemptyInterval.pure a} ↔ t = a

def Tense.stativeDenotation {T : Type u_1} [LinearOrder T] (i : NonemptyInterval T) : RunTimes T

Stative denotation: the maximal interval i with all its subintervals — the principal downset Set.Iic i, a lower set, which is the subinterval-closure property. The activity case (a minimal-parts floor: a single step is not "running") is the stratified reference of Aspect/Stratified ([champollion-2017]), not this lower set.

Equations

• Tense.stativeDenotation i = Set.Iic i

def Tense.accomplishmentDenotation {T : Type u_1} [LinearOrder T] (i : NonemptyInterval T) : RunTimes T

Accomplishment denotation: exactly the singleton {i} — quantization.

Equations

• Tense.accomplishmentDenotation i = {i}

theorem Tense.stativeDenotation_self {T : Type u_1} [LinearOrder T] (i : NonemptyInterval T) : i ∈ stativeDenotation i

theorem Tense.timeTrace_stativeDenotation {T : Type u_1} [LinearOrder T] (i : NonemptyInterval T) : timeTrace (stativeDenotation i) = {t : T | t ∈ i}

theorem Tense.mem_timeTrace_stativeDenotation {T : Type u_1} [LinearOrder T] {i : NonemptyInterval T} {t : T} : t ∈ timeTrace (stativeDenotation i) ↔ t ∈ i

theorem Tense.timeTrace_accomplishmentDenotation {T : Type u_1} [LinearOrder T] (i : NonemptyInterval T) : timeTrace (accomplishmentDenotation i) = {t : T | t ∈ i}

theorem Tense.timeTrace_eventDenotation {T : Type u_1} [LinearOrder T] (P : Event T → Prop) : timeTrace (eventDenotation P) = {t : T | ∃ (e : Event T), P e ∧ t ∈ e.τ}

theorem Tense.eventDenotation_singleton {T : Type u_1} [LinearOrder T] (e₀ : Event T) : (eventDenotation fun (e : Event T) => e = e₀) = accomplishmentDenotation e₀.τ

theorem Tense.eventDenotation_sub_stative {T : Type u_1} [LinearOrder T] (i : NonemptyInterval T) (P : Event T → Prop) (hP : ∀ (e : Event T), P e → e.τ ≤ i) : eventDenotation P ⊆ stativeDenotation i