Unified Tense Pronoun Architecture

[Abu97] [Hei94a] [Kra98a] [Par73] [vS09] [Ogi89]

[Par73]'s insight: a tense morpheme is a temporal pronoun — a variable with a temporal constraint and a binding mode (indexical/anaphoric/bound). The constraint-as-presupposition formulation follows [Hei94a] (commenting on [Abu97]) and [Kra98a]. This single concept projects onto five representations of temporal reference in the codebase:

1. Priorean operators (PAST/PRES/FUT): Core.Order.holds constraint
2. Reichenbach frames (S, P, R, E): TensePronoun.toFrame
3. Referential variables: TensePronoun.resolve
4. Kaplan indexicals (rigid to speech time): mode =.indexical
5. Attitude binding (zero tense, [Ogi89]): mode =.bound

The existing ad-hoc bridge theorems (referential_past_decomposition, temporallyBound_gives_simultaneous, indexical_tense_matches_opNow, ogihara_bound_tense_simultaneous) become trivial projections from this unified type.

Implementation notes

The shared tense-pronoun substrate (TensePronoun, …) the Tense/ and Attitudes/ theories build on. A tense constraint is a Finset Ordering comparison category (Core.Order); the temporal primitives it imports (Reichenbach/Relation/WorldTimeIndex) stay in Core/.

SOTParameter

inductive Tense.SOTParameter : Type

Sequence of Tenses (SOT) parameter.

Languages differ in how embedded tense interacts with matrix tense:

• SOT languages (English): Embedded tense is relative to matrix
• Non-SOT languages (Japanese): Embedded tense is absolute

• relative : SOTParameter
• absolute : SOTParameter

@[implicit_reducible]

instance Tense.instDecidableEqSOTParameter : DecidableEq SOTParameter

Equations

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

@[implicit_reducible]

instance Tense.instReprSOTParameter : Repr SOTParameter

Equations

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

def Tense.instReprSOTParameter.repr : SOTParameter → ℕ → Std.Format

Equations

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

TenseInterpretation

@[reducible, inline]

abbrev Tense.TenseInterpretation : Type

Tense interpretation modes. Tenses parallel pronouns: indexical (deictic), anaphoric (discourse-bound), and bound variable (zero tense).

This is an alias for Intensional.ReferentialMode.ReferentialMode, which captures Partee's insight that the same three-way classification applies to both pronouns and tenses.

Equations

• Tense.TenseInterpretation = Intensional.ReferentialMode.ReferentialMode

Temporal Variable Infrastructure ([Par73])

Temporal assignment functions are the temporal instantiation of Core.Assignment (Assignment Time = ℕ → Time). All update laws are mathlib's Function.update lemmas.

@[reducible, inline]

abbrev Tense.TemporalAssignment (Time : Type u_1) : Type u_1

Temporal assignment function: maps variable indices to times. The temporal analogue of H&K's Assignment (ℕ → Entity).

Equations

• Tense.TemporalAssignment Time = Core.Assignment Time

@[reducible, inline]

abbrev Tense.updateTemporal {Time : Type u_1} (g : TemporalAssignment Time) (n : ℕ) (t : Time) : TemporalAssignment Time

Modified temporal assignment g[n ↦ t]. Specializes Function.update.

Equations

• Tense.updateTemporal g n t = Function.update g n t

@[reducible, inline]

abbrev Tense.interpTense {Time : Type u_1} (n : ℕ) (g : TemporalAssignment Time) : Time

Temporal variable denotation: ⟦tₙ⟧^g = g(n).

Equations

• Tense.interpTense n g = g n

@[reducible, inline]

abbrev Tense.temporalLambdaAbs {Time : Type u_1} {α : Type u_2} (n : ℕ) (body : TemporalAssignment Time → α) : TemporalAssignment Time → Time → α

Temporal lambda abstraction: bind a time variable.

