Documentation

Linglib.Theories.Semantics.Tense.SequenceOfTense

Sequence of Tense: TC ↔ IS Bridge #

@cite{heim-kratzer-1998} @cite{kratzer-1998} @cite{reichenbach-1947} @cite{von-stechow-2009}

Bridge theorems connecting the truth-conditional tense operators (applyTense from TC/Tense/Basic.lean) to the intensional semantic embedding infrastructure (embeddedFrame, simultaneousFrame, etc. from IS/Tense/Basic.lean).

Also bridges the situation-semantic formulation of attitude accessibility (temporallyBound from IS/Attitude/SituationDependent.lean) to the Reichenbach frame analysis.

Core Embedding Infrastructure #

The embedding infrastructure (embedded frames, SOT readings, upper limit constraint) lives in Theories/Semantics.Intensional/Tense/Basic.lean. This file provides the bridge between that infrastructure and the truth-conditional tense operators.

For the full six-theory comparison (Abusch, Von Stechow, Kratzer, Ogihara, Klecha, Deal), see Theories/Semantics.Intensional/Tense/ and Comparisons/TenseTheories.lean.

Connecting applyTense to the Embedding Infrastructure #

applyTense (truth-conditional) and embeddedFrame (intensional semantic) are defined in different layers. The following theorems bridge them, showing that the TC tense operators interact correctly with the IS perspective-shift mechanism.

source
theorem Semantics.Tense.SequenceOfTense.embeddedPast_means_before_matrix {Time : Type u_1} [LinearOrder Time] (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) (embeddedR embeddedE : Time) :
applyTense Core.Tense.GramTense.past (embeddedFrame matrixFrame embeddedR embeddedE) ↔ embeddedR < matrixFrame.eventTime

Applying embedded PAST to the embedded frame means R' < E_matrix.

The shifted reading: the embedded tense really is PAST relative to the shifted perspective (matrix event time).

source
theorem Semantics.Tense.SequenceOfTense.embeddedPresent_means_at_matrix {Time : Type u_1} [LinearOrder Time] (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) (embeddedR embeddedE : Time) :
applyTense Core.Tense.GramTense.present (embeddedFrame matrixFrame embeddedR embeddedE) ↔ embeddedR = matrixFrame.eventTime

Applying embedded PRESENT to the embedded frame means R' = E_matrix.

The simultaneous reading: the embedded tense is PRESENT relative to the shifted perspective.

Connecting Attitude Accessibility to Reichenbach Frames #

The attitude side (SituationDependent.temporallyBound) and the tense side (simultaneousFrame) describe the same empirical phenomenon — the simultaneous reading — using different formal vocabularies. The following theorems prove their equivalence, completing the missing edge in the dependency graph.

@cite{ogihara-1989}: the bound (zero) tense variable receives the matrix event time via lambda abstraction. The Reichenbach frame has R = P (simultaneous). The situation-semantic formulation imposes time-equality on accessible situations. All three descriptions collapse to the same truth condition.

source
theorem Semantics.Tense.SequenceOfTense.temporallyBound_forces_time_eq {W : Type u_1} {Time : Type u_2} {E : Type u_3} [DecidableEq Time] (R : Core.ModalLogic.AgentAccessRel W E) (agent : E) (s₁ s₂ : Situation W Time) (h : Attitudes.SituationDependent.temporallyBound R agent s₁ s₂ = true) :
s₂.time = s₁.time

Temporal binding extracts a time-equality constraint from situation accessibility. This is the situation-semantic formulation of "the embedded tense receives the matrix event time."

source
theorem Semantics.Tense.SequenceOfTense.temporallyBound_gives_simultaneous {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LinearOrder Time] (R : Core.ModalLogic.AgentAccessRel W E) (agent : E) (s₁ s₂ : Situation W Time) (speechTime : Time) (h : Attitudes.SituationDependent.temporallyBound R agent s₁ s₂ = true) :
have embFrame := { speechTime := speechTime, perspectiveTime := s₁.time, referenceTime := s₂.time, eventTime := s₂.time }; embFrame.isPresent

The time-equality from temporallyBound corresponds to the Reichenbach PRESENT relation (R = P) in the embedded frame — i.e., the simultaneous reading.

This connects the attitude-side formalization (SituationDependent.temporallyBound) to the tense-side formalization (simultaneousFrame in IS/Tense/Basic).