@cite{woolford-1997} — Four-Way Case Systems

@cite{woolford-1997} @cite{woolford-2006} @cite{baker-2015} @cite{marantz-1991}

Formalization of @cite{woolford-1997}'s analysis of four-way case systems, with Nez Perce as the primary case study.

Key Claims

1. ERG is lexical (inherent) Case, like dative — assigned at D-structure in conjunction with θ-role assignment. This contrasts with NOM/ACC/ABS, which are structural cases assigned at S-structure.

2. Two structural object Cases: OBJ (assigned/checked by Agr-O, associated with object agreement) and ACC (assigned/checked by V/P, not associated with object agreement). These are distinct cases.

3. Maximum Accusatives formula: The number of structural accusative cases in a clause = #arguments − #lexical cases − 1 (the −1 accounts for the subject, which receives NOM).

4. Subject-object agreement (not ergative): All subjects (NOM and ERG) trigger subject agreement; only OBJ (not ACC) triggers object agreement. ERG subjects do NOT trigger ergative agreement — they trigger the same subject agreement as NOM subjects.

5. Generalization (19): lexically Cased subject → *structural accusative object. In a clause with a lexically Cased subject (e.g., ergative or dative), the highest object cannot have structural accusative Case (although that object can have objective Case). This is subsumed by the Max. Acc. formula for the highest object and derives the prohibited transitive and ditransitive patterns.

Nez Perce Patterns

Transitive (2 args, 1 lexical = ERG):

• Max ACC = 2 − 1 − 1 = 0, but one structural object case is available
• Allowed: NOM-ACC, ERG-OBJ
• Prohibited: *NOM-OBJ, *ERG-ACC

Ditransitive (3 args: agent, goal, theme):

