@cite{von-stechow-2009}: Tenses in Compositional Semantics

@cite{von-stechow-2009}

Von Stechow'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: tense feature checked against local eval time
2. Perspective shift: attitude verb sets embedded eval time = matrix E
3. SOT as feature checking: simultaneous reading = [PRES] checked against matrix E (no deletion, no ambiguity)

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

def Semantics.Tense.FeatureChecking.checkTenseFeature {Time : Type u_1} [LinearOrder Time] (feature : Core.Tense.GramTense) (refTime evalTime : Time) : Prop

Von Stechow's tense feature checking: the tense morpheme's feature ([PAST]/[PRES]/[FUT]) is checked against the local evaluation time. The feature is satisfied when the temporal relation holds between the reference time and the eval time.

Equations

• Semantics.Tense.FeatureChecking.checkTenseFeature feature refTime evalTime = feature.constrains refTime evalTime

theorem Semantics.Tense.FeatureChecking.checkTenseFeature_eq_constrains {Time : Type u_1} [LinearOrder Time] (feature : Core.Tense.GramTense) (refTime evalTime : Time) : checkTenseFeature feature refTime evalTime ↔ feature.constrains refTime evalTime

Feature checking is equivalent to GramTense.constrains (by definition).

def Semantics.Tense.FeatureChecking.vonStechowShift {Time : Type u_1} (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) (embeddedR embeddedE : Time) : Core.Reichenbach.ReichenbachFrame Time

Von Stechow's perspective shift: the attitude verb sets the embedded evaluation time to the matrix event time. This is the same operation as embeddedFrame in IS/Tense/Basic.lean.

Equations

• Semantics.Tense.FeatureChecking.vonStechowShift matrixFrame embeddedR embeddedE = Semantics.Tense.embeddedFrame matrixFrame embeddedR embeddedE

theorem Semantics.Tense.FeatureChecking.vonStechow_is_embeddedFrame {Time : Type u_1} (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) (embeddedR embeddedE : Time) : vonStechowShift matrixFrame embeddedR embeddedE = embeddedFrame matrixFrame embeddedR embeddedE

Von Stechow's shift IS the existing embeddedFrame mechanism. This grounds the Von Stechow formalization in the shared embedding infrastructure.

theorem Semantics.Tense.FeatureChecking.vonStechow_derives_shifted {Time : Type u_1} [LinearOrder Time] (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) (embeddedR embeddedE : Time) (hPast : checkTenseFeature Core.Tense.GramTense.past embeddedR matrixFrame.eventTime) : (vonStechowShift matrixFrame embeddedR embeddedE).isPast

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

theorem Semantics.Tense.FeatureChecking.vonStechow_derives_simultaneous {Time : Type u_1} [LinearOrder Time] (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) (embeddedE : Time) (hPres : checkTenseFeature Core.Tense.GramTense.present matrixFrame.eventTime matrixFrame.eventTime) : (vonStechowShift matrixFrame matrixFrame.eventTime embeddedE).isPresent

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

theorem Semantics.Tense.FeatureChecking.vonStechow_derives_double_access {Time : Type u_1} [LinearOrder Time] (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) (hPres : checkTenseFeature Core.Tense.GramTense.present matrixFrame.eventTime matrixFrame.eventTime) (p : Time → Prop) (h_matrix : p matrixFrame.eventTime) (h_speech : p matrixFrame.speechTime) : p matrixFrame.eventTime ∧ p matrixFrame.speechTime

Von Stechow 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 Semantics.Tense.FeatureChecking.vonStechow_derives_relative_clause {Time : Type u_1} [LinearOrder Time] (rcPerspective rcRefTime : Time) (hPast : checkTenseFeature Core.Tense.GramTense.past rcRefTime rcPerspective) : rcRefTime < rcPerspective

Von Stechow 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 Abusch: the feature-checking mechanism does not require attitude semantics or res movement — any eval time source works.

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

Von Stechow's feature checking is TensePronoun.fullPresupposition when the eval time resolves to the same value.