Perspectival Tense Theory

@cite{tsilia-zhao-2026} @cite{sharvit-2003} @cite{zhao-2025} @cite{anand-nevins-2004} @cite{deal-2020}

Reusable infrastructure for perspectival tense interpretation: tense presuppositions anchored to a perspective parameter π, the OP_π shift operator, and the InterpParams architecture enforcing independence of context and perspective.

Core Formal System

The interpretation function ⟦·⟧^{c,π,g} takes three parameters:

• c: context parameter ⟨c_s, c_a, c_t, c_w⟩ — for indexical interpretation
• π: temporal perspective — for tense interpretation
• g: variable assignment

Two shift operators with the same shape ("overwrite parameter with evaluation index") but operating on independent parameters:

• OP_c: overwrites c with the evaluation index (indexical shift, @cite{anand-nevins-2004})
• OP_π: overwrites π with the time component of the evaluation index (tense shift)

Tense Presuppositions

Tenses are presupposition triggers anchored to π:

• PRES: g(n) ○ π (reference overlaps perspective)
• PAST: g(n) < π (reference precedes perspective)
• ⌈then⌉: ¬(g(n) ○ π) (reference disjoint from perspective)

def Semantics.Tense.Perspective.presPresup {Time : Type u_1} (f : Core.Reichenbach.ReichenbachFrame Time) : Prop

PRES presupposes g(n) ○ π: the temporal reference overlaps the perspective. Point approximation: R = P.

Equations

• Semantics.Tense.Perspective.presPresup f = (f.referenceTime = f.perspectiveTime)

def Semantics.Tense.Perspective.pastPresup {Time : Type u_1} [LT Time] (f : Core.Reichenbach.ReichenbachFrame Time) : Prop

PAST presupposes g(n) < π: the temporal reference precedes the perspective.

Equations

• Semantics.Tense.Perspective.pastPresup f = (f.referenceTime < f.perspectiveTime)

theorem Semantics.Tense.Perspective.presPresup_iff_isPresent {Time : Type u_1} [LinearOrder Time] (f : Core.Reichenbach.ReichenbachFrame Time) : presPresup f ↔ f.isPresent

The PRES presupposition is definitionally equal to isPresent.

theorem Semantics.Tense.Perspective.pastPresup_iff_isPast {Time : Type u_1} [LinearOrder Time] (f : Core.Reichenbach.ReichenbachFrame Time) : pastPresup f ↔ f.isPast

The PAST presupposition is definitionally equal to isPast.

def Semantics.Tense.Perspective.opPi {Time : Type u_1} (f : Core.Reichenbach.ReichenbachFrame Time) (newPi : Time) : Core.Reichenbach.ReichenbachFrame Time

OP_π shifts the perspective time to a new value. ⟦OP_π φ⟧^{c,π,g} = λi_κ. ⟦φ⟧^{c,i_t,g}(i)

Equations

• Semantics.Tense.Perspective.opPi f newPi = { speechTime := f.speechTime, perspectiveTime := newPi, referenceTime := f.referenceTime, eventTime := f.eventTime }

theorem Semantics.Tense.Perspective.opPi_eq_embeddedFrame {Time : Type u_1} (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) (embeddedR embeddedE : Time) : opPi { speechTime := matrixFrame.speechTime, perspectiveTime := matrixFrame.speechTime, referenceTime := embeddedR, eventTime := embeddedE } matrixFrame.eventTime = embeddedFrame matrixFrame embeddedR embeddedE

OP_π corresponds to embeddedFrame when shifting to the matrix event time.

def Semantics.Tense.Perspective.thenPresup {Time : Type u_1} (thenRef perspective : Time) : Prop

⌈then⌉ presupposes ¬(g(n) ○ π): its temporal reference is disjoint from the perspective. Point approximation: thenRef ≠ π.

This is ⌈then⌉'s OWN presupposition, separate from the presuppositions of any co-clausal tense. The incompatibility with PRES arises because composition (via "during then") forces the PRES reference to be contained in the then reference, bridging the two presuppositions.

