Russian noun gender

This file defines the three controller genders of Russian, masculine, feminine and neuter, and nouns with their gender, the gender of their referents where they have one, and their declension class. Gender is partly fixed by the referent and partly by the declension ([Cor91]): djadja 'uncle' declines like most feminines and is masculine by its referents, and the soft-sign nouns are feminine as a rule ([Wad20] §63) but for put' 'way', of which "Despite feminine endings in the genitive, dative and prepositional singular, путь is qualified by masculine adjectives" (§66). The declension classes are Corbett's as [Kra20] reports them: zakon, škola, kost' and vino are her examples of the correlation of class and gender (18), the neuter znamja 'banner' (Wade §64) and the masculine put' of its exceptions (19), and the kinship and animal nouns stand for the semantic core (17). Vrač 'doctor' is masculine but takes feminine agreement on a predicate when the referent is female, Врач обязана помочь больному 'The doctor is obliged to help the patient' ([Wad20] §313); the file records its declensional gender, and the hybrid agreement is in Studies/Kramer2020.lean.

The past-tense concord of the verb and the nominative endings of the adjective are the agreement evidence that the three genders are distinct ([Cor91]).

References

• [Wad20]
• [Cor91]
• [Cor98]
• [Kra20]

Genders and declension classes

inductive Russian.Gender.Value : Type

The three controller genders.

• masc : Value
• fem : Value
• neut : Value

@[instance_reducible]

instance Russian.Gender.instDecidableEqValue : DecidableEq Value

Equations

• Russian.Gender.instDecidableEqValue x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Russian.Gender.instReprValue.repr : Value → ℕ → Std.Format

Equations

• Russian.Gender.instReprValue.repr Russian.Gender.Value.masc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Russian.Gender.Value.masc")).group prec✝
• Russian.Gender.instReprValue.repr Russian.Gender.Value.fem prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Russian.Gender.Value.fem")).group prec✝
• Russian.Gender.instReprValue.repr Russian.Gender.Value.neut prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Russian.Gender.Value.neut")).group prec✝

@[instance_reducible]

instance Russian.Gender.instReprValue : Repr Value

Equations

• Russian.Gender.instReprValue = { reprPrec := Russian.Gender.instReprValue.repr }

@[instance_reducible]

instance Russian.Gender.instFintypeValue : Fintype Value

Equations

• Russian.Gender.instFintypeValue = { elems := { val := ↑Russian.Gender.Value.enumList, nodup := Russian.Gender.Value.enumList_nodup }, complete := Russian.Gender.instFintypeValue._proof_1 }

def Russian.Gender.Value.toLabel : Value → Gender

The comparative label of each gender.

Equations

• Russian.Gender.Value.masc.toLabel = Gender.masculine
• Russian.Gender.Value.fem.toLabel = Gender.feminine
• Russian.Gender.Value.neut.toLabel = Gender.neuter

inductive Russian.Gender.DeclClass : Type

The declension classes, with which gender correlates without either fixing the other.

• I : DeclClass

  The class of zakon 'law', typically masculine.

• II : DeclClass

  The class of škola 'school', typically feminine.

• III : DeclClass

  The class of kost' 'bone', typically feminine, with put' and znamja the exceptions.

• IV : DeclClass

  The remaining patterns, typically neuter.

@[instance_reducible]

instance Russian.Gender.instDecidableEqDeclClass : DecidableEq DeclClass

Equations

• Russian.Gender.instDecidableEqDeclClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Russian.Gender.instReprDeclClass.repr : DeclClass → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Russian.Gender.instReprDeclClass : Repr DeclClass

Equations

• Russian.Gender.instReprDeclClass = { reprPrec := Russian.Gender.instReprDeclClass.repr }

structure Russian.Gender.Nounextends GenderedNoun Russian.Gender.Value : Type

A Russian noun with its controller gender, the gender of its referents where they have one, and its declension class.

• form : String
• gloss : String
• gender : Russian.Gender.Value
• naturalGender : Option Gender
• declClass : Option DeclClass

  The declension class, left out for a noun whose gender its referents fix.

@[instance_reducible]

instance Russian.Gender.instDecidableEqNoun : DecidableEq Noun

Equations

• Russian.Gender.instDecidableEqNoun = Russian.Gender.instDecidableEqNoun.decEq

def Russian.Gender.instDecidableEqNoun.decEq (x✝ x✝¹ : Noun) : Decidable (x✝ = x✝¹)

Equations

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

def Russian.Gender.instReprNoun.repr : Noun → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Russian.Gender.instReprNoun : Repr Noun

Equations

• Russian.Gender.instReprNoun = { reprPrec := Russian.Gender.instReprNoun.repr }

Nouns whose referents fix their gender

def Russian.Gender.otec : Noun

otec 'father'.

Equations

• Russian.Gender.otec = { form := "otec", gloss := "father", gender := Russian.Gender.Value.masc, naturalGender := some Gender.masculine }

def Russian.Gender.mat' : Noun

mat' 'mother'.

Equations

• Russian.Gender.mat' = { form := "mat'", gloss := "mother", gender := Russian.Gender.Value.fem, naturalGender := some Gender.feminine }

def Russian.Gender.brat : Noun

brat 'brother'.

Equations

• Russian.Gender.brat = { form := "brat", gloss := "brother", gender := Russian.Gender.Value.masc, naturalGender := some Gender.masculine }

def Russian.Gender.sestra : Noun

sestra 'sister'.

Equations

• Russian.Gender.sestra = { form := "sestra", gloss := "sister", gender := Russian.Gender.Value.fem, naturalGender := some Gender.feminine }

def Russian.Gender.byk : Noun

byk 'bull'.

Equations

• Russian.Gender.byk = { form := "byk", gloss := "bull", gender := Russian.Gender.Value.masc, naturalGender := some Gender.masculine }

def Russian.Gender.korova : Noun

korova 'cow'.

Equations

• Russian.Gender.korova = { form := "korova", gloss := "cow", gender := Russian.Gender.Value.fem, naturalGender := some Gender.feminine }

def Russian.Gender.djadja : Noun

djadja 'uncle', of the declension of most feminines and masculine by its referents.

Equations

• Russian.Gender.djadja = { form := "djadja", gloss := "uncle", gender := Russian.Gender.Value.masc, naturalGender := some Gender.masculine, declClass := some Russian.Gender.DeclClass.II }

Nouns whose declension goes with their gender

def Russian.Gender.zakon : Noun

zakon 'law'.

Equations

• Russian.Gender.zakon = { form := "zakon", gloss := "law", gender := Russian.Gender.Value.masc, declClass := some Russian.Gender.DeclClass.I }

def Russian.Gender.škola : Noun

škola 'school'.

Equations

• Russian.Gender.škola = { form := "škola", gloss := "school", gender := Russian.Gender.Value.fem, declClass := some Russian.Gender.DeclClass.II }

def Russian.Gender.kost' : Noun

kost' 'bone', a soft-sign feminine ([Wad20] §63).

Equations

• Russian.Gender.kost' = { form := "kost'", gloss := "bone", gender := Russian.Gender.Value.fem, declClass := some Russian.Gender.DeclClass.III }

def Russian.Gender.vino : Noun

vino 'wine'.

Equations

• Russian.Gender.vino = { form := "vino", gloss := "wine", gender := Russian.Gender.Value.neut, declClass := some Russian.Gender.DeclClass.IV }

def Russian.Gender.znamja : Noun

znamja 'banner', of the class of kost' but neuter, one of the neuters in -mja ([Wad20] §64).

Equations

• Russian.Gender.znamja = { form := "znamja", gloss := "banner", gender := Russian.Gender.Value.neut, declClass := some Russian.Gender.DeclClass.III }

def Russian.Gender.put' : Noun

put' 'way', of the class of kost' but masculine ([Wad20] §66).

Equations

• Russian.Gender.put' = { form := "put'", gloss := "way", gender := Russian.Gender.Value.masc, declClass := some Russian.Gender.DeclClass.III }

def Russian.Gender.vrač : Noun

vrač 'doctor', masculine and of the class of zakon, which takes feminine agreement on a predicate when the referent is female ([Wad20] §313).

Equations

• Russian.Gender.vrač = { form := "vrač", gloss := "doctor", gender := Russian.Gender.Value.masc, declClass := some Russian.Gender.DeclClass.I }

The entries

def Russian.Gender.semanticCoreNouns : List Noun

The nouns whose referents fix their gender.

Equations

• Russian.Gender.semanticCoreNouns = [Russian.Gender.otec, Russian.Gender.mat', Russian.Gender.brat, Russian.Gender.sestra, Russian.Gender.byk, Russian.Gender.korova, Russian.Gender.djadja]

def Russian.Gender.remainderNouns : List Noun

The nouns whose gender goes with their declension, znamja and put' the exceptions.

Equations

• Russian.Gender.remainderNouns = [Russian.Gender.zakon, Russian.Gender.škola, Russian.Gender.kost', Russian.Gender.vino, Russian.Gender.znamja, Russian.Gender.put']

def Russian.Gender.allNouns : List Noun

The entries.

Equations

• Russian.Gender.allNouns = Russian.Gender.semanticCoreNouns ++ Russian.Gender.remainderNouns ++ [Russian.Gender.vrač]

theorem Russian.Gender.declClass_ne_gender : znamja.declClass = kost'.declClass ∧ znamja.gender ≠ kost'.gender

The declension class does not fix the gender: znamja and kost' share a class and differ in gender.

Agreement evidence

inductive Russian.Gender.PastConcord : Type

The past-tense concord endings of the verb, -∅, -a and -o.

• zero : PastConcord
• a : PastConcord
• o : PastConcord

@[instance_reducible]

instance Russian.Gender.instDecidableEqPastConcord : DecidableEq PastConcord

Equations

• Russian.Gender.instDecidableEqPastConcord x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Russian.Gender.instReprPastConcord : Repr PastConcord

Equations

• Russian.Gender.instReprPastConcord = { reprPrec := Russian.Gender.instReprPastConcord.repr }

def Russian.Gender.instReprPastConcord.repr : PastConcord → ℕ → Std.Format

Equations

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

def Russian.Gender.Value.pastConcord : Value → PastConcord

The past-tense concord ending of each gender.

Equations

• Russian.Gender.Value.masc.pastConcord = Russian.Gender.PastConcord.zero
• Russian.Gender.Value.fem.pastConcord = Russian.Gender.PastConcord.a
• Russian.Gender.Value.neut.pastConcord = Russian.Gender.PastConcord.o

inductive Russian.Gender.AdjEnding : Type

The nominative endings of a hard-stem adjective such as novyj 'new': -yj, -aja, -oe by gender in the singular, -ye for all three in the plural ([Wad20]; [Cor98]).

• yj : AdjEnding
• aja : AdjEnding
• oe : AdjEnding
• ye : AdjEnding

@[instance_reducible]

instance Russian.Gender.instDecidableEqAdjEnding : DecidableEq AdjEnding

Equations

• Russian.Gender.instDecidableEqAdjEnding x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Russian.Gender.instReprAdjEnding.repr : AdjEnding → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Russian.Gender.instReprAdjEnding : Repr AdjEnding

Equations

• Russian.Gender.instReprAdjEnding = { reprPrec := Russian.Gender.instReprAdjEnding.repr }

@[instance_reducible]

instance Russian.Gender.instFintypeAdjEnding : Fintype AdjEnding

Equations

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

def Russian.Gender.Value.adjEnding : Value → Bool → AdjEnding

The nominative ending by gender and number.

Equations

• Russian.Gender.Value.masc.adjEnding false = Russian.Gender.AdjEnding.yj
• Russian.Gender.Value.fem.adjEnding false = Russian.Gender.AdjEnding.aja
• Russian.Gender.Value.neut.adjEnding false = Russian.Gender.AdjEnding.oe
• x✝.adjEnding true = Russian.Gender.AdjEnding.ye

theorem Russian.Gender.faithful_adjEnding : Function.Injective fun (x : Value) => x.adjEnding false

The singular ending alone distinguishes the three genders.

theorem Russian.Gender.faithful_pastConcord : Function.Injective Value.pastConcord

The past-tense concord distinguishes the three genders on a single target.