Tense Phenomena: Empirical Data

@cite{abusch-1997} @cite{anand-nevins-2004} @cite{banfield-1982} @cite{comrie-1985} @cite{deal-2020} @cite{declerck-1991} @cite{declerck-2006} @cite{heim-kratzer-1998} @cite{iatridou-2000} @cite{klecha-2016} @cite{kratzer-1998} @cite{ogihara-sharvit-2012} @cite{schlenker-2004} @cite{sharvit-2003} @cite{von-stechow-2009} @cite{wurmbrand-2014} @cite{condoravdi-2002} @cite{schlenker-2003}

Unified entry point for tense phenomena. Absorbs the former Phenomena/SequenceOfTense/Data.lean and extends coverage to 10+ temporal phenomena that distinguish tense theories.

Theory-neutral empirical data only — no theoretical commitments. Bridge theorems connecting this data to specific tense theories are in Studies/HeimKratzer1998.lean.

Phenomena Covered

Baseline (§0)

0. Root-clause simple tenses: past, present, future

Core comparison set (10 + 1 debate)

1. Past-under-past: "John said Mary was sick" (shifted + simultaneous)
2. Present-under-past: "John said Mary is sick" (double access)
3. Future-under-past: "John said Mary would leave"
4. SOT vs non-SOT: English vs Japanese
5. Upper Limit Constraint: no forward-shifted readings
6. Relative clause tense: "the man who was tall"
7. Modal-tense interaction: "John might have left"
8. Counterfactual tense: "If John were here..."
9. Temporal de re: "John believed it was raining"
10. Deletion vs ambiguity: same surface, different mechanisms

Eventual targets (7)

11. SOT in indirect questions: "John asked who was sick"
12. Free indirect discourse: perspective shift without attitude verb
13. Historical/narrative present: "Napoleon enters the room"
14. Perfect tense interactions: "John said Mary had been sick"
15. Future-oriented complements: "John wanted to leave"
16. Tense in adjunct clauses: "Before John left, Mary was happy"
17. Indexical tense shift: Amharic/Zazaki tense under attitudes

Extended phenomena (5) — Sharvit, Zeijlstra, Wurmbrand

18. Embedded present puzzle: "John will say Mary is sick"
19. Lifetime effects: "Aristotle was a philosopher"
20. Fake past: "If John were taller..."
21. Optional SOT (Hebrew-type)
22. Dependent vs independent tense

Discourse-level phenomena (6) — @cite{declerck-1991}/2006

23. Temporal domain shift vs subordination
24. False tense: politeness and tentativeness
25. PPS vs FPS in conditionals
26. Temporal conjunctions with implicit TOs
27. Bounded/unbounded default interpretation (PUTI)
28. Present perfect vs preterit: time-sphere distinction

The most elementary tense phenomena: root-clause sentences with simple past, present, and future tense. These are the baseline against which all embedded and discourse-level phenomena are measured.

"John left." — simple past
"It rains." — simple present
"John will leave." — simple future

All three are root clauses (P = S), perfective aspect (E = R),
and satisfy exactly one of PAST / PRESENT / FUTURE. 

def Phenomena.TenseAspect.simplePastLeft : Core.Reichenbach.ReichenbachFrame ℤ

"John left." — simple past root clause. S = P = 0 (root: perspective = speech time). R = E = -2 (past: reference before perspective, perfective: E = R).

Equations

• Phenomena.TenseAspect.simplePastLeft = { speechTime := 0, perspectiveTime := 0, referenceTime := -2, eventTime := -2 }

def Phenomena.TenseAspect.simplePresentRains : Core.Reichenbach.ReichenbachFrame ℤ

"It rains." — simple present root clause. S = P = R = E = 0 (present: reference at perspective, perfective).

Equations

• Phenomena.TenseAspect.simplePresentRains = { speechTime := 0, perspectiveTime := 0, referenceTime := 0, eventTime := 0 }

def Phenomena.TenseAspect.simpleFutureWillLeave : Core.Reichenbach.ReichenbachFrame ℤ

"John will leave." — simple future root clause. S = P = 0, R = E = 3 (future: reference after perspective).

Equations

• Phenomena.TenseAspect.simpleFutureWillLeave = { speechTime := 0, perspectiveTime := 0, referenceTime := 3, eventTime := 3 }

theorem Phenomena.TenseAspect.simplePast_isPast : simplePastLeft.isPast

Simple past: R < P.

theorem Phenomena.TenseAspect.simplePresent_isPresent : simplePresentRains.isPresent

Simple present: R = P.

theorem Phenomena.TenseAspect.simpleFuture_isFuture : simpleFutureWillLeave.isFuture

Simple future: P < R.

theorem Phenomena.TenseAspect.simplePast_root : simplePastLeft.isSimpleCase

All three are root clauses: P = S.

theorem Phenomena.TenseAspect.simplePresent_root : simplePresentRains.isSimpleCase

theorem Phenomena.TenseAspect.simpleFuture_root : simpleFutureWillLeave.isSimpleCase

theorem Phenomena.TenseAspect.simplePast_perfective : simplePastLeft.isPerfective

All three are perfective: E = R.

theorem Phenomena.TenseAspect.simplePresent_perfective : simplePresentRains.isPerfective

theorem Phenomena.TenseAspect.simpleFuture_perfective : simpleFutureWillLeave.isPerfective

theorem Phenomena.TenseAspect.simplePast_not_present : ¬simplePastLeft.isPresent

Past excludes present and future.

theorem Phenomena.TenseAspect.simplePast_not_future : ¬simplePastLeft.isFuture

theorem Phenomena.TenseAspect.simplePresent_not_past : ¬simplePresentRains.isPast

Present excludes past and future.

theorem Phenomena.TenseAspect.simplePresent_not_future : ¬simplePresentRains.isFuture

theorem Phenomena.TenseAspect.simpleFuture_not_past : ¬simpleFutureWillLeave.isPast

Future excludes past and present.

theorem Phenomena.TenseAspect.simpleFuture_not_present : ¬simpleFutureWillLeave.isPresent

Two readings of "John said that Mary was sick": - SIMULTANEOUS: Mary's being sick overlaps with John's saying - SHIFTED: Mary's being sick precedes John's saying

def Phenomena.TenseAspect.matrixSaid : Core.Reichenbach.ReichenbachFrame ℤ

Matrix frame for "John said..." (past tense, perfective). Speech time S = 0, saying event at t = -2.

Equations

• Phenomena.TenseAspect.matrixSaid = { speechTime := 0, perspectiveTime := 0, referenceTime := -2, eventTime := -2 }

def Phenomena.TenseAspect.embeddedSickSimultaneous : Core.Reichenbach.ReichenbachFrame ℤ

Embedded frame for "Mary was sick" — SIMULTANEOUS reading. Embedded P = matrix E = -2, R' = E_matrix = -2. Mary is sick at the time of the saying.

Equations

