Christopoulos & Zompì 2023: Weak Case Containment

[CZ23]

Three rival featural decompositions of NOM ≺ ACC ≺ DAT, run against two discriminating predictions under Subset-Principle competition. Strong Case Containment (Table 1; [Cah09], [SMX+19]) nests the three cases in a chain; No Case Containment (Table 2) makes them pairwise incomparable; the paper's Weak Case Containment (Table 24) keeps ACC ⊂ DAT but gives NOM its own feature, incomparable to ACC. The predictions:

• *ABA ([Bob12]'s coinage): SCC and WCC exclude it structurally (noABA, discharged for both by their shared order-theoretic profile: ACC-appliers persist to DAT, and NOM∩DAT-appliers reach ACC); NCC derives it (ncc_aba_generable, via a rule referencing its ACC-only feature k₃).
• Non-Elsewhere Nominative Stems: SCC forces any NOM-applying rule to be the featureless elsewhere (scc_nom_forces_empty) — Doric Greek h-stems, Latvian pat-, and English 3sg h- stems refute this; WCC's k₀ writes them directly (Table 25 rows 2–3; the Latvian rules (7) below). [McF18]'s markedness rescue of SCC is refuted on Latvian/Tocharian Gender in the paper's §3.3 (not formalized here).

Table 25's eight derivation rows are reproduced by decide; the Latvian emphatic pronoun (Table 20, rules (7)) and the Yiddish 1st person (fn. 25) are run as full stem-distribution checks, including the paper's two minimality points: pat- needs the singular feature alongside k₀ (fn. 26), and undz needs k₁ (fn. 25).

Main results

• noABA_scc / noABA_wcc — the generic Decomposition.noABA (*ABA excluded under any decomposition nesting the middle cell) discharged for SCC and WCC by decide on the order-theoretic hypotheses
• ncc_aba_generable — the two-rule NCC vocabulary generating A B A
• scc_nom_forces_empty — SCC has no non-elsewhere nominative rules
• table25_row1 … table25_row8 — the WCC derivation table
• latvian_stems / latvian_gender_blind / latvian_pat_needs_singular — Table 20 under rules (7)
• yiddish_stems / undz_needs_k1 — the fn. 25 paradigm and its k₁ argument

inductive ChristopoulosZompi2023.K : Type

The privative features: k₀–k₃ across the three Case decompositions (Tables 1, 2, 24), plus number (s₀ singular, p₀ plural) and gender features for the empirical paradigms — no property contained in its category-mates (fn. 26).

• k0 : K
• k1 : K
• k2 : K
• k3 : K
• s0 : K
• p0 : K
• m0 : K
• f0 : K

@[implicit_reducible]

instance ChristopoulosZompi2023.instDecidableEqK : DecidableEq K

Equations

• ChristopoulosZompi2023.instDecidableEqK x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance ChristopoulosZompi2023.instFintypeK : Fintype K

Equations

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

def ChristopoulosZompi2023.instReprK.repr : K → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ChristopoulosZompi2023.instReprK : Repr K

Equations

• ChristopoulosZompi2023.instReprK = { reprPrec := ChristopoulosZompi2023.instReprK.repr }

inductive ChristopoulosZompi2023.Case3 : Type

The case triplet, in the *ABA order NOM ≺ ACC ≺ DAT.

• nom : Case3
• acc : Case3
• dat : Case3

@[implicit_reducible]

instance ChristopoulosZompi2023.instDecidableEqCase3 : DecidableEq Case3

Equations

• ChristopoulosZompi2023.instDecidableEqCase3 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance ChristopoulosZompi2023.instFintypeCase3 : Fintype Case3

Equations

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

def ChristopoulosZompi2023.instReprCase3.repr : Case3 → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ChristopoulosZompi2023.instReprCase3 : Repr Case3

Equations

• ChristopoulosZompi2023.instReprCase3 = { reprPrec := ChristopoulosZompi2023.instReprCase3.repr }

def ChristopoulosZompi2023.scc : Case3 → Finset K

Strong Case Containment (Table 1): a chain ∅ ⊂ {k₁} ⊂ {k₁,k₂}.

Equations

• ChristopoulosZompi2023.scc ChristopoulosZompi2023.Case3.nom = ∅
• ChristopoulosZompi2023.scc ChristopoulosZompi2023.Case3.acc = {ChristopoulosZompi2023.K.k1}
• ChristopoulosZompi2023.scc ChristopoulosZompi2023.Case3.dat = {ChristopoulosZompi2023.K.k1, ChristopoulosZompi2023.K.k2}

def ChristopoulosZompi2023.ncc : Case3 → Finset K

No Case Containment (Table 2): pairwise incomparable feature sets; k₃ is the NOM/ACC feature absent from DAT.

Equations

• ChristopoulosZompi2023.ncc ChristopoulosZompi2023.Case3.nom = {ChristopoulosZompi2023.K.k0, ChristopoulosZompi2023.K.k3}
• ChristopoulosZompi2023.ncc ChristopoulosZompi2023.Case3.acc = {ChristopoulosZompi2023.K.k1, ChristopoulosZompi2023.K.k3}
• ChristopoulosZompi2023.ncc ChristopoulosZompi2023.Case3.dat = {ChristopoulosZompi2023.K.k1, ChristopoulosZompi2023.K.k2}

def ChristopoulosZompi2023.wcc : Case3 → Finset K

Weak Case Containment (Table 24): ACC ⊂ DAT as in SCC, but NOM carries its own k₀, incomparable to ACC — no k₃.

Equations

• ChristopoulosZompi2023.wcc ChristopoulosZompi2023.Case3.nom = {ChristopoulosZompi2023.K.k0}
• ChristopoulosZompi2023.wcc ChristopoulosZompi2023.Case3.acc = {ChristopoulosZompi2023.K.k1}
• ChristopoulosZompi2023.wcc ChristopoulosZompi2023.Case3.dat = {ChristopoulosZompi2023.K.k1, ChristopoulosZompi2023.K.k2}

*ABA

The generic order-theoretic exclusion is Decomposition.noABA: whenever the middle cell nests between the outer two, a rule winning both outer cells wins the middle, so no distinct B can interrupt an A_A pattern. It discharges for the two containment decompositions by decide on the hypotheses; NCC violates the first (ncc_aba_generable).

theorem ChristopoulosZompi2023.noABA_scc {F : Type u_1} {v : List (Morphology.Decomposition.Rule Case3 scc F)} {A B : Morphology.Decomposition.Rule Case3 scc F} (hnom : Morphology.Decomposition.IsWinner v Case3.nom A) (hdat : Morphology.Decomposition.IsWinner v Case3.dat A) (hacc : Morphology.Decomposition.IsWinner v Case3.acc B) : B = A

*ABA under Strong Case Containment ([Cah09], [SMX+19]).

theorem ChristopoulosZompi2023.noABA_wcc {F : Type u_1} {v : List (Morphology.Decomposition.Rule Case3 wcc F)} {A B : Morphology.Decomposition.Rule Case3 wcc F} (hnom : Morphology.Decomposition.IsWinner v Case3.nom A) (hdat : Morphology.Decomposition.IsWinner v Case3.dat A) (hacc : Morphology.Decomposition.IsWinner v Case3.acc B) : B = A

*ABA under Weak Case Containment: the paper's Table 24 decomposition keeps SCC's exclusion.

inductive ChristopoulosZompi2023.Ex : Type

Exponent labels for the derivation tables.

• A : Ex
• B : Ex
• C : Ex

@[implicit_reducible]

instance ChristopoulosZompi2023.instDecidableEqEx : DecidableEq Ex

Equations

• ChristopoulosZompi2023.instDecidableEqEx x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ChristopoulosZompi2023.instReprEx.repr : Ex → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ChristopoulosZompi2023.instReprEx : Repr Ex

Equations

• ChristopoulosZompi2023.instReprEx = { reprPrec := ChristopoulosZompi2023.instReprEx.repr }

theorem ChristopoulosZompi2023.ncc_aba_generable : Morphology.Decomposition.pattern [{ feats := ∅, exponent := Ex.A }, { feats := {K.k1, K.k3}, exponent := Ex.B }] Case3.nom = some Ex.A ∧ Morphology.Decomposition.pattern [{ feats := ∅, exponent := Ex.A }, { feats := {K.k1, K.k3}, exponent := Ex.B }] Case3.acc = some Ex.B ∧ Morphology.Decomposition.pattern [{ feats := ∅, exponent := Ex.A }, { feats := {K.k1, K.k3}, exponent := Ex.B }] Case3.dat = some Ex.A

ABA is generable under NCC: an elsewhere rule plus a rule referencing {k₁, k₃} — features jointly present only in ACC — yields A B A (the overgeneration of the paper's §2).

Non-Elsewhere Nominative Stems

theorem ChristopoulosZompi2023.scc_nom_forces_empty {F : Type u_1} {r : Morphology.Decomposition.Rule Case3 scc F} (h : Morphology.Exponence.Applies r Case3.nom) : r.feats = ∅

Under SCC, a rule applicable in the nominative is featureless — the elsewhere rule. SCC therefore cannot write a Non-Elsewhere Nominative Stem (the paper's §3 problem: Doric h-stems, Latvian pat-, English h-).

Table 25: derivations of AAA, ABB, AAB, ABC under WCC

Each row's rule inventory, its generated pattern by decide. Rows 5 and 7 use the minimal {k₂} variant of the table's {(k₁,)k₂}. Rows 2–3 are the NENS derivations — rule A strictly or weakly outranks the elsewhere B.

theorem ChristopoulosZompi2023.table25_row1 (c : Case3) : Morphology.Decomposition.pattern [{ feats := ∅, exponent := Ex.A }] c = some Ex.A

theorem ChristopoulosZompi2023.table25_row2 : Morphology.Decomposition.pattern [{ feats := {K.k0}, exponent := Ex.A }, { feats := {K.k1}, exponent := Ex.B }] Case3.nom = some Ex.A ∧ Morphology.Decomposition.pattern [{ feats := {K.k0}, exponent := Ex.A }, { feats := {K.k1}, exponent := Ex.B }] Case3.acc = some Ex.B ∧ Morphology.Decomposition.pattern [{ feats := {K.k0}, exponent := Ex.A }, { feats := {K.k1}, exponent := Ex.B }] Case3.dat = some Ex.B

theorem ChristopoulosZompi2023.table25_row3 : Morphology.Decomposition.pattern [{ feats := {K.k0}, exponent := Ex.A }, { feats := ∅, exponent := Ex.B }] Case3.nom = some Ex.A ∧ Morphology.Decomposition.pattern [{ feats := {K.k0}, exponent := Ex.A }, { feats := ∅, exponent := Ex.B }] Case3.acc = some Ex.B ∧ Morphology.Decomposition.pattern [{ feats := {K.k0}, exponent := Ex.A }, { feats := ∅, exponent := Ex.B }] Case3.dat = some Ex.B

theorem ChristopoulosZompi2023.table25_row4 : Morphology.Decomposition.pattern [{ feats := ∅, exponent := Ex.A }, { feats := {K.k1}, exponent := Ex.B }] Case3.nom = some Ex.A ∧ Morphology.Decomposition.pattern [{ feats := ∅, exponent := Ex.A }, { feats := {K.k1}, exponent := Ex.B }] Case3.acc = some Ex.B ∧ Morphology.Decomposition.pattern [{ feats := ∅, exponent := Ex.A }, { feats := {K.k1}, exponent := Ex.B }] Case3.dat = some Ex.B

theorem ChristopoulosZompi2023.table25_row5 : Morphology.Decomposition.pattern [{ feats := ∅, exponent := Ex.A }, { feats := {K.k2}, exponent := Ex.B }] Case3.nom = some Ex.A ∧ Morphology.Decomposition.pattern [{ feats := ∅, exponent := Ex.A }, { feats := {K.k2}, exponent := Ex.B }] Case3.acc = some Ex.A ∧ Morphology.Decomposition.pattern [{ feats := ∅, exponent := Ex.A }, { feats := {K.k2}, exponent := Ex.B }] Case3.dat = some Ex.B

theorem ChristopoulosZompi2023.table25_row6 : Morphology.Decomposition.pattern [{ feats := ∅, exponent := Ex.A }, { feats := {K.k1}, exponent := Ex.B }, { feats := {K.k1, K.k2}, exponent := Ex.C }] Case3.nom = some Ex.A ∧ Morphology.Decomposition.pattern [{ feats := ∅, exponent := Ex.A }, { feats := {K.k1}, exponent := Ex.B }, { feats := {K.k1, K.k2}, exponent := Ex.C }] Case3.acc = some Ex.B ∧ Morphology.Decomposition.pattern [{ feats := ∅, exponent := Ex.A }, { feats := {K.k1}, exponent := Ex.B }, { feats := {K.k1, K.k2}, exponent := Ex.C }] Case3.dat = some Ex.C

theorem ChristopoulosZompi2023.table25_row7 : Morphology.Decomposition.pattern [{ feats := {K.k0}, exponent := Ex.A }, { feats := ∅, exponent := Ex.B }, { feats := {K.k2}, exponent := Ex.C }] Case3.nom = some Ex.A ∧ Morphology.Decomposition.pattern [{ feats := {K.k0}, exponent := Ex.A }, { feats := ∅, exponent := Ex.B }, { feats := {K.k2}, exponent := Ex.C }] Case3.acc = some Ex.B ∧ Morphology.Decomposition.pattern [{ feats := {K.k0}, exponent := Ex.A }, { feats := ∅, exponent := Ex.B }, { feats := {K.k2}, exponent := Ex.C }] Case3.dat = some Ex.C

theorem ChristopoulosZompi2023.table25_row8 : Morphology.Decomposition.pattern [{ feats := {K.k0}, exponent := Ex.A }, { feats := {K.k1}, exponent := Ex.B }, { feats := {K.k1, K.k2}, exponent := Ex.C }] Case3.nom = some Ex.A ∧ Morphology.Decomposition.pattern [{ feats := {K.k0}, exponent := Ex.A }, { feats := {K.k1}, exponent := Ex.B }, { feats := {K.k1, K.k2}, exponent := Ex.C }] Case3.acc = some Ex.B ∧ Morphology.Decomposition.pattern [{ feats := {K.k0}, exponent := Ex.A }, { feats := {K.k1}, exponent := Ex.B }, { feats := {K.k1, K.k2}, exponent := Ex.C }] Case3.dat = some Ex.C

Latvian pat- ~ paš- (Table 20, rules (7))

The emphatic pronoun singles out nominative singular across both genders: pat-s / pat-i against paš- everywhere else. Rules (7): pat- in k₀ singular contexts, paš- elsewhere. Number decomposes with neither value contained in the other (fn. 26); gender features are carried by the cells but referenced by no rule.

inductive ChristopoulosZompi2023.LNum : Type

Number.

• sg : LNum
• pl : LNum

@[implicit_reducible]

instance ChristopoulosZompi2023.instDecidableEqLNum : DecidableEq LNum

Equations

• ChristopoulosZompi2023.instDecidableEqLNum x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance ChristopoulosZompi2023.instFintypeLNum : Fintype LNum

Equations

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

@[implicit_reducible]

instance ChristopoulosZompi2023.instReprLNum : Repr LNum

Equations

• ChristopoulosZompi2023.instReprLNum = { reprPrec := ChristopoulosZompi2023.instReprLNum.repr }

def ChristopoulosZompi2023.instReprLNum.repr : LNum → ℕ → Std.Format

Equations

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

inductive ChristopoulosZompi2023.LGen : Type

Gender.

• masc : LGen
• fem : LGen

@[implicit_reducible]

instance ChristopoulosZompi2023.instDecidableEqLGen : DecidableEq LGen

Equations

• ChristopoulosZompi2023.instDecidableEqLGen x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance ChristopoulosZompi2023.instFintypeLGen : Fintype LGen

Equations

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

def ChristopoulosZompi2023.instReprLGen.repr : LGen → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ChristopoulosZompi2023.instReprLGen : Repr LGen

Equations

• ChristopoulosZompi2023.instReprLGen = { reprPrec := ChristopoulosZompi2023.instReprLGen.repr }

structure ChristopoulosZompi2023.LCell : Type

A Latvian cell: case, number, gender.

• case : Case3
• num : LNum
• gen : LGen

@[implicit_reducible]

instance ChristopoulosZompi2023.instDecidableEqLCell : DecidableEq LCell

Equations

• ChristopoulosZompi2023.instDecidableEqLCell = ChristopoulosZompi2023.instDecidableEqLCell.decEq

def ChristopoulosZompi2023.instDecidableEqLCell.decEq (x✝ x✝¹ : LCell) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance ChristopoulosZompi2023.instFintypeLCell : Fintype LCell

Equations

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

@[implicit_reducible]

instance ChristopoulosZompi2023.instReprLCell : Repr LCell

Equations

• ChristopoulosZompi2023.instReprLCell = { reprPrec := ChristopoulosZompi2023.instReprLCell.repr }

def ChristopoulosZompi2023.instReprLCell.repr : LCell → ℕ → Std.Format

Equations

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

def ChristopoulosZompi2023.latvian (c : LCell) : Finset K

The Latvian decomposition: WCC for case, s₀/p₀ for number, m₀/f₀ for gender.

Equations

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

def ChristopoulosZompi2023.latvianRules : List (Morphology.Decomposition.Rule LCell latvian String)

Rules (7): pat- in k₀ singular contexts; paš- elsewhere.

Equations

• ChristopoulosZompi2023.latvianRules = [{ feats := {ChristopoulosZompi2023.K.k0, ChristopoulosZompi2023.K.s0}, exponent := "pat" }, { feats := ∅, exponent := "paš" }]

def ChristopoulosZompi2023.table20stem (c : LCell) : String

The stem distribution of Table 20: pat- exactly in the nominative singulars, paš- elsewhere (stems read off pat-s, pat-i, paš-u, paš-am, paš-ai, paš-i, paš-as, paš-us, paš-iem, paš-ām).

Equations

• ChristopoulosZompi2023.table20stem c = if c.case = ChristopoulosZompi2023.Case3.nom ∧ c.num = ChristopoulosZompi2023.LNum.sg then "pat" else "paš"

theorem ChristopoulosZompi2023.latvian_stems (c : LCell) : Morphology.Decomposition.pattern latvianRules c = some (table20stem c)

Rules (7) generate Table 20's stem distribution.

theorem ChristopoulosZompi2023.latvian_gender_blind (c : Case3) (n : LNum) : Morphology.Decomposition.pattern latvianRules { case := c, num := n, gen := LGen.masc } = Morphology.Decomposition.pattern latvianRules { case := c, num := n, gen := LGen.fem }

The pattern "cuts across genders": neither rule references gender, so the distribution is gender-blind.

theorem ChristopoulosZompi2023.latvian_pat_needs_singular : Morphology.Decomposition.pattern [{ feats := {K.k0}, exponent := "pat" }, { feats := ∅, exponent := "paš" }] { case := Case3.nom, num := LNum.pl, gen := LGen.masc } = some "pat"

pat- must be specified for the singular alongside k₀ (fn. 26): dropping s₀ overgenerates pat- into the nominative plural.

Yiddish 1st person (fn. 25): why k₁ exists

ix (NOM.SG), m- (elsewhere: m-ir, m-ix), undz (ACC.PL and DAT.PL). The undz rule must reference k₁: specified for plural alone it would also capture the nominative plural m-ir. This ABB row with B more specific than the elsewhere is the evidence that WCC's k₁ is not eliminable.

structure ChristopoulosZompi2023.YCell : Type

A Yiddish cell: case and number.

• case : Case3
• num : LNum

@[implicit_reducible]

instance ChristopoulosZompi2023.instDecidableEqYCell : DecidableEq YCell

Equations

• ChristopoulosZompi2023.instDecidableEqYCell = ChristopoulosZompi2023.instDecidableEqYCell.decEq

def ChristopoulosZompi2023.instDecidableEqYCell.decEq (x✝ x✝¹ : YCell) : Decidable (x✝ = x✝¹)

Equations

• ChristopoulosZompi2023.instDecidableEqYCell.decEq { case := a, num := a_1 } { case := b, num := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance ChristopoulosZompi2023.instFintypeYCell : Fintype YCell

Equations

• ChristopoulosZompi2023.instFintypeYCell = Fintype.ofEquiv ((_ : ChristopoulosZompi2023.Case3) × ChristopoulosZompi2023.LNum) ChristopoulosZompi2023.YCell.proxyTypeEquiv

def ChristopoulosZompi2023.instReprYCell.repr : YCell → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ChristopoulosZompi2023.instReprYCell : Repr YCell

Equations

• ChristopoulosZompi2023.instReprYCell = { reprPrec := ChristopoulosZompi2023.instReprYCell.repr }

def ChristopoulosZompi2023.yiddish (c : YCell) : Finset K

The Yiddish decomposition: WCC for case, s₀/p₀ for number.

Equations

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

def ChristopoulosZompi2023.yiddishRules : List (Morphology.Decomposition.Rule YCell yiddish String)

The three stem rules: ix a non-elsewhere nominative-singular stem, undz the k₁-plural stem, m- the elsewhere.

Equations

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

def ChristopoulosZompi2023.yiddishStem (c : YCell) : String

The fn. 25 paradigm's stem distribution: ix / m-ix / m-ir in the singular, m-ir / undz / undz in the plural.

Equations

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

theorem ChristopoulosZompi2023.yiddish_stems (c : YCell) : Morphology.Decomposition.pattern yiddishRules c = some (yiddishStem c)

The three rules generate the paradigm.

theorem ChristopoulosZompi2023.undz_needs_k1 : Morphology.Decomposition.pattern [{ feats := {K.k0, K.s0}, exponent := "ix" }, { feats := {K.p0}, exponent := "undz" }, { feats := ∅, exponent := "m" }] { case := Case3.nom, num := LNum.pl } = some "undz"

undz needs k₁ (fn. 25): specified for plural alone, it wrongly beats m- in the nominative plural.