Dependent case by Agree: ergative in Shawi

Clem and Deal derive the Shawi ergative suffix -ri from Agree. The probe on v is Deal's strictly descending grammar, [INT:φ, SAT:SPKR] with [PART] interacting dynamically: it Agrees with a visible object and then, when the person hierarchy permits, with the subject, and goal flagging carries the object's φ-features onto the subject, where -ri realizes the φ root of the flag and object agreement on the subject realizes the rest. Ergative is thus the case of a probe's second goal, and its distribution over Table 4 follows from the run of the probe over the goals v can see: a high object and then the subject, or the subject alone when a third-person object stays inside the categorizing v phase. Section 5 generalizes: a probe on v yields ergative and a probe on T accusative, the person split of a language is the grammar of its probe, and so global case splits range over the hierarchy effects of agreement (Tables 6–7).

Main definitions

• flag, DependentCase: the goal flag a probe deposits on the last goal it reaches, and dependent case as a flag carrying an earlier goal's φ-features.
• positions, goals: the positions open to a Shawi object by its person and surface syntax, and the goals v meets for an object in either position.
• Ergative, marking: ergative on the subject, and Table 4's obligatory, optional and impossible cells.
• oagrOnS: object agreement on the subject, the object-agreement exponent of the flag.
• Locus: the probe on v or on T, ordering the goals of a transitive clause.

Main results

• dependentCase_iff_licit: with two goals, dependent case on the second is Deal's licit Agree with both, so the PCC typology transfers to case splits.
• halt_of_spkr_object, narrow_of_part_object, flag_of_third_object, flag_of_low_object: the derivations (15), (17) and (19), (22), and (24) behind Table 4.
• table4, marking_optional_iff, ergative_of_fronted_or_dropped: the distribution of ergative, optionality as the structural ambiguity of third-person objects, and obligatory ergative with a fronted or dropped object.
• oagrOnS_isSome: object agreement on the subject only under ergative, and off the diagonal only for a first-person subject and a second-person object.
• rule1_overgenerates, no_1_3_2_hierarchy: the configurational rule fires where Shawi has no ergative, and no grammar of the probe space yields a 1>3>2 hierarchy.
• dependentCase_noPCC, dependentCase_strong_iff, dependentCase_weak_iff, dependentCase_sd_iff, dependentCase_sd_off_diagonal_iff: Tables 6–7, the four splits in either locus.

Implementation notes

• Table 4 has no reflexive rows. The mechanism predicts ergative at 2→2 and none at 1→1, where a first-person object satisfies the probe, so the paper's "at least as high as" and its claim that object agreement on the subject is overt only at 1→2 are stated here off the diagonal; the paper expects the anaphor agreement effect to interfere there (§5.3).
• Locators are the paper's example and table numbers.

References

• [CD26]
• [Dea24]
• [BR09]
• [Bak15]
• [BS24a]
• [BV10]
• [Dea10]
• [Cle19]
• [Val11]
• [Mas03]
• [vU15]

Dependent case as the flag of a second goal

def ClemDeal2024.flag (g : Deal2024.Grammar) (goals : List Person) : Option (List Person)

A probe of grammar g walking goals in order deposits a flag on the last of them, none if it never Agrees with that goal and otherwise the goals it Agreed with before, whose φ-features it carries and transfers there with its own ((31)).

Equations

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

def ClemDeal2024.DependentCase (g : Deal2024.Grammar) (goals : List Person) : Prop

A probe assigns dependent case when the last goal's flag carries the φ-features of an earlier goal, the structure a dependent-case vocabulary item realizes ((31), (34), (43)).

Equations

• ClemDeal2024.DependentCase g goals = ∃ (p : Person) (l : List Person), ClemDeal2024.flag g goals = some (p :: l)

@[instance_reducible]

instance ClemDeal2024.instDecidableDependentCase (g : Deal2024.Grammar) (goals : List Person) : Decidable (DependentCase g goals)

Equations

