Italian Pronoun and Clitic Fragment

Personal pronouns (strong forms) and clitic paradigm for Italian.

Strong Pronouns

@cite{munoz-perez-2026}

Italian has a T/V distinction in 2nd person:

• Singular: tu (familiar T) vs Lei (formal V, 3sg agreement)
• Plural: voi (familiar) vs Loro (formal, archaic; voi now used for both)

Clitic Paradigm

Italian object clitics show the same syncretism pattern as Spanish: 1sg/2sg are syncretic across accusative, dative, and reflexive cases, while 3sg/3pl are not.

Person	ACC	DAT	REFL
1sg	mi	mi	mi
2sg	ti	ti	ti
3sg	lo/la	gli/le	si
1pl	ci	ci	ci
2pl	vi	vi	vi
3pl	li/le	loro	si

def Fragments.Italian.Pronouns.io : Typology.PronounEntry

io — 1sg.

Equations

• Fragments.Italian.Pronouns.io = { form := "io", person := some UD.Person.first, number := some Number.sg }

def Fragments.Italian.Pronouns.tu : Typology.PronounEntry

tu — 2sg familiar (T form).

Equations

• Fragments.Italian.Pronouns.tu = { form := "tu", person := some UD.Person.second, number := some Number.sg }

def Fragments.Italian.Pronouns.lei_formal : Typology.PronounEntry

Lei — polite 2sg (V form). Formally 3rd person: triggers 3sg verbal agreement, patterns with 3sg.f clitics, binds 3rd person reflexive si. Interpretably 2nd person: triggers PCC effects, Fancy Constraint effects, 2PL resolved agreement in coordination. @cite{adamson-zompi-2025}

Equations

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

def Fragments.Italian.Pronouns.lui : Typology.PronounEntry

lui — 3sg masculine.

Equations

• Fragments.Italian.Pronouns.lui = { form := "lui", person := some UD.Person.third, number := some Number.sg }

def Fragments.Italian.Pronouns.lei : Typology.PronounEntry

lei — 3sg feminine.

Equations

• Fragments.Italian.Pronouns.lei = { form := "lei", person := some UD.Person.third, number := some Number.sg }

def Fragments.Italian.Pronouns.noi : Typology.PronounEntry

noi — 1pl.

Equations

• Fragments.Italian.Pronouns.noi = { form := "noi", person := some UD.Person.first, number := some Number.pl }

def Fragments.Italian.Pronouns.voi : Typology.PronounEntry

voi — 2pl (familiar; also used as general 2pl in modern Italian).

Equations

• Fragments.Italian.Pronouns.voi = { form := "voi", person := some UD.Person.second, number := some Number.pl }

def Fragments.Italian.Pronouns.loro_formal : Typology.PronounEntry

Loro — 2pl formal (archaic, largely replaced by voi).

Equations

• Fragments.Italian.Pronouns.loro_formal = { form := "Loro", person := some UD.Person.second, number := some Number.pl, register := Features.Register.Level.formal }

def Fragments.Italian.Pronouns.loro : Typology.PronounEntry

loro — 3pl.

Equations

• Fragments.Italian.Pronouns.loro = { form := "loro", person := some UD.Person.third, number := some Number.pl }

def Fragments.Italian.Pronouns.secondPersonPronouns : List Typology.PronounEntry

Equations

• Fragments.Italian.Pronouns.secondPersonPronouns = [Fragments.Italian.Pronouns.tu, Fragments.Italian.Pronouns.lei_formal]

def Fragments.Italian.Pronouns.allPronouns : List Typology.PronounEntry

Equations

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

inductive Fragments.Italian.Pronouns.CliticCase : Type

The three-way case distinction for Italian clitics.

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

@[implicit_reducible]

instance Fragments.Italian.Pronouns.instDecidableEqCliticCase : DecidableEq CliticCase

Equations

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

def Fragments.Italian.Pronouns.instReprCliticCase.repr : CliticCase → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Italian.Pronouns.instReprCliticCase : Repr CliticCase

Equations

• Fragments.Italian.Pronouns.instReprCliticCase = { reprPrec := Fragments.Italian.Pronouns.instReprCliticCase.repr }

structure Fragments.Italian.Pronouns.CliticEntry : Type

A single clitic form in the paradigm.

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

@[implicit_reducible]

instance Fragments.Italian.Pronouns.instReprCliticEntry : Repr CliticEntry

Equations

• Fragments.Italian.Pronouns.instReprCliticEntry = { reprPrec := Fragments.Italian.Pronouns.instReprCliticEntry.repr }

def Fragments.Italian.Pronouns.instReprCliticEntry.repr : CliticEntry → ℕ → Std.Format