Equations

• Semantics.Tense.Perspective.thenPresup thenRef perspective = (thenRef ≠ perspective)

theorem Semantics.Tense.Perspective.then_present_clash {Time : Type u_1} (presRef thenRef perspective : Time) (hPres : presRef = perspective) (hDuring : presRef = thenRef) (hThen : thenPresup thenRef perspective) : False

The ⌈then⌉-present clash. Three ingredients produce the contradiction:

1. PRES presupposes presRef = π (overlap with perspective)
2. The temporal assertion requires presRef = thenRef ("during then")
3. ⌈then⌉ presupposes thenRef ≠ π (disjoint from perspective)

Together: π = presRef = thenRef, but thenRef ≠ π.

theorem Semantics.Tense.Perspective.then_perspective_clash {Time : Type u_1} (f : Core.Reichenbach.ReichenbachFrame Time) (localEval : Time) (hOP : f.perspectiveTime = localEval) (hThen : f.perspectiveTime ≠ localEval) : False

General OP_π + ⌈then⌉ clash at the frame level: OP_π sets P = localEval; anything requiring P ≠ localEval contradicts.

inductive Semantics.Tense.Perspective.EmbeddedTenseStatus : Type

Status of an embedded tense morpheme.

• shifted : EmbeddedTenseStatus

  Tense interpreted with presupposition anchored to shifted π

• deleted : EmbeddedTenseStatus

  Tense deleted by SOT; no temporal presupposition

instance Semantics.Tense.Perspective.instDecidableEqEmbeddedTenseStatus : DecidableEq EmbeddedTenseStatus

Equations

• Semantics.Tense.Perspective.instDecidableEqEmbeddedTenseStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Tense.Perspective.instReprEmbeddedTenseStatus.repr : EmbeddedTenseStatus → ℕ → Std.Format

Equations

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

instance Semantics.Tense.Perspective.instReprEmbeddedTenseStatus : Repr EmbeddedTenseStatus

Equations

• Semantics.Tense.Perspective.instReprEmbeddedTenseStatus = { reprPrec := Semantics.Tense.Perspective.instReprEmbeddedTenseStatus.repr }

def Semantics.Tense.Perspective.instBEqEmbeddedTenseStatus.beq : EmbeddedTenseStatus → EmbeddedTenseStatus → Bool

Equations

• Semantics.Tense.Perspective.instBEqEmbeddedTenseStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Tense.Perspective.instBEqEmbeddedTenseStatus : BEq EmbeddedTenseStatus

Equations

• Semantics.Tense.Perspective.instBEqEmbeddedTenseStatus = { beq := Semantics.Tense.Perspective.instBEqEmbeddedTenseStatus.beq }

def Semantics.Tense.Perspective.shiftedTensePresup {Time : Type u_1} [LT Time] (f : Core.Reichenbach.ReichenbachFrame Time) (isPres : Bool) : Prop

A shifted tense retains its presupposition (PRES or PAST relative to π).

Equations

• Semantics.Tense.Perspective.shiftedTensePresup f isPres = if isPres = true then Semantics.Tense.Perspective.presPresup f else Semantics.Tense.Perspective.pastPresup f

theorem Semantics.Tense.Perspective.deletedTensePresup : True

A deleted tense has no temporal presupposition — trivially satisfied.

theorem Semantics.Tense.Perspective.then_deleted_tense_compatible {Time : Type u_1} (thenRef perspective : Time) (hDisjoint : thenRef ≠ perspective) : thenPresup thenRef perspective

⌈then⌉ + deleted tense → compatible. Deleted tense has no presupposition anchoring it to π, so there is no overlap requirement. ⌈then⌉ can freely pick a reference disjoint from π.

theorem Semantics.Tense.Perspective.then_shifted_present_clash {Time : Type u_1} (presRef thenRef shiftedPi : Time) (hPres : presRef = shiftedPi) (hDuring : presRef = thenRef) (hThen : thenPresup thenRef shiftedPi) : False

