Tenses and Pronouns: Partee's Structural Analogy #
@cite{abusch-1997} @cite{elbourne-2013} @cite{heim-kratzer-1998} @cite{kaplan-1989} @cite{kratzer-1998} @cite{partee-1973} @cite{klecha-2016}
Formalizes @cite{partee-1973}: tenses in English exhibit the same three-way interpretive ambiguity as pronouns — indexical, anaphoric, and bound-variable — and share the same formal mechanisms (assignment functions, variable lookup, lambda abstraction).
The unifying type for all five views of tense is Core.Tense.TensePronoun: a variable index + a presupposed temporal constraint + a
binding mode + an eval time index. The bridges in this file —
referential_past_decomposition, indexical_tense_matches_opNow,
toSitVarStatus — are projections of TensePronoun onto specific
theoretical vocabularies.
For the full tense theory comparison (Abusch, Von Stechow, Kratzer,
Ogihara, Klecha, Deal, Sharvit, Zeijlstra, Wurmbrand), see
Comparisons/TenseTheories.lean and Theories/Semantics/Tense/.
The Analogy #
| Mode | Pronouns | Tenses |
|---|---|---|
| Indexical | "I" → agent of context | present → speech time |
| Anaphoric | "he" → salient individual | past → salient narrative time |
| Bound | "his" in ∀x...his... | tense in "whenever...is..." |
Partee's main argument against Prior's tense-as-operator view: "I didn't turn off the stove" with past tense does NOT mean "at SOME past time I didn't turn off the stove" (trivially true). It means "at THAT specific time (when I left) I didn't turn off the stove." Tenses refer; they don't quantify.
Structural Parallel to Variables.lean #
The definitions here are the temporal counterparts of @cite{heim-kratzer-1998} entity
variable infrastructure in Semantics.Montague.Variables. Both are
instantiations of the generic Core.VarAssignment infrastructure:
| Generic (Core.VarAssignment) | Entity (Variables.lean) | Temporal (this file) |
|---|---|---|
VarAssignment D (ℕ → D) | Assignment m (ℕ → Ent) | TemporalAssignment Time |
lookupVar n g = g(n) | interpPronoun n g | interpTense n g |
updateVar g n d | Assignment.update g n x | updateTemporal g n t |
varLambdaAbs n body | lambdaAbsG n body | temporalLambdaAbs n body |
The algebraic structure is identical: Partee's insight is that the SAME referential mechanism operates over different domains.
Partee: indexical tenses are anchored to utterance time, just as "I"
is anchored to the speaker. Kaplan's opNow cT φ evaluates φ at context
time cT — this IS the indexical tense interpretation.
Kaplan `pronI` : character = λc. rigid(c.agent) — "I" → speaker
Temporal parallel : character = λc. rigid(c.time) — present → speech time
An indexically interpreted tense is equivalent to Kaplan's Now: both fix the temporal coordinate to a context-given value, ignoring the circumstance evaluation time.
@cite{elbourne-2013} generalizes Partee from times to situations (world–time
pairs). His SitVarStatus (free/bound) collapses Partee's three-way
distinction: indexical and anaphoric tenses both have FREE variables,
differing only in how the free variable is pragmatically resolved
(utterance context vs. discourse salience).
Map Partee's three-way classification to Elbourne's two-way.
Indexical and anaphoric → free; bound → bound.
Uses ReferentialMode.isFree for the coarsening.
Equations
Instances For
Surjective: Partee's classification is at least as fine as Elbourne's.
Not injective: indexical ≠ anaphoric but both map to free. The indexical/anaphoric distinction is a pragmatic refinement invisible to Elbourne's structural semantics.
The codebase contains both perspectives on tense:
@cite{prior-1967}: PAST P s s' := s.time < s'.time ∧ P s. Tense is an
operator that constrains temporal relations — existential quantification
over past times.
@cite{partee-1973}: interpTense n g = g n. Tense is a variable that
refers to a specific contextual time.
Partee's argument: "I didn't turn off the stove" under Prior's analysis
gives ∃t < now. ¬turn_off(stove, t) — trivially true, since there are
always past times when you weren't turning off the stove. The intended
reading is ¬turn_off(stove, t_i) where t_i is a specific time (when
you left the house). Only the referential analysis captures this.
The Priorean operators PAST/PRES/FUT in Tense/Basic.lean remain
useful for modeling tense in isolation. The referential analysis here
is needed for discourse anaphora and binding.
Partee's stove example: "I didn't turn off the stove."
Past tense introduces a temporal variable resolved to a specific contextually salient time. The negation scopes OVER the temporal reference, giving ¬P(t_i) rather than Prior's ∃t.¬P(t).
Equations
- Phenomena.TenseAspect.ComparePartee.parteeStoveExample turnedOff g n = !turnedOff (Core.Tense.interpTense n g)
Instances For
Partee's narrative example: "He turned the corner. He saw a house."
Both past tenses refer to the same (or closely related) narrative time — temporal anaphora. Under the referential analysis, both clauses evaluate at g(n) for the same discourse-salient temporal variable n. Anaphoric tenses corefer with a previously established temporal referent, just as anaphoric pronouns corefer with a previously established individual.
Equations
- Phenomena.TenseAspect.ComparePartee.narrativeAnaphora P Q g n = (P (Core.Tense.interpTense n g) && Q (Core.Tense.interpTense n g))
Instances For
The Priorean operators PAST/PRES/FUT in Tense/Basic.lean and the
referential analysis (interpTense, temporalLambdaAbs) are not competitors
but complementary layers. @cite{ogihara-1989} §2.3: tense is a variable (picks a
time) that must satisfy a temporal presupposition (the picked time is
past/present/future). The following theorems make this reconciliation formal.
The Priorean PAST operator, applied at a referentially-determined time g(n), decomposes into the conjunction of (1) the referential time precedes the speech situation and (2) the predicate holds at the referential time.
This is the formal reconciliation: the referential analysis (Partee) picks the TIME; the operator analysis (Prior) imposes the CONSTRAINT. They are not competitors but complementary layers.
@cite{ogihara-1989} §2.3: tense is a variable (picks a time) that must satisfy a temporal presupposition (the picked time is past/present/future).
Bound tense under attitude embedding: the binder (attitude verb) fills the temporal variable, yielding the simultaneous reading.
temporalLambdaAbs n body g t = body (g[n ↦ t]): the body is
evaluated with variable n set to binder time t. The tense variable
no longer refers independently — it receives the attitude's event time.
Kratzer (1998 §3) extends the Partee analogy to a FOURTH parallel: the distribution of overt vs. zero (phonologically empty) referential expressions. Just as the three-way classification (indexical/anaphoric/bound) applies uniformly to entities, times, and situations, the locality condition on zero forms applies uniformly across all three domains:
| Mode | Entity | Time | Surface |
|---|---|---|---|
| Indexical | "I" | PRESENT | overt |
| Anaphoric | "he" | PAST (German) | overt |
| Bound, local | reflexive | simultaneous (SOT) | zero |
| Bound, non-local | "him" in ∀x...him... | embedded tense (Persian) | overt |
The key generalization: bound + local agreement domain → zero. This explains why Persian has zero PRONOUNS but NOT zero TENSE (tense is in C, outside the local domain of Agr in Infl).
Overtness.fromBinding (Core/Tense.lean) formalizes this as a function
from (ReferentialMode × localDomain) to Overtness.
The four-way classification: all three referential modes produce overt forms except bound+local, which produces zero.
This extends the Partee three-way analogy with a morphophonological
dimension: the same ReferentialMode that determines how a referential
expression gets its reference ALSO determines (via locality) whether
it surfaces overtly.
The zero tense under SOT is bound + local → zero, just as
a reflexive pronoun is bound + local → reduced/zero.
This connects Kratzer's zero tense analysis to Core.Tense.Overtness.
The Partee analogy extended from three to four dimensions:
| Dimension | Origin@cite{partee-1973} | + @cite{heim-kratzer-1998} |
|---|---|---|
| Domain | Entity ↔ Time | + Situation |
| Mode | Indexical/Anaphoric/Bound | (same) |
| Resolution | Context/Discourse/Binder | (same) |
| Overtness | — | overt/zero |
The toSitVarStatus bridge from §6 collapses the indexical/anaphoric
distinction (both → free). Kratzer's Overtness.fromBinding collapses
differently: free → overt, bound + local → zero. Together, they show
that the three-way classification has TWO natural coarsenings:
- Elbourne's {free, bound} (structural)
- Kratzer's {overt, zero} (morphophonological)