von Stechow 2009: tenses in compositional semantics

[vS09]'s theory: tense features are checked against a local evaluation time that shifts under attitude embedding. The key mechanism is feature checking: tense morphology bears a feature ([PAST], [PRES]) that must be checked against the local temporal anchor.

Core Mechanisms

1. Feature checking = Core.Order.holds (substrate primitive in Core/Time/Tense.lean). The "checking" terminology is von Stechow's; the underlying predicate is the framework-neutral Core.Order.holds feature refTime evalTime.
2. Perspective shift = embeddedFrame (substrate primitive in Semantics/Tense/Embedding.lean). The attitude verb sets the embedded eval time = matrix E. von Stechow calls this "perspective shift"; the operation is the framework-neutral embeddedFrame matrixFrame embeddedR embeddedE.
3. SOT as feature checking: simultaneous reading = [PRES] checked against matrix E (no deletion, no ambiguity).

The paper's second contribution is the situation-indexed attitude semantics it synthesizes from [Lew79a], [HK98], and [Ogi89]: believe's complement type shifts from propositions to situation-dependent propositions (predicates over Index), and the doxastic alternatives become world–time pairs. sitBoxAt is the universal modal over situations, with Hintikka world-only semantics the time-invariant special case (sitBoxAt_lift_eq_BoxAt); genuinely temporal accessibility constraints (temporallyBound, futureOriented) are what tie embedded tense to the matrix event time in sequence of tense.

Advantages Over Abusch

• Handles relative clause tense: feature checking works in relative clauses where the perspective time is the modified NP's temporal coordinate, not the matrix event time.
• Cleaner compositional architecture: no res movement needed.

theorem VonStechow2009.vonStechow_derives_shifted {Time : Type u_1} [LinearOrder Time] (matrixFrame : _root_.Time.ReichenbachFrame Time) (embeddedR embeddedE : Time) (hPast : Core.Order.holds Tense.past embeddedR matrixFrame.eventTime) : (Tense.embeddedFrame matrixFrame embeddedR embeddedE).isPast

[vS09] derives the shifted reading: [PAST] feature checked against matrix E. The embedded reference time is before the matrix event time.

theorem VonStechow2009.vonStechow_derives_simultaneous {Time : Type u_1} [LinearOrder Time] (matrixFrame : _root_.Time.ReichenbachFrame Time) (embeddedE : Time) : (Tense.embeddedFrame matrixFrame matrixFrame.eventTime embeddedE).isPresent

[vS09] derives the simultaneous reading: [PRES] feature checked against matrix E. The embedded reference time equals the matrix event time — no deletion rule needed.

theorem VonStechow2009.vonStechow_derives_double_access {Time : Type u_1} (matrixFrame : _root_.Time.ReichenbachFrame Time) (p : Time → Prop) (h_matrix : p matrixFrame.eventTime) (h_speech : p matrixFrame.speechTime) : p matrixFrame.eventTime ∧ p matrixFrame.speechTime

[vS09] derives double-access: [PRES] feature under past attitude verb. The present tense is checked against matrix E, but its indexical nature also requires truth at speech time.

theorem VonStechow2009.vonStechow_derives_relative_clause {Time : Type u_1} [LinearOrder Time] (rcPerspective rcRefTime : Time) (hPast : Core.Order.holds Tense.past rcRefTime rcPerspective) : rcRefTime < rcPerspective

[vS09] derives relative clause tense: the perspective time in a relative clause is the modified NP's temporal coordinate, not necessarily the matrix event time. Feature checking works uniformly regardless of the source of the eval time.

This is where von Stechow has an advantage over [Abu97]: feature checking does not require attitude semantics or res movement — any eval time source works.

theorem VonStechow2009.feature_checking_is_fullPresupposition {Time : Type u_1} [LinearOrder Time] (tp : Tense.TensePronoun) (g : Tense.TemporalAssignment Time) : Core.Order.holds tp.constraint (tp.resolve g) (tp.evalTime g) ↔ tp.fullPresupposition g

[vS09]'s feature checking is TensePronoun.fullPresupposition when the eval time resolves to the same value.

Situation-indexed attitudes

The complement type of believe shifts from W → Prop to predicates over Index W Time, and doxastic alternatives become world–time pairs: ⟦x believes p⟧(w,t) = ∀(w',t') ∈ Dox_x(w,t). p(w',t').

def VonStechow2009.sitBoxAt {W : Type u_1} {Time : Type u_2} {E : Type u_3} (R : E → Intensional.Index W Time → Intensional.Index W Time → Prop) (agent : E) (s : Intensional.Index W Time) (situations : List (Intensional.Index W Time)) (p : Intensional.Index W Time → Prop) : Prop

Universal modal over situations: p holds at every accessible world–time pair.

Equations

• VonStechow2009.sitBoxAt R agent s situations p = ∀ s' ∈ situations, R agent s s' → p s'

@[instance_reducible]