⌈then⌉ + shifted tense → clash (when shifted tense is PRES). The shifted PRES anchors to π via OP_π, so presRef overlaps with the shifted π. If "during then" forces presRef = thenRef, then's disjointness presupposition ¬(thenRef ○ π) fails.

def Semantics.Tense.Perspective.presAsPrProp {Time : Type u_1} [DecidableEq Time] (f : Core.Reichenbach.ReichenbachFrame Time) : Core.Presupposition.PrProp Unit

Wrap PRES presupposition as a PrProp, showing how tense presuppositions compose with the existing presupposition projection system.

Equations

• Semantics.Tense.Perspective.presAsPrProp f = { presup := fun (x : Unit) => decide (f.referenceTime = f.perspectiveTime), assertion := fun (x : Unit) => true }

theorem Semantics.Tense.Perspective.presAsPrProp_defined_iff {Time : Type u_1} [DecidableEq Time] (f : Core.Reichenbach.ReichenbachFrame Time) : (presAsPrProp f).presup () = true ↔ f.referenceTime = f.perspectiveTime

The PrProp encoding is defined iff the PRES presupposition holds.

structure Semantics.Tense.Perspective.InterpParams (W : Type u_1) (E : Type u_2) (P : Type u_3) (T : Type u_4) : Type (max (max (max u_1 u_2) u_3) u_4)

The interpretation parameter tuple ⟨c, π⟩ from ⟦·⟧^{c,π,g}.

Context c (for indexical interpretation, @cite{anand-nevins-2004}) and perspective π (for tense interpretation) are independent parameters. This structure makes their independence explicit and architectural: shiftPerspective preserves context, and shiftContext preserves perspective.

The variable assignment g is orthogonal and handled separately (in Montague/Variables.lean).

• context : Core.Context.KContext W E P T

  Context parameter c = ⟨c_s, c_a, c_t, c_w⟩ — for indexicals (I, now, here)

• perspective : T

  Temporal perspective π — for tense (PRES, PAST, ⌈then⌉). Defaults to c_t in root clauses; shifted by OP_π under attitude verbs.

