Tense and Evidence

[Cum26] [Rei47]

[Cum26] argues that English nonfuture tenses encode an evidential constraint: the speaker's evidence must be causally downstream of the described event. The formal backbone is a triple (S, A, T) — speech time, evidence-acquisition time, topic-event time — with language-specific ordering constraints on these parameters.

The (S, A, T) System

Extending Reichenbach's (S, R, E), Cumming adds A (evidence-acquisition time): the time at which the speaker acquires the evidence grounding the assertion. Nonfuture tenses (past, present) impose T ≤ A — evidence is downstream of the event. Future tense lifts this constraint.

Cross-linguistic Data

The paper's tables (17)–(22) show that Korean (-te, -ney) and Bulgarian (-l) tense morphology systematically interacts with evidential perspective. Paradigm data is in Fragments/{English/Tense, Korean/Evidentials, Bulgarian/Evidentials}; verification theorems are in Studies/Cumming2026.lean.

EP/UP Constraint Enums

EPCondition and UPCondition enumerate the distinct constraint shapes attested across the three languages. Each has a toConstraint method that recovers the predicate over EvidentialFrame ℤ. This replaces the earlier design where paradigm entries stored opaque lambdas.

Connection to Modal Evidentiality

The tense evidential constraint parallels [vFG10] kernelMust presupposition: both require non-direct evidence. (A formal bridge between the two phenomena has not been built.)

Connection to Features.Evidentiality

EPCondition is a HasEvidentialPerspective instance: each of the five EP constraint shapes maps to (an Option of) the canonical EvidentialPerspective classification in Features.Evidentiality. EPCondition.IsNonfuture and TAMEEntry.IsNonfuture are dot-notation aliases for the typeclass-derived Features.Evidentiality.IsNonfuture predicate.

Evidential Frame

structure Tense.Evidential.EvidentialFrame (Time : Type u_1) extends _root_.Time.ReichenbachFrame Time : Type u_1

Cumming's (S, A, T) frame. Extends Reichenbach with an evidence-acquisition time A. S = speechTime, T = eventTime, A = acquisitionTime. The existing referenceTime (R) stays — it governs utterance perspective independently.

• speechTime : Time
• perspectiveTime : Time
• referenceTime : Time
• eventTime : Time
• acquisitionTime : Time

  Evidence-acquisition time (A): when the speaker acquires the evidence grounding the assertion.

EP Constraint Enum

inductive Tense.Evidential.EPCondition : Type

Evidential perspective constraint shapes attested across English, Korean, and Bulgarian ([Cum26], Tables 17–22). Each value corresponds to a distinct ordering on T vs A.

• downstream : EPCondition

  T ≤ A: evidence downstream of event (English past/progressive, Bulgarian NFUT).

• strictDownstream : EPCondition

  T < A: strict downstream (Korean -te PAST, -ney PAST).

• contemporaneous : EPCondition

  T = A: contemporaneous evidence (Korean -te PRES, -ney PRES).

• prospective : EPCondition

  A < T: prospective evidence (Korean -te FUT, -ney FUT, English will-have/will-now, Bulgarian FUT).

• unconstrained : EPCondition

  No EP constraint (English bare future/will).

@[implicit_reducible]

instance Tense.Evidential.instDecidableEqEPCondition : DecidableEq EPCondition

Equations

• Tense.Evidential.instDecidableEqEPCondition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Tense.Evidential.instReprEPCondition : Repr EPCondition

Equations

• Tense.Evidential.instReprEPCondition = { reprPrec := Tense.Evidential.instReprEPCondition.repr }

def Tense.Evidential.instReprEPCondition.repr : EPCondition → ℕ → Std.Format

Equations

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

def Tense.Evidential.EPCondition.toRelation : EPCondition → Finset Ordering

Underlying comparison category: EPCondition is a domain-flavored selector over the abstract Core.Order partition. The evidential vocabulary (downstream/prospective/…) maps onto the abstract before/after/… comparison cells; the slot pair is (eventTime, acquisitionTime).

Equations

• Tense.Evidential.EPCondition.downstream.toRelation = Core.Order.notAfter
• Tense.Evidential.EPCondition.strictDownstream.toRelation = Core.Order.before
• Tense.Evidential.EPCondition.contemporaneous.toRelation = Core.Order.overlapping
• Tense.Evidential.EPCondition.prospective.toRelation = Core.Order.after
• Tense.Evidential.EPCondition.unconstrained.toRelation = Core.Order.unrestricted

