@cite{abusch-1997}: Sequence of Tense and Temporal De Re

@cite{abusch-1997} @cite{sharvit-2003}

Abusch's theory: tense morphemes are temporal pronouns (variables with presupposed constraints and binding modes). The key innovation is temporal de re: tense can take wide scope over attitude operators via res movement, just as DPs can scope out of attitude complements.

Core Mechanisms

1. Tense as pronoun: TensePronoun with variable index, constraint, mode
2. Relation transmission: attitude verb transmits event time as new eval time
3. Upper Limit Constraint (ULC): embedded R ≤ matrix E (from branching futures)
4. Temporal de re: tense variable in res position of attitude

Derivation Theorems

• Shifted reading: free past variable with presupposition against eval time
• Simultaneous reading: bound variable receives matrix event time
• Double-access: indexical present + attitude binding
• ULC: blocks forward-shifted readings
• Temporal de re: res movement for wide-scope tense

Limitations

• Relative clause tense: Sharvit's challenge (the mechanism doesn't extend straightforwardly to relative clauses where the tense takes the perspective of a participant)
• Modal-tense interaction: not addressed in original framework
• Counterfactual tense: not addressed

structure Semantics.Tense.TemporalDeRe.TemporalDeRe (Time : Type u_1) : Type u_1

Abusch's temporal de re: a tense variable can take wide scope over an attitude operator by occupying the res position.

The res has three components:

• referent: the time denoted (resolved in the matrix context)
• evalTime: the evaluation time in the embedded context
• constraint: the presupposed temporal relation

This parallels individual de re: "John believes the president is wise" where "the president" is evaluated in the actual world, not in John's belief worlds. Similarly, temporal de re evaluates tense in the matrix temporal context.

• referent : Time

  The time referred to (resolved in matrix context)

• evalTime : Time

  The evaluation time (shifted by attitude)

• constraint : Core.Tense.GramTense

  The temporal constraint (past/present/future)

def Semantics.Tense.TemporalDeRe.TemporalDeRe.isFelicitous {Time : Type u_1} [LinearOrder Time] (dr : TemporalDeRe Time) : Prop

A temporal de re is felicitous when the constraint is satisfied in the matrix context (referent checked against matrix eval time).

Equations

• dr.isFelicitous = dr.constraint.constrains dr.referent dr.evalTime

def Semantics.Tense.TemporalDeRe.relationTransmission {Time : Type u_1} (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) (g : Core.Tense.TemporalAssignment Time) (evalIdx : ℕ) : Core.Tense.TemporalAssignment Time

Abusch's relation transmission: an attitude verb transmits its event time as the new evaluation time for the embedded clause. This is the semantic effect of the attitude on temporal interpretation.

Equations

• Semantics.Tense.TemporalDeRe.relationTransmission matrixFrame g evalIdx = Core.Tense.updateTemporal g evalIdx matrixFrame.eventTime

theorem Semantics.Tense.TemporalDeRe.relationTransmission_shifts_eval {Time : Type u_1} (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) (g : Core.Tense.TemporalAssignment Time) (evalIdx : ℕ) : Core.Tense.interpTense evalIdx (relationTransmission matrixFrame g evalIdx) = matrixFrame.eventTime

After relation transmission, the eval time IS the matrix event time.

theorem Semantics.Tense.TemporalDeRe.relationTransmission_is_evalTime_update {Time : Type u_1} (tp : Core.Tense.TensePronoun) (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) (g : Core.Tense.TemporalAssignment Time) : tp.evalTime (relationTransmission matrixFrame g tp.evalTimeIndex) = matrixFrame.eventTime

Relation transmission = updating the eval time index on TensePronoun. This bridges Abusch's mechanism to the evalTimeIndex field.

def Semantics.Tense.TemporalDeRe.abuschiULC {Time : Type u_1} [LE Time] (embeddedR evalTime : Time) : Prop

Abusch's ULC: in intensional contexts, tense reference cannot exceed the local evaluation time. From branching futures: at the attitude event time, future branches diverge, so no time beyond the attitude time is accessible across all doxastic alternatives.

Equations

• Semantics.Tense.TemporalDeRe.abuschiULC embeddedR evalTime = Semantics.Tense.upperLimitConstraint embeddedR evalTime

theorem Semantics.Tense.TemporalDeRe.abuschiULC_eq_ulc {Time : Type u_1} [LE Time] (embeddedR evalTime : Time) : abuschiULC embeddedR evalTime ↔ upperLimitConstraint embeddedR evalTime

The ULC is equivalent to the shared formulation.

theorem Semantics.Tense.TemporalDeRe.abusch_derives_shifted {Time : Type u_1} [LinearOrder Time] (tp : Core.Tense.TensePronoun) (g : Core.Tense.TemporalAssignment Time) (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) (_hPast : tp.constraint = Core.Tense.GramTense.past) (hPresup : tp.resolve g < matrixFrame.eventTime) : (embeddedFrame matrixFrame (tp.resolve g) (tp.resolve g)).isPast

Abusch derives the shifted reading: a free past variable with presupposition checked against the (shifted) eval time. The past constraint gives R < evalTime = matrixE.

theorem Semantics.Tense.TemporalDeRe.abusch_derives_simultaneous {Time : Type u_1} (tp : Core.Tense.TensePronoun) (g : Core.Tense.TemporalAssignment Time) (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) (hBind : tp.resolve g = matrixFrame.eventTime) : (embeddedFrame matrixFrame (tp.resolve g) (tp.resolve g)).isPresent

Abusch derives the simultaneous reading: a bound variable receives the matrix event time via lambda abstraction.

theorem Semantics.Tense.TemporalDeRe.abusch_derives_simultaneous_via_binding {Time : Type u_1} (tp : Core.Tense.TensePronoun) (g : Core.Tense.TemporalAssignment Time) (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) : tp.resolve (Core.Tense.updateTemporal g tp.varIndex matrixFrame.eventTime) = matrixFrame.eventTime

Abusch derives the simultaneous reading via the bound variable mechanism: updating the temporal assignment so the tense variable receives matrix E.

theorem Semantics.Tense.TemporalDeRe.abusch_derives_double_access {Time : Type u_1} (p : Time → Prop) (speechTime matrixEventTime : Time) (h_speech : p speechTime) (h_matrix : p matrixEventTime) : Core.Tense.doubleAccess p speechTime matrixEventTime

Abusch derives double-access: indexical present requires truth at BOTH speech time (indexical rigidity) AND matrix event time (attitude accessibility).

theorem Semantics.Tense.TemporalDeRe.abusch_blocks_forward_shift {Time : Type u_1} [LinearOrder Time] (embeddedR matrixE : Time) (h_ulc : abuschiULC embeddedR matrixE) (h_forward : embeddedR > matrixE) : False

Abusch's ULC blocks the forward-shifted reading: if R > evalTime, the ULC (R ≤ evalTime) is violated.

theorem Semantics.Tense.TemporalDeRe.abusch_derives_temporal_de_re {Time : Type u_1} [LinearOrder Time] (dr : TemporalDeRe Time) (hPast : dr.constraint = Core.Tense.GramTense.past) (hBefore : dr.referent < dr.evalTime) : dr.isFelicitous

Abusch derives temporal de re: the tense variable in res position is evaluated in the matrix context, giving wide-scope temporal reference. When the res referent satisfies the past constraint against the matrix eval time, the de re reading is felicitous.