Documentation

Linglib.Fragments.Italian.Pronouns

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 :

Core.Pronouns.PronounEntry

io — 1sg.

Equations

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

Instances For

def Fragments.Italian.Pronouns.tu :

Core.Pronouns.PronounEntry

tu — 2sg familiar (T form).

Equations

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

Instances For

def Fragments.Italian.Pronouns.lei_formal :

Core.Pronouns.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.

Instances For

def Fragments.Italian.Pronouns.lui :

Core.Pronouns.PronounEntry

lui — 3sg masculine.

Equations

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

Instances For

def Fragments.Italian.Pronouns.lei :

Core.Pronouns.PronounEntry

lei — 3sg feminine.

Equations

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

Instances For

def Fragments.Italian.Pronouns.noi :

Core.Pronouns.PronounEntry

noi — 1pl.

Equations

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

Instances For

def Fragments.Italian.Pronouns.voi :

Core.Pronouns.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 }

Instances For

def Fragments.Italian.Pronouns.loro_formal :

Core.Pronouns.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 := Core.Register.Level.formal }

Instances For

def Fragments.Italian.Pronouns.loro :

Core.Pronouns.PronounEntry

loro — 3pl.

Equations

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

Instances For

def Fragments.Italian.Pronouns.secondPersonPronouns :

List Core.Pronouns.PronounEntry

Equations

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

Instances For

def Fragments.Italian.Pronouns.allPronouns :

List Core.Pronouns.PronounEntry

Equations

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

Instances For

inductive Fragments.Italian.Pronouns.CliticCase :

The three-way case distinction for Italian clitics.

accusative : CliticCase
dative : CliticCase
reflexive : CliticCase

Instances For

instance Fragments.Italian.Pronouns.instDecidableEqCliticCase :

DecidableEq CliticCase

Equations

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

instance Fragments.Italian.Pronouns.instBEqCliticCase :

Equations

Fragments.Italian.Pronouns.instBEqCliticCase = { beq := Fragments.Italian.Pronouns.instBEqCliticCase.beq }

def Fragments.Italian.Pronouns.instBEqCliticCase.beq :

CliticCase → CliticCase → Bool

Equations

Fragments.Italian.Pronouns.instBEqCliticCase.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Fragments.Italian.Pronouns.instReprCliticCase :

Repr CliticCase

Equations

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

def Fragments.Italian.Pronouns.instReprCliticCase.repr :

CliticCase → ℕ → Std.Format

Equations

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

Instances For

structure Fragments.Italian.Pronouns.CliticEntry :

A single clitic form in the paradigm.

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

Instances For

def Fragments.Italian.Pronouns.instReprCliticEntry.repr :

CliticEntry → ℕ → Std.Format

Equations

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

Instances For

instance Fragments.Italian.Pronouns.instReprCliticEntry :

Repr CliticEntry

Equations

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

instance Fragments.Italian.Pronouns.instBEqCliticEntry :

BEq CliticEntry

Equations

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

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

Instances For

def Fragments.Italian.Pronouns.mi_acc :

Equations

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

Instances For

def Fragments.Italian.Pronouns.mi_dat :

Equations

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

Instances For

def Fragments.Italian.Pronouns.mi_refl :

Equations

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

Instances For

def Fragments.Italian.Pronouns.ti_acc :

Equations

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

Instances For

def Fragments.Italian.Pronouns.ti_dat :

Equations

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

Instances For

def Fragments.Italian.Pronouns.ti_refl :

Equations

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

Instances For

def Fragments.Italian.Pronouns.lo_cl :

Equations

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

Instances For

def Fragments.Italian.Pronouns.la_cl :

Equations

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

Instances For

def Fragments.Italian.Pronouns.gli_dat :

Equations

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

Instances For

def Fragments.Italian.Pronouns.le_dat :

Equations

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

Instances For

def Fragments.Italian.Pronouns.si_refl :

Equations

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

Instances For

def Fragments.Italian.Pronouns.ci_acc :

Equations

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

Instances For

def Fragments.Italian.Pronouns.ci_dat :

Equations

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

Instances For

def Fragments.Italian.Pronouns.ci_refl :

Equations

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

Instances For

def Fragments.Italian.Pronouns.vi_acc :

Equations

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

Instances For

def Fragments.Italian.Pronouns.vi_dat :

Equations

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

Instances For

def Fragments.Italian.Pronouns.vi_refl :

Equations

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

Instances For

def Fragments.Italian.Pronouns.li_cl :

Equations

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

Instances For

def Fragments.Italian.Pronouns.le_cl :

Equations

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

Instances For

def Fragments.Italian.Pronouns.loro_dat :

Equations

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

Instances For

def Fragments.Italian.Pronouns.si_refl_pl :

Equations

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

Instances For

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.

Instances For

def Fragments.Italian.Pronouns.lookupForm (p : Person) (n : Number) (c : CliticCase) :

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.

Instances For

def Fragments.Italian.Pronouns.isSyncretic (p : Person) (n : Number) (c1 c2 : CliticCase) :

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.

Instances For

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

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

Instances For

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 = Core.Register.Level.informal ∧ lei_formal.register = Core.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 Core.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 : Core.Pronouns.PronounEntry) => x.person == some UD.Person.first) = true ∧ (allPronouns.any fun (x : Core.Pronouns.PronounEntry) => x.person == some UD.Person.second) = true ∧ (allPronouns.any fun (x : Core.Pronouns.PronounEntry) => x.person == some UD.Person.third) = true

All three persons are attested.

theorem Fragments.Italian.Pronouns.has_both_numbers :

(allPronouns.any fun (x : Core.Pronouns.PronounEntry) => x.number == some Number.sg) = true ∧ (allPronouns.any fun (x : Core.Pronouns.PronounEntry) => x.number == some Number.pl) = true

Both singular and plural are attested.