@[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.Tense.SitProp W Time → Situation W Time → Situation W Time → Prop)

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

Equations

• Semantics.Tense.PAST P s s' = (s.time < s'.time ∧ 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

Equations

• Semantics.Tense.PRES P s s' = (s.time = s'.time ∧ 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

Equations

• Semantics.Tense.FUT P s s' = (s.time > s'.time ∧ 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.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.Tense.GramTense.past f = (f.referenceTime < f.perspectiveTime)
• Semantics.Tense.applyTense Core.Tense.GramTense.present f = (f.referenceTime = f.perspectiveTime)
• Semantics.Tense.applyTense Core.Tense.GramTense.future 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.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.Tense.GramTense.past f = decide (f.referenceTime < f.perspectiveTime)
• Semantics.Tense.satisfiesTense Core.Tense.GramTense.present f = (f.referenceTime == f.perspectiveTime)
• Semantics.Tense.satisfiesTense Core.Tense.GramTense.future 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.Tense.GramTense.past Core.Tense.GramTense.past = Core.Tense.GramTense.past
• Semantics.Tense.composeTense Core.Tense.GramTense.past Core.Tense.GramTense.present = Core.Tense.GramTense.past
• Semantics.Tense.composeTense Core.Tense.GramTense.past Core.Tense.GramTense.future = Core.Tense.GramTense.past
• Semantics.Tense.composeTense Core.Tense.GramTense.present x✝ = x✝
• Semantics.Tense.composeTense Core.Tense.GramTense.future Core.Tense.GramTense.past = Core.Tense.GramTense.future
• Semantics.Tense.composeTense Core.Tense.GramTense.future Core.Tense.GramTense.present = Core.Tense.GramTense.future
• Semantics.Tense.composeTense Core.Tense.GramTense.future Core.Tense.GramTense.future = Core.Tense.GramTense.future

theorem Semantics.Tense.applyTense_eq_constrains {Time : Type u_1} [LinearOrder Time] (t : GramTense) (f : Core.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' : Situation 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' : Situation 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' : Situation 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' : Situation 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' : Situation 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' : Situation 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.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.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.Tense.GramTense.past Core.Tense.GramTense.past = Core.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.Tense.GramTense.future Core.Tense.GramTense.future = Core.Tense.GramTense.future

Tense composition is idempotent for future.