@[reducible, inline]

abbrev Semantics.Tense.TenseOp (W : Type u_1) (Time : Type u_2) : Type (max u_2 u_1)

Type of tense operators.

A tense operator takes:

• A temporal predicate P : (s, s') → Prop
• Two situations: the "now" situation s and evaluation situation s'
• Returns whether P holds with the tense constraint

Equations

• Semantics.Tense.TenseOp W Time = (Core.Time.Tense.SitProp W Time → Core.WorldTimeIndex W Time → Core.WorldTimeIndex W Time → Prop)

The temporal constraint of each tense, factored out as a pure relation on WorldTimeIndex pairs and shared with the dynamic-context-update counterparts in Tense/Dynamic.lean via dynRelation. This is the Heim-Kratzer "tense as relation between times" intuition isolated from the propositional payload, so that a single relation kernel (precedes/ coincides/follows) is the source of truth for both static PAST/ PRES/FUT (Compositional, this file) and their dynamic eliminative- update counterparts (Tense/Dynamic.lean). Trichotomy and pairwise exclusion proved at this layer propagate to both static and dynamic operators by definitional unfolding.

@[reducible, inline]

abbrev Semantics.Tense.precedes {W : Type u_1} {Time : Type u_2} [LT Time] (s₁ s₂ : Core.WorldTimeIndex W Time) : Prop

Event time precedes reference time. The temporal kernel of PAST and dynPAST. Reducible so decide and rw see through to the underlying < on .time.

Equations

• Semantics.Tense.precedes s₁ s₂ = (s₁.time < s₂.time)

@[reducible, inline]

abbrev Semantics.Tense.coincides {W : Type u_1} {Time : Type u_2} (s₁ s₂ : Core.WorldTimeIndex W Time) : Prop

Event time coincides with reference time. The temporal kernel of PRES and dynPRES.

Equations

• Semantics.Tense.coincides s₁ s₂ = (s₁.time = s₂.time)

@[reducible, inline]

abbrev Semantics.Tense.follows {W : Type u_1} {Time : Type u_2} [LT Time] (s₁ s₂ : Core.WorldTimeIndex W Time) : Prop

Event time follows reference time. The temporal kernel of FUT and dynFUT.

Equations

• Semantics.Tense.follows s₁ s₂ = (s₁.time > s₂.time)

theorem Semantics.Tense.precedes_or_coincides_or_follows {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (s₁ s₂ : Core.WorldTimeIndex W Time) : precedes s₁ s₂ ∨ coincides s₁ s₂ ∨ follows s₁ s₂

The three temporal relations partition any pair of situations on a linear order. Used downstream by temporal_partition (in Tense/Dynamic.lean) and by static analyses that need exhaustive case analysis on tense.

theorem Semantics.Tense.not_precedes_and_follows {W : Type u_1} {Time : Type u_2} [Preorder Time] (s₁ s₂ : Core.WorldTimeIndex W Time) : ¬(precedes s₁ s₂ ∧ follows s₁ s₂)

precedes and follows are mutually exclusive on any preorder.

theorem Semantics.Tense.not_precedes_and_coincides {W : Type u_1} {Time : Type u_2} [Preorder Time] (s₁ s₂ : Core.WorldTimeIndex W Time) : ¬(precedes s₁ s₂ ∧ coincides s₁ s₂)

precedes and coincides are mutually exclusive on any preorder.

theorem Semantics.Tense.not_coincides_and_follows {W : Type u_1} {Time : Type u_2} [Preorder Time] (s₁ s₂ : Core.WorldTimeIndex W Time) : ¬(coincides s₁ s₂ ∧ follows s₁ s₂)

coincides and follows are mutually exclusive on any preorder.

def Semantics.Tense.PAST {W : Type u_1} {Time : Type u_2} [LT Time] : TenseOp W Time

PAST operator (@cite{mendes-2025} style)

⟦PAST⟧ = λP.λs.λs'. τ(s) < τ(s') ∧ P(s)

The PAST operator:

1. Requires the event situation s to precede reference situation s'
2. Evaluates P at the past situation s

Defined via the precedes kernel (above) so the temporal constraint is shared with dynPAST in Tense/Dynamic.lean.

Equations

• Semantics.Tense.PAST P s s' = (Semantics.Tense.precedes s s' ∧ P s)

def Semantics.Tense.PRES {W : Type u_1} {Time : Type u_2} : TenseOp W Time

PRES operator (@cite{mendes-2025} style)

⟦PRES⟧ = λP.λs.λs'. τ(s) = τ(s') ∧ P(s)

The PRESENT operator:

1. Requires the event situation s to be contemporaneous with s'
2. Evaluates P at situation s

Defined via the coincides kernel.

Equations

• Semantics.Tense.PRES P s s' = (Semantics.Tense.coincides s s' ∧ P s)

