def Japanese.Pronouns.watashi : PersonalPronoun

私 watashi — 1sg neutral/polite.

Equations

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

def Japanese.Pronouns.boku : PersonalPronoun

僕 boku — 1sg informal, masculine-associated via register (no inherent gender feature; cf. [Och92]).

Equations

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

def Japanese.Pronouns.ore : PersonalPronoun

俺 ore — 1sg male very informal. Strongly indexes masculine identity through assertive/coarse interactional stance ([Och92]).

Equations

• Japanese.Pronouns.ore = { form := "ore", person := some Person.first, number := some Number.singular, script := some "俺" }

def Japanese.Pronouns.watashitachi : PersonalPronoun

私たち watashitachi — 1pl.

Equations

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

def Japanese.Pronouns.kimi : PersonalPronoun

君 kimi — 2sg plain.

Equations

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

def Japanese.Pronouns.anata : PersonalPronoun

あなた anata — 2sg polite.

Equations

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

def Japanese.Pronouns.kare : PersonalPronoun

彼 kare — 3sg masculine.

Equations

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

def Japanese.Pronouns.kanojo : PersonalPronoun

彼女 kanojo — 3sg feminine.

Equations

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

def Japanese.Pronouns.karera : PersonalPronoun

彼ら karera — 3pl.

Equations

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

def Japanese.Pronouns.otagai : PersonalPronoun

互い 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

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

def Japanese.Pronouns.secondPersonPronouns : List PersonalPronoun

Equations

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

def Japanese.Pronouns.allPronouns : List PersonalPronoun

Equations

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

def Japanese.Pronouns.desuMasu : Pronoun.AllocutiveEntry

-desu polite copula / -masu polite verbal.

Equations

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

def Japanese.Pronouns.allAllocParticles : List Pronoun.AllocutiveEntry

Equations

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

structure Japanese.Pronouns.VerbForm : Type

A verb form showing speech-level inflection.

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

@[implicit_reducible]

instance Japanese.Pronouns.instReprVerbForm : Repr VerbForm

Equations

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

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

Equations

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

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

Equations

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

@[implicit_reducible]

instance Japanese.Pronouns.instBEqVerbForm : BEq VerbForm

Equations

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

def Japanese.Pronouns.iku : VerbForm

行く iku — "go" (plain).

Equations

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

def Japanese.Pronouns.ikimasu : VerbForm

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

Equations

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

theorem Japanese.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 Japanese.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 Japanese.Pronouns.first_person_register : boku.register = Features.Register.Level.informal ∧ watashi.register = Features.Register.Level.formal

1st person has register-based distinction.

theorem Japanese.Pronouns.second_person_all_2p : (secondPersonPronouns.all fun (x : PersonalPronoun) => x.person == some Person.second) = true

2nd person pronouns are all second person.

theorem Japanese.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 Japanese.Pronouns.verb_register_span : iku.register = Features.Register.Level.informal ∧ ikimasu.register = Features.Register.Level.formal

Verb forms span plain and polite levels.