Spanish Clitic Paradigm

@cite{munoz-perez-2026}

The full Spanish clitic paradigm, with syncretism data critical for Muñoz @cite{munoz-perez-2026}. The key observation: 1SG and 2SG are syncretic across accusative, dative, and reflexive, while 3SG/PL are not. This syncretism drives the availability of stylistic applicatives.

Paradigm (Muñoz @cite{munoz-perez-2026}, ex. 59)

	ACC	DAT	REFL
1SG	me	me	me
2SG	te	te	te
3SG	lo/la	le/se	se
1PL	nos	nos	nos
2/3PL	los/las	les/se	se

inductive Fragments.Spanish.Clitics.CliticCase : Type

The three-way case distinction for Spanish clitics.

• accusative : CliticCase
• dative : CliticCase
• reflexive : CliticCase

instance Fragments.Spanish.Clitics.instDecidableEqCliticCase : DecidableEq CliticCase

Equations

• Fragments.Spanish.Clitics.instDecidableEqCliticCase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Spanish.Clitics.instBEqCliticCase.beq : CliticCase → CliticCase → Bool

Equations

• Fragments.Spanish.Clitics.instBEqCliticCase.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Spanish.Clitics.instBEqCliticCase : BEq CliticCase

Equations

• Fragments.Spanish.Clitics.instBEqCliticCase = { beq := Fragments.Spanish.Clitics.instBEqCliticCase.beq }

def Fragments.Spanish.Clitics.instReprCliticCase.repr : CliticCase → Nat → Std.Format

Equations

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

instance Fragments.Spanish.Clitics.instReprCliticCase : Repr CliticCase

Equations

• Fragments.Spanish.Clitics.instReprCliticCase = { reprPrec := Fragments.Spanish.Clitics.instReprCliticCase.repr }

structure Fragments.Spanish.Clitics.CliticEntry : Type

A single clitic form in the paradigm.

• form : String
• person : Person
• number : Number
• case_ : CliticCase

def Fragments.Spanish.Clitics.instReprCliticEntry.repr : CliticEntry → Nat → Std.Format

Equations

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

instance Fragments.Spanish.Clitics.instReprCliticEntry : Repr CliticEntry

Equations

• Fragments.Spanish.Clitics.instReprCliticEntry = { reprPrec := Fragments.Spanish.Clitics.instReprCliticEntry.repr }

instance Fragments.Spanish.Clitics.instBEqCliticEntry : BEq CliticEntry

Equations

• Fragments.Spanish.Clitics.instBEqCliticEntry = { beq := Fragments.Spanish.Clitics.instBEqCliticEntry.beq }

def Fragments.Spanish.Clitics.instBEqCliticEntry.beq : CliticEntry → CliticEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Spanish.Clitics.instBEqCliticEntry.beq x✝¹ x✝ = false

def Fragments.Spanish.Clitics.me_acc : CliticEntry

Equations

• Fragments.Spanish.Clitics.me_acc = { form := "me", person := UD.Person.first, number := UD.Number.Sing, case_ := Fragments.Spanish.Clitics.CliticCase.accusative }

def Fragments.Spanish.Clitics.me_dat : CliticEntry

Equations

• Fragments.Spanish.Clitics.me_dat = { form := "me", person := UD.Person.first, number := UD.Number.Sing, case_ := Fragments.Spanish.Clitics.CliticCase.dative }

def Fragments.Spanish.Clitics.me_refl : CliticEntry

Equations

• Fragments.Spanish.Clitics.me_refl = { form := "me", person := UD.Person.first, number := UD.Number.Sing, case_ := Fragments.Spanish.Clitics.CliticCase.reflexive }

def Fragments.Spanish.Clitics.te_acc : CliticEntry

Equations

• Fragments.Spanish.Clitics.te_acc = { form := "te", person := UD.Person.second, number := UD.Number.Sing, case_ := Fragments.Spanish.Clitics.CliticCase.accusative }

def Fragments.Spanish.Clitics.te_dat : CliticEntry

Equations

• Fragments.Spanish.Clitics.te_dat = { form := "te", person := UD.Person.second, number := UD.Number.Sing, case_ := Fragments.Spanish.Clitics.CliticCase.dative }

def Fragments.Spanish.Clitics.te_refl : CliticEntry

Equations

• Fragments.Spanish.Clitics.te_refl = { form := "te", person := UD.Person.second, number := UD.Number.Sing, case_ := Fragments.Spanish.Clitics.CliticCase.reflexive }

def Fragments.Spanish.Clitics.lo : CliticEntry

Equations

• Fragments.Spanish.Clitics.lo = { form := "lo", person := UD.Person.third, number := UD.Number.Sing, case_ := Fragments.Spanish.Clitics.CliticCase.accusative }

def Fragments.Spanish.Clitics.la : CliticEntry

Equations

• Fragments.Spanish.Clitics.la = { form := "la", person := UD.Person.third, number := UD.Number.Sing, case_ := Fragments.Spanish.Clitics.CliticCase.accusative }

def Fragments.Spanish.Clitics.le_dat : CliticEntry

