Oswalt (1986): The Evidential System of Kashaya

This file formalizes Oswalt's description of the Kashaya evidential suffixes, recorded in Fragments/Kashaya/Evidentiality.lean as the columns of his Table 1. The suffixes of a column are mutually exclusive, only one appearing on a verb, and cover disjoint sources, so every column is a well-formed paradigm (paradigm_wellFormed). A response to another's words drops the performative pair, the factual-visual pair taking its place (paradigm_responsive, performative_notMem_responsive). The narrative construction simplifies the distinctions to two, personal experience against the quotative: as a partition of the sources a spontaneous remark expresses, every column is a coarsening of the spontaneous column (spontaneous_le), the spontaneous column making four distinctions of source and the narrative and remote columns two (card_parts_spontaneous, card_parts_narrative). The rows of the table are a hierarchy, Performative > Factual-Visual > Auditory > Inferential > Quotative, each with priority over those below it, so the evidential a speaker uses is the first of the column covering a source at hand (preferred). Seeing takes precedence over every other source (preferred_of_visual_mem), the quotative is used exactly when report is at hand and no other row covers a source at hand (preferred_eq_quotative_iff), and the performative is never chosen on the strength of a parameter (preferred_ne_performative). Inferential II must be followed by another suffix and belongs to no column (inferentialII_notMem). The chapter's examples name the evidential they illustrate and, for the suffixes of the paradigm, the mode; each lies in the paradigm of its mode for the aspect of its stem (examples_mem_paradigm).

References

• [Osw86]

The columns of Table 1

theorem Oswalt1986.paradigm_wellFormed (m : Kashaya.Evidentiality.Mode) (a : Aspect.Perfectivity) : Evidential.WellFormed (Kashaya.Evidentiality.paradigm m a)

The suffixes of a column are mutually exclusive and cover disjoint sources.

theorem Oswalt1986.paradigm_responsive (a : Aspect.Perfectivity) : Kashaya.Evidentiality.paradigm Kashaya.Evidentiality.Mode.responsive a = (Kashaya.Evidentiality.paradigm Kashaya.Evidentiality.Mode.spontaneous a).erase (Kashaya.Evidentiality.performative a)

A response drops the performative pair, the factual-visual pair taking its place.

theorem Oswalt1986.performative_notMem_responsive (a : Aspect.Perfectivity) : Kashaya.Evidentiality.performative a ∉ Kashaya.Evidentiality.paradigm Kashaya.Evidentiality.Mode.responsive a

The performative does not take the responsive suffix, so that men s̓ímela 'I have done that' is normal as an isolated remark and men s̓ímelam does not occur.

theorem Oswalt1986.inferentialII_notMem (m : Kashaya.Evidentiality.Mode) (a : Aspect.Perfectivity) : Kashaya.Evidentiality.inferentialII ∉ Kashaya.Evidentiality.paradigm m a

Inferential II, never verb-final, belongs to no column.

The narrative simplification

theorem Oswalt1986.expressed_spontaneous_subset (m : Kashaya.Evidentiality.Mode) (a : Aspect.Perfectivity) : Evidential.expressed (Kashaya.Evidentiality.paradigm Kashaya.Evidentiality.Mode.spontaneous a) ⊆ Evidential.expressed (Kashaya.Evidentiality.paradigm m a)

No column leaves a source unexpressed that a spontaneous remark expresses.

theorem Oswalt1986.spontaneous_le (m : Kashaya.Evidentiality.Mode) (a : Aspect.Perfectivity) : Evidential.finpartition (Kashaya.Evidentiality.paradigm Kashaya.Evidentiality.Mode.spontaneous a) ⋯ ≤ (Evidential.finpartition (Kashaya.Evidentiality.paradigm m a) ⋯).restrict ⋯

Every column is a coarsening of the spontaneous column, its paradigm restricted to the sources a spontaneous remark expresses being refined by the spontaneous paradigm.

theorem Oswalt1986.card_parts_spontaneous (a : Aspect.Perfectivity) : (Evidential.finpartition (Kashaya.Evidentiality.paradigm Kashaya.Evidentiality.Mode.spontaneous a) ⋯).parts.card = 4

A spontaneous remark makes four distinctions of source in either aspect, since the performative, covering no parameter, adds no block.

theorem Oswalt1986.card_parts_narrative (a : Aspect.Perfectivity) : (Evidential.finpartition (Kashaya.Evidentiality.paradigm Kashaya.Evidentiality.Mode.narrative a) ⋯).parts.card = 2 ∧ (Evidential.finpartition (Kashaya.Evidentiality.paradigm Kashaya.Evidentiality.Mode.remote a) ⋯).parts.card = 2

The narrative construction and the remote past simplify the distinctions to two, personal experience against the quotative.

The hierarchy

def Oswalt1986.preferred (es : List Evidential) (sources : Finset Evidential.Parameter) : Option Evidential

The evidential a column prefers for the sources at hand is its first suffix covering one of them, the rows of Table 1 being ordered so that each has priority over those below.

Equations

• Oswalt1986.preferred es sources = List.find? (fun (e : Evidential) => decide (e.covers ∩ sources).Nonempty) es

theorem Oswalt1986.preferred_of_visual_mem (a : Aspect.Perfectivity) {S : Finset Evidential.Parameter} (h : Evidential.Parameter.visual ∈ S) : preferred (Kashaya.Evidentiality.paradigm Kashaya.Evidentiality.Mode.spontaneous a) S = some (Kashaya.Evidentiality.factualVisual a)

Seeing takes priority over every other source, so whatever else a speaker has, the factual-visual is used.

theorem Oswalt1986.preferred_append_singleton_eq_some {es : List Evidential} {e : Evidential} (he : e ∉ es) (S : Finset Evidential.Parameter) : preferred (es ++ [e]) S = some e ↔ ¬Disjoint e.covers S ∧ ∀ x ∈ es, Disjoint x.covers S

A column prefers its last suffix exactly when that suffix covers a source at hand and no suffix above it does.

theorem Oswalt1986.preferred_eq_quotative_iff (a : Aspect.Perfectivity) (S : Finset Evidential.Parameter) : preferred (Kashaya.Evidentiality.paradigm Kashaya.Evidentiality.Mode.spontaneous a) S = some Kashaya.Evidentiality.quotative ↔ ¬Disjoint Kashaya.Evidentiality.quotative.covers S ∧ ∀ e ∈ Kashaya.Evidentiality.paradigm Kashaya.Evidentiality.Mode.spontaneous a, e ≠ Kashaya.Evidentiality.quotative → Disjoint e.covers S

The quotative is used exactly when report is at hand and no other row of the column covers a source at hand.

theorem Oswalt1986.preferred_ne_performative (a : Aspect.Perfectivity) (S : Finset Evidential.Parameter) : preferred (Kashaya.Evidentiality.paradigm Kashaya.Evidentiality.Mode.spontaneous a) S ≠ some (Kashaya.Evidentiality.performative a)

The performative, whose source lies outside the parameters, is never chosen on the strength of one.

The examples

def Oswalt1986.mode? (r : Datum) : Option Kashaya.Evidentiality.Mode

The mode an example's mode feature names.

Equations

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

def Oswalt1986.aspects (r : Datum) : List Aspect.Perfectivity

The aspects an example's stem may have, the one its aspect feature names or else either.

Equations

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

def Oswalt1986.evidential? (r : Datum) (a : Aspect.Perfectivity) : Option Evidential

The evidential an example's evidential feature names, for a stem of the given aspect.

Equations

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

theorem Oswalt1986.examples_named (r : Datum) : r ∈ Examples.all → ∀ a ∈ aspects r, (evidential? r a).isSome = true ∧ (evidential? r a ≠ some Kashaya.Evidentiality.inferentialII → (mode? r).isSome = true)

Every example names an evidential, and every one whose evidential is a suffix of the paradigm names its mode.

theorem Oswalt1986.examples_mem_paradigm (r : Datum) : r ∈ Examples.all → ∀ m ∈ mode? r, ∀ a ∈ aspects r, ∀ e ∈ evidential? r a, e ∈ Kashaya.Evidentiality.paradigm m a

The evidential of each example lies in the paradigm of its mode, for the aspect of its stem.