Tense Theory Infrastructure: Shared Types

[Abu97] [Hei94a] [Ogi89] [Par73]

Shared embedding infrastructure for the tense theories: embedded Reichenbach frames, the shifted/simultaneous reading split, the upper limit constraint, and the projections connecting TensePronoun to the SOT frame constructors.

Main declarations

• embeddedFrame: the frame of a clause embedded under an attitude verb (P' = matrix E); simultaneousFrame and shiftedFrame specialize it
• EmbeddedTenseReading, availableReadings: the SOT-parameterized shifted/simultaneous split
• upperLimitConstraint: [Abu97]'s ULC, presuppositional construal
• AttitudeTemporalSemantics: how an attitude verb shifts eval time

AttitudeTemporalSemantics

structure Tense.AttitudeTemporalSemantics (Time : Type u_1) : Type u_1

How an attitude verb shifts the evaluation time for its complement.

All six theories agree that attitude verbs modify the temporal evaluation context of their complement. They differ in the formal mechanism (eval time shift, feature checking, deletion, binding). This structure captures the shared interface.

• shiftEvalTime : _root_.Time.ReichenbachFrame Time → Time

  Given a matrix Reichenbach frame, compute the eval time for the embedded clause. Typically = matrix event time.

• embeddedConstraint : Time → Time → Prop

  The temporal constraint imposed on the embedded clause: embeddedRefTime must stand in this relation to the shifted eval time.

inductive Tense.EmbeddedTenseReading : Type

The two available readings for embedded past under past.

When past tense appears in the complement of a past-tense attitude verb, the embedded past can be interpreted as:

• shifted: the embedded event occurred BEFORE the matrix event (R' < P' = E_matrix)
• simultaneous: the embedded event occurred AT the matrix event time (R' = P' = E_matrix), via SOT deletion ([Ogi89], §11.2 (83))

• shifted : EmbeddedTenseReading
• simultaneous : EmbeddedTenseReading

@[implicit_reducible]

instance Tense.instDecidableEqEmbeddedTenseReading : DecidableEq EmbeddedTenseReading

Equations

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

@[implicit_reducible]

instance Tense.instReprEmbeddedTenseReading : Repr EmbeddedTenseReading

Equations

• Tense.instReprEmbeddedTenseReading = { reprPrec := Tense.instReprEmbeddedTenseReading.repr }

def Tense.instReprEmbeddedTenseReading.repr : EmbeddedTenseReading → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Tense.instInhabitedEmbeddedTenseReading : Inhabited EmbeddedTenseReading

Equations

• Tense.instInhabitedEmbeddedTenseReading = { default := Tense.instInhabitedEmbeddedTenseReading.default }

def Tense.standardShift {Time : Type u_1} : AttitudeTemporalSemantics Time

Standard eval time shift: embedded eval time = matrix event time. This is the default across all six theories.

Equations

• Tense.standardShift = { shiftEvalTime := fun (f : _root_.Time.ReichenbachFrame Time) => f.eventTime, embeddedConstraint := fun (_embR _evalT : Time) => True }

Embedded Frames

def Tense.embeddedFrame {Time : Type u_1} (matrixFrame : _root_.Time.ReichenbachFrame Time) (embeddedR embeddedE : Time) : _root_.Time.ReichenbachFrame Time

Construct the Reichenbach frame for an embedded clause under an attitude verb.

The key operation: embedded perspective time P' = matrix event time E. The embedded clause's tense locates its R' relative to P' = E_matrix, not relative to S (speech time).

embeddedR and embeddedE are the embedded clause's reference and event times, determined by its tense and aspect.

Equations

• Tense.embeddedFrame matrixFrame embeddedR embeddedE = { speechTime := matrixFrame.speechTime, perspectiveTime := matrixFrame.eventTime, referenceTime := embeddedR, eventTime := embeddedE }

Embedded Tense Readings

def Tense.availableReadings (param : SOTParameter) : List EmbeddedTenseReading

Available readings depend on the SOT parameter of the language.

SOT languages (English): both shifted and simultaneous readings. Non-SOT languages (Japanese): only shifted (absolute tense).

Equations

• Tense.availableReadings Tense.SOTParameter.relative = [Tense.EmbeddedTenseReading.shifted, Tense.EmbeddedTenseReading.simultaneous]
• Tense.availableReadings Tense.SOTParameter.absolute = [Tense.EmbeddedTenseReading.shifted]

Reading-Specific Frames

def Tense.simultaneousFrame {Time : Type u_1} (matrixFrame : _root_.Time.ReichenbachFrame Time) (embeddedE : Time) : _root_.Time.ReichenbachFrame Time

The simultaneous reading: embedded R = matrix E.

"John said Mary was sick" (she was sick AT THE TIME of saying). The embedded reference time equals the matrix event time, so embedded tense = PRESENT relative to embedded P. embeddedFrame with R' = E_matrix.

Equations

• Tense.simultaneousFrame matrixFrame embeddedE = Tense.embeddedFrame matrixFrame matrixFrame.eventTime embeddedE

def Tense.shiftedFrame {Time : Type u_1} (matrixFrame : _root_.Time.ReichenbachFrame Time) (embeddedR embeddedE : Time) : _root_.Time.ReichenbachFrame Time

The shifted reading: embedded R < matrix E.

"John said Mary had been sick" (she was sick BEFORE the saying). The embedded reference time precedes the matrix event time, so embedded tense = PAST relative to embedded P. Definitionally embeddedFrame; the inequality R' < E_matrix is a hypothesis at use sites, not enforced by the constructor.

Equations

• Tense.shiftedFrame matrixFrame embeddedR embeddedE = Tense.embeddedFrame matrixFrame embeddedR embeddedE

Perspective Shift Derivations

theorem Tense.past_under_past_shifted_is_past {Time : Type u_1} [LinearOrder Time] (S P R E R' : Time) (h_root : P = S) (h_matrix_past : R < P) (h_perfective : E ≤ R) (h_shifted : R' < E) : R' < S

In a past-under-past configuration with the shifted reading, the embedded reference time is past relative to speech time.

Derivation: R' < E_matrix ≤ R_matrix < P_matrix = S Therefore R' < S, which is PAST relative to speech time.

theorem Tense.past_under_past_simultaneous_is_past {Time : Type u_1} [LinearOrder Time] (S P R E R' : Time) (h_root : P = S) (h_matrix_past : R < P) (h_perfective : E ≤ R) (h_simultaneous : R' = E) : R' < S

In a past-under-past configuration with the simultaneous reading, the embedded reference time is still past relative to speech time.

Derivation: R' = E_matrix ≤ R_matrix < P_matrix = S Therefore R' < S.

theorem Tense.simultaneousFrame_isPresent {Time : Type u_1} (matrixFrame : _root_.Time.ReichenbachFrame Time) (embeddedE : Time) : (simultaneousFrame matrixFrame embeddedE).isPresent

The simultaneous frame satisfies PRESENT (R = P) relative to embedded P.

Available Readings Theorems

theorem Tense.sot_simultaneous_available : EmbeddedTenseReading.simultaneous ∈ availableReadings SOTParameter.relative

In SOT languages, the simultaneous reading is available.

theorem Tense.sot_shifted_available : EmbeddedTenseReading.shifted ∈ availableReadings SOTParameter.relative

In SOT languages, the shifted reading is available.

theorem Tense.nonSOT_only_shifted : availableReadings SOTParameter.absolute = [EmbeddedTenseReading.shifted]

In non-SOT languages, only the shifted reading is available.

theorem Tense.nonSOT_no_simultaneous : EmbeddedTenseReading.simultaneous ∉ availableReadings SOTParameter.absolute

Non-SOT languages do not have the simultaneous reading.

Upper Limit Constraint ([Abu97])

The Upper Limit Constraint is stated by [Abu97] §7 (p. 25): "the now of an epistemic alternative is an upper limit for the denotation of tenses". The motivation is branching futures: at the now of an intensional context, future branches diverge across epistemic alternatives, so forward reference past the now is unsupported. The presuppositional construal — ULC as a constraint on definedness of semantic values, projecting via Karttunen-Heim — is due to [Hei94a]; [Abu97] fn 20 endorses this construal.

ULC: embedded R' ≤ matrix E (= embedded P).

Note on faithfulness: the value-level reduction embeddedR ≤ matrixE strips the modal-alternative quantification Abusch's formulation carries (the "now of an epistemic alternative" quantifies over doxastic alternatives). A modal-layer formulation (over HistoricalAlternatives W Time, à la [Kle16]'s actualHistoryBase) would be more faithful to the original; deferred future work.

