Aikhenvald (2004): Evidentiality

This file formalizes the typology of grammatical evidentiality systems in chapter 2 of Aikhenvald's Evidentiality. A system is classified by how many information sources a speaker must choose among and how they are grouped: five kinds with two choices (A1–A5), five with three, three with four and one with five (D1). Table 2.1 draws the systems as rows over the six semantic parameters, each term spanning the parameters it covers, and leaves out the four kinds organized around an evidentiality-neutral "everything else" term.

A kind's systems (Kind.rows) are its rows of the table, or, for an everything-else kind, the marked terms opposed to the neutral one. Every term spans an interval of the parameters (Kind.ordConnected_cells), and the letter counts the terms plus one for an everything-else term (Kind.length_rows). An inventory realizes a kind when its evidentials cover the terms of one of its systems, one evidential to a term (Realizes); it then realizes no other kind, is well formed, and has as many evidentials as the kind has marked terms. Turkish, Abkhaz and Bulgarian realize A2, their unmarked pasts read as evidentiality-neutral, Aymara and Cuzco Quechua B1, Tuyuca and Tariana D1. The Kashaya performative lies outside the six parameters, so a spontaneous remark realizes no kind; West Greenlandic's synonymous reported evidentials form no paradigm, though each, read as a system on its own, is A3; Euchee's auditory evidential is A5.

Implementation notes

The rows follow Table 2.1 cell for cell, including its A4 term, which the table gives as non-visual although the book's prose describes the Ngiyambaa sensory evidential as covering seeing too. The A2 systems are the two opposites of a firsthand term the A1 rows draw, the book describing the non-firsthand of both kinds as the opposite of the firsthand. An inventory realizes a system only when it covers each term exactly, so a system whose term covers less than its cell, as a B1 system whose first term is visual only, realizes none.

References

• [Aik04]
• [Bar84]
• [For03]
• [Lin00]
• [Osw86]
• [Wil88]

The systems

inductive Aikhenvald2004.Term : Type

The book's names for the terms of evidentiality systems.

• firsthand : Term
• nonfirsthand : Term
• direct : Term
• visual : Term
• nonVisual : Term
• auditory : Term
• inferred : Term
• assumed : Term
• reported : Term
• quotative : Term

@[instance_reducible]

instance Aikhenvald2004.instDecidableEqTerm : DecidableEq Term

Equations

• Aikhenvald2004.instDecidableEqTerm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Aikhenvald2004.instReprTerm.repr : Term → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Aikhenvald2004.instReprTerm.repr Aikhenvald2004.Term.direct prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aikhenvald2004.Term.direct")).group prec✝
• Aikhenvald2004.instReprTerm.repr Aikhenvald2004.Term.visual prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aikhenvald2004.Term.visual")).group prec✝

@[instance_reducible]

instance Aikhenvald2004.instReprTerm : Repr Term

Equations

• Aikhenvald2004.instReprTerm = { reprPrec := Aikhenvald2004.instReprTerm.repr }

inductive Aikhenvald2004.Kind : Type

The fourteen kinds of evidentiality system, the letter giving the number of choices and the digit the grouping of information sources.

• A1 : Kind
• A2 : Kind
• A3 : Kind
• A4 : Kind
• A5 : Kind
• B1 : Kind
• B2 : Kind
• B3 : Kind
• B4 : Kind
• B5 : Kind
• C1 : Kind
• C2 : Kind
• C3 : Kind
• D1 : Kind

@[instance_reducible]

instance Aikhenvald2004.instDecidableEqKind : DecidableEq Kind

Equations

• Aikhenvald2004.instDecidableEqKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Aikhenvald2004.instReprKind.repr : Kind → ℕ → Std.Format

Equations

