Personal pronouns

A personal pronoun is a pronoun with a register and the referential categories it denotes. The categories are by default those its agreement person and number realize. A polite pronoun overrides the default: Italian Lei and German Sie agree as third person and denote the addressee, so their formal features govern agreement, clitic allomorphy and reflexive binding while their referential categories govern the person-case constraint and resolved agreement.

A pronoun records only features whose values are shared across languages. Honorific grades are not: each language has its own, ordered by the deference they present, and a form may serve several, as Maithili tõ is both the nonhonorific and the mid-honorific second person. A fragment therefore states its grades as a type and its pronouns as a paradigm over them, a function from grades to entries like the tables the grammars print. The grades a form serves are a preimage of that function, its syncretisms the kernel, and paradigms are compared across languages by shape.

Main definitions

• PersonalPronoun — a pronoun with its register and referential categories
• PersonalPronoun.referentialPerson, PersonalPronoun.referentialNumber — the person and number the pronoun contributes to interpretation
• PersonalPronoun.IsOrdinary — the pronoun denotes what its agreement features realize
• PersonalPronoun.paradigm — the forms an inventory offers for each referential category, whose kernel Setoid.ker is the inventory's person-number syncretism

Main results

• PersonalPronoun.referentialPerson_eq_person — an ordinary pronoun's referential person is its agreement person
• PersonalPronoun.bindingClassOf_toWord — a personal pronoun is a pronominal

References

• L. J. Adamson and S. Zompì, Polite Pronouns and the PCC (2025)
• M. Cysouw, The Paradigmatic Structure of Person Marking (2003)
• P. Kumari and P. Chandra, Honorificity Feature as an Enabler: Bridging the Person Gap (2026)

structure PersonalPronounextends Pronoun : Type

A personal pronoun is a Pronoun with its register and the referential categories it denotes.

• form : String
• person : Option Person
• number : Option Number
• case_ : Option Case
• gender : Option Gender
• script : Option String
• strength : Option Strength
• register : SocialMeaning.Register

  The register. Japanese boku is an informal first person, and Korean geu a third person of written narrative.

• referential : Finset Person.Category

  The referential categories the pronoun can denote, by default those its agreement person and number realize. Italian Lei denotes {addressee} and German Sie {addressee, addresseeOthers} ([AZ25a]).

def instDecidableEqPersonalPronoun.decEq (x✝ x✝¹ : PersonalPronoun) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance instDecidableEqPersonalPronoun : DecidableEq PersonalPronoun

Equations

• instDecidableEqPersonalPronoun = instDecidableEqPersonalPronoun.decEq

@[instance_reducible]

instance PersonalPronoun.instHasPhi : HasPhi PersonalPronoun

Equations

• PersonalPronoun.instHasPhi = { phi := fun (p : PersonalPronoun) => p.phi }

def PersonalPronoun.referentialPerson (p : PersonalPronoun) : Option Person

The person a pronoun contributes to interpretation: the one its referential categories share.

Equations

• p.referentialPerson = Person.Category.sharedPerson p.referential

def PersonalPronoun.referentialNumber (p : PersonalPronoun) : Option Number

The number a pronoun contributes to interpretation: the one its referential categories share, general for a number-neutral form such as polite Sie.

Equations

• p.referentialNumber = Person.Category.sharedNumber p.referential

def PersonalPronoun.IsOrdinary (p : PersonalPronoun) : Prop

An ordinary pronoun denotes exactly the categories its agreement features realize.

Equations

• p.IsOrdinary = (p.referential = p.categories)

@[instance_reducible]

instance PersonalPronoun.instDecidableIsOrdinary {p : PersonalPronoun} : Decidable p.IsOrdinary

Equations

• PersonalPronoun.instDecidableIsOrdinary = { decide := decide (p.referential.val = p.categories.val), reflects_decide := ⋯ }

theorem PersonalPronoun.referentialPerson_eq_person {p : PersonalPronoun} (h : p.IsOrdinary) (hne : p.referential.Nonempty) : p.referentialPerson = p.person

An ordinary pronoun's referential person is its agreement person.

The paradigm of an inventory

def PersonalPronoun.paradigm : Finset PersonalPronoun → Person.Category → Finset String

The paradigm of an inventory assigns each referential category the forms the inventory offers for it. A category no pronoun denotes gets ∅, and two categories receive the same forms exactly when the inventory does not distinguish them.

Equations

• PersonalPronoun.paradigm = Morphology.formsAt (fun (x : PersonalPronoun) => x.referential) fun (x : PersonalPronoun) => x.form

theorem PersonalPronoun.mem_paradigm {I : Finset PersonalPronoun} {c : Person.Category} {f : String} : f ∈ paradigm I c ↔ ∃ p ∈ I, c ∈ p.referential ∧ p.form = f

theorem PersonalPronoun.paradigm_mono {I J : Finset PersonalPronoun} (h : I ⊆ J) (c : Person.Category) : paradigm I c ⊆ paradigm J c

The pronoun as a token

def PersonalPronoun.toWord (p : PersonalPronoun) : Morphology.Word

A personal pronoun's token is of UD pronoun type Prs.

Equations

• p.toWord = p.toWord (some UD.PronType.Prs)

@[simp]

theorem PersonalPronoun.bindingClassOf_toWord (p : PersonalPronoun) : Binding.bindingClassOf p.toWord = some Binding.BindingClass.pronoun

A personal pronoun is a pronominal.