@[reducible, inline]

abbrev Tense.upperLimitConstraint {Time : Type u_1} [LE Time] (embeddedR matrixE : Time) : Prop

The Upper Limit Constraint.

Stated by [Abu97] §7 ("the now of an epistemic alternative is an upper limit for the denotation of tenses"); presuppositional construal due to [Hei94a], endorsed by Abusch 1997 fn 20. The current value-level reduction is embeddedR ≤ matrixE against bare [LE Time].

Equations

• Tense.upperLimitConstraint embeddedR matrixE = (embeddedR ≤ matrixE)

theorem Tense.ulc_blocks_forward_shift {Time : Type u_1} [LinearOrder Time] (embeddedR matrixE : Time) (h_ulc : upperLimitConstraint embeddedR matrixE) (h_forward : embeddedR > matrixE) : False

The ULC blocks the forward-shifted reading. If embedded R' must satisfy R' ≤ E_matrix (ULC) AND R' > E_matrix (forward shift), contradiction.

theorem Tense.shifted_satisfies_ulc {Time : Type u_1} [Preorder Time] (embeddedR matrixE : Time) (h : embeddedR < matrixE) : upperLimitConstraint embeddedR matrixE

Shifted reading satisfies ULC: R' < E_matrix → R' ≤ E_matrix.

