Then-Present Puzzle (@cite{zhao-2025})

@cite{zhao-2025} @cite{kiparsky-2002}

Temporal ⌈then⌉ is cross-linguistically incompatible with present tense.

The puzzle

⌈then⌉ presupposes ¬(g(n) ○ π): its reference is disjoint from the temporal perspective. PRES presupposes g(n) ○ π: overlap with the perspective. When composition forces the PRES reference inside the then reference ("during then"), the presuppositions clash.

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

def Phenomena.TenseAspect.Studies.Zhao2025ThenPresent.thenAdverbs : List Semantics.Tense.ThenAdverb

All "then" adverbs from Fragment entries.

Equations

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

theorem Phenomena.TenseAspect.Studies.Zhao2025ThenPresent.all_then_shift_perspective (a : Semantics.Tense.ThenAdverb) : a ∈ thenAdverbs → a.shiftsPerspective = true

Every "then" adverb in our inventory shifts perspective.

theorem Phenomena.TenseAspect.Studies.Zhao2025ThenPresent.then_present_incompatible {Time : Type u_1} [LinearOrder Time] (f : Core.Reichenbach.ReichenbachFrame Time) (_hPresent : f.isPresent) (hSimple : f.isSimpleCase) (hShift : f.perspectiveTime ≠ f.speechTime) : False

Root clause: PRES (R = P) + isSimpleCase (P = S) means R = S. ⌈then⌉ requires its reference ≠ π = S. Since composition puts the PRES reference inside the then reference, both equal S in the point model, contradicting then's presupposition.

theorem Phenomena.TenseAspect.Studies.Zhao2025ThenPresent.root_clause_is_presuppositional_corollary {Time : Type u_1} (f : Core.Reichenbach.ReichenbachFrame Time) (hSimple : f.isSimpleCase) (hThen : f.perspectiveTime ≠ f.speechTime) : False

The root-clause incompatibility is a corollary of the general perspective clash: in root clauses, π = S (no OP_π), so localEval = S and then_perspective_clash applies.

theorem Phenomena.TenseAspect.Studies.Zhao2025ThenPresent.then_compatible_with_deleted_tense {Time : Type u_1} (thenRef perspective : Time) (hDisjoint : thenRef ≠ perspective) : Semantics.Tense.Perspective.thenPresup thenRef perspective

⌈then⌉ + deleted tense is compatible: when SOT deletes the embedded tense, no presupposition anchors it to π, so ⌈then⌉ can freely pick a reference disjoint from π.