Temporal Connective Infrastructure

@cite{allen-1983} @cite{krifka-1989}

Shared types and basic lemmas for temporal connective semantics.

Sentence denotations are sets of temporal intervals — the "run-times" of a sentence's truth. Two canonical patterns:

• Stative: the maximal interval plus all its subintervals (homogeneity)
• Accomplishment: a singleton interval (quantized)

Temporal trace (timeTrace) projects from interval sets (Level 2) to point sets (Level 1). This is the lower half of the three-level projection chain:

Level 3: EvPred Time (event predicates)
    ↓ eventDenotation (see EventBridge.lean)
Level 2: SentDenotation Time (interval sets — this file)
    ↓ timeTrace
Level 1: Set Time (point sets)

@[reducible, inline]

abbrev Semantics.Tense.TemporalConnectives.SentDenotation (Time : Type u_2) [LE Time] : Type u_2

A sentence denotes a set of temporal intervals (its "run-times"). Statives denote homogeneous interval sets; accomplishments denote singletons.

Equations

• Semantics.Tense.TemporalConnectives.SentDenotation Time = Set (Core.Time.Interval Time)

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

The set of all time points contained in some interval of a denotation. This projects from interval-set representation to time-set representation, which is what @cite{rett-2020}'s formalization quantifies over.

Equations

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

def Semantics.Tense.TemporalConnectives.stativeDenotation {Time : Type u_1} [LinearOrder Time] (i : Core.Time.Interval Time) : SentDenotation Time

Stative denotation: the maximal interval i plus all its subintervals. Captures the subinterval (homogeneity) property of states/activities.

Equations

• Semantics.Tense.TemporalConnectives.stativeDenotation i = {j : Core.Time.Interval Time | j.subinterval i}

def Semantics.Tense.TemporalConnectives.accomplishmentDenotation {Time : Type u_1} [LinearOrder Time] (i : Core.Time.Interval Time) : SentDenotation Time

Accomplishment denotation: exactly the singleton interval i. Captures the quantized property of telic events.

Equations

• Semantics.Tense.TemporalConnectives.accomplishmentDenotation i = {j : Core.Time.Interval Time | j = i}

theorem Semantics.Tense.TemporalConnectives.stative_denotation_subinterval_closed {Time : Type u_1} [LinearOrder Time] (i j : Core.Time.Interval Time) : j ∈ stativeDenotation i → ∀ (k : Core.Time.Interval Time), k.subinterval j → k ∈ stativeDenotation i

Stative denotations are closed under subintervals (the subinterval property). This connects to Krifka's CUM (cumulative reference): if an interval is in the denotation, all its subintervals are too.

theorem Semantics.Tense.TemporalConnectives.stativeDenotation_contains_point {Time : Type u_1} [LinearOrder Time] (i : Core.Time.Interval Time) (t : Time) (ht : i.contains t) : Core.Time.Interval.point t ∈ stativeDenotation i

Every point subinterval of a stative denotation's maximal interval is in the set.

theorem Semantics.Tense.TemporalConnectives.accomplishmentDenotation_singleton {Time : Type u_1} [LinearOrder Time] (i j : Core.Time.Interval Time) : j ∈ accomplishmentDenotation i ↔ j = i

An accomplishment denotation has exactly one member.

theorem Semantics.Tense.TemporalConnectives.stativeDenotation_self {Time : Type u_1} [LinearOrder Time] (i : Core.Time.Interval Time) : i ∈ stativeDenotation i

The maximal interval is in its own stative denotation (reflexivity).

theorem Semantics.Tense.TemporalConnectives.timeTrace_stativeDenotation {Time : Type u_1} [LinearOrder Time] (i : Core.Time.Interval Time) : timeTrace (stativeDenotation i) = {t : Time | i.contains t}

The time trace of a stative denotation is exactly the set of times contained in the maximal interval.

theorem Semantics.Tense.TemporalConnectives.timeTrace_accomplishmentDenotation {Time : Type u_1} [LinearOrder Time] (i : Core.Time.Interval Time) : timeTrace (accomplishmentDenotation i) = {t : Time | i.contains t}

The time trace of an accomplishment denotation is exactly the set of times contained in the unique interval.