instance VonStechow2009.instDecidableSitBoxAtOfDecidablePredIndex {W : Type u_1} {Time : Type u_2} {E : Type u_3} (R : E → Intensional.Index W Time → Intensional.Index W Time → Prop) [(a : E) → (s s' : Intensional.Index W Time) → Decidable (R a s s')] (agent : E) (s : Intensional.Index W Time) (situations : List (Intensional.Index W Time)) (p : Intensional.Index W Time → Prop) [DecidablePred p] : Decidable (sitBoxAt R agent s situations p)

Equations

• VonStechow2009.instDecidableSitBoxAtOfDecidablePredIndex R agent s situations p = VonStechow2009.instDecidableSitBoxAtOfDecidablePredIndex._aux_1 R agent s situations p

def VonStechow2009.liftProp {W : Type u_1} {Time : Type u_2} (p : W → Prop) : Intensional.Index W Time → Prop

A world-proposition as a situation-proposition ignoring the temporal coordinate.

Equations

• VonStechow2009.liftProp p s = p s.world

def VonStechow2009.liftAccess {W : Type u_1} {Time : Type u_2} {E : Type u_3} (R : E → W → W → Prop) : E → Intensional.Index W Time → Intensional.Index W Time → Prop

A world-accessibility relation as a situation-accessibility relation ignoring temporal coordinates — classic Hintikka behavior, where doxastic alternatives differ only in world.

Equations

• VonStechow2009.liftAccess R agent s₁ s₂ = R agent s₁.world s₂.world

theorem VonStechow2009.sitBoxAt_lift_eq_BoxAt {W : Type u_1} {Time : Type u_2} {E : Type u_3} (R : E → W → W → Prop) (agent : E) (s : Intensional.Index W Time) (sits : List (Intensional.Index W Time)) (p : W → Prop) : sitBoxAt (liftAccess R) agent s sits (liftProp p) ↔ Doxastic.BoxAt R agent s.world (List.map (fun (x : Intensional.Index W Time) => x.world) sits) p

Hintikka semantics is the time-invariant special case: on lifted relations and propositions, the situation modal is BoxAt over the world projections.

def VonStechow2009.sitVeridicalityHolds {W : Type u_1} {Time : Type u_2} (v : Features.Veridicality) (p : Intensional.Index W Time → Prop) (s : Intensional.Index W Time) : Prop

The veridicality check at a situation: veridical predicates require the complement at the evaluation situation.

Equations

• VonStechow2009.sitVeridicalityHolds Features.Veridicality.veridical p s = p s
• VonStechow2009.sitVeridicalityHolds Features.Veridicality.nonVeridical p s = True

@[instance_reducible]

instance VonStechow2009.instDecidableSitVeridicalityHoldsOfDecidablePredIndex {W : Type u_1} {Time : Type u_2} (v : Features.Veridicality) (p : Intensional.Index W Time → Prop) [DecidablePred p] (s : Intensional.Index W Time) : Decidable (sitVeridicalityHolds v p s)

Equations

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

theorem VonStechow2009.sitVeridicalityHolds_lift {W : Type u_1} {Time : Type u_2} (v : Features.Veridicality) (p : W → Prop) (s : Intensional.Index W Time) : sitVeridicalityHolds v (liftProp p) s ↔ Doxastic.VeridicalityHolds v p s.world

Lifted veridicality is world-level veridicality.

structure VonStechow2009.SitDoxasticPredicate (W : Type u_4) (Time : Type u_5) (E : Type u_6) : Type (max (max u_4 u_5) u_6)

A doxastic predicate with situation-indexed accessibility: Dox_y(w,t) is a set of world–time pairs.

• access : E → Intensional.Index W Time → Intensional.Index W Time → Prop

  Situation-indexed accessibility relation.

• veridicality : Features.Veridicality

  Veridicality (veridical or not).

def VonStechow2009.SitDoxasticPredicate.HoldsAt {W : Type u_1} {Time : Type u_2} {E : Type u_3} (V : SitDoxasticPredicate W Time E) (agent : E) (p : Intensional.Index W Time → Prop) (s : Intensional.Index W Time) (situations : List (Intensional.Index W Time)) : Prop

⟦x V that p⟧(s): the veridicality check at s plus the universal modal over accessible situations.

Equations

• V.HoldsAt agent p s situations = (VonStechow2009.sitVeridicalityHolds V.veridicality p s ∧ VonStechow2009.sitBoxAt V.access agent s situations p)

theorem VonStechow2009.sit_veridical_entails_complement {W : Type u_1} {Time : Type u_2} {E : Type u_3} (V : SitDoxasticPredicate W Time E) (hV : V.veridicality = Features.Veridicality.veridical) (agent : E) (p : Intensional.Index W Time → Prop) (s : Intensional.Index W Time) (sits : List (Intensional.Index W Time)) (holds : V.HoldsAt agent p s sits) : p s

Veridical situation-indexed predicates entail their complement at the evaluation situation.

def VonStechow2009.liftDoxastic {W : Type u_1} {E : Type u_3} (V : Doxastic.DoxasticPredicate W E) (Time : Type u_4) : SitDoxasticPredicate W Time E

A world-level DoxasticPredicate as a situation-indexed one, with time-invariant accessibility.