• ClemDeal2024.instDecidableDependentCase g goals = match h : ClemDeal2024.flag g goals with | some (p :: l) => isTrue ⋯ | some [] => isFalse ⋯ | none => isFalse ⋯

theorem ClemDeal2024.dependentCase_iff_licit (g : Deal2024.Grammar) (g₁ g₂ : Person) : DependentCase g [g₁, g₂] ↔ Deal2024.Licit g { high := g₂, low := g₁ }

With two goals, dependent case on the second is [Dea24]'s licit Agree with both, the probe meeting the first goal in the direct-object slot and the second in the indirect-object slot.

Shawi: the v probe and the position of the object

inductive ClemDeal2024.ObjectPosition : Type

A Shawi object sits in the specifier of the categorizing v, above the phase boundary and visible to the v probe, or in its base position inside that phase, invisible to it ((30)).

• high : ObjectPosition
• low : ObjectPosition

@[instance_reducible]

instance ClemDeal2024.instDecidableEqObjectPosition : DecidableEq ObjectPosition

Equations

• ClemDeal2024.instDecidableEqObjectPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ClemDeal2024.instReprObjectPosition : Repr ObjectPosition

Equations

• ClemDeal2024.instReprObjectPosition = { reprPrec := ClemDeal2024.instReprObjectPosition.repr }

def ClemDeal2024.instReprObjectPosition.repr : ObjectPosition → ℕ → Std.Format

Equations

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

inductive ClemDeal2024.ObjectSyntax : Type

On the surface an object follows the subject (SOV or SVO), is fronted over it (OSV), or is dropped.

• inSitu : ObjectSyntax
• fronted : ObjectSyntax
• dropped : ObjectSyntax

@[instance_reducible]

instance ClemDeal2024.instDecidableEqObjectSyntax : DecidableEq ObjectSyntax

Equations

• ClemDeal2024.instDecidableEqObjectSyntax x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ClemDeal2024.instReprObjectSyntax.repr : ObjectSyntax → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ClemDeal2024.instReprObjectSyntax : Repr ObjectSyntax

Equations

• ClemDeal2024.instReprObjectSyntax = { reprPrec := ClemDeal2024.instReprObjectSyntax.repr }

def ClemDeal2024.positions (p : Person) : ObjectSyntax → List ObjectPosition

An object of person p with surface syntax x may occupy these positions (§3.2). Local persons move to the high position obligatorily and third persons optionally, and fronting over the subject ((26b)) and pro-drop ((21a), as in Dinka [vU15]) require it.

Equations

• ClemDeal2024.positions p ClemDeal2024.ObjectSyntax.inSitu = if p.IsSAP then [ClemDeal2024.ObjectPosition.high] else [ClemDeal2024.ObjectPosition.high, ClemDeal2024.ObjectPosition.low]
• ClemDeal2024.positions p ClemDeal2024.ObjectSyntax.fronted = [ClemDeal2024.ObjectPosition.high]
• ClemDeal2024.positions p ClemDeal2024.ObjectSyntax.dropped = [ClemDeal2024.ObjectPosition.high]

def ClemDeal2024.goals (subj obj : Person) : ObjectPosition → List Person

The v probe meets a high object and then the subject ((22)), or the subject alone when the object is low or absent ((24)), by the cyclic expansion of [BR09] ((13)).

Equations

• ClemDeal2024.goals subj obj ClemDeal2024.ObjectPosition.high = [obj, subj]
• ClemDeal2024.goals subj obj ClemDeal2024.ObjectPosition.low = [subj]

def ClemDeal2024.Ergative (subj obj : Person) (pos : ObjectPosition) : Prop

The subject is ergative when v, with [INT:φ, SAT:SPKR] and [PART] interacting dynamically (Deal2024.strictlyDescending, §3.1), Agrees with it as its second goal; -ri realizes the φ root of the flag it leaves there ((34)).

Equations

• ClemDeal2024.Ergative subj obj pos = ClemDeal2024.DependentCase Deal2024.strictlyDescending (ClemDeal2024.goals subj obj pos)

