Case Containment and Syncretism

@cite{caha-2009} @cite{mcfadden-2018} @cite{bobaljik-2012} @cite{blake-1994}

Containment

@cite{caha-2009} proposes that the morphosyntactic representation of each case on the hierarchy literally contains the representations of all cases below it:

[[[[[ NOM ] ACC ] GEN ] DAT ] P ]

This means ACC's representation includes NOM's; GEN's includes both ACC's and NOM's; etc. A Vocabulary Insertion rule conditioned on feature F therefore matches every case whose representation contains F. A rule conditioned on ACC matches ACC, GEN, DAT, and P — the set of all nonnominative cases — explaining the widespread NOM vs. oblique split in stem allomorphy (@cite{mcfadden-2018}).

The *ABA Constraint

@cite{bobaljik-2012} and @cite{caha-2009} observe that case-conditioned suppletion obeys a contiguity restriction: if two cases X and Z (with X ⊂ Y ⊂ Z on the hierarchy) share a suppletive form A, then the case Y between them must also have form A. The pattern A–B–A (with B ≠ A) is systematically unattested. This is the *ABA constraint.

The constraint falls out from containment: if a VI rule inserts form B in the context of feature F, and Y's representation contains F, then so does Z's (since Z ⊃ Y ⊃ X). There is no way for Z to "skip" B and revert to A.

Syncretism

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.

Connection to Blake

Core.Case.Hierarchy formalizes Blake's typological hierarchy — an implicational tendency about which cases languages tend to have. Caha's containment hierarchy is a different object: a syntactic claim about the internal structure of case representations. The two are complementary, not competing.

def Theories.Morphology.CaseContainment.containmentRank : Core.Case → Option Nat

Caha's containment rank (@cite{caha-2009}). Cases higher on the containment hierarchy have representations that include all lower cases.

[[[[[ NOM ] ACC ] GEN ] DAT ] P ]

The P(ostpositional) layer includes LOC and other spatial cases whose representations contain the full case spine.

Returns none for cases not on the containment hierarchy (e.g., ERG/ABS in ergative systems, or minor cases whose containment structure is less well established).

Equations

• Theories.Morphology.CaseContainment.containmentRank Core.Case.nom = some 0
• Theories.Morphology.CaseContainment.containmentRank Core.Case.acc = some 1
• Theories.Morphology.CaseContainment.containmentRank Core.Case.gen = some 2
• Theories.Morphology.CaseContainment.containmentRank Core.Case.dat = some 3
• Theories.Morphology.CaseContainment.containmentRank Core.Case.loc = some 4
• Theories.Morphology.CaseContainment.containmentRank x✝ = none

def Theories.Morphology.CaseContainment.containedIn (inner outer : Core.Case) : Bool

Does case inner have a representation contained within case outer? True when inner.containmentRank ≤ outer.containmentRank.

Equations

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

theorem Theories.Morphology.CaseContainment.nom_contained_in_acc : containedIn Core.Case.nom Core.Case.acc = true

NOM is contained in every case on the hierarchy.

theorem Theories.Morphology.CaseContainment.nom_contained_in_gen : containedIn Core.Case.nom Core.Case.gen = true

theorem Theories.Morphology.CaseContainment.nom_contained_in_dat : containedIn Core.Case.nom Core.Case.dat = true

theorem Theories.Morphology.CaseContainment.nom_contained_in_loc : containedIn Core.Case.nom Core.Case.loc = true

theorem Theories.Morphology.CaseContainment.acc_contained_in_gen : containedIn Core.Case.acc Core.Case.gen = true

ACC is contained in GEN, DAT, and LOC but not NOM.

theorem Theories.Morphology.CaseContainment.acc_contained_in_dat : containedIn Core.Case.acc Core.Case.dat = true

theorem Theories.Morphology.CaseContainment.acc_contained_in_loc : containedIn Core.Case.acc Core.Case.loc = true

theorem Theories.Morphology.CaseContainment.acc_not_in_nom : containedIn Core.Case.acc Core.Case.nom = false

theorem Theories.Morphology.CaseContainment.containment_reflexive (c : Core.Case) (h : (containmentRank c).isSome = true) : containedIn c c = true

Every case contains itself.

theorem Theories.Morphology.CaseContainment.containment_transitive (a b c : Core.Case) (hab : containedIn a b = true) (hbc : containedIn b c = true) : containedIn a c = true

Containment is transitive.

def Theories.Morphology.CaseContainment.isNonnom (c : Core.Case) : Bool

The set of nonnominative cases on the containment hierarchy: those whose representation contains ACC.