Equations

• VonStechow2009.liftDoxastic V Time = { access := VonStechow2009.liftAccess V.access, veridicality := V.veridicality }

theorem VonStechow2009.liftDoxastic_holdsAt_iff {W : Type u_1} {Time : Type u_2} {E : Type u_3} (V : Doxastic.DoxasticPredicate W E) (agent : E) (p : W → Prop) (s : Intensional.Index W Time) (sits : List (Intensional.Index W Time)) : (liftDoxastic V Time).HoldsAt agent (liftProp p) s sits ↔ V.HoldsAt agent p s.world (List.map (fun (x : Intensional.Index W Time) => x.world) sits)

The lifted predicate has exactly the world-level semantics — any DoxasticPredicate analysis replays unchanged in the situation-indexed framework.

Temporal accessibility constraints

What makes the situation indexing do work beyond the lift: relations that genuinely constrain the temporal coordinate, tying the embedded clause's temporal interpretation to the matrix event time.

def VonStechow2009.temporallyBound {W : Type u_1} {Time : Type u_2} {E : Type u_3} (R : E → W → W → Prop) : E → Intensional.Index W Time → Intensional.Index W Time → Prop

Accessible situations share the evaluation time — the simultaneous reading in sequence of tense.

Equations

• VonStechow2009.temporallyBound R agent s₁ s₂ = (R agent s₁.world s₂.world ∧ s₂.time = s₁.time)

@[instance_reducible]

instance VonStechow2009.instDecidableTemporallyBoundOfDecidableEq {W : Type u_1} {Time : Type u_2} {E : Type u_3} [DecidableEq Time] (R : E → W → W → Prop) [(a : E) → (w w' : W) → Decidable (R a w w')] (a : E) (s₁ s₂ : Intensional.Index W Time) : Decidable (temporallyBound R a s₁ s₂)

Equations

• VonStechow2009.instDecidableTemporallyBoundOfDecidableEq R a s₁ s₂ = id inferInstance

def VonStechow2009.futureOriented {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] (R : E → W → W → Prop) : E → Intensional.Index W Time → Intensional.Index W Time → Prop

Accessible situations are at or after the evaluation time — forward-looking attitudes like expect and intend.

Equations

• VonStechow2009.futureOriented R agent s₁ s₂ = (R agent s₁.world s₂.world ∧ s₁.time ≤ s₂.time)

@[instance_reducible]

instance VonStechow2009.instDecidableFutureOrientedOfDecidableRelLe {W : Type u_1} {Time : Type u_2} {E : Type u_3} [LE Time] [DecidableRel fun (x1 x2 : Time) => x1 ≤ x2] (R : E → W → W → Prop) [(a : E) → (w w' : W) → Decidable (R a w w')] (a : E) (s₁ s₂ : Intensional.Index W Time) : Decidable (futureOriented R a s₁ s₂)

Equations

• VonStechow2009.instDecidableFutureOrientedOfDecidableRelLe R a s₁ s₂ = id inferInstance

Temporal tower bridge ([Abu97] ↔ ContextTower)

[Abu97]'s De Bruijn temporal indexing is 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 — and the perspective shift of this paper is pushing a temporalShift onto the tower.

def VonStechow2009.tensePronounAccessPattern {W : Type u_4} {E : Type u_5} {P : Type u_6} {T : Type u_7} (tp : Tense.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 is the origin (speech-act context time), evalTimeIndex = k the k-th embedding's time. Abusch's variable indices ARE tower depth indices for the temporal coordinate.

Equations

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

def VonStechow2009.towerFaithful {W : Type u_4} {E : Type u_5} {P : Type u_6} {T : Type u_7} (g : Tense.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.

Equations

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

theorem VonStechow2009.tense_tower_bridge {W : Type u_4} {E : Type u_5} {P : Type u_6} {T : Type u_7} (tp : Tense.TensePronoun) (g : Tense.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.

theorem VonStechow2009.tense_root_bridge {W : Type u_4} {E : Type u_5} {P : Type u_6} {T : Type u_7} (tp : Tense.TensePronoun) (c : Semantics.Context.KContext W E P T) (hEval : tp.evalTimeIndex = 0) (g : Tense.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 — root-clause temporal evaluation is origin access, Kaplan's thesis for time.

theorem VonStechow2009.tensePronounAccessPattern_root_resolves {W : Type u_4} {E : Type u_5} {P : Type u_6} {T : Type u_7} (tp : Tense.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, the origin.

theorem VonStechow2009.von_stechow_tower {W : Type u_4} {E : Type u_5} {P : Type u_6} {T : Type u_7} (g : Tense.TemporalAssignment T) (t : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (newTime : T) : Tense.updateTemporal g t.depth newTime t.depth = newTime

[vS09]'s perspective shift — the attitude verb transmits its event time to the embedded clause — as pushing a temporalShift onto the tower: the updated assignment at the tower depth yields the new time.

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

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

theorem VonStechow2009.von_stechow_tower_innermost {W : Type u_4} {E : Type u_5} {P : Type u_6} {T : Type u_7} (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.