@cite{tsilia-zhao-sharvit-2026}: Tense and Perspective

@cite{tsilia-zhao-sharvit-2026} @cite{sharvit-2003} @cite{zhao-2025}The cross-linguistic incompatibility of temporal ⌈then⌉ with shifted present tense is derived from tense presuppositions anchored to a perspectival parameter π. This creates the architecturally significant import edge from tense theory to Core.Presupposition.

Core Insight

Tenses are presupposition triggers:

• PRES presupposes R = P (reference time = perspective time)
• PAST presupposes R < P

OP_π shifts the perspective parameter to the local evaluation time. ⌈then⌉ presupposes that π has been shifted away from the default (P ≠ S) AND that R = P. The incompatibility arises because OP_π forces P = local evaluation time, while ⌈then⌉ requires P ≠ local evaluation time — a direct contradiction.

Connection to @cite{sharvit-2003}

Sharvit's simultaneous tense is the special case where the embedded tense presupposition is trivially satisfied at the shifted perspective: the simultaneous reading has R = P' where P' = E_matrix, which satisfies the PRES presupposition at the shifted π.

def Semantics.Tense.TsiliaEtAl2026.presPresup {Time : Type u_1} (f : Core.Reichenbach.ReichenbachFrame Time) : Prop

PRES presupposes R = P: the reference time equals the perspective time. This is a point-approximation of the paper's t ○ π overlap condition.

Equations

• Semantics.Tense.TsiliaEtAl2026.presPresup f = (f.referenceTime = f.perspectiveTime)

def Semantics.Tense.TsiliaEtAl2026.pastPresup {Time : Type u_1} [LT Time] (f : Core.Reichenbach.ReichenbachFrame Time) : Prop

PAST presupposes R < P: the reference time precedes the perspective time.

Equations

• Semantics.Tense.TsiliaEtAl2026.pastPresup f = (f.referenceTime < f.perspectiveTime)

theorem Semantics.Tense.TsiliaEtAl2026.presPresup_iff_isPresent {Time : Type u_1} [LinearOrder Time] (f : Core.Reichenbach.ReichenbachFrame Time) : presPresup f ↔ f.isPresent

The PRES presupposition is definitionally equal to isPresent.

theorem Semantics.Tense.TsiliaEtAl2026.pastPresup_iff_isPast {Time : Type u_1} [LinearOrder Time] (f : Core.Reichenbach.ReichenbachFrame Time) : pastPresup f ↔ f.isPast

The PAST presupposition is definitionally equal to isPast.

def Semantics.Tense.TsiliaEtAl2026.opPi {Time : Type u_1} (f : Core.Reichenbach.ReichenbachFrame Time) (newPi : Time) : Core.Reichenbach.ReichenbachFrame Time

OP_π shifts the perspective time to a new value. Under attitude verbs, this sets P' = E_matrix (the matrix event time), so that embedded tenses are evaluated relative to the attitude time.

Equations

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

