Tense and evidence

An evidential frame locates an assertion by three times: the time of speech, the time of the event, and the time at which the speaker acquires the evidence for the assertion, the learning time of Koev's account of the Bulgarian evidential and the acquisition time of Cumming's account of tense-evidential paradigms. Evidence is downstream of the event when the event precedes or coincides with its acquisition, so that on linear time the event stands to the acquisition in a nonfuture position.

Main definitions

• Tense.EvidentialFrame: the speech time, the event time and the acquisition time of an assertion.
• Tense.EvidentialFrame.Downstream: the event is no later than the acquisition of the evidence.

Implementation notes

• Downstream evidence is read temporally, the event no later than the acquisition, as in Koev's and Lee's accounts and Cumming's tables; Cumming's own constraint is causal.

References

• [Cum26]
• [Koe17]
• [Hui25]

structure Tense.EvidentialFrame (T : Type u_1) : Type u_1

An evidential frame consists of the time of speech, the time of the event, and the time at which the speaker acquires the evidence for the assertion.

• speechTime : T

  The time at which the utterance occurs.

• eventTime : T

  The time at which the event occurs.

• acquisitionTime : T

  The time at which the speaker acquires the evidence for the assertion.

def Tense.EvidentialFrame.Downstream {T : Type u_1} [LE T] (f : EvidentialFrame T) : Prop

The evidence is downstream of the event when the event precedes or coincides with its acquisition.

Equations

• f.Downstream = (f.eventTime ≤ f.acquisitionTime)

@[instance_reducible]

instance Tense.EvidentialFrame.instDecidableDownstreamOfDecidableLE {T : Type u_1} [LE T] [DecidableLE T] (f : EvidentialFrame T) : Decidable f.Downstream

Equations

• f.instDecidableDownstreamOfDecidableLE = Tense.EvidentialFrame.instDecidableDownstreamOfDecidableLE._aux_1 f

theorem Tense.EvidentialFrame.downstream_iff {T : Type u_1} [LinearOrder T] (f : EvidentialFrame T) : f.Downstream ↔ compare f.eventTime f.acquisitionTime ∈ (Semantics.Denotes.denote future)ᶜ