Nine Theories of Tense in One Type System

The landscape

Tense is one of the most heavily theorized domains in formal semantics. The sentence “John said Mary was sick” has two readings — Mary was sick before the saying (shifted), or Mary was sick at the time of the saying (simultaneous) — and explaining how past-under-past morphology yields a simultaneous reading has occupied a substantial literature. There are at least nine distinct proposals, spanning six decades, and they agree on the core data while disagreeing on the mechanism.

Linglib formalizes all nine. This post describes how.

The unified tense pronoun

The foundation is a type in Core/Tense.lean called TensePronoun, following Abusch’s (1997) insight that a tense morpheme is a temporal pronoun — a variable (Partee 1973) with a presupposed temporal constraint and a binding mode.

structure TensePronoun where
  varIndex : ℕ
  constraint : GramTense          -- past / present / future
  mode : TenseInterpretation      -- indexical / anaphoric / bound
  evalTimeIndex : ℕ := 0          -- which eval time to check against

This single type projects onto five historical representations of temporal reference:

1. Priorean operators (Prior 1967): the constraint field — PAST means “reference time before perspective time.”
2. Reichenbach frames (Reichenbach 1947): toFrame constructs S, P, R, E from the assignment.
3. Referential variables (Partee 1973): resolve g looks up the temporal variable in the assignment.
4. Kaplan indexicals: mode = .indexical means the variable is rigid to speech time.
5. Attitude binding (Ogihara 1989): mode = .bound means the variable receives its value from an attitude verb — zero tense.

The evalTimeIndex field captures a further insight from Klecha (2016): not just attitude verbs but also modals can shift the evaluation time. In a root clause, evalTimeIndex = 0 points at speech time. Under embedding, an attitude verb updates the assignment so that the evaluation time becomes the matrix event time. The theorem evalTime_shifts_under_embedding makes this explicit.

The nine theories

Each theory gets its own file and a TenseTheory identity card recording which mechanisms it uses. The identity card has no verdict field — whether a theory “handles” a given phenomenon is determined by the existence of a derivation theorem in that theory’s file.

Semantic theories (7):

Abusch (1997) treats tense variables as undergoing res-movement out of attitude complements, yielding temporal de re — wide-scope temporal reference. This is the only theory with a temporal de re mechanism. The simultaneous reading arises when a bound variable receives the matrix event time.

Von Stechow (2009) uses feature checking: tense features [PAST] or [PRES] are checked against the local evaluation time. The simultaneous reading arises when a [PRES] feature is checked against the matrix event time. This mechanism extends uniformly to relative clauses, where Abusch’s res-movement is less natural.

Kratzer (1998) derives the simultaneous reading by SOT deletion — the embedded past morphology is deleted when it matches the matrix tense, leaving the complement tenseless (hence simultaneous). Past morphology is never ambiguous; it always means past.

Ogihara (1996) derives the same reading through ambiguity: past morphology has a zero-tense reading in which it contributes no temporal constraint. The embedded verb receives the matrix event time by binding. The predictions are identical to Kratzer’s for core SOT data; the theories differ in whether “past” is ever semantically vacuous.

Klecha (2016) extends the evaluation-time shift to modals. “John might have left” is puzzling if past tense is always checked against speech time — the leaving is past relative to the modal, not relative to now. Klecha’s mechanism is captured directly by the evalTimeIndex field on TensePronoun.

Deal (2020) refines Abusch’s Upper Limit Constraint, distinguishing temporal uses of past morphology (which obey the ULC) from counterfactual uses (which violate it). “If John were here” uses past morphology with present reference — not a temporal past but a modal-distance past.

Sharvit (2003) posits a dedicated simultaneous tense morpheme with its own semantics, rather than deriving the simultaneous reading from deletion, binding, or zero tense. This handles SOT in indirect questions (“John asked who was sick”) without the machinery that other theories require.

Syntactic theories (2):

Zeijlstra (2012) models SOT as syntactic Agree, parallel to Negative Concord. The matrix T carries [iPAST] (interpretable); the embedded T carries [uPAST] (uninterpretable, semantically vacuous via Agree). Only the matrix tense contributes temporal semantics.

Wurmbrand (2014) classifies infinitival complements into three temporal classes — future irrealis (want, decide), propositional (believe), and restructuring (try, begin) — rather than treating all infinitives as uniformly tenseless.

What they agree on