@cite{mcfadden-2018} argues this is the key natural class for stem allomorphy: a VI rule conditioned on [ACC] captures the NOM-vs-oblique split found cross-linguistically.

Equations

• Theories.Morphology.CaseContainment.isNonnom c = Theories.Morphology.CaseContainment.containedIn Core.Case.acc c

theorem Theories.Morphology.CaseContainment.acc_is_nonnom : isNonnom Core.Case.acc = true

theorem Theories.Morphology.CaseContainment.gen_is_nonnom : isNonnom Core.Case.gen = true

theorem Theories.Morphology.CaseContainment.dat_is_nonnom : isNonnom Core.Case.dat = true

theorem Theories.Morphology.CaseContainment.loc_is_nonnom : isNonnom Core.Case.loc = true

theorem Theories.Morphology.CaseContainment.nom_not_nonnom : isNonnom Core.Case.nom = false

structure Theories.Morphology.CaseContainment.AllomorphyPattern : Type

An allomorphy pattern over the four core cases (NOM, ACC, GEN, DAT), represented as a form-class index for each case.

• nom : Nat
• acc : Nat
• gen : Nat
• dat : Nat

def Theories.Morphology.CaseContainment.instDecidableEqAllomorphyPattern.decEq (x✝ x✝¹ : AllomorphyPattern) : Decidable (x✝ = x✝¹)

Equations

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

instance Theories.Morphology.CaseContainment.instDecidableEqAllomorphyPattern : DecidableEq AllomorphyPattern

Equations

• Theories.Morphology.CaseContainment.instDecidableEqAllomorphyPattern = Theories.Morphology.CaseContainment.instDecidableEqAllomorphyPattern.decEq

def Theories.Morphology.CaseContainment.instBEqAllomorphyPattern.beq : AllomorphyPattern → AllomorphyPattern → Bool

Equations

• One or more equations did not get rendered due to their size.
• Theories.Morphology.CaseContainment.instBEqAllomorphyPattern.beq x✝¹ x✝ = false

instance Theories.Morphology.CaseContainment.instBEqAllomorphyPattern : BEq AllomorphyPattern

Equations

• Theories.Morphology.CaseContainment.instBEqAllomorphyPattern = { beq := Theories.Morphology.CaseContainment.instBEqAllomorphyPattern.beq }

instance Theories.Morphology.CaseContainment.instReprAllomorphyPattern : Repr AllomorphyPattern

Equations

• Theories.Morphology.CaseContainment.instReprAllomorphyPattern = { reprPrec := Theories.Morphology.CaseContainment.instReprAllomorphyPattern.repr }

def Theories.Morphology.CaseContainment.instReprAllomorphyPattern.repr : AllomorphyPattern → Nat → Std.Format

Equations

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

def Theories.Morphology.CaseContainment.AllomorphyPattern.violatesABA (p : AllomorphyPattern) : Bool

Does a pattern contain an ABA subsequence? An ABA violation occurs when two non-adjacent cases on the containment hierarchy share a form that the intervening case does not.

Equations

• p.violatesABA = (p.nom == p.gen && p.nom != p.acc || p.nom == p.dat && p.nom != p.acc || p.nom == p.dat && p.nom != p.gen || p.acc == p.dat && p.acc != p.gen)

def Theories.Morphology.CaseContainment.AllomorphyPattern.isContiguous (p : AllomorphyPattern) : Bool

Is a pattern contiguous? Each form class occupies a contiguous span on the containment hierarchy. Equivalent to ¬violatesABA.

Equations

• p.isContiguous = !p.violatesABA

def Theories.Morphology.CaseContainment.abbPattern : AllomorphyPattern

Equations

• Theories.Morphology.CaseContainment.abbPattern = { nom := 0, acc := 1, gen := 1, dat := 1 }

theorem Theories.Morphology.CaseContainment.abb_contiguous : abbPattern.isContiguous = true

theorem Theories.Morphology.CaseContainment.abb_no_aba : abbPattern.violatesABA = false

def Theories.Morphology.CaseContainment.aabPattern : AllomorphyPattern

Equations

• Theories.Morphology.CaseContainment.aabPattern = { nom := 0, acc := 0, gen := 0, dat := 1 }

theorem Theories.Morphology.CaseContainment.aab_contiguous : aabPattern.isContiguous = true

def Theories.Morphology.CaseContainment.aabbPattern : AllomorphyPattern

Equations

• Theories.Morphology.CaseContainment.aabbPattern = { nom := 0, acc := 0, gen := 1, dat := 1 }

theorem Theories.Morphology.CaseContainment.aabb_contiguous : aabbPattern.isContiguous = true

