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 feature value drawn from Features.Evidentiality.

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

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

@[implicit_reducible]

instance Semantics.Evidential.instDecidableEqExponent : DecidableEq Exponent

Equations

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

@[implicit_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).

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 ⋯

@[implicit_reducible]

instance instDecidableEqEvidential : DecidableEq Evidential

Equations

• instDecidableEqEvidential = instDecidableEqEvidential.decEq

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) " }"

@[implicit_reducible]

instance instReprEvidential : Repr Evidential

Equations

• instReprEvidential = { reprPrec := instReprEvidential.repr }

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 : Features.Evidentiality.DirectSource

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

@[implicit_reducible]

instance instDecidableEqDirectEvidential : DecidableEq DirectEvidential

Equations

• instDecidableEqDirectEvidential = instDecidableEqDirectEvidential.decEq

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

Equations

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

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

Equations

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

@[implicit_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 : Features.Evidentiality.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.

@[implicit_reducible]

instance instDecidableEqReportativeEvidential : DecidableEq ReportativeEvidential

Equations

• instDecidableEqReportativeEvidential = instDecidableEqReportativeEvidential.decEq

@[implicit_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 : Features.Evidentiality.InferentialBasis

  The basis of inference.

@[implicit_reducible]

instance instDecidableEqInferentialEvidential : DecidableEq InferentialEvidential

Equations

• instDecidableEqInferentialEvidential = instDecidableEqInferentialEvidential.decEq

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

Equations

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

@[implicit_reducible]

instance instReprInferentialEvidential : Repr InferentialEvidential

Equations

• instReprInferentialEvidential = { reprPrec := instReprInferentialEvidential.repr }

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

Equations

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

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

@[implicit_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 ⋯

@[implicit_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

@[implicit_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

@[implicit_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

@[implicit_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