Evidential Source Classification

@cite{aikhenvald-2004} @cite{cumming-2026} @cite{von-fintel-gillies-2010}

Canonical three-way classification of evidential source and its causal-temporal correlates.

All evidential sources — direct observation, hearsay, and inference — share the property that the speaker's evidence is causally downstream of the described event: the event causes the perceptual state, the report, or the observable effects from which the inference is drawn.

This module provides the shared vocabulary that bridges:

• @cite{cumming-2026}'s tense evidentiality (T ≤ A = downstream evidence)
• @cite{von-fintel-gillies-2010} epistemic evidentiality (direct vs indirect)

inductive Core.Evidence.EvidentialSource : Type

Canonical three-way evidential source classification.

• direct : EvidentialSource

  Direct sensory observation (seeing, hearing the event).

• hearsay : EvidentialSource

  Hearsay / reported evidence (told about the event).

• inference : EvidentialSource

  Inference from observable effects (reasoning about the event).

instance Core.Evidence.instDecidableEqEvidentialSource : DecidableEq EvidentialSource

Equations

• Core.Evidence.instDecidableEqEvidentialSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Evidence.instReprEvidentialSource : Repr EvidentialSource

Equations

• Core.Evidence.instReprEvidentialSource = { reprPrec := Core.Evidence.instReprEvidentialSource.repr }

def Core.Evidence.instReprEvidentialSource.repr : EvidentialSource → Nat → Std.Format

Equations

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

def Core.Evidence.instBEqEvidentialSource.beq : EvidentialSource → EvidentialSource → Bool

Equations

• Core.Evidence.instBEqEvidentialSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Evidence.instBEqEvidentialSource : BEq EvidentialSource

Equations

• Core.Evidence.instBEqEvidentialSource = { beq := Core.Evidence.instBEqEvidentialSource.beq }

instance Core.Evidence.instInhabitedEvidentialSource : Inhabited EvidentialSource

Equations

• Core.Evidence.instInhabitedEvidentialSource = { default := Core.Evidence.instInhabitedEvidentialSource.default }

def Core.Evidence.instInhabitedEvidentialSource.default : EvidentialSource

Equations

• Core.Evidence.instInhabitedEvidentialSource.default = Core.Evidence.EvidentialSource.direct

inductive Core.Evidence.EvidentialPerspective : Type

Evidential perspective: the temporal relation of T to A. @cite{cumming-2026}'s three evidential orientations. Framework-agnostic: just names the three temporal relations between event and evidence acquisition.

• retrospective : EvidentialPerspective

  T ≤ A: evidence acquired after (or at) the event. Speaker observed consequences or received reports.

• contemporaneous : EvidentialPerspective

  T = A: evidence acquired contemporaneously with the event.

• prospective : EvidentialPerspective

  A < T: evidence acquired before the event. Speaker has predictive grounds (plans, schedules, dispositions).

instance Core.Evidence.instDecidableEqEvidentialPerspective : DecidableEq EvidentialPerspective

Equations

• Core.Evidence.instDecidableEqEvidentialPerspective x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Evidence.instReprEvidentialPerspective : Repr EvidentialPerspective

Equations

• Core.Evidence.instReprEvidentialPerspective = { reprPrec := Core.Evidence.instReprEvidentialPerspective.repr }

def Core.Evidence.instReprEvidentialPerspective.repr : EvidentialPerspective → Nat → Std.Format

Equations

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

def Core.Evidence.instBEqEvidentialPerspective.beq : EvidentialPerspective → EvidentialPerspective → Bool

Equations

• Core.Evidence.instBEqEvidentialPerspective.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Evidence.instBEqEvidentialPerspective : BEq EvidentialPerspective

Equations

• Core.Evidence.instBEqEvidentialPerspective = { beq := Core.Evidence.instBEqEvidentialPerspective.beq }

def Core.Evidence.EvidentialPerspective.isNonfuture : EvidentialPerspective → Bool

Is this evidential perspective nonfuture? Retrospective and contemporaneous perspectives involve evidence that is downstream of the event (T ≤ A); prospective does not.

Equations

• Core.Evidence.EvidentialPerspective.retrospective.isNonfuture = true
• Core.Evidence.EvidentialPerspective.contemporaneous.isNonfuture = true
• Core.Evidence.EvidentialPerspective.prospective.isNonfuture = false

def Core.Evidence.EvidentialSource.toEvidentialPerspective : EvidentialSource → EvidentialPerspective

Every evidential source maps to an evidential perspective. Direct observation is contemporaneous (A = T), hearsay and inference are retrospective (A ≥ T) — in all cases, the event causally precedes or coincides with evidence acquisition.

Equations

• Core.Evidence.EvidentialSource.direct.toEvidentialPerspective = Core.Evidence.EvidentialPerspective.contemporaneous
• Core.Evidence.EvidentialSource.hearsay.toEvidentialPerspective = Core.Evidence.EvidentialPerspective.retrospective
• Core.Evidence.EvidentialSource.inference.toEvidentialPerspective = Core.Evidence.EvidentialPerspective.retrospective

inductive Core.Evidence.MirativityValue : Type

Mirativity: whether the propositional content is expected or surprising to the speaker (@cite{delancey-1997}, @cite{aikhenvald-2004} Ch 6).

• expected : MirativityValue
• unexpected : MirativityValue
• neutral : MirativityValue

instance Core.Evidence.instDecidableEqMirativityValue : DecidableEq MirativityValue

Equations

• Core.Evidence.instDecidableEqMirativityValue x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Core.Evidence.instReprMirativityValue : Repr MirativityValue

Equations

• Core.Evidence.instReprMirativityValue = { reprPrec := Core.Evidence.instReprMirativityValue.repr }

def Core.Evidence.instReprMirativityValue.repr : MirativityValue → Nat → Std.Format

Equations

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

def Core.Evidence.instBEqMirativityValue.beq : MirativityValue → MirativityValue → Bool

Equations

• Core.Evidence.instBEqMirativityValue.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Evidence.instBEqMirativityValue : BEq MirativityValue

Equations

• Core.Evidence.instBEqMirativityValue = { beq := Core.Evidence.instBEqMirativityValue.beq }

def Core.Evidence.MirativityValue.isMirative : MirativityValue → Bool

Does this mirativity value mark surprise/new information?

Equations

• Core.Evidence.MirativityValue.unexpected.isMirative = true
• x✝.isMirative = false

def Core.Evidence.EvidentialSource.isIndirect : EvidentialSource → Bool

Is this evidence source indirect? Hearsay and inference are indirect; direct observation is not. This is @cite{izvorski-1997}'s binary partition of Aikhenvald's three-way classification.

Equations

• Core.Evidence.EvidentialSource.direct.isIndirect = false
• Core.Evidence.EvidentialSource.hearsay.isIndirect = true
• Core.Evidence.EvidentialSource.inference.isIndirect = true