Perspectival tense: presuppositions anchored to π

[TZ26] and [Zha25] interpret tenses as temporal pronouns with presuppositions anchored to a perspective parameter π (ReichenbachFrame.perspectiveTime): PRES presupposes overlap of its reference with π, PAST precedence, and temporal ⌈then⌉ disjointness (thenPresup). The operator OP_π (opPi), modelled on the context-shifting monsters of [AN04b] and [Dea20], rebinds π for a whole clause, so clausemate PRES and ⌈then⌉ always read the same π and their presuppositions clash (then_present_clash) — the ⌈then⌉-present puzzle. Deleted (SOT) tense carries no perspectival presupposition, so ⌈then⌉ remains satisfiable (thenPresup_satisfiable).

In the point approximation used throughout, overlap is equality: the PRES presupposition is ReichenbachFrame.isPresent (R = π) and the PAST presupposition is ReichenbachFrame.isPast (R < π), so theorems here are stated directly with the frame predicates. Tenses and ⌈then⌉ are temporal pronouns in one architecture ([Par73], TensePronoun): each presupposes a comparison category (Finset Ordering) of its reference against π — PAST Tense.past, PRES Tense.present, and ⌈then⌉ Core.Order.distinct, the complement of Tense.present, so the ⌈then⌉-present clash is disjointness of comparison categories.

The ⌈then⌉ presupposition

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

Temporal ⌈then⌉ presupposes that its reference is disjoint from the perspective π: the Core.Order.distinct comparison category, the complement of PRES's Tense.present ([TZ26]). This is ⌈then⌉'s own presupposition, separate from the presuppositions of any co-clausal tense; the clash with PRES arises because the temporal assertion ("during then") forces the PRES reference inside the ⌈then⌉ reference.

Equations

• Tense.Perspective.thenPresup thenRef perspective = Core.Order.holds Core.Order.distinct thenRef perspective

@[simp]

theorem Tense.Perspective.thenPresup_def {Time : Type u_1} [LinearOrder Time] (thenRef perspective : Time) : thenPresup thenRef perspective ↔ thenRef ≠ perspective

structure Tense.Perspective.ThenAdverb : Type

A ⌈then⌉-type temporal adverb: a lexical item denoting a temporal pronoun that carries the thenPresup disjointness presupposition (English then, Greek tóte, Japanese tōji, ... — [Zha25]). Entries live in Fragments/{Language}/TemporalDeictic.lean.

• form : String

  Surface form

• gloss : String

  English gloss

@[instance_reducible]

instance Tense.Perspective.instReprThenAdverb : Repr ThenAdverb

Equations

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

def Tense.Perspective.instReprThenAdverb.repr : ThenAdverb → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Tense.Perspective.instDecidableEqThenAdverb : DecidableEq ThenAdverb

Equations

• Tense.Perspective.instDecidableEqThenAdverb = Tense.Perspective.instDecidableEqThenAdverb.decEq

def Tense.Perspective.instDecidableEqThenAdverb.decEq (x✝ x✝¹ : ThenAdverb) : Decidable (x✝ = x✝¹)

Equations

• Tense.Perspective.instDecidableEqThenAdverb.decEq { form := a, gloss := a_1 } { form := b, gloss := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

OP_π: the 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.

Clash and satisfiability

theorem Tense.Perspective.then_present_clash {Time : Type u_1} [LinearOrder Time] (f : _root_.Time.ReichenbachFrame Time) {thenRef : Time} (hPres : f.isPresent) (hDuring : f.referenceTime = thenRef) (hThen : thenPresup thenRef f.perspectiveTime) : False

The ⌈then⌉-present clash. Three ingredients produce the contradiction: PRES presupposes R = π (isPresent), the temporal assertion requires the ⌈then⌉ reference to contain — in the point approximation, equal — R ("during then"), and ⌈then⌉ presupposes its reference disjoint from π.

theorem Tense.Perspective.thenPresup_satisfiable {Time : Type u_1} [LinearOrder Time] [Nontrivial Time] (perspective : Time) : ∃ (thenRef : Time), thenPresup thenRef perspective

⌈then⌉'s presupposition is satisfiable on any timeline with two points. This is why ⌈then⌉ is compatible with deleted (SOT) tense ([TZ26]): a deleted tense contributes no perspectival presupposition, leaving only thenPresup, which any reference off the perspective witnesses.