@[instance_reducible]

instance ClemDeal2024.instDecidableErgative (subj obj : Person) (pos : ObjectPosition) : Decidable (Ergative subj obj pos)

Equations

• ClemDeal2024.instDecidableErgative subj obj pos = ClemDeal2024.instDecidableErgative._aux_1 subj obj pos

The derivations behind Table 4

theorem ClemDeal2024.halt_of_spkr_object (subj obj : Person) (h : Minimalist.PersonSegment.speaker ∈ Minimalist.PersonSegment.spec obj) : (Deal2024.runProbe Deal2024.strictlyDescending [obj, subj]).satisfied = true ∧ flag Deal2024.strictlyDescending [obj, subj] = none

A first-person object bears [SPKR] and satisfies the probe, which halts, so the subject is never reached, whatever its person (15).

theorem ClemDeal2024.narrow_of_part_object (subj obj : Person) (h₁ : Minimalist.PersonSegment.speaker ∉ Minimalist.PersonSegment.spec obj) (h₂ : Minimalist.PersonSegment.participant ∈ Minimalist.PersonSegment.spec obj) : (Deal2024.runProbe Deal2024.strictlyDescending [obj, subj]).int = {Minimalist.PersonSegment.pi, Minimalist.PersonSegment.participant} ∧ (flag Deal2024.strictlyDescending [obj, subj] = some [obj] ↔ Minimalist.PersonSegment.participant ∈ Minimalist.PersonSegment.spec subj)

A second-person object lacks [SPKR] but bears [PART], so the probe is not satisfied but narrows to [INT:PART]; it then reaches the subject exactly when the subject bears [PART] ((17), (19)).

theorem ClemDeal2024.flag_of_third_object (subj obj : Person) (h : Minimalist.PersonSegment.participant ∉ Minimalist.PersonSegment.spec obj) : flag Deal2024.strictlyDescending [obj, subj] = some [obj]

A third-person object neither satisfies nor narrows the probe, so the subject is reached whatever its person (22).

theorem ClemDeal2024.flag_of_low_object (subj : Person) : flag Deal2024.strictlyDescending [subj] = some []

With a low or absent object the probe expands and Agrees with the subject alone (24). The subject is Agreed with but is not a second goal, so its flag is empty and there is no ergative ((25)).

theorem ClemDeal2024.not_ergative_low (subj obj : Person) : ¬Ergative subj obj ObjectPosition.low

Table 4

inductive ClemDeal2024.Marking : Type

The three values of a Table 4 cell.

• obligatory : Marking
• optional : Marking
• impossible : Marking

@[instance_reducible]

instance ClemDeal2024.instDecidableEqMarking : DecidableEq Marking

Equations

• ClemDeal2024.instDecidableEqMarking x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance ClemDeal2024.instReprMarking : Repr Marking

Equations

• ClemDeal2024.instReprMarking = { reprPrec := ClemDeal2024.instReprMarking.repr }

def ClemDeal2024.instReprMarking.repr : Marking → ℕ → Std.Format

Equations

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

def ClemDeal2024.marking (subj obj : Person) : Marking

Table 4's cell for a subject and an in-situ object records whether the subject is ergative in every position open to the object, in some, or in none.

Equations

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

theorem ClemDeal2024.table4 : marking Person.first Person.second = Marking.obligatory ∧ marking Person.first Person.third = Marking.optional ∧ marking Person.second Person.first = Marking.impossible ∧ marking Person.second Person.third = Marking.optional ∧ marking Person.third Person.first = Marking.impossible ∧ marking Person.third Person.second = Marking.impossible ∧ marking Person.third Person.third = Marking.optional

Ergative is obligatory at 1→2, impossible at 2→1, 3→1 and 3→2, and optional with a third-person object, as in Table 4.

theorem ClemDeal2024.marking_optional_iff (subj obj : Person) : marking subj obj = Marking.optional ↔ ¬obj.IsSAP