• Phenomena.TenseAspect.embeddedSickSimultaneous = { speechTime := 0, perspectiveTime := -2, referenceTime := -2, eventTime := -2 }

def Phenomena.TenseAspect.embeddedSickShifted : Core.Reichenbach.ReichenbachFrame ℤ

Embedded frame for "Mary was sick" — SHIFTED reading. Embedded P = matrix E = -2, R' = -5 < E_matrix. Mary was sick before the saying.

Equations

• Phenomena.TenseAspect.embeddedSickShifted = { speechTime := 0, perspectiveTime := -2, referenceTime := -5, eventTime := -5 }

def Phenomena.TenseAspect.embeddedSickPresent : Core.Reichenbach.ReichenbachFrame ℤ

Embedded frame for "Mary is sick" — PRESENT under PAST. Double-access reading: Mary is sick now (at speech time) AND the sickness is relevant at the time of saying.

Equations

• Phenomena.TenseAspect.embeddedSickPresent = { speechTime := 0, perspectiveTime := -2, referenceTime := -2, eventTime := 0 }

def Phenomena.TenseAspect.embeddedWouldLeave : Core.Reichenbach.ReichenbachFrame ℤ

Embedded frame for "Mary would leave" — FUTURE under PAST. "Would" = PAST + FUTURE: the leaving is after the saying but before or at speech time.

Equations

• Phenomena.TenseAspect.embeddedWouldLeave = { speechTime := 0, perspectiveTime := -2, referenceTime := -1, eventTime := -1 }

def Phenomena.TenseAspect.matrixItta : Core.Reichenbach.ReichenbachFrame ℤ

Japanese matrix frame: "Taroo-ga... to itta" (Taro said...). Same temporal structure as English matrix.

Equations

• Phenomena.TenseAspect.matrixItta = { speechTime := 0, perspectiveTime := 0, referenceTime := -2, eventTime := -2 }

def Phenomena.TenseAspect.embeddedByookiDatta : Core.Reichenbach.ReichenbachFrame ℤ

Japanese embedded: "Mary-ga byooki-datta" (Mary was sick) — absolute past. In non-SOT Japanese, embedded past is absolute (relative to S, not E). Only the shifted reading: sick-time < say-time.

Equations

• Phenomena.TenseAspect.embeddedByookiDatta = { speechTime := 0, perspectiveTime := 0, referenceTime := -5, eventTime := -5 }

def Phenomena.TenseAspect.embeddedSickForwardShifted : Core.Reichenbach.ReichenbachFrame ℤ

Hypothetical forward-shifted frame (for gap demonstration). If past-under-past allowed forward shift, R' > E_matrix. This frame is PREDICTED NOT TO EXIST as a reading.

Equations

• Phenomena.TenseAspect.embeddedSickForwardShifted = { speechTime := 0, perspectiveTime := -2, referenceTime := -1, eventTime := -1 }

def Phenomena.TenseAspect.rcWasTall : Core.Reichenbach.ReichenbachFrame ℤ

Relative clause frame: "the man who was tall" Perspective time = time of the described event (not matrix E). The past tense in the RC is checked against the RC's own perspective time, not the matrix tense.

Equations

• Phenomena.TenseAspect.rcWasTall = { speechTime := 0, perspectiveTime := 0, referenceTime := -3, eventTime := -3 }

def Phenomena.TenseAspect.rcWasTallUnderPast : Core.Reichenbach.ReichenbachFrame ℤ

Relative clause under past matrix: "John met the man who was tall" Here the RC tense could be relative to matrix E or to S — this is the Sharvit challenge to Abusch.

Equations

• Phenomena.TenseAspect.rcWasTallUnderPast = { speechTime := 0, perspectiveTime := -2, referenceTime := -4, eventTime := -4 }

def Phenomena.TenseAspect.modalPast : Core.Reichenbach.ReichenbachFrame ℤ

Modal-past frame: "John might have left" The past tense "have left" is under the modal "might". The leaving is past relative to... what? Speech time? Modal eval time? @cite{klecha-2016}: relative to the modal's evaluation time.

Equations

• Phenomena.TenseAspect.modalPast = { speechTime := 0, perspectiveTime := 0, referenceTime := -1, eventTime := -1 }

def Phenomena.TenseAspect.counterfactualWere : Core.Reichenbach.ReichenbachFrame ℤ

Counterfactual frame: "If John were here..." Past morphology ("were") but present-time reference. The "pastness" is modal distance, not temporal precedence.

Equations

• Phenomena.TenseAspect.counterfactualWere = { speechTime := 0, perspectiveTime := 0, referenceTime := 0, eventTime := 0 }

def Phenomena.TenseAspect.temporalDeRe : Core.Reichenbach.ReichenbachFrame ℤ

Temporal de re frame: "John believed it was raining" The rain event is located at a time determined in the actual world (de re), not in John's belief worlds (de dicto).

Equations

• Phenomena.TenseAspect.temporalDeRe = { speechTime := 0, perspectiveTime := -2, referenceTime := -3, eventTime := -3 }

The simultaneous reading of "John said Mary was sick" arises from the same surface form regardless of mechanism. The debate is about the underlying representation: - Kratzer: deletion removes embedded past → R' = E_matrix - Ogihara: zero tense reading of past → R' = E_matrix Both produce embeddedSickSimultaneous — same Reichenbach frame. The disagreement is about the derivation, not the result.

Indirect questions show SOT effects: "John asked who was sick" has both a simultaneous reading (who is sick at the asking time?) and a shifted reading (who was sick before the asking?).

The question embedding adds a layer: the embedded wh-clause's
tense interacts with both the question semantics and the matrix
tense. @cite{sharvit-2003} and @cite{ogihara-sharvit-2012} argue this
is not a simple extension of declarative SOT. 

def Phenomena.TenseAspect.matrixAsked : Core.Reichenbach.ReichenbachFrame ℤ

Matrix frame for "John asked..." (past tense, perfective).

Equations

• Phenomena.TenseAspect.matrixAsked = { speechTime := 0, perspectiveTime := 0, referenceTime := -2, eventTime := -2 }

def Phenomena.TenseAspect.indirectQSimultaneous : Core.Reichenbach.ReichenbachFrame ℤ

Embedded frame for "who was sick" — simultaneous with asking. The question is about sickness at the asking time.

Equations

• Phenomena.TenseAspect.indirectQSimultaneous = { speechTime := 0, perspectiveTime := -2, referenceTime := -2, eventTime := -2 }

def Phenomena.TenseAspect.indirectQShifted : Core.Reichenbach.ReichenbachFrame ℤ

Embedded frame for "who was sick" — shifted before asking. The question is about sickness before the asking time.

Equations

• Phenomena.TenseAspect.indirectQShifted = { speechTime := 0, perspectiveTime := -2, referenceTime := -4, eventTime := -4 }

Free indirect discourse (FID) exhibits perspective shift in tense without an overt attitude verb:

