Perspectival Tense Theory

[TZ26] [Sha03] [Zha25] [AN04b] [Dea20]

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, [AN04b])
• 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)

Tense Presuppositions

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

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

Equations

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

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

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

Equations

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

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

The PRES presupposition is definitionally equal to isPresent.

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

The PAST presupposition is definitionally equal to isPast.

OP_π: Perspective-Shifting Operator

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

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

Equations

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

theorem Tense.Perspective.opPi_eq_embeddedFrame {Time : Type u_1} (matrixFrame : _root_.Time.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.

⌈then⌉ Presupposition

def 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

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

Core Clash Theorems

theorem 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 Tense.Perspective.then_perspective_clash {Time : Type u_1} (f : _root_.Time.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.

Deleted vs. Shifted Tense

inductive 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; imposes no temporal presupposition at all (there is no definedness condition to state, which is why then_deleted_tense_compatible below needs no presupposition hypothesis).

@[implicit_reducible]

instance Tense.Perspective.instDecidableEqEmbeddedTenseStatus : DecidableEq EmbeddedTenseStatus

Equations

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

@[implicit_reducible]

instance Tense.Perspective.instReprEmbeddedTenseStatus : Repr EmbeddedTenseStatus

Equations

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

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

Equations

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

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

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

Equations

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

theorem 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 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.

Bridge to PartialProp

def Tense.Perspective.presAsPartialProp {Time : Type u_1} [DecidableEq Time] (f : _root_.Time.ReichenbachFrame Time) : Semantics.Presupposition.PartialProp Unit

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

Equations

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

theorem Tense.Perspective.presAsPartialProp_defined_iff {Time : Type u_1} [DecidableEq Time] (f : _root_.Time.ReichenbachFrame Time) : (presAsPartialProp f).presup () = (true = true) ↔ f.referenceTime = f.perspectiveTime

The PartialProp encoding is defined iff the PRES presupposition holds.

Interpretation Parameters: c and π

structure 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, [AN04b]) 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 : Semantics.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 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 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 : Semantics.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 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 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 : Semantics.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 Tense.Perspective.InterpParams.rootDefault {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (c : Semantics.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

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

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

Root default satisfies the co-valuation π = c_t.

theorem 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 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 : Time.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.