@cite{heim-kratzer-1998}: More Structural Analogies Between Pronouns and Tenses

@cite{kratzer-1998} @cite{heim-kratzer-1998} @cite{klein-1994} @cite{partee-1973}Kratzer extends @cite{partee-1973}'s tense–pronoun analogy in three directions beyond the shared indexical/anaphoric/bound classification:

Core Contributions

1. Aspect decomposition of English simple past (§4): English "simple past" is morphologically fused but semantically = PRESENT tense + PERFECT aspect. This explains why English past can be used "out of the blue" (deictically): the tense head is PRESENT (indexical). German Preterit is a genuine PAST pronoun (anaphoric — requires a discourse antecedent).

2. SOT deletion (§5): the simultaneous reading under attitude embedding arises from morphological identity triggering optional deletion of the embedded tense, leaving the embedded clause tenseless (hence simultaneous). Past is NEVER ambiguous — it always encodes temporal precedence.

3. Zero forms and locality (§3): zero (phonologically empty) pronouns and tenses are licensed when a referential expression is locally bound by an agreeing head. This unifies zero tense under SOT, Japanese pro-drop, and reflexive reduction, and explains why Persian has zero pronouns but NOT zero tense (tense is in C, outside the local agreement domain of Agr/Infl).

4. Reflexive ↔ simultaneous parallel (§3): reflexive pronouns = locally bound zero pronouns; simultaneous tense = locally bound zero tense. Same locality condition, different referential domains.

Key Distinction from Ogihara

Kratzer and Ogihara make the same SOT predictions (both derive shifted and simultaneous readings) but differ on what "past" means:

• Kratzer: past is NEVER ambiguous; simultaneous = deletion of past
• Ogihara: past IS ambiguous; simultaneous = zero-tense reading of past

def Semantics.Tense.Decomposition.sotDeletionApplicable (matrixTense embeddedTense : GramTense) : Bool

Kratzer's SOT deletion: when embedded tense morphology is identical to matrix tense morphology, the embedded tense can be optionally deleted, making the embedded clause temporally dependent on the matrix event time.

matrixTense: the tense of the matrix clause embeddedTense: the tense of the embedded clause Returns whether deletion is possible.

Equations

• Semantics.Tense.Decomposition.sotDeletionApplicable matrixTense embeddedTense = (matrixTense == embeddedTense)

theorem Semantics.Tense.Decomposition.past_past_deletion : sotDeletionApplicable Core.Tense.GramTense.past Core.Tense.GramTense.past = true

Deletion is applicable for past-under-past (the core SOT case).

theorem Semantics.Tense.Decomposition.present_past_no_deletion : sotDeletionApplicable Core.Tense.GramTense.past Core.Tense.GramTense.present = false

Deletion is NOT applicable for present-under-past (no morphological identity between present and past).

def Semantics.Tense.Decomposition.applyDeletion {Time : Type u_1} (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) : Core.Reichenbach.ReichenbachFrame Time

When SOT deletion applies, the embedded reference time becomes the matrix event time (the embedded clause inherits matrix temporal coordinates).

Equations

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

theorem Semantics.Tense.Decomposition.kratzer_derives_simultaneous {Time : Type u_1} (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) (hDeletion : sotDeletionApplicable Core.Tense.GramTense.past Core.Tense.GramTense.past = true) : (applyDeletion matrixFrame).isPresent

Kratzer derives the simultaneous reading via SOT deletion. When deletion applies, R' = E_matrix, giving the PRESENT relation.

theorem Semantics.Tense.Decomposition.kratzer_derives_shifted {Time : Type u_1} [LinearOrder Time] (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) (embeddedR embeddedE : Time) (hPast : embeddedR < matrixFrame.eventTime) : (embeddedFrame matrixFrame embeddedR embeddedE).isPast

Kratzer derives the shifted reading: genuine past (no deletion). When deletion does not apply (or is not chosen), the embedded past tense contributes its own temporal precedence.

theorem Semantics.Tense.Decomposition.kratzer_deletion_yields_simultaneous {Time : Type u_1} (matrixFrame : Core.Reichenbach.ReichenbachFrame Time) : (applyDeletion matrixFrame).referenceTime = matrixFrame.eventTime

SOT deletion yields the simultaneous reading: R' = E_matrix.

structure Semantics.Tense.Decomposition.KratzerDecomposition : Type

Kratzer's decomposition of surface tense morphology into underlying tense head + optional aspect head (@cite{heim-kratzer-1998} §4).

The key insight: surface morphology can fuse tense and aspect, hiding the underlying tense head. English "simple past" fuses PRESENT + PERFECT; German Preterit is a bare PAST.

• language : String

  Language

• surfaceForm : String

  Surface morphological form

• tensePronoun : TensePronoun

  The underlying tense pronoun (tense head proper)

• hasPerfect : Bool

  Whether a PERFECT aspect head intervenes between VP and Tense

def Semantics.Tense.Decomposition.instReprKratzerDecomposition.repr : KratzerDecomposition → ℕ → Std.Format

Equations

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

instance Semantics.Tense.Decomposition.instReprKratzerDecomposition : Repr KratzerDecomposition

Equations

• Semantics.Tense.Decomposition.instReprKratzerDecomposition = { reprPrec := Semantics.Tense.Decomposition.instReprKratzerDecomposition.repr }

def Semantics.Tense.Decomposition.instDecidableEqKratzerDecomposition.decEq (x✝ x✝¹ : KratzerDecomposition) : Decidable (x✝ = x✝¹)

Equations

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

instance Semantics.Tense.Decomposition.instDecidableEqKratzerDecomposition : DecidableEq KratzerDecomposition

Equations

• Semantics.Tense.Decomposition.instDecidableEqKratzerDecomposition = Semantics.Tense.Decomposition.instDecidableEqKratzerDecomposition.decEq

instance Semantics.Tense.Decomposition.instBEqKratzerDecomposition : BEq KratzerDecomposition

Equations

• Semantics.Tense.Decomposition.instBEqKratzerDecomposition = { beq := Semantics.Tense.Decomposition.instBEqKratzerDecomposition.beq }

def Semantics.Tense.Decomposition.instBEqKratzerDecomposition.beq : KratzerDecomposition → KratzerDecomposition → Bool

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Tense.Decomposition.instBEqKratzerDecomposition.beq x✝¹ x✝ = false

def Semantics.Tense.Decomposition.KratzerDecomposition.canBeDeictic (d : KratzerDecomposition) : Bool

Can this form be used deictically ("out of the blue")? Derived: indexical tense head → deictic-compatible.

Equations

• d.canBeDeictic = d.tensePronoun.isIndexical

def Semantics.Tense.Decomposition.KratzerDecomposition.tenseOvertness (d : KratzerDecomposition) (localDomain : Bool) : Core.Tense.Overtness

Phonological overtness of the tense head, given locality.

Equations

• d.tenseOvertness localDomain = Core.Tense.Overtness.fromBinding d.tensePronoun.mode localDomain

Kratzer (1998 §4): English "simple past" is morphologically fused but semantically decomposes into PRESENT tense + PERFECT aspect. The tense head is present (indexical, anchored to speech time); the aspect head (PERF) introduces temporal precedence. This is literally presPerfSimple from TenseAspectComposition.lean.

German Preterit, by contrast, has a genuine PAST tense head with no intervening PERF. The PAST pronoun is anaphoric — it requires a discourse-salient temporal antecedent. This explains the striking contrast:

English: "I didn't turn off the stove." ✓ (out of the blue — deictic) German: #"Ich schaltete den Herd nicht aus." ✗ (needs narrative context) German: "Ich habe den Herd nicht ausgeschaltet." ✓ (present perfect ok)

def Semantics.Tense.Decomposition.kratzerEnglishPast : TensePronoun

Kratzer's English simple past = PRESENT tense + PERFECT aspect. The tense head is PRESENT (indexical-compatible), so the surface form can be used deictically. Pastness comes from the PERF aspect head.

Equations

• Semantics.Tense.Decomposition.kratzerEnglishPast = { varIndex := 0, constraint := Core.Tense.GramTense.present, mode := Core.ReferentialMode.ReferentialMode.indexical }

def Semantics.Tense.Decomposition.kratzerGermanPreterit (n : ℕ) : TensePronoun

German Preterit: a genuine PAST pronoun. Must be anaphoric — requires a discourse-established temporal antecedent. Cannot be used "out of the blue" in modern German.

Equations

• Semantics.Tense.Decomposition.kratzerGermanPreterit n = { varIndex := n, constraint := Core.Tense.GramTense.past, mode := Core.ReferentialMode.ReferentialMode.anaphoric }

theorem Semantics.Tense.Decomposition.english_past_is_present : kratzerEnglishPast.constraint = Core.Tense.GramTense.present

English simple past has PRESENT tense constraint. Pastness is in the aspect (PERF), not the tense head.

theorem Semantics.Tense.Decomposition.german_preterit_is_past (n : ℕ) : (kratzerGermanPreterit n).constraint = Core.Tense.GramTense.past

German Preterit has PAST tense constraint.

theorem Semantics.Tense.Decomposition.english_deictic_german_anaphoric (n : ℕ) : kratzerEnglishPast.isIndexical = true ∧ (kratzerGermanPreterit n).isIndexical = false

English simple past is indexical-compatible: can be used "out of the blue." German Preterit forces anaphoric mode: cannot be used "out of the blue."

theorem Semantics.Tense.Decomposition.english_past_eq_presPerfSimple {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (V : Aspect.Core.EventPred W Time) (tc : Time) (w : W) : TenseAspectComposition.presPerfSimple V tc w ↔ ∃ (pts : Core.Time.Interval Time), Aspect.Core.RB pts tc ∧ Aspect.Core.PRFV V w pts

Kratzer's aspect decomposition bridge: the English simple past (PRESENT + PERFECT) maps to presPerfSimple from the compositional tense–aspect pipeline. The PRESENT tense head contributes evalPres; the PERFECT aspect head contributes PERF (PRFV V).

presPerfSimple V tc w = evalPres (PERF (PRFV V)) tc w

This is the central prediction: English simple past and English present perfect have the SAME compositional semantics. They differ only in whether the PERF is morphologically fused or transparent.

theorem Semantics.Tense.Decomposition.german_preterit_eq_simplePast {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (V : Aspect.Core.EventPred W Time) (tc : Time) (w : W) : TenseAspectComposition.simplePast V tc w ↔ ∃ t < tc, Aspect.Core.PRFV V w (Core.Time.Interval.point t)

German Preterit maps to simplePast from the pipeline: genuine past tense (existential over past times) + perfective aspect.

Kratzer (1998 §3): zero (phonologically empty) referential expressions arise when a bound variable is in a local agreement domain. This applies uniformly to pronouns and tenses:

• Zero tense under SOT: the embedded tense is locally bound by the attitude verb's Agr → surfaces as ∅
• Japanese subject pro: locally bound by Agr → surfaces as ∅
• Persian: zero PRONOUNS (locally bound by Agr) but NOT zero TENSE (tense is in C, outside the local domain of Agr in Infl)

The distribution of overt vs. zero follows from Core.Tense.Overtness.

def Semantics.Tense.Decomposition.kratzerZeroTense (n : ℕ) : TensePronoun

Zero tense: a bound present tense in a local agreement domain.

Under SOT in English, the embedded "past" morphology is analyzed as a locally bound PRESENT tense that surfaces as zero because of agreement locality. This is Kratzer's alternative to Ogihara's zero-tense ambiguity: the "zero" isn't an ambiguity of PAST — it's a genuinely different morpheme (bound PRESENT) licensed by locality.

Equations

• Semantics.Tense.Decomposition.kratzerZeroTense n = { varIndex := n, constraint := Core.Tense.GramTense.present, mode := Core.ReferentialMode.ReferentialMode.bound }

theorem Semantics.Tense.Decomposition.zero_tense_is_present (n : ℕ) : (kratzerZeroTense n).constraint = Core.Tense.GramTense.present

Zero tense has present constraint (not past). Past is NEVER zero/ambiguous in Kratzer's theory.

theorem Semantics.Tense.Decomposition.zero_tense_overtness (n : ℕ) : Core.Tense.Overtness.fromBinding (kratzerZeroTense n).mode true = Core.Tense.Overtness.zero

Zero tense surfaces as zero (from Core.Tense.Overtness).

theorem Semantics.Tense.Decomposition.past_never_zero : (kratzerZeroTense 1).constraint = Core.Tense.GramTense.present

Kratzer's key claim: past is NEVER zero tense. The zero morpheme under SOT is a bound PRESENT, not an ambiguous PAST. Contrast with kratzerZeroTense which IS zero but is PRESENT.

Kratzer (1998 §3) draws an explicit structural parallel between reflexive binding and simultaneous tense:

• Reflexive pronouns = locally bound entity pronouns → zero/reduced form
• Simultaneous tense = locally bound temporal pronoun → zero tense

Both are instances of the same generalization: local binding by an agreeing head yields a phonologically reduced (zero) referential expression. The locality condition is the same; only the domain differs (entities vs. times).

theorem Semantics.Tense.Decomposition.reflexive_simultaneous_parallel (n : ℕ) : (kratzerZeroTense n).isBound = true ∧ Core.Tense.Overtness.fromBinding (kratzerZeroTense n).mode true = Core.Tense.Overtness.zero

The reflexive ↔ simultaneous parallel: both are locally bound referential expressions that surface as zero.

Left conjunct: zero tense is bound (like a reflexive). Right conjunct: it surfaces as zero (like reflexive morphology).

theorem Semantics.Tense.Decomposition.german_preterit_always_overt (n : ℕ) (localDomain : Bool) : Core.Tense.Overtness.fromBinding (kratzerGermanPreterit n).mode localDomain = Core.Tense.Overtness.overt

The German Preterit is NOT zero-compatible: it's free (anaphoric), so it surfaces as overt morphology regardless of locality. This parallels overt (non-reflexive) pronouns.

theorem Semantics.Tense.Decomposition.english_indexical_always_overt (localDomain : Bool) : Core.Tense.Overtness.fromBinding kratzerEnglishPast.mode localDomain = Core.Tense.Overtness.overt

English indexical tense is also always overt: free expressions surface as overt regardless of locality.