Equations

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

def Fragments.Italian.Pronouns.instBEqCliticEntry.beq : CliticEntry → CliticEntry → Bool

Equations

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

@[implicit_reducible]

instance Fragments.Italian.Pronouns.instBEqCliticEntry : BEq CliticEntry

Equations

• Fragments.Italian.Pronouns.instBEqCliticEntry = { beq := Fragments.Italian.Pronouns.instBEqCliticEntry.beq }

def Fragments.Italian.Pronouns.mi_acc : CliticEntry

Equations

• Fragments.Italian.Pronouns.mi_acc = { form := "mi", person := UD.Person.first, number := UD.Number.Sing, case_ := Fragments.Italian.Pronouns.CliticCase.accusative }

def Fragments.Italian.Pronouns.mi_dat : CliticEntry

Equations

• Fragments.Italian.Pronouns.mi_dat = { form := "mi", person := UD.Person.first, number := UD.Number.Sing, case_ := Fragments.Italian.Pronouns.CliticCase.dative }

def Fragments.Italian.Pronouns.mi_refl : CliticEntry

Equations

• Fragments.Italian.Pronouns.mi_refl = { form := "mi", person := UD.Person.first, number := UD.Number.Sing, case_ := Fragments.Italian.Pronouns.CliticCase.reflexive }

def Fragments.Italian.Pronouns.ti_acc : CliticEntry

Equations

• Fragments.Italian.Pronouns.ti_acc = { form := "ti", person := UD.Person.second, number := UD.Number.Sing, case_ := Fragments.Italian.Pronouns.CliticCase.accusative }

def Fragments.Italian.Pronouns.ti_dat : CliticEntry

Equations

• Fragments.Italian.Pronouns.ti_dat = { form := "ti", person := UD.Person.second, number := UD.Number.Sing, case_ := Fragments.Italian.Pronouns.CliticCase.dative }

def Fragments.Italian.Pronouns.ti_refl : CliticEntry

Equations

• Fragments.Italian.Pronouns.ti_refl = { form := "ti", person := UD.Person.second, number := UD.Number.Sing, case_ := Fragments.Italian.Pronouns.CliticCase.reflexive }

def Fragments.Italian.Pronouns.lo_cl : CliticEntry

Equations

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

def Fragments.Italian.Pronouns.la_cl : CliticEntry

Equations

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

def Fragments.Italian.Pronouns.gli_dat : CliticEntry

Equations

• Fragments.Italian.Pronouns.gli_dat = { form := "gli", person := UD.Person.third, number := UD.Number.Sing, case_ := Fragments.Italian.Pronouns.CliticCase.dative }

def Fragments.Italian.Pronouns.le_dat : CliticEntry

Equations

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

def Fragments.Italian.Pronouns.si_refl : CliticEntry

Equations

• Fragments.Italian.Pronouns.si_refl = { form := "si", person := UD.Person.third, number := UD.Number.Sing, case_ := Fragments.Italian.Pronouns.CliticCase.reflexive }

def Fragments.Italian.Pronouns.ci_acc : CliticEntry

Equations

• Fragments.Italian.Pronouns.ci_acc = { form := "ci", person := UD.Person.first, number := UD.Number.Plur, case_ := Fragments.Italian.Pronouns.CliticCase.accusative }

def Fragments.Italian.Pronouns.ci_dat : CliticEntry

Equations

• Fragments.Italian.Pronouns.ci_dat = { form := "ci", person := UD.Person.first, number := UD.Number.Plur, case_ := Fragments.Italian.Pronouns.CliticCase.dative }

def Fragments.Italian.Pronouns.ci_refl : CliticEntry

Equations

• Fragments.Italian.Pronouns.ci_refl = { form := "ci", person := UD.Person.first, number := UD.Number.Plur, case_ := Fragments.Italian.Pronouns.CliticCase.reflexive }

def Fragments.Italian.Pronouns.vi_acc : CliticEntry

Equations

• Fragments.Italian.Pronouns.vi_acc = { form := "vi", person := UD.Person.second, number := UD.Number.Plur, case_ := Fragments.Italian.Pronouns.CliticCase.accusative }

def Fragments.Italian.Pronouns.vi_dat : CliticEntry

Equations

• Fragments.Italian.Pronouns.vi_dat = { form := "vi", person := UD.Person.second, number := UD.Number.Plur, case_ := Fragments.Italian.Pronouns.CliticCase.dative }

def Fragments.Italian.Pronouns.vi_refl : CliticEntry

Equations

• Fragments.Italian.Pronouns.vi_refl = { form := "vi", person := UD.Person.second, number := UD.Number.Plur, case_ := Fragments.Italian.Pronouns.CliticCase.reflexive }

