Grammatical tense as a comparison category

A grammatical tense is a comparison category between a reference time and a perspective time — a Finset Ordering (Core.Order). There is no bespoke tense type: the four traditional labels name four of the comparison cells Core.Order already provides, so tense, evidentials, and modal-base time all share one Ordering-grounded spine.

• past = before (ref < perspective)
• present = overlapping (ref = perspective)
• future = after (ref > perspective)
• nonpast = notBefore (ref ≥ perspective — the present-or-future union, [Kle16])

The constraint a tense imposes is Core.Order.holds, grounded in Ordering over the order on T. The frame predicates (ReichenbachFrame.isPast/isFuture/isNonpast) and the compositional tense operators are views of holds (with Core.Order.holds_before etc. reducing them to </=/≥).

[Kle16] (the nonpast case) [Kip02]

@[reducible, inline]

abbrev Tense.past : Finset Ordering

Past: reference time before perspective time.

Equations

• Tense.past = Core.Order.before

@[reducible, inline]

abbrev Tense.present : Finset Ordering

Present: reference time overlaps (equals) perspective time.

Equations

• Tense.present = Core.Order.overlapping

@[reducible, inline]

abbrev Tense.future : Finset Ordering

Future: reference time after perspective time.

Equations

• Tense.future = Core.Order.after

@[reducible, inline]

abbrev Tense.nonpast : Finset Ordering

Nonpast ([Kle16]): reference time at or after perspective time — the present-or-future union (Core.Order.notBefore), not a fourth atomic tense. Lets embedded tense under circumstantial modals have future-oriented readings (⟦NPST⟧ requires ref ≥ perspective).

Equations

• Tense.nonpast = Core.Order.notBefore

theorem Tense.nonpast_eq_present_sup_future : nonpast = present ⊔ future

[Kle16]'s point made literal: nonpast is the Boolean join of present and future in the comparison-category algebra (Core.Order), not a fourth atomic tense.