def Theories.Morphology.CaseContainment.ababPattern : AllomorphyPattern

Equations

• Theories.Morphology.CaseContainment.ababPattern = { nom := 0, acc := 1, gen := 0, dat := 1 }

theorem Theories.Morphology.CaseContainment.abab_violates_aba : ababPattern.violatesABA = true

theorem Theories.Morphology.CaseContainment.abab_not_contiguous : ababPattern.isContiguous = false

def Theories.Morphology.CaseContainment.abaPattern : AllomorphyPattern

Equations

• Theories.Morphology.CaseContainment.abaPattern = { nom := 0, acc := 1, gen := 0, dat := 0 }

theorem Theories.Morphology.CaseContainment.aba_violates : abaPattern.violatesABA = true

def Theories.Morphology.CaseContainment.babPattern : AllomorphyPattern

Equations

• Theories.Morphology.CaseContainment.babPattern = { nom := 1, acc := 0, gen := 1, dat := 0 }

theorem Theories.Morphology.CaseContainment.bab_violates : babPattern.violatesABA = true

def Theories.Morphology.CaseContainment.uniformPattern : AllomorphyPattern

Equations

• Theories.Morphology.CaseContainment.uniformPattern = { nom := 0, acc := 0, gen := 0, dat := 0 }

theorem Theories.Morphology.CaseContainment.uniform_contiguous : uniformPattern.isContiguous = true

theorem Theories.Morphology.CaseContainment.containment_refines_blake : Core.Case.nom.hierarchyRank ≥ Core.Case.acc.hierarchyRank ∧ Core.Case.acc.hierarchyRank ≥ Core.Case.gen.hierarchyRank ∧ Core.Case.gen.hierarchyRank ≥ Core.Case.dat.hierarchyRank

Containment rank preserves Blake's typological ordering on the core cases (NOM, ACC, GEN, DAT): the orderings are inverses. Blake ranks by "how likely a language is to have it" (NOM most common → highest), while containment ranks by "how much structure it contains" (NOM least complex → lowest).

structure Theories.Morphology.CaseContainment.Syncretism : Type

A syncretism pattern: two cases share a morphological exponent.

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

instance Theories.Morphology.CaseContainment.instReprSyncretism : Repr Syncretism

Equations

• Theories.Morphology.CaseContainment.instReprSyncretism = { reprPrec := Theories.Morphology.CaseContainment.instReprSyncretism.repr }

def Theories.Morphology.CaseContainment.instReprSyncretism.repr : Syncretism → Nat → Std.Format

Equations

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

def Theories.Morphology.CaseContainment.hierarchyAdjacent (c1 c2 : Core.Case) : Bool

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

Equations

• Theories.Morphology.CaseContainment.hierarchyAdjacent c1 c2 = (c1.hierarchyRank == c2.hierarchyRank || c1.hierarchyRank + 1 == c2.hierarchyRank || c2.hierarchyRank + 1 == c1.hierarchyRank)

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

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

Equations

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

def Theories.Morphology.CaseContainment.nomAccSyncretism : Syncretism

Equations

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

def Theories.Morphology.CaseContainment.comInstSyncretism : Syncretism

Equations

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

theorem Theories.Morphology.CaseContainment.nom_acc_adjacent : hierarchyAdjacent Core.Case.nom Core.Case.acc = true

theorem Theories.Morphology.CaseContainment.com_inst_adjacent : hierarchyAdjacent Core.Case.com Core.Case.inst = true

theorem Theories.Morphology.CaseContainment.dat_loc_adjacent : hierarchyAdjacent Core.Case.dat Core.Case.loc = true

theorem Theories.Morphology.CaseContainment.gen_dat_adjacent : hierarchyAdjacent Core.Case.gen Core.Case.dat = true

theorem Theories.Morphology.CaseContainment.erg_inst_not_strictly_adjacent : hierarchyAdjacent Core.Case.erg Core.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 Theories.Morphology.CaseContainment.erg_inst_inv_adjacent : inventoryAdjacent [Core.Case.erg, Core.Case.abs, Core.Case.inst] Core.Case.erg Core.Case.inst = true

But ERG/INST IS inventory-adjacent in a system with only {ERG, ABS, INST}.

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

Same-tier cases are always strictly adjacent.

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

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

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

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

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

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

ERG/INST syncretism: both share the {src} feature despite hierarchy non-adjacency.

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

NOM/ACC syncretism (neuter nouns): both contain the abs feature.

theorem Theories.Morphology.CaseContainment.abl_loc_same_case_relation : Core.Case.abl.toCaseRelation = Core.Case.loc.toCaseRelation

ABL/LOC syncretism: both map to {loc}.