Spanish object clitics

Spanish object pronouns are clitics on the verb. The first and second persons have one form each for direct object, indirect object and reflexive use: me, te, nos and os. Only the third person tells the three apart: accusative lo, la, los and las mark gender and number, dative le and les mark number alone, and reflexive se marks neither. A third-person dative is replaced by se before a third-person accusative, se lo doy and never le lo doy, so se is also a form of the dative. Os belongs to vosotros and is confined to Spain; elsewhere the third-person plural forms serve for plural addressees. The description follows Butt, Benjamin and Moreira Rodríguez's reference grammar.

Main declarations

• Spanish.Clitics.accusative, Spanish.Clitics.dative — the two object series, personal pronouns of the clitic strength class
• Spanish.Clitics.reflexive — the reflexive series
• Spanish.Clitics.paradigm_accusative_eq_paradigm_dative_iff, Spanish.Clitics.paradigm_dative_eq_paradigm_reflexive_iff — the series are syncretic exactly outside the third person
• Spanish.Clitics.isSome_gender_iff — gender is marked by the third-person accusatives alone

References

• J. Butt, C. Benjamin and A. Moreira Rodríguez, A New Reference Grammar of Modern Spanish (2019)

The accusative series

def Spanish.Clitics.me_acc : PersonalPronoun

me, first person singular accusative.

Equations

• Spanish.Clitics.me_acc = { form := "me", person := some Person.first, number := some Number.singular, case_ := some Case.acc, strength := some Pronoun.Strength.clitic }

def Spanish.Clitics.te_acc : PersonalPronoun

te, second person singular accusative.

Equations

• Spanish.Clitics.te_acc = { form := "te", person := some Person.second, number := some Number.singular, case_ := some Case.acc, strength := some Pronoun.Strength.clitic }

def Spanish.Clitics.lo : PersonalPronoun

lo, third person singular masculine accusative.

Equations

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

def Spanish.Clitics.la : PersonalPronoun

la, third person singular feminine accusative.

Equations

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

def Spanish.Clitics.nos_acc : PersonalPronoun

nos, first person plural accusative.

Equations

• Spanish.Clitics.nos_acc = { form := "nos", person := some Person.first, number := some Number.plural, case_ := some Case.acc, strength := some Pronoun.Strength.clitic }

def Spanish.Clitics.os_acc : PersonalPronoun

os, second person plural accusative, used in Spain.

Equations

• Spanish.Clitics.os_acc = { form := "os", person := some Person.second, number := some Number.plural, case_ := some Case.acc, strength := some Pronoun.Strength.clitic }

def Spanish.Clitics.los : PersonalPronoun

los, third person plural masculine accusative.

Equations

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

def Spanish.Clitics.las : PersonalPronoun

las, third person plural feminine accusative.

Equations

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

def Spanish.Clitics.accusative : Finset PersonalPronoun

The accusative series.

Equations

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

The dative series

def Spanish.Clitics.me_dat : PersonalPronoun

me, first person singular dative.

Equations

• Spanish.Clitics.me_dat = { form := "me", person := some Person.first, number := some Number.singular, case_ := some Case.dat, strength := some Pronoun.Strength.clitic }

def Spanish.Clitics.te_dat : PersonalPronoun

te, second person singular dative.

Equations

• Spanish.Clitics.te_dat = { form := "te", person := some Person.second, number := some Number.singular, case_ := some Case.dat, strength := some Pronoun.Strength.clitic }

def Spanish.Clitics.le : PersonalPronoun

le, third person singular dative.

Equations

• Spanish.Clitics.le = { form := "le", person := some Person.third, number := some Number.singular, case_ := some Case.dat, strength := some Pronoun.Strength.clitic }

def Spanish.Clitics.nos_dat : PersonalPronoun

nos, first person plural dative.

Equations

• Spanish.Clitics.nos_dat = { form := "nos", person := some Person.first, number := some Number.plural, case_ := some Case.dat, strength := some Pronoun.Strength.clitic }

def Spanish.Clitics.os_dat : PersonalPronoun

