Basque Agreement Fragment [Jus24]

[Lak96] [Pre14] [Bla94b]

Basque (isolate) has a rich agreement system where the finite verb indexes up to three arguments: ergative (A), absolutive (S/P), and dative (R). Crucially, object (P/R) agreement is person-conditioned: the verb cross-references 1st/2nd person objects but not 3rd person objects in many constructions.

This is a classic case of differential P indexing conditioned by person prominence: SAP objects are indexed, 3rd person objects are not.

Agreement Paradigm Overview

Argument	Case	Indexed?
A (transitive agent)	ERG	Always
S (intransitive subj)	ABS	Always
P (transitive patient)	ABS	SAP only (differential)

inductive Basque.Agreement.ArgPosition : Type

Argument positions in a Basque clause.

• agent : ArgPosition

  A: transitive agent (ERG)

• patient : ArgPosition

  P: transitive patient (ABS)

• intranS : ArgPosition

  S: intransitive subject (ABS)

@[implicit_reducible]

instance Basque.Agreement.instDecidableEqArgPosition : DecidableEq ArgPosition

Equations

• Basque.Agreement.instDecidableEqArgPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Basque.Agreement.instReprArgPosition.repr : ArgPosition → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Basque.Agreement.instReprArgPosition : Repr ArgPosition

Equations

• Basque.Agreement.instReprArgPosition = { reprPrec := Basque.Agreement.instReprArgPosition.repr }

def Basque.Agreement.pIsIndexed (c : Agreement.Cell) : Bool

Whether a P argument at a given φ-cell is indexed on the verb. Basque cross-references SAP objects (1st/2nd person) but not 3rd person objects in the relevant constructions; A/S arguments are always indexed. Keyed by the canonical φ-cell (Agreement.Cell), so a pronoun's Word.agrCell drives it directly.

Equations

• Basque.Agreement.pIsIndexed c = c.isSAP

def Basque.Agreement.asIsIndexed : Agreement.Cell → Bool

Whether an A/S argument is indexed. Always true — A and S indexing is not differential in Basque.

Equations

• Basque.Agreement.asIsIndexed x✝ = true

theorem Basque.Agreement.sap_objects_indexed : pIsIndexed (Agreement.Cell.pn UD.Person.first UD.Number.Sing) = true ∧ pIsIndexed (Agreement.Cell.pn UD.Person.second UD.Number.Sing) = true ∧ pIsIndexed (Agreement.Cell.pn UD.Person.first UD.Number.Plur) = true ∧ pIsIndexed (Agreement.Cell.pn UD.Person.second UD.Number.Plur) = true

SAP objects are indexed.

theorem Basque.Agreement.third_objects_not_indexed : pIsIndexed (Agreement.Cell.pn UD.Person.third UD.Number.Sing) = false ∧ pIsIndexed (Agreement.Cell.pn UD.Person.third UD.Number.Plur) = false

3rd person objects are NOT indexed.

theorem Basque.Agreement.p_indexing_differential : Agreement.Cell.pnCells.any pIsIndexed = true ∧ (!decide (Agreement.Cell.pnCells.all pIsIndexed = true)) = true

P indexing is differential: some φ-cells indexed, some not.

theorem Basque.Agreement.as_indexing_uniform : Agreement.Cell.pnCells.all asIsIndexed = true

A/S indexing is NOT differential: all φ-cells indexed.

def Basque.Agreement.agreementCaseInventory : Finset Case

Basque agreement-relevant case inventory: {ERG, ABS, DAT}. The full Basque case system has ~12 cases (ERG, ABS, DAT, GEN, LOC, ABL, ALL, INST, COM, PERL, BEN, and more), but the agreement system only distinguishes these three.

Equations

• Basque.Agreement.agreementCaseInventory = {Case.erg, Case.abs, Case.dat}

def Basque.Agreement.fullCaseInventory : Finset Case

The full Basque case inventory (representative selection).

Equations

• Basque.Agreement.fullCaseInventory = {Case.erg, Case.abs, Case.gen, Case.dat, Case.loc, Case.abl, Case.all, Case.inst, Case.com, Case.perl, Case.ben}