Reichenbach's Temporal Framework

@cite{kiparsky-2002} @cite{klein-1994} @cite{reichenbach-1947}

@cite{reichenbach-1947} / @cite{klein-1994} tense–aspect parameters, extended with @cite{kiparsky-2002}'s perspective time P.

Three (four) distinguished times:

• S (Speech time): When the utterance occurs
• P (Perspective time): Origin of temporal deixis
• R (Reference/Topic time): The time being talked about
• E (Event time): When the event occurs

Tense relates R to P; Aspect relates E to R.

structure Core.Reichenbach.ReichenbachFrame (Time : Type u_1) : Type u_1

Reichenbach's temporal parameters for tense/aspect analysis, extended with @cite{kiparsky-2002}'s perspective time P.

• speechTime: When the utterance is made (S)
• perspectiveTime: Origin of temporal deixis (P, @cite{kiparsky-2002})
• referenceTime: The time being talked about (R, Klein's "topic time")
• eventTime: When the described event occurs (E)

P = S in root clauses but diverges for flashbacks, free indirect discourse, and embedded tenses. Tense locates R relative to P (not S).

• speechTime : Time

  Speech time (S): when the utterance occurs

• perspectiveTime : Time

  Perspective time (P): origin of temporal deixis. Equals S in root clauses; shifts in flashback, FID, embedded tenses.

• referenceTime : Time

  Reference time (R): the time under discussion

• eventTime : Time

  Event time (E): when the event takes place

def Core.Reichenbach.ReichenbachFrame.isPast {Time : Type u_1} [LinearOrder Time] (f : ReichenbachFrame Time) : Prop

PAST: R < P (reference time precedes perspective time). @cite{kiparsky-2002}: tense locates R relative to P, not S.

Equations

• f.isPast = (f.referenceTime < f.perspectiveTime)

def Core.Reichenbach.ReichenbachFrame.isPresent {Time : Type u_1} (f : ReichenbachFrame Time) : Prop

PRESENT: R = P (reference time equals perspective time).

Equations

• f.isPresent = (f.referenceTime = f.perspectiveTime)

def Core.Reichenbach.ReichenbachFrame.isFuture {Time : Type u_1} [LinearOrder Time] (f : ReichenbachFrame Time) : Prop

FUTURE: P < R (perspective time precedes reference time).

Equations

• f.isFuture = (f.perspectiveTime < f.referenceTime)

def Core.Reichenbach.ReichenbachFrame.isSimpleCase {Time : Type u_1} (f : ReichenbachFrame Time) : Prop

Simple case: P = S (root clause, no perspective shift).

Equations

• f.isSimpleCase = (f.perspectiveTime = f.speechTime)

def Core.Reichenbach.ReichenbachFrame.defaultPR {Time : Type u_1} [LinearOrder Time] (f : ReichenbachFrame Time) : Prop

Kiparsky's unmarked P–R default: P ≤ R.

Equations

• f.defaultPR = (f.perspectiveTime ≤ f.referenceTime)

def Core.Reichenbach.ReichenbachFrame.defaultER {Time : Type u_1} [LinearOrder Time] (f : ReichenbachFrame Time) : Prop

Kiparsky's unmarked E–R default: E ≤ R.

Equations

• f.defaultER = (f.eventTime ≤ f.referenceTime)

theorem Core.Reichenbach.ReichenbachFrame.isPast_simpleCase {Time : Type u_1} [LinearOrder Time] (f : ReichenbachFrame Time) (h : f.isSimpleCase) : f.isPast ↔ f.referenceTime < f.speechTime

In the simple case (P = S), isPast reduces to R < S.

def Core.Reichenbach.ReichenbachFrame.isPerfective {Time : Type u_1} (f : ReichenbachFrame Time) : Prop

Perfective: E ⊆ R (event contained in reference). Simplified to E = R for point-based times. TODO: proper interval-based perfective/imperfective distinction lives in Theories/Semantics/Lexical/Verb/ViewpointAspect.lean.

Equations

• f.isPerfective = (f.eventTime = f.referenceTime)

def Core.Reichenbach.ReichenbachFrame.isPerfect {Time : Type u_1} [LinearOrder Time] (f : ReichenbachFrame Time) : Prop

Perfect: E < R (event precedes reference)

Equations

• f.isPerfect = (f.eventTime < f.referenceTime)

def Core.Reichenbach.ReichenbachFrame.isProspective {Time : Type u_1} [LinearOrder Time] (f : ReichenbachFrame Time) : Prop

Prospective: R < E (reference precedes event)

Equations

• f.isProspective = (f.referenceTime < f.eventTime)