Latin noun declension

Latin nouns inflect for six cases and two numbers, and the endings fuse case and number, and in the first two declensions gender as well. Five declensions are traditionally recognised, named for historical stem classes that are no longer transparent: ā-stems, o-stems, the third declension with its consonant stems and i-stems, u-stems and ē-stems. The paradigms here are the seven of Blake's table of Latin case paradigms.

No paradigm distinguishes all six cases. Two syncretisms predominate: nominative and accusative fall together in every neuter and in many plurals, and dative and ablative fall together in every plural, in the singular of the second declension and in the singular of the i-stems. The vocative differs from the nominative only in the singular of non-neuter second-declension nouns.

Main declarations

• Latin.Declension.forms: the forms of the six cases, in the order of the school paradigms.
• Latin.Declension.Noun: a noun with its declension, genders and the form of each case in each number.
• separatesPoints_paradigms, not_injective: the paradigms of the table separate the six cases, though no one of them does.
• nom_acc_syncretic_of_neuter, plural_dat_abl_syncretic, singular_dat_abl_syncretic_iff, singular_nom_voc_syncretic_iff: the syncretisms, read off the forms.

Implementation notes

Blake's table gives two forms for the ablative singular and the accusative plural of cīvis. Noun.singular and Noun.plural hold the first, the i-stem form, and civis.variant the second. The genders of the four nouns whose columns the table leaves unlabelled are the dictionary ones.

References

• [Bla94b]
• [Bla01]

inductive Latin.Declension.Class : Type

The declensions, the third split into consonant stems and i-stems.

• first : Class
• second : Class
• thirdConsonant : Class
• thirdI : Class
• fourth : Class
• fifth : Class

@[instance_reducible]

instance Latin.Declension.instDecidableEqClass : DecidableEq Class

Equations

• Latin.Declension.instDecidableEqClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Latin.Declension.instReprClass.repr : Class → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Latin.Declension.instReprClass : Repr Class

Equations

• Latin.Declension.instReprClass = { reprPrec := Latin.Declension.instReprClass.repr }

def Latin.Declension.forms (nom voc acc gen dat abl : String) : Case → String

The forms of the six cases, in the order of the school paradigms.

Equations

• Latin.Declension.forms nom voc acc gen dat abl Latin.Case.nom = nom
• Latin.Declension.forms nom voc acc gen dat abl Latin.Case.voc = voc
• Latin.Declension.forms nom voc acc gen dat abl Latin.Case.acc = acc
• Latin.Declension.forms nom voc acc gen dat abl Latin.Case.gen = gen
• Latin.Declension.forms nom voc acc gen dat abl Latin.Case.dat = dat
• Latin.Declension.forms nom voc acc gen dat abl Latin.Case.abl = abl

structure Latin.Declension.Noun : Type

A noun by the form of each case in each number.

• gloss : String

  The gloss.

• cls : Class

  The declension.

• genders : Finset Gender.Value

  The genders the noun takes, two for a noun of common gender.

• singular : Case → String

  The singular form in each case.

• plural : Case → String

  The plural form in each case.

def Latin.Declension.Noun.IsNeuter (n : Noun) : Prop

The noun is neuter.

Equations

• n.IsNeuter = (n.genders = {Latin.Gender.Value.neut})

@[instance_reducible]

instance Latin.Declension.instDecidableIsNeuter (n : Noun) : Decidable n.IsNeuter

Equations

• Latin.Declension.instDecidableIsNeuter n = { decide := decide (n.genders.val = {Latin.Gender.Value.neut}.val), reflects_decide := ⋯ }

def Latin.Declension.domina : Noun

domina 'mistress', first declension.

Equations

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

def Latin.Declension.dominus : Noun

dominus 'master', second declension.

Equations

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

def Latin.Declension.bellum : Noun

bellum 'war', second declension neuter.

Equations

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

def Latin.Declension.consul : Noun

cōnsul 'consul', third declension consonant stem.

Equations

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

def Latin.Declension.civis : Noun

cīvis 'citizen', third declension i-stem, of common gender.

Equations

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

def Latin.Declension.civis.variant : Noun

The consonant-stem forms cīvis also takes: cīve in the ablative singular and cīvēs in the accusative plural.

Equations

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

def Latin.Declension.manus : Noun

manus 'hand', fourth declension.

Equations

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

def Latin.Declension.dies : Noun

diēs 'day', fifth declension, masculine, and feminine of an appointed day.

Equations

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

def Latin.Declension.nouns : List Noun

The nouns of Blake's table.

Equations

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

The cases the paradigms distinguish

theorem Latin.Declension.separatesPoints_paradigms : {p : Case → String | ∃ n ∈ nouns, p = n.singular ∨ p = n.plural}.SeparatesPoints

The paradigms of the table, singular and plural, separate the six cases: any two cases differ in some form of some noun, which is how the traditional description establishes them ([Bla01] §2.2.1).

theorem Latin.Declension.not_injective (n : Noun) : n ∈ nouns → ¬Function.Injective n.singular ∧ ¬Function.Injective n.plural

No one paradigm of the table distinguishes all six cases.

Syncretism

theorem Latin.Declension.nom_acc_syncretic_of_neuter (n : Noun) : n ∈ nouns → n.IsNeuter → n.singular Case.nom = n.singular Case.acc ∧ n.plural Case.nom = n.plural Case.acc

A neuter does not distinguish nominative and accusative in either number.

theorem Latin.Declension.plural_dat_abl_syncretic (n : Noun) : n ∈ nouns → n.plural Case.dat = n.plural Case.abl

No plural distinguishes dative and ablative.

theorem Latin.Declension.singular_dat_abl_syncretic_iff (n : Noun) : n ∈ nouns → (n.singular Case.dat = n.singular Case.abl ↔ n.cls = Class.second ∨ n.cls = Class.thirdI)

The singular fails to distinguish dative and ablative in the second declension and the i-stems, and nowhere else.

theorem Latin.Declension.singular_nom_voc_syncretic_iff (n : Noun) : n ∈ nouns → (n.singular Case.nom = n.singular Case.voc ↔ ¬(n.cls = Class.second ∧ ¬n.IsNeuter))

The vocative singular differs from the nominative in the non-neuters of the second declension, and nowhere else.

theorem Latin.Declension.plural_nom_voc_syncretic (n : Noun) : n ∈ nouns → n.plural Case.nom = n.plural Case.voc

No plural distinguishes nominative and vocative.

theorem Latin.Declension.plural_nom_acc_syncretic : (∀ n ∈ nouns, n.cls = Class.thirdConsonant ∨ n.cls = Class.fourth ∨ n.cls = Class.fifth → n.plural Case.nom = n.plural Case.acc) ∧ civis.variant.plural Case.nom = civis.variant.plural Case.acc

The plurals of the consonant stems, the u-stems and the ē-stems do not distinguish nominative and accusative, and with its consonant-stem accusative neither does cīvis.