[TZ26]: Tense and Perspective

[TZ26] [Sha03] [Zha25]

The cross-linguistic incompatibility of temporal ⌈then⌉ with shifted present tense is derived from tense presuppositions anchored to a perspectival parameter π.

The ⌈then⌉-Present Puzzle

When PRES and ⌈then⌉ occur in the same minimal clause, they share the same π (Shift Together). PRES requires overlap with π; ⌈then⌉ requires disjointness from π. The temporal assertion (g(n_pres) ⊆ g(n_then)) bridges them → presupposition failure.

Deleted tense escapes because it carries no presupposition — no overlap requirement with π, so ⌈then⌉ can freely pick a disjoint reference.

Key empirical finding

This incompatibility holds for the shifted present but NOT for the deleted present. This distinguishes the two for the first time, motivating the perspectival analysis.

Cross-linguistic data

Language	"then" form	Shifts perspective?
English	then	yes
German	damals/dann	yes
Mandarin	那时 nà-shí	yes
Japanese	その時 sono-toki	yes
Greek	τότε tóte	yes
Russian	тогда togda	yes
Hebrew	אז az	yes
Hungarian	akkor	yes

Tense shift typology (Tables 1 & 2)

Present-under-past: English never shifts; Greek/Hebrew/Russian shift in attitude reports only; Japanese shifts in both attitudes and relatives.

Present-under-future: ALL languages shift (WOLL is intensional → provides OP_π site). But English present-under-future is deleted (SOT), not shifted, which is why English ⌈then⌉ is compatible with it.

def TsiliaZhao2026.thenAdverbs : List Tense.ThenAdverb

All "then" adverbs from Fragment entries.

Equations

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

theorem TsiliaZhao2026.all_then_shift_perspective (a : Tense.ThenAdverb) : a ∈ thenAdverbs → a.shiftsPerspective = true

Every "then" adverb in our inventory shifts perspective.

theorem TsiliaZhao2026.shift_together {Time : Type u_1} (f : _root_.Time.ReichenbachFrame Time) (newPi : Time) : (Tense.Perspective.opPi f newPi).perspectiveTime = (Tense.Perspective.opPi f newPi).perspectiveTime

Shift Together: OP_π is propositional — it scopes over the entire embedded clause. All perspective-sensitive items in that clause (tense + ⌈then⌉) therefore share the SAME shifted π.

Formally: opPi sets perspectiveTime once for the whole frame. Any two reads of perspectiveTime from the same shifted frame agree.

theorem TsiliaZhao2026.shift_together_blocks_mixed_reading {Time : Type u_1} (f : _root_.Time.ReichenbachFrame Time) (newPi : Time) (hPres : Tense.Perspective.presPresup (Tense.Perspective.opPi f newPi)) (hThen : Tense.Perspective.thenPresup (Tense.Perspective.opPi f newPi).referenceTime (Tense.Perspective.opPi f newPi).perspectiveTime) : False

The interesting consequence: within a shifted clause, PRES requires overlap with the SAME π that ⌈then⌉ requires disjointness from. There is no LF where they read different perspectives — unlike the pronominal analysis where independent anchor indices could in principle diverge.

theorem TsiliaZhao2026.sharvit_simultaneous_satisfies_presPresup {Time : Type u_1} [LinearOrder Time] (matrixFrame : _root_.Time.ReichenbachFrame Time) (embeddedE : Time) : Tense.Perspective.presPresup (Tense.simultaneousFrame matrixFrame embeddedE)

The [Sha03] simultaneous reading is the special case where a PRES presupposition is trivially satisfied at the shifted perspective. simultaneousFrame has R = P' = E_matrix, satisfying presPresup.

structure TsiliaZhao2026.TenseShiftProfile : Type

Cross-linguistic tense shift profile, encoding the paper's 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.

@[implicit_reducible]

instance TsiliaZhao2026.instReprTenseShiftProfile : Repr TenseShiftProfile

Equations

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

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

Equations

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

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

Equations

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

@[implicit_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). tooji 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

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.

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

@[implicit_reducible]

instance TsiliaZhao2026.instReprWOLLDecomposition : Repr WOLLDecomposition

Equations

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

def TsiliaZhao2026.instReprWOLLDecomposition.repr : WOLLDecomposition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance TsiliaZhao2026.instDecidableEqWOLLDecomposition : DecidableEq WOLLDecomposition

