Reichenbach's temporal frame

A Reichenbach frame locates a clause by four times. Reichenbach's three are points: the point of speech S, the point of reference R and the point of the event E. Kiparsky adds the perspective time P, the origin of temporal deixis, which includes S in the simple case and departs from it in flashbacks and historical presents. A frame has two positions, of R relative to P and of E relative to R (ReichenbachFrame.referencePosition, ReichenbachFrame.eventPosition). Reichenbach names the first past, present or future and the second anterior, simple or posterior; Kiparsky calls the first tense and the second aspect, the perfect placing E before R and the prospective after it. A tense cell of Semantics/Tense/Defs.lean constrains the first position, as in f.referencePosition ∈ ⟦past⟧. Kiparsky links E to P only through R, so their comparison is one that the composition of the two positions allows. Reichenbach's own frames are those whose perspective is the point of speech (ReichenbachFrame.root).

Main definitions

• Tense.ReichenbachFrame: the four times of a clause.
• Tense.ReichenbachFrame.root: Reichenbach's frame, the perspective at the point of speech.
• Tense.ReichenbachFrame.referencePosition, Tense.ReichenbachFrame.eventPosition: R relative to P and E relative to R.

Main results

• Tense.ReichenbachFrame.compare_eventTime_perspectiveTime_mem: E stands to P as the composition of the event position with the reference position allows.

Implementation notes

The times are points of a linear order, as Reichenbach's are. Kiparsky takes them to be intervals with points as the degenerate case, so his default inclusions of P and E in R become equalities here, and the duration of an event that reaches up to the point of speech is not represented; his interval account of the perfect is Studies/Kiparsky2002.lean, and interval aspect is Semantics/Aspect/Viewpoint.lean. A frame records times, not morphology: that a sentence's tense form yields a frame with a given position is a study's claim.

References

• [Rei47]
• [Kip02]

structure Tense.ReichenbachFrame (T : Type u_1) : Type u_1

A Reichenbach frame consists of the point of speech, the perspective time, the point of reference and the point of the event of a clause.

• speechTime : T

  The point of speech S is when the utterance occurs.

• perspectiveTime : T

  The perspective time P is the origin of temporal deixis.

• referenceTime : T

  The point of reference R is the time to which adverbs refer.

• eventTime : T

  The point of the event E is when the event occurs.

def Tense.ReichenbachFrame.root {T : Type u_1} (s r e : T) : ReichenbachFrame T

Reichenbach's frame of the points s, r and e takes the point of speech as the perspective.

Equations

• Tense.ReichenbachFrame.root s r e = { speechTime := s, perspectiveTime := s, referenceTime := r, eventTime := e }

@[simp]

theorem Tense.ReichenbachFrame.root_eventTime {T : Type u_1} (s r e : T) : (root s r e).eventTime = e

@[simp]

theorem Tense.ReichenbachFrame.root_referenceTime {T : Type u_1} (s r e : T) : (root s r e).referenceTime = r

@[simp]

theorem Tense.ReichenbachFrame.root_speechTime {T : Type u_1} (s r e : T) : (root s r e).speechTime = s

@[simp]

theorem Tense.ReichenbachFrame.root_perspectiveTime {T : Type u_1} (s r e : T) : (root s r e).perspectiveTime = s

def Tense.ReichenbachFrame.referencePosition {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Ordering

The reference position of a frame is how its point of reference stands to its perspective time, which the words past, present and future indicate.

Equations

• f.referencePosition = compare f.referenceTime f.perspectiveTime

def Tense.ReichenbachFrame.eventPosition {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : Ordering

The event position of a frame is how its point of the event stands to its point of reference, which the words anterior, simple and posterior indicate.

Equations

• f.eventPosition = compare f.eventTime f.referenceTime

@[simp]

theorem Tense.ReichenbachFrame.referencePosition_eq_lt {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.referencePosition = Ordering.lt ↔ f.referenceTime < f.perspectiveTime

@[simp]

theorem Tense.ReichenbachFrame.referencePosition_eq_eq {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.referencePosition = Ordering.eq ↔ f.referenceTime = f.perspectiveTime

@[simp]

theorem Tense.ReichenbachFrame.referencePosition_eq_gt {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.referencePosition = Ordering.gt ↔ f.perspectiveTime < f.referenceTime

@[simp]

theorem Tense.ReichenbachFrame.eventPosition_eq_lt {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.eventPosition = Ordering.lt ↔ f.eventTime < f.referenceTime

@[simp]

theorem Tense.ReichenbachFrame.eventPosition_eq_eq {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.eventPosition = Ordering.eq ↔ f.eventTime = f.referenceTime

@[simp]

theorem Tense.ReichenbachFrame.eventPosition_eq_gt {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : f.eventPosition = Ordering.gt ↔ f.referenceTime < f.eventTime

theorem Tense.ReichenbachFrame.compare_eventTime_perspectiveTime_mem {T : Type u_1} [LinearOrder T] (f : ReichenbachFrame T) : compare f.eventTime f.perspectiveTime ∈ f.eventPosition.comp f.referencePosition

The point of the event stands to the perspective time as the composition of the event position with the reference position allows.