Evidentials

This file defines the evidential as a lexical object: a form, its realization, and the information sources it covers. Following Aikhenvald, information source is carved into six recurrent semantic parameters — visual, non-visual sensory, inference, assumption, hearsay and quotative — and an evidential covers a set of them: a firsthand term covers visual and sensory evidence together, a non-firsthand term covers inference, assumption and hearsay, a visual term covers visual evidence alone. A language's inventory is a List Evidential declared in its Fragment; it is well formed when no parameter is covered twice, so that the terms partition the parameters the language expresses (Semantics/Evidential/Basic.lean).

Main definitions

• Evidential.Parameter — the six semantic parameters of information source.
• Evidential.Exponent — how an evidential is realized.
• Evidential — the lexical entry; Evidential.covers its information sources.
• Evidential.IsDirect, IsInferential, IsReportative, IsNonfirsthand — the coarse kinds of term, as properties of coverage.
• Evidential.WellFormed, Evidential.expressed — a paradigm's disjointness and its span.

References

• [Aik04], §2.5
• [willett-1988]

inductive Evidential.Parameter : Type

The six recurrent semantic parameters of information source.

• visual : Parameter

  Information acquired through seeing.

• sensory : Parameter

  Information acquired through hearing, extended to smell, taste and touch.

• inference : Parameter

  Inference from visible or tangible evidence or result.

• assumption : Parameter

  Assumption from reasoning or general knowledge.

• hearsay : Parameter

  Reported information with no reference to its source.

• quotative : Parameter

  Reported information with overt reference to the quoted source.

@[instance_reducible]

instance Evidential.instDecidableEqParameter : DecidableEq Parameter

Equations

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

def Evidential.instReprParameter.repr : Parameter → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Evidential.instReprParameter : Repr Parameter

Equations

• Evidential.instReprParameter = { reprPrec := Evidential.instReprParameter.repr }

@[instance_reducible]

instance Evidential.instFintypeParameter : Fintype Parameter

Equations

• Evidential.instFintypeParameter = { elems := { val := ↑Evidential.Parameter.enumList, nodup := Evidential.Parameter.enumList_nodup }, complete := Evidential.instFintypeParameter._proof_1 }

inductive Evidential.Exponent : Type

How an evidential is morphosyntactically realized.

• verbalAffix : Exponent

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

• tamFusion : Exponent

  Fused into the TAM paradigm (the Bulgarian l-form).

• clitic2P : Exponent

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

• clauseParticle : Exponent

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

• parenthetical : Exponent

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

• lexicalFrame : Exponent

  A grammaticalized lexical frame (Korean -tay).

• toneAblaut : Exponent

  Tonal or ablaut realization.

@[instance_reducible]

instance Evidential.instDecidableEqExponent : DecidableEq Exponent

Equations

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

@[instance_reducible]

instance Evidential.instReprExponent : Repr Exponent

Equations

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

def Evidential.instReprExponent.repr : Exponent → ℕ → Std.Format

Equations

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

structure Evidential : Type

An evidential: its form, its realization, and the information sources it covers.

• form : String

  A representative morpheme or construction label.

• exponent : Exponent

  The realization strategy.

• covers : Finset Parameter

  The semantic parameters the term covers.

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

Equations

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

@[instance_reducible]

instance instDecidableEqEvidential : DecidableEq Evidential

Equations

• instDecidableEqEvidential = instDecidableEqEvidential.decEq

def Evidential.IsDirect (e : Evidential) : Prop

A direct evidential covers firsthand evidence only.

Equations

• e.IsDirect = (e.covers.Nonempty ∧ e.covers ⊆ {Evidential.Parameter.visual, Evidential.Parameter.sensory})

def Evidential.IsInferential (e : Evidential) : Prop

An inferential evidential covers inference or assumption only.

Equations

• e.IsInferential = (e.covers.Nonempty ∧ e.covers ⊆ {Evidential.Parameter.inference, Evidential.Parameter.assumption})

def Evidential.IsReportative (e : Evidential) : Prop

A reportative evidential covers hearsay or quotation only.

Equations

• e.IsReportative = (e.covers.Nonempty ∧ e.covers ⊆ {Evidential.Parameter.hearsay, Evidential.Parameter.quotative})

def Evidential.IsNonfirsthand (e : Evidential) : Prop

A non-firsthand evidential covers inference and hearsay together but not visual evidence: the marked term of a two-choice system.

Equations

• e.IsNonfirsthand = (Evidential.Parameter.inference ∈ e.covers ∧ Evidential.Parameter.hearsay ∈ e.covers ∧ Evidential.Parameter.visual ∉ e.covers)

@[instance_reducible]

instance Evidential.instDecidablePredIsDirect : DecidablePred IsDirect

Equations

• x✝.instDecidablePredIsDirect = Evidential.instDecidablePredIsDirect._aux_1 x✝

@[instance_reducible]

instance Evidential.instDecidablePredIsInferential : DecidablePred IsInferential

Equations

• x✝.instDecidablePredIsInferential = Evidential.instDecidablePredIsInferential._aux_1 x✝

@[instance_reducible]

instance Evidential.instDecidablePredIsReportative : DecidablePred IsReportative

Equations

• x✝.instDecidablePredIsReportative = Evidential.instDecidablePredIsReportative._aux_1 x✝

@[instance_reducible]

instance Evidential.instDecidablePredIsNonfirsthand : DecidablePred IsNonfirsthand

Equations

• x✝.instDecidablePredIsNonfirsthand = Evidential.instDecidablePredIsNonfirsthand._aux_1 x✝

def Evidential.expressed (es : List Evidential) : Finset Parameter

The parameters an inventory expresses.

Equations

• Evidential.expressed es = (List.map Evidential.covers es).toFinset.sup id

def Evidential.WellFormed (es : List Evidential) : Prop

An inventory is well formed when distinct terms cover disjoint parameters.

Equations

• Evidential.WellFormed es = ∀ a ∈ es, ∀ b ∈ es, a ≠ b → Disjoint a.covers b.covers

@[instance_reducible]

instance Evidential.instDecidablePredListWellFormed : DecidablePred WellFormed

Equations

• Evidential.instDecidablePredListWellFormed es = Evidential.instDecidablePredListWellFormed._aux_1 es