inductive Fragments.English.Pronouns.GenderParadigm : Type

English pronominal gender paradigm.

Each paradigm class groups the personal and reflexive pronouns that must agree in gender. Used for binding agreement (Principle A/B).

Epicene covers singular they/them/themself — animate referents whose gender is either unspecified in the discourse or whose personal pronouns are they/them. This replaces the earlier .plural constructor, which incorrectly conflated number (plural) with gender (ungendered). Singular they has been attested since Middle English (@cite{balhorn-2004}); @cite{arnold-2026} distinguishes two pragmatic uses (underspecified vs. personal).

• masculine : GenderParadigm
• feminine : GenderParadigm
• neuter : GenderParadigm
• epicene : GenderParadigm
• unspecified : GenderParadigm

@[implicit_reducible]

instance Fragments.English.Pronouns.instDecidableEqGenderParadigm : DecidableEq GenderParadigm

Equations

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

def Fragments.English.Pronouns.instReprGenderParadigm.repr : GenderParadigm → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.English.Pronouns.instReprGenderParadigm : Repr GenderParadigm

Equations

• Fragments.English.Pronouns.instReprGenderParadigm = { reprPrec := Fragments.English.Pronouns.instReprGenderParadigm.repr }

def Fragments.English.Pronouns.GenderParadigm.toSurfaceGender : GenderParadigm → Option Features.SurfaceGender

Coarsening from English gender paradigm to cross-linguistic surface gender. Returns none for epicene (no single SurfaceGender for animate-ungendered) and unspecified.

Equations

• Fragments.English.Pronouns.GenderParadigm.masculine.toSurfaceGender = some Features.SurfaceGender.masculine
• Fragments.English.Pronouns.GenderParadigm.feminine.toSurfaceGender = some Features.SurfaceGender.feminine
• Fragments.English.Pronouns.GenderParadigm.neuter.toSurfaceGender = some Features.SurfaceGender.neuter
• Fragments.English.Pronouns.GenderParadigm.epicene.toSurfaceGender = none
• Fragments.English.Pronouns.GenderParadigm.unspecified.toSurfaceGender = none

def Fragments.English.Pronouns.Typology.PronounSpec.toGenderParadigm : Typology.PronounSpec → GenderParadigm

Map a personal pronoun specification to its English gender paradigm.

Equations

• Fragments.English.Pronouns.Typology.PronounSpec.toGenderParadigm Typology.PronounSpec.heHim = Fragments.English.Pronouns.GenderParadigm.masculine
• Fragments.English.Pronouns.Typology.PronounSpec.toGenderParadigm Typology.PronounSpec.sheHer = Fragments.English.Pronouns.GenderParadigm.feminine
• Fragments.English.Pronouns.Typology.PronounSpec.toGenderParadigm Typology.PronounSpec.theyThem = Fragments.English.Pronouns.GenderParadigm.epicene

inductive Fragments.English.Pronouns.PronounType : Type

Type of pronoun.

• personal : PronounType
• reflexive : PronounType
• reciprocal : PronounType
• wh : PronounType
• relative : PronounType
• demonstrative : PronounType

@[implicit_reducible]

instance Fragments.English.Pronouns.instDecidableEqPronounType : DecidableEq PronounType

Equations

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

@[implicit_reducible]

instance Fragments.English.Pronouns.instReprPronounType : Repr PronounType

Equations

• Fragments.English.Pronouns.instReprPronounType = { reprPrec := Fragments.English.Pronouns.instReprPronounType.repr }

def Fragments.English.Pronouns.instReprPronounType.repr : PronounType → ℕ → Std.Format

Equations

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

structure Fragments.English.Pronouns.PronounEntry : Type

A lexical entry for a pronoun.

• form : String

  Surface form

• pronounType : PronounType

  Pronoun type

• person : Option Person

  Person (for personal/reflexive)

• number : Option Number

  Number

• case_ : Option Case

  Case (for personal pronouns)

• genderParadigm : Option GenderParadigm

  Gender paradigm class (3rd-person singular agreement). Epicene covers singular they; none for 1st/2nd person, reciprocals, and wh-pronouns.

• wh : Bool

  Is this a wh-word?

@[implicit_reducible]

instance Fragments.English.Pronouns.instReprPronounEntry : Repr PronounEntry

Equations

• Fragments.English.Pronouns.instReprPronounEntry = { reprPrec := Fragments.English.Pronouns.instReprPronounEntry.repr }

def Fragments.English.Pronouns.instReprPronounEntry.repr : PronounEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.English.Pronouns.instBEqPronounEntry : BEq PronounEntry

Equations

• Fragments.English.Pronouns.instBEqPronounEntry = { beq := Fragments.English.Pronouns.instBEqPronounEntry.beq }

def Fragments.English.Pronouns.instBEqPronounEntry.beq : PronounEntry → PronounEntry → Bool

Equations

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

def Fragments.English.Pronouns.i : PronounEntry

Equations

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

def Fragments.English.Pronouns.me : PronounEntry

Equations

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

def Fragments.English.Pronouns.we : PronounEntry

Equations

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

def Fragments.English.Pronouns.us : PronounEntry

Equations

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

def Fragments.English.Pronouns.you : PronounEntry

Equations

• Fragments.English.Pronouns.you = { form := "you", pronounType := Fragments.English.Pronouns.PronounType.personal, person := some UD.Person.second, number := some Number.sg }

def Fragments.English.Pronouns.you_pl : PronounEntry

Equations

• Fragments.English.Pronouns.you_pl = { form := "you", pronounType := Fragments.English.Pronouns.PronounType.personal, person := some UD.Person.second, number := some Number.pl }

def Fragments.English.Pronouns.he : PronounEntry

Equations

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

def Fragments.English.Pronouns.him : PronounEntry

Equations

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

def Fragments.English.Pronouns.she : PronounEntry

Equations

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

def Fragments.English.Pronouns.her : PronounEntry

Equations

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

def Fragments.English.Pronouns.it : PronounEntry

Equations

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

def Fragments.English.Pronouns.they : PronounEntry

Equations

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

def Fragments.English.Pronouns.them : PronounEntry

Equations

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

def Fragments.English.Pronouns.they_sg : PronounEntry

Equations

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

def Fragments.English.Pronouns.them_sg : PronounEntry

Equations

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

def Fragments.English.Pronouns.myself : PronounEntry

Equations

• Fragments.English.Pronouns.myself = { form := "myself", pronounType := Fragments.English.Pronouns.PronounType.reflexive, person := some UD.Person.first, number := some Number.sg }

def Fragments.English.Pronouns.yourself : PronounEntry

Equations

• Fragments.English.Pronouns.yourself = { form := "yourself", pronounType := Fragments.English.Pronouns.PronounType.reflexive, person := some UD.Person.second, number := some Number.sg }

def Fragments.English.Pronouns.himself : PronounEntry

Equations

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

def Fragments.English.Pronouns.herself : PronounEntry

Equations

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

def Fragments.English.Pronouns.itself : PronounEntry

Equations

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

def Fragments.English.Pronouns.ourselves : PronounEntry

Equations

• Fragments.English.Pronouns.ourselves = { form := "ourselves", pronounType := Fragments.English.Pronouns.PronounType.reflexive, person := some UD.Person.first, number := some Number.pl }

def Fragments.English.Pronouns.yourselves : PronounEntry

Equations

• Fragments.English.Pronouns.yourselves = { form := "yourselves", pronounType := Fragments.English.Pronouns.PronounType.reflexive, person := some UD.Person.second, number := some Number.pl }

def Fragments.English.Pronouns.themselves : PronounEntry

Equations

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

def Fragments.English.Pronouns.themself : PronounEntry

Equations

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

def Fragments.English.Pronouns.eachOther : PronounEntry

Equations

• Fragments.English.Pronouns.eachOther = { form := "each other", pronounType := Fragments.English.Pronouns.PronounType.reciprocal }

def Fragments.English.Pronouns.oneAnother : PronounEntry

Equations

• Fragments.English.Pronouns.oneAnother = { form := "one another", pronounType := Fragments.English.Pronouns.PronounType.reciprocal }

def Fragments.English.Pronouns.who : PronounEntry

Equations

• Fragments.English.Pronouns.who = { form := "who", pronounType := Fragments.English.Pronouns.PronounType.wh, wh := true }

def Fragments.English.Pronouns.whom : PronounEntry

Equations

• Fragments.English.Pronouns.whom = { form := "whom", pronounType := Fragments.English.Pronouns.PronounType.wh, case_ := some UD.Case.acc, wh := true }

def Fragments.English.Pronouns.what : PronounEntry

Equations

• Fragments.English.Pronouns.what = { form := "what", pronounType := Fragments.English.Pronouns.PronounType.wh, wh := true }

def Fragments.English.Pronouns.which : PronounEntry

Equations

• Fragments.English.Pronouns.which = { form := "which", pronounType := Fragments.English.Pronouns.PronounType.wh, wh := true }

def Fragments.English.Pronouns.where_ : PronounEntry

Equations

• Fragments.English.Pronouns.where_ = { form := "where", pronounType := Fragments.English.Pronouns.PronounType.wh, wh := true }

def Fragments.English.Pronouns.when_ : PronounEntry

Equations

• Fragments.English.Pronouns.when_ = { form := "when", pronounType := Fragments.English.Pronouns.PronounType.wh, wh := true }

def Fragments.English.Pronouns.why : PronounEntry

Equations

• Fragments.English.Pronouns.why = { form := "why", pronounType := Fragments.English.Pronouns.PronounType.wh, wh := true }

def Fragments.English.Pronouns.how : PronounEntry

Equations

• Fragments.English.Pronouns.how = { form := "how", pronounType := Fragments.English.Pronouns.PronounType.wh, wh := true }

def Fragments.English.Pronouns.genderOf (form : String) : GenderParadigm

Map a pronoun form to its gender paradigm.

Equations

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

def Fragments.English.Pronouns.nameGender (form : String) : GenderParadigm

Map a proper noun to its gender paradigm, if known. Returns .unspecified for unknown names.

Equations

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

def Fragments.English.Pronouns.genderAgrees (form1 form2 : String) : Bool

Do two forms agree in gender? Unspecified gender agrees with anything.

Equations

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

def Fragments.English.Pronouns.PronounEntry.isWhAdverb (p : PronounEntry) : Bool

Is this a wh-adverb (where, when, why, how) rather than a wh-pronoun?

Equations

• p.isWhAdverb = decide (p.form ∈ ["where", "when", "why", "how"])

def Fragments.English.Pronouns.PronounEntry.toWord (p : PronounEntry) : Word

Equations

• p.toWord = { form := p.form, cat := if p.isWhAdverb = true then UD.UPOS.ADV else UD.UPOS.PRON, features := { wh := p.wh, number := p.number, person := p.person, case_ := p.case_ } }

def Fragments.English.Pronouns.allPronouns : List PronounEntry

Equations

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

def Fragments.English.Pronouns.lookup (form : String) : Option PronounEntry

Equations

• Fragments.English.Pronouns.lookup form = List.find? (fun (p : Fragments.English.Pronouns.PronounEntry) => p.form == form) Fragments.English.Pronouns.allPronouns

theorem Fragments.English.Pronouns.he_gender_consistent : he.genderParadigm = some (genderOf "he")

Every 3rd-person pronoun's structural genderParadigm field agrees with the string-based genderOf function. This makes the field redundant for these forms but proves the two representations are consistent — future code can use either.

theorem Fragments.English.Pronouns.she_gender_consistent : she.genderParadigm = some (genderOf "she")

theorem Fragments.English.Pronouns.it_gender_consistent : it.genderParadigm = some (genderOf "it")

theorem Fragments.English.Pronouns.they_gender_consistent : they.genderParadigm = some (genderOf "they")

theorem Fragments.English.Pronouns.they_sg_gender_consistent : they_sg.genderParadigm = some (genderOf "they")

theorem Fragments.English.Pronouns.themself_gender_consistent : themself.genderParadigm = some (genderOf "themself")

theorem Fragments.English.Pronouns.sg_pl_same_gender : they_sg.genderParadigm = they.genderParadigm

Singular and plural they share the same gender paradigm despite differing in number. This is the structural correlate of Arnold's observation that underspecified and personal they share phonological form and the ungendered morphosyntactic feature.

def Fragments.English.pronounProfile : Typology.PronounProfile

English (Indo-European, Germanic) WALS pronoun typology profile. No incl/excl; gender in 3rd sg only (he/she/it); no politeness; generic-noun-based indefinites (somebody, something); intensifier and reflexive identical (himself); no person marking on adpositions. (WALS Chs 39, 40, 44–48.)

Equations

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

def Fragments.English.pronounShapeProfile : Typology.PronounShapeProfile

English pronoun phonological shape (WALS Chs 136–137, @cite{nichols-peterson-2013}): no M-T pattern (1SG I/me, 2SG you), but 1SG has /m/ in me/my; no N-M pattern; no /m/ in 2SG.

Equations

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