Tense decomposition and SOT deletion

[Kra98a]'s architecture relating tense morphology to underlying tense–aspect structure, extending [Par73]'s tense–pronoun analogy. A surface tense form is a SurfaceTense: an underlying tense pronoun plus an optional PERFECT aspect head. The three pronoun values the account uses are indexicalPresent (the head of the English simple past — pastness from PERF, hence deictic), anaphoricPast (the German Preterit — requires a discourse antecedent), and boundPresent (zero tense — locally bound, surfaces as zero via Overtness). SOT deletion (sotDeletionApplicable, applyDeletion) deletes an embedded tense under morphological identity with the matrix, leaving the embedded clause temporally dependent on the matrix event time (applyDeletion_isPresent).

The paper-attributed predictions, the Fragment instances, and the divergence from [Ogi96] live in Studies/Kratzer1998.lean.

SOT deletion

def Tense.Decomposition.sotDeletionApplicable (matrixTense embeddedTense : Finset Ordering) : Bool

[Kra98a]'s SOT deletion condition: an embedded tense whose morphology is identical to the matrix tense can be optionally deleted, making the embedded clause temporally dependent on the matrix event time.

Equations

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

theorem Tense.Decomposition.past_past_deletion : sotDeletionApplicable past past = true

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

theorem Tense.Decomposition.present_past_no_deletion : sotDeletionApplicable past present = false

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

def Tense.Decomposition.applyDeletion {Time : Type u_1} (matrixFrame : _root_.Time.ReichenbachFrame Time) : _root_.Time.ReichenbachFrame Time

The embedded frame after SOT deletion: the embedded reference time becomes the matrix event time (the embedded clause inherits the matrix temporal coordinates).

Equations

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

theorem Tense.Decomposition.applyDeletion_eq_simultaneousFrame {Time : Type u_1} (matrixFrame : _root_.Time.ReichenbachFrame Time) : applyDeletion matrixFrame = simultaneousFrame matrixFrame matrixFrame.eventTime

Deletion and the SOT simultaneousFrame agree definitionally: deleting the embedded tense yields exactly the simultaneous-reading frame whose embedded event time is the matrix event time — the formal core of the Kratzer/Ogihara "same predictions" agreement.

theorem Tense.Decomposition.applyDeletion_isPresent {Time : Type u_1} (matrixFrame : _root_.Time.ReichenbachFrame Time) : (applyDeletion matrixFrame).isPresent

Deletion derives the simultaneous reading: after deletion the embedded reference time is the matrix event time, the PRESENT relation.

Surface tense

structure Tense.Decomposition.SurfaceTense : Type

[Kra98a] §4's decomposition of a surface tense form: an underlying tense pronoun plus an optional PERFECT aspect head between VP and Tense. Surface morphology can fuse the two (English simple past = indexicalPresent + PERFECT); surface-form metadata lives with the Fragment entries that instantiate this structure.

• tensePronoun : TensePronoun

  The underlying tense pronoun (tense head proper)

• hasPerfect : Bool

  Whether a PERFECT aspect head intervenes between VP and Tense

@[instance_reducible]

instance Tense.Decomposition.instDecidableEqSurfaceTense : DecidableEq SurfaceTense

Equations

• Tense.Decomposition.instDecidableEqSurfaceTense = Tense.Decomposition.instDecidableEqSurfaceTense.decEq

def Tense.Decomposition.instDecidableEqSurfaceTense.decEq (x✝ x✝¹ : SurfaceTense) : Decidable (x✝ = x✝¹)

Equations

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

def Tense.Decomposition.SurfaceTense.canBeDeictic (d : SurfaceTense) : Prop

A surface form can be used deictically ("out of the blue") iff its tense head is indexical.

Equations

• d.canBeDeictic = d.tensePronoun.isIndexical

@[instance_reducible]

instance Tense.Decomposition.instDecidableCanBeDeictic (d : SurfaceTense) : Decidable d.canBeDeictic

Equations

• Tense.Decomposition.instDecidableCanBeDeictic d = Tense.Decomposition.instDecidableCanBeDeictic._aux_1 d

def Tense.Decomposition.SurfaceTense.tenseOvertness (d : SurfaceTense) (localDomain : Bool) : Intensional.Overtness

Phonological overtness of the tense head, given locality.

Equations

• d.tenseOvertness localDomain = Intensional.Overtness.fromBinding d.tensePronoun.mode localDomain

The tense pronouns

def Tense.Decomposition.indexicalPresent : TensePronoun

The indexical PRESENT pronoun — [Kra98a] §4's tense head of the English simple past (and German Perfekt): pastness comes from the PERFECT aspect head, so the form can be used deictically ("out of the blue"). English simple past and present perfect share this head; they differ only in whether the PERF is morphologically fused.

Equations

• Tense.Decomposition.indexicalPresent = { varIndex := 0, constraint := Tense.present, mode := Intensional.ReferentialMode.indexical }

def Tense.Decomposition.anaphoricPast (n : ℕ) : TensePronoun

The anaphoric PAST pronoun — the German Preterit: a genuine past requiring a discourse-established temporal antecedent, so it cannot be used "out of the blue".

Equations

• Tense.Decomposition.anaphoricPast n = { varIndex := n, constraint := Tense.past, mode := Intensional.ReferentialMode.anaphoric }

def Tense.Decomposition.boundPresent (n : ℕ) : TensePronoun

The bound PRESENT pronoun — [Kra98a] §3's zero tense: locally bound by the attitude verb's agreement head, it surfaces as zero (Overtness.fromBinding), by the same locality that reduces locally bound entity pronouns to reflexives. This is Kratzer's alternative to [Ogi96]'s ambiguous past: the "zero" is not a reading of PAST but a distinct bound PRESENT morpheme.

Equations

• Tense.Decomposition.boundPresent n = { varIndex := n, constraint := Tense.present, mode := Intensional.ReferentialMode.bound }