Modern Greek nominal declensions

The eight nominal inflection classes of Modern Greek by their case–number endings, after Ralli's description as Ackerman and Malouf simplify it (stem alternations and stress set aside), as a paradigm system whose classes are the rows 1–8 of their Table 1 and whose cells pair a number with one of the four cases.

Only the first declension, of nouns in -os such as anθropos 'man', gives each case its own ending, and only in the singular: every plural has the vocative of its nominative. The paradigms therefore separate the four cases of Greek.StandardModern.Case.

Main statements

• injective_iff: a declension gives each case of a number its own ending exactly when it is the first declension and the number is the singular (Ralli p. 205).
• nominal_vocPl, injOn_pl: every plural has the vocative of its nominative, and the first declension distinguishes the other three cases in the plural (Ralli p. 205).
• separatesPoints_paradigms: the paradigms separate the four cases.

Implementation notes

Ralli's table gives the accusative singular of the first declension as anθropo(n), with an optional -n, and the genitive singular of the fourth as polis beside the literary poleos; the endings are Ackerman and Malouf's -on and -s.

References

• [AM13a]
• [Ral00]

inductive Greek.StandardModern.Declension.Row : Type

The rows of the cells: the singular and the plural.

• sg : Row
• pl : Row

@[instance_reducible]

instance Greek.StandardModern.Declension.instDecidableEqRow : DecidableEq Row

Equations

• Greek.StandardModern.Declension.instDecidableEqRow x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Greek.StandardModern.Declension.instFintypeRow : Fintype Row

Equations

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

def Greek.StandardModern.Declension.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Greek.StandardModern.Declension.instReprRow : Repr Row

Equations

• Greek.StandardModern.Declension.instReprRow = { reprPrec := Greek.StandardModern.Declension.instReprRow.repr }

def Greek.StandardModern.Declension.Row.number : Row → Number

The number of a row.

Equations

• Greek.StandardModern.Declension.Row.sg.number = Number.singular
• Greek.StandardModern.Declension.Row.pl.number = Number.plural

@[reducible, inline]

abbrev Greek.StandardModern.Declension.nomSg : Row × Case

The nominative singular.

Equations

• Greek.StandardModern.Declension.nomSg = (Greek.StandardModern.Declension.Row.sg, Greek.StandardModern.Case.nom)

@[reducible, inline]

abbrev Greek.StandardModern.Declension.genSg : Row × Case

The genitive singular.

Equations

• Greek.StandardModern.Declension.genSg = (Greek.StandardModern.Declension.Row.sg, Greek.StandardModern.Case.gen)

@[reducible, inline]

abbrev Greek.StandardModern.Declension.accSg : Row × Case

The accusative singular.

Equations

• Greek.StandardModern.Declension.accSg = (Greek.StandardModern.Declension.Row.sg, Greek.StandardModern.Case.acc)

@[reducible, inline]

abbrev Greek.StandardModern.Declension.vocSg : Row × Case

The vocative singular.

Equations

• Greek.StandardModern.Declension.vocSg = (Greek.StandardModern.Declension.Row.sg, Greek.StandardModern.Case.voc)

@[reducible, inline]

abbrev Greek.StandardModern.Declension.nomPl : Row × Case

The nominative plural.

Equations

• Greek.StandardModern.Declension.nomPl = (Greek.StandardModern.Declension.Row.pl, Greek.StandardModern.Case.nom)

@[reducible, inline]

abbrev Greek.StandardModern.Declension.genPl : Row × Case

The genitive plural.

Equations

• Greek.StandardModern.Declension.genPl = (Greek.StandardModern.Declension.Row.pl, Greek.StandardModern.Case.gen)

@[reducible, inline]

abbrev Greek.StandardModern.Declension.accPl : Row × Case

The accusative plural.

Equations

• Greek.StandardModern.Declension.accPl = (Greek.StandardModern.Declension.Row.pl, Greek.StandardModern.Case.acc)

@[reducible, inline]

abbrev Greek.StandardModern.Declension.vocPl : Row × Case

The vocative plural.

Equations

• Greek.StandardModern.Declension.vocPl = (Greek.StandardModern.Declension.Row.pl, Greek.StandardModern.Case.voc)

def Greek.StandardModern.Declension.nominal : Morphology.ParadigmSystem (Fin 8) (Row × Case) String

The endings of the eight declensions, rows 1–8 of Table 1 of [AM13a], -∅ the zero ending.

Equations

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

The cases the paradigms distinguish

theorem Greek.StandardModern.Declension.injective_iff {d : Fin 8} {r : Row} : Function.Injective (Function.curry (nominal d) r) ↔ d = 0 ∧ r = Row.sg

theorem Greek.StandardModern.Declension.nominal_vocPl (d : Fin 8) : nominal d vocPl = nominal d nomPl

theorem Greek.StandardModern.Declension.injOn_pl : Set.InjOn (Function.curry (nominal 0) Row.pl) {Case.voc}ᶜ

theorem Greek.StandardModern.Declension.separatesPoints_paradigms : {p : Case → String | ∃ (d : Fin 8) (r : Row), p = Function.curry (nominal d) r}.SeparatesPoints

The paradigms separate the four cases.