os, second person plural dative, used in Spain.

Equations

• Spanish.Clitics.os_dat = { form := "os", person := some Person.second, number := some Number.plural, case_ := some Case.dat, strength := some Pronoun.Strength.clitic }

def Spanish.Clitics.les : PersonalPronoun

les, third person plural dative.

Equations

• Spanish.Clitics.les = { form := "les", person := some Person.third, number := some Number.plural, case_ := some Case.dat, strength := some Pronoun.Strength.clitic }

def Spanish.Clitics.se_dat : PersonalPronoun

se, the form le and les take before a third-person accusative clitic, as in se lo doy 'I give it to them'. It is number-neutral.

Equations

• Spanish.Clitics.se_dat = { form := "se", person := some Person.third, number := some Number.general, case_ := some Case.dat, strength := some Pronoun.Strength.clitic }

def Spanish.Clitics.dative : Finset PersonalPronoun

The dative series.

Equations

• Spanish.Clitics.dative = {Spanish.Clitics.me_dat, Spanish.Clitics.te_dat, Spanish.Clitics.le, Spanish.Clitics.nos_dat, Spanish.Clitics.os_dat, Spanish.Clitics.les, Spanish.Clitics.se_dat}

The reflexive series

def Spanish.Clitics.me_refl : ReflexivePronoun

me, first person singular reflexive.

Equations

• Spanish.Clitics.me_refl = { form := "me", person := some Person.first, number := some Number.singular, strength := some Pronoun.Strength.clitic }

def Spanish.Clitics.te_refl : ReflexivePronoun

te, second person singular reflexive.

Equations

• Spanish.Clitics.te_refl = { form := "te", person := some Person.second, number := some Number.singular, strength := some Pronoun.Strength.clitic }

def Spanish.Clitics.se : ReflexivePronoun

se, third person reflexive, number-neutral.

Equations

• Spanish.Clitics.se = { form := "se", person := some Person.third, number := some Number.general, strength := some Pronoun.Strength.clitic }

def Spanish.Clitics.nos_refl : ReflexivePronoun

nos, first person plural reflexive.

Equations

• Spanish.Clitics.nos_refl = { form := "nos", person := some Person.first, number := some Number.plural, strength := some Pronoun.Strength.clitic }

def Spanish.Clitics.os_refl : ReflexivePronoun

os, second person plural reflexive, used in Spain.

Equations

• Spanish.Clitics.os_refl = { form := "os", person := some Person.second, number := some Number.plural, strength := some Pronoun.Strength.clitic }

def Spanish.Clitics.reflexive : Finset ReflexivePronoun

The reflexive series.

Equations

• Spanish.Clitics.reflexive = {Spanish.Clitics.me_refl, Spanish.Clitics.te_refl, Spanish.Clitics.se, Spanish.Clitics.nos_refl, Spanish.Clitics.os_refl}

Syncretism across the series

theorem Spanish.Clitics.paradigm_accusative_eq_paradigm_dative_iff (c : Person.Category) : PersonalPronoun.paradigm accusative c = PersonalPronoun.paradigm dative c ↔ c.person ≠ Person.third

The accusative and the dative have the same forms exactly outside the third person.

theorem Spanish.Clitics.paradigm_dative_eq_paradigm_reflexive_iff (c : Person.Category) : PersonalPronoun.paradigm dative c = ReflexivePronoun.paradigm reflexive c ↔ c.person ≠ Person.third

The dative and the reflexive have the same forms exactly outside the third person, where the dative has le or les beside se and the reflexive se alone.

theorem Spanish.Clitics.paradigm_reflexive_nonempty (c : Person.Category) : (ReflexivePronoun.paradigm reflexive c).Nonempty

Every category has a reflexive form.

theorem Spanish.Clitics.isSome_gender_iff {p : PersonalPronoun} (hp : p ∈ accusative ∪ dative) : p.gender.isSome = true ↔ p.person = some Person.third ∧ p.case_ = some Case.acc

Gender is marked by the third-person accusatives alone.