Tsilia & Zhao 2026: Tense and perspective

[TZ26] solve the ⌈then⌉-present puzzle: temporal ⌈then⌉ is incompatible with the present tense across languages, even where the present shifts (denoting the attitude 'now' rather than utterance time) — yet compatible in the very same language (Modern Greek) with deleted (SOT) tense, distinguishing the shifted present from deleted tense for the first time. Tenses and ⌈then⌉ are interpreted relative to a temporal perspective π; the operator OP_π rebinds π clause-wide, so a shifted PRES and a clausemate ⌈then⌉ read the SAME π and their overlap/disjointness presuppositions clash — a shift-together effect in the temporal domain, after the indexical-shift monsters of [AN04b] and [Dea20] (shifted_present_blocks_then). Deleted tense has no perspectival presupposition, so ⌈then⌉ stays satisfiable (Tense.Perspective.thenPresup_satisfiable). The [Sha03] simultaneous reading is the case where the shifted PRES presupposition holds trivially (Tense.simultaneousFrame_isPresent).

Cross-linguistic data

The ⌈then⌉ inventory is Zhao2025.thenAdverbs (Greek tóte, Hebrew az, Russian togda, Japanese tōji, English then). The tense-shift typology (TenseShiftProfile): present-under-past shifts in attitude reports in Greek, Hebrew and Russian, also in relative clauses in Japanese, and never in English; present-under-future shifts everywhere, because will = WOLL + PRES and WOLL is intensional, providing the OP_π site even in relative clauses. The English present under future is deleted by SOT (c-commanded by WOLL's PRES), not shifted — which is why English ⌈then⌉ tolerates present-under-future.

Shift together

theorem TsiliaZhao2026.shifted_present_blocks_then {Time : Type u_1} [LinearOrder Time] (f : _root_.Time.ReichenbachFrame Time) (attitudeTime : Time) (hPres : (Tense.Perspective.opPi f attitudeTime).isPresent) : ¬∃ (thenRef : Time), (Tense.Perspective.opPi f attitudeTime).referenceTime = thenRef ∧ Tense.Perspective.thenPresup thenRef (Tense.Perspective.opPi f attitudeTime).perspectiveTime

A shifted present blocks ⌈then⌉: OP_π rebinds π for the whole frame, so the shifted PRES (R = π') and a clausemate ⌈then⌉ (reference disjoint from π') read the same π' — no reference satisfies both the "during then" containment and disjointness. *Nate said Erica is angry (then).

Tense-shift typology

structure TsiliaZhao2026.TenseShiftProfile : Type

A language's tense-shift profile: whether a simultaneous reading of an embedded present is available in each of the four past/future × attitude/relative configurations, and whether the language's SOT rule can delete a present.

• language : String

  Language name

• 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 tōji cannot co-occur with future matrix tense.

def TsiliaZhao2026.instReprTenseShiftProfile.repr : TenseShiftProfile → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance TsiliaZhao2026.instReprTenseShiftProfile : Repr TenseShiftProfile

Equations

• TsiliaZhao2026.instReprTenseShiftProfile = { reprPrec := TsiliaZhao2026.instReprTenseShiftProfile.repr }

def TsiliaZhao2026.instDecidableEqTenseShiftProfile.decEq (x✝ x✝¹ : TenseShiftProfile) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TsiliaZhao2026.instDecidableEqTenseShiftProfile : DecidableEq TenseShiftProfile

Equations

• TsiliaZhao2026.instDecidableEqTenseShiftProfile = TsiliaZhao2026.instDecidableEqTenseShiftProfile.decEq

def TsiliaZhao2026.greekProfile : TenseShiftProfile

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

Equations

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

def TsiliaZhao2026.hebrewProfile : TenseShiftProfile

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

Equations

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

def TsiliaZhao2026.russianProfile : TenseShiftProfile

Russian: same pattern as Greek/Hebrew for shift.

Equations

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

def TsiliaZhao2026.japaneseProfile : TenseShiftProfile

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

Equations

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

def TsiliaZhao2026.englishProfile : TenseShiftProfile

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

Equations

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

def TsiliaZhao2026.allProfiles : List TenseShiftProfile

The surveyed languages' tense-shift profiles.

Equations

• TsiliaZhao2026.allProfiles = [TsiliaZhao2026.greekProfile, TsiliaZhao2026.hebrewProfile, TsiliaZhao2026.russianProfile, TsiliaZhao2026.japaneseProfile, TsiliaZhao2026.englishProfile]

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

theorem TsiliaZhao2026.universal_shift_under_future (p : TenseShiftProfile) : p ∈ allProfiles → p.futAttitude = true ∧ p.futRelative = true

Under future, all surveyed languages shift, in attitude reports and relative clauses alike — WOLL is universally intensional.

theorem TsiliaZhao2026.sot_deletes_present_unique (p : TenseShiftProfile) : p ∈ allProfiles → p.sotDeletesPresent = true → p = englishProfile

English is the only surveyed language whose SOT deletes the present.

theorem TsiliaZhao2026.past_relative_shift_unique (p : TenseShiftProfile) : p ∈ allProfiles → p.pastRelative = true → p = japaneseProfile

Japanese is the only surveyed language that shifts the present in a relative clause under past.

Perspective is not context

structure TsiliaZhao2026.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 indexicals, [AN04b]) and perspective π (for tense) are independent parameters: shiftPerspective preserves context, and shiftContext preserves perspective. This is the paper's argument that the perspective can be identified with neither the context nor the evaluation index: tense shift is possible without indexical shift (Modern Greek shifts the present but never τώρα 'now'), and neither shift is obligatory.

• 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 TsiliaZhao2026.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.

Equations

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

def TsiliaZhao2026.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 π.

Equations

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

theorem TsiliaZhao2026.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): tense shift does not entail indexical shift.

theorem TsiliaZhao2026.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 TsiliaZhao2026.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 Truth Convention evaluates ⟦φ⟧ relative to c and π = c_t.

Equations

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

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