def Tense.Evidential.EPCondition.toConstraint (e : EPCondition) (f : EvidentialFrame ℤ) : Prop

Recover the predicate over EvidentialFrame ℤ from an EPCondition.

Equations

• e.toConstraint f = Core.Order.holds e.toRelation f.eventTime f.acquisitionTime

def Tense.Evidential.EPCondition.toEvidentialPerspective : EPCondition → Option Features.Evidentiality.EvidentialPerspective

Map EP constraint shapes to EvidentialPerspective where applicable. Unconstrained has no single perspective.

Equations

• Tense.Evidential.EPCondition.downstream.toEvidentialPerspective = some Features.Evidentiality.EvidentialPerspective.retrospective
• Tense.Evidential.EPCondition.strictDownstream.toEvidentialPerspective = some Features.Evidentiality.EvidentialPerspective.retrospective
• Tense.Evidential.EPCondition.contemporaneous.toEvidentialPerspective = some Features.Evidentiality.EvidentialPerspective.contemporaneous
• Tense.Evidential.EPCondition.prospective.toEvidentialPerspective = some Features.Evidentiality.EvidentialPerspective.prospective
• Tense.Evidential.EPCondition.unconstrained.toEvidentialPerspective = none

@[implicit_reducible]

instance Tense.Evidential.instHasEvidentialPerspectiveEPCondition : Features.Evidentiality.HasEvidentialPerspective EPCondition

Equations

• Tense.Evidential.instHasEvidentialPerspectiveEPCondition = { toEvidentialPerspective := Tense.Evidential.EPCondition.toEvidentialPerspective }

def Tense.Evidential.EPCondition.IsNonfuture (e : EPCondition) : Prop

Dot-notation alias for the typeclass-derived Features.Evidentiality.IsNonfuture on EP constraint shapes. Downstream, strict downstream, and contemporaneous all project to retrospective/contemporaneous; prospective and unconstrained do not.

Equations

• e.IsNonfuture = Features.Evidentiality.IsNonfuture e

@[implicit_reducible]

instance Tense.Evidential.instDecidablePredEPConditionIsNonfuture : DecidablePred EPCondition.IsNonfuture

Equations

• Tense.Evidential.instDecidablePredEPConditionIsNonfuture x✝ = Tense.Evidential.instDecidablePredEPConditionIsNonfuture._aux_1 x✝

@[simp]

theorem Tense.Evidential.EPCondition.toEvidentialPerspective_downstream : downstream.toEvidentialPerspective = some Features.Evidentiality.EvidentialPerspective.retrospective

@[simp]

theorem Tense.Evidential.EPCondition.toEvidentialPerspective_strictDownstream : strictDownstream.toEvidentialPerspective = some Features.Evidentiality.EvidentialPerspective.retrospective

@[simp]

theorem Tense.Evidential.EPCondition.toEvidentialPerspective_contemporaneous : contemporaneous.toEvidentialPerspective = some Features.Evidentiality.EvidentialPerspective.contemporaneous

@[simp]

theorem Tense.Evidential.EPCondition.toEvidentialPerspective_prospective : prospective.toEvidentialPerspective = some Features.Evidentiality.EvidentialPerspective.prospective

@[simp]

theorem Tense.Evidential.EPCondition.toEvidentialPerspective_unconstrained : unconstrained.toEvidentialPerspective = none

UP Constraint Enum

inductive Tense.Evidential.UPCondition : Type

Utterance perspective constraint shapes attested across the three languages. Each value corresponds to a distinct ordering on T vs S.

• past : UPCondition

  T < S: past.

• present : UPCondition

  T = S: present.

• future : UPCondition

  S < T: future.

• nonfuture : UPCondition

  T ≤ S: nonfuture (Bulgarian NFUT).

• unconstrained : UPCondition

  No UP constraint.

@[implicit_reducible]

instance Tense.Evidential.instDecidableEqUPCondition : DecidableEq UPCondition

Equations

• Tense.Evidential.instDecidableEqUPCondition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Tense.Evidential.instReprUPCondition.repr : UPCondition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Tense.Evidential.instReprUPCondition : Repr UPCondition

Equations

• Tense.Evidential.instReprUPCondition = { reprPrec := Tense.Evidential.instReprUPCondition.repr }

def Tense.Evidential.UPCondition.toConstraint : UPCondition → EvidentialFrame ℤ → Prop

Recover the predicate over EvidentialFrame ℤ from a UPCondition.

Equations

• Tense.Evidential.UPCondition.past.toConstraint = fun (f : Tense.Evidential.EvidentialFrame ℤ) => f.eventTime < f.speechTime
• Tense.Evidential.UPCondition.present.toConstraint = fun (f : Tense.Evidential.EvidentialFrame ℤ) => f.eventTime = f.speechTime
• Tense.Evidential.UPCondition.future.toConstraint = fun (f : Tense.Evidential.EvidentialFrame ℤ) => f.speechTime < f.eventTime
• Tense.Evidential.UPCondition.nonfuture.toConstraint = fun (f : Tense.Evidential.EvidentialFrame ℤ) => f.eventTime ≤ f.speechTime
• Tense.Evidential.UPCondition.unconstrained.toConstraint = fun (x : Tense.Evidential.EvidentialFrame ℤ) => True

Tense-Evidential Paradigm

structure Tense.Evidential.TAMEEntry : Type

A row in a tense-aspect-mood-evidentiality paradigm table. Generalizes [Cum26]'s tense-evidential paradigm (Tables 17–22) with optional mood and mirativity fields, enabling unified TAME fragment entries. Existing { label, ep, up } constructions still work because mood and mirative have default values (none).

• label : String

  Morphological label (e.g., "simple past", "-te PAST")

• ep : EPCondition

  Evidential perspective constraint: T vs A

• up : UPCondition

  Utterance perspective constraint: T vs S

• mood : Option Semantics.Mood.GramMood

  Grammatical mood (indicative, subjunctive), if specified

• mirative : Option Features.Mirativity.MirativityValue

  Mirativity value (expected, unexpected, neutral), if specified

@[implicit_reducible]

instance Tense.Evidential.instHasEvidentialPerspectiveTAMEEntry : Features.Evidentiality.HasEvidentialPerspective TAMEEntry

Equations

• Tense.Evidential.instHasEvidentialPerspectiveTAMEEntry = { toEvidentialPerspective := fun (p : Tense.Evidential.TAMEEntry) => Features.Evidentiality.toEvidentialPerspective p.ep }

def Tense.Evidential.TAMEEntry.IsNonfuture (p : TAMEEntry) : Prop

Dot-notation alias for the typeclass-derived Features.Evidentiality.IsNonfuture on TAME paradigm rows. A row is nonfuture iff its EP constraint is.

Equations

• p.IsNonfuture = Features.Evidentiality.IsNonfuture p

@[implicit_reducible]

instance Tense.Evidential.instDecidablePredTAMEEntryIsNonfuture : DecidablePred TAMEEntry.IsNonfuture

Equations

• Tense.Evidential.instDecidablePredTAMEEntryIsNonfuture x✝ = Tense.Evidential.instDecidablePredTAMEEntryIsNonfuture._aux_1 x✝

def Tense.Evidential.TAMEEntry.epConstraint (p : TAMEEntry) : EvidentialFrame ℤ → Prop

The EP constraint as a predicate over EvidentialFrame ℤ.

Equations

• p.epConstraint = p.ep.toConstraint

def Tense.Evidential.TAMEEntry.upConstraint (p : TAMEEntry) : EvidentialFrame ℤ → Prop

The UP constraint as a predicate over EvidentialFrame ℤ.

Equations

• p.upConstraint = p.up.toConstraint

Core Predicates

def Tense.Evidential.downstreamEvidence (f : EvidentialFrame ℤ) : Prop

Cumming's constraint (10): evidence is downstream of the event. T ≤ A — the event precedes (or coincides with) evidence acquisition.

Equations

• Tense.Evidential.downstreamEvidence f = (f.eventTime ≤ f.acquisitionTime)

Generic Downstream Lemma

theorem Tense.Evidential.EPCondition.nonfuture_implies_downstream (ep : EPCondition) (f : EvidentialFrame ℤ) (h_nf : ep.IsNonfuture) (h_ep : ep.toConstraint f) : downstreamEvidence f

Any nonfuture EP constraint entails downstream evidence (T ≤ A). One proof, six cases — the three nonfuture cases follow from ≤, <, = respectively; the three non-nonfuture cases are eliminated by h_nf.

Presuppositional Nonfuture Meaning

def Tense.Evidential.nonfutureMeaning {W : Type u_1} (f : EvidentialFrame ℤ) (p : Bool) : Semantics.Presupposition.PartialProp W

Nonfuture meaning as a presuppositional proposition: the presupposition is that evidence is downstream (T ≤ A); the assertion is the bare propositional content p.

This captures the non-truth-conditional status of the evidential constraint: it is a felicity condition (presupposition), not part of what is asserted. Parameterized over an arbitrary world type W.

Equations

• Tense.Evidential.nonfutureMeaning f p = { presup := fun (x : W) => decide (f.eventTime ≤ f.acquisitionTime) = true, assertion := fun (x : W) => p = true }

theorem Tense.Evidential.nonfutureMeaning_presup {W : Type u_1} (f : EvidentialFrame ℤ) (p : Bool) (w : W) : (nonfutureMeaning f p).presup w = (decide (f.eventTime ≤ f.acquisitionTime) = true)

The presupposition of nonfutureMeaning checks downstream evidence.

Tower Integration: Evidential Shift

Evidential Shift as Tower Push

[Cum26]'s key insight is that nonfuture tenses encode an evidential constraint: T ≤ A (evidence is downstream of the event). In the tower framework, this is modeled as a property of the local context at the tense's depth: the evidence-acquisition time at that tower layer must be downstream of the event time.

The evidentialShift changes the evidence-acquisition time in the context, modeling the operator that introduces a new evidential perspective (e.g., a hearsay report shifts the acquisition time to report time).

def Tense.Evidential.evidentialTimeShift {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (acquisitionTime : T) : Semantics.Context.ContextShift (Semantics.Context.KContext W E P T)

Evidential shift: changes the time coordinate to the evidence-acquisition time. When the temporal coordinate of a KContext represents the evidence-acquisition time (Cumming's A), this shift moves A to a new value.

In the tower framework, a hearsay report pushes an evidential shift that sets A to the time of the report.

Equations

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

@[simp]

theorem Tense.Evidential.evidentialTimeShift_sets_time {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (acquisitionTime : T) (c : Semantics.Context.KContext W E P T) : ((evidentialTimeShift acquisitionTime).apply c).time = acquisitionTime

Pushing an evidential shift sets the time to the acquisition time.

def Tense.Evidential.downstreamAtDepth {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [Preorder T] (tower : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (eventTime : T) (depth : ℕ) : Prop

Cumming's downstream evidence constraint as a property of the tower's local context: at the tense's depth, the event time must not exceed the acquisition time (the time coordinate at that layer).

This bridges Cumming's frame-level constraint T ≤ A to the tower's depth-indexed context.

Equations

• Tense.Evidential.downstreamAtDepth tower eventTime depth = (eventTime ≤ (tower.contextAt depth).time)

theorem Tense.Evidential.downstreamAtDepth_root_eq {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [Preorder T] (c : Semantics.Context.KContext W E P T) (eventTime : T) : downstreamAtDepth (Semantics.Context.ContextTower.root c) eventTime 0 ↔ eventTime ≤ c.time

In a root tower whose origin time is the acquisition time, downstreamAtDepth at depth 0 is equivalent to the frame-level downstreamEvidence constraint.

theorem Tense.Evidential.downstream_preserved_by_nondecreasing_shift {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [Preorder T] (tower : Semantics.Context.ContextTower (Semantics.Context.KContext W E P T)) (σ : Semantics.Context.ContextShift (Semantics.Context.KContext W E P T)) (eventTime : T) (k : ℕ) (h_downstream : downstreamAtDepth tower eventTime k) (h_nondecreasing : (tower.contextAt k).time ≤ (σ.apply (tower.contextAt k)).time) : eventTime ≤ (σ.apply (tower.contextAt k)).time

The downstream constraint is preserved by nondecreasing shifts: if T ≤ A holds at depth k, and the shift at depth k doesn't decrease the time coordinate, then T ≤ A still holds after the shift.