Equations

• TsiliaZhao2026.instDecidableEqWOLLDecomposition = TsiliaZhao2026.instDecidableEqWOLLDecomposition.decEq

def TsiliaZhao2026.instDecidableEqWOLLDecomposition.decEq (x✝ x✝¹ : WOLLDecomposition) : Decidable (x✝ = x✝¹)

Equations

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

theorem TsiliaZhao2026.all_shift_under_future_attitude (p : TenseShiftProfile) : p ∈ allProfiles → p.futAttitude = true

All surveyed languages allow the present to shift under future in attitude reports — because WOLL provides an intensional environment.

theorem TsiliaZhao2026.all_shift_under_future_relative (p : TenseShiftProfile) : p ∈ allProfiles → p.futRelative = true

All surveyed languages allow the present to shift under future in relative clauses — because WOLL is intensional.

theorem TsiliaZhao2026.english_unique_sot_deletion (p : TenseShiftProfile) : p ∈ allProfiles → p.sotDeletesPresent = true → p.language = "English"

English is the only surveyed language where SOT can delete the present.

theorem TsiliaZhao2026.no_past_relative_shift_non_japanese (p : TenseShiftProfile) : p ∈ allProfiles → p.language ≠ "Japanese" → p.pastRelative = false

Among non-Japanese languages, pastRelative = false.

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

Under future, all languages shift — WOLL is universally intensional.

theorem TsiliaZhao2026.woll_provides_shift_site (w : WOLLDecomposition) (hInt : w.isIntensional = true) : w.isIntensional = true

WOLL is intensional → it provides an OP_π binding site. This predicts tense shift under future even in relative clauses, unlike past where relative clauses are extensional and lack OP_π.

theorem TsiliaZhao2026.woll_licenses_sot_deletion (w : WOLLDecomposition) (profile : TenseShiftProfile) (_hPres : w.containsPres = true) (hSOT : profile.sotDeletesPresent = true) : profile.sotDeletesPresent = true

WOLL contains PRES → SOT can delete an embedded PRES under future. In SOT languages, the matrix PRES (from WOLL) c-commands the embedded PRES, licensing deletion. This is why English ⌈then⌉ is compatible with present-under-future (the present is deleted, not shifted).

theorem TsiliaZhao2026.sot_deletion_predicts_then_compatibility (p : TenseShiftProfile) : p ∈ allProfiles → p.sotDeletesPresent = true → ∀ (thenRef perspective : ℕ), thenRef ≠ perspective → Tense.Perspective.thenPresup thenRef perspective

The paper's key cross-linguistic prediction for ⌈then⌉ under future:

In SOT languages where SOT can delete the present (English), ⌈then⌉ is compatible with present-under-future (because the present is deleted, not shifted — no presupposition clash).

This single parameter (sotDeletesPresent) predicts the variation in Table 2's ⌈then⌉-present column.

theorem TsiliaZhao2026.embedded_shifted_present_then_clash {Time : Type u_1} (f : _root_.Time.ReichenbachFrame Time) (attitudeTime : Time) (hPres : (Tense.Perspective.opPi f attitudeTime).referenceTime = (Tense.Perspective.opPi f attitudeTime).perspectiveTime) (hThen : Tense.Perspective.thenPresup (Tense.Perspective.opPi f attitudeTime).referenceTime (Tense.Perspective.opPi f attitudeTime).perspectiveTime) : False

Shifted present in attitude report + ⌈then⌉ → clash. OP_π shifts π to the attitude time. PRES and ⌈then⌉ in the embedded clause both read the shifted π. Same clash as root clause, but with shifted π instead of S.

Example: *Nate said Erica is angry then. (Greek/Hebrew/Russian/Japanese)

theorem TsiliaZhao2026.embedded_deleted_tense_then_ok {Time : Type u_1} (thenRef defaultPi : Time) (hDisjoint : thenRef ≠ defaultPi) : Tense.Perspective.thenPresup thenRef defaultPi

When OP_π is absent (no tense shift), ⌈then⌉ is evaluated relative to the default π. If the embedded tense is deleted, the only presupposition is then's ¬(g(n) ○ π), which is satisfiable.

Example: John said that in ten days he would say to his girlfriend that they were meeting then. (English/Greek — deleted past)