Pronoun

Lexical core for the pronoun as a grammatical object: the general Pronoun structure (the morphosyntactic core every pronoun type shares), the PersonalPronoun schema for personal/referential pronouns (which extends Pronoun), allocutive markers, and [CS99a]'s Strength deficiency classification.

Cross-categorial features a pronoun carries — person, number, gender, Case — are not redefined here; they live under Features/ and are composed in as fields of the general Pronoun.

Main declarations

• Pronoun — the general pronoun object: surface form + agreement φ-features, everything true of all pronouns. Specializations extends it (mathlib-style: the general concept gets the plain name).
• PersonalPronoun — personal/referential pronoun: extends Pronoun with the register and referential-person features specific to deictic pronouns.
• Pronoun.Strength — [CS99a] strong/weak/clitic deficiency scale, a LinearOrder (clitic < weak < strong), carried per-series by Pronoun.strength. Orthogonal to [DW02]'s categorial pro-DP/φP/NP axis; a framework's structural account of the order stays in its study file.
• Pronoun.AllocutiveEntry — speaker–addressee (allocutive) markers.

Structural deficiency ([CS99a])

inductive Pronoun.Strength : Type

[CS99a]'s three pronoun classes, linearly ordered by structural deficiency: clitic < weak < strong (more structure = greater; C&S's morphological asymmetry is exactly this chain). The classes are structural/distributional — clitic = deficient head, weak = deficient phrase, strong = non-deficient phrase; (un)stressedness is explicitly not the defining property (C&S document stressed deficients and unstressed strongs). Framework-neutral: only the scale lives here; a framework's structural account of it stays in its study file (e.g. [PGG17]), and it is orthogonal to [DW02]'s pro-DP/pro-φP/pro-NP categorial axis. [Cet04] and [JM22] refine the scale four ways (splitting strong into stressed/unstressed); that refinement and its monotone collapse onto this scale live with those studies.

• clitic : Strength

  Deficient and a head (X°) at surface structure: verb-adjacent, clustering, prosodically dependent (Italian lo, French le, Slovak mu). Bottom of the scale.

• weak : Strength

  Deficient but a maximal projection: confined to derived XP positions, non-coordinable, yet a prosodic word of its own (German es, Slovak ono, Italian dative loro).

• strong : Strength

  Non-deficient maximal projection: full structure — coordinable, c-modifiable, possible in θ- and peripheral positions, bears its own range restriction (Italian/French lui, Slovak jemu). Top of the scale.

@[implicit_reducible]

instance Pronoun.instDecidableEqStrength : DecidableEq Strength

Equations

• Pronoun.instDecidableEqStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Pronoun.instReprStrength : Repr Strength

Equations

• Pronoun.instReprStrength = { reprPrec := Pronoun.instReprStrength.repr }

def Pronoun.instReprStrength.repr : Strength → ℕ → Std.Format

Equations

• Pronoun.instReprStrength.repr Pronoun.Strength.clitic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Pronoun.Strength.clitic")).group prec✝
• Pronoun.instReprStrength.repr Pronoun.Strength.weak prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Pronoun.Strength.weak")).group prec✝
• Pronoun.instReprStrength.repr Pronoun.Strength.strong prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Pronoun.Strength.strong")).group prec✝

def Pronoun.Strength.toNat : Strength → ℕ

Numeric embedding into ℕ preserving the deficiency order.

Equations

• Pronoun.Strength.clitic.toNat = 0
• Pronoun.Strength.weak.toNat = 1
• Pronoun.Strength.strong.toNat = 2

@[implicit_reducible]

instance Pronoun.Strength.instLinearOrder : LinearOrder Strength

Equations

• Pronoun.Strength.instLinearOrder = LinearOrder.lift' Pronoun.Strength.toNat Pronoun.Strength.instLinearOrder._proof_1

theorem Pronoun.Strength.clitic_lt_weak : clitic < weak

A clitic is more deficient than a weak pronoun.

theorem Pronoun.Strength.weak_lt_strong : weak < strong

A weak pronoun is more deficient than a strong one.

theorem Pronoun.Strength.clitic_le (s : Strength) : clitic ≤ s

clitic is the most deficient class.