"She walked to the window. The garden was/*is beautiful."

The past tense in the second sentence is evaluated from the
character's perspective time, not the narrator's. This challenges
theories that derive perspective shift from attitude verb semantics
(Abusch, Von Stechow, Kratzer, Ogihara) — there is no attitude verb
to trigger the shift.

@cite{banfield-1982}, @cite{schlenker-2004},. 

def Phenomena.TenseAspect.fidWalked : Core.Reichenbach.ReichenbachFrame ℤ

FID matrix: "She walked to the window" (past, narrated event at -3).

Equations

• Phenomena.TenseAspect.fidWalked = { speechTime := 0, perspectiveTime := 0, referenceTime := -3, eventTime := -3 }

def Phenomena.TenseAspect.fidGardenBeautiful : Core.Reichenbach.ReichenbachFrame ℤ

FID continuation: "The garden was beautiful." Perspective shifts to character's viewpoint (E_matrix = -3) even though there is no attitude verb.

Equations

• Phenomena.TenseAspect.fidGardenBeautiful = { speechTime := 0, perspectiveTime := -3, referenceTime := -3, eventTime := -3 }

Historical present: present tense morphology with past temporal reference.

"Napoleon enters the room. He sees the generals."

The present tense "enters" does not locate the event at speech time.
It refers to a past event but uses present morphology for vividness.
This is problematic for theories where present tense = R = S:
the constraint is violated, yet the sentence is felicitous.

@cite{wolfson-1979}, @cite{schiffrin-1981}. 

def Phenomena.TenseAspect.historicalPresent : Core.Reichenbach.ReichenbachFrame ℤ

Historical present: "Napoleon enters the room." Present morphology (R = P) but the event is in the past. Speech time S = 0, but the narrated event is at -200 (schematic).

Equations

• Phenomena.TenseAspect.historicalPresent = { speechTime := 0, perspectiveTime := -200, referenceTime := -200, eventTime := -200 }

theorem Phenomena.TenseAspect.historicalPresent_is_present : historicalPresent.isPresent

Historical present is "present" relative to narrative perspective.

The pluperfect (past perfect) disambiguates past-under-past:

"John said Mary had been sick."

Unlike simple past-under-past ("John said Mary was sick"), the
pluperfect ONLY has the shifted reading. There is no simultaneous
reading — "had been" forces the sickness to precede the saying.
This is a useful test case because it disambiguates between
theories' predictions about what triggers the simultaneous reading.

@cite{comrie-1985}, @cite{ogihara-1996} ch. 4. 

def Phenomena.TenseAspect.pluperfectShifted : Core.Reichenbach.ReichenbachFrame ℤ

Pluperfect under past: "John said Mary had been sick." Only the shifted reading: sickness before saying. The pluperfect adds an additional layer of temporal precedence: E < R (perfect aspect) + R < P (past tense).

Equations

• Phenomena.TenseAspect.pluperfectShifted = { speechTime := 0, perspectiveTime := -2, referenceTime := -4, eventTime := -5 }

theorem Phenomena.TenseAspect.pluperfect_is_perfect : pluperfectShifted.isPerfect

The pluperfect frame has the perfect configuration: E < R.

theorem Phenomena.TenseAspect.pluperfect_is_past : pluperfectShifted.isPast

The pluperfect frame is past relative to embedded P: R < P.

Verbs like want, plan, hope orient their complement toward the future without standard SOT:

"John wanted to leave."

The leaving is AFTER the wanting, but there is no future tense
morphology. The futurity comes from the verb's lexical semantics,
not from tense. @cite{wurmbrand-2014}: the temporal orientation is
part of the verb's selection, not tense composition.

"John planned to leave" — the leaving is strictly after the planning.
"John hoped to win" — the winning is after the hoping.

These complements behave differently from standard SOT because the
embedded temporal location is lexically determined, not computed
from tense morphology. 

def Phenomena.TenseAspect.wantedToLeave : Core.Reichenbach.ReichenbachFrame ℤ

Future-oriented complement: "John wanted to leave." The wanting is past; the (desired) leaving is after the wanting. No tense morphology on the infinitival complement.

Equations

• Phenomena.TenseAspect.wantedToLeave = { speechTime := 0, perspectiveTime := 0, referenceTime := -2, eventTime := -1 }

theorem Phenomena.TenseAspect.wantedToLeave_future_oriented : wantedToLeave.eventTime > wantedToLeave.referenceTime

Future-oriented: event time after reference time.

Temporal adjunct clauses have their own tense interpretation that doesn't follow the attitude-embedding pattern:

"Before John left, Mary was happy."
"After John arrived, Mary smiled."

The tense in the adjunct ("left", "arrived") locates an event
relative to the matrix event, but NOT via the perspective-shift
mechanism used for attitude complements. The adjunct tense is
more like an independent temporal reference anchored by the
temporal connective (*before*, *after*).

@cite{arregui-kusumoto-1998}, @cite{ogihara-sharvit-2012}. 

def Phenomena.TenseAspect.adjunctBeforeLeft : Core.Reichenbach.ReichenbachFrame ℤ

Adjunct clause: "Before John left, Mary was happy." John's leaving is before Mary's happiness. Both are past relative to S, but their relative ordering comes from "before", not from tense composition.

Equations

• Phenomena.TenseAspect.adjunctBeforeLeft = { speechTime := 0, perspectiveTime := 0, referenceTime := -3, eventTime := -3 }

def Phenomena.TenseAspect.matrixWasHappy : Core.Reichenbach.ReichenbachFrame ℤ

Matrix with adjunct: "Mary was happy (before John left)."

Equations

• Phenomena.TenseAspect.matrixWasHappy = { speechTime := 0, perspectiveTime := 0, referenceTime := -2, eventTime := -2 }

theorem Phenomena.TenseAspect.adjunct_before_matrix : adjunctBeforeLeft.eventTime < matrixWasHappy.eventTime

The adjunct event precedes the matrix event (from "before").

In some languages, tense can shift under attitude verbs in ways that parallel the shift of indexical pronouns.

**Amharic**: the present tense in an attitude
complement can be interpreted relative to the attitude holder's
"now" rather than the speaker's speech time.

**Zazaki**: similar indexical shift for tense
under reportative evidentials.

This directly bears on the @cite{partee-1973} analogy between tenses
and pronouns: if both can undergo indexical shift in the same
environments, the structural parallel runs deeper than English
data alone suggests.

In English, indexical shift of tense is debated (but see the
double-access reading as a partial parallel). In shifting languages,
the embedded present tense receives the attitude holder's time,
not the speaker's speech time. 

def Phenomena.TenseAspect.indexicalShiftPresent : Core.Reichenbach.ReichenbachFrame ℤ

Indexical-shift present under past (Amharic-type): "Abebe said Mary IS-sick" where the present tense is interpreted at Abebe's saying time, not at speech time.

