def Fragments.Japanese.Pronouns.watashi : Core.Pronouns.PronounEntry

私 watashi — 1sg neutral/polite.

Equations

• Fragments.Japanese.Pronouns.watashi = { form := "watashi", person := some UD.Person.first, number := some Number.sg, register := Core.Register.Level.formal, script := some "私" }

def Fragments.Japanese.Pronouns.boku : Core.Pronouns.PronounEntry

僕 boku — 1sg male informal.

Equations

• Fragments.Japanese.Pronouns.boku = { form := "boku", person := some UD.Person.first, number := some Number.sg, script := some "僕" }

def Fragments.Japanese.Pronouns.watashitachi : Core.Pronouns.PronounEntry

私たち watashitachi — 1pl.

Equations

• Fragments.Japanese.Pronouns.watashitachi = { form := "watashitachi", person := some UD.Person.first, number := some Number.pl, script := some "私たち" }

def Fragments.Japanese.Pronouns.kimi : Core.Pronouns.PronounEntry

君 kimi — 2sg plain.

Equations

• Fragments.Japanese.Pronouns.kimi = { form := "kimi", person := some UD.Person.second, number := some Number.sg, script := some "君" }

def Fragments.Japanese.Pronouns.anata : Core.Pronouns.PronounEntry

あなた anata — 2sg polite.

Equations

• Fragments.Japanese.Pronouns.anata = { form := "anata", person := some UD.Person.second, number := some Number.sg, register := Core.Register.Level.formal, script := some "あなた" }

def Fragments.Japanese.Pronouns.kare : Core.Pronouns.PronounEntry

彼 kare — 3sg masculine.

Equations

• Fragments.Japanese.Pronouns.kare = { form := "kare", person := some UD.Person.third, number := some Number.sg, script := some "彼" }

def Fragments.Japanese.Pronouns.kanojo : Core.Pronouns.PronounEntry

彼女 kanojo — 3sg feminine.

Equations

• Fragments.Japanese.Pronouns.kanojo = { form := "kanojo", person := some UD.Person.third, number := some Number.sg, script := some "彼女" }

def Fragments.Japanese.Pronouns.karera : Core.Pronouns.PronounEntry

彼ら karera — 3pl.

Equations

• Fragments.Japanese.Pronouns.karera = { form := "karera", person := some UD.Person.third, number := some Number.pl, script := some "彼ら" }

def Fragments.Japanese.Pronouns.otagai : Core.Pronouns.PronounEntry

互い otagai — reciprocal pronoun 'each other, one another'. Formally distinct from the reflexive jibun (自分). This is an NP/argument reciprocal strategy (reciprocal pronoun), unlike languages that mark reciprocity on the verb.

Equations

• Fragments.Japanese.Pronouns.otagai = { form := "otagai", person := some UD.Person.third, number := some Number.pl, script := some "互い" }

def Fragments.Japanese.Pronouns.secondPersonPronouns : List Core.Pronouns.PronounEntry

Equations

• Fragments.Japanese.Pronouns.secondPersonPronouns = [Fragments.Japanese.Pronouns.kimi, Fragments.Japanese.Pronouns.anata]

def Fragments.Japanese.Pronouns.allPronouns : List Core.Pronouns.PronounEntry

Equations

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

def Fragments.Japanese.Pronouns.desuMasu : Core.Pronouns.AllocutiveEntry

-desu polite copula / -masu polite verbal.

Equations

• Fragments.Japanese.Pronouns.desuMasu = { form := "-desu/-masu", register := Core.Register.Level.formal, gloss := "POL" }

def Fragments.Japanese.Pronouns.allAllocParticles : List Core.Pronouns.AllocutiveEntry

Equations

• Fragments.Japanese.Pronouns.allAllocParticles = [Fragments.Japanese.Pronouns.desuMasu]

structure Fragments.Japanese.Pronouns.VerbForm : Type

A verb form showing speech-level inflection.

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

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

Equations

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

instance Fragments.Japanese.Pronouns.instReprVerbForm : Repr VerbForm

Equations

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

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

Equations

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

instance Fragments.Japanese.Pronouns.instBEqVerbForm : BEq VerbForm

Equations

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

def Fragments.Japanese.Pronouns.iku : VerbForm

行く iku — "go" (plain).

Equations

• Fragments.Japanese.Pronouns.iku = { form := "iku", gloss := "go.PLN", register := Core.Register.Level.informal }

def Fragments.Japanese.Pronouns.ikimasu : VerbForm

行きます ikimasu — "go" (polite).

Equations

• Fragments.Japanese.Pronouns.ikimasu = { form := "ikimasu", gloss := "go.POL", register := Core.Register.Level.formal }

theorem Fragments.Japanese.Pronouns.has_all_persons : (allPronouns.any fun (x : Core.Pronouns.PronounEntry) => x.person == some UD.Person.first) = true ∧ (allPronouns.any fun (x : Core.Pronouns.PronounEntry) => x.person == some UD.Person.second) = true ∧ (allPronouns.any fun (x : Core.Pronouns.PronounEntry) => x.person == some UD.Person.third) = true

All three persons are attested.

theorem Fragments.Japanese.Pronouns.has_both_numbers : (allPronouns.any fun (x : Core.Pronouns.PronounEntry) => x.number == some Number.sg) = true ∧ (allPronouns.any fun (x : Core.Pronouns.PronounEntry) => x.number == some Number.pl) = true

Both singular and plural are attested.

theorem Fragments.Japanese.Pronouns.first_person_register : boku.register = Core.Register.Level.informal ∧ watashi.register = Core.Register.Level.formal

1st person has register-based distinction.

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

2nd person pronouns are all second person.

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

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

theorem Fragments.Japanese.Pronouns.verb_register_span : iku.register = Core.Register.Level.informal ∧ ikimasu.register = Core.Register.Level.formal

Verb forms span plain and polite levels.