Evidentiality

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

Framework-agnostic evidentiality vocabulary: the canonical Aikhenvald three-way source taxonomy, the temporal-orientation classification of evidence acquisition, and a typeclass HasEvidentialPerspective that lets downstream types (semantic constraint enums, paradigm rows, modal evidence types) project into the perspective taxonomy uniformly.

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 supplies the shared vocabulary that bridges @cite{cumming-2026}'s tense evidentiality (T ≤ A = downstream evidence) and @cite{von-fintel-gillies-2010} epistemic evidentiality (direct vs indirect).

inductive Features.Evidentiality.EvidentialSource : Type

Canonical three-way evidential source classification (@cite{aikhenvald-2004}).

• 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).

@[implicit_reducible]

instance Features.Evidentiality.instDecidableEqEvidentialSource : DecidableEq EvidentialSource

Equations

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

def Features.Evidentiality.instReprEvidentialSource.repr : EvidentialSource → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Evidentiality.instReprEvidentialSource : Repr EvidentialSource

Equations

• Features.Evidentiality.instReprEvidentialSource = { reprPrec := Features.Evidentiality.instReprEvidentialSource.repr }

def Features.Evidentiality.instInhabitedEvidentialSource.default : EvidentialSource

Equations

• Features.Evidentiality.instInhabitedEvidentialSource.default = Features.Evidentiality.EvidentialSource.direct

@[implicit_reducible]

instance Features.Evidentiality.instInhabitedEvidentialSource : Inhabited EvidentialSource

Equations

• Features.Evidentiality.instInhabitedEvidentialSource = { default := Features.Evidentiality.instInhabitedEvidentialSource.default }

inductive Features.Evidentiality.EvidentialPerspective : Type

Evidential perspective: the temporal relation of evidence acquisition to the described event. @cite{cumming-2026}'s three evidential orientations, named in framework-agnostic terms.

• 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).

@[implicit_reducible]

instance Features.Evidentiality.instDecidableEqEvidentialPerspective : DecidableEq EvidentialPerspective

Equations

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

def Features.Evidentiality.instReprEvidentialPerspective.repr : EvidentialPerspective → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Evidentiality.instReprEvidentialPerspective : Repr EvidentialPerspective

Equations

• Features.Evidentiality.instReprEvidentialPerspective = { reprPrec := Features.Evidentiality.instReprEvidentialPerspective.repr }

@[implicit_reducible]

instance Features.Evidentiality.instInhabitedEvidentialPerspective : Inhabited EvidentialPerspective

Equations

• Features.Evidentiality.instInhabitedEvidentialPerspective = { default := Features.Evidentiality.instInhabitedEvidentialPerspective.default }

def Features.Evidentiality.instInhabitedEvidentialPerspective.default : EvidentialPerspective

Equations

• Features.Evidentiality.instInhabitedEvidentialPerspective.default = Features.Evidentiality.EvidentialPerspective.retrospective

class Features.Evidentiality.HasEvidentialPerspective (α : Type) : Type

Types that project to an evidential perspective.

The Option codomain accommodates types like tense-paradigm constraints where some values (e.g. an unconstrained future) have no canonical perspective. Types with a total projection (the source taxonomy itself, or the perspective type) wrap the result in some.

• toEvidentialPerspective : α → Option EvidentialPerspective

  The evidential perspective of a, when defined.

def Features.Evidentiality.IsNonfuture {α : Type} [HasEvidentialPerspective α] (a : α) : Prop

A value is nonfuture iff it projects to a retrospective or contemporaneous perspective — i.e., evidence is downstream of the event (T ≤ A). Prospective and "no perspective" both fail.

Defined uniformly over HasEvidentialPerspective so that downstream types (constraint enums, paradigm rows, modal evidence types) inherit one decidable predicate instead of hand-rolling parallel definitions.

Equations

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

@[implicit_reducible]

instance Features.Evidentiality.instDecidablePredIsNonfuture {α : Type} [HasEvidentialPerspective α] : DecidablePred IsNonfuture

Equations

• Features.Evidentiality.instDecidablePredIsNonfuture x✝ = Features.Evidentiality.instDecidablePredIsNonfuture._aux_1 x✝

def Features.Evidentiality.EvidentialSource.toEvidentialPerspective : EvidentialSource → Option EvidentialPerspective

The Aikhenvald source taxonomy projects to perspective by the canonical typological mapping: direct observation is contemporaneous (A = T), while hearsay and inference are retrospective (A ≥ T). The event causally precedes or coincides with evidence acquisition in all three cases.

Note: this encodes a typological generalization, not a definitional truth. Live quotatives and predictive inference can violate the canonical mapping; per-construction classifications should override.

Equations

• Features.Evidentiality.EvidentialSource.direct.toEvidentialPerspective = some Features.Evidentiality.EvidentialPerspective.contemporaneous
• Features.Evidentiality.EvidentialSource.hearsay.toEvidentialPerspective = some Features.Evidentiality.EvidentialPerspective.retrospective
• Features.Evidentiality.EvidentialSource.inference.toEvidentialPerspective = some Features.Evidentiality.EvidentialPerspective.retrospective

@[implicit_reducible]

instance Features.Evidentiality.instHasEvidentialPerspectiveEvidentialSource : HasEvidentialPerspective EvidentialSource

Equations

• Features.Evidentiality.instHasEvidentialPerspectiveEvidentialSource = { toEvidentialPerspective := Features.Evidentiality.EvidentialSource.toEvidentialPerspective }

@[implicit_reducible]

instance Features.Evidentiality.instHasEvidentialPerspectiveEvidentialPerspective : HasEvidentialPerspective EvidentialPerspective

The perspective type projects to itself.

Equations

• Features.Evidentiality.instHasEvidentialPerspectiveEvidentialPerspective = { toEvidentialPerspective := some }

def Features.Evidentiality.EvidentialPerspective.IsNonfuture (p : EvidentialPerspective) : Prop

Dot-notation alias for Features.Evidentiality.IsNonfuture on perspectives.

Equations

• p.IsNonfuture = Features.Evidentiality.IsNonfuture p

@[implicit_reducible]

instance Features.Evidentiality.instDecidablePredEvidentialPerspectiveIsNonfuture : DecidablePred EvidentialPerspective.IsNonfuture

Equations

• Features.Evidentiality.instDecidablePredEvidentialPerspectiveIsNonfuture x✝ = Features.Evidentiality.instDecidablePredEvidentialPerspectiveIsNonfuture._aux_1 x✝

@[simp]

theorem Features.Evidentiality.EvidentialSource.toEvidentialPerspective_direct : direct.toEvidentialPerspective = some EvidentialPerspective.contemporaneous

@[simp]

theorem Features.Evidentiality.EvidentialSource.toEvidentialPerspective_hearsay : hearsay.toEvidentialPerspective = some EvidentialPerspective.retrospective

@[simp]

theorem Features.Evidentiality.EvidentialSource.toEvidentialPerspective_inference : inference.toEvidentialPerspective = some EvidentialPerspective.retrospective