def Fragments.Italian.Pronouns.li_cl : CliticEntry

Equations

• Fragments.Italian.Pronouns.li_cl = { form := "li", person := UD.Person.third, number := UD.Number.Plur, case_ := Fragments.Italian.Pronouns.CliticCase.accusative }

def Fragments.Italian.Pronouns.le_cl : CliticEntry

Equations

• Fragments.Italian.Pronouns.le_cl = { form := "le", person := UD.Person.third, number := UD.Number.Plur, case_ := Fragments.Italian.Pronouns.CliticCase.accusative }

def Fragments.Italian.Pronouns.loro_dat : CliticEntry

Equations

• Fragments.Italian.Pronouns.loro_dat = { form := "loro", person := UD.Person.third, number := UD.Number.Plur, case_ := Fragments.Italian.Pronouns.CliticCase.dative }

def Fragments.Italian.Pronouns.si_refl_pl : CliticEntry

Equations

• Fragments.Italian.Pronouns.si_refl_pl = { form := "si", person := UD.Person.third, number := UD.Number.Plur, case_ := Fragments.Italian.Pronouns.CliticCase.reflexive }

def Fragments.Italian.Pronouns.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.Italian.Pronouns.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.Italian.Pronouns.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.

Equations

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

def Fragments.Italian.Pronouns.datReflSyncretic (p : Person) (n : Number) : Bool

DAT/REFL syncretism for a given person/number.

Equations

• Fragments.Italian.Pronouns.datReflSyncretic p n = Fragments.Italian.Pronouns.isSyncretic p n Fragments.Italian.Pronouns.CliticCase.dative Fragments.Italian.Pronouns.CliticCase.reflexive

theorem Fragments.Italian.Pronouns.syncretic_1sg : datReflSyncretic UD.Person.first UD.Number.Sing = true

1sg: dative and reflexive are syncretic (both "mi").

theorem Fragments.Italian.Pronouns.syncretic_2sg : datReflSyncretic UD.Person.second UD.Number.Sing = true

2sg: dative and reflexive are syncretic (both "ti").

theorem Fragments.Italian.Pronouns.not_syncretic_3sg : datReflSyncretic UD.Person.third UD.Number.Sing = false

3sg: dative and reflexive are NOT syncretic ("gli" ≠ "si").

theorem Fragments.Italian.Pronouns.syncretic_1pl : datReflSyncretic UD.Person.first UD.Number.Plur = true

1pl: dative and reflexive are syncretic (both "ci").

theorem Fragments.Italian.Pronouns.syncretic_2pl : datReflSyncretic UD.Person.second UD.Number.Plur = true

2pl: dative and reflexive are syncretic (both "vi").

theorem Fragments.Italian.Pronouns.not_syncretic_3pl : datReflSyncretic UD.Person.third UD.Number.Plur = false

3pl: dative and reflexive are NOT syncretic ("loro" ≠ "si").

theorem Fragments.Italian.Pronouns.mi_forms_identical : mi_acc.form = mi_dat.form ∧ mi_dat.form = mi_refl.form

1sg forms are identical across all three cases.

theorem Fragments.Italian.Pronouns.ti_forms_identical : ti_acc.form = ti_dat.form ∧ ti_dat.form = ti_refl.form

2sg forms are identical across all three cases.

theorem Fragments.Italian.Pronouns.gli_ne_si : gli_dat.form ≠ si_refl.form

3sg dative ≠ 3sg reflexive (gli ≠ si).

theorem Fragments.Italian.Pronouns.tv_distinction : tu.register = Features.Register.Level.informal ∧ lei_formal.register = Features.Register.Level.formal

tu is informal, Lei is formal.

theorem Fragments.Italian.Pronouns.lei_formal_dual_person : lei_formal.person = some UD.Person.third ∧ lei_formal.referentialPerson = some Features.Prominence.PersonLevel.second

Lei has 3rd person agreement features but 2nd person interpretable features. @cite{adamson-zompi-2025}

theorem Fragments.Italian.Pronouns.has_all_persons : (allPronouns.any fun (x : Typology.PronounEntry) => x.person == some UD.Person.first) = true ∧ (allPronouns.any fun (x : Typology.PronounEntry) => x.person == some UD.Person.second) = true ∧ (allPronouns.any fun (x : Typology.PronounEntry) => x.person == some UD.Person.third) = true

All three persons are attested.

theorem Fragments.Italian.Pronouns.has_both_numbers : (allPronouns.any fun (x : Typology.PronounEntry) => x.number == some Number.sg) = true ∧ (allPronouns.any fun (x : Typology.PronounEntry) => x.number == some Number.pl) = true

Both singular and plural are attested.