English Tense Fragment (@cite{cumming-2026} + @cite{lakoff-1970})

@cite{cumming-2026} @cite{lakoff-1970} @cite{heim-kratzer-1998}

Paradigm entries for English tense forms from @cite{cumming-2026}, Tables 20 and 22. Each entry specifies evidential perspective (EP) and utterance perspective (UP) constraints via EPCondition and UPCondition enums.

Cumming Entries

Form	EP constraint	UP constraint	Nonfuture?
simple past	T ≤ A	T < S	yes
present prog	T ≤ A	T = S	yes
future (will)	(none)	S < T	no
will have V-ed	A < T	S < T	no
will now be V-ing	A < T	T = S	no
will (bare)	(none)	S < T	no

Lakoff Perspective Entries (§4)

TensePerspectiveEntry extends TAMEEntry with the morphological form type (synthetic vs periphrastic) and grammatical tense, connecting Cumming's evidential constraints to Lakoff's false-tense diagnostic.

def Fragments.English.Tense.simplePast : Semantics.Tense.Evidential.TAMEEntry

English simple past: T ≤ A (downstream), T < S (past).

Equations

• Fragments.English.Tense.simplePast = { label := "simple past", ep := Semantics.Tense.Evidential.EPCondition.downstream, up := Semantics.Tense.Evidential.UPCondition.past }

def Fragments.English.Tense.presentProg : Semantics.Tense.Evidential.TAMEEntry

English present progressive: T ≤ A (downstream), T = S (present).

Equations

• Fragments.English.Tense.presentProg = { label := "present progressive", ep := Semantics.Tense.Evidential.EPCondition.downstream, up := Semantics.Tense.Evidential.UPCondition.present }

def Fragments.English.Tense.future : Semantics.Tense.Evidential.TAMEEntry

English future (will): no EP constraint, S < T (future).

Equations

• Fragments.English.Tense.future = { label := "future (will)", ep := Semantics.Tense.Evidential.EPCondition.unconstrained, up := Semantics.Tense.Evidential.UPCondition.future }

def Fragments.English.Tense.willHave : Semantics.Tense.Evidential.TAMEEntry

English "will have V-ed": A < T (prospective), S < T (future).

Equations

• Fragments.English.Tense.willHave = { label := "will have V-ed", ep := Semantics.Tense.Evidential.EPCondition.prospective, up := Semantics.Tense.Evidential.UPCondition.future }

def Fragments.English.Tense.willNow : Semantics.Tense.Evidential.TAMEEntry

English "will now be V-ing": A < T (prospective), T = S (present).

Equations

• Fragments.English.Tense.willNow = { label := "will now be V-ing", ep := Semantics.Tense.Evidential.EPCondition.prospective, up := Semantics.Tense.Evidential.UPCondition.present }

def Fragments.English.Tense.willBare : Semantics.Tense.Evidential.TAMEEntry

English bare "will": no EP constraint, S < T (future).

Equations

• Fragments.English.Tense.willBare = { label := "will (bare)", ep := Semantics.Tense.Evidential.EPCondition.unconstrained, up := Semantics.Tense.Evidential.UPCondition.future }

def Fragments.English.Tense.allEntries : List Semantics.Tense.Evidential.TAMEEntry

All English tense paradigm entries.

Equations

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

def Fragments.English.Tense.nonfutureEntries : List Semantics.Tense.Evidential.TAMEEntry

English nonfuture entries.

Equations

• Fragments.English.Tense.nonfutureEntries = List.filter (fun (x : Semantics.Tense.Evidential.TAMEEntry) => x.isNonfuture) Fragments.English.Tense.allEntries

structure Fragments.English.Tense.TensePerspectiveEntryextends Semantics.Tense.Evidential.TAMEEntry : Type

A tense paradigm entry enriched with Lakoff's perspective dimensions: grammatical tense and morphological form type (synthetic vs periphrastic).

allowsFalseTense is derived: only synthetic forms permit false tense.

