Tense Phenomena: Bridge Theorems #
@cite{lakoff-1970}
Per-theory × per-phenomenon derivation theorems connecting the empirical
data in Data.lean to the nine tense theories in
Theories/Semantics.Intensional/Tense/ and Theories/Minimalism/Tense/.
Also absorbs the former Phenomena/SequenceOfTense/Bridge.lean content:
frame verification, constructor matching, SOT parameter bridges, aspect
pipeline, ULC bridges.
Structure #
For each concrete data frame and each theory, this file proves that the
theory's mechanism produces the expected Reichenbach frame. The comparison
matrix in Comparisons/TenseTheories.lean is assembled from these
per-datum verification theorems.
Simple past satisfies PAST.
Simple present satisfies PRESENT.
Simple future satisfies FUTURE.
Simple past does NOT satisfy PRESENT or FUTURE.
GramTense.constrains agrees with isPast for simple past.
GramTense.constrains agrees with isPresent for simple present.
GramTense.constrains agrees with isFuture for simple future.
Past rule generates "walked" from "walk".
Present rule generates "walks" from "walk".
Future rule generates "will leave" from "leave".
Irregular past form overrides default.
Past participle rule generates "walked" from "walk".
Periphrastic past generates "used to walk".
Periphrastic future generates "going to leave".
All tense rules have .tense category.
All synthetic tense rules are semantically vacuous — temporal semantics comes from the Theory layer, not morphology.
English simple past perspective entry has gramTense =.past.
English simple present perspective entry has gramTense =.present.
Synthetic forms allow false tense.
Periphrastic forms block false tense.
Simple past is synthetic; "used to" is periphrastic.
An indexical past tense pronoun at root level (g maps var 1 to -2,
P = S = 0) produces a frame satisfying isPast.
An indexical present tense pronoun at root level produces
a frame satisfying isPresent (R = P).
An indexical future tense pronoun at root level produces
a frame satisfying isFuture (P < R).
The tense pronoun's presupposition matches the frame's tense classification: a past tense pronoun presupposes R < P.
The matrix "said" frame satisfies PAST.
The simultaneous embedded frame satisfies PRESENT relative to embedded P.
The shifted embedded frame satisfies PAST relative to embedded P.
The present-under-past frame satisfies PRESENT relative to embedded P.
The future-under-past frame: R > P (future relative to matrix E).
The simultaneousFrame constructor reproduces the data frame.
The shiftedFrame constructor reproduces the data frame.
English has the simultaneous reading (SOT language).
Japanese lacks the simultaneous reading (non-SOT language).
Japanese only has the shifted reading.
Both readings yield overall past relative to speech time.
Forward-shifted reading violates ULC.
Simultaneous reading satisfies ULC.
Shifted reading satisfies ULC.
The compositional pipeline from aspect to tense is well-typed.
evalPast agrees with PAST.
evalPres agrees with PointPred application at speech time.
The matrix "said" frame is perfective (E = R).
The shifted embedded frame is perfective (E = R).
Perfective aspect implies E ≤ R.
Per @cite{abusch-1997}'s analysis (formalized in
Phenomena/TenseAspect/Studies/Abusch1997.lean against the
Core.Time.Tense.TensePronoun substrate), the simultaneous reading of
"John said Mary was sick" is derived by a bound tense variable that
receives the matrix event time, and the shifted reading by a free past
variable below the matrix event time. The two theorems below verify
the data-frame projections (the simultaneous frame is isPresent,
the shifted frame is isPast) — they do not invoke TensePronoun,
since the data file defines embeddedSickSimultaneous and
embeddedSickShifted as standalone ReichenbachFrame ℤ instances
rather than as embeddedFrame matrixSaid … applications. Wiring
through the substrate would require reshaping the data file.
Per Abusch: the simultaneous data frame is isPresent.
Per Abusch: the shifted data frame is isPast.
Per @cite{von-stechow-2009}: feature checking against the
shifted local eval time. The "perspective shift" operation IS
embeddedFrame from Theories/Semantics/Tense/Basic.lean (no
separate von-Stechow-namespace primitive needed).
Von Stechow derives the simultaneous frame via [PRES] feature.
Von Stechow derives the shifted frame via [PAST] feature.
Kratzer derives the simultaneous frame via SOT deletion.
Kratzer derives the shifted frame via genuine past (no deletion).
Per @cite{ogihara-1996} (formalized in
Phenomena/TenseAspect/Studies/Ogihara1996.lean), the simultaneous
reading derives from the zero-tense reading of past: the bound variable
receives E_matrix via zeroTense_receives_binder_time. The theorem
below verifies the data-frame projection (HK1998Data's
embeddedSickSimultaneous-style embeddedFrame matrixSaid … is
isPresent).
Ogihara derives the simultaneous frame via zero tense. The zero-tense
receives matrix E by zeroTense_receives_binder_time (substrate);
the resulting frame is isPresent.
Klecha derives the modal-past data: past tense checked against modal eval time.
Deal derives the counterfactual frame: past morphology with present reference, via modal distance rather than temporal precedence. The refined ULC is satisfied (counterfactual exempt).
Zeijlstra derives the simultaneous data frame: embedded T has [uPAST] (semantically vacuous via Agree), so the embedded clause is interpreted at matrix event time.
Zeijlstra derives the shifted data frame: embedded T has [iPAST] (independent tense, no Agree), contributing genuine past semantics.
Wurmbrand classifies "wanted to leave" as future irrealis: the complement is tenseless + woll → future-oriented.
Wurmbrand classifies "believes to be sick" as propositional: NOW-anchored → simultaneous with believing.
Wurmbrand classifies "tried to leave" as restructuring: dependent on matrix → same temporal domain.
Sharvit derives the indirect question simultaneous reading: the simultaneous tense in "John asked who was sick" locates sickness at the asking time.
Sharvit derives the embedded present puzzle: present under future → simultaneous tense at future eval time.
Deal derives fake past: past morphology with present reference, via modal distance rather than temporal precedence.
Both left frames satisfy PAST.
Subordination: wouldReturn satisfies FUTURE relative to shifted P.
Shift: cameBack satisfies PAST relative to absolute P.
Both false-past frames satisfy PRESENT (despite past morphology).
False tense and fake past produce identical frames: the distinction is pragmatic (politeness vs counterfactuality), not temporal-structural.
PPS if-clause satisfies PRESENT.
FPS if-clause satisfies FUTURE.
PPS matrix satisfies FUTURE.
FPS matrix satisfies PRESENT.
Future perfect satisfies FUTURE (R > P).
When-clause satisfies PRESENT relative to implicit TO.
Past perfect satisfies PAST (R < P).
Before-clause satisfies PAST.
All §27 frames satisfy PAST.
Present perfect satisfies PRESENT (R = P: present time-sphere).
Preterit satisfies PAST (R < P: past time-sphere).
Both time-sphere frames have identical event time: the structural difference is R's relation to P, not E's location.
End-to-end derivational chain connecting Fragment entries → Theory operators → composed semantics → Reichenbach data → empirical phenomena.
The chain for English simple past:
Fragment entry (kratzerSimplePast)
↓.tensePronoun.constraint =.present (.hasPerfect = true)
Theory operators (TensePronoun + PERF + PRFV from ViewpointAspect)
↓ evalPres (PERF (PRFV V))
Composed semantics = presPerfSimple (from TenseAspectComposition)
↓ evalPres evaluates at speech time
Reichenbach frame: R = P (isPresent) — present time-sphere
↓ matches §28 data
Phenomena: perfectVisitedParis.isPresent ✓
Fragment: canBeDeictic = true → Data: outOfTheBlue = true ✓
The chain for German Preterit:
Fragment entry (kratzerPreterit)
↓.tensePronoun.constraint =.past (.hasPerfect = false)
Theory operators (TensePronoun with genuine PAST)
↓ evalPast (PRFV V).atPoint
Composed semantics = simplePast (from TenseAspectComposition)
↓ evalPast existentially quantifies over past times
Reichenbach frame: R < P (isPast) — past time-sphere
↓ matches §28 data
Phenomena: preteritVisitedParis.isPast ✓
Fragment: canBeDeictic = false → Data: outOfTheBlue = false ✓
English full chain: Fragment entry → Theory → Composed semantics → Data.
- Fragment: underlying tense head is PRESENT (not PAST)
- Fragment: the form can be used deictically (indexical mode)
- Theory→Pipeline: the decomposition maps to
presPerfSimple - Pipeline→Reichenbach: present tense head → present time-sphere
- Reichenbach→Data: matches §28
perfectVisitedParis.isPresent - Data:
outOfTheBlue = trueagrees with Fragment's deictic prediction
If ANY layer changes — Fragment decomposition, Theory operators, Pipeline composition, Reichenbach frame, or empirical data — this theorem breaks.
German Preterit full chain: Fragment → Theory → Pipeline → Data.
- Fragment: underlying tense head is PAST
- Fragment: the form CANNOT be used deictically (anaphoric mode)
- Theory→Pipeline: maps to
simplePast(genuine existential past) - Pipeline→Reichenbach: past tense head → past time-sphere
- Data:
outOfTheBlue = falseagrees with Fragment's anaphoric prediction - Data–Fragment agreement: not deictic ↔ anaphoric mode
German Perfekt chain: same underlying decomposition as English simple past (PRESENT + PERFECT), predicting deictic compatibility. The Perfekt's rise in spoken German follows from this: it fills the functional role that the anaphoric Preterit cannot (deictic past).
Zero tense chain: the SOT simultaneous reading connects Kratzer's zero tense to the existing SOT deletion mechanism.
- Theory: zero tense is bound PRESENT (not ambiguous PAST)
- Theory: surfaces as phonologically zero
- Theory: SOT deletion yields the simultaneous frame (R = P)
- Existing derivation:
kratzer_derives_embeddedSickSimultaneous