theorem Semantics.Tense.TsiliaEtAl2026.opPi_eq_embeddedFrame {Time : Type u_1} (matrixFrame : Core.Reichenbach.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. embeddedFrame already sets perspectiveTime := matrixFrame.eventTime.

def Semantics.Tense.TsiliaEtAl2026.thenPresup {Time : Type u_1} (f : Core.Reichenbach.ReichenbachFrame Time) : Prop

⌈then⌉ presupposes:

1. R = P (overlap with perspective — same as PRES)
2. P ≠ S (perspective has been shifted from default)

The second conjunct captures the anaphoric/non-default requirement: ⌈then⌉ requires a contextually shifted perspective point.

Equations

• Semantics.Tense.TsiliaEtAl2026.thenPresup f = (f.referenceTime = f.perspectiveTime ∧ f.perspectiveTime ≠ f.speechTime)

inductive Semantics.Tense.TsiliaEtAl2026.EmbeddedTenseStatus : Type

Status of an embedded tense morpheme.

• shifted : EmbeddedTenseStatus

  Tense present with presupposition anchored to shifted π

• deleted : EmbeddedTenseStatus

  Tense deleted by SOT; no temporal presupposition

instance Semantics.Tense.TsiliaEtAl2026.instDecidableEqEmbeddedTenseStatus : DecidableEq EmbeddedTenseStatus

Equations

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

instance Semantics.Tense.TsiliaEtAl2026.instReprEmbeddedTenseStatus : Repr EmbeddedTenseStatus

Equations

• Semantics.Tense.TsiliaEtAl2026.instReprEmbeddedTenseStatus = { reprPrec := Semantics.Tense.TsiliaEtAl2026.instReprEmbeddedTenseStatus.repr }

def Semantics.Tense.TsiliaEtAl2026.instReprEmbeddedTenseStatus.repr : EmbeddedTenseStatus → ℕ → Std.Format

Equations

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

def Semantics.Tense.TsiliaEtAl2026.instBEqEmbeddedTenseStatus.beq : EmbeddedTenseStatus → EmbeddedTenseStatus → Bool

Equations

• Semantics.Tense.TsiliaEtAl2026.instBEqEmbeddedTenseStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Tense.TsiliaEtAl2026.instBEqEmbeddedTenseStatus : BEq EmbeddedTenseStatus

Equations

• Semantics.Tense.TsiliaEtAl2026.instBEqEmbeddedTenseStatus = { beq := Semantics.Tense.TsiliaEtAl2026.instBEqEmbeddedTenseStatus.beq }

def Semantics.Tense.TsiliaEtAl2026.shiftedTensePresup {Time : Type u_1} [LT Time] (f : Core.Reichenbach.ReichenbachFrame Time) (isPres : Bool) : Prop

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

Equations

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

theorem Semantics.Tense.TsiliaEtAl2026.deletedTensePresup : True

A deleted tense has no temporal presupposition — trivially satisfied.

theorem Semantics.Tense.TsiliaEtAl2026.then_perspective_clash {Time : Type u_1} (f : Core.Reichenbach.ReichenbachFrame Time) (localEval : Time) (hOP : f.perspectiveTime = localEval) (hThen : f.perspectiveTime ≠ localEval) : False

General then-perspective incompatibility: OP_π sets P = localEval, ⌈then⌉ requires P ≠ localEval → contradiction.

The root-clause case (in TenseAspect/Studies/Zhao2025ThenPresent.lean) has localEval = S and hOP = isSimpleCase. The embedded case has localEval = attitudeTime and hOP comes from OP_π.

theorem Semantics.Tense.TsiliaEtAl2026.then_deleted_tense_compatible {Time : Type u_1} (f : Core.Reichenbach.ReichenbachFrame Time) (hShifted : f.perspectiveTime ≠ f.speechTime) (hOverlap : f.referenceTime = f.perspectiveTime) : thenPresup f

⌈then⌉ + deleted tense → compatible. Deleted tense has no presupposition, so OP_π is not required, and ⌈then⌉ can freely set P to a contextually salient past time.

def Semantics.Tense.TsiliaEtAl2026.presAsPrProp {Time : Type u_1} [DecidableEq Time] (f : Core.Reichenbach.ReichenbachFrame Time) : Core.Presupposition.PrProp Unit

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

Equations

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

theorem Semantics.Tense.TsiliaEtAl2026.presAsPrProp_defined_iff {Time : Type u_1} [DecidableEq Time] (f : Core.Reichenbach.ReichenbachFrame Time) : (presAsPrProp f).presup () = true ↔ f.referenceTime = f.perspectiveTime

The PrProp encoding is defined iff the PRES presupposition holds.

def Semantics.Tense.TsiliaEtAl2026.TsiliaEtAl2026 : TenseTheory

@cite{tsilia-zhao-sharvit-2026} identity card. The theory treats tenses as presupposition triggers (the key innovation) and uses SOT deletion for the then-deleted tense compatibility.

Equations

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

theorem Semantics.Tense.TsiliaEtAl2026.sharvit_simultaneous_satisfies_presPresup {Time : Type u_1} [LinearOrder Time] (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) (embeddedE : Time) : presPresup (simultaneousFrame matrixFrame embeddedE)

The @cite{sharvit-2003} 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.