@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 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 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

@[implicit_reducible]

instance Woolford1997.instDecidableEqWCase : DecidableEq WCase

Equations

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

@[implicit_reducible]

instance Woolford1997.instReprWCase : Repr WCase

Equations

• Woolford1997.instReprWCase = { reprPrec := Woolford1997.instReprWCase.repr }

def Woolford1997.instReprWCase.repr : WCase → ℕ → Std.Format

Equations

• Woolford1997.instReprWCase.repr Woolford1997.WCase.nom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Woolford1997.WCase.nom")).group prec✝
• Woolford1997.instReprWCase.repr Woolford1997.WCase.obj prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Woolford1997.WCase.obj")).group prec✝
• Woolford1997.instReprWCase.repr Woolford1997.WCase.acc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Woolford1997.WCase.acc")).group prec✝
• Woolford1997.instReprWCase.repr Woolford1997.WCase.erg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Woolford1997.WCase.erg")).group prec✝
• Woolford1997.instReprWCase.repr Woolford1997.WCase.dat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Woolford1997.WCase.dat")).group prec✝

inductive Woolford1997.CaseKind : Type

Structural vs lexical classification.

• structural : CaseKind
• lexical : CaseKind

@[implicit_reducible]

instance Woolford1997.instDecidableEqCaseKind : DecidableEq CaseKind

Equations

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

def Woolford1997.instReprCaseKind.repr : CaseKind → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Woolford1997.instReprCaseKind : Repr CaseKind

Equations

• Woolford1997.instReprCaseKind = { reprPrec := Woolford1997.instReprCaseKind.repr }

def Woolford1997.WCase.kind : WCase → CaseKind

Each case's structural/lexical classification.

Equations

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

def 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

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

def 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

• Woolford1997.WCase.obj.triggersObjAgr = true
• x✝.triggersObjAgr = false

def 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

• Woolford1997.maxAcc nArgs nLexCases = nArgs - nLexCases - 1

def Woolford1997.countAccIn (cases : List WCase) : ℕ

Count ACC cases in a list of case assignments.

Equations

• Woolford1997.countAccIn cases = (List.filter (fun (x : Woolford1997.WCase) => x == Woolford1997.WCase.acc) cases).length

def Woolford1997.countLexIn (cases : List WCase) : ℕ

Count lexical cases in a list of case assignments.

Equations

• Woolford1997.countLexIn cases = (List.filter (fun (c : Woolford1997.WCase) => c.kind == Woolford1997.CaseKind.lexical) cases).length

def 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

• Woolford1997.generalization19 subject goal = (subject.kind != Woolford1997.CaseKind.lexical || goal != Woolford1997.WCase.acc)

theorem 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 Woolford1997.gen19_transitive_nom : generalization19 WCase.nom WCase.acc = true

Generalization (19) is vacuously satisfied for NOM subjects.

def 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

• Woolford1997.generalization19_strong subject objects = (subject.kind != Woolford1997.CaseKind.lexical || objects.all fun (x : Woolford1997.WCase) => x != Woolford1997.WCase.acc)

theorem 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 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 Woolford1997.TransPattern : Type

A transitive pattern: subject case + object case.

• subject : WCase
• object : WCase

@[implicit_reducible]

instance Woolford1997.instDecidableEqTransPattern : DecidableEq TransPattern

Equations

• Woolford1997.instDecidableEqTransPattern = Woolford1997.instDecidableEqTransPattern.decEq

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

Equations

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

def Woolford1997.instReprTransPattern.repr : TransPattern → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Woolford1997.instReprTransPattern : Repr TransPattern

Equations

• Woolford1997.instReprTransPattern = { reprPrec := Woolford1997.instReprTransPattern.repr }

def 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

• Woolford1997.npTransAllowed = [{ subject := Woolford1997.WCase.nom, object := Woolford1997.WCase.acc }, { subject := Woolford1997.WCase.erg, object := Woolford1997.WCase.obj }]

def 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

• Woolford1997.npTransProhibited = [{ subject := Woolford1997.WCase.nom, object := Woolford1997.WCase.obj }, { subject := Woolford1997.WCase.erg, object := Woolford1997.WCase.acc }]

def 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 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 Woolford1997.instDecidableEqDitransPattern.decEq (x✝ x✝¹ : DitransPattern) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Woolford1997.instDecidableEqDitransPattern : DecidableEq DitransPattern

Equations

• Woolford1997.instDecidableEqDitransPattern = Woolford1997.instDecidableEqDitransPattern.decEq

@[implicit_reducible]

instance Woolford1997.instReprDitransPattern : Repr DitransPattern

Equations

• Woolford1997.instReprDitransPattern = { reprPrec := Woolford1997.instReprDitransPattern.repr }

def Woolford1997.instReprDitransPattern.repr : DitransPattern → ℕ → Std.Format

Equations

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

def 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 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 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 Woolford1997.trans_allowed_predicted : npTransAllowed.all predictTransitive = true

All allowed transitive patterns are predicted as allowed.

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

All prohibited transitive patterns are predicted as prohibited.

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

The allowed/prohibited lists are disjoint.

theorem Woolford1997.trans_complete : npTransAllowed.length + npTransProhibited.length = 4

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

theorem Woolford1997.trans_nom_maxAcc : maxAcc 2 0 = 1

