Compositional tense operators

[Men25] [Par73]

The compositional interpretation of a tense cell (Tense/Defs.lean) in the situation-semantic style of [Men25]: constrain s P sit sit' holds when the cell s relates the event situation's time to the evaluation situation's time and the payload P holds at the event situation. Following [Par73], the event situation is retrieved (an argument), not quantified over. PAST/PRES/FUT name the three atomic cells' operators; the dynamic counterparts in Tense/Dynamic.lean are the same cells behind the update spine's test filter.

def Tense.constrain {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (s : Finset Ordering) (P : Intensional.Index W Time → Prop) (sit sit' : Intensional.Index W Time) : Prop

The tense cell s, applied compositionally ([Men25]): ⟦s⟧ = λP.λsit.λsit'. holds s τ(sit) τ(sit') ∧ P(sit) — the cell constrains the event–evaluation comparison and the payload is evaluated at the event situation.

Equations

• Tense.constrain s P sit sit' = (Core.Order.holds s sit.time sit'.time ∧ P sit)

@[reducible, inline]

abbrev Tense.PAST {W : Type u_1} {Time : Type u_2} [LinearOrder Time] : (Intensional.Index W Time → Prop) → Intensional.Index W Time → Intensional.Index W Time → Prop

⟦PAST⟧ = constrain past: the event situation precedes the evaluation situation.

Equations

• Tense.PAST = Tense.constrain Tense.past

@[reducible, inline]

abbrev Tense.PRES {W : Type u_1} {Time : Type u_2} [LinearOrder Time] : (Intensional.Index W Time → Prop) → Intensional.Index W Time → Intensional.Index W Time → Prop

⟦PRES⟧ = constrain present: the event situation is contemporaneous with the evaluation situation.

Equations

• Tense.PRES = Tense.constrain Tense.present

@[reducible, inline]

abbrev Tense.FUT {W : Type u_1} {Time : Type u_2} [LinearOrder Time] : (Intensional.Index W Time → Prop) → Intensional.Index W Time → Intensional.Index W Time → Prop

⟦FUT⟧ = constrain future: the event situation follows the evaluation situation.

Equations

• Tense.FUT = Tense.constrain Tense.future

@[simp]

theorem Tense.constrain_past_iff {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Intensional.Index W Time → Prop) (sit sit' : Intensional.Index W Time) : constrain past P sit sit' ↔ sit.time < sit'.time ∧ P sit

@[simp]

theorem Tense.constrain_present_iff {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Intensional.Index W Time → Prop) (sit sit' : Intensional.Index W Time) : constrain present P sit sit' ↔ sit.time = sit'.time ∧ P sit

@[simp]

theorem Tense.constrain_future_iff {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Intensional.Index W Time → Prop) (sit sit' : Intensional.Index W Time) : constrain future P sit sit' ↔ sit'.time < sit.time ∧ P sit