Partee's bound tense: "Whenever Mary phones, Sam is asleep" — present tense bound by "whenever", just as "Every farmer beats his donkey" has "his" bound by "every farmer".

Equations

• Tense.temporalLambdaAbs n body g t = body (Function.update g n t)

def Tense.situationToTemporal {W : Type u_1} {Time : Type u_2} (g : ℕ → Intensional.WorldTimeIndex W Time) : TemporalAssignment Time

Project a situation assignment to a temporal assignment. This is the formal bridge between situation semantics and tense semantics: the temporal coordinate of each situation is extracted.

Equations

• Tense.situationToTemporal g n = (g n).time

theorem Tense.situation_temporal_commutes {W : Type u_1} {Time : Type u_2} (g : ℕ → Intensional.WorldTimeIndex W Time) (n : ℕ) : interpTense n (situationToTemporal g) = (g n).time

Temporal interpretation via situation assignment commutes with time projection: interpTense n (π g) = (g n).time.

theorem Tense.zeroTense_receives_binder_time {Time : Type u_1} (g : TemporalAssignment Time) (n : ℕ) (binderTime : Time) : interpTense n (updateTemporal g n binderTime) = binderTime

Zero tense: a bound tense variable contributes no independent temporal constraint. When an attitude verb binds it, the variable receives the matrix event time. This is the SOT mechanism: the "past" morphology on the embedded verb is agreement, not a semantic tense.

SitProp (Prop-valued)

@[reducible, inline]

abbrev Tense.SitProp (W : Type u_1) (Time : Type u_2) : Type (max u_2 u_1)

Type of situation-level propositions (Prop-valued, for proof-level temporal reasoning).

A temporal predicate takes a situation and returns a truth value. This is what tense operators modify. Re-exported by Semantics/Attitudes/SituationDependent.lean and Semantics/Tense/Compositional.lean for downstream use.

Equations

• Tense.SitProp W Time = (Intensional.WorldTimeIndex W Time → Prop)

TensePronoun ([Abu97])

structure Tense.TensePronoun : Type

[Abu97]'s unified tense denotation.

A tense morpheme introduces a temporal variable with:

• A variable index in the temporal assignment
• A presupposed temporal constraint (past/present/future)
• A binding mode (indexical, anaphoric, or bound)

This unifies five views of tense:

• Priorean: Core.Order.holds constraint (temporal ordering)
• Reichenbach: resolve g = R, perspective time = P
• Referential: resolve g = interpTense varIndex g
• Kaplan indexical: mode =.indexical → rigid to speech time
• Attitude binding: mode =.bound → zero tense

• varIndex : ℕ
• constraint : Finset Ordering
• mode : TenseInterpretation
• evalTimeIndex : ℕ

  Index of the evaluation time variable in the temporal assignment. Default 0 = speech time slot. Under embedding, attitude verbs update this index to point at the matrix event time. [Kle16]: modals can also shift the eval time index.

@[implicit_reducible]

instance Tense.instDecidableEqTensePronoun : DecidableEq TensePronoun

Equations

• Tense.instDecidableEqTensePronoun = Tense.instDecidableEqTensePronoun.decEq

def Tense.instDecidableEqTensePronoun.decEq (x✝ x✝¹ : TensePronoun) : Decidable (x✝ = x✝¹)

Equations

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

def Tense.TensePronoun.resolve {Time : Type u_1} (tp : TensePronoun) (g : TemporalAssignment Time) : Time

Resolve: look up the temporal variable.

Equations

• tp.resolve g = Tense.interpTense tp.varIndex g

def Tense.TensePronoun.presupposition {Time : Type u_1} [LinearOrder Time] (tp : TensePronoun) (resolvedTime perspectiveTime : Time) : Prop

Presupposition: the constraint applied to the resolved time.

Equations

• tp.presupposition resolvedTime perspectiveTime = Core.Order.holds tp.constraint resolvedTime perspectiveTime