theorem Pronoun.Strength.le_strong (s : Strength) : s ≤ strong

strong is the least deficient class.

structure Pronoun : Type

The general pronoun object: the morphosyntactic core shared by every pronoun type (personal, indefinite, demonstrative, interrogative, …). Carries what is true of all pronouns — surface form, agreement φ-features, and a binding-theoretic bindingClass slot (the Principle A/B/C role every pronoun has; none on the bare base, fixed by the kind: PersonalPronoun defaults it, reflexive/reciprocal shells declare it) — and has no denotation of its own; each specialization (PersonalPronoun for personal/ referential pronouns, and future IndefinitePronoun etc.) extends this and supplies its own meaning. Coexists with namespace Pronoun (a type and a namespace may share a name, cf. List).

• form : String

  Surface form (romanization or orthographic).

• person : Option Person

  Grammatical person — the canonical analytical inventory (root Person). Clusivity is carried as a person value: Tagalog tayo = firstInclusive, kami = firstExclusive; English we = plain first ([Cys09]).

• number : Option Number

  Grammatical number — the canonical analytical inventory (root Number); UD realization via Number.toUD (partial: the minimal/augmented values have no UD tag).

• case_ : Option Case

  Grammatical case.

• gender : Option Gender

  Grammatical gender. For 3rd-person pronouns in gendered languages (French il/elle, German er/sie/es, …). 1st/2nd-person pronouns and languages without pronominal gender leave this none.

• script : Option String

  Native script form (hangul, kanji, Devanagari, …).

• pronType : Option UD.PronType

  Pronoun type (UD PronType): the pro-form's lexical kind — personal (Prs), interrogative (Int), relative (Rel), demonstrative (Dem), … Real UD morphology, threaded onto the projected word by toWord; doubles as the lexical-kind axis the capability tower deferred. Reciprocal (Rcp) is not stored: toWord derives it from bindingClass = .reciprocal. none where unspecified.

• bindingClass : Option Features.BindingClass

  The binding class this pro-form declares — its Features.BindingSource Pronoun value: Principle A anaphor (.reflexive/.reciprocal), B pronominal (.pronoun), or C R-expression. One source of an expression's binding class — the lexical declaration ([Cho81]'s GB classes); the binding engine is polymorphic over BindingSource, so a theory may instead source the class structurally or from context. none for a bare φ-shell.