Optionality is the structural ambiguity of a third-person object ((23) against (24)), a cell being optional exactly when the object may stay low.

theorem ClemDeal2024.ergative_of_fronted_or_dropped (subj : Person) (x : ObjectSyntax) (hx : x ≠ ObjectSyntax.inSitu) (pos : ObjectPosition) : pos ∈ positions Person.third x → Ergative subj Person.third pos

A third-person object fronted over the subject or dropped has moved high, and ergative becomes obligatory ((20)–(21), (26)).

Object agreement on the subject

def ClemDeal2024.oagrOnS (subj obj : Person) (n : Number) (pos : ObjectPosition) : Option String

Object agreement on the subject is the object-agreement exponent of the person the subject's flag carries, with the object's number ((36)), realizing the [PART, v] remainder of the flag once -ri has realized its φ root (§3.3).

Equations

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

theorem ClemDeal2024.oagrOnS_isSome {subj obj : Person} {n : Number} {pos : ObjectPosition} (hne : subj.prominence ≠ obj.prominence) (h : (oagrOnS subj obj n pos).isSome = true) : Ergative subj obj pos ∧ Minimalist.PersonSegment.speaker ∈ Minimalist.PersonSegment.spec subj ∧ obj = Person.second

Object agreement appears on the subject only if the subject is ergative (§2, fn. 7), and, off the diagonal, is overt only for a first-person subject and a second-person object (§3.3), since a third-person object has no exponent and no other pair lets the subject Agree.

theorem ClemDeal2024.oagrOnS_examples : oagrOnS Person.firstExclusive Person.second Number.augmented ObjectPosition.high = some "-((n)ke)ma'" ∧ oagrOnS Person.second Person.firstExclusive Number.minimal ObjectPosition.high = none ∧ Ergative Person.firstExclusive Person.third ObjectPosition.high ∧ oagrOnS Person.firstExclusive Person.third Number.minimal ObjectPosition.high = none

A first-person exclusive augmented subject with a second-person augmented object bears -ri and the object's marker (12), a second-person subject with a first-person object bears neither (11), and a third-person object leaves -ri nothing to accompany (23a).

Configurational rules (§1, §4.1)

theorem ClemDeal2024.rule1_overgenerates : Option.map (fun (x : Case × Case.Mechanism) => x.1) (Case.Valuation.valueOf 0 (DependentCase.assignCases Alignment.AlignmentType.ergative (fun (x : Fin 2) => none) [0, 1])) = some Case.erg ∧ ¬Ergative Person.second Person.first ObjectPosition.high ∧ ¬Ergative Person.third Person.first ObjectPosition.high ∧ ¬Ergative Person.third Person.second ObjectPosition.high

Rule (1) ([Bak15]) values the higher of two caseless NPs in one domain ergative whatever their persons, as DependentCase.assignCases does; Shawi withholds ergative at 2→1, 3→1 and 3→2 with the object in v's domain ((7a–c)).

theorem ClemDeal2024.no_1_3_2_hierarchy (g : Deal2024.Grammar) (h : DependentCase g [Person.second, Person.third]) : DependentCase g [Person.third, Person.second]

No grammar of [Dea24]'s probe space yields a 1>3>2 hierarchy (§4.1). None makes 3→2 a second-goal configuration while 2→3 is not, since a third-person first goal neither satisfies nor narrows the probe. Rule (37) of [BS24a]'s kind, whose hierarchy is stipulated, has no such limit.

The typology of global case splits (§5)

inductive ClemDeal2024.Locus : Type

The probe sits on v, between object and subject, so the object is its first goal and the dependent case of the subject is ergative ((40)), or on T above both, so the subject is first and the dependent case of the object is accusative ((41)).

• v : Locus
• T : Locus

@[instance_reducible]

instance ClemDeal2024.instDecidableEqLocus : DecidableEq Locus

Equations

• ClemDeal2024.instDecidableEqLocus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ClemDeal2024.instReprLocus.repr : Locus → ℕ → Std.Format

Equations