Equations

• Fragments.Spanish.Clitics.le_dat = { form := "le", person := UD.Person.third, number := UD.Number.Sing, case_ := Fragments.Spanish.Clitics.CliticCase.dative }

def Fragments.Spanish.Clitics.se_refl : CliticEntry

Equations

• Fragments.Spanish.Clitics.se_refl = { form := "se", person := UD.Person.third, number := UD.Number.Sing, case_ := Fragments.Spanish.Clitics.CliticCase.reflexive }

def Fragments.Spanish.Clitics.nos_acc : CliticEntry

Equations

• Fragments.Spanish.Clitics.nos_acc = { form := "nos", person := UD.Person.first, number := UD.Number.Plur, case_ := Fragments.Spanish.Clitics.CliticCase.accusative }

def Fragments.Spanish.Clitics.nos_dat : CliticEntry

Equations

• Fragments.Spanish.Clitics.nos_dat = { form := "nos", person := UD.Person.first, number := UD.Number.Plur, case_ := Fragments.Spanish.Clitics.CliticCase.dative }

def Fragments.Spanish.Clitics.nos_refl : CliticEntry

Equations

• Fragments.Spanish.Clitics.nos_refl = { form := "nos", person := UD.Person.first, number := UD.Number.Plur, case_ := Fragments.Spanish.Clitics.CliticCase.reflexive }

def Fragments.Spanish.Clitics.los : CliticEntry

Equations

• Fragments.Spanish.Clitics.los = { form := "los", person := UD.Person.third, number := UD.Number.Plur, case_ := Fragments.Spanish.Clitics.CliticCase.accusative }

def Fragments.Spanish.Clitics.las : CliticEntry

Equations

• Fragments.Spanish.Clitics.las = { form := "las", person := UD.Person.third, number := UD.Number.Plur, case_ := Fragments.Spanish.Clitics.CliticCase.accusative }

def Fragments.Spanish.Clitics.les_dat : CliticEntry

Equations

• Fragments.Spanish.Clitics.les_dat = { form := "les", person := UD.Person.third, number := UD.Number.Plur, case_ := Fragments.Spanish.Clitics.CliticCase.dative }

def Fragments.Spanish.Clitics.se_refl_pl : CliticEntry

Equations

• Fragments.Spanish.Clitics.se_refl_pl = { form := "se", person := UD.Person.third, number := UD.Number.Plur, case_ := Fragments.Spanish.Clitics.CliticCase.reflexive }

def Fragments.Spanish.Clitics.paradigm : List CliticEntry

The full clitic paradigm as a flat list.

Equations

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

def Fragments.Spanish.Clitics.lookupForm (p : Person) (n : Number) (c : CliticCase) : Option String

Look up the form for a given person, number, and case in the paradigm.

Equations

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

def Fragments.Spanish.Clitics.isSyncretic (p : Person) (n : Number) (c1 c2 : CliticCase) : Bool

Are two clitic cases syncretic for a given person/number combination? DERIVED from the paradigm data: syncretism holds iff the looked-up forms are identical (and both exist).

Equations

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

def Fragments.Spanish.Clitics.datReflSyncretic (p : Person) (n : Number) : Bool

The set of person/number combinations where DAT and REFL are syncretic. This is the key condition for SE-optionality.

Equations

• Fragments.Spanish.Clitics.datReflSyncretic p n = Fragments.Spanish.Clitics.isSyncretic p n Fragments.Spanish.Clitics.CliticCase.dative Fragments.Spanish.Clitics.CliticCase.reflexive

theorem Fragments.Spanish.Clitics.syncretic_1sg : datReflSyncretic UD.Person.first UD.Number.Sing = true

1SG: dative and reflexive are syncretic (both "me").

theorem Fragments.Spanish.Clitics.syncretic_2sg : datReflSyncretic UD.Person.second UD.Number.Sing = true

2SG: dative and reflexive are syncretic (both "te").

theorem Fragments.Spanish.Clitics.not_syncretic_3sg : datReflSyncretic UD.Person.third UD.Number.Sing = false

3SG: dative and reflexive are NOT syncretic ("le" ≠ "se").

theorem Fragments.Spanish.Clitics.syncretic_1pl : datReflSyncretic UD.Person.first UD.Number.Plur = true

1PL: dative and reflexive are syncretic (both "nos").

theorem Fragments.Spanish.Clitics.not_syncretic_3pl : datReflSyncretic UD.Person.third UD.Number.Plur = false

3PL: dative and reflexive are NOT syncretic ("les" ≠ "se").

theorem Fragments.Spanish.Clitics.me_forms_identical : me_acc.form = me_dat.form ∧ me_dat.form = me_refl.form

1SG forms are identical across all three cases.

theorem Fragments.Spanish.Clitics.te_forms_identical : te_acc.form = te_dat.form ∧ te_dat.form = te_refl.form

2SG forms are identical across all three cases.

theorem Fragments.Spanish.Clitics.le_ne_se : le_dat.form ≠ se_refl.form

3SG dative ≠ 3SG reflexive (le ≠ se).