Dutch pronouns

This file defines the strong subject pronouns of Dutch. The third person singular distinguishes three genders and the plural none; wij makes no clusivity distinction. The second person distinguishes the familiar jij and jullie from the polite u, a single form for one addressee or several that takes singular agreement.

Main definitions

• Dutch.Pronouns.pronouns: the strong subject pronouns.
• Dutch.Pronouns.addresseeSg, Dutch.Pronouns.addresseePl: the pronouns of address at each grade.

Main results

• Dutch.Pronouns.addressee_number, Dutch.Pronouns.u_referential: the polite grade does not distinguish one addressee from several, and u denotes what the two familiar forms denote together.

References

• [AN18]

inductive Dutch.Grade : Type

The honorific grades of Dutch pronouns, lowest first.

• familiar : Grade

  The familiar grade, jij and jullie.

• polite : Grade

  The polite grade, u.

@[instance_reducible]

instance Dutch.instDecidableEqGrade : DecidableEq Grade

Equations

• Dutch.instDecidableEqGrade x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Dutch.instFintypeGrade : Fintype Grade

Equations

• Dutch.instFintypeGrade = { elems := { val := ↑Dutch.Grade.enumList, nodup := Dutch.Grade.enumList_nodup }, complete := Dutch.instFintypeGrade._proof_1 }

@[instance_reducible]

instance Dutch.instReprGrade : Repr Grade

Equations

• Dutch.instReprGrade = { reprPrec := Dutch.instReprGrade.repr }

def Dutch.instReprGrade.repr : Grade → ℕ → Std.Format

Equations

• Dutch.instReprGrade.repr Dutch.Grade.familiar prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dutch.Grade.familiar")).group prec✝
• Dutch.instReprGrade.repr Dutch.Grade.polite prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Dutch.Grade.polite")).group prec✝

@[instance_reducible]

instance Dutch.instLinearOrderGrade : LinearOrder Grade

Equations

• Dutch.instLinearOrderGrade = LinearOrder.lift' Dutch.Grade.ctorIdx Dutch.instLinearOrderGrade._proof_1

def Dutch.Pronouns.ik : PersonalPronoun

The first person singular ik.

Equations

• Dutch.Pronouns.ik = { form := "ik", person := some Person.first, number := some Number.singular, case_ := some Case.nom, strength := some Pronoun.Strength.strong }

def Dutch.Pronouns.jij : PersonalPronoun

The familiar second person singular jij.

Equations

• Dutch.Pronouns.jij = { form := "jij", person := some Person.second, number := some Number.singular, case_ := some Case.nom, strength := some Pronoun.Strength.strong }

def Dutch.Pronouns.u : PersonalPronoun

The polite second person u, for one or several addressees, with singular agreement.

Equations

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

def Dutch.Pronouns.hij : PersonalPronoun

The third person singular masculine hij.

Equations

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

def Dutch.Pronouns.zij_sg : PersonalPronoun

The third person singular feminine zij.

Equations

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

def Dutch.Pronouns.het : PersonalPronoun

The third person singular neuter het.

Equations

• Dutch.Pronouns.het = { form := "het", person := some Person.third, number := some Number.singular, gender := some Gender.neuter, strength := some Pronoun.Strength.strong }

def Dutch.Pronouns.wij : PersonalPronoun

The first person plural wij.

Equations

• Dutch.Pronouns.wij = { form := "wij", person := some Person.first, number := some Number.plural, case_ := some Case.nom, strength := some Pronoun.Strength.strong }

def Dutch.Pronouns.jullie : PersonalPronoun

The familiar second person plural jullie.

Equations

• Dutch.Pronouns.jullie = { form := "jullie", person := some Person.second, number := some Number.plural, strength := some Pronoun.Strength.strong }

def Dutch.Pronouns.zij_pl : PersonalPronoun

The third person plural zij.

Equations

• Dutch.Pronouns.zij_pl = { form := "zij", person := some Person.third, number := some Number.plural, case_ := some Case.nom, strength := some Pronoun.Strength.strong }

def Dutch.Pronouns.addresseeSg : Grade → PersonalPronoun

The pronoun for a single addressee at each grade.

Equations

• Dutch.Pronouns.addresseeSg Dutch.Grade.familiar = Dutch.Pronouns.jij
• Dutch.Pronouns.addresseeSg Dutch.Grade.polite = Dutch.Pronouns.u

def Dutch.Pronouns.addresseePl : Grade → PersonalPronoun

The pronoun for several addressees at each grade.

Equations

• Dutch.Pronouns.addresseePl Dutch.Grade.familiar = Dutch.Pronouns.jullie
• Dutch.Pronouns.addresseePl Dutch.Grade.polite = Dutch.Pronouns.u

def Dutch.Pronouns.pronouns : Finset PersonalPronoun

The strong subject pronouns.

Equations

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

theorem Dutch.Pronouns.addressee_number : addresseeSg Grade.familiar ≠ addresseePl Grade.familiar ∧ addresseeSg Grade.polite = addresseePl Grade.polite

The familiar grade distinguishes one addressee from several, and the polite grade does not.

theorem Dutch.Pronouns.u_referential : u.referential = jij.referential ∪ jullie.referential

The polite form denotes exactly what the two familiar forms denote between them.