• ClemDeal2024.instReprLocus.repr ClemDeal2024.Locus.v prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ClemDeal2024.Locus.v")).group prec✝
• ClemDeal2024.instReprLocus.repr ClemDeal2024.Locus.T prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ClemDeal2024.Locus.T")).group prec✝

@[instance_reducible]

instance ClemDeal2024.instReprLocus : Repr Locus

Equations

• ClemDeal2024.instReprLocus = { reprPrec := ClemDeal2024.instReprLocus.repr }

def ClemDeal2024.Locus.goals : Locus → Person → Person → List Person

The goals of a transitive clause in the order a probe at l meets them.

Equations

• ClemDeal2024.Locus.v.goals x✝¹ x✝ = [x✝, x✝¹]
• ClemDeal2024.Locus.T.goals x✝¹ x✝ = [x✝¹, x✝]

theorem ClemDeal2024.dependentCase_noPCC (l : Locus) (subj obj : Person) : DependentCase Deal2024.noPCC (l.goals subj obj)

Without a split (§5.1), an insatiable probe with no dynamic interaction Agrees with both arguments whatever their persons, giving ergative on v (Nez Perce [Dea10], Amahuaca [Cle19]) and accusative on T (Sakha, [BV10]).

theorem ClemDeal2024.dependentCase_strong_iff (g₁ g₂ : Person) : DependentCase Deal2024.strong [g₁, g₂] ↔ Minimalist.PersonSegment.participant ∉ Minimalist.PersonSegment.spec g₁

Under the strong PCC of Table 7 there is dependent case iff the first goal is third person, on the subject when the object is third (Shiwilu, [Val11]) and on the object when the subject is third (Yurok).

theorem ClemDeal2024.dependentCase_weak_iff (g₁ g₂ : Person) : DependentCase Deal2024.weak [g₁, g₂] ↔ Minimalist.PersonSegment.participant ∈ Minimalist.PersonSegment.spec g₁ → Minimalist.PersonSegment.participant ∈ Minimalist.PersonSegment.spec g₂

Under the weak PCC of Table 7 there is dependent case unless the first goal is local and the second is third, so on the object except in local→third (Kolyma Yukaghir, [Mas03]).

theorem ClemDeal2024.dependentCase_sd_iff (g₁ g₂ : Person) : DependentCase Deal2024.strictlyDescending [g₁, g₂] ↔ Minimalist.PersonSegment.speaker ∉ Minimalist.PersonSegment.spec g₁ ∧ (Minimalist.PersonSegment.participant ∈ Minimalist.PersonSegment.spec g₁ → Minimalist.PersonSegment.participant ∈ Minimalist.PersonSegment.spec g₂)

Under the strictly descending PCC of Table 7 there is dependent case iff the first goal lacks [SPKR] and the second bears [PART] whenever the first does.

theorem ClemDeal2024.dependentCase_sd_off_diagonal_iff (g₁ g₂ : Person) (h : g₁.prominence ≠ g₂.prominence) : DependentCase Deal2024.strictlyDescending [g₁, g₂] ↔ g₂.prominence > g₁.prominence

Off the diagonal the strictly descending split is the hierarchy 1>2>3, dependent case holding exactly when the second goal outranks the first, the subject over the object with the probe on v (Shawi) and the object over the subject with it on T (Kashmiri, fn. 42).

def ClemDeal2024.kolymaYukaghirAccusative (subj obj : Person) : Option String

In the Kolyma Yukaghir accusative ((52)), -ul realizes [φ, PART] in the object's flag and -gele its φ root, so the form records whether the subject T Agreed with first was a local person.

Equations

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

theorem ClemDeal2024.kolymaYukaghirAccusative_49 : kolymaYukaghirAccusative Person.third Person.first = some "-gele" ∧ kolymaYukaghirAccusative Person.first Person.second = some "-ul" ∧ kolymaYukaghirAccusative Person.first Person.third = none

The accusative is -gele at 3→1 and -ul at 1→2, and there is none at 1→3 (49).