Compare with English double-access embeddedSickPresent where present under past requires truth at BOTH speech time and matrix E. In Amharic, there is no double-access requirement — the present is simply evaluated at the attitude holder's time.

Equations

• Phenomena.TenseAspect.indexicalShiftPresent = { speechTime := 0, perspectiveTime := -2, referenceTime := -2, eventTime := -2 }

theorem Phenomena.TenseAspect.indexicalShift_not_at_speech : indexicalShiftPresent.eventTime ≠ indexicalShiftPresent.speechTime

Indexical shift: event time ≠ speech time (unlike English present). The key difference from English double-access: no requirement that E = S. The shifted present locates the event at the attitude holder's time exclusively.

The embedded present puzzle: present tense under a future matrix verb gets a simultaneous reading with the FUTURE saying time, not with speech time.

"John will say Mary is sick" → Mary is sick at the (future) saying
time, not necessarily at speech time.

This is puzzling for theories where present = R = S: the present
tense should force the event to be at speech time, yet the reading
locates it at the future saying time. Sharvit: the "present" is
a simultaneous tense evaluated at the future saying time. 

def Phenomena.TenseAspect.matrixWillSay : Core.Reichenbach.ReichenbachFrame ℤ

Matrix frame for "John will say..." (future tense). Speech time S = 0, saying event at t = 3 (future).

Equations

• Phenomena.TenseAspect.matrixWillSay = { speechTime := 0, perspectiveTime := 0, referenceTime := 3, eventTime := 3 }

def Phenomena.TenseAspect.embeddedPresentUnderFuture : Core.Reichenbach.ReichenbachFrame ℤ

Embedded frame for "Mary is sick" under future — simultaneous. The sickness is at the future saying time (= matrix E = 3), not at speech time.

Equations

• Phenomena.TenseAspect.embeddedPresentUnderFuture = { speechTime := 0, perspectiveTime := 3, referenceTime := 3, eventTime := 3 }

Lifetime effects (@cite{musan-1995}/1997): past tense with individual-level predicates implicates that the subject no longer exists.

"Aristotle was a philosopher" → Aristotle is dead.
"Aristotle was blond" → Aristotle is dead (or no longer blond).

But: "Aristotle was a philosopher" does NOT merely mean that his
philosophizing ended — it implicates his death. This is the
"lifetime effect": past tense + individual-level predicate →
subject's lifetime has ended.

This bears on tense theory because it shows that past tense
interacts with predicate type (individual-level vs stage-level)
in ways that go beyond simple temporal precedence. 

def Phenomena.TenseAspect.lifetimeAristotle : Core.Reichenbach.ReichenbachFrame ℤ

Lifetime effect frame: "Aristotle was a philosopher." The past tense locates the philosophical property in the past. The lifetime effect (Aristotle is dead) is an implicature, not part of the Reichenbach frame.

Equations

• Phenomena.TenseAspect.lifetimeAristotle = { speechTime := 0, perspectiveTime := 0, referenceTime := -2400, eventTime := -2400 }

Fake past: past morphology with non-past semantics in subjunctive/counterfactual contexts.

"If John were taller, he would play basketball."

The "were" is morphologically past but does not locate the event
before speech time. Rather, it expresses counterfactual distance or modal remoteness.

This differs from Deal's `counterfactualTense` in specificity:
fake past is the broader phenomenon (Iatridou's cross-linguistic
generalization), while Deal's treatment focuses on ULC refinement
for counterfactuals. 

def Phenomena.TenseAspect.fakePastSubjunctive : Core.Reichenbach.ReichenbachFrame ℤ

Fake past frame: "If John were taller..." Past morphology ("were") but present-time reference. The temporal coordinates are present; the "pastness" is modal distance, not temporal.

Equations

• Phenomena.TenseAspect.fakePastSubjunctive = { speechTime := 0, perspectiveTime := 0, referenceTime := 0, eventTime := 0 }

Optional SOT in Hebrew-type languages.

In English, SOT is obligatory: "John said Mary was sick" is the
only form for the simultaneous reading. In Hebrew, both forms
are grammatical:

"John said Mary was sick" → simultaneous reading (simultaneous tense)
"John said Mary is sick" → simultaneous reading (present tense)

Both forms are available with slightly different pragmatic profiles.
The past-form version uses Sharvit's simultaneous tense; the
present-form version uses genuine present tense. 

def Phenomena.TenseAspect.optionalSOTPastForm : Core.Reichenbach.ReichenbachFrame ℤ

Hebrew-type SOT with past form (simultaneous tense): "John said Mary was sick" → simultaneous reading. Same frame as English embeddedSickSimultaneous.

Equations

• Phenomena.TenseAspect.optionalSOTPastForm = { speechTime := 0, perspectiveTime := -2, referenceTime := -2, eventTime := -2 }

def Phenomena.TenseAspect.optionalSOTPresentForm : Core.Reichenbach.ReichenbachFrame ℤ

Hebrew-type SOT with present form: "John said Mary is sick" → also simultaneous, but via present tense. The present tense directly locates the event at the attitude time.

Equations

• Phenomena.TenseAspect.optionalSOTPresentForm = { speechTime := 0, perspectiveTime := -2, referenceTime := -2, eventTime := -2 }

@cite{wurmbrand-2014} classifies infinitival tense into three types:

1. **Future irrealis** (decide, want): no independent tense;
   future orientation comes from woll.
   "John decided to leave" → leaving after deciding.

2. **Propositional** (believe, claim): NOW-anchored tense.
   "John believes Mary to be sick" → simultaneous with believing.

3. **Restructuring** (try, begin): dependent on matrix tense.
   "John tried to leave" → leaving in the same temporal domain.

This is relevant because it shows that the "tenselessness" of
infinitives is not uniform — different complement types have
different temporal behavior. 

def Phenomena.TenseAspect.decidedToLeave : Core.Reichenbach.ReichenbachFrame ℤ

Future-irrealis complement: "John decided to leave." The deciding is past; the leaving is after the deciding. No tense morphology on "to leave."

Equations

• Phenomena.TenseAspect.decidedToLeave = { speechTime := 0, perspectiveTime := 0, referenceTime := -2, eventTime := -1 }

def Phenomena.TenseAspect.believesToBeSick : Core.Reichenbach.ReichenbachFrame ℤ

Propositional complement: "John believes Mary to be sick." The believing is present; the sickness is simultaneous.

Equations

• Phenomena.TenseAspect.believesToBeSick = { speechTime := 0, perspectiveTime := 0, referenceTime := 0, eventTime := 0 }

def Phenomena.TenseAspect.triedToLeave : Core.Reichenbach.ReichenbachFrame ℤ

Restructuring complement: "John tried to leave." The trying and the leaving are in the same temporal domain.

Equations

• Phenomena.TenseAspect.triedToLeave = { speechTime := 0, perspectiveTime := 0, referenceTime := -2, eventTime := -2 }

