Compositional Tense Operators

[Men25] [Par73]

Semantic operators for grammatical tense (PAST, PRES, FUT) in the situation-semantic style ([Men25]: operators constrain the temporal coordinate of a situation argument), driven by the shared temporal-relation kernel (precedes/coincides/follows), which also grounds the dynamic counterparts in Tense/Dynamic.lean. (Reichenbach frame-based tense predicates live in Tense/Reichenbach.lean.) Following [Par73], tenses are pronoun-like: they retrieve temporal reference points rather than quantify over all times.

@[reducible, inline]

abbrev 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

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

Temporal-relation kernel

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 Tense.precedes {W : Type u_1} {Time : Type u_2} [LT Time] (s₁ s₂ : Intensional.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

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

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

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

Equations

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

theorem Tense.precedes_or_coincides_or_follows {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (s₁ s₂ : Intensional.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 Tense.not_precedes_and_follows {W : Type u_1} {Time : Type u_2} [Preorder Time] (s₁ s₂ : Intensional.WorldTimeIndex W Time) : ¬(precedes s₁ s₂ ∧ follows s₁ s₂)

precedes and follows are mutually exclusive on any preorder.

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

precedes and coincides are mutually exclusive on any preorder.

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

coincides and follows are mutually exclusive on any preorder.

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

PAST operator ([Men25] 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

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

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

PRES operator ([Men25] 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

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

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

FUT operator ([Men25] 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

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

def 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

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

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

Simple PRESENT: Event time equals speech time.

Equations

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

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

Simple FUTURE: Event time follows speech time.

Equations

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

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

PAST requires temporal precedence.

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

FUT requires temporal succession.

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

PRES requires contemporaneity.

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

Tense preserves the predicate.

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

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

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

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

Example predicate: "rain at situation s"

Equations

• Tense.raining W _s = True