theorem Tense.simultaneous_satisfies_ulc {Time : Type u_1} [Preorder Time] (embeddedR matrixE : Time) (h : embeddedR = matrixE) : upperLimitConstraint embeddedR matrixE

Simultaneous reading satisfies ULC: R' = E_matrix → R' ≤ E_matrix.

TensePronoun Projections onto SOT Frames

The TensePronoun type in Tense unifies the five views of tense. The following theorems show that simultaneousFrame and shiftedFrame are projections of specific tense pronouns — a bound present pronoun gives the simultaneous reading; a free past pronoun gives the shifted reading.

theorem Tense.simultaneousFrame_from_tense_pronoun {Time : Type u_1} (matrixFrame : _root_.Time.ReichenbachFrame Time) (g : TemporalAssignment Time) (n : ℕ) (embeddedE : Time) (tp : TensePronoun) (hIdx : tp.varIndex = n) (_hPres : tp.constraint = present) (hResolve : interpTense n g = matrixFrame.eventTime) : tp.toFrame g matrixFrame.speechTime matrixFrame.eventTime embeddedE = simultaneousFrame matrixFrame embeddedE

The simultaneous reading = bound present tense pronoun. A present-constraint tense pronoun whose variable resolves to P (the matrix event time) produces a simultaneousFrame.

theorem Tense.shiftedFrame_from_tense_pronoun {Time : Type u_1} (matrixFrame : _root_.Time.ReichenbachFrame Time) (g : TemporalAssignment Time) (n : ℕ) (embeddedR embeddedE : Time) (tp : TensePronoun) (hIdx : tp.varIndex = n) (_hPast : tp.constraint = past) (hResolve : interpTense n g = embeddedR) : tp.toFrame g matrixFrame.speechTime matrixFrame.eventTime embeddedE = shiftedFrame matrixFrame embeddedR embeddedE

The shifted reading = free past tense pronoun. A past-constraint tense pronoun whose variable resolves to some R' < P produces a shiftedFrame.

theorem Tense.doubleAccess_present_under_past {Time : Type u_1} [LinearOrder Time] (matrixFrame : _root_.Time.ReichenbachFrame Time) (_embeddedE : Time) (p : Time → Prop) (h_simul : p matrixFrame.eventTime) (h_speech : p matrixFrame.speechTime) : doubleAccess p matrixFrame.speechTime matrixFrame.eventTime

Double-access: present-under-past requires the complement to hold at BOTH speech time AND matrix event time.

This bridges the doubleAccess definition from Tense to the SOT analysis: the present-under-past frame's R = P (simultaneous), and the speech time is independently accessible via indexical rigidity.

theorem Tense.bound_tense_simultaneous {Time : Type u_1} [LinearOrder Time] (g : TemporalAssignment Time) (n : ℕ) (matrixFrame : _root_.Time.ReichenbachFrame Time) : interpTense n (updateTemporal g n matrixFrame.eventTime) = matrixFrame.eventTime ∧ (simultaneousFrame matrixFrame matrixFrame.eventTime).isPresent

Ogihara's synthesis: bound tense (zero tense) + attitude binding = simultaneous reading. The zero tense variable receives the matrix event time via lambda abstraction; the Reichenbach frame has R = P.

ThenAdverb

structure Tense.ThenAdverb : Type

A "then"-type temporal adverb. Cross-linguistically, "then" shifts the perspective time P away from the speech time S ([Zha25], [TZ26]).

• language : String

  Language name

• form : String

  Surface form

• gloss : String

  English gloss

• shiftsPerspective : Bool

  "then" shifts P away from S: P ≠ S after "then" applies.

@[implicit_reducible]

instance Tense.instReprThenAdverb : Repr ThenAdverb

Equations

• Tense.instReprThenAdverb = { reprPrec := Tense.instReprThenAdverb.repr }

def Tense.instReprThenAdverb.repr : ThenAdverb → ℕ → Std.Format

Equations

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

def Tense.instDecidableEqThenAdverb.decEq (x✝ x✝¹ : ThenAdverb) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Tense.instDecidableEqThenAdverb : DecidableEq ThenAdverb

Equations

• Tense.instDecidableEqThenAdverb = Tense.instDecidableEqThenAdverb.decEq