maxAcc for transitives: NOM subject → 1 ACC slot.

theorem Woolford1997.trans_erg_maxAcc : maxAcc 2 1 = 0

maxAcc for transitives: ERG subject → 0 ACC slots.

theorem Woolford1997.ditrans_allowed_predicted : npDitransAllowed.all predictDitransitive = true

All allowed ditransitive patterns are predicted.

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

All prohibited ditransitive patterns are rejected.

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

The allowed/prohibited lists are disjoint.

theorem 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 Woolford1997.ditrans_erg_maxAcc : maxAcc 3 1 = 1

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

theorem Woolford1997.ditrans_nom_maxAcc : maxAcc 3 0 = 2

maxAcc for ditransitives: NOM subject → 2 ACC slots.

theorem Woolford1997.ditrans_erg_dat_maxAcc : maxAcc 3 2 = 0

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

theorem Woolford1997.erg_is_lexical : WCase.erg.kind = CaseKind.lexical

ERG is lexical (inherent), not structural.

theorem Woolford1997.nom_is_structural : WCase.nom.kind = CaseKind.structural

NOM is structural.

theorem Woolford1997.erg_triggers_subj_agr : WCase.erg.triggersSubjAgr = true

ERG subjects trigger subject agreement (not ergative agreement).

theorem Woolford1997.nom_triggers_subj_agr : WCase.nom.triggersSubjAgr = true

NOM subjects trigger subject agreement.

theorem Woolford1997.acc_no_obj_agr : WCase.acc.triggersObjAgr = false

ACC does NOT trigger object agreement.

theorem Woolford1997.obj_triggers_obj_agr : WCase.obj.triggersObjAgr = true

OBJ triggers object agreement.

theorem 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 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 Woolford1997.intransitive_maxAcc : maxAcc 1 0 = 0

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

theorem 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 Woolford1997.LexAssignment : Type

Whether a language assigns ERG obligatorily or optionally.

• obligatory : LexAssignment
• optional : LexAssignment

@[implicit_reducible]

instance Woolford1997.instDecidableEqLexAssignment : DecidableEq LexAssignment

Equations

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

def Woolford1997.instReprLexAssignment.repr : LexAssignment → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Woolford1997.instReprLexAssignment : Repr LexAssignment

Equations

• Woolford1997.instReprLexAssignment = { reprPrec := Woolford1997.instReprLexAssignment.repr }

structure 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

@[implicit_reducible]

instance Woolford1997.instReprLexParams : Repr LexParams

Equations

• Woolford1997.instReprLexParams = { reprPrec := Woolford1997.instReprLexParams.repr }

def Woolford1997.instReprLexParams.repr : LexParams → ℕ → Std.Format

Equations

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

def Woolford1997.nezPerce : LexParams

Nez Perce: optional ERG, optional DAT.

Equations

• Woolford1997.nezPerce = { ergAssignment := Woolford1997.LexAssignment.optional, datAssignment := Woolford1997.LexAssignment.optional }

def Woolford1997.thangu : LexParams

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

Equations

• Woolford1997.thangu = { ergAssignment := Woolford1997.LexAssignment.obligatory, datAssignment := Woolford1997.LexAssignment.obligatory }

def 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

• Woolford1997.kalkatungu = { ergAssignment := Woolford1997.LexAssignment.obligatory, datAssignment := Woolford1997.LexAssignment.optional }

def 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 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 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 Woolford1997.np_ditrans_from_params : availableDitransPatterns nezPerce = npDitransAllowed

Nez Perce ditransitive predictions match the attested patterns.

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

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

theorem 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 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 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 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 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 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

• Woolford1997.WCase.nom.toCore = UD.Case.nom
• Woolford1997.WCase.obj.toCore = UD.Case.acc
• Woolford1997.WCase.acc.toCore = UD.Case.acc
• Woolford1997.WCase.erg.toCore = UD.Case.erg
• Woolford1997.WCase.dat.toCore = UD.Case.dat

def Woolford1997.npInventory : Finset 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

• Woolford1997.npInventory = {UD.Case.nom, UD.Case.acc, UD.Case.erg}

theorem Woolford1997.np_core_valid : Core.Case.IsValidInventory npInventory

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

def Woolford1997.npFullInventory : Finset Core.Case

Full inventory including DAT requires GEN for contiguity.

Equations

• Woolford1997.npFullInventory = {UD.Case.nom, UD.Case.acc, UD.Case.erg, UD.Case.gen, UD.Case.dat}

theorem Woolford1997.np_full_valid : Core.Case.IsValidInventory npFullInventory

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 Woolford1997.WCase.toCoreCase : WCase → Core.Case

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

Equations

• Woolford1997.WCase.nom.toCoreCase = UD.Case.nom
• Woolford1997.WCase.obj.toCoreCase = UD.Case.acc
• Woolford1997.WCase.acc.toCoreCase = UD.Case.acc
• Woolford1997.WCase.erg.toCoreCase = UD.Case.erg
• Woolford1997.WCase.dat.toCoreCase = UD.Case.dat

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

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

theorem Woolford1997.diverge_on_obj_vs_acc : WCase.obj ≠ WCase.acc ∧ WCase.obj.toCoreCase = WCase.acc.toCoreCase

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

theorem 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 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).