Modal-Temporal Axes

@cite{condoravdi-2002}

The two temporal axes that any modal interpretation theory must distinguish (cf. @cite{condoravdi-2002}, §2):

• Temporal perspective: the time at which the modal base / ordering source is evaluated. Either present (utterance time) or past (an earlier evaluation point, accessed via a past-shifting operator scoping over the modal).

• Temporal orientation: the relation between the perspective time and the time of the modal's prejacent. Past, present (coincident), or future.

These axes are framework-neutral: they are used by Condoravdi 2002 (English might/would), Hacquard 2006 (event-relative modals), Klecha 2016 (CIR-based future orientation), Matthewson 2013 (Gitksan dim-based future orientation), and any other modal-temporal theory.

This file is the canonical home; downstream modules import from here rather than redeclaring local copies.

Note on @cite{condoravdi-2002}'s narrower local enums

Phenomena/Modality/Studies/Condoravdi2002.lean carries its own 2-element Perspective (matching TemporalPerspective here) and a 2-element Orientation (future | past only — Condoravdi's 4-reading typology has no present-orientation cell). Those local enums are tightly coupled with ModalReading, projectedRegion, and FrameAdverb.compatible machinery and are not migrated here. The canonical TemporalOrientation below is the strict superset; a Condoravdi-style 2-way Orientation would inject into it.

inductive Core.Modality.TemporalPerspective : Type

Temporal perspective: the time at which a modal base / ordering source is evaluated.

• present : TemporalPerspective

  Modal base evaluated at the utterance time.

• past : TemporalPerspective

  Modal base evaluated at a prior time (e.g., via PERF > MODAL).

@[implicit_reducible]

instance Core.Modality.instDecidableEqTemporalPerspective : DecidableEq TemporalPerspective

Equations

• Core.Modality.instDecidableEqTemporalPerspective x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Modality.instReprTemporalPerspective.repr : TemporalPerspective → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Core.Modality.instReprTemporalPerspective : Repr TemporalPerspective

Equations

• Core.Modality.instReprTemporalPerspective = { reprPrec := Core.Modality.instReprTemporalPerspective.repr }

def Core.Modality.instBEqTemporalPerspective.beq : TemporalPerspective → TemporalPerspective → Bool

Equations

• Core.Modality.instBEqTemporalPerspective.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Core.Modality.instBEqTemporalPerspective : BEq TemporalPerspective

Equations

• Core.Modality.instBEqTemporalPerspective = { beq := Core.Modality.instBEqTemporalPerspective.beq }

@[implicit_reducible]

instance Core.Modality.instInhabitedTemporalPerspective : Inhabited TemporalPerspective

Equations

• Core.Modality.instInhabitedTemporalPerspective = { default := Core.Modality.instInhabitedTemporalPerspective.default }

def Core.Modality.instInhabitedTemporalPerspective.default : TemporalPerspective

Equations

• Core.Modality.instInhabitedTemporalPerspective.default = Core.Modality.TemporalPerspective.present

inductive Core.Modality.TemporalOrientation : Type

Temporal orientation: the temporal relation between the perspective time and the prejacent's instantiation time.

• past : TemporalOrientation

  Prejacent instantiated before the perspective time.

• present : TemporalOrientation

  Prejacent coincides with the perspective time.

• future : TemporalOrientation

  Prejacent instantiated at or after the perspective time.

@[implicit_reducible]

instance Core.Modality.instDecidableEqTemporalOrientation : DecidableEq TemporalOrientation

Equations

• Core.Modality.instDecidableEqTemporalOrientation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Modality.instReprTemporalOrientation.repr : TemporalOrientation → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Core.Modality.instReprTemporalOrientation : Repr TemporalOrientation

Equations

• Core.Modality.instReprTemporalOrientation = { reprPrec := Core.Modality.instReprTemporalOrientation.repr }

@[implicit_reducible]

instance Core.Modality.instBEqTemporalOrientation : BEq TemporalOrientation

Equations

• Core.Modality.instBEqTemporalOrientation = { beq := Core.Modality.instBEqTemporalOrientation.beq }

def Core.Modality.instBEqTemporalOrientation.beq : TemporalOrientation → TemporalOrientation → Bool

Equations

• Core.Modality.instBEqTemporalOrientation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance Core.Modality.instInhabitedTemporalOrientation : Inhabited TemporalOrientation

Equations

• Core.Modality.instInhabitedTemporalOrientation = { default := Core.Modality.instInhabitedTemporalOrientation.default }

def Core.Modality.instInhabitedTemporalOrientation.default : TemporalOrientation

Equations

• Core.Modality.instInhabitedTemporalOrientation.default = Core.Modality.TemporalOrientation.past