Basque Agreement Fragment @cite{just-2024}

@cite{laka-1996} @cite{preminger-2014} @cite{blake-1994}

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 Fragments.Basque.Agreement.PersonNumber : Type

Person-number combinations in the Basque agreement paradigm.

• p1sg : PersonNumber
• p2sg : PersonNumber
• p3sg : PersonNumber
• p1pl : PersonNumber
• p2pl : PersonNumber
• p3pl : PersonNumber

instance Fragments.Basque.Agreement.instDecidableEqPersonNumber : DecidableEq PersonNumber

Equations

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

def Fragments.Basque.Agreement.instBEqPersonNumber.beq : PersonNumber → PersonNumber → Bool

Equations

• Fragments.Basque.Agreement.instBEqPersonNumber.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Basque.Agreement.instBEqPersonNumber : BEq PersonNumber

Equations

• Fragments.Basque.Agreement.instBEqPersonNumber = { beq := Fragments.Basque.Agreement.instBEqPersonNumber.beq }

def Fragments.Basque.Agreement.instReprPersonNumber.repr : PersonNumber → Nat → Std.Format

Equations

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

instance Fragments.Basque.Agreement.instReprPersonNumber : Repr PersonNumber

Equations

• Fragments.Basque.Agreement.instReprPersonNumber = { reprPrec := Fragments.Basque.Agreement.instReprPersonNumber.repr }

def Fragments.Basque.Agreement.allPersonNumbers : List PersonNumber

All person-number values.

Equations

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

def Fragments.Basque.Agreement.PersonNumber.person : PersonNumber → Nat

Person value (1, 2, or 3).

Equations

• Fragments.Basque.Agreement.PersonNumber.p1sg.person = 1
• Fragments.Basque.Agreement.PersonNumber.p1pl.person = 1
• Fragments.Basque.Agreement.PersonNumber.p2sg.person = 2
• Fragments.Basque.Agreement.PersonNumber.p2pl.person = 2
• Fragments.Basque.Agreement.PersonNumber.p3sg.person = 3
• Fragments.Basque.Agreement.PersonNumber.p3pl.person = 3

def Fragments.Basque.Agreement.PersonNumber.isSAP (pn : PersonNumber) : Bool

Is this a SAP (speech act participant)?

Equations

• pn.isSAP = (pn.person == 1 || pn.person == 2)

inductive Fragments.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)

instance Fragments.Basque.Agreement.instDecidableEqArgPosition : DecidableEq ArgPosition

Equations

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

def Fragments.Basque.Agreement.instBEqArgPosition.beq : ArgPosition → ArgPosition → Bool

Equations

• Fragments.Basque.Agreement.instBEqArgPosition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Basque.Agreement.instBEqArgPosition : BEq ArgPosition

Equations

• Fragments.Basque.Agreement.instBEqArgPosition = { beq := Fragments.Basque.Agreement.instBEqArgPosition.beq }

instance Fragments.Basque.Agreement.instReprArgPosition : Repr ArgPosition

Equations

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

def Fragments.Basque.Agreement.instReprArgPosition.repr : ArgPosition → Nat → Std.Format

Equations

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

def Fragments.Basque.Agreement.pIsIndexed (pn : PersonNumber) : Bool

Whether a P argument at a given person-number is indexed on the verb.

Basque cross-references SAP objects (1st/2nd person) but not 3rd person objects in the relevant constructions. A and S arguments are always indexed regardless of person.

Equations

• Fragments.Basque.Agreement.pIsIndexed pn = pn.isSAP

def Fragments.Basque.Agreement.asIsIndexed : PersonNumber → Bool

Whether an A/S argument at a given person-number is indexed. Always true — A and S indexing is not differential in Basque.

Equations

• Fragments.Basque.Agreement.asIsIndexed x✝ = true

theorem Fragments.Basque.Agreement.sap_objects_indexed : pIsIndexed PersonNumber.p1sg = true ∧ pIsIndexed PersonNumber.p2sg = true ∧ pIsIndexed PersonNumber.p1pl = true ∧ pIsIndexed PersonNumber.p2pl = true

SAP objects are indexed.

theorem Fragments.Basque.Agreement.third_objects_not_indexed : pIsIndexed PersonNumber.p3sg = false ∧ pIsIndexed PersonNumber.p3pl = false

3rd person objects are NOT indexed.

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

P indexing is differential: some person-numbers indexed, some not.

theorem Fragments.Basque.Agreement.as_indexing_uniform : allPersonNumbers.all asIsIndexed = true

A/S indexing is NOT differential: all person-numbers indexed.

def Fragments.Basque.Agreement.agreementCaseInventory : List Core.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

• Fragments.Basque.Agreement.agreementCaseInventory = [Core.Case.erg, Core.Case.abs, Core.Case.dat]

def Fragments.Basque.Agreement.fullCaseInventory : List Core.Case

The full Basque case inventory (representative selection).

Equations

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

theorem Fragments.Basque.Agreement.full_inventory_valid : Core.validInventory fullCaseInventory = true

The full inventory is valid per Blake's hierarchy (ranks 6 down to 1, all represented).