def Fragments.Korean.Pronouns.na : Typology.PronounEntry

나 na — 1sg plain.

Equations

• Fragments.Korean.Pronouns.na = { form := "na", person := some UD.Person.first, number := some Number.sg, script := some "나" }

def Fragments.Korean.Pronouns.jeo : Typology.PronounEntry

저 jeo — 1sg humble.

Equations

• Fragments.Korean.Pronouns.jeo = { form := "jeo", person := some UD.Person.first, number := some Number.sg, register := Features.Register.Level.formal, script := some "저" }

def Fragments.Korean.Pronouns.uri : Typology.PronounEntry

우리 uri — 1pl.

Equations

• Fragments.Korean.Pronouns.uri = { form := "uri", person := some UD.Person.first, number := some Number.pl, script := some "우리" }

def Fragments.Korean.Pronouns.neo : Typology.PronounEntry

너 neo — 2sg plain.

Equations

• Fragments.Korean.Pronouns.neo = { form := "neo", person := some UD.Person.second, number := some Number.sg, script := some "너" }

def Fragments.Korean.Pronouns.dangsin : Typology.PronounEntry

당신 dangsin — 2sg polite.

Equations

• Fragments.Korean.Pronouns.dangsin = { form := "dangsin", person := some UD.Person.second, number := some Number.sg, register := Features.Register.Level.formal, script := some "당신" }

def Fragments.Korean.Pronouns.geu : Typology.PronounEntry

그 geu (Yale: ku) — 3sg masculine, literary register. 76,235 written vs 145 oral tokens (@cite{kwon-lee-2026} fn. 2).

Equations

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

def Fragments.Korean.Pronouns.geunyeo : Typology.PronounEntry

그녀 geunyeo (Yale: kunye) — 3sg feminine, literary register. Compound of ku ('that') + nye ('female'). 25,085 written vs 9 oral tokens (@cite{kwon-lee-2026} fn. 2).

Equations

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

def Fragments.Korean.Pronouns.gyae : Typology.PronounEntry

걔 gyae (Yale: kyay) — 3sg gender-neutral, colloquial pronoun. Contracted from ku ay ('that' + contracted ai 'child'). 1,160 oral vs 226 written tokens — the reverse register pattern of geu/geunyeo. Implies familiarity between speaker and referent (@cite{kwon-lee-2026} §5). The overt-pronoun referential form tested in @cite{kwon-lee-2026}'s experiments.

Equations

• Fragments.Korean.Pronouns.gyae = { form := "gyae", person := some UD.Person.third, number := some Number.sg, script := some "걔" }

def Fragments.Korean.Pronouns.geudeul : Typology.PronounEntry

그들 geudeul — 3pl. Plural of geu; literary in register (the colloquial plural is the proximal demonstrative + ai-tul).

Equations

• Fragments.Korean.Pronouns.geudeul = { form := "geudeul", person := some UD.Person.third, number := some Number.pl, register := Features.Register.Level.formal, script := some "그들" }

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

Equations

• Fragments.Korean.Pronouns.secondPersonPronouns = [Fragments.Korean.Pronouns.neo, Fragments.Korean.Pronouns.dangsin]

def Fragments.Korean.Pronouns.thirdPersonPronouns : List Typology.PronounEntry

3rd-person pronouns: literary geu/geunyeo/geudeul and colloquial gyae. Yale-romanization variants (ku/kunye/kutul/ kyay) refer to the same lexical items.

Equations

• Fragments.Korean.Pronouns.thirdPersonPronouns = [Fragments.Korean.Pronouns.geu, Fragments.Korean.Pronouns.geunyeo, Fragments.Korean.Pronouns.geudeul, Fragments.Korean.Pronouns.gyae]

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

Equations

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

def Fragments.Korean.Pronouns.yo : Typology.AllocutiveEntry

-yo polite particle.

Equations

• Fragments.Korean.Pronouns.yo = { form := "-yo", register := Features.Register.Level.neutral, gloss := "POL" }

def Fragments.Korean.Pronouns.supnida : Typology.AllocutiveEntry

-(su)pnida formal particle.

Equations

• Fragments.Korean.Pronouns.supnida = { form := "-(su)pnida", register := Features.Register.Level.formal, gloss := "FORM" }

def Fragments.Korean.Pronouns.allAllocParticles : List Typology.AllocutiveEntry

Equations

• Fragments.Korean.Pronouns.allAllocParticles = [Fragments.Korean.Pronouns.yo, Fragments.Korean.Pronouns.supnida]

structure Fragments.Korean.Pronouns.VerbForm : Type

A verb form showing speech-level inflection.

• form : String
• gloss : String
• register : Features.Register.Level

@[implicit_reducible]

instance Fragments.Korean.Pronouns.instReprVerbForm : Repr VerbForm

Equations

• Fragments.Korean.Pronouns.instReprVerbForm = { reprPrec := Fragments.Korean.Pronouns.instReprVerbForm.repr }

def Fragments.Korean.Pronouns.instReprVerbForm.repr : VerbForm → ℕ → Std.Format

Equations

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

def Fragments.Korean.Pronouns.instBEqVerbForm.beq : VerbForm → VerbForm → Bool

Equations

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

@[implicit_reducible]

instance Fragments.Korean.Pronouns.instBEqVerbForm : BEq VerbForm

Equations

• Fragments.Korean.Pronouns.instBEqVerbForm = { beq := Fragments.Korean.Pronouns.instBEqVerbForm.beq }

def Fragments.Korean.Pronouns.ga : VerbForm

가 ga — "go" (plain/intimate).

Equations

• Fragments.Korean.Pronouns.ga = { form := "ga", gloss := "go.PLN", register := Features.Register.Level.informal }

def Fragments.Korean.Pronouns.gayo : VerbForm

가요 gayo — "go" (polite).

Equations

• Fragments.Korean.Pronouns.gayo = { form := "gayo", gloss := "go.POL", register := Features.Register.Level.neutral }

def Fragments.Korean.Pronouns.gamnida : VerbForm

갑니다 gamnida — "go" (formal).

Equations

• Fragments.Korean.Pronouns.gamnida = { form := "gamnida", gloss := "go.FORM", register := Features.Register.Level.formal }

theorem Fragments.Korean.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.Korean.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.

theorem Fragments.Korean.Pronouns.first_person_humble : na.register = Features.Register.Level.informal ∧ jeo.register = Features.Register.Level.formal

1st person has plain/humble register distinction.

theorem Fragments.Korean.Pronouns.second_person_all_2p : (secondPersonPronouns.all fun (x : Typology.PronounEntry) => x.person == some UD.Person.second) = true

2nd person pronouns are all second person.

theorem Fragments.Korean.Pronouns.tv_distinction : (secondPersonPronouns.any fun (x : Typology.PronounEntry) => x.register == Features.Register.Level.informal) = true ∧ (secondPersonPronouns.any fun (x : Typology.PronounEntry) => x.register == Features.Register.Level.formal) = true

The T/V register distinction is present in 2nd person.

theorem Fragments.Korean.Pronouns.verb_three_levels : ga.register = Features.Register.Level.informal ∧ gayo.register = Features.Register.Level.neutral ∧ gamnida.register = Features.Register.Level.formal

Verb forms span all three speech levels.

theorem Fragments.Korean.Pronouns.third_person_register_split : gyae.register = Features.Register.Level.informal ∧ geu.register = Features.Register.Level.formal ∧ geunyeo.register = Features.Register.Level.formal ∧ geudeul.register = Features.Register.Level.formal

3rd-person pronouns split by register: gyae is colloquial, geu/geunyeo/geudeul are literary (@cite{kwon-lee-2026} fn. 2).

theorem Fragments.Korean.Pronouns.gyae_gender_neutral : gyae.gender = none ∧ geu.gender = some Features.SurfaceGender.masculine ∧ geunyeo.gender = some Features.SurfaceGender.feminine

gyae is gender-neutral; geu/geunyeo are gendered. This is the central asymmetry of the Korean 3rd-person system: the colloquial pronoun lacks the gender contrast carried by the literary forms.

def Fragments.Korean.pronounProfile : Typology.PronounProfile

Korean (Koreanic) WALS pronoun typology profile. No incl/excl; no person marking on verbs; gender in 3rd sg only (geu/geunyeo); pronouns avoided for politeness (elaborate honorific system uses titles/names instead); interrogative-based indefinites (nuguinka from nugu 'who'); intensifier and reflexive identical (caki); no person marking on adpositions.

Equations

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

def Fragments.Korean.pronounShapeProfile : Typology.PronounShapeProfile

Korean pronoun phonological shape (WALS Chs 136–137): no M-T; no /m/ in 1SG (na/jeo); no N-M; no /m/ in 2SG.

Equations

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