Reichenbach's Temporal Framework

[Kip02] [Kle94] [Rei47]

[Rei47] / [Kle94] tense–aspect parameters, extended with [Kip02]'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 Time.ReichenbachFrame (T : Type u_1) : Type u_1

Reichenbach's temporal parameters for tense/aspect analysis, extended with [Kip02]'s perspective time P.

• speechTime: When the utterance is made (S)
• perspectiveTime: Origin of temporal deixis (P, [Kip02])
• 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 : T

  Speech time (S): when the utterance occurs

• perspectiveTime : T

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

• referenceTime : T

  Reference time (R): the time under discussion

• eventTime : T

  Event time (E): when the described event occurs (E)

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

PAST: R < P (reference time precedes perspective time) — a view of Core.Order.holds Tense.past. [Kip02]: tense locates R relative to P, not S.

Equations

• f.isPast = Core.Order.holds Tense.past f.referenceTime f.perspectiveTime

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

PRESENT: R = P (reference time equals perspective time). Present is the one tense that needs no ordering, so it stays the bare equality (frame predicates over unordered time keep typechecking); it is definitionally Core.Order.holds Tense.present.

Equations

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

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

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

Equations

• f.isFuture = Core.Order.holds Tense.future f.referenceTime f.perspectiveTime

def Time.ReichenbachFrame.isNonpast {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Prop

NONPAST: P ≤ R (present or future) ([Kle16]) — the view of Core.Order.holds Tense.nonpast. Completes the four-way relation on frames.

Equations

• f.isNonpast = Core.Order.holds Tense.nonpast f.referenceTime f.perspectiveTime

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

def Time.ReichenbachFrame.isPerfective {T : Type u_1} (f : ReichenbachFrame T) : 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 Semantics/Aspect/Basic.lean (Perfectivity).

Equations

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

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

Perfect: E < R (event precedes reference)

Equations

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

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

Prospective: R < E (reference precedes event)

Equations

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

Unfolding lemmas and decidability

One _def simp lemma and one Decidable instance per predicate, so consumers can close concrete goals with decide and rewrite with simp only [isPast_def] instead of unfolding definitions by hand.

@[simp]

theorem Time.ReichenbachFrame.isPast_def {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.isPast ↔ f.referenceTime < f.perspectiveTime

@[simp]

theorem Time.ReichenbachFrame.isPresent_def {T : Type u_1} (f : ReichenbachFrame T) : f.isPresent ↔ f.referenceTime = f.perspectiveTime

@[simp]

theorem Time.ReichenbachFrame.isFuture_def {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.isFuture ↔ f.perspectiveTime < f.referenceTime

@[simp]

theorem Time.ReichenbachFrame.isNonpast_def {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.isNonpast ↔ f.perspectiveTime ≤ f.referenceTime

@[simp]

theorem Time.ReichenbachFrame.isSimpleCase_def {T : Type u_1} (f : ReichenbachFrame T) : f.isSimpleCase ↔ f.perspectiveTime = f.speechTime

@[simp]

theorem Time.ReichenbachFrame.defaultPR_def {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.defaultPR ↔ f.perspectiveTime ≤ f.referenceTime

@[simp]

theorem Time.ReichenbachFrame.defaultER_def {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.defaultER ↔ f.eventTime ≤ f.referenceTime

@[simp]

theorem Time.ReichenbachFrame.isPerfective_def {T : Type u_1} (f : ReichenbachFrame T) : f.isPerfective ↔ f.eventTime = f.referenceTime

@[simp]

theorem Time.ReichenbachFrame.isPerfect_def {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.isPerfect ↔ f.eventTime < f.referenceTime

@[simp]

theorem Time.ReichenbachFrame.isProspective_def {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.isProspective ↔ f.referenceTime < f.eventTime

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

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

@[instance_reducible]

instance Time.ReichenbachFrame.instDecidableIsPast {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Decidable f.isPast

Equations

• f.instDecidableIsPast = id inferInstance

@[instance_reducible]

instance Time.ReichenbachFrame.instDecidableIsPresent {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Decidable f.isPresent

Equations

• f.instDecidableIsPresent = Time.ReichenbachFrame.instDecidableIsPresent._aux_1 f

@[instance_reducible]

instance Time.ReichenbachFrame.instDecidableIsFuture {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Decidable f.isFuture

Equations

• f.instDecidableIsFuture = id inferInstance

@[instance_reducible]

instance Time.ReichenbachFrame.instDecidableIsNonpast {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Decidable f.isNonpast

Equations

• f.instDecidableIsNonpast = id inferInstance

@[instance_reducible]

instance Time.ReichenbachFrame.instDecidableIsSimpleCase {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Decidable f.isSimpleCase

Equations

• f.instDecidableIsSimpleCase = Time.ReichenbachFrame.instDecidableIsSimpleCase._aux_1 f

@[instance_reducible]

instance Time.ReichenbachFrame.instDecidableDefaultPR {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Decidable f.defaultPR

Equations

• f.instDecidableDefaultPR = Time.ReichenbachFrame.instDecidableDefaultPR._aux_1 f

@[instance_reducible]

instance Time.ReichenbachFrame.instDecidableDefaultER {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Decidable f.defaultER

Equations

• f.instDecidableDefaultER = Time.ReichenbachFrame.instDecidableDefaultER._aux_1 f

@[instance_reducible]

instance Time.ReichenbachFrame.instDecidableIsPerfective {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Decidable f.isPerfective

Equations

• f.instDecidableIsPerfective = Time.ReichenbachFrame.instDecidableIsPerfective._aux_1 f

@[instance_reducible]

instance Time.ReichenbachFrame.instDecidableIsPerfect {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Decidable f.isPerfect

Equations

• f.instDecidableIsPerfect = Time.ReichenbachFrame.instDecidableIsPerfect._aux_1 f

@[instance_reducible]

instance Time.ReichenbachFrame.instDecidableIsProspective {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Decidable f.isProspective

Equations

• f.instDecidableIsProspective = Time.ReichenbachFrame.instDecidableIsProspective._aux_1 f