Evidential paradigms

This file proves the basic facts about Willett's types of evidence and builds the paradigm a well-formed inventory forms: its terms partition the parameters the language expresses, a Finpartition. The block of a type is the fiber of Parameter.evidenceType (EvidenceType.mem_block), the blocks of the three types are the pairs of parameters (EvidenceType.block_attested, block_inferring, block_reported), a term is of at most one type (IsOfType.eq), and evidenceType? is the type a term is of (evidenceType?_eq_some_iff).

Main definitions

• Evidential.finpartition — the paradigm of a well-formed inventory.

References

• [Aik04]
• [Wil88]

@[simp]

theorem Evidential.EvidenceType.mem_block {p : Parameter} {t : EvidenceType} : p ∈ t.block ↔ p.evidenceType = t

@[simp]

theorem Evidential.EvidenceType.block_attested : attested.block = {Parameter.visual, Parameter.sensory}

@[simp]

theorem Evidential.EvidenceType.block_inferring : inferring.block = {Parameter.inference, Parameter.assumption}

@[simp]

theorem Evidential.EvidenceType.block_reported : reported.block = {Parameter.hearsay, Parameter.quotative}

theorem Evidential.IsOfType.eq {e : Evidential} {t t' : EvidenceType} (h : e.IsOfType t) (h' : e.IsOfType t') : t = t'

A term is of at most one type of evidence.

theorem Evidential.evidenceType?_eq_some_iff {e : Evidential} {t : EvidenceType} : e.evidenceType? = some t ↔ e.IsOfType t

evidenceType? is the type a term is of.

def Evidential.finpartition (es : List Evidential) (h : WellFormed es) : Finpartition (expressed es)

The paradigm of a well-formed inventory: its terms partition the parameters it expresses.

Equations

• Evidential.finpartition es h = Finpartition.ofErase (List.map Evidential.covers es).toFinset ⋯ ⋯