Morphomes: syncretism classes with no natural characterization

A realization map p : Cell → F assigns a form to each paradigm cell. Its syncretism relation — cells receiving the same form — is exactly mathlib's kernel setoid Setoid.ker p, and the syncretism classes are its equivalence classes. A morphome ([Aro94] coined the term) is a systematic syncretism that does not define a natural class; [Her23] adopts the working definition "a systematic morphological syncretism which does not define a (syntactically or semantically) natural class" (Trommer 2016, quoted approvingly).

Naturalness is a parameter Natural : Set Cell → Prop, not stipulated here. [Her23] operationalizes a natural class as one "coextensive with a value (e.g. SG) or conjunction of values (e.g. 1SG)" and treats naturalness as gradient, so Natural is best read as a threshold slice of that scale; the value-or-conjunction predicate is its canonical instantiation, supplied by the consumer (see Studies/Herce2023.lean). Systematicity — recurrence of the pattern under more than one exponent or allomorph — is a separate criterion the consumer establishes.

Two limitations, per [baerman-2015]'s three-way analysis space for syncretism (morphosyntactic identity / underspecification / morphological stipulation, p. 146): an elsewhere form's fiber is typically also nontrivial and non-natural (one specified cell, the default covers the unnatural rest — Skou, p. 145), so IsMorphome is necessary but not sufficient for stipulation-hood; distinguishing the two needs opposition structure or the systematicity criterion above. And directional syncretism (a cell wearing another cell's form "in place of the expected" one, p. 142) is invisible to the symmetric kernel.

The vocabulary here is deliberately just "morphome": [Her23] rejects Round's rhizomorphome metamorphome meromorphome subdivision as needless jargon, and "metasyncretism" does not appear in the book.

Main declarations

• Morphology.syncretism — the syncretism setoid of a realization map (Setoid.ker)
• Morphology.syncretismClass — the class (fiber) of a given cell
• Morphology.IsMorphome — a nontrivial syncretism class failing Natural

@[reducible, inline]

abbrev Morphology.syncretism {Cell : Type u_1} {F : Type u_2} (p : Cell → F) : Setoid Cell

The syncretism relation of a realization map p: two cells are syncretic iff p assigns them the same form. Exactly the kernel setoid Setoid.ker p; its equivalence classes are the paradigm's syncretism patterns.

Equations

• Morphology.syncretism p = Setoid.ker p

def Morphology.syncretismClass {Cell : Type u_1} {F : Type u_2} (p : Cell → F) (a : Cell) : Set Cell

The syncretism class of a cell a: every cell realized as a is.

Equations

• Morphology.syncretismClass p a = {x : Cell | p x = p a}

theorem Morphology.syncretismClass_mem_classes {Cell : Type u_1} {F : Type u_2} (p : Cell → F) (a : Cell) : syncretismClass p a ∈ (syncretism p).classes

def Morphology.IsMorphome {Cell : Type u_1} {F : Type u_2} (p : Cell → F) (Natural : Set Cell → Prop) (c : Set Cell) : Prop

A morphome ([Her23]): a syncretism class of p that groups more than one cell (Set.Nontrivial) yet is not a Natural class — a grouping visible only in the realization, with no phonological, syntactic, or semantic characterization ([Aro94]'s "morphology by itself"). Natural is a parameter (see the module docstring).

Equations

• Morphology.IsMorphome p Natural c = (c ∈ (Morphology.syncretism p).classes ∧ c.Nontrivial ∧ ¬Natural c)

theorem Morphology.isMorphome_syncretismClass {Cell : Type u_1} {F : Type u_2} (p : Cell → F) (Natural : Set Cell → Prop) (a : Cell) (hnt : (syncretismClass p a).Nontrivial) (hnat : ¬Natural (syncretismClass p a)) : IsMorphome p Natural (syncretismClass p a)

The syncretism class of a is a morphome once it is nontrivial and unnatural — the shape a concrete paradigm instantiates.