Basque verbal agreement

The finite verb of Basque, in most clauses an auxiliary, agrees with the absolutive, the dative and the ergative phrase of its clause. Each case has its own marker and its own place: the absolutive marker stands before the root, the dative marker after it, and the ergative marker after that, as in d-i-da-zu 'you have (sold) it to me'. The dative and ergative markers are the same for the first and second persons and differ in the third, where the dative has -o and -e and the ergative has nothing in the singular and -te in the plural. The familiar second person hi is the one place where the verb marks gender, -k for a man and -n for a woman.

The absolutive slot treats the third person differently from the others. The first and second persons have the prefixes n-, h-, g- and z- in every tense. A third person absolutive has no prefix of its own: the slot holds d- in the present and z- in the past, whatever the number, and the number of the absolutive phrase shows only in a separate plural marker. In a past-tense transitive verb with a third person absolutive the slot is taken over by the ergative phrase, which then has no suffix, so that n-u-en 'I had it' begins like n-ind-u-zu-n 'you had me'. This is the pattern known as ergative displacement.

The pronoun zu, once a plural and now the ordinary way of addressing one person, still agrees as a plural, and the newer plural zuek adds a further plural marker to the forms of zu.

Main declarations

• Basque.absolutive, Basque.dative, Basque.ergative: the marker of each slot for each person and number, in the present tense.
• Basque.thirdAbsolutive: what fills the absolutive slot by tense when the absolutive phrase is third person.
• Basque.displacedErgative: the ergative markers of a past-tense verb with a third person absolutive.
• Basque.HasPersonPrefix: the absolutive slot has a prefix for the person and number.

Main results

• Basque.hasPersonPrefix_iff_isSAP: the absolutive prefixes are those of the first and second persons.
• Basque.dative_eq_ergative: the dative and ergative markers of the first and second persons coincide.
• Basque.displacedErgative_head: a displaced ergative begins with what would fill the absolutive slot for its own person and number in the past.
• Basque.allocutive_eq_ergative: the familiar allocutive suffixes are the ergative suffixes of hi.

Implementation notes

The cells are the bundles of Syntax/Agreement/Bundle.lean, so that a pronoun's features index a table directly. The second person plural cell is that of zu, following the forms rather than the meaning, and zuek has no cell of its own. The two cells of hi with a gender occur only in the dative and ergative tables. The first and second person singular suffixes are given as they stand at the end of the word; before another suffix they are -da-, -a- and -na-. Forms with modal markers, where the third person filler is l-, are not covered.

References

• [Lak96]

def Basque.familiar (g : Gender) : Agreement.Bundle

The cell of the familiar second person hi addressed to a person of the given gender.

Equations

• Basque.familiar g = Agreement.Bundle.set Agreement.Dimension.gender g (Agreement.Bundle.personNumber Person.second Number.singular)

The three slots

def Basque.absolutive : Agreement.Paradigm (List Morphology.Morph)

The absolutive prefixes. Only the first and second persons have one.

Equations

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

def Basque.participantSuffixes : Agreement.Paradigm (List Morphology.Morph)

The suffixes of the first and second persons, which the dative and ergative slots share.

Equations

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

def Basque.dative : Agreement.Paradigm (List Morphology.Morph)

The dative suffixes.

Equations

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

def Basque.ergative : Agreement.Paradigm (List Morphology.Morph)

The ergative suffixes. The third person singular has none.

Equations

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

def Basque.thirdAbsolutive : Tense → Option Morphology.Morph

The element in the absolutive slot when the absolutive phrase is third person, d- in the present and z- in the past. Basque has no future inflection.

Equations

• Basque.thirdAbsolutive Tense.present = some (Morphology.Morph.pref "d")
• Basque.thirdAbsolutive Tense.past = some (Morphology.Morph.pref "z")
• Basque.thirdAbsolutive Tense.future = none

def Basque.displacedErgative : Agreement.Paradigm (List Morphology.Morph)

The ergative markers of a past-tense verb whose absolutive phrase is third person. They stand in the absolutive slot, and the third person plural keeps its suffix.

Equations

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

Person in the absolutive slot

def Basque.HasPersonPrefix (c : Agreement.Bundle) : Prop

The absolutive slot has a prefix for the cell.

Equations

• Basque.HasPersonPrefix c = ((Basque.absolutive.realize c).isSome = true)

@[instance_reducible]

instance Basque.instDecidablePredBundleHasPersonPrefix : DecidablePred HasPersonPrefix

Equations

• Basque.instDecidablePredBundleHasPersonPrefix x✝ = Basque.instDecidablePredBundleHasPersonPrefix._aux_1 x✝

theorem Basque.hasPersonPrefix_iff_isSAP (c : Agreement.Bundle) : c ∈ Agreement.Bundle.personNumberCells → (HasPersonPrefix c ↔ c.IsSAP)

The absolutive prefixes are those of the first and second persons.

theorem Basque.hasPersonPrefix_phi_iff (p : PersonalPronoun) : p ∈ Pronouns.pronouns → (HasPersonPrefix (phi p) ↔ p.person ≠ some Person.third)

Every personal pronoun but the third person ones has an absolutive prefix.

theorem Basque.dative_eq_ergative {c : Agreement.Bundle} (h : c.IsSAP) : dative.realize c = ergative.realize c

The dative and ergative markers of the first and second persons coincide.

theorem Basque.displacedErgative_head (c : Agreement.Bundle) : c ∈ Agreement.Bundle.personNumberCells → ((displacedErgative.realize c).bind fun (x : List Morphology.Morph) => x.head?) = ((absolutive.realize c).bind fun (x : List Morphology.Morph) => x.head?).or (thirdAbsolutive Tense.past)

A displaced ergative begins with what would fill the absolutive slot for its own person and number in the past: the absolutive prefix of a first or second person, the past filler of a third.

theorem Basque.allocutive_eq_ergative (g : Gender) : Option.map (fun (x : Morphology.Morph) => [x]) (Pronouns.allocutive Grade.familiar g) = ergative.realize (familiar g)

The allocutive suffix of a familiar addressee is, for each gender, the ergative suffix of hi.