theorem Phenomena.TenseAspect.matrixSaid_R_lt_P : matrixSaid.referenceTime < matrixSaid.perspectiveTime

The matrix "said" is past: R < P.

theorem Phenomena.TenseAspect.matrixSaid_root : matrixSaid.perspectiveTime = matrixSaid.speechTime

The matrix frame is a root clause: P = S.

theorem Phenomena.TenseAspect.simultaneous_R_eq_matrix_E : embeddedSickSimultaneous.referenceTime = matrixSaid.eventTime

Simultaneous reading: embedded R = matrix E.

theorem Phenomena.TenseAspect.shifted_R_lt_matrix_E : embeddedSickShifted.referenceTime < matrixSaid.eventTime

Shifted reading: embedded R < matrix E.

theorem Phenomena.TenseAspect.simultaneous_sick_at_say_time : embeddedSickSimultaneous.eventTime = matrixSaid.eventTime

Simultaneous: sick-time = say-time.

theorem Phenomena.TenseAspect.shifted_sick_before_say : embeddedSickShifted.eventTime < matrixSaid.eventTime

Shifted: sick-time < say-time.

theorem Phenomena.TenseAspect.japanese_absolute_perspective : embeddedByookiDatta.perspectiveTime = embeddedByookiDatta.speechTime

Japanese: embedded P = S (absolute, not shifted to matrix E).

theorem Phenomena.TenseAspect.english_simultaneous_perspective_shifted : embeddedSickSimultaneous.perspectiveTime = matrixSaid.eventTime

English simultaneous: embedded P = matrix E (perspective shifted).

theorem Phenomena.TenseAspect.english_shifted_perspective_shifted : embeddedSickShifted.perspectiveTime = matrixSaid.eventTime

English shifted: embedded P = matrix E (perspective shifted).

theorem Phenomena.TenseAspect.forwardShifted_R_gt_matrix_E : embeddedSickForwardShifted.referenceTime > matrixSaid.eventTime

Forward-shifted: R' > matrix E (theory-neutral temporal fact).

theorem Phenomena.TenseAspect.double_access_overlaps_speech : embeddedSickPresent.eventTime = embeddedSickPresent.speechTime

Double access reading: present-under-past requires overlap with speech time.

theorem Phenomena.TenseAspect.futureUnderPast_R_gt_matrix_E : embeddedWouldLeave.referenceTime > matrixSaid.eventTime

Future-under-past: embedded R > matrix E.

theorem Phenomena.TenseAspect.counterfactual_present_reference : counterfactualWere.referenceTime = counterfactualWere.perspectiveTime

Counterfactual: past morphology but R = P (present reference).

theorem Phenomena.TenseAspect.deRe_past_reference : temporalDeRe.referenceTime < temporalDeRe.perspectiveTime

Temporal de re: R < P (past reference relative to belief time).

theorem Phenomena.TenseAspect.rc_past_reference : rcWasTall.referenceTime < rcWasTall.perspectiveTime

RC tense: past reference.

theorem Phenomena.TenseAspect.modalPast_past_reference : modalPast.referenceTime < modalPast.perspectiveTime

Modal past: past reference relative to modal eval time.

theorem Phenomena.TenseAspect.indirectQ_simultaneous_present : indirectQSimultaneous.isPresent

Indirect question: simultaneous frame has R = P.

theorem Phenomena.TenseAspect.indirectQ_shifted_past : indirectQShifted.referenceTime < indirectQShifted.perspectiveTime

Indirect question: shifted frame has R < P.

theorem Phenomena.TenseAspect.fid_perspective_shifted : fidGardenBeautiful.perspectiveTime = fidWalked.eventTime

FID: perspective shifts without attitude verb.

theorem Phenomena.TenseAspect.fid_garden_present : fidGardenBeautiful.isPresent