def Semantics.Tense.Perspective.InterpParams.shiftPerspective {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (ip : InterpParams W E P T) (newPi : T) : InterpParams W E P T

OP_π on the interpretation parameter tuple: shift π, preserve c. ⟦OP_π φ⟧^{c,π,g} = λi_κ. ⟦φ⟧^{c,i_t,g}(i)

Equations

• ip.shiftPerspective newPi = { context := ip.context, perspective := newPi }

def Semantics.Tense.Perspective.InterpParams.shiftContext {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (ip : InterpParams W E P T) (newC : Core.Context.KContext W E P T) : InterpParams W E P T

OP_c on the interpretation parameter tuple: shift c, preserve π. ⟦OP_c φ⟧^{c,π,g} = λi_κ. ⟦φ⟧^{i,π,g}(i)

Equations

• ip.shiftContext newC = { context := newC, perspective := ip.perspective }

@[simp]

theorem Semantics.Tense.Perspective.InterpParams.shiftPerspective_preserves_context {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (ip : InterpParams W E P T) (newPi : T) : (ip.shiftPerspective newPi).context = ip.context

OP_π preserves the context parameter (including c_t). This is the formal content of §7.1: tense shift does not entail indexical shift. Modern Greek allows OP_π (shifted present) but blocks the temporal indexical τώρα 'now' from shifting.

@[simp]

theorem Semantics.Tense.Perspective.InterpParams.shiftContext_preserves_perspective {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (ip : InterpParams W E P T) (newC : Core.Context.KContext W E P T) : (ip.shiftContext newC).perspective = ip.perspective

OP_c preserves the temporal perspective. Indexical shift does not entail tense shift.

def Semantics.Tense.Perspective.InterpParams.rootDefault {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Core.Context.KContext W E P T) : InterpParams W E P T

In root clauses, π defaults to c_t (the temporal component of the context). This is the Truth Convention: ⟦φ⟧ is true relative to c and assignment g iff ⟦φ⟧^{c,c_t,g}(c) = 1.

Equations

• Semantics.Tense.Perspective.InterpParams.rootDefault c = { context := c, perspective := c.time }

theorem Semantics.Tense.Perspective.InterpParams.rootDefault_covalued {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Core.Context.KContext W E P T) : (rootDefault c).perspective = (rootDefault c).context.time

Root default satisfies the co-valuation π = c_t.

theorem Semantics.Tense.Perspective.InterpParams.perspective_context_diverge {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (ip : InterpParams W E P T) (newPi : T) (hDistinct : newPi ≠ ip.context.time) : (ip.shiftPerspective newPi).perspective ≠ (ip.shiftPerspective newPi).context.time

After OP_π, c_t is unchanged — π and c_t can diverge.

theorem Semantics.Tense.Perspective.InterpParams.shiftPerspective_matches_opPi {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (ip : InterpParams W E P T) (f : Core.Reichenbach.ReichenbachFrame T) (newPi : T) (_hSync : f.perspectiveTime = ip.perspective) : (opPi f newPi).perspectiveTime = (ip.shiftPerspective newPi).perspective

OP_π on InterpParams corresponds to opPi on ReichenbachFrame.

structure Semantics.Tense.Perspective.TenseShiftProfile : Type

Cross-linguistic tense shift profile, encoding Tables 1 & 2.

Each Bool records whether a simultaneous reading of the embedded present is available in that configuration. The mechanism (OP_π shift vs SOT deletion) is recorded separately in sotDeletesPresent.

• language : String
• pastAttitude : Bool

  Present-under-past, attitude report complement

• pastRelative : Bool

  Present-under-past, relative clause

• futAttitude : Bool

  Present-under-future, attitude report complement

• futRelative : Bool

  Present-under-future, relative clause

• sotDeletesPresent : Bool

  Does the language have SOT deletion that can apply to the present? English: yes (present under future is deleted, not shifted). Modern Greek: no (the "Interpret the Present" constraint blocks deletion).

• thenPastOnly : Bool

  Is ⌈then⌉ restricted to past-oriented contexts? Japanese tooji cannot co-occur with future matrix tense.

instance Semantics.Tense.Perspective.instReprTenseShiftProfile : Repr TenseShiftProfile

Equations

• Semantics.Tense.Perspective.instReprTenseShiftProfile = { reprPrec := Semantics.Tense.Perspective.instReprTenseShiftProfile.repr }

def Semantics.Tense.Perspective.instReprTenseShiftProfile.repr : TenseShiftProfile → ℕ → Std.Format

Equations

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

instance Semantics.Tense.Perspective.instDecidableEqTenseShiftProfile : DecidableEq TenseShiftProfile

Equations

• Semantics.Tense.Perspective.instDecidableEqTenseShiftProfile = Semantics.Tense.Perspective.instDecidableEqTenseShiftProfile.decEq

def Semantics.Tense.Perspective.instDecidableEqTenseShiftProfile.decEq (x✝ x✝¹ : TenseShiftProfile) : Decidable (x✝ = x✝¹)

Equations

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

def Semantics.Tense.Perspective.instBEqTenseShiftProfile.beq : TenseShiftProfile → TenseShiftProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Tense.Perspective.instBEqTenseShiftProfile.beq x✝¹ x✝ = false

instance Semantics.Tense.Perspective.instBEqTenseShiftProfile : BEq TenseShiftProfile

Equations

• Semantics.Tense.Perspective.instBEqTenseShiftProfile = { beq := Semantics.Tense.Perspective.instBEqTenseShiftProfile.beq }

def Semantics.Tense.Perspective.greekProfile : TenseShiftProfile

Modern Greek: shifts in attitude reports (past & future) and relative clauses under future, but NOT in relative clauses under past.

Equations

• Semantics.Tense.Perspective.greekProfile = { language := "Modern Greek", pastAttitude := true, pastRelative := false, futAttitude := true, futRelative := true, sotDeletesPresent := false }

def Semantics.Tense.Perspective.hebrewProfile : TenseShiftProfile

Modern Hebrew: same pattern as Greek for shift; no SOT deletion of present.

Equations

• Semantics.Tense.Perspective.hebrewProfile = { language := "Modern Hebrew", pastAttitude := true, pastRelative := false, futAttitude := true, futRelative := true, sotDeletesPresent := false }

def Semantics.Tense.Perspective.russianProfile : TenseShiftProfile

Russian: same pattern as Greek/Hebrew for shift.

Equations

• Semantics.Tense.Perspective.russianProfile = { language := "Russian", pastAttitude := true, pastRelative := false, futAttitude := true, futRelative := true, sotDeletesPresent := false }

def Semantics.Tense.Perspective.japaneseProfile : TenseShiftProfile

Japanese: uniquely shifts in relative clauses under past too (tenses are intensional). tooji is restricted to past-oriented contexts.

Equations

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

def Semantics.Tense.Perspective.englishProfile : TenseShiftProfile

English: no shift under past; simultaneous reading under future comes from SOT deletion (will = WOLL + PRES, embedded PRES deleted by SOT).

Equations

• Semantics.Tense.Perspective.englishProfile = { language := "English", pastAttitude := false, pastRelative := false, futAttitude := true, futRelative := true, sotDeletesPresent := true }

def Semantics.Tense.Perspective.allProfiles : List TenseShiftProfile

Equations

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

theorem Semantics.Tense.Perspective.relative_shift_implies_attitude_shift (p : TenseShiftProfile) : p ∈ allProfiles → p.pastRelative = true → p.pastAttitude = true

No language allows shift in relative clauses under past unless it also allows shift in attitude reports under past.

structure Semantics.Tense.Perspective.WOLLDecomposition : Type

will = WOLL + PRES. WOLL is an intensional modal operator that:

1. Quantifies over accessible future indices (∀i' ∈ ACC(i)(t). i'_t > t)
2. Provides an intensional environment that can bind the perspective

This decomposition explains:

• Why ALL surveyed languages allow present-under-future shift: WOLL is intensional, providing the OP_π binding site even in relative clauses
• Why English ⌈then⌉ is compatible with present-under-future: the embedded PRES can be deleted by SOT (c-commanded by WOLL's PRES)

• isIntensional : Bool

  WOLL is an intensional operator (quantifies over future indices)

• containsPres : Bool

  WOLL decomposes into a modal component + PRES

instance Semantics.Tense.Perspective.instReprWOLLDecomposition : Repr WOLLDecomposition

Equations

• Semantics.Tense.Perspective.instReprWOLLDecomposition = { reprPrec := Semantics.Tense.Perspective.instReprWOLLDecomposition.repr }

def Semantics.Tense.Perspective.instReprWOLLDecomposition.repr : WOLLDecomposition → ℕ → Std.Format

Equations

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

def Semantics.Tense.Perspective.instDecidableEqWOLLDecomposition.decEq (x✝ x✝¹ : WOLLDecomposition) : Decidable (x✝ = x✝¹)

Equations

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

instance Semantics.Tense.Perspective.instDecidableEqWOLLDecomposition : DecidableEq WOLLDecomposition

Equations

• Semantics.Tense.Perspective.instDecidableEqWOLLDecomposition = Semantics.Tense.Perspective.instDecidableEqWOLLDecomposition.decEq

instance Semantics.Tense.Perspective.instBEqWOLLDecomposition : BEq WOLLDecomposition

Equations

• Semantics.Tense.Perspective.instBEqWOLLDecomposition = { beq := Semantics.Tense.Perspective.instBEqWOLLDecomposition.beq }

def Semantics.Tense.Perspective.instBEqWOLLDecomposition.beq : WOLLDecomposition → WOLLDecomposition → Bool

Equations

• Semantics.Tense.Perspective.instBEqWOLLDecomposition.beq { isIntensional := a, containsPres := a_1 } { isIntensional := b, containsPres := b_1 } = (a == b && a_1 == b_1)
• Semantics.Tense.Perspective.instBEqWOLLDecomposition.beq x✝¹ x✝ = false