def Semantics.Tense.FUT {W : Type u_1} {Time : Type u_2} [LT Time] : TenseOp W Time

FUT operator (@cite{mendes-2025} style)

⟦FUT⟧ = λP.λs.λs'. τ(s) > τ(s') ∧ P(s)

The FUTURE operator:

1. Requires the event situation s to follow reference situation s'
2. Evaluates P at the future situation s

Defined via the follows kernel.

Equations

• Semantics.Tense.FUT P s s' = (Semantics.Tense.follows s s' ∧ P s)

def Semantics.Tense.pastSimple {Time : Type u_1} [LT Time] (P : Time → Prop) (eventTime speechTime : Time) : Prop

Simple PAST: Event time precedes speech time.

⟦PAST⟧ₛᵢₘₚₗₑ = λP.λt.λt_s. t < t_s ∧ P(t)

Equations

• Semantics.Tense.pastSimple P eventTime speechTime = (eventTime < speechTime ∧ P eventTime)

def Semantics.Tense.presSimple {Time : Type u_1} (P : Time → Prop) (eventTime speechTime : Time) : Prop

Simple PRESENT: Event time equals speech time.

Equations

• Semantics.Tense.presSimple P eventTime speechTime = (eventTime = speechTime ∧ P eventTime)

def Semantics.Tense.futSimple {Time : Type u_1} [LT Time] (P : Time → Prop) (eventTime speechTime : Time) : Prop

Simple FUTURE: Event time follows speech time.

Equations

• Semantics.Tense.futSimple P eventTime speechTime = (eventTime > speechTime ∧ P eventTime)

def Semantics.Tense.applyTense {Time : Type u_1} [LinearOrder Time] (t : GramTense) (f : Core.Time.Reichenbach.ReichenbachFrame Time) : Prop

Apply a tense to a Reichenbach frame, constraining R relative to P. Tense locates reference time relative to perspective time, not speech time. In root clauses P = S, so this reduces to the standard Reichenbach analysis. In SOT languages, embedded P shifts to the matrix event time, making the embedded tense relative.

Equations

• Semantics.Tense.applyTense Core.Time.Tense.GramTense.past f = (f.referenceTime < f.perspectiveTime)
• Semantics.Tense.applyTense Core.Time.Tense.GramTense.present f = (f.referenceTime = f.perspectiveTime)
• Semantics.Tense.applyTense Core.Time.Tense.GramTense.future f = (f.referenceTime > f.perspectiveTime)
• Semantics.Tense.applyTense Core.Time.Tense.GramTense.nonpast f = (f.referenceTime ≥ f.perspectiveTime)

def Semantics.Tense.satisfiesTense {Time : Type u_1} [LinearOrder Time] [DecidableEq Time] [DecidableRel fun (x1 x2 : Time) => x1 < x2] (t : GramTense) (f : Core.Time.Reichenbach.ReichenbachFrame Time) : Bool

Check if a Reichenbach frame satisfies a given tense. Tense locates R relative to P (perspective time).

Equations

• Semantics.Tense.satisfiesTense Core.Time.Tense.GramTense.past f = decide (f.referenceTime < f.perspectiveTime)
• Semantics.Tense.satisfiesTense Core.Time.Tense.GramTense.present f = (f.referenceTime == f.perspectiveTime)
• Semantics.Tense.satisfiesTense Core.Time.Tense.GramTense.future f = decide (f.referenceTime > f.perspectiveTime)
• Semantics.Tense.satisfiesTense Core.Time.Tense.GramTense.nonpast f = decide (f.referenceTime ≥ f.perspectiveTime)

def Semantics.Tense.composeTense : GramTense → GramTense → GramTense

Sequence of tenses (for embedded tense in reported speech, etc.)

"John said that Mary left" - past under past

Equations