def Tense.TensePronoun.toFrame {Time : Type u_1} (tp : TensePronoun) (g : TemporalAssignment Time) (speechTime perspectiveTime eventTime : Time) : _root_.Time.ReichenbachFrame Time

Construct the Reichenbach frame. R = g(varIndex), P = perspectiveTime.

Equations

• tp.toFrame g speechTime perspectiveTime eventTime = { speechTime := speechTime, perspectiveTime := perspectiveTime, referenceTime := tp.resolve g, eventTime := eventTime }

def Tense.TensePronoun.isIndexical (tp : TensePronoun) : Prop

Equations

• tp.isIndexical = (tp.mode = Intensional.ReferentialMode.ReferentialMode.indexical)

@[implicit_reducible]

instance Tense.TensePronoun.instDecidableIsIndexical (tp : TensePronoun) : Decidable tp.isIndexical

Equations

• tp.instDecidableIsIndexical = Tense.TensePronoun.instDecidableIsIndexical._aux_1 tp

def Tense.TensePronoun.isBound (tp : TensePronoun) : Prop

Equations

• tp.isBound = (tp.mode = Intensional.ReferentialMode.ReferentialMode.bound)

@[implicit_reducible]

instance Tense.TensePronoun.instDecidableIsBound (tp : TensePronoun) : Decidable tp.isBound

Equations

• tp.instDecidableIsBound = Tense.TensePronoun.instDecidableIsBound._aux_1 tp

TensePronoun Bridge Theorems

def Tense.TensePronoun.evalTime {Time : Type u_1} (tp : TensePronoun) (g : TemporalAssignment Time) : Time

Resolve the evaluation time from the assignment. In root clauses (evalTimeIndex = 0, g(0) = speech time), this is speech time. Under embedding, the attitude verb updates the assignment so that g(evalTimeIndex) = matrix event time.

Equations

• tp.evalTime g = Tense.interpTense tp.evalTimeIndex g

def Tense.TensePronoun.fullPresupposition {Time : Type u_1} [LinearOrder Time] (tp : TensePronoun) (g : TemporalAssignment Time) : Prop

Full presupposition: the tense constraint checked against the resolved evaluation time (not just a bare perspective time parameter). This makes the eval time compositionally determined rather than stipulated.

Equations

• tp.fullPresupposition g = Core.Order.holds tp.constraint (tp.resolve g) (tp.evalTime g)

theorem Tense.evalTime_root_is_speech {Time : Type u_1} (tp : TensePronoun) (g : TemporalAssignment Time) (speechTime : Time) (hEval : tp.evalTimeIndex = 0) (hRoot : g 0 = speechTime) : tp.evalTime g = speechTime

When evalTimeIndex = 0 and g(0) = speechTime, the evaluation time is speech time. This is the root-clause default: tense is checked against speech time.

theorem Tense.evalTime_shifts_under_embedding {Time : Type u_1} (tp : TensePronoun) (g : TemporalAssignment Time) (matrixEventTime : Time) : tp.evalTime (updateTemporal g tp.evalTimeIndex matrixEventTime) = matrixEventTime

Updating the eval time index gives Von Stechow's perspective shift: the embedded tense is now checked against a different time (the matrix event time). This is how attitude verbs "transmit" their event time.

theorem Tense.TensePronoun.bound_resolve_eq_binder {Time : Type u_1} (tp : TensePronoun) (g : TemporalAssignment Time) (binderTime : Time) : tp.resolve (updateTemporal g tp.varIndex binderTime) = binderTime

Resolving a bound tense under binding yields the binder time.

theorem Tense.TensePronoun.bound_present_simultaneous {Time : Type u_1} (tp : TensePronoun) (g : TemporalAssignment Time) (speechTime perspTime eventTime : Time) (hBind : tp.resolve g = perspTime) (_hPres : tp.constraint = present) : (tp.toFrame g speechTime perspTime eventTime).isPresent

A present-constraint bound tense under binding gives R = P (simultaneous). The hPres hypothesis constrains the theorem to present tenses; the frame equality follows from hBind alone (R = resolve = perspTime).

