Tense pronouns

[Abu97] [Hei94a] [Kra98a] [Par73]

[Par73]'s insight: a tense morpheme is a temporal pronoun — a variable with a temporal constraint and a binding mode (indexical/anaphoric/bound). TensePronoun carries the four ingredients (variable index, comparison-cell constraint, ReferentialMode, evaluation index); the constraint-as-presupposition formulation (fullPresupposition) follows [Hei94a] (commenting on [Abu97]) and [Kra98a]. The assignment infrastructure is the temporal instantiation of Assignment; all update laws are mathlib's Function.update lemmas.

Temporal variable infrastructure ([Par73])

@[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 = 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.Index W Time) : TemporalAssignment Time

Project a situation assignment to a temporal assignment: 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.Index 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.

TensePronoun ([Abu97])

structure Tense.TensePronoun : Type

[Abu97]'s unified tense denotation: a temporal variable with a presupposed comparison-cell constraint and a [Par73] binding mode. Indexical mode is rigid to speech time; bound mode is the zero tense of attitude binding ([Ogi89]).

• varIndex : ℕ
• constraint : Finset Ordering
• mode : Intensional.ReferentialMode
• 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.

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

Equations

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

@[instance_reducible]

instance Tense.instDecidableEqTensePronoun : DecidableEq TensePronoun

Equations

• Tense.instDecidableEqTensePronoun = Tense.instDecidableEqTensePronoun.decEq

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.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)

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

Equations

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

@[instance_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.bound)

@[instance_reducible]

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

Equations

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

theorem Tense.TensePronoun.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.TensePronoun.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.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.