Event–Interval Bridge

@cite{krifka-1989} @cite{parsons-1990}

The projection from event predicates (Level 3) to interval sets (Level 2):

Level 3: EvPred Time (event predicates — O&ST, future theories)
    ↓ eventDenotation (this file)
Level 2: SentDenotation Time (interval sets — Anscombe, Rett)
    ↓ timeTrace (Basic.lean)
Level 1: Set Time (point sets)

eventDenotation is the τ-image of an event predicate: the set of runtime intervals of events satisfying P. It is the architectural bridge that lets event-level theories (O&ST) be compared with interval-level theories (Rett) and point-level theories (Anscombe).

Key Properties

• eventDenotation preserves emptiness (no events ↔ empty denotation)
• Time traces factor through: timeTrace (eventDenotation P) = { t | ∃ e, P e ∧ τ(e) contains t }
• The projection is sort-erasing: event sort (action/state) is lost. This is correct for temporal connectives, which don't care about event sort.

def Semantics.Tense.TemporalConnectives.eventDenotation {Time : Type u_1} [LinearOrder Time] (P : Events.EvPred Time) : SentDenotation Time

The τ-image projection: the set of runtime intervals of events satisfying P.

This is the fundamental bridge between event semantics (Level 3) and interval-set semantics (Level 2). Every event-level temporal connective theory can be projected down to the interval level through this map, then compared with Anscombe and Rett.

Equations

• Semantics.Tense.TemporalConnectives.eventDenotation P = {i : Core.Time.Interval Time | ∃ (e : Semantics.Events.Ev Time), P e ∧ e.τ = i}

theorem Semantics.Tense.TemporalConnectives.eventDenotation_empty {Time : Type u_1} [LinearOrder Time] : (eventDenotation fun (x : Events.Ev Time) => False) = ∅

Empty predicate gives empty denotation.

theorem Semantics.Tense.TemporalConnectives.eventDenotation_nonempty {Time : Type u_1} [LinearOrder Time] (P : Events.EvPred Time) (e : Events.Ev Time) (he : P e) : e.τ ∈ eventDenotation P

Nonempty predicate gives nonempty denotation (if there exists a witness).

theorem Semantics.Tense.TemporalConnectives.timeTrace_eventDenotation {Time : Type u_1} [LinearOrder Time] (P : Events.EvPred Time) : timeTrace (eventDenotation P) = {t : Time | ∃ (e : Events.Ev Time), P e ∧ e.τ.contains t}

The time trace of an event denotation factors through τ: a time is in the trace iff some event satisfying P has a runtime containing that time.

This is the composition timeTrace ∘ eventDenotation, showing that the full projection chain Level 3 → Level 1 can be stated directly.

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

A singleton event predicate (exactly one event with runtime i) gives an accomplishment denotation.

theorem Semantics.Tense.TemporalConnectives.eventDenotation_sub_stative {Time : Type u_1} [LinearOrder Time] (i : Core.Time.Interval Time) (P : Events.EvPred Time) (hP : ∀ (e : Events.Ev Time), P e → e.τ.subinterval i) : eventDenotation P ⊆ stativeDenotation i

An event predicate selecting all events with runtime subinterval of i gives a subset of the stative denotation.

Note: this is a subset, not equality, because stativeDenotation i contains all subintervals including those that might not be runtimes of any event.