• Semantics.Tense.composeTense Core.Time.Tense.GramTense.past Core.Time.Tense.GramTense.past = Core.Time.Tense.GramTense.past
• Semantics.Tense.composeTense Core.Time.Tense.GramTense.past Core.Time.Tense.GramTense.present = Core.Time.Tense.GramTense.past
• Semantics.Tense.composeTense Core.Time.Tense.GramTense.past Core.Time.Tense.GramTense.future = Core.Time.Tense.GramTense.past
• Semantics.Tense.composeTense Core.Time.Tense.GramTense.past Core.Time.Tense.GramTense.nonpast = Core.Time.Tense.GramTense.past
• Semantics.Tense.composeTense Core.Time.Tense.GramTense.present x✝ = x✝
• Semantics.Tense.composeTense Core.Time.Tense.GramTense.nonpast Core.Time.Tense.GramTense.past = Core.Time.Tense.GramTense.past
• Semantics.Tense.composeTense Core.Time.Tense.GramTense.nonpast Core.Time.Tense.GramTense.present = Core.Time.Tense.GramTense.nonpast
• Semantics.Tense.composeTense Core.Time.Tense.GramTense.nonpast Core.Time.Tense.GramTense.future = Core.Time.Tense.GramTense.future
• Semantics.Tense.composeTense Core.Time.Tense.GramTense.nonpast Core.Time.Tense.GramTense.nonpast = Core.Time.Tense.GramTense.nonpast
• Semantics.Tense.composeTense Core.Time.Tense.GramTense.future Core.Time.Tense.GramTense.past = Core.Time.Tense.GramTense.future
• Semantics.Tense.composeTense Core.Time.Tense.GramTense.future Core.Time.Tense.GramTense.present = Core.Time.Tense.GramTense.future
• Semantics.Tense.composeTense Core.Time.Tense.GramTense.future Core.Time.Tense.GramTense.future = Core.Time.Tense.GramTense.future
• Semantics.Tense.composeTense Core.Time.Tense.GramTense.future Core.Time.Tense.GramTense.nonpast = Core.Time.Tense.GramTense.future

theorem Semantics.Tense.applyTense_eq_constrains {Time : Type u_1} [LinearOrder Time] (t : GramTense) (f : Core.Time.Reichenbach.ReichenbachFrame Time) : applyTense t f ↔ t.constrains f.referenceTime f.perspectiveTime

applyTense is the Reichenbach-frame projection of GramTense.constrains: applying a tense to a frame is equivalent to the tense's temporal constraint on the frame's R and P.

theorem Semantics.Tense.past_requires_precedence {W : Type u_1} {Time : Type u_2} [LT Time] (P : SitProp W Time) (s s' : Core.WorldTimeIndex W Time) : PAST P s s' → s.time < s'.time

PAST requires temporal precedence.

theorem Semantics.Tense.fut_requires_succession {W : Type u_1} {Time : Type u_2} [LT Time] (P : SitProp W Time) (s s' : Core.WorldTimeIndex W Time) : FUT P s s' → s.time > s'.time

FUT requires temporal succession.

theorem Semantics.Tense.pres_requires_contemporaneity {W : Type u_1} {Time : Type u_2} (P : SitProp W Time) (s s' : Core.WorldTimeIndex W Time) : PRES P s s' → s.time = s'.time

PRES requires contemporaneity.

theorem Semantics.Tense.past_preserves_pred {W : Type u_1} {Time : Type u_2} [LT Time] (P : SitProp W Time) (s s' : Core.WorldTimeIndex W Time) : PAST P s s' → P s

Tense preserves the predicate.

If TENSE(P)(s, s'), then P(s).

theorem Semantics.Tense.pres_preserves_pred {W : Type u_1} {Time : Type u_2} (P : SitProp W Time) (s s' : Core.WorldTimeIndex W Time) : PRES P s s' → P s

theorem Semantics.Tense.fut_preserves_pred {W : Type u_1} {Time : Type u_2} [LT Time] (P : SitProp W Time) (s s' : Core.WorldTimeIndex W Time) : FUT P s s' → P s

def Semantics.Tense.raining (W : Type u_1) : SitProp W ℤ

Example predicate: "rain at situation s"

Equations

• Semantics.Tense.raining W _s = True

composeTense Properties

@cite{kiparsky-2002}

composeTense is a stipulative function defining how surface tenses compose under embedding. The following theorems establish its algebraic properties.

For the DERIVED version — showing that composeTense matches the Reichenbach analysis with perspective shifting — see Semantics.Tense (in IS/Tense/Basic.lean) and the TC↔IS bridge in Semantics.Tense.SequenceOfTense.

theorem Semantics.Tense.composeTense_present_left (t : GramTense) : composeTense Core.Time.Tense.GramTense.present t = t

Present is transparent under composition (left): composing with matrix present always yields the embedded tense. This reflects present's semantics: R = P, so tense relative to a present perspective is unchanged.

theorem Semantics.Tense.composeTense_present_right (t : GramTense) : composeTense t Core.Time.Tense.GramTense.present = t

Present is transparent under composition (right): embedding present under any tense yields the matrix tense. Embedded present = "at the matrix event time" = same tense relative to speech time.

theorem Semantics.Tense.composeTense_past_idempotent : composeTense Core.Time.Tense.GramTense.past Core.Time.Tense.GramTense.past = Core.Time.Tense.GramTense.past

Tense composition is idempotent for past: embedding past arbitrarily deep under past still yields past.

theorem Semantics.Tense.composeTense_future_idempotent : composeTense Core.Time.Tense.GramTense.future Core.Time.Tense.GramTense.future = Core.Time.Tense.GramTense.future

Tense composition is idempotent for future.