Latin Adjective Degree Forms

@cite{bobaljik-2012}

Latin comparative and superlative morphology, used for cross-linguistic verification of @cite{bobaljik-2012}'s *ABA constraint and pattern inventory.

Latin exhibits all three attested degree suppletion patterns:

• AAA: regular (longus – longior – longissimus)
• ABB: suppletive CMPR+SPRL sharing a root (magnus – maior – maximus)
• ABC: three distinct roots (bonus – melior – optimus)

No Latin adjective shows an *ABA pattern.

structure Fragments.Latin.Adjectives.LatinAdjEntry : Type

A Latin adjective entry with positive, comparative, and superlative forms plus the suppletive pattern. Minimal structure — Latin data here is purely morphological (no scale type, dimension, etc.).

• pos : String
• cmpr : String
• sprl : String
• suppletion : Core.Morphology.DegreeContainment.DegreePattern

def Fragments.Latin.Adjectives.instDecidableEqLatinAdjEntry.decEq (x✝ x✝¹ : LatinAdjEntry) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Fragments.Latin.Adjectives.instDecidableEqLatinAdjEntry : DecidableEq LatinAdjEntry

Equations

• Fragments.Latin.Adjectives.instDecidableEqLatinAdjEntry = Fragments.Latin.Adjectives.instDecidableEqLatinAdjEntry.decEq

def Fragments.Latin.Adjectives.instReprLatinAdjEntry.repr : LatinAdjEntry → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Latin.Adjectives.instReprLatinAdjEntry : Repr LatinAdjEntry

Equations

• Fragments.Latin.Adjectives.instReprLatinAdjEntry = { reprPrec := Fragments.Latin.Adjectives.instReprLatinAdjEntry.repr }

@[implicit_reducible]

instance Fragments.Latin.Adjectives.instBEqLatinAdjEntry : BEq LatinAdjEntry

Equations

• Fragments.Latin.Adjectives.instBEqLatinAdjEntry = { beq := Fragments.Latin.Adjectives.instBEqLatinAdjEntry.beq }

def Fragments.Latin.Adjectives.instBEqLatinAdjEntry.beq : LatinAdjEntry → LatinAdjEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Latin.Adjectives.instBEqLatinAdjEntry.beq x✝¹ x✝ = false

def Fragments.Latin.Adjectives.longus : LatinAdjEntry

longus – longior – longissimus ('long'): regular synthetic comparative and superlative with productive suffixes -ior/-issimus.

Equations

• Fragments.Latin.Adjectives.longus = { pos := "longus", cmpr := "longior", sprl := "longissimus", suppletion := Core.Morphology.DegreeContainment.aaa }

def Fragments.Latin.Adjectives.altus : LatinAdjEntry

altus – altior – altissimus ('tall/high/deep'): regular.

Equations

• Fragments.Latin.Adjectives.altus = { pos := "altus", cmpr := "altior", sprl := "altissimus", suppletion := Core.Morphology.DegreeContainment.aaa }

def Fragments.Latin.Adjectives.fortis : LatinAdjEntry

fortis – fortior – fortissimus ('brave/strong'): regular.

Equations

• Fragments.Latin.Adjectives.fortis = { pos := "fortis", cmpr := "fortior", sprl := "fortissimus", suppletion := Core.Morphology.DegreeContainment.aaa }

def Fragments.Latin.Adjectives.bonus : LatinAdjEntry

bonus – melior – optimus ('good – better – best'): three distinct roots (ABC). The paradigmatic example of ABC suppletion (@cite{bobaljik-2012}).

Equations

• Fragments.Latin.Adjectives.bonus = { pos := "bonus", cmpr := "melior", sprl := "optimus", suppletion := Core.Morphology.DegreeContainment.abc }

def Fragments.Latin.Adjectives.malus : LatinAdjEntry

malus – peior – pessimus ('bad – worse – worst'): three distinct roots (ABC).

Equations

• Fragments.Latin.Adjectives.malus = { pos := "malus", cmpr := "peior", sprl := "pessimus", suppletion := Core.Morphology.DegreeContainment.abc }

def Fragments.Latin.Adjectives.magnus : LatinAdjEntry

magnus – maior – maximus ('great – greater – greatest'): ABB. The comparative and superlative share the suppletive root mai-/max-.

Equations

• Fragments.Latin.Adjectives.magnus = { pos := "magnus", cmpr := "maior", sprl := "maximus", suppletion := Core.Morphology.DegreeContainment.abb }

def Fragments.Latin.Adjectives.parvus : LatinAdjEntry

parvus – minor – minimus ('small – smaller – smallest'): ABB. Suppletive root min- shared across comparative and superlative.

Equations

• Fragments.Latin.Adjectives.parvus = { pos := "parvus", cmpr := "minor", sprl := "minimus", suppletion := Core.Morphology.DegreeContainment.abb }

def Fragments.Latin.Adjectives.allEntries : List LatinAdjEntry

Equations

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

theorem Fragments.Latin.Adjectives.latin_no_aba (e : LatinAdjEntry) : e ∈ allEntries → e.suppletion.IsContiguous

All Latin entries satisfy contiguity (no *ABA).

theorem Fragments.Latin.Adjectives.longus_aaa : longus.suppletion = Core.Morphology.DegreeContainment.aaa

Regular entries derive AAA patterns.

theorem Fragments.Latin.Adjectives.altus_aaa : altus.suppletion = Core.Morphology.DegreeContainment.aaa

theorem Fragments.Latin.Adjectives.fortis_aaa : fortis.suppletion = Core.Morphology.DegreeContainment.aaa

theorem Fragments.Latin.Adjectives.bonus_abc : bonus.suppletion = Core.Morphology.DegreeContainment.abc

bonus/melior/optimus is ABC.

theorem Fragments.Latin.Adjectives.malus_abc : malus.suppletion = Core.Morphology.DegreeContainment.abc

malus/peior/pessimus is ABC.

theorem Fragments.Latin.Adjectives.magnus_abb : magnus.suppletion = Core.Morphology.DegreeContainment.abb

magnus/maior/maximus is ABB.

theorem Fragments.Latin.Adjectives.parvus_abb : parvus.suppletion = Core.Morphology.DegreeContainment.abb

parvus/minor/minimus is ABB.

theorem Fragments.Latin.Adjectives.latin_has_aaa : (allEntries.any fun (e : LatinAdjEntry) => e.suppletion == Core.Morphology.DegreeContainment.aaa) = true

Latin has all three attested patterns: AAA, ABB, ABC.

theorem Fragments.Latin.Adjectives.latin_has_abb : (allEntries.any fun (e : LatinAdjEntry) => e.suppletion == Core.Morphology.DegreeContainment.abb) = true

theorem Fragments.Latin.Adjectives.latin_has_abc : (allEntries.any fun (e : LatinAdjEntry) => e.suppletion == Core.Morphology.DegreeContainment.abc) = true