English Tense Fragment ([Cum26] + [Lak70])

[Cum26] [Lak70] [Kra98a]

Paradigm entries for English tense forms from [Cum26], 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 English.Tense.simplePast : Tense.Evidential.TAMEEntry

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

All English tense paradigm entries.

Equations

• English.Tense.allEntries = [English.Tense.simplePast, English.Tense.presentProg, English.Tense.future, English.Tense.willHave, English.Tense.willNow, English.Tense.willBare]

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

English nonfuture entries.

Equations

• English.Tense.nonfutureEntries = List.filter (fun (x : Tense.Evidential.TAMEEntry) => decide x.IsNonfuture) English.Tense.allEntries

structure English.Tense.TensePerspectiveEntryextends 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 Semantics.Mood.GramMood
• mirative : Option Features.Mirativity.MirativityValue
• gramTense : Finset Ordering

  The grammatical tense this form realizes

• formType : Morphology.Tense.TenseFormType

  Synthetic (inflectional) or periphrastic (auxiliary-based)

def 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 == Morphology.Tense.TenseFormType.synthetic)

def 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 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 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 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 English.Tense.simplePast_allows_false : simplePastPerspective.allowsFalseTense = true

Synthetic entries allow false tense.

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

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

Periphrastic entries block false tense.

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

def English.Tense.kratzerSimplePast : Tense.SOT.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

• English.Tense.kratzerSimplePast = { tensePronoun := Tense.SOT.Decomposition.kratzerEnglishPast, hasPerfect := true }

def English.Tense.kratzerPresentPerfect : Tense.SOT.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

• English.Tense.kratzerPresentPerfect = { tensePronoun := Tense.SOT.Decomposition.kratzerEnglishPast, hasPerfect := true }

theorem English.Tense.kratzerSimplePast_deictic : kratzerSimplePast.canBeDeictic

English simple past can be deictic (from decomposition).

theorem English.Tense.kratzerSimplePast_underlyingPresent : kratzerSimplePast.tensePronoun.constraint = Tense.present

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

theorem 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 English.Tense.lakoff_kratzer_diverge : simplePastPerspective.gramTense = Tense.past ∧ kratzerSimplePast.tensePronoun.constraint = Tense.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.