FID garden: R = P (simultaneous with character's experience).

theorem Phenomena.TenseAspect.historicalPresent_R_eq_P : historicalPresent.referenceTime = historicalPresent.perspectiveTime

Historical present: present morphology despite past event.

theorem Phenomena.TenseAspect.historicalPresent_not_at_speech : historicalPresent.eventTime ≠ historicalPresent.speechTime

Historical present: event time ≠ speech time.

theorem Phenomena.TenseAspect.pluperfect_E_lt_R_lt_P : pluperfectShifted.eventTime < pluperfectShifted.referenceTime ∧ pluperfectShifted.referenceTime < pluperfectShifted.perspectiveTime

Pluperfect: E < R < P (both perfect and past).

theorem Phenomena.TenseAspect.adjunct_precedes_matrix : adjunctBeforeLeft.eventTime < matrixWasHappy.eventTime

Adjunct "before": adjunct event precedes matrix event.

theorem Phenomena.TenseAspect.indexicalShift_at_attitude_time : indexicalShiftPresent.referenceTime = indexicalShiftPresent.perspectiveTime ∧ indexicalShiftPresent.eventTime ≠ indexicalShiftPresent.speechTime

Indexical shift: present tense at attitude time, not speech time.

theorem Phenomena.TenseAspect.embeddedPresentUnderFuture_simultaneous : embeddedPresentUnderFuture.isPresent

Embedded present puzzle: present under future has R = P (simultaneous).

theorem Phenomena.TenseAspect.embeddedPresentUnderFuture_not_at_speech : embeddedPresentUnderFuture.eventTime ≠ embeddedPresentUnderFuture.speechTime

Embedded present puzzle: event NOT at speech time.

theorem Phenomena.TenseAspect.matrixWillSay_is_future : matrixWillSay.referenceTime > matrixWillSay.perspectiveTime

Embedded present puzzle: matrix is future.

theorem Phenomena.TenseAspect.lifetimeAristotle_past : lifetimeAristotle.referenceTime < lifetimeAristotle.perspectiveTime

Lifetime effects: past reference.

theorem Phenomena.TenseAspect.fakePast_present_reference : fakePastSubjunctive.referenceTime = fakePastSubjunctive.perspectiveTime

Fake past: past morphology but R = P (present reference).

theorem Phenomena.TenseAspect.optionalSOT_both_simultaneous : optionalSOTPastForm.isPresent ∧ optionalSOTPresentForm.isPresent

Optional SOT: both forms give R = P.

theorem Phenomena.TenseAspect.optionalSOT_same_frame : optionalSOTPastForm = optionalSOTPresentForm

Optional SOT: both forms have the same temporal structure.

theorem Phenomena.TenseAspect.decidedToLeave_future_oriented : decidedToLeave.eventTime > decidedToLeave.referenceTime

Future-irrealis complement: event after reference (future-oriented).

theorem Phenomena.TenseAspect.believesToBeSick_simultaneous : believesToBeSick.eventTime = believesToBeSick.referenceTime

Propositional complement: event at reference (simultaneous).

theorem Phenomena.TenseAspect.triedToLeave_same_domain : triedToLeave.eventTime = triedToLeave.referenceTime

Restructuring complement: event at reference (same domain).

Two ways successive clauses relate temporally:

**Temporal subordination**: "He left and would never come back."
The conditional (`would`) is a *relative* tense expressing
posteriority within the past domain established by `left`.

**Domain shift**: "He left and never came back."
Both clauses use *absolute* preterits establishing independent
domains. Temporal ordering is recovered pragmatically, not
structurally.

@cite{declerck-1991} ch. 2 §12–14. 

def Phenomena.TenseAspect.domainSubordLeft : Core.Reichenbach.ReichenbachFrame ℤ

"He left..." — past domain anchor (subordination pair). Speech time S = 0, leaving event at t = -5.

Equations

• Phenomena.TenseAspect.domainSubordLeft = { speechTime := 0, perspectiveTime := 0, referenceTime := -5, eventTime := -5 }

def Phenomena.TenseAspect.domainSubordWouldReturn : Core.Reichenbach.ReichenbachFrame ℤ

"... and would never come back" — relative tense within the past domain established by left. The would expresses posteriority relative to the leaving, not to speech time.

Equations

• Phenomena.TenseAspect.domainSubordWouldReturn = { speechTime := 0, perspectiveTime := -5, referenceTime := -3, eventTime := -3 }

def Phenomena.TenseAspect.domainShiftLeft : Core.Reichenbach.ReichenbachFrame ℤ

"He left..." — independent past domain (shift pair).

Equations

• Phenomena.TenseAspect.domainShiftLeft = { speechTime := 0, perspectiveTime := 0, referenceTime := -5, eventTime := -5 }

def Phenomena.TenseAspect.domainShiftCameBack : Core.Reichenbach.ReichenbachFrame ℤ

"... and never came back" — independent past domain. Both clauses are absolute preterits; no structural temporal relation between them.

Equations

• Phenomena.TenseAspect.domainShiftCameBack = { speechTime := 0, perspectiveTime := 0, referenceTime := -3, eventTime := -3 }

theorem Phenomena.TenseAspect.domainSubord_left_past : domainSubordLeft.referenceTime < domainSubordLeft.perspectiveTime

Both left frames are past (R < P).

theorem Phenomena.TenseAspect.domainShift_left_past : domainShiftLeft.referenceTime < domainShiftLeft.perspectiveTime

theorem Phenomena.TenseAspect.domainSubord_posteriority : domainSubordWouldReturn.referenceTime > domainSubordLeft.eventTime

Subordination: wouldReturn is posterior within the domain established by left (R > P' where P' = left's E).

theorem Phenomena.TenseAspect.domainShift_both_absolute : domainShiftLeft.perspectiveTime = domainShiftLeft.speechTime ∧ domainShiftCameBack.perspectiveTime = domainShiftCameBack.speechTime

Shift: both frames independently satisfy PAST relative to their own P. The shift pair has P = S for both clauses (absolute perspective).

theorem Phenomena.TenseAspect.domainSubord_shifted_perspective : domainSubordWouldReturn.perspectiveTime ≠ domainSubordWouldReturn.speechTime

Subordination: wouldReturn has shifted perspective (P ≠ S).

Past morphology with present-time reference for pragmatic effects:

"I wanted to ask you something." — past morphology, present request
"Could you help me?" — past modal, present request

Distinct from §20 (fake past / counterfactual): false tense is *not*
counterfactual — the speaker is genuinely asking now. Declerck
analyzes this as a shift of temporal perspective from present to past,
exploiting the metaphor between temporal remoteness and social distance.

@cite{declerck-1991} ch. 2 §20–21. 

def Phenomena.TenseAspect.falsePastWanted : Core.Reichenbach.ReichenbachFrame ℤ

"I wanted to ask you something." — false past. Past morphology ("wanted") but present-time reference: the wanting is happening now, not in the past.

Equations

• Phenomena.TenseAspect.falsePastWanted = { speechTime := 0, perspectiveTime := 0, referenceTime := 0, eventTime := 0 }

def Phenomena.TenseAspect.falsePastCould : Core.Reichenbach.ReichenbachFrame ℤ

"Could you help me?" — false past modal. Past modal morphology ("could") but present-time request.

Equations

• Phenomena.TenseAspect.falsePastCould = { speechTime := 0, perspectiveTime := 0, referenceTime := 0, eventTime := 0 }

theorem Phenomena.TenseAspect.falsePast_present_reference_wanted : falsePastWanted.referenceTime = falsePastWanted.perspectiveTime

Both false-past frames have R = P (present reference).

theorem Phenomena.TenseAspect.falsePast_present_reference_could : falsePastCould.referenceTime = falsePastCould.perspectiveTime

theorem Phenomena.TenseAspect.falsePast_same_structure_as_counterfactual : falsePastWanted = counterfactualWere

False past and counterfactual produce identical Reichenbach frames. The difference is pragmatic (politeness vs counterfactuality), not temporal.

Standard conditionals use the Present Perspective System (PPS): present tense in if-clause for future reference. Non-standard types use the Future Perspective System (FPS): will/be going to in if-clause.

PPS: "If he comes, I will be happy."
FPS: "If he will go to China, we should publish now."

The FPS if-clause has explicit future morphology, reversing the
typical temporal anchoring: the if-clause is future and the
matrix clause is present.

@cite{declerck-1991} ch. 4 §2. 

def Phenomena.TenseAspect.ppsIfComes : Core.Reichenbach.ReichenbachFrame ℤ

PPS if-clause: "If he comes..." — present morphology, future pragmatic reference. R = P (present tense form).

Equations

• Phenomena.TenseAspect.ppsIfComes = { speechTime := 0, perspectiveTime := 0, referenceTime := 0, eventTime := 3 }

def Phenomena.TenseAspect.ppsWillBeHappy : Core.Reichenbach.ReichenbachFrame ℤ

PPS matrix: "... I will be happy." — future tense.

Equations

• Phenomena.TenseAspect.ppsWillBeHappy = { speechTime := 0, perspectiveTime := 0, referenceTime := 3, eventTime := 3 }

def Phenomena.TenseAspect.fpsIfWillGo : Core.Reichenbach.ReichenbachFrame ℤ

FPS if-clause: "If he will go to China..." — future in the if-clause (non-standard).

Equations

• Phenomena.TenseAspect.fpsIfWillGo = { speechTime := 0, perspectiveTime := 0, referenceTime := 5, eventTime := 5 }

def Phenomena.TenseAspect.fpsShouldPublish : Core.Reichenbach.ReichenbachFrame ℤ

FPS matrix: "... we should publish now." — present tense.

Equations

• Phenomena.TenseAspect.fpsShouldPublish = { speechTime := 0, perspectiveTime := 0, referenceTime := 0, eventTime := 0 }

theorem Phenomena.TenseAspect.pps_ifClause_present_morphology : ppsIfComes.referenceTime = ppsIfComes.perspectiveTime

PPS if-clause: present morphology (R = P).

theorem Phenomena.TenseAspect.fps_ifClause_future_morphology : fpsIfWillGo.referenceTime > fpsIfWillGo.perspectiveTime

FPS if-clause: future morphology (R > P).

theorem Phenomena.TenseAspect.pps_fps_reversed_anchoring : ppsWillBeHappy.referenceTime > ppsWillBeHappy.perspectiveTime ∧ fpsShouldPublish.referenceTime = fpsShouldPublish.perspectiveTime

PPS matrix is future; FPS matrix is present — reversed anchoring.

theorem Phenomena.TenseAspect.pps_ifClause_future_event : ppsIfComes.eventTime > ppsIfComes.speechTime

PPS: if-clause event is in the future despite present morphology.

Temporal connectives (before/after/when) involve an implicit TO distinct from the situation-TOs of either clause:

"Bill will have left when John arrives."
The present tense in the when-clause expresses simultaneity with
an implicit TO (= TO₂ of the future perfect), not with Bill's leaving.

"John had left before we arrived."
The preterit `arrived` expresses simultaneity with an implicit TO
that is posterior to John's leaving.

@cite{declerck-1991} ch. 2 §24–25. 

def Phenomena.TenseAspect.futPerfLeft : Core.Reichenbach.ReichenbachFrame ℤ

"Bill will have left..." — future perfect. E < R (perfect: leaving before reference) and R > P (future).

Equations

• Phenomena.TenseAspect.futPerfLeft = { speechTime := 0, perspectiveTime := 0, referenceTime := 5, eventTime := 3 }

def Phenomena.TenseAspect.whenArrives : Core.Reichenbach.ReichenbachFrame ℤ

"... when John arrives." — when-clause present tense. R = P' where P' is the implicit TO (= futPerfLeft.R). The present tense is relative to the implicit TO, not speech time.

Equations

• Phenomena.TenseAspect.whenArrives = { speechTime := 0, perspectiveTime := 5, referenceTime := 5, eventTime := 5 }

def Phenomena.TenseAspect.hadLeftBefore : Core.Reichenbach.ReichenbachFrame ℤ

"John had left..." — past perfect (before-clause pair). E < R (perfect) and R < P (past).

Equations

• Phenomena.TenseAspect.hadLeftBefore = { speechTime := 0, perspectiveTime := 0, referenceTime := -2, eventTime := -4 }

def Phenomena.TenseAspect.beforeArrived : Core.Reichenbach.ReichenbachFrame ℤ

"... before we arrived." — before-clause. The arrival is at the implicit TO, which is posterior to John's leaving.

Equations

• Phenomena.TenseAspect.beforeArrived = { speechTime := 0, perspectiveTime := 0, referenceTime := -2, eventTime := -2 }

theorem Phenomena.TenseAspect.futPerf_leaving_before_arrival : futPerfLeft.eventTime < whenArrives.eventTime

Future perfect: leaving before arrival (E_left < E_arrives).

theorem Phenomena.TenseAspect.futPerf_is_perfect : futPerfLeft.isPerfect

Future perfect frame has E < R (perfect aspect).

theorem Phenomena.TenseAspect.when_clause_present : whenArrives.isPresent

When-clause: present relative to implicit TO (R = P).

theorem Phenomena.TenseAspect.before_leaving_before_arrival : hadLeftBefore.eventTime < beforeArrived.eventTime

Before-clause: leaving before arrival (E_had_left < E_arrived).

theorem Phenomena.TenseAspect.hadLeft_is_perfect : hadLeftBefore.isPerfect

Past perfect frame has E < R (perfect aspect).

Declerck's Principle of Unmarked Temporal Interpretation (PUTI):

- Bounded + bounded → iconic (sequential) ordering
- Unbounded + unbounded → simultaneity
- Mixed → temporal inclusion

These are pragmatic defaults, not semantic entailments.

@cite{declerck-1991} ch. 3 §1.2. 

structure Phenomena.TenseAspect.BoundedFrame : Type

A Reichenbach frame paired with its aspectual boundedness.

• frame : Core.Reichenbach.ReichenbachFrame ℤ
• boundedness : Core.Time.SituationBoundedness

def Phenomena.TenseAspect.arrivedBounded : BoundedFrame

"He arrived." — bounded (achievement).

Equations

• Phenomena.TenseAspect.arrivedBounded = { frame := { speechTime := 0, perspectiveTime := 0, referenceTime := -5, eventTime := -5 }, boundedness := Core.Time.SituationBoundedness.bounded }

def Phenomena.TenseAspect.satDownBounded : BoundedFrame

"He sat down." — bounded (achievement), after arrival.

Equations

• Phenomena.TenseAspect.satDownBounded = { frame := { speechTime := 0, perspectiveTime := 0, referenceTime := -4, eventTime := -4 }, boundedness := Core.Time.SituationBoundedness.bounded }

def Phenomena.TenseAspect.rainingUnbounded : BoundedFrame

"It was raining." — unbounded (activity/state).

Equations

• Phenomena.TenseAspect.rainingUnbounded = { frame := { speechTime := 0, perspectiveTime := 0, referenceTime := -3, eventTime := -3 }, boundedness := Core.Time.SituationBoundedness.unbounded }

def Phenomena.TenseAspect.windBlowingUnbounded : BoundedFrame

"The wind was blowing." — unbounded (activity), simultaneous with rain.

Equations

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

def Phenomena.TenseAspect.readingUnbounded : BoundedFrame

"He was reading." — unbounded (activity).

Equations

• Phenomena.TenseAspect.readingUnbounded = { frame := { speechTime := 0, perspectiveTime := 0, referenceTime := -3, eventTime := -3 }, boundedness := Core.Time.SituationBoundedness.unbounded }

def Phenomena.TenseAspect.phoneRangBounded : BoundedFrame

"The phone rang." — bounded (achievement), included in reading interval.

Equations

• Phenomena.TenseAspect.phoneRangBounded = { frame := { speechTime := 0, perspectiveTime := 0, referenceTime := -3, eventTime := -3 }, boundedness := Core.Time.SituationBoundedness.bounded }

theorem Phenomena.TenseAspect.bounded_sequential : arrivedBounded.frame.eventTime < satDownBounded.frame.eventTime

Sequential (bounded + bounded): arrival before sitting (iconic ordering).

theorem Phenomena.TenseAspect.unbounded_simultaneous : rainingUnbounded.frame.eventTime = windBlowingUnbounded.frame.eventTime

Simultaneous (unbounded + unbounded): rain and wind at the same time.

theorem Phenomena.TenseAspect.mixed_inclusion : phoneRangBounded.frame.eventTime = readingUnbounded.frame.eventTime

Inclusion (mixed): phone ringing within reading interval.

theorem Phenomena.TenseAspect.sequential_both_bounded : arrivedBounded.boundedness = Core.Time.SituationBoundedness.bounded ∧ satDownBounded.boundedness = Core.Time.SituationBoundedness.bounded

Both bounded frames are bounded.

theorem Phenomena.TenseAspect.simultaneous_both_unbounded : rainingUnbounded.boundedness = Core.Time.SituationBoundedness.unbounded ∧ windBlowingUnbounded.boundedness = Core.Time.SituationBoundedness.unbounded

Both unbounded frames are unbounded.

theorem Phenomena.TenseAspect.inclusion_mixed_boundedness : readingUnbounded.boundedness = Core.Time.SituationBoundedness.unbounded ∧ phoneRangBounded.boundedness = Core.Time.SituationBoundedness.bounded

Mixed: one unbounded, one bounded.

Declerck's distinctive claim: the present perfect and preterit differ not in definiteness or current relevance but in time-sphere membership. Both can refer to the same objective event; what differs is the speaker's conceptualization.

"I have visited Paris." (pre-present sector: E ≤ R ≤ P,
  situation anchored to present time-sphere)
"I visited Paris." (past time-sphere: E = R < P,
  situation detached from present)

@cite{declerck-1991} ch. 7 §1,3; @cite{declerck-2006}. 

def Phenomena.TenseAspect.perfectVisitedParis : Core.Reichenbach.ReichenbachFrame ℤ

"I have visited Paris." — present perfect. Pre-present sector: E < R and R = P (present time-sphere). The event is past but the reference frame is present.

Equations

• Phenomena.TenseAspect.perfectVisitedParis = { speechTime := 0, perspectiveTime := 0, referenceTime := 0, eventTime := -3 }

def Phenomena.TenseAspect.preteritVisitedParis : Core.Reichenbach.ReichenbachFrame ℤ

"I visited Paris." — simple preterit. Past time-sphere: E = R < P. Same objective event time as the perfect, but the reference frame is past.

Equations

• Phenomena.TenseAspect.preteritVisitedParis = { speechTime := 0, perspectiveTime := 0, referenceTime := -3, eventTime := -3 }

theorem Phenomena.TenseAspect.perfectPreterit_both_event_before_speech : perfectVisitedParis.eventTime < perfectVisitedParis.speechTime ∧ preteritVisitedParis.eventTime < preteritVisitedParis.speechTime

Both frames locate the event before speech time.

theorem Phenomena.TenseAspect.perfectPreterit_same_eventTime : perfectVisitedParis.eventTime = preteritVisitedParis.eventTime

Same event time — the difference is structural, not temporal.

theorem Phenomena.TenseAspect.perfect_is_perfect : perfectVisitedParis.isPerfect

Present perfect: E < R (perfect aspect, pre-present).

theorem Phenomena.TenseAspect.perfect_isPresent : perfectVisitedParis.isPresent

Present perfect: R = P (present orientation).

theorem Phenomena.TenseAspect.preterit_isPast : preteritVisitedParis.isPast

Preterit: R < P (past orientation).

theorem Phenomena.TenseAspect.preterit_is_perfective : preteritVisitedParis.isPerfective

Preterit is perfective (E = R).

@cite{heim-kratzer-1998} predicts that the distribution of deictic vs anaphoric past tense varies cross-linguistically because surface "past" can decompose differently:

English simple past = PRESENT + PERFECT (@cite{heim-kratzer-1998} §4). The tense head is PRESENT (indexical), so it can be used deictically.

German Preterit = genuine PAST pronoun (@cite{heim-kratzer-1998} §5). The tense head is PAST (anaphoric), requiring a discourse antecedent.

The empirical contrast: English: "I didn't turn off the stove." ✓ (out of the blue) German: #"Ich schaltete den Herd nicht aus." ✗ (out of the blue) German: "Ich habe den Herd nicht ausgeschaltet." ✓ (present perfect)

This data is tested against the theory in Studies/HeimKratzer1998.lean §29.

structure Phenomena.TenseAspect.TenseDeicticDatum : Type

Whether a surface past tense form can be used deictically (without a discourse-established temporal antecedent).

• language : String

  Language

• surfaceForm : String

  Surface morphological form

• sentence : String

  Example sentence

• outOfTheBlue : Bool

  Can this form be used "out of the blue"?

• underlyingMode : Core.ReferentialMode.ReferentialMode

  The underlying referential mode (indexical = deictic-compatible, anaphoric = requires antecedent)

instance Phenomena.TenseAspect.instReprTenseDeicticDatum : Repr TenseDeicticDatum

Equations

• Phenomena.TenseAspect.instReprTenseDeicticDatum = { reprPrec := Phenomena.TenseAspect.instReprTenseDeicticDatum.repr }

def Phenomena.TenseAspect.instReprTenseDeicticDatum.repr : TenseDeicticDatum → ℕ → Std.Format

Equations

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

instance Phenomena.TenseAspect.instDecidableEqTenseDeicticDatum : DecidableEq TenseDeicticDatum

Equations

• Phenomena.TenseAspect.instDecidableEqTenseDeicticDatum = Phenomena.TenseAspect.instDecidableEqTenseDeicticDatum.decEq

def Phenomena.TenseAspect.instDecidableEqTenseDeicticDatum.decEq (x✝ x✝¹ : TenseDeicticDatum) : Decidable (x✝ = x✝¹)

Equations

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

def Phenomena.TenseAspect.instBEqTenseDeicticDatum.beq : TenseDeicticDatum → TenseDeicticDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.TenseAspect.instBEqTenseDeicticDatum.beq x✝¹ x✝ = false

instance Phenomena.TenseAspect.instBEqTenseDeicticDatum : BEq TenseDeicticDatum

Equations

• Phenomena.TenseAspect.instBEqTenseDeicticDatum = { beq := Phenomena.TenseAspect.instBEqTenseDeicticDatum.beq }

def Phenomena.TenseAspect.englishSimplePastDatum : TenseDeicticDatum

English simple past: CAN be used out of the blue.

Equations

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

def Phenomena.TenseAspect.germanPreteritDatum : TenseDeicticDatum

German Preterit: CANNOT be used out of the blue.

Equations

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

def Phenomena.TenseAspect.germanPerfektDatum : TenseDeicticDatum

German Perfekt: CAN be used out of the blue (present tense head).

Equations

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

def Phenomena.TenseAspect.tenseDeicticData : List TenseDeicticDatum

The cross-linguistic deictic data set.

Equations

• Phenomena.TenseAspect.tenseDeicticData = [Phenomena.TenseAspect.englishSimplePastDatum, Phenomena.TenseAspect.germanPreteritDatum, Phenomena.TenseAspect.germanPerfektDatum]

theorem Phenomena.TenseAspect.deictic_tracks_indexical : List.map (fun (x : TenseDeicticDatum) => x.outOfTheBlue) tenseDeicticData = List.map (fun (x : TenseDeicticDatum) => x.underlyingMode == Core.ReferentialMode.ReferentialMode.indexical) tenseDeicticData

Deictic compatibility tracks indexical mode.