Tense and Evidence

@cite{cumming-2026} @cite{reichenbach-1947}

@cite{cumming-2026} 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 Phenomena/Cumming2026/Bridge.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 @cite{von-fintel-gillies-2010} kernelMust presupposition: both require non-direct evidence. The bridge between these two phenomena is formalized in Comparisons/TenseModalEvidentiality.lean.

Connection to Core.Evidence

EPCondition.toEvidentialPerspective maps the five EP constraint shapes to the canonical EvidentialPerspective classification in Core.Evidence.

structure Semantics.Tense.Evidential.EvidentialFrame (Time : Type u_1) extends Core.Reichenbach.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.

inductive Semantics.Tense.Evidential.EPCondition : Type

Evidential perspective constraint shapes attested across English, Korean, and Bulgarian (@cite{cumming-2026}, 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).

instance Semantics.Tense.Evidential.instDecidableEqEPCondition : DecidableEq EPCondition

Equations

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

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

Equations

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

instance Semantics.Tense.Evidential.instReprEPCondition : Repr EPCondition

Equations

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

def Semantics.Tense.Evidential.instBEqEPCondition.beq : EPCondition → EPCondition → Bool

Equations

• Semantics.Tense.Evidential.instBEqEPCondition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Tense.Evidential.instBEqEPCondition : BEq EPCondition

Equations

• Semantics.Tense.Evidential.instBEqEPCondition = { beq := Semantics.Tense.Evidential.instBEqEPCondition.beq }

def Semantics.Tense.Evidential.EPCondition.toConstraint : EPCondition → EvidentialFrame ℤ → Prop

Recover the predicate over EvidentialFrame ℤ from an EPCondition.

Equations

• Semantics.Tense.Evidential.EPCondition.downstream.toConstraint = fun (f : Semantics.Tense.Evidential.EvidentialFrame ℤ) => f.eventTime ≤ f.acquisitionTime
• Semantics.Tense.Evidential.EPCondition.strictDownstream.toConstraint = fun (f : Semantics.Tense.Evidential.EvidentialFrame ℤ) => f.eventTime < f.acquisitionTime
• Semantics.Tense.Evidential.EPCondition.contemporaneous.toConstraint = fun (f : Semantics.Tense.Evidential.EvidentialFrame ℤ) => f.eventTime = f.acquisitionTime
• Semantics.Tense.Evidential.EPCondition.prospective.toConstraint = fun (f : Semantics.Tense.Evidential.EvidentialFrame ℤ) => f.acquisitionTime < f.eventTime
• Semantics.Tense.Evidential.EPCondition.unconstrained.toConstraint = fun (x : Semantics.Tense.Evidential.EvidentialFrame ℤ) => True

def Semantics.Tense.Evidential.EPCondition.isNonfuture : EPCondition → Bool

Is this EP constraint nonfuture? Downstream, strict downstream, and contemporaneous all entail T ≤ A; prospective and unconstrained do not.

Equations

• Semantics.Tense.Evidential.EPCondition.downstream.isNonfuture = true
• Semantics.Tense.Evidential.EPCondition.strictDownstream.isNonfuture = true
• Semantics.Tense.Evidential.EPCondition.contemporaneous.isNonfuture = true
• Semantics.Tense.Evidential.EPCondition.prospective.isNonfuture = false
• Semantics.Tense.Evidential.EPCondition.unconstrained.isNonfuture = false

def Semantics.Tense.Evidential.EPCondition.toEvidentialPerspective : EPCondition → Option Core.Evidence.EvidentialPerspective

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

Equations

• Semantics.Tense.Evidential.EPCondition.downstream.toEvidentialPerspective = some Core.Evidence.EvidentialPerspective.retrospective
• Semantics.Tense.Evidential.EPCondition.strictDownstream.toEvidentialPerspective = some Core.Evidence.EvidentialPerspective.retrospective
• Semantics.Tense.Evidential.EPCondition.contemporaneous.toEvidentialPerspective = some Core.Evidence.EvidentialPerspective.contemporaneous
• Semantics.Tense.Evidential.EPCondition.prospective.toEvidentialPerspective = some Core.Evidence.EvidentialPerspective.prospective
• Semantics.Tense.Evidential.EPCondition.unconstrained.toEvidentialPerspective = none

inductive Semantics.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.

instance Semantics.Tense.Evidential.instDecidableEqUPCondition : DecidableEq UPCondition

Equations

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

instance Semantics.Tense.Evidential.instReprUPCondition : Repr UPCondition

Equations

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

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

Equations

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

instance Semantics.Tense.Evidential.instBEqUPCondition : BEq UPCondition

Equations

• Semantics.Tense.Evidential.instBEqUPCondition = { beq := Semantics.Tense.Evidential.instBEqUPCondition.beq }

def Semantics.Tense.Evidential.instBEqUPCondition.beq : UPCondition → UPCondition → Bool

Equations

• Semantics.Tense.Evidential.instBEqUPCondition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

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

Recover the predicate over EvidentialFrame ℤ from a UPCondition.

Equations

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

structure Semantics.Tense.Evidential.TAMEEntry : Type

A row in a tense-aspect-mood-evidentiality paradigm table. Generalizes @cite{cumming-2026}'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 Core.Discourse.GramMood

  Grammatical mood (indicative, subjunctive), if specified

• mirative : Option Core.Evidence.MirativityValue

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

def Semantics.Tense.Evidential.TAMEEntry.isNonfuture (p : TAMEEntry) : Bool

Is this a nonfuture tense? Derived from the EP constraint.

Equations

• p.isNonfuture = p.ep.isNonfuture

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

The EP constraint as a predicate over EvidentialFrame ℤ.

Equations

• p.epConstraint = p.ep.toConstraint

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

The UP constraint as a predicate over EvidentialFrame ℤ.

Equations

• p.upConstraint = p.up.toConstraint

def Semantics.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

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

theorem Semantics.Tense.Evidential.EPCondition.nonfuture_implies_downstream (ep : EPCondition) (f : EvidentialFrame ℤ) (h_nf : ep.isNonfuture = true) (h_ep : ep.toConstraint f) : downstreamEvidence f

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

def Semantics.Tense.Evidential.nonfutureMeaning {W : Type u_1} (f : EvidentialFrame ℤ) (p : Bool) : Core.Presupposition.PrProp 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

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

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

The presupposition of nonfutureMeaning checks downstream evidence.

Evidential Shift as Tower Push

@cite{cumming-2026}'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 Semantics.Tense.Evidential.evidentialTimeShift {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (acquisitionTime : T) : Core.Context.ContextShift (Core.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 Semantics.Tense.Evidential.evidentialTimeShift_sets_time {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} (acquisitionTime : T) (c : Core.Context.KContext W E P T) : ((evidentialTimeShift acquisitionTime).apply c).time = acquisitionTime

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

def Semantics.Tense.Evidential.downstreamAtDepth {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [Preorder T] (tower : Core.Context.ContextTower (Core.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

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

theorem Semantics.Tense.Evidential.downstreamAtDepth_root_eq {W : Type u_1} {E : Type u_2} {P : Type u_3} {T : Type u_4} [Preorder T] (c : Core.Context.KContext W E P T) (eventTime : T) : downstreamAtDepth (Core.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 Semantics.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 : Core.Context.ContextTower (Core.Context.KContext W E P T)) (σ : Core.Context.ContextShift (Core.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.