All nine theories derive the core SOT phenomena: the shifted reading, the simultaneous reading, present-under-past double access, and the SOT/non-SOT parametric variation (English vs. Japanese). The comparison file proves this:

theorem all_derive_simultaneous_different_mechanisms :
    Abusch.simultaneousMechanism ≠ KratzerTense.simultaneousMechanism ∧
    KratzerTense.simultaneousMechanism ≠ Ogihara.simultaneousMechanism ∧
    Ogihara.simultaneousMechanism ≠ Zeijlstra.simultaneousMechanism ∧
    Zeijlstra.simultaneousMechanism ≠ Sharvit.simultaneousMechanism ∧
    Sharvit.simultaneousMechanism ≠ Abusch.simultaneousMechanism

Five distinct mechanisms — binding, deletion, zero tense, Agree, dedicated simultaneous tense — all producing the same Reichenbach frame (R = P, present relative to the embedded perspective time).

Where they diverge

The theories come apart on phenomena beyond core SOT:

• Temporal de re: only Abusch. The other eight theories are silent on wide-scope temporal reference.
• Relative clause tense: Von Stechow handles this uniformly via feature checking. Abusch’s res-movement doesn’t extend naturally to relative clauses, since there is no attitude holder to provide the binding.
• Modal-tense interaction: primarily Klecha. “John might have left” requires the evaluation time to shift under a modal, which most theories don’t address.
• Counterfactual tense: only Deal. The refined ULC distinguishes temporal past from modal-distance past.
• Indirect question SOT: Sharvit’s dedicated simultaneous tense handles this directly; other theories would need additional machinery.

The theorem no_single_theory_covers_all records that every theory has gaps. minimal_cover identifies the smallest combination that covers all 22 documented phenomena: Abusch + Von Stechow + Klecha + Deal + Sharvit.

A clean divide separates the syntactic from the semantic theories: semantic_vs_syntactic_divide proves that no semantic theory uses Agree, and no syntactic theory posits temporal de re or the ULC.

The data layer

Phenomena/Tense/Data.lean contains 22 phenomena as concrete Reichenbach frames over the integers. Each frame specifies speech time, perspective time, reference time, and event time for a particular sentence and reading. “John said Mary was sick” with the simultaneous reading, for example, has S = 0, P = E = -3 (the saying event, three units in the past), and R = -3 (reference time equals the matrix event time):

The data frames are theory-neutral. Bridge theorems in Phenomena/Tense/Bridge.lean connect each frame to each theory: abusch_derives_embeddedSickSimultaneous proves that Abusch’s binding mechanism produces the simultaneous frame; kratzer_derives_embeddedSickSimultaneous proves that Kratzer’s deletion mechanism produces the same frame. The theorems verify that the frame constructors (simultaneousFrame, shiftedFrame) reproduce the data.

The Kratzer-Ogihara equivalence

One comparison is worth noting because of what it illustrates about theory comparison. Kratzer and Ogihara make identical predictions for all core SOT data. The theorem deletion_vs_ambiguity_empirically_hard records this: Kratzer has SOT deletion but no zero tense; Ogihara has zero tense but no deletion; both produce the simultaneous reading. The debate between them is about linguistic ontology — whether past morphology is ever semantically vacuous — not about truth conditions. Formalizing both theories in the same type system makes the equivalence precise: the derivation theorems produce the same Reichenbach frames, and the TenseTheory identity cards record where the mechanisms differ.

File map

Core/Tense.lean                              — TensePronoun, GramTense, variable infrastructure
Theories/IntensionalSemantics/Tense/
  Basic.lean                                  — TensePhenomenon (23), TenseTheory, shared frames
  Abusch.lean                                 — Temporal de re, binding
  VonStechow.lean                             — Feature checking
  Kratzer.lean                                — SOT deletion
  Ogihara.lean                                — Zero tense ambiguity
  Klecha.lean                                 — Modal eval time shift
  Deal.lean                                   — ULC refinement, counterfactuals
  Sharvit.lean                                — Simultaneous tense, indirect questions
Theories/Minimalism/Tense/
  Zeijlstra.lean                              — Agree-based SOT
  Wurmbrand.lean                              — Infinitival tense classification
Phenomena/Tense/
  Data.lean                                   — 22 concrete Reichenbach frames
  Bridge.lean                                 — Per-theory × per-phenomenon derivations
Comparisons/TenseTheories.lean                — 9-theory comparison matrix