Temporal Connective Infrastructure

[All83] [Kri89]

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: Event Time → Prop (event predicates)
    ↓ eventDenotation (see Projection.lean)
Level 2: SentDenotation Time (interval sets — this file)
    ↓ timeTrace
Level 1: Set Time (point sets)

Sentence Denotations as NonemptyInterval Sets

@[reducible, inline]

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

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

Equations

• Tense.TemporalConnectives.SentDenotation Time = Set (NonemptyInterval Time)

def 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 [Ret20]'s formalization quantifies over.

Equations

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

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

Stative denotation: the maximal interval i plus all its subintervals — the principal downset Set.Iic i. It is therefore an IsLowerSet (isLowerSet_Iic), which is the subinterval-closure property.

This models the idealized stative subinterval property (homogeneous down to instants). The activity case has a minimal-parts floor — a single step is not "running" — which is the proper-subinterval stratified reference of Aspect/Stratified / [Cha17], not this lower set.

Equations

• Tense.TemporalConnectives.stativeDenotation i = Set.Iic i

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

Accomplishment denotation: exactly the singleton interval i ({i}). Captures the quantized property of telic events.

Equations

• Tense.TemporalConnectives.accomplishmentDenotation i = {i}

Basic Properties

theorem Tense.TemporalConnectives.stativeDenotation_contains_point {Time : Type u_1} [LinearOrder Time] (i : NonemptyInterval Time) (t : Time) (ht : t ∈ i) : NonemptyInterval.pure t ∈ stativeDenotation i

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

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

An accomplishment denotation has exactly one member.

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

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

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

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

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

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