• Aikhenvald2004.instReprKind.repr Aikhenvald2004.Kind.A1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aikhenvald2004.Kind.A1")).group prec✝
• Aikhenvald2004.instReprKind.repr Aikhenvald2004.Kind.A2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aikhenvald2004.Kind.A2")).group prec✝
• Aikhenvald2004.instReprKind.repr Aikhenvald2004.Kind.A3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aikhenvald2004.Kind.A3")).group prec✝
• Aikhenvald2004.instReprKind.repr Aikhenvald2004.Kind.A4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aikhenvald2004.Kind.A4")).group prec✝
• Aikhenvald2004.instReprKind.repr Aikhenvald2004.Kind.A5 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aikhenvald2004.Kind.A5")).group prec✝
• Aikhenvald2004.instReprKind.repr Aikhenvald2004.Kind.B1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aikhenvald2004.Kind.B1")).group prec✝
• Aikhenvald2004.instReprKind.repr Aikhenvald2004.Kind.B2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aikhenvald2004.Kind.B2")).group prec✝
• Aikhenvald2004.instReprKind.repr Aikhenvald2004.Kind.B3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aikhenvald2004.Kind.B3")).group prec✝
• Aikhenvald2004.instReprKind.repr Aikhenvald2004.Kind.B4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aikhenvald2004.Kind.B4")).group prec✝
• Aikhenvald2004.instReprKind.repr Aikhenvald2004.Kind.B5 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aikhenvald2004.Kind.B5")).group prec✝
• Aikhenvald2004.instReprKind.repr Aikhenvald2004.Kind.C1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aikhenvald2004.Kind.C1")).group prec✝
• Aikhenvald2004.instReprKind.repr Aikhenvald2004.Kind.C2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aikhenvald2004.Kind.C2")).group prec✝
• Aikhenvald2004.instReprKind.repr Aikhenvald2004.Kind.C3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aikhenvald2004.Kind.C3")).group prec✝
• Aikhenvald2004.instReprKind.repr Aikhenvald2004.Kind.D1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aikhenvald2004.Kind.D1")).group prec✝

@[instance_reducible]

instance Aikhenvald2004.instReprKind : Repr Kind

Equations

• Aikhenvald2004.instReprKind = { reprPrec := Aikhenvald2004.instReprKind.repr }

@[instance_reducible]

instance Aikhenvald2004.instFintypeKind : Fintype Kind

Equations

• Aikhenvald2004.instFintypeKind = { elems := { val := ↑Aikhenvald2004.Kind.enumList, nodup := Aikhenvald2004.Kind.enumList_nodup }, complete := Aikhenvald2004.instFintypeKind._proof_1 }

def Aikhenvald2004.Kind.choices : Kind → ℕ

The number of evidentiality choices, counting an evidentiality-neutral term.

Equations

• Aikhenvald2004.Kind.A1.choices = 2
• Aikhenvald2004.Kind.A2.choices = 2
• Aikhenvald2004.Kind.A3.choices = 2
• Aikhenvald2004.Kind.A4.choices = 2
• Aikhenvald2004.Kind.A5.choices = 2
• Aikhenvald2004.Kind.B1.choices = 3
• Aikhenvald2004.Kind.B2.choices = 3
• Aikhenvald2004.Kind.B3.choices = 3
• Aikhenvald2004.Kind.B4.choices = 3
• Aikhenvald2004.Kind.B5.choices = 3
• Aikhenvald2004.Kind.C1.choices = 4
• Aikhenvald2004.Kind.C2.choices = 4
• Aikhenvald2004.Kind.C3.choices = 4
• Aikhenvald2004.Kind.D1.choices = 5

def Aikhenvald2004.Kind.HasDefault (k : Kind) : Prop

The kinds organized around an evidentiality-neutral "everything else" term.

Equations

• k.HasDefault = (k ∈ {Aikhenvald2004.Kind.A2, Aikhenvald2004.Kind.A3, Aikhenvald2004.Kind.A5, Aikhenvald2004.Kind.B5})

@[instance_reducible]

instance Aikhenvald2004.Kind.instDecidablePredHasDefault : DecidablePred HasDefault

Equations

• x✝.instDecidablePredHasDefault = Aikhenvald2004.Kind.instDecidablePredHasDefault._aux_1 x✝

def Aikhenvald2004.Kind.rows : Kind → List (List (Term × Finset Evidential.Parameter))

The systems of each kind, each the list of its marked terms with the parameters they cover. They are the rows of Table 2.1, and for an everything-else kind the terms opposed to the neutral one.

Equations

• One or more equations did not get rendered due to their size.
• Aikhenvald2004.Kind.A3.rows = [[(Aikhenvald2004.Term.reported, {Evidential.Parameter.hearsay, Evidential.Parameter.quotative})]]
• Aikhenvald2004.Kind.A5.rows = [[(Aikhenvald2004.Term.auditory, {Evidential.Parameter.sensory})]]
• Aikhenvald2004.Kind.B5.rows = [[(Aikhenvald2004.Term.reported, {Evidential.Parameter.hearsay}), (Aikhenvald2004.Term.quotative, {Evidential.Parameter.quotative})]]

theorem Aikhenvald2004.Kind.ordConnected_cells (k : Kind) (r : List (Term × Finset Evidential.Parameter)) : r ∈ k.rows → ∀ c ∈ r, (↑c.2).OrdConnected

Every term covers an interval of the parameters, so that in Aikhenvald's order no term skips one.

theorem Aikhenvald2004.Kind.nonempty_cells (k : Kind) (r : List (Term × Finset Evidential.Parameter)) : r ∈ k.rows → ∀ c ∈ r, c.2.Nonempty

Every term covers some parameter.

theorem Aikhenvald2004.Kind.pairwise_disjoint_cells (k : Kind) (r : List (Term × Finset Evidential.Parameter)) : r ∈ k.rows → List.Pairwise (fun (c d : Term × Finset Evidential.Parameter) => Disjoint c.2 d.2) r

The terms of a system cover disjoint parameters.

theorem Aikhenvald2004.Kind.length_rows (k : Kind) (r : List (Term × Finset Evidential.Parameter)) : r ∈ k.rows → (r.length + if k.HasDefault then 1 else 0) = k.choices

The letter of a kind counts the terms of each of its systems, plus one for an everything-else term.

theorem Aikhenvald2004.Kind.length_rows_lt (k : Kind) (r : List (Term × Finset Evidential.Parameter)) : r ∈ k.rows → r.length < Fintype.card Evidential.Parameter

No system gives each of the six parameters a term of its own.

theorem Aikhenvald2004.Kind.eq_of_perm (k k' : Kind) (r : List (Term × Finset Evidential.Parameter)) : r ∈ k.rows → ∀ r' ∈ k'.rows, (List.map Prod.snd r).Perm (List.map Prod.snd r') → k = k'

Distinct kinds have no system in common, even up to the order of the terms.

theorem Aikhenvald2004.Kind.B1_willett : List.map (fun (x : List (Term × Finset Evidential.Parameter)) => List.map Prod.snd x) B1.rows = [[Evidential.EvidenceType.attested.block, Evidential.EvidenceType.inferring.block, Evidential.EvidenceType.reported.block]]

B1 groups the parameters into Willett's three types of evidence.

def Aikhenvald2004.Kind.terms (k : Kind) : Finset Term

The names of the terms of a kind's systems.

Equations

• k.terms = (List.flatMap (fun (x : List (Aikhenvald2004.Term × Finset Evidential.Parameter)) => List.map Prod.fst x) k.rows).toFinset

theorem Aikhenvald2004.Kind.A2_rows_subset : A2.rows ⊆ List.map (fun (x : List (Term × Finset Evidential.Parameter)) => List.filter (fun (x : Term × Finset Evidential.Parameter) => decide (x.1 ≠ Term.firsthand)) x) A1.rows

The non-firsthand term of an A2 system is that of an A1 system, the neutral term replacing the firsthand one.

Inventories

def Aikhenvald2004.Realizes (es : List Evidential) (k : Kind) : Prop

An inventory realizes a kind when its evidentials cover the terms of one of the kind's systems, one evidential to a term.

Equations

• Aikhenvald2004.Realizes es k = ∃ r ∈ k.rows, (List.map Evidential.covers es).Perm (List.map Prod.snd r)

@[instance_reducible]

instance Aikhenvald2004.instDecidableRealizes (es : List Evidential) (k : Kind) : Decidable (Realizes es k)

Equations

• Aikhenvald2004.instDecidableRealizes es k = Aikhenvald2004.instDecidableRealizes._aux_1 es k

theorem Aikhenvald2004.Realizes.eq {es : List Evidential} {k k' : Kind} (h : Realizes es k) (h' : Realizes es k') : k = k'

An inventory realizes at most one kind.

theorem Aikhenvald2004.Realizes.nonempty {es : List Evidential} {k : Kind} (h : Realizes es k) {e : Evidential} (he : e ∈ es) : e.covers.Nonempty

The evidentials of an inventory realizing a kind each cover some parameter.

theorem Aikhenvald2004.Realizes.wellFormed {es : List Evidential} {k : Kind} (h : Realizes es k) : Evidential.WellFormed es

An inventory realizing a kind is well formed.

theorem Aikhenvald2004.Realizes.length_add {es : List Evidential} {k : Kind} (h : Realizes es k) : (es.length + if k.HasDefault then 1 else 0) = k.choices

An inventory realizing a kind has one evidential for each of its marked terms.

theorem Aikhenvald2004.not_realizes_nil (k : Kind) : ¬Realizes [] k

An empty inventory, an evidentiality strategy or none at all, realizes no kind.

The Fragment languages

theorem Aikhenvald2004.turkish : Realizes Turkish.Evidentiality.evidentials Kind.A2

theorem Aikhenvald2004.abkhaz : Realizes Abkhaz.Evidentiality.evidentials Kind.A2

theorem Aikhenvald2004.bulgarian : Realizes Bulgarian.Evidentiality.evidentials Kind.A2

theorem Aikhenvald2004.aymara : Realizes Aymara.Evidentiality.evidentials Kind.B1

theorem Aikhenvald2004.quechua : Realizes Quechua.Evidentiality.evidentials Kind.B1

theorem Aikhenvald2004.tuyuca : Realizes Tuyuca.Evidentiality.evidentials Kind.D1

theorem Aikhenvald2004.tariana : Realizes Tariana.Evidentiality.evidentials Kind.D1

theorem Aikhenvald2004.kashaya_spontaneous (a : Aspect.Perfectivity) (k : Kind) : ¬Realizes (Kashaya.Evidentiality.paradigm Kashaya.Evidentiality.Mode.spontaneous a) k

The Kashaya performative covers none of the six parameters, so in either aspect the paradigm of a spontaneous remark realizes no kind.

theorem Aikhenvald2004.westGreenlandic_not_wellFormed : ¬Evidential.WellFormed WestGreenlandic.Evidentiality.evidentials

West Greenlandic's reported evidentials are synonymous, so they form no paradigm.

theorem Aikhenvald2004.westGreenlandic (k : Kind) : ¬Realizes WestGreenlandic.Evidentiality.evidentials k

West Greenlandic's reported evidentials together realize no kind.

theorem Aikhenvald2004.westGreenlandic_A3 (e : Evidential) : e ∈ WestGreenlandic.Evidentiality.evidentials → Realizes [e] Kind.A3

Each West Greenlandic reported evidential, read as a system on its own, is A3.

Euchee

def Aikhenvald2004.eucheeKe : Evidential

The Euchee auditory evidential -ke, as Linn analyses it; an earlier grammar takes it for a locative only.

Equations

• Aikhenvald2004.eucheeKe = { morphs := [Morphology.Morph.suff "ke"], covers := {Evidential.Parameter.sensory} }

theorem Aikhenvald2004.euchee : Realizes [eucheeKe] Kind.A5

Euchee, the one language found with an A5 system, opposes its auditory evidential to an unmarked term.

The book's examples

def Aikhenvald2004.termNames : List (String × Term)

The terms named by the examples' term feature.

Equations

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

def Aikhenvald2004.kindNames : List (String × Kind)

The kinds named by the examples' system feature.

Equations

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

def Aikhenvald2004.sourceNames : List (String × Evidential.Parameter)

The parameters named by the examples' source feature.

Equations

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

theorem Aikhenvald2004.examples_source_mem_cell (x : Datum) : x ∈ Examples.all → ∀ k ∈ x.parse? "system" kindNames, ∀ t ∈ x.parse? "term" termNames, ∀ p ∈ x.parse? "source" sourceNames, ∃ r ∈ k.rows, ∃ c ∈ r, c.1 = t ∧ p ∈ c.2

In every example the term used covers the source at hand, which lies in the cell of that term in a system of the example's kind.

def Aikhenvald2004.illustrated (lang : String) : Finset Term

The terms illustrated by the examples from a language.

Equations

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

theorem Aikhenvald2004.tariana_illustration : illustrated "tari1256" = Kind.D1.terms

The Tariana illustration runs through every term of a D1 system.

theorem Aikhenvald2004.wanka_illustration : illustrated "jauj1238" = Kind.B1.terms

The Wanka Quechua examples run through every term of a B1 system.

theorem Aikhenvald2004.turkish_illustration : illustrated "nucl1301" = Kind.A2.terms

The Turkish examples, of report, inference and non-visual perception, all use the non-firsthand term of an A2 system.