• strength : Option Strength

  [CS99a] deficiency class of the form-series this entry represents, when the series is homogeneous (an Italian object clitic some .clitic, French lui some .strong). none = unrecorded, or no stable class ([JM22]'s double-duty forms). Consumers condition on some; there is no default class — C&S's deficient-as-default ("Minimize Structure") is a refutable theory claim, not API.

def instReprPronoun.repr : Pronoun → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance instReprPronoun : Repr Pronoun

Equations

• instReprPronoun = { reprPrec := instReprPronoun.repr }

def instBEqPronoun.beq : Pronoun → Pronoun → Bool

Equations

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

@[implicit_reducible]

instance instBEqPronoun : BEq Pronoun

Equations

• instBEqPronoun = { beq := instBEqPronoun.beq }

def instDecidableEqPronoun.decEq (x✝ x✝¹ : Pronoun) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance instDecidableEqPronoun : DecidableEq Pronoun

Equations

• instDecidableEqPronoun = instDecidableEqPronoun.decEq

structure PersonalPronounextends Pronoun : Type

Cross-linguistic personal/referential pronoun: the general Pronoun object (form + φ-features) plus the register and referential-person features specific to deictic pronouns. Covers personal pronouns across all Fragment languages; any language-specific refinements remain in their respective Fragment files.

• form : String
• person : Option Person
• number : Option Number
• case_ : Option Case
• gender : Option Gender
• script : Option String
• pronType : Option UD.PronType
• bindingClass : Option Features.BindingClass
• strength : Option Strength
• register : Features.Register.Level

  Register level (formality/honorifics). Binary T/V systems use .informal/.formal; ternary honorific systems (Hindi, Magahi, Maithili, Korean) use all three levels.

• referentialPerson : Option Person

  Referential person — who the pronoun refers to in terms of discourse role — when it diverges from formal/agreement person. For polite pronouns (Italian LEI, Spanish USTED, German SIE), the formal person field is 3rd (governing agreement, clitic allomorphy, reflexive binding), while referentialPerson is 2nd (governing the PCC, Fancy Constraint, resolved agreement). For ordinary pronouns, leave as none — referential person coincides with formal person. [AZ25a]

def instReprPersonalPronoun.repr : PersonalPronoun → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance instReprPersonalPronoun : Repr PersonalPronoun

Equations

• instReprPersonalPronoun = { reprPrec := instReprPersonalPronoun.repr }

def instBEqPersonalPronoun.beq : PersonalPronoun → PersonalPronoun → Bool

Equations

• instBEqPersonalPronoun.beq { toPronoun := a, register := a_1, referentialPerson := a_2 } { toPronoun := b, register := b_1, referentialPerson := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• instBEqPersonalPronoun.beq x✝¹ x✝ = false

@[implicit_reducible]

instance instBEqPersonalPronoun : BEq PersonalPronoun

Equations

• instBEqPersonalPronoun = { beq := instBEqPersonalPronoun.beq }

@[implicit_reducible]

instance instDecidableEqPersonalPronoun : DecidableEq PersonalPronoun

Equations

• instDecidableEqPersonalPronoun = instDecidableEqPersonalPronoun.decEq

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

Equations

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

Realization as a Word

def Pronoun.toWord (p : Pronoun) : Word

The pronoun realized as a Word: a .PRON-category lexical item carrying the entry's φ-features (person/number/case_). The cross-linguistic realization every pronoun shares; language-specific refinements (e.g. English wh-words that surface as adverbs) stay in the relevant fragment.

Equations

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

Derived person category and well-formedness ([Cys09])

def Pronoun.category (p : Pronoun) : Option Person.Category

The [Cys09] Category this pronoun's person + number realizes, when fully specified — the neutral typological view of its person-reference, derived (not stored). none when person/number is underspecified, or for a clusivity-unmarked first-person plural (plain first, a syncretism over .minIncl/.augIncl/.excl, e.g. English we).

Equations

• p.category = match p.person, p.number with | some per, some num => Person.Category.ofPersonNumber per num | x, x_1 => none

def Pronoun.WellFormed (p : Pronoun) : Prop

Well-formedness of a pronoun's φ-features: clusivity is borne only by a first-person non-singular (dual/plural) form — the inclusive/exclusive split of the 1st-person plural/dual ([Cys09]). This is the invariant a person-value type tower would have enforced, carried as a predicate (the mathlib way) so illegal states are catchable without fragmenting the type.

Equations

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

@[implicit_reducible]

instance Pronoun.instDecidableWellFormed (p : Pronoun) : Decidable p.WellFormed

Equations

• p.instDecidableWellFormed = id inferInstance

Lexical entry schemas ([AB26])

structure Pronoun.AllocutiveEntry : Type

Cross-linguistic allocutive marker entry.

Covers verbal suffixes, particles, and clitics that realize allocutive agreement across all Fragment languages.

• form : String

  Surface form of the marker

• register : Features.Register.Level

  Register level (matching PersonalPronoun.register scale)

• gloss : String

  Gloss string (e.g., "IMP.NH", "POL", "2sg.DAT.fam")

@[implicit_reducible]

instance Pronoun.instReprAllocutiveEntry : Repr AllocutiveEntry

Equations

• Pronoun.instReprAllocutiveEntry = { reprPrec := Pronoun.instReprAllocutiveEntry.repr }

def Pronoun.instReprAllocutiveEntry.repr : AllocutiveEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Pronoun.instBEqAllocutiveEntry : BEq AllocutiveEntry

Equations

• Pronoun.instBEqAllocutiveEntry = { beq := Pronoun.instBEqAllocutiveEntry.beq }

def Pronoun.instBEqAllocutiveEntry.beq : AllocutiveEntry → AllocutiveEntry → Bool

Equations

• Pronoun.instBEqAllocutiveEntry.beq { form := a, register := a_1, gloss := a_2 } { form := b, register := b_1, gloss := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Pronoun.instBEqAllocutiveEntry.beq x✝¹ x✝ = false