Evidential — coarse source and perspective

[willett-1988] [Aik04] [Cum26] [vFG10]

Framework-agnostic evidentiality vocabulary: [willett-1988]'s coarse three-way source taxonomy, the temporal-orientation classification of evidence acquisition, and the typeclasses HasCoarseSource and HasEvidentialPerspective that let downstream types (semantic constraint enums, paradigm rows, modal evidence types) project into the taxonomies uniformly.

In the typologically canonical case, an evidential source — direct observation, report, or inference from results — is causally downstream of the described event: the event causes the perceptual state, the report, or the observable effects. Assumption-based inferentials and predictive evidentials fall outside this pattern; the prospective perspective and the Option codomain of the projection accommodate them.

This module supplies the shared vocabulary consumed by both [Cum26]'s tense evidentiality (T ≤ A = downstream evidence) and [vFG10]'s epistemic evidentiality (direct vs indirect). [Aik04]'s finer six-way parameter carving lives with the evidential lexical API in the sibling Defs/Basic files.

inductive Semantics.Evidential.CoarseSource : Type

Coarse three-way evidential source classification: [willett-1988]'s attested / reported / inferring tripartition. hearsay is the umbrella for Willett's reported category (subsuming hearsay proper and quotative); finer carvings ([Aik04]) live at Semantics/Evidential/.

• 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 Semantics.Evidential.instDecidableEqCoarseSource : DecidableEq CoarseSource

Equations

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

@[implicit_reducible]

instance Semantics.Evidential.instReprCoarseSource : Repr CoarseSource

Equations

• Semantics.Evidential.instReprCoarseSource = { reprPrec := Semantics.Evidential.instReprCoarseSource.repr }

def Semantics.Evidential.instReprCoarseSource.repr : CoarseSource → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Evidential.instInhabitedCoarseSource : Inhabited CoarseSource

Equations

• Semantics.Evidential.instInhabitedCoarseSource = { default := Semantics.Evidential.instInhabitedCoarseSource.default }

def Semantics.Evidential.CoarseSource.IsIndirect (s : CoarseSource) : Prop

A coarse source is indirect iff it is not direct observation. The shared contrast variable of indirect-evidential operators: [Izv97]'s EV and [vFG10]'s must both presuppose an indirect evidence basis.

Equations

• s.IsIndirect = (s ≠ Semantics.Evidential.CoarseSource.direct)

@[implicit_reducible]

instance Semantics.Evidential.instDecidablePredCoarseSourceIsIndirect : DecidablePred CoarseSource.IsIndirect

Equations

• Semantics.Evidential.instDecidablePredCoarseSourceIsIndirect s = Semantics.Evidential.instDecidablePredCoarseSourceIsIndirect._aux_1 s

inductive Semantics.Evidential.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 Semantics.Evidential.instDecidableEqEvidentialPerspective : DecidableEq EvidentialPerspective

Equations

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

def Semantics.Evidential.instReprEvidentialPerspective.repr : EvidentialPerspective → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Evidential.instReprEvidentialPerspective : Repr EvidentialPerspective

Equations

• Semantics.Evidential.instReprEvidentialPerspective = { reprPrec := Semantics.Evidential.instReprEvidentialPerspective.repr }

@[implicit_reducible]

instance Semantics.Evidential.instInhabitedEvidentialPerspective : Inhabited EvidentialPerspective

Equations

• Semantics.Evidential.instInhabitedEvidentialPerspective = { default := Semantics.Evidential.instInhabitedEvidentialPerspective.default }

class Semantics.Evidential.HasEvidentialPerspective (α : Type u_1) : Type u_1

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 Semantics.Evidential.IsNonfuture {α : Type u_1} [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 Semantics.Evidential.instDecidablePredIsNonfuture {α : Type u_1} [HasEvidentialPerspective α] : DecidablePred IsNonfuture

Equations

• Semantics.Evidential.instDecidablePredIsNonfuture x✝ = Semantics.Evidential.instDecidablePredIsNonfuture._aux_1 x✝

class Semantics.Evidential.HasCoarseSource (α : Type u_1) : Type u_1

Types that project to a coarse evidential source. The stronger entry point into the vocabulary: declaring a source also yields a perspective, via the canonical source mapping (the low-priority instance below). Types whose evidence classification cross-cuts the source taxonomy project partially (none off the shared part).

• toCoarseSource : α → Option CoarseSource

  The coarse evidential source of a, when defined.

Canonical instances

def Semantics.Evidential.CoarseSource.toEvidentialPerspective : CoarseSource → Option EvidentialPerspective

The coarse 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

• Semantics.Evidential.CoarseSource.direct.toEvidentialPerspective = some Semantics.Evidential.EvidentialPerspective.contemporaneous
• Semantics.Evidential.CoarseSource.hearsay.toEvidentialPerspective = some Semantics.Evidential.EvidentialPerspective.retrospective
• Semantics.Evidential.CoarseSource.inference.toEvidentialPerspective = some Semantics.Evidential.EvidentialPerspective.retrospective

@[implicit_reducible]

instance Semantics.Evidential.instHasCoarseSourceCoarseSource : HasCoarseSource CoarseSource

Equations

• Semantics.Evidential.instHasCoarseSourceCoarseSource = { toCoarseSource := some }

@[implicit_reducible, instance 100]

instance Semantics.Evidential.instHasEvidentialPerspectiveOfHasCoarseSource {α : Type u_1} [HasCoarseSource α] : HasEvidentialPerspective α

Source-declaring types inherit their perspective through the canonical mapping. Low priority: a type with its own perspective classification keeps it.

Equations

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

@[implicit_reducible]

instance Semantics.Evidential.instHasEvidentialPerspectiveEvidentialPerspective : HasEvidentialPerspective EvidentialPerspective

The perspective type projects to itself.

Equations

• Semantics.Evidential.instHasEvidentialPerspectiveEvidentialPerspective = { toEvidentialPerspective := some }