Evidential — lexical structure for evidential markers

[Aik04] [dH13b] [Mur17]

The evidential as a lexical object, following the Determiner-API pattern (Semantics/Definiteness/Determiner.lean). The base Evidential carries only what is universal to all evidential markers — a surface form; each specialization (DirectEvidential, ReportativeEvidential, InferentialEvidential) adds its own structure: an Exponent (realization strategy) plus a fine-grained source value ([Aik04]'s parameter carving).

A language's evidential inventory is a List Evidential.Entry (heterogeneous across the three kinds) declared in its Fragment. Typological classifications — WALS Ch 77 system-type, Ch 78 coding strategy, [Aik04] paradigm system-type — are derived from the inventory, not stipulated: a language's WALS cell is a theorem about its declared evidentials.

Main declarations

• Evidential — the base lexical-item record (just form).
• DirectEvidential, ReportativeEvidential, InferentialEvidential — the three Aikhenvald-coarse specializations.
• Evidential.Exponent — realization-strategy enum (analysis-neutral).
• DirectSource, ReportativeSource, InferentialBasis — the [Aik04] fine-grained source taxonomies the specializations carry.
• Evidential.Entry — an evidential occurrence in a language's inventory.

Implementation notes

• The semantic side (Murray-style not-at-issue contribution, Faller-style illocutionary modification, Korotkova-style modal force, Cumming-style temporal anchoring) is deferred to Studies/{Author}{Year}.lean files which provide opt-in typeclass instances on Entry. This file is the framework-agnostic lexical and typological-derivation substrate only.
• Mirrors the Semantics/Definiteness/Determiner.lean pattern: structure + Exponent realization enum + Entry heterogeneous sum + typological derivations as theorems about the declared inventory.

Fine-grained source taxonomies ([Aik04])

inductive Semantics.Evidential.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

@[instance_reducible]

instance Semantics.Evidential.instDecidableEqDirectSource : DecidableEq DirectSource

Equations

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

def Semantics.Evidential.instReprDirectSource.repr : DirectSource → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Semantics.Evidential.instReprDirectSource : Repr DirectSource

Equations

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

@[instance_reducible]

instance Semantics.Evidential.instInhabitedDirectSource : Inhabited DirectSource

Equations

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

inductive Semantics.Evidential.ReportativeSource : Type

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

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

@[instance_reducible]

instance Semantics.Evidential.instDecidableEqReportativeSource : DecidableEq ReportativeSource

Equations

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

@[instance_reducible]

instance Semantics.Evidential.instReprReportativeSource : Repr ReportativeSource

Equations

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

def Semantics.Evidential.instReprReportativeSource.repr : ReportativeSource → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Semantics.Evidential.instInhabitedReportativeSource : Inhabited ReportativeSource

Equations

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

inductive Semantics.Evidential.InferentialBasis : Type

Basis of an inferential evidential. [Aik04] distinguishes inference fromResult (observable consequences) from fromAssumption (general knowledge / reasoning).

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

@[instance_reducible]

instance Semantics.Evidential.instDecidableEqInferentialBasis : DecidableEq InferentialBasis

Equations

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

@[instance_reducible]

instance Semantics.Evidential.instReprInferentialBasis : Repr InferentialBasis

Equations

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

def Semantics.Evidential.instReprInferentialBasis.repr : InferentialBasis → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Semantics.Evidential.instInhabitedInferentialBasis : Inhabited InferentialBasis

Equations

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

inductive Semantics.Evidential.Exponent : Type

How an evidential is morphosyntactically realized. Analysis-neutral — distinguishes Bulgarian-style TAM-fusion from Cuzco-Quechua-style second-position clitic from Cheyenne-style clausal particle without committing to a syntactic analysis.

• verbalAffix : Exponent

  A verbal affix or bound suffix (Kashaya -yá, Turkish -mIş).

• tamFusion : Exponent

  Fused into the TAM paradigm (Bulgarian indirect in the perfect).

• clitic2P : Exponent

  A second-position (Wackernagel) clitic (Cuzco Quechua -si/-chá).

• clauseParticle : Exponent

  A clausal particle, typically clause-final (Cheyenne =sėstse, Japanese soo da).

• parenthetical : Exponent

  A parenthetical / matrix-frame construction (English "I hear").

• lexicalFrame : Exponent

  A grammaticalized lexical frame (Korean -tay matrix quotative).

• toneAblaut : Exponent

  Tonal or ablaut realization (some Akha and Tibeto-Burman cases).

@[instance_reducible]

instance Semantics.Evidential.instDecidableEqExponent : DecidableEq Exponent

Equations

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

@[instance_reducible]

instance Semantics.Evidential.instReprExponent : Repr Exponent

Equations

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

def Semantics.Evidential.instReprExponent.repr : Exponent → Nat → Std.Format

Equations

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

structure Evidential : Type

The base evidential lexical item: only what is universal — a surface form. Specializations (DirectEvidential, ReportativeEvidential, InferentialEvidential) extends this.

• form : String

  Surface form (a representative morpheme or construction label).

@[instance_reducible]

instance instDecidableEqEvidential : DecidableEq Evidential

Equations

• instDecidableEqEvidential = instDecidableEqEvidential.decEq

def instDecidableEqEvidential.decEq (x✝ x✝¹ : Evidential) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqEvidential.decEq { form := a } { form := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance instReprEvidential : Repr Evidential

Equations

• instReprEvidential = { reprPrec := instReprEvidential.repr }

def instReprEvidential.repr : Evidential → Nat → Std.Format

Equations

• instReprEvidential.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "form" ++ Std.Format.text " := " ++ (Std.Format.nest 8 (repr x✝.form)).group) " }"

structure DirectEvidentialextends Evidential : Type

A direct (firsthand) evidential: signals that the speaker has direct sensory evidence for the prejacent. The source field records the sensory channel for languages that grammaticalize it (visual vs non-visual sensory, etc.).

• form : String
• exponent : Semantics.Evidential.Exponent
• source : Semantics.Evidential.DirectSource

  Aikhenvald-fine sensory channel (visual / auditory / …). Defaults to .unspecified for languages that don't grammaticalize the contrast.

def instDecidableEqDirectEvidential.decEq (x✝ x✝¹ : DirectEvidential) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance instDecidableEqDirectEvidential : DecidableEq DirectEvidential

Equations

• instDecidableEqDirectEvidential = instDecidableEqDirectEvidential.decEq

def instReprDirectEvidential.repr : DirectEvidential → Nat → Std.Format

Equations

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

@[instance_reducible]

instance instReprDirectEvidential : Repr DirectEvidential

Equations

• instReprDirectEvidential = { reprPrec := instReprDirectEvidential.repr }

structure ReportativeEvidentialextends Evidential : Type

A reportative (hearsay / quotative) evidential: signals that the speaker learned the prejacent from another speaker. sourceIdentity records whether the original speaker is named (identified — quotative) or not (unidentified — hearsay).

• form : String
• exponent : Semantics.Evidential.Exponent
• sourceIdentity : Semantics.Evidential.ReportativeSource

  Whether the original speaker is identified.

def instDecidableEqReportativeEvidential.decEq (x✝ x✝¹ : ReportativeEvidential) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance instDecidableEqReportativeEvidential : DecidableEq ReportativeEvidential

Equations

• instDecidableEqReportativeEvidential = instDecidableEqReportativeEvidential.decEq

@[instance_reducible]

instance instReprReportativeEvidential : Repr ReportativeEvidential

Equations

• instReprReportativeEvidential = { reprPrec := instReprReportativeEvidential.repr }

def instReprReportativeEvidential.repr : ReportativeEvidential → Nat → Std.Format

Equations

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

structure InferentialEvidentialextends Evidential : Type

An inferential evidential: signals that the speaker reasoned to the prejacent from indirect evidence. basis records whether the inference is from observable results (Aikhenvald fromResult) or from general knowledge / reasoning (Aikhenvald fromAssumption).

• form : String
• exponent : Semantics.Evidential.Exponent
• basis : Semantics.Evidential.InferentialBasis

  The basis of inference.

def instDecidableEqInferentialEvidential.decEq (x✝ x✝¹ : InferentialEvidential) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance instDecidableEqInferentialEvidential : DecidableEq InferentialEvidential

Equations

• instDecidableEqInferentialEvidential = instDecidableEqInferentialEvidential.decEq

def instReprInferentialEvidential.repr : InferentialEvidential → Nat → Std.Format

Equations

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

@[instance_reducible]

instance instReprInferentialEvidential : Repr InferentialEvidential

Equations

• instReprInferentialEvidential = { reprPrec := instReprInferentialEvidential.repr }

inductive Semantics.Evidential.Entry : Type

An evidential occurrence in a language's inventory: one of the three coarse kinds, carrying its typed payload.

• direct (e : DirectEvidential) : Entry
• reportative (e : ReportativeEvidential) : Entry
• inferential (e : InferentialEvidential) : Entry

@[instance_reducible]

instance Semantics.Evidential.instDecidableEqEntry : DecidableEq Entry

Equations

• Semantics.Evidential.instDecidableEqEntry = Semantics.Evidential.instDecidableEqEntry.decEq

def Semantics.Evidential.instDecidableEqEntry.decEq (x✝ x✝¹ : Entry) : Decidable (x✝ = x✝¹)

Equations

• Semantics.Evidential.instDecidableEqEntry.decEq (Semantics.Evidential.Entry.direct a) (Semantics.Evidential.Entry.direct b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Semantics.Evidential.instDecidableEqEntry.decEq (Semantics.Evidential.Entry.direct e) (Semantics.Evidential.Entry.reportative e_1) = isFalse ⋯
• Semantics.Evidential.instDecidableEqEntry.decEq (Semantics.Evidential.Entry.direct e) (Semantics.Evidential.Entry.inferential e_1) = isFalse ⋯
• Semantics.Evidential.instDecidableEqEntry.decEq (Semantics.Evidential.Entry.reportative e) (Semantics.Evidential.Entry.direct e_1) = isFalse ⋯
• Semantics.Evidential.instDecidableEqEntry.decEq (Semantics.Evidential.Entry.reportative a) (Semantics.Evidential.Entry.reportative b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Semantics.Evidential.instDecidableEqEntry.decEq (Semantics.Evidential.Entry.reportative e) (Semantics.Evidential.Entry.inferential e_1) = isFalse ⋯
• Semantics.Evidential.instDecidableEqEntry.decEq (Semantics.Evidential.Entry.inferential e) (Semantics.Evidential.Entry.direct e_1) = isFalse ⋯
• Semantics.Evidential.instDecidableEqEntry.decEq (Semantics.Evidential.Entry.inferential e) (Semantics.Evidential.Entry.reportative e_1) = isFalse ⋯
• Semantics.Evidential.instDecidableEqEntry.decEq (Semantics.Evidential.Entry.inferential a) (Semantics.Evidential.Entry.inferential b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Semantics.Evidential.instReprEntry : Repr Entry

Equations

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

def Semantics.Evidential.instReprEntry.repr : Entry → Nat → Std.Format

Equations

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

def Semantics.Evidential.Entry.IsDirect : Entry → Prop

The occurrence is a direct evidential.

Equations

• (Semantics.Evidential.Entry.direct e).IsDirect = True
• x✝.IsDirect = False

@[instance_reducible]

instance Semantics.Evidential.Entry.instDecidablePredIsDirect : DecidablePred IsDirect

Equations

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

def Semantics.Evidential.Entry.IsReportative : Entry → Prop

The occurrence is a reportative evidential.

Equations

• (Semantics.Evidential.Entry.reportative e).IsReportative = True
• x✝.IsReportative = False

@[instance_reducible]

instance Semantics.Evidential.Entry.instDecidablePredIsReportative : DecidablePred IsReportative

Equations

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

def Semantics.Evidential.Entry.IsInferential : Entry → Prop

The occurrence is an inferential evidential.

Equations

• (Semantics.Evidential.Entry.inferential e).IsInferential = True
• x✝.IsInferential = False

@[instance_reducible]

instance Semantics.Evidential.Entry.instDecidablePredIsInferential : DecidablePred IsInferential

Equations

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

def Semantics.Evidential.Entry.exponent : Entry → Exponent

The realization strategy of an entry.

Equations

• (Semantics.Evidential.Entry.direct a).exponent = a.exponent
• (Semantics.Evidential.Entry.reportative a).exponent = a.exponent
• (Semantics.Evidential.Entry.inferential a).exponent = a.exponent

def Semantics.Evidential.Entry.form : Entry → String

The surface form of an entry.

Equations

• (Semantics.Evidential.Entry.direct a).form = a.form
• (Semantics.Evidential.Entry.reportative a).form = a.form
• (Semantics.Evidential.Entry.inferential a).form = a.form