• NOM subject (0 lexical): max ACC = 3 − 0 − 1 = 2 → two ACC
• NOM + DAT goal (1 lexical): max ACC = 3 − 1 − 1 = 1 → one ACC
• ERG subject (1 lexical): max ACC = 3 − 1 − 1 = 1 → one ACC (theme only; gen. (19) blocks ACC for goal)
• ERG + DAT goal (2 lexical): max ACC = 3 − 2 − 1 = 0
• 4 allowed patterns, 8 prohibited (paper's (22))

Integration

• Local WCase type adds OBJ (absent from CaseVal/Core.Case)
• Bridge theorems connect to Core.Case hierarchy validation
• Bridge theorems connect to dependent case algorithm (DependentCase.lean) showing where the theories agree and diverge

inductive Phenomena.Case.Studies.Woolford1997.WCase : Type

Woolford's five-way case inventory for Nez Perce. OBJ is the structural object case distinct from ACC — this is the key innovation over standard NOM/ACC systems.

• nom : WCase
• obj : WCase
• acc : WCase
• erg : WCase
• dat : WCase

instance Phenomena.Case.Studies.Woolford1997.instDecidableEqWCase : DecidableEq WCase

Equations

• Phenomena.Case.Studies.Woolford1997.instDecidableEqWCase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Case.Studies.Woolford1997.instBEqWCase.beq : WCase → WCase → Bool

Equations

• Phenomena.Case.Studies.Woolford1997.instBEqWCase.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Case.Studies.Woolford1997.instBEqWCase : BEq WCase

Equations

• Phenomena.Case.Studies.Woolford1997.instBEqWCase = { beq := Phenomena.Case.Studies.Woolford1997.instBEqWCase.beq }

def Phenomena.Case.Studies.Woolford1997.instReprWCase.repr : WCase → ℕ → Std.Format

Equations

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

instance Phenomena.Case.Studies.Woolford1997.instReprWCase : Repr WCase

Equations

• Phenomena.Case.Studies.Woolford1997.instReprWCase = { reprPrec := Phenomena.Case.Studies.Woolford1997.instReprWCase.repr }

inductive Phenomena.Case.Studies.Woolford1997.CaseKind : Type

Structural vs lexical classification.

• structural : CaseKind
• lexical : CaseKind

instance Phenomena.Case.Studies.Woolford1997.instDecidableEqCaseKind : DecidableEq CaseKind

Equations

• Phenomena.Case.Studies.Woolford1997.instDecidableEqCaseKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Case.Studies.Woolford1997.instBEqCaseKind : BEq CaseKind

Equations

• Phenomena.Case.Studies.Woolford1997.instBEqCaseKind = { beq := Phenomena.Case.Studies.Woolford1997.instBEqCaseKind.beq }

def Phenomena.Case.Studies.Woolford1997.instBEqCaseKind.beq : CaseKind → CaseKind → Bool

Equations

• Phenomena.Case.Studies.Woolford1997.instBEqCaseKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Case.Studies.Woolford1997.instReprCaseKind : Repr CaseKind

Equations

• Phenomena.Case.Studies.Woolford1997.instReprCaseKind = { reprPrec := Phenomena.Case.Studies.Woolford1997.instReprCaseKind.repr }

def Phenomena.Case.Studies.Woolford1997.instReprCaseKind.repr : CaseKind → ℕ → Std.Format

Equations

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

def Phenomena.Case.Studies.Woolford1997.WCase.kind : WCase → CaseKind

Each case's structural/lexical classification.

Equations

• Phenomena.Case.Studies.Woolford1997.WCase.nom.kind = Phenomena.Case.Studies.Woolford1997.CaseKind.structural
• Phenomena.Case.Studies.Woolford1997.WCase.obj.kind = Phenomena.Case.Studies.Woolford1997.CaseKind.structural
• Phenomena.Case.Studies.Woolford1997.WCase.acc.kind = Phenomena.Case.Studies.Woolford1997.CaseKind.structural
• Phenomena.Case.Studies.Woolford1997.WCase.erg.kind = Phenomena.Case.Studies.Woolford1997.CaseKind.lexical
• Phenomena.Case.Studies.Woolford1997.WCase.dat.kind = Phenomena.Case.Studies.Woolford1997.CaseKind.lexical

def Phenomena.Case.Studies.Woolford1997.WCase.triggersSubjAgr : WCase → Bool

Subject agreement: triggered by ALL subjects (NOM and ERG alike). Woolford's key point: ERG subjects trigger subject agreement, not ergative agreement. The agreement system is nominative-accusative, even though the case system has ergative.

Equations

• Phenomena.Case.Studies.Woolford1997.WCase.nom.triggersSubjAgr = true
• Phenomena.Case.Studies.Woolford1997.WCase.erg.triggersSubjAgr = true
• x✝.triggersSubjAgr = false

def Phenomena.Case.Studies.Woolford1997.WCase.triggersObjAgr : WCase → Bool

Object agreement: triggered ONLY by OBJ, not by ACC. This asymmetry is evidence that OBJ and ACC are distinct cases: OBJ is assigned by Agr-O (associated with agreement), while ACC is assigned by V/P (no agreement).

Equations

• Phenomena.Case.Studies.Woolford1997.WCase.obj.triggersObjAgr = true
• x✝.triggersObjAgr = false

def Phenomena.Case.Studies.Woolford1997.maxAcc (nArgs nLexCases : ℕ) : ℕ

The maximum number of structural accusative cases assignable in a clause. Formula: #arguments − #lexical cases − 1 (the −1 is the subject slot). Uses Nat subtraction (saturating at 0).

Equations

• Phenomena.Case.Studies.Woolford1997.maxAcc nArgs nLexCases = nArgs - nLexCases - 1

def Phenomena.Case.Studies.Woolford1997.countAccIn (cases : List WCase) : ℕ

Count ACC cases in a list of case assignments.

Equations

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

def Phenomena.Case.Studies.Woolford1997.countLexIn (cases : List WCase) : ℕ

Count lexical cases in a list of case assignments.

Equations

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

def Phenomena.Case.Studies.Woolford1997.generalization19 (subject goal : WCase) : Bool

Generalization (19): a lexically Cased subject cannot be followed by a structural accusative object. Under the weak interpretation, this applies to the thematically highest object (goal > theme).

Equations

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

theorem Phenomena.Case.Studies.Woolford1997.gen19_transitive_erg : generalization19 WCase.erg WCase.obj = true

Generalization (19) holds for all allowed transitive patterns: ERG (lexical) subject → object is OBJ, not ACC.

theorem Phenomena.Case.Studies.Woolford1997.gen19_transitive_nom : generalization19 WCase.nom WCase.acc = true

Generalization (19) is vacuously satisfied for NOM subjects.

def Phenomena.Case.Studies.Woolford1997.generalization19_strong (subject : WCase) (objects : List WCase) : Bool

The strong interpretation of generalization (19) would block ACC on ALL objects when the subject is lexical.

Equations

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

theorem Phenomena.Case.Studies.Woolford1997.strong_interpretation_too_restrictive : generalization19_strong WCase.erg [WCase.obj, WCase.acc] = false

The strong interpretation incorrectly prohibits ERG-OBJ-ACC (paper's (22A.3)), which is an attested Nez Perce ditransitive pattern. The goal gets OBJ (per weak gen (19)), but the theme can still get ACC. The paper argues for the weak interpretation on these grounds.

theorem Phenomena.Case.Studies.Woolford1997.weak_allows_erg_obj_acc : generalization19 WCase.erg WCase.obj = true

The weak interpretation correctly allows ERG-OBJ-ACC: it only checks the goal (highest object), which is OBJ, not ACC.

structure Phenomena.Case.Studies.Woolford1997.TransPattern : Type

A transitive pattern: subject case + object case.

• subject : WCase
• object : WCase

def Phenomena.Case.Studies.Woolford1997.instDecidableEqTransPattern.decEq (x✝ x✝¹ : TransPattern) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Case.Studies.Woolford1997.instDecidableEqTransPattern : DecidableEq TransPattern

Equations

• Phenomena.Case.Studies.Woolford1997.instDecidableEqTransPattern = Phenomena.Case.Studies.Woolford1997.instDecidableEqTransPattern.decEq

def Phenomena.Case.Studies.Woolford1997.instBEqTransPattern.beq : TransPattern → TransPattern → Bool

Equations

• Phenomena.Case.Studies.Woolford1997.instBEqTransPattern.beq { subject := a, object := a_1 } { subject := b, object := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Case.Studies.Woolford1997.instBEqTransPattern.beq x✝¹ x✝ = false

instance Phenomena.Case.Studies.Woolford1997.instBEqTransPattern : BEq TransPattern

Equations

• Phenomena.Case.Studies.Woolford1997.instBEqTransPattern = { beq := Phenomena.Case.Studies.Woolford1997.instBEqTransPattern.beq }

def Phenomena.Case.Studies.Woolford1997.instReprTransPattern.repr : TransPattern → ℕ → Std.Format

Equations

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

instance Phenomena.Case.Studies.Woolford1997.instReprTransPattern : Repr TransPattern

Equations

• Phenomena.Case.Studies.Woolford1997.instReprTransPattern = { reprPrec := Phenomena.Case.Studies.Woolford1997.instReprTransPattern.repr }

def Phenomena.Case.Studies.Woolford1997.npTransAllowed : List TransPattern

The two allowed transitive patterns in Nez Perce (paper's (16A)).

• NOM subject + ACC object (structural subject, structural object)
• ERG subject + OBJ object (lexical subject, structural object)

Equations

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

def Phenomena.Case.Studies.Woolford1997.npTransProhibited : List TransPattern

The two prohibited transitive patterns (paper's (16B)).

• *NOM + OBJ: NOM subject should pair with ACC, not OBJ
• *ERG + ACC: blocked by generalization (19)

Equations

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

def Phenomena.Case.Studies.Woolford1997.predictTransitive (p : TransPattern) : Bool

Predict whether a transitive pattern is allowed. Structural subject (NOM) → object is ACC. Lexical subject (ERG) → object is OBJ (generalization (19) blocks ACC).

Equations

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

structure Phenomena.Case.Studies.Woolford1997.DitransPattern : Type

A ditransitive pattern: subject + goal (higher object) + theme (lower object). The thematic hierarchy (goal > theme) matters for generalization (19): a lexical subject blocks structural accusative on the goal (highest object), not the theme.

• subject : WCase
• goal : WCase
• theme : WCase

def Phenomena.Case.Studies.Woolford1997.instDecidableEqDitransPattern.decEq (x✝ x✝¹ : DitransPattern) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Case.Studies.Woolford1997.instDecidableEqDitransPattern : DecidableEq DitransPattern

Equations

• Phenomena.Case.Studies.Woolford1997.instDecidableEqDitransPattern = Phenomena.Case.Studies.Woolford1997.instDecidableEqDitransPattern.decEq

instance Phenomena.Case.Studies.Woolford1997.instBEqDitransPattern : BEq DitransPattern

Equations

• Phenomena.Case.Studies.Woolford1997.instBEqDitransPattern = { beq := Phenomena.Case.Studies.Woolford1997.instBEqDitransPattern.beq }

def Phenomena.Case.Studies.Woolford1997.instBEqDitransPattern.beq : DitransPattern → DitransPattern → Bool

Equations

• Phenomena.Case.Studies.Woolford1997.instBEqDitransPattern.beq { subject := a, goal := a_1, theme := a_2 } { subject := b, goal := b_1, theme := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Phenomena.Case.Studies.Woolford1997.instBEqDitransPattern.beq x✝¹ x✝ = false

instance Phenomena.Case.Studies.Woolford1997.instReprDitransPattern : Repr DitransPattern

Equations

• Phenomena.Case.Studies.Woolford1997.instReprDitransPattern = { reprPrec := Phenomena.Case.Studies.Woolford1997.instReprDitransPattern.repr }

def Phenomena.Case.Studies.Woolford1997.instReprDitransPattern.repr : DitransPattern → ℕ → Std.Format

Equations

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

def Phenomena.Case.Studies.Woolford1997.npDitransAllowed : List DitransPattern

The four allowed ditransitive patterns in Nez Perce (paper's (22A)). Columns are Agent, Goal, Theme following the paper's labels.

Equations

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

def Phenomena.Case.Studies.Woolford1997.npDitransProhibited : List DitransPattern

The eight prohibited ditransitive patterns (paper's (22B)).

Equations

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

def Phenomena.Case.Studies.Woolford1997.predictDitransitive (p : DitransPattern) : Bool

Predict whether a ditransitive pattern is allowed. Encodes the Max. Acc. formula, structural constraints on OBJ, and generalization (19).

Equations

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

theorem Phenomena.Case.Studies.Woolford1997.trans_allowed_predicted : npTransAllowed.all predictTransitive = true

All allowed transitive patterns are predicted as allowed.

theorem Phenomena.Case.Studies.Woolford1997.trans_prohibited_predicted : (npTransProhibited.all fun (p : TransPattern) => !predictTransitive p) = true

All prohibited transitive patterns are predicted as prohibited.

theorem Phenomena.Case.Studies.Woolford1997.trans_disjoint : (npTransAllowed.all fun (p : TransPattern) => npTransProhibited.all fun (x : TransPattern) => x != p) = true

The allowed/prohibited lists are disjoint.

theorem Phenomena.Case.Studies.Woolford1997.trans_complete : npTransAllowed.length + npTransProhibited.length = 4

The allowed/prohibited lists cover all NOM/ERG × ACC/OBJ combinations.

theorem Phenomena.Case.Studies.Woolford1997.trans_nom_maxAcc : maxAcc 2 0 = 1

maxAcc for transitives: NOM subject → 1 ACC slot.

theorem Phenomena.Case.Studies.Woolford1997.trans_erg_maxAcc : maxAcc 2 1 = 0

maxAcc for transitives: ERG subject → 0 ACC slots.

theorem Phenomena.Case.Studies.Woolford1997.ditrans_allowed_predicted : npDitransAllowed.all predictDitransitive = true

All allowed ditransitive patterns are predicted.

theorem Phenomena.Case.Studies.Woolford1997.ditrans_prohibited_predicted : (npDitransProhibited.all fun (p : DitransPattern) => !predictDitransitive p) = true

All prohibited ditransitive patterns are rejected.

theorem Phenomena.Case.Studies.Woolford1997.ditrans_disjoint : (npDitransAllowed.all fun (p : DitransPattern) => npDitransProhibited.all fun (x : DitransPattern) => x != p) = true

The allowed/prohibited lists are disjoint.

theorem Phenomena.Case.Studies.Woolford1997.ditrans_complete : npDitransAllowed.length + npDitransProhibited.length = 12

The allowed/prohibited lists cover all 12 NOM/ERG × {ACC,OBJ,DAT}² patterns (excluding DAT-DAT which never arises).

theorem Phenomena.Case.Studies.Woolford1997.ditrans_erg_maxAcc : maxAcc 3 1 = 1

maxAcc for ditransitives: ERG subject, no DAT → 1 ACC slot.

theorem Phenomena.Case.Studies.Woolford1997.ditrans_nom_maxAcc : maxAcc 3 0 = 2

maxAcc for ditransitives: NOM subject → 2 ACC slots.

theorem Phenomena.Case.Studies.Woolford1997.ditrans_erg_dat_maxAcc : maxAcc 3 2 = 0

maxAcc for ditransitives: ERG + DAT → 0 ACC slots.

theorem Phenomena.Case.Studies.Woolford1997.erg_is_lexical : WCase.erg.kind = CaseKind.lexical

ERG is lexical (inherent), not structural.

theorem Phenomena.Case.Studies.Woolford1997.nom_is_structural : WCase.nom.kind = CaseKind.structural

NOM is structural.

theorem Phenomena.Case.Studies.Woolford1997.erg_triggers_subj_agr : WCase.erg.triggersSubjAgr = true

ERG subjects trigger subject agreement (not ergative agreement).

theorem Phenomena.Case.Studies.Woolford1997.nom_triggers_subj_agr : WCase.nom.triggersSubjAgr = true

NOM subjects trigger subject agreement.

theorem Phenomena.Case.Studies.Woolford1997.acc_no_obj_agr : WCase.acc.triggersObjAgr = false

ACC does NOT trigger object agreement.

theorem Phenomena.Case.Studies.Woolford1997.obj_triggers_obj_agr : WCase.obj.triggersObjAgr = true

OBJ triggers object agreement.

theorem Phenomena.Case.Studies.Woolford1997.agreement_is_nom_acc : WCase.nom.triggersSubjAgr = WCase.erg.triggersSubjAgr

Agreement is subject-object, not ergative-absolutive: both NOM and ERG trigger the SAME (subject) agreement.

theorem Phenomena.Case.Studies.Woolford1997.obj_acc_agreement_differ : WCase.obj.triggersObjAgr ≠ WCase.acc.triggersObjAgr

OBJ and ACC differ in agreement properties: OBJ triggers object agreement, ACC does not. This justifies treating them as distinct cases and reflects their different structural sources (Agr-O vs V/P).

theorem Phenomena.Case.Studies.Woolford1997.intransitive_maxAcc : maxAcc 1 0 = 0

Intransitives: 1 argument, 0 lexical → maxAcc = 0. The sole argument gets NOM (structural from Agr-S).

theorem Phenomena.Case.Studies.Woolford1997.burzio_from_maxAcc : maxAcc 1 0 = 0 ∧ maxAcc 2 1 = 0 ∧ maxAcc 2 0 = 1

Burzio's generalization as a corollary of the Max. Acc. formula. @cite{woolford-1997} argues that three apparently separate generalizations are all instances of the Max. Acc. formula: (i) No verb assigns structural ACC to its subject (the −1 term). (ii) A verb without an external subject cannot assign ACC (Burzio's generalization): 1 arg, 0 lexical → maxAcc = 0. (iii) A lexically Cased subject blocks ACC on the highest object (generalization (19)): 2 args, 1 lexical → maxAcc = 0. The Max. Acc. formula unifies all three.

inductive Phenomena.Case.Studies.Woolford1997.LexAssignment : Type

Whether a language assigns ERG obligatorily or optionally.

• obligatory : LexAssignment
• optional : LexAssignment

instance Phenomena.Case.Studies.Woolford1997.instDecidableEqLexAssignment : DecidableEq LexAssignment

Equations

• Phenomena.Case.Studies.Woolford1997.instDecidableEqLexAssignment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Case.Studies.Woolford1997.instBEqLexAssignment : BEq LexAssignment

Equations

• Phenomena.Case.Studies.Woolford1997.instBEqLexAssignment = { beq := Phenomena.Case.Studies.Woolford1997.instBEqLexAssignment.beq }

def Phenomena.Case.Studies.Woolford1997.instBEqLexAssignment.beq : LexAssignment → LexAssignment → Bool

Equations

• Phenomena.Case.Studies.Woolford1997.instBEqLexAssignment.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Case.Studies.Woolford1997.instReprLexAssignment.repr : LexAssignment → ℕ → Std.Format

Equations

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

instance Phenomena.Case.Studies.Woolford1997.instReprLexAssignment : Repr LexAssignment

Equations

• Phenomena.Case.Studies.Woolford1997.instReprLexAssignment = { reprPrec := Phenomena.Case.Studies.Woolford1997.instReprLexAssignment.repr }

structure Phenomena.Case.Studies.Woolford1997.LexParams : Type

Language parameters for a three- or four-way system. The range of Case patterns a language allows follows from whether verbs assign ERG and DAT obligatorily or optionally.

• ergAssignment : LexAssignment
• datAssignment : LexAssignment

def Phenomena.Case.Studies.Woolford1997.instReprLexParams.repr : LexParams → ℕ → Std.Format

Equations

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

instance Phenomena.Case.Studies.Woolford1997.instReprLexParams : Repr LexParams

Equations

• Phenomena.Case.Studies.Woolford1997.instReprLexParams = { reprPrec := Phenomena.Case.Studies.Woolford1997.instReprLexParams.repr }

def Phenomena.Case.Studies.Woolford1997.nezPerce : LexParams

Nez Perce: optional ERG, optional DAT.

Equations

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

def Phenomena.Case.Studies.Woolford1997.thangu : LexParams

Thangu: obligatory ERG, obligatory DAT (three-way system: no ACC surfaces).

Equations

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

def Phenomena.Case.Studies.Woolford1997.kalkatungu : LexParams

Kalkatungu: obligatory ERG, optional DAT (four-way system like Nez Perce, but no nominative-accusative pattern since ERG is always assigned).

Equations

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

def Phenomena.Case.Studies.Woolford1997.availableTransPatterns (params : LexParams) : List TransPattern

Predict which transitive patterns are available given language parameters. Obligatory ERG → only ERG-OBJ (no NOM-ACC). Optional ERG → both NOM-ACC and ERG-OBJ.

Equations

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

def Phenomena.Case.Studies.Woolford1997.availableDitransPatterns (params : LexParams) : List DitransPattern

Predict which ditransitive patterns are available given language parameters. The interaction of ERG and DAT optionality determines the full set.

Equations

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

theorem Phenomena.Case.Studies.Woolford1997.np_trans_from_params : availableTransPatterns nezPerce = npTransAllowed

Nez Perce (optional ERG): both transitive patterns available. The predicted patterns match the attested data exactly.

theorem Phenomena.Case.Studies.Woolford1997.np_ditrans_from_params : availableDitransPatterns nezPerce = npDitransAllowed

Nez Perce ditransitive predictions match the attested patterns.

theorem Phenomena.Case.Studies.Woolford1997.thangu_trans_erg_only : availableTransPatterns thangu = [{ subject := WCase.erg, object := WCase.obj }]

Thangu (obligatory ERG): only ERG-OBJ in transitives.

theorem Phenomena.Case.Studies.Woolford1997.thangu_ditrans_no_acc : availableDitransPatterns thangu = [{ subject := WCase.erg, goal := WCase.dat, theme := WCase.obj }]

Thangu (obligatory ERG + DAT): only ERG-DAT-OBJ in ditransitives. With 2 lexical cases, maxAcc = 3 − 2 − 1 = 0 — no ACC at all.

theorem Phenomena.Case.Studies.Woolford1997.kalkatungu_trans_erg_only : availableTransPatterns kalkatungu = [{ subject := WCase.erg, object := WCase.obj }]

Kalkatungu (obligatory ERG, optional DAT): ERG-OBJ only in transitives (no NOM-ACC pattern since ERG is always assigned).

theorem Phenomena.Case.Studies.Woolford1997.kalkatungu_ditrans : availableDitransPatterns kalkatungu = [{ subject := WCase.erg, goal := WCase.obj, theme := WCase.acc }, { subject := WCase.erg, goal := WCase.dat, theme := WCase.obj }]

Kalkatungu ditransitives: ERG-OBJ-ACC (without DAT) and ERG-DAT-OBJ (with DAT). Unlike Thangu, Kalkatungu's optional DAT allows ACC to appear in ditransitives.

theorem Phenomena.Case.Studies.Woolford1997.all_predicted_trans_valid : ([nezPerce, thangu, kalkatungu].all fun (params : LexParams) => (availableTransPatterns params).all predictTransitive) = true

All predicted patterns are valid: every predicted transitive pattern passes the prediction function.

theorem Phenomena.Case.Studies.Woolford1997.all_predicted_ditrans_valid : ([nezPerce, thangu, kalkatungu].all fun (params : LexParams) => (availableDitransPatterns params).all predictDitransitive) = true

All predicted ditransitive patterns pass the prediction function.

def Phenomena.Case.Studies.Woolford1997.WCase.toCore : WCase → Core.Case

Map Woolford's cases to Core.Case for hierarchy validation. OBJ maps to ACC (both are structural object cases).

Equations

• Phenomena.Case.Studies.Woolford1997.WCase.nom.toCore = Core.Case.nom
• Phenomena.Case.Studies.Woolford1997.WCase.obj.toCore = Core.Case.acc
• Phenomena.Case.Studies.Woolford1997.WCase.acc.toCore = Core.Case.acc
• Phenomena.Case.Studies.Woolford1997.WCase.erg.toCore = Core.Case.erg
• Phenomena.Case.Studies.Woolford1997.WCase.dat.toCore = Core.Case.dat

def Phenomena.Case.Studies.Woolford1997.npInventory : List Core.Case

Nez Perce structural case inventory (NOM + ACC/OBJ + ERG). Under Blake's hierarchy, these are all core cases (rank 6) plus DAT (rank 4), with GEN (rank 5) between.

Equations

• Phenomena.Case.Studies.Woolford1997.npInventory = [Core.Case.nom, Core.Case.acc, Core.Case.erg]

theorem Phenomena.Case.Studies.Woolford1997.np_core_valid : Core.validInventory npInventory = true

The core-case subset is valid per Blake's hierarchy (all at rank 6, no gaps).

def Phenomena.Case.Studies.Woolford1997.npFullInventory : List Core.Case

Full inventory including DAT requires GEN for contiguity.

Equations

• Phenomena.Case.Studies.Woolford1997.npFullInventory = [Core.Case.nom, Core.Case.acc, Core.Case.erg, Core.Case.gen, Core.Case.dat]

theorem Phenomena.Case.Studies.Woolford1997.np_full_valid : Core.validInventory npFullInventory = true

Woolford vs. Baker/Marantz

@cite{woolford-1997} and @cite{baker-2015}/@cite{marantz-1991} make overlapping but distinct predictions. Key agreement: both assign structural ACC in transitives with two caseless NPs. Key disagreement: dependent case has no OBJ/ACC distinction — it assigns a single dependent case (ACC) to the lower NP, regardless of whether the higher NP has lexical case.

def Phenomena.Case.Studies.Woolford1997.WCase.toCaseVal : WCase → Minimalism.CaseVal

Map Woolford's cases to CaseVal for comparison with dependent case.

Equations

• Phenomena.Case.Studies.Woolford1997.WCase.nom.toCaseVal = Minimalism.CaseVal.nom
• Phenomena.Case.Studies.Woolford1997.WCase.obj.toCaseVal = Minimalism.CaseVal.acc
• Phenomena.Case.Studies.Woolford1997.WCase.acc.toCaseVal = Minimalism.CaseVal.acc
• Phenomena.Case.Studies.Woolford1997.WCase.erg.toCaseVal = Minimalism.CaseVal.erg
• Phenomena.Case.Studies.Woolford1997.WCase.dat.toCaseVal = Minimalism.CaseVal.dat

theorem Phenomena.Case.Studies.Woolford1997.agree_on_nom_acc_transitive : have depResult := Minimalism.assignCases Minimalism.CaseLanguageType.accusative [{ label := "subj", lexicalCase := none }, { label := "obj", lexicalCase := none }]; Minimalism.getCaseOf "obj" depResult = some Minimalism.CaseVal.acc ∧ { subject := WCase.nom, object := WCase.acc }.object.toCaseVal = Minimalism.CaseVal.acc

Where Woolford and dependent case agree: in a NOM-ACC transitive, the object gets ACC under both theories.

theorem Phenomena.Case.Studies.Woolford1997.diverge_on_obj_vs_acc : WCase.obj ≠ WCase.acc ∧ WCase.obj.toCaseVal = WCase.acc.toCaseVal

Where they diverge: Woolford distinguishes OBJ from ACC. Under dependent case, both map to the same CaseVal.acc.

theorem Phenomena.Case.Studies.Woolford1997.agreement_asymmetry_is_woolford_specific : WCase.obj.triggersObjAgr = true ∧ WCase.acc.triggersObjAgr = false

Dependent case has no analogue of Woolford's agreement asymmetry: under dependent case, there is one ACC — it either triggers agreement or not. Woolford's two structural object cases explain why some objects trigger agreement (OBJ from Agr-O) and others don't (ACC from V/P).

theorem Phenomena.Case.Studies.Woolford1997.erg_nonstructural : WCase.erg.kind = CaseKind.lexical

ERG is lexical under both theories: Woolford's inherent case and Baker's dependent ergative both treat ERG as non-structural, though the mechanisms differ (θ-role assignment vs. configuration).