def Korean.Pronouns.na : PersonalPronoun

나 na — 1sg plain.

Equations

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

def Korean.Pronouns.jeo : PersonalPronoun

저 jeo — 1sg humble.

Equations

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

def Korean.Pronouns.uri : PersonalPronoun

우리 uri — 1pl.

Equations

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

def Korean.Pronouns.neo : PersonalPronoun

너 neo — 2sg plain.

Equations

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

def Korean.Pronouns.dangsin : PersonalPronoun

당신 dangsin — 2sg polite.

Equations

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

def Korean.Pronouns.geu : PersonalPronoun

그 geu (Yale: ku) — 3sg masculine, literary register. 76,235 written vs 145 oral tokens ([KL26] fn. 2).

Equations

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

def Korean.Pronouns.geunyeo : PersonalPronoun

그녀 geunyeo (Yale: kunye) — 3sg feminine, literary register. Compound of ku ('that') + nye ('female'). 25,085 written vs 9 oral tokens ([KL26] fn. 2).

Equations

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

def Korean.Pronouns.gyae : PersonalPronoun

걔 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 ([KL26] §5). The overt-pronoun referential form tested in [KL26]'s experiments.

Equations

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

def Korean.Pronouns.geudeul : PersonalPronoun

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

Equations

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

def Korean.Pronouns.secondPersonPronouns : List PersonalPronoun

Equations

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

def Korean.Pronouns.thirdPersonPronouns : List PersonalPronoun

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

Equations

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

def Korean.Pronouns.allPronouns : List PersonalPronoun

Equations

• Korean.Pronouns.allPronouns = [Korean.Pronouns.na, Korean.Pronouns.jeo, Korean.Pronouns.uri] ++ Korean.Pronouns.secondPersonPronouns ++ Korean.Pronouns.thirdPersonPronouns

def Korean.Pronouns.yo : Pronoun.AllocutiveEntry

-yo polite particle.

Equations

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

def Korean.Pronouns.supnida : Pronoun.AllocutiveEntry

-(su)pnida formal particle.

Equations

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

def Korean.Pronouns.allAllocParticles : List Pronoun.AllocutiveEntry

Equations

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

structure Korean.Pronouns.VerbForm : Type

A verb form showing speech-level inflection.

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

@[implicit_reducible]

instance Korean.Pronouns.instReprVerbForm : Repr VerbForm

Equations

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

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

Equations

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

@[implicit_reducible]

instance Korean.Pronouns.instBEqVerbForm : BEq VerbForm

Equations

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

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

Equations

• 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))
• Korean.Pronouns.instBEqVerbForm.beq x✝¹ x✝ = false

def Korean.Pronouns.ga : VerbForm

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

Equations

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

def Korean.Pronouns.gayo : VerbForm

가요 gayo — "go" (polite).

Equations

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

def Korean.Pronouns.gamnida : VerbForm

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

Equations

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

theorem Korean.Pronouns.has_all_persons : (allPronouns.any fun (x : PersonalPronoun) => x.person == some Person.first) = true ∧ (allPronouns.any fun (x : PersonalPronoun) => x.person == some Person.second) = true ∧ (allPronouns.any fun (x : PersonalPronoun) => x.person == some Person.third) = true

All three persons are attested.

theorem Korean.Pronouns.has_both_numbers : (allPronouns.any fun (x : PersonalPronoun) => x.number == some Number.singular) = true ∧ (allPronouns.any fun (x : PersonalPronoun) => x.number == some Number.plural) = true

Both singular and plural are attested.

theorem 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 Korean.Pronouns.second_person_all_2p : (secondPersonPronouns.all fun (x : PersonalPronoun) => x.person == some Person.second) = true

2nd person pronouns are all second person.

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

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

theorem 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 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 ([KL26] fn. 2).

theorem Korean.Pronouns.gyae_gender_neutral : gyae.gender = none ∧ geu.gender = some Gender.masculine ∧ geunyeo.gender = some Gender.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.