def Tense.doubleAccess {Time : Type u_1} (p : Time → Prop) (speechTime matrixEventTime : Time) : Prop

Double-access: present-under-past requires the complement to hold at BOTH speech time (indexical rigidity) AND matrix event time (attitude accessibility).

Equations

• Tense.doubleAccess p speechTime matrixEventTime = (p speechTime ∧ p matrixEventTime)

theorem Tense.TensePronoun.indexical_present_at_speech {Time : Type u_1} [LinearOrder Time] (tp : TensePronoun) (resolvedTime speechTime : Time) (hPres : tp.constraint = present) (hPresup : tp.presupposition resolvedTime speechTime) : resolvedTime = speechTime

An indexical present tense presupposes resolution to speech time.

Overtness ([Kra98a])

inductive Tense.Overtness : Type

Phonological overtness of a referential expression ([Kra98a] §3).

Applies uniformly to pronouns and tenses: English has zero tense under SOT (bound present surfaces as ∅); Japanese has zero pronouns in subject position (locally bound by Agr). Persian has zero pronouns but NOT zero tense (tense is in C, outside the local agreement domain).

The distribution of overt vs. zero is governed by locality of agreement: a referential expression that is locally bound by an agreeing head surfaces as zero.

• overt : Overtness
• zero : Overtness

@[implicit_reducible]

instance Tense.instDecidableEqOvertness : DecidableEq Overtness

Equations

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

def Tense.instReprOvertness.repr : Overtness → ℕ → Std.Format

Equations

• Tense.instReprOvertness.repr Tense.Overtness.overt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tense.Overtness.overt")).group prec✝
• Tense.instReprOvertness.repr Tense.Overtness.zero prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Tense.Overtness.zero")).group prec✝

@[implicit_reducible]

instance Tense.instReprOvertness : Repr Overtness

Equations

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

@[implicit_reducible]

instance Tense.instInhabitedOvertness : Inhabited Overtness

Equations

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

def Tense.Overtness.fromBinding : Intensional.ReferentialMode.ReferentialMode → (localDomain : Bool) → Overtness

Kratzer's locality generalization (1998, formula 26):

A referential expression that is locally bound by an agreeing head surfaces as zero. Free (indexical or anaphoric) expressions surface as overt. This unifies:

• Reflexives = locally bound entity pronouns → zero/reduced
• Simultaneous tense = locally bound temporal pronoun → zero under SOT
• Japanese subject pro = locally bound by Agr → zero
• Persian pronouns = locally bound by Agr → zero, but tense is NOT local to Agr (tense is in C) → overt

Equations

• Tense.Overtness.fromBinding Intensional.ReferentialMode.ReferentialMode.bound true = Tense.Overtness.zero
• Tense.Overtness.fromBinding x✝¹ x✝ = Tense.Overtness.overt

theorem Tense.Overtness.free_always_overt (m : Intensional.ReferentialMode.ReferentialMode) (l : Bool) (hFree : m.isFree = true) : fromBinding m l = overt

Free (indexical or anaphoric) expressions are always overt.

theorem Tense.Overtness.bound_local_is_zero : fromBinding Intensional.ReferentialMode.ReferentialMode.bound true = zero

Bound expressions in a local domain are zero.

theorem Tense.Overtness.bound_nonlocal_is_overt : fromBinding Intensional.ReferentialMode.ReferentialMode.bound false = overt

Bound expressions outside the local domain remain overt. This is the Persian case: tense is bound but not in a local agreement domain (tense is in C, Agr is in Infl).

Temporal Tower Bridge ([Abu97] ↔ ContextTower)

The key bridge showing that [Abu97]'s De Bruijn temporal indexing is already tower-style depth access. TensePronoun.evalTimeIndex is a depth-relative index into the tower: when the temporal assignment encodes tower time coordinates (g k = (tower.contextAt k).time), interpTense agrees with AccessPattern.resolve.

• tensePronounAccessPattern — converts TensePronoun.evalTimeIndex to an AccessPattern with depth :=.relative tp.evalTimeIndex
• tense_tower_bridge — when g encodes tower time coordinates, interpTense agrees with AccessPattern.resolve
• tense_root_bridge — root clause: evalTimeIndex = 0 means origin time
• von_stechow_tower — pushing a temporal shift = Von Stechow's perspective shift

def Tense.tensePronounAccessPattern {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tp : TensePronoun) : Semantics.Context.AccessPattern (Semantics.Context.KContext W E P T) T

Convert a TensePronoun's eval-time index to an AccessPattern that reads the time coordinate at the corresponding tower depth.

evalTimeIndex = 0 → origin (speech-act context time) evalTimeIndex = k → depth k (the k-th embedding's time)

This makes explicit the observation that Abusch's variable indices ARE tower depth indices for the temporal coordinate.

Equations

• Tense.tensePronounAccessPattern tp = { depth := Semantics.Context.DepthSpec.relative tp.evalTimeIndex, project := Semantics.Context.KContext.time }

def Tense.towerFaithful {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (g : TemporalAssignment T) (t : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) : Prop

A temporal assignment that faithfully represents a tower: g k returns the time coordinate at tower depth k. This is the bridge condition connecting the variable-assignment world to the tower world.

Equations

• Tense.towerFaithful g t = ∀ (k : ℕ), g k = (t.contextAt k).time

theorem Tense.tense_tower_bridge {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tp : TensePronoun) (g : TemporalAssignment T) (t : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (hFaithful : towerFaithful g t) : tp.evalTime g = (tensePronounAccessPattern tp).resolve t

When the temporal assignment encodes tower time coordinates, interpTense at the eval-time index agrees with resolving the tensePronounAccessPattern against the tower.

This is the central result: Abusch's De Bruijn indexing IS tower-depth access for the temporal coordinate.

theorem Tense.tense_root_bridge {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tp : TensePronoun) (c : Semantics.Context.KContext W E P T) (hEval : tp.evalTimeIndex = 0) (g : TemporalAssignment T) (hFaithful : towerFaithful g (Semantics.Context.ContextTower.root c)) : tp.evalTime g = c.time

In a root tower (no shifts), evalTimeIndex = 0 accesses the origin time. This is the root-clause default: tense is checked against speech time.

Combined with evalTime_root_is_speech, this shows that root-clause temporal evaluation is origin access — exactly Kaplan's thesis for time.

theorem Tense.tensePronounAccessPattern_root_resolves {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (tp : TensePronoun) (hEval : tp.evalTimeIndex = 0) (c : Semantics.Context.KContext W E P T) : (tensePronounAccessPattern tp).resolve (Semantics.Context.ContextTower.root c) = c.time

The access pattern for a root-clause tense pronoun (evalTimeIndex = 0) resolves to depth 0, which is the origin.

theorem Tense.von_stechow_tower {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (g : TemporalAssignment T) (t : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (newTime : T) : updateTemporal g t.depth newTime t.depth = newTime

[vS09]'s perspective shift — the attitude verb transmits its event time to the embedded clause — corresponds to pushing a temporalShift onto the tower.

Concretely: the updated assignment at the tower depth yields the new time.

theorem Tense.von_stechow_tower_preserves {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (g : TemporalAssignment T) (t : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (newTime : T) (hFaithful : towerFaithful g t) (k : ℕ) (hk : k < t.depth) : updateTemporal g t.depth newTime k = (t.contextAt k).time

Under faithful encoding, layers below the push point are preserved.

theorem Tense.von_stechow_tower_innermost {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (t : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (newTime : T) : (t.push (Semantics.Context.temporalShift newTime)).innermost.time = newTime

Pushing a temporal shift assigns newTime to the new depth in the extended tower, mirroring von_stechow_tower on the assignment side.