Cumming (2026): Tense and evidence

This file formalizes Cumming's answer to Ninan's puzzle, that a future-tense sentence can be asserted on prior inferential grounds while the past-tense sentence about the same event cannot. Cumming, amending Cariani, assigns the nonfuture tenses the non-truth-conditional constraint that the speaker's evidence be downstream of the event, and the future forms no such constraint. A cell of a tense-evidential paradigm constrains three relations of the frame, the evidential perspective, of the event to the acquisition of the evidence, the relation of the acquisition to speech, and the utterance perspective, of the event to speech, each a cell of the tense partition. Under the Korean evidentials -te and -ney of Lee and the Bulgarian -l of Koev, the evidential fixes the relation of the acquisition to speech and the tense the evidential perspective, and the utterance perspective is the composition of the two; the English nonfuture tenses fix the utterance perspective and carry the downstream constraint, and the past- and present-directed will forms of Winans restrict the evidence to the prospective.

We derive the utterance-perspective columns of the paper's tables by composing cells, show that the nonfuture cells of all three languages require downstream evidence, that no true future can, and that the prospective cells lie beyond Cariani's obviation, and check the paper's felicity judgments against the cells on the frames its scenarios fix, with planned events exempt.

Implementation notes

• The constraints are read temporally, as in the paper's tables; Cumming's own constraint is causal, and cases turning on the difference, as the rewatched film of footnote 9, are not represented.
• Koev distinguishes a null past and a null present tense under -l; Cumming's nonfuture cell is their join, and a frame satisfies it exactly when it satisfies one of Koev's two.
• The printed table (22) gives will have the utterance perspective T > S; the text and the example of the Fed's meeting require a past event, recorded here.

References

• S. Cumming, Tense and evidence (2026)
• D. Ninan, Assertion, evidence, and the future (2022)
• F. Cariani, The modal future (2021)
• F. Cariani, Future-past asymmetries, evidential grounding, and projection (2022)
• J. Lee, Evidentiality and its interaction with tense: evidence from Korean (2011)
• J. Lee, Temporal constraints on the meaning of evidentiality (2013)
• T. Koev, Evidentiality, learning events and spatiotemporal distance (2017)
• L. Winans, Inferences of will (2016)
• S. Cumming, L. Winans, Counterfactuals and abduction (2021)
• L. Matthewson, Evidence type, evidence location, evidence strength (2020)

Paradigm cells

structure Cumming2026.Cell : Type

A cell of a tense-evidential paradigm constrains the evidential perspective, the relation of the event to the acquisition of the evidence, the relation of the acquisition to speech, and the utterance perspective, the relation of the event to speech, each by a cell of the tense partition, ⊤ where the paradigm leaves the relation open.

• ep : Finset Ordering

  The constraint on the evidential perspective.

• acquisition : Finset Ordering

  The constraint on the relation of the acquisition of the evidence to speech.

• up : Finset Ordering

  The constraint on the utterance perspective.

def Cumming2026.instDecidableEqCell.decEq (x✝ x✝¹ : Cell) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Cumming2026.instDecidableEqCell : DecidableEq Cell

Equations

• Cumming2026.instDecidableEqCell = Cumming2026.instDecidableEqCell.decEq

def Cumming2026.Cell.Holds {T : Type u_1} [LinearOrder T] (c : Cell) (f : Tense.EvidentialFrame T) : Prop

A cell holds at a frame when its three constraints do.

Equations

• c.Holds f = (compare f.eventTime f.acquisitionTime ∈ c.ep ∧ compare f.acquisitionTime f.speechTime ∈ c.acquisition ∧ compare f.eventTime f.speechTime ∈ c.up)

@[instance_reducible]

instance Cumming2026.Cell.instDecidableHolds {T : Type u_1} [LinearOrder T] (c : Cell) (f : Tense.EvidentialFrame T) : Decidable (c.Holds f)

Equations

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

def Cumming2026.Cell.derivedUp (c : Cell) : Finset Ordering

The utterance perspective that a cell's evidential perspective and its relation of the acquisition to speech compose to (§3).

Equations

• c.derivedUp = Tense.comp c.ep c.acquisition

theorem Cumming2026.Cell.compare_mem_derivedUp {T : Type u_1} [LinearOrder T] {c : Cell} {f : Tense.EvidentialFrame T} (h : c.Holds f) : compare f.eventTime f.speechTime ∈ c.derivedUp

At a frame where a cell holds, the event stands to speech in the composition of the cell's evidential perspective with its relation of the acquisition to speech.

theorem Cumming2026.Cell.downstream_of_holds {T : Type u_1} [LinearOrder T] {c : Cell} (hc : c.ep ⊆ (Semantics.Denotes.denote Tense.future)ᶜ) {f : Tense.EvidentialFrame T} (h : c.Holds f) : f.Downstream

A cell whose evidential perspective lies within the nonfuture requires downstream evidence, the constraint (10).

noncomputable def Cumming2026.Cell.meaning {T : Type u_1} [LinearOrder T] {W : Type u_2} (c : Cell) (f : Tense.EvidentialFrame T) (φ : W → Prop) : W → SignType

The meaning of a cell at a frame presupposes the constraints and asserts the content, so the constraint is not part of what is asserted.

Equations

• c.meaning f φ = {_w : W | c.Holds f}.indicator fun (w : W) => SignType.ofProp (φ w)

def Cumming2026.evidential (acquisition tense : Finset Ordering) : Cell

An evidential fixes the relation of the acquisition of the evidence to speech and turns the tense it combines with into a constraint on the evidential perspective (§3).

Equations

• Cumming2026.evidential acquisition tense = { ep := tense, acquisition := acquisition }

theorem Cumming2026.holds_evidential_sup {T : Type u_1} [LinearOrder T] {a t t' : Finset Ordering} {f : Tense.EvidentialFrame T} : (evidential a (t ⊔ t')).Holds f ↔ (evidential a t).Holds f ∨ (evidential a t').Holds f

A tense that is the join of two tenses holds under an evidential exactly when one of them does.

The paradigms (§2 to §4)

def Cumming2026.te : Finset Ordering → Cell

Korean -te, sensory evidence acquired in the past of speech ((13), (18)).

Equations

• Cumming2026.te = Cumming2026.evidential (Semantics.Denotes.denote Tense.past)

def Cumming2026.ney : Finset Ordering → Cell

Korean -ney, sensory evidence acquired at speech ((14), (19)).

Equations

• Cumming2026.ney = Cumming2026.evidential (Semantics.Denotes.denote Tense.present)

def Cumming2026.l : Finset Ordering → Cell

Bulgarian -l, indirect evidence acquired by the time of speech ((15) to (17)).

Equations

• Cumming2026.l = Cumming2026.evidential (Semantics.Denotes.denote Tense.future)ᶜ

def Cumming2026.simplePast : Cell

The English simple past requires downstream evidence for a past event ((20)).

Equations

• Cumming2026.simplePast = { ep := (Semantics.Denotes.denote Tense.future)ᶜ, up := Semantics.Denotes.denote Tense.past }

def Cumming2026.presentProgressive : Cell

The English present progressive requires downstream evidence for a present event ((20)).

Equations

• Cumming2026.presentProgressive = { ep := (Semantics.Denotes.denote Tense.future)ᶜ, up := Semantics.Denotes.denote Tense.present }

def Cumming2026.will : Cell

The English future will places no evidential constraint on a future event ((20)).

Equations

• Cumming2026.will = { up := Semantics.Denotes.denote Tense.future }

def Cumming2026.willHave : Cell

The past-directed will have requires prospective evidence for a past event ((22)).

Equations

• Cumming2026.willHave = { ep := Semantics.Denotes.denote Tense.future, up := Semantics.Denotes.denote Tense.past }

def Cumming2026.willNow : Cell

The present-directed will now requires prospective evidence for a present event ((22)).

Equations

• Cumming2026.willNow = { ep := Semantics.Denotes.denote Tense.future, up := Semantics.Denotes.denote Tense.present }

The utterance perspective derived (§3)

Under -te and -ney the tense fixes the evidential perspective and the evidential the relation of the acquisition to speech, and the utterance-perspective columns of tables (18) and (19) are compositions; under -l the same holds of table (17), whose nonfuture cell is the join of Koev's null past and null present.

theorem Cumming2026.te_past_derivedUp : (te (Semantics.Denotes.denote Tense.past)).derivedUp = Semantics.Denotes.denote Tense.past

theorem Cumming2026.te_present_derivedUp : (te (Semantics.Denotes.denote Tense.present)).derivedUp = Semantics.Denotes.denote Tense.past

theorem Cumming2026.te_future_derivedUp : (te (Semantics.Denotes.denote Tense.future)).derivedUp = ⊤

Prospective evidence acquired in the past of speech leaves the utterance perspective open, so the future under -te is compatible with a past, present or future event.

theorem Cumming2026.ney_past_derivedUp : (ney (Semantics.Denotes.denote Tense.past)).derivedUp = Semantics.Denotes.denote Tense.past

theorem Cumming2026.ney_present_derivedUp : (ney (Semantics.Denotes.denote Tense.present)).derivedUp = Semantics.Denotes.denote Tense.present

theorem Cumming2026.ney_future_derivedUp : (ney (Semantics.Denotes.denote Tense.future)).derivedUp = Semantics.Denotes.denote Tense.future

Present evidence that is prospective is for a future event, since S = A and A < T give S < T.

theorem Cumming2026.l_nonfuture_derivedUp : (l (Semantics.Denotes.denote Tense.future)ᶜ).derivedUp = (Semantics.Denotes.denote Tense.future)ᶜ

Downstream evidence acquired by the time of speech is for a nonfuture event ((17)).

theorem Cumming2026.l_future_derivedUp : (l (Semantics.Denotes.denote Tense.future)).derivedUp = ⊤

Prospective evidence acquired by the time of speech leaves the utterance perspective open, so the future under -l describes yesterday's forecast rain ((16)).

theorem Cumming2026.holds_l_nonfuture_iff {T : Type u_1} [LinearOrder T] {f : Tense.EvidentialFrame T} : (l (Semantics.Denotes.denote Tense.future)ᶜ).Holds f ↔ (l (Semantics.Denotes.denote Tense.past)).Holds f ∨ (l (Semantics.Denotes.denote Tense.present)).Holds f

Cumming's nonfuture cell under -l holds exactly when Koev's null past or null present does (footnote 7).

Downstream evidence, obviation and the true future (§5, §7)

theorem Cumming2026.nonfuture_ep_le (c : Cell) : c ∈ [simplePast, presentProgressive, te (Semantics.Denotes.denote Tense.past), te (Semantics.Denotes.denote Tense.present), ney (Semantics.Denotes.denote Tense.past), ney (Semantics.Denotes.denote Tense.present), l (Semantics.Denotes.denote Tense.future)ᶜ] → c.ep ⊆ (Semantics.Denotes.denote Tense.future)ᶜ

Across the three languages, the nonfuture tenses restrict the evidence to the non-prospective.

theorem Cumming2026.prospective_beyond_obviation (c : Cell) : c ∈ [te (Semantics.Denotes.denote Tense.future), ney (Semantics.Denotes.denote Tense.future), l (Semantics.Denotes.denote Tense.future), willHave, willNow] → c.ep ≠ (Semantics.Denotes.denote Tense.future)ᶜ ∧ c.ep ≠ ⊤

The prospective cells of Korean, Bulgarian and the English will forms are neither restricted to downstream evidence nor unrestricted, the two options Cariani's obviation provides (§5).

theorem Cumming2026.speechTime_lt_acquisitionTime {T : Type u_1} [LinearOrder T] {f : Tense.EvidentialFrame T} (h : { ep := (Semantics.Denotes.denote Tense.future)ᶜ, up := Semantics.Denotes.denote Tense.future }.Holds f) : f.speechTime < f.acquisitionTime

No true future is restricted to downstream evidence, since at a frame where such a cell held the speaker would speak before acquiring the evidence (§7).

theorem Cumming2026.willHave_meaning_eq_simplePast_meaning {T : Type u_1} [LinearOrder T] {W : Type u_2} {f f' : Tense.EvidentialFrame T} (φ : W → Prop) (h : willHave.Holds f) (h' : simplePast.Holds f') : willHave.meaning f φ = simplePast.meaning f' φ

The past-directed will have and the simple past assert the same proposition and differ in what they presuppose, so will have is no necessity modal ((23)). At frames meeting their respective constraints the two are the same proposition.

The felicity judgments

def Cumming2026.cell? (e : Datum) : Option Cell

The cell a row's form feature names.

Equations

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

def Cumming2026.frame? (e : Datum) : Option (Tense.EvidentialFrame ℤ)

The frame a row's scenario fixes.

Equations

• Cumming2026.frame? e = do let s ← e.nat? "speechTime" let a ← e.nat? "acquisitionTime" let t ← e.nat? "eventTime" pure { speechTime := ↑s, eventTime := ↑t, acquisitionTime := ↑a }

def Cumming2026.Scheduled (e : Datum) : Prop

The row describes a planned or scheduled event (§6).

Equations

• Cumming2026.Scheduled e = (e.feature? "scheduled" = some "true")

@[instance_reducible]

instance Cumming2026.instDecidablePredDatumScheduled : DecidablePred Scheduled

Equations

• Cumming2026.instDecidablePredDatumScheduled x✝ = Cumming2026.instDecidablePredDatumScheduled._aux_1 x✝

theorem Cumming2026.cell?_frame?_isSome (e : Datum) : e ∈ Examples.all → (cell? e).isSome = true ∧ (frame? e).isSome = true

Every example names a cell and a scenario.

theorem Cumming2026.judgment_iff (e : Datum) : e ∈ Examples.all → ∀ c ∈ cell? e, ∀ f ∈ frame? e, e.JudgedFelicitous ↔ Scheduled e ∨ c.Holds f

An assertion is felicitous exactly when its cell holds on the scenario's frame, planned or scheduled events exempt (§6).