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

@cite{von-stechow-2009}

@cite{von-stechow-2009}'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 = GramTense.constrains (substrate primitive in Core/Time/Tense.lean). The "checking" terminology is von Stechow's; the underlying predicate is the framework-neutral feature.constrains refTime evalTime.
2. Perspective shift = embeddedFrame (substrate primitive in Theories/Semantics/Tense/Basic.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).

Architectural Note

After the 0.230.452 wrapper-trim and the Phase E 0.230.456 split, this file has no concept-file companion in Theories/Semantics/Tense/. @cite{von-stechow-2009}'s contribution is terminological — the "feature checking" name for what is structurally GramTense.constrains applied at a embeddedFrame-shifted eval time. The substrate lives entirely in Core.Time.Tense and Semantics.Tense.Basic; this file collects the paper-attributed theorems.

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 Phenomena.TenseAspect.Studies.VonStechow2009.vonStechow_derives_shifted {Time : Type u_1} [LinearOrder Time] (matrixFrame : Core.Time.Reichenbach.ReichenbachFrame Time) (embeddedR embeddedE : Time) (hPast : Core.Time.Tense.GramTense.past.constrains embeddedR matrixFrame.eventTime) : (Semantics.Tense.embeddedFrame matrixFrame embeddedR embeddedE).isPast

@cite{von-stechow-2009} derives the shifted reading: [PAST] feature checked against matrix E. The embedded reference time is before the matrix event time.

theorem Phenomena.TenseAspect.Studies.VonStechow2009.vonStechow_derives_simultaneous {Time : Type u_1} [LinearOrder Time] (matrixFrame : Core.Time.Reichenbach.ReichenbachFrame Time) (embeddedE : Time) : (Semantics.Tense.embeddedFrame matrixFrame matrixFrame.eventTime embeddedE).isPresent

@cite{von-stechow-2009} derives the simultaneous reading: [PRES] feature checked against matrix E. The embedded reference time equals the matrix event time — no deletion rule needed.

theorem Phenomena.TenseAspect.Studies.VonStechow2009.vonStechow_derives_double_access {Time : Type u_1} (matrixFrame : Core.Time.Reichenbach.ReichenbachFrame Time) (p : Time → Prop) (h_matrix : p matrixFrame.eventTime) (h_speech : p matrixFrame.speechTime) : p matrixFrame.eventTime ∧ p matrixFrame.speechTime

@cite{von-stechow-2009} 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 Phenomena.TenseAspect.Studies.VonStechow2009.vonStechow_derives_relative_clause {Time : Type u_1} [LinearOrder Time] (rcPerspective rcRefTime : Time) (hPast : Core.Time.Tense.GramTense.past.constrains rcRefTime rcPerspective) : rcRefTime < rcPerspective

@cite{von-stechow-2009} 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 @cite{abusch-1997}: feature checking does not require attitude semantics or res movement — any eval time source works.

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

@cite{von-stechow-2009}'s feature checking IS TensePronoun.fullPresupposition when the eval time resolves to the same value.