Case Syncretism @cite{blake-1994}

@cite{baerman-2005} @cite{caha-2009}

Syncretism is the systematic neutralization of case distinctions: two or more cases share a single morphological exponent in some paradigm cells. @cite{blake-1994} documents syncretism patterns in Latin, Greek, and other IE languages. He observes that syncretisms cluster into groups (NOM+ACC vs. DAT+ABL) that are "significant on other grounds" (p. 22).

The adjacency constraint — that syncretic cases must be adjacent on the case hierarchy — is a generalization from the Nanosyntax tradition, not an explicit claim by Blake. Blake's data is consistent with it, and his ERG/INST syncretism (Australian languages) is the canonical exception, which he explains via historical derivation of ERG from INST (pp. 174–175).

Examples

• NOM/ACC syncretism in neuter nouns (Latin, Greek, Russian): same tier (rank 6)
• COM/INST syncretism (WALS Ch. 52): adjacent (ranks 1, 2)

Formalization

We define syncretism as a relation between two cases within a given inventory. hierarchyAdjacent checks strict adjacency (ranks differ by ≤ 1). inventoryAdjacent checks relaxed adjacency (no intervening case in the actual inventory).

structure Core.Syncretism : Type

A syncretism pattern: two cases share a morphological exponent.

• case1 : Case

  The two syncretic cases

• case2 : Case
• neq : self.case1 ≠ self.case2

  The cases must be distinct

def Core.instReprSyncretism.repr : Syncretism → Nat → Std.Format

Equations

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

instance Core.instReprSyncretism : Repr Syncretism

Equations

• Core.instReprSyncretism = { reprPrec := Core.instReprSyncretism.repr }

def Core.hierarchyAdjacent (c1 c2 : Case) : Bool

Are two cases adjacent on the hierarchy (same rank or ranks differ by 1)?

This is the strict form of the adjacency constraint. In practice, some syncretisms span larger distances (e.g., ERG/INST in Australian languages), but the generalization is that adjacency is the norm.

Equations

• Core.hierarchyAdjacent c1 c2 = (c1.hierarchyRank == c2.hierarchyRank || c1.hierarchyRank + 1 == c2.hierarchyRank || c2.hierarchyRank + 1 == c1.hierarchyRank)

def Core.inventoryAdjacent (inv : List Case) (c1 c2 : Case) : Bool

Relaxed adjacency: no case in the inventory falls strictly between the two syncretic cases on the hierarchy.

This captures the idea that syncretism is "locally adjacent" within the language's actual inventory, even if non-adjacent on the full hierarchy. E.g., DAT/ACC might be adjacent in a system that lacks GEN.

Equations

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

def Core.nomAccSyncretism : Syncretism

NOM/ACC syncretism (neuter nouns in Latin, Greek, Russian, etc.). Same rank — trivially adjacent.

Equations

• Core.nomAccSyncretism = { case1 := Core.Case.nom, case2 := Core.Case.acc, neq := Core.nomAccSyncretism._proof_1 }

def Core.comInstSyncretism : Syncretism

COM/INST syncretism (WALS Ch. 52: many languages use one marker).

Equations

• Core.comInstSyncretism = { case1 := Core.Case.com, case2 := Core.Case.inst, neq := Core.comInstSyncretism._proof_1 }

theorem Core.nom_acc_adjacent : hierarchyAdjacent Case.nom Case.acc = true

NOM/ACC syncretism satisfies strict adjacency (same tier).

theorem Core.com_inst_adjacent : hierarchyAdjacent Case.com Case.inst = true

COM/INST syncretism satisfies strict adjacency (ranks 1, 2).

theorem Core.dat_loc_adjacent : hierarchyAdjacent Case.dat Case.loc = true

DAT/LOC syncretism satisfies strict adjacency (ranks 4, 3).

theorem Core.gen_dat_adjacent : hierarchyAdjacent Case.gen Case.dat = true

GEN/DAT syncretism satisfies strict adjacency (ranks 5, 4).

theorem Core.erg_inst_not_strictly_adjacent : hierarchyAdjacent Case.erg Case.inst = false

ERG/INST syncretism does NOT satisfy strict adjacency (ranks 6, 2) — this is Blake's known exception, explained by historical derivation.

theorem Core.erg_inst_inv_adjacent : inventoryAdjacent [Case.erg, Case.abs, Case.inst] Case.erg Case.inst = true

But ERG/INST IS inventory-adjacent in a system with only {ERG, ABS, INST} (no GEN, DAT, LOC between them).

theorem Core.same_tier_adjacent (c1 c2 : Case) (h : c1.hierarchyRank = c2.hierarchyRank) : hierarchyAdjacent c1 c2 = true

Same-tier cases (NOM/ACC, ERG/ABS, ABL/INST) are always strictly adjacent. These are the most common syncretism targets cross-linguistically.

theorem Core.neuter_syncretism_contiguous : { nom := 0, acc := 0, gen := 1, dat := 1 }.isContiguous = true

NOM/ACC syncretism (neuter paradigms): NOM=ACC share form 0, GEN and DAT have form 1. AABB pattern — contiguous.

theorem Core.nom_gen_without_acc_violates_aba : { nom := 0, acc := 1, gen := 0, dat := 1 }.violatesABA = true

NOM/GEN syncretism without ACC syncretism would be an ABA pattern — predicted NOT to occur by @cite{caha-2009}.

theorem Core.acc_gen_syncretism_contiguous : { nom := 0, acc := 1, gen := 1, dat := 2 }.isContiguous = true

ACC/GEN syncretism with distinct NOM and DAT: ABBC — contiguous.

theorem Core.gen_dat_syncretism_contiguous : { nom := 0, acc := 1, gen := 2, dat := 2 }.isContiguous = true

GEN/DAT syncretism: NOM and ACC distinct from GEN=DAT. AABC — contiguous.

theorem Core.nom_dat_syncretism_violates_aba : { nom := 0, acc := 1, gen := 1, dat := 0 }.violatesABA = true

NOM/DAT syncretism (skipping ACC and GEN): ABBA — violates *ABA. The containment hierarchy predicts this cannot occur: DAT contains ACC, so any form shared by NOM and DAT must also be shared by ACC.

theorem Core.erg_inst_share_src : Option.map CaseRelation.src Case.erg.toCaseRelation = some true ∧ Option.map CaseRelation.src Case.inst.toCaseRelation = some true ∧ hierarchyAdjacent Case.erg Case.inst = false

ERG/INST syncretism (@cite{blake-1994}, pp. 174–175) is NOT adjacent on Blake's hierarchy (ranks 6 vs 2), but Anderson's feature decomposition explains it: both ERG and INST share the {src} feature. ERG = abs+src (by subject formation, eq. 40); INST = src (source of force). The shared src feature makes syncretism natural despite hierarchy non-adjacency.

theorem Core.nom_acc_share_abs : Option.map CaseRelation.abs Case.nom.toCaseRelation = some true ∧ Option.map CaseRelation.abs Case.acc.toCaseRelation = some true

NOM/ACC syncretism (neuter nouns) is explained by Anderson: both are absolutive-containing relations. NOM = abs{erg} by subject formation (eq. 40); ACC = abs{goal}. They share the abs feature.

theorem Core.abl_loc_same_case_relation : Case.abl.toCaseRelation = Case.loc.toCaseRelation

ABL/LOC syncretism is explained by Anderson: both map to {loc}.