Evidentiality

[Aik04] [Cum26] [vFG10]

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 [Cum26]'s tense evidentiality (T ≤ A = downstream evidence) and [vFG10] epistemic evidentiality (direct vs indirect).

inductive Features.Evidentiality.CoarseSource : Type

Canonical three-way evidential source classification ([Aik04]).

• direct : CoarseSource

  Direct sensory observation (seeing, hearing the event).

• hearsay : CoarseSource

  Hearsay / reported evidence (told about the event).

• inference : CoarseSource

  Inference from observable effects (reasoning about the event).

@[implicit_reducible]

instance Features.Evidentiality.instDecidableEqCoarseSource : DecidableEq CoarseSource

Equations

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

@[implicit_reducible]

instance Features.Evidentiality.instReprCoarseSource : Repr CoarseSource

Equations

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

def Features.Evidentiality.instReprCoarseSource.repr : CoarseSource → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Evidentiality.instInhabitedCoarseSource : Inhabited CoarseSource

Equations

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

inductive Features.Evidentiality.EvidentialPerspective : Type

Evidential perspective: the temporal relation of evidence acquisition to the described event. [Cum26]'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 ⋯

@[implicit_reducible]

instance Features.Evidentiality.instReprEvidentialPerspective : Repr EvidentialPerspective

Equations

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

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.instInhabitedEvidentialPerspective : Inhabited EvidentialPerspective

Equations

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

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.CoarseSource.toEvidentialPerspective : CoarseSource → 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.CoarseSource.direct.toEvidentialPerspective = some Features.Evidentiality.EvidentialPerspective.contemporaneous
• Features.Evidentiality.CoarseSource.hearsay.toEvidentialPerspective = some Features.Evidentiality.EvidentialPerspective.retrospective
• Features.Evidentiality.CoarseSource.inference.toEvidentialPerspective = some Features.Evidentiality.EvidentialPerspective.retrospective

@[implicit_reducible]

instance Features.Evidentiality.instHasEvidentialPerspectiveCoarseSource : HasEvidentialPerspective CoarseSource

Equations

• Features.Evidentiality.instHasEvidentialPerspectiveCoarseSource = { toEvidentialPerspective := Features.Evidentiality.CoarseSource.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.CoarseSource.toEvidentialPerspective_direct : direct.toEvidentialPerspective = some EvidentialPerspective.contemporaneous

@[simp]

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

@[simp]

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

inductive Features.Evidentiality.DirectSource : Type

Sensory channel of a direct (firsthand) evidential. The visual vs non-visual contrast is grammaticalized in many languages (Tuyuca, Tariana, Kashaya); finer distinctions (auditory vs other non-visual sensory) are grammaticalized in some (Kashaya). Languages that don't grammaticalize the contrast use .unspecified.

• unspecified : DirectSource
• visual : DirectSource
• auditory : DirectSource
• nonvisualSensory : DirectSource
• olfactory : DirectSource

@[implicit_reducible]

instance Features.Evidentiality.instDecidableEqDirectSource : DecidableEq DirectSource

Equations

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

def Features.Evidentiality.instReprDirectSource.repr : DirectSource → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Evidentiality.instReprDirectSource : Repr DirectSource

Equations

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

@[implicit_reducible]

instance Features.Evidentiality.instInhabitedDirectSource : Inhabited DirectSource

Equations

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

inductive Features.Evidentiality.ReportativeSource : Type

Source-identity of a reportative evidential. Aikhenvald 2004 distinguishes hearsay (original speaker not identified) from quotative (specifically named source).

• unspecified : ReportativeSource
• unidentified : ReportativeSource
• identified : ReportativeSource

@[implicit_reducible]

instance Features.Evidentiality.instDecidableEqReportativeSource : DecidableEq ReportativeSource

Equations

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

def Features.Evidentiality.instReprReportativeSource.repr : ReportativeSource → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Evidentiality.instReprReportativeSource : Repr ReportativeSource

Equations

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

@[implicit_reducible]

instance Features.Evidentiality.instInhabitedReportativeSource : Inhabited ReportativeSource

Equations

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

inductive Features.Evidentiality.InferentialBasis : Type

Basis of an inferential evidential. Aikhenvald 2004 distinguishes inference fromResult (observable consequences) from fromAssumption (general knowledge / reasoning).

• unspecified : InferentialBasis
• fromResult : InferentialBasis
• fromAssumption : InferentialBasis

@[implicit_reducible]

instance Features.Evidentiality.instDecidableEqInferentialBasis : DecidableEq InferentialBasis

Equations

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

def Features.Evidentiality.instReprInferentialBasis.repr : InferentialBasis → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Features.Evidentiality.instReprInferentialBasis : Repr InferentialBasis

Equations

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

@[implicit_reducible]

instance Features.Evidentiality.instInhabitedInferentialBasis : Inhabited InferentialBasis

Equations

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