Sentence denotations as run-time interval sets

[Kri89]

A sentence denotes the set of its run-time intervals (SentDenotation). 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, Rett2020, …).

@[reducible, inline]

abbrev Tense.SentDenotation (Time : Type u_2) [LinearOrder Time] : Type u_2

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

Equations

• Tense.SentDenotation Time = Set (NonemptyInterval Time)

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

The time points contained in some interval of a denotation.

Equations

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

@[simp]

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

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

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

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 ([Cha17]), not this lower set.

Equations

• Tense.stativeDenotation i = Set.Iic i

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

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

Equations

• Tense.accomplishmentDenotation i = {i}

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

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

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

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

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

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