• label : String
• ep : EPCondition
• up : UPCondition
• mood : Option Core.Discourse.GramMood
• mirative : Option Core.Evidence.MirativityValue
• gramTense : Core.Tense.GramTense

  The grammatical tense this form realizes

• formType : Core.Morphology.Tense.TenseFormType

  Synthetic (inflectional) or periphrastic (auxiliary-based)

def Fragments.English.Tense.TensePerspectiveEntry.allowsFalseTense (e : TensePerspectiveEntry) : Bool

Does this form allow false-tense interpretations? Derived from formType: only synthetic forms can.

Equations

• e.allowsFalseTense = (e.formType == Core.Morphology.Tense.TenseFormType.synthetic)

def Fragments.English.Tense.simplePastPerspective : TensePerspectiveEntry

English simple past with perspective: synthetic, allows false past.

Equations

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

def Fragments.English.Tense.simplePresentPerspective : TensePerspectiveEntry

English simple present with perspective: synthetic, allows false uses.

Equations

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

def Fragments.English.Tense.usedTo : TensePerspectiveEntry

English periphrastic past "used to V": cannot express false past.

Equations

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

def Fragments.English.Tense.goingTo : TensePerspectiveEntry

English periphrastic future "going to V": cannot express false future.

Equations

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

theorem Fragments.English.Tense.simplePast_allows_false : simplePastPerspective.allowsFalseTense = true

Synthetic entries allow false tense.

theorem Fragments.English.Tense.simplePresent_allows_false : simplePresentPerspective.allowsFalseTense = true

theorem Fragments.English.Tense.usedTo_blocks_false : usedTo.allowsFalseTense = false

Periphrastic entries block false tense.

theorem Fragments.English.Tense.goingTo_blocks_false : goingTo.allowsFalseTense = false

def Fragments.English.Tense.kratzerSimplePast : Semantics.Tense.Decomposition.KratzerDecomposition

English simple past: Kratzer decomposition. Surface "V-ed" = PRESENT tense + PERFECT aspect. The tense head is present (indexical), so the form can be used deictically ("out of the blue").

Equations

• Fragments.English.Tense.kratzerSimplePast = { language := "English", surfaceForm := "V-ed", tensePronoun := Semantics.Tense.Decomposition.kratzerEnglishPast, hasPerfect := true }

def Fragments.English.Tense.kratzerPresentPerfect : Semantics.Tense.Decomposition.KratzerDecomposition

English present perfect: no decomposition mismatch. Surface "have V-ed" = PRESENT tense + PERFECT aspect. Identical underlying structure to simple past — the difference is that the present perfect is morphologically transparent.

Equations

• Fragments.English.Tense.kratzerPresentPerfect = { language := "English", surfaceForm := "have V-ed", tensePronoun := Semantics.Tense.Decomposition.kratzerEnglishPast, hasPerfect := true }

theorem Fragments.English.Tense.kratzerSimplePast_deictic : kratzerSimplePast.canBeDeictic = true

English simple past can be deictic (from decomposition).

theorem Fragments.English.Tense.kratzerSimplePast_underlyingPresent : kratzerSimplePast.tensePronoun.constraint = Core.Tense.GramTense.present

The underlying tense head is PRESENT, not PAST. Pastness comes from the PERF aspect head, not the tense.

theorem Fragments.English.Tense.simplePast_presentPerfect_same_decomposition : kratzerSimplePast.tensePronoun = kratzerPresentPerfect.tensePronoun ∧ kratzerSimplePast.hasPerfect = kratzerPresentPerfect.hasPerfect

Simple past and present perfect share the same underlying decomposition: both are PRESENT + PERFECT. The difference is that simple past fuses the two morphemes while present perfect makes the PERF transparent via auxiliary "have".

theorem Fragments.English.Tense.lakoff_kratzer_diverge : simplePastPerspective.gramTense = Core.Tense.GramTense.past ∧ kratzerSimplePast.tensePronoun.constraint = Core.Tense.GramTense.present

The Lakoff gramTense =.past records the surface morphology; the Kratzer constraint =.present records the underlying tense head. These are DIFFERENT for English simple past — that's Kratzer's point.