Bobaljik (2012): Universals in Comparative Morphology

@cite{bobaljik-2012}

Overview

@cite{bobaljik-2012} surveys comparative and superlative morphology across languages and derives several cross-linguistic generalizations from the containment hypothesis: the superlative structurally contains the comparative ([[[ADJ] CMPR] SPRL]).

Key Generalizations

1. CSG (Comparative-Superlative Generalization): *ABA is unattested — if the comparative is suppletive, the superlative is too (and vice versa). Attested: AAA, ABB, ABC. Unattested: *ABA. Scope: applies to relative superlatives, not absolute superlatives / elatives (p. 2, p. 28).

2. SSG (Synthetic Superlative Generalization): No language has a morphological (synthetic) superlative without also having a morphological comparative.

3. RSG (Root Suppletion Generalization): Root suppletion is limited to synthetic (morphological) comparatives. No language has a periphrastic comparative with a suppletive root (*good → more bett).

4. Lesslessness: No language has a synthetic comparative of inferiority. "Less tall" is always periphrastic.

English and Latin Fragment Verification

This module verifies the CSG, SSG, RSG, and lesslessness against both the English adjective fragment (Fragments/English/Modifiers/ Adjectives.lean) and the Latin adjective fragment (Fragments/Latin/ Adjectives.lean), using the suppletion field on each entry to encode empirically observed root-class patterns.

Connects morphological infrastructure (Core.Morphology) to scalar- alternative infrastructure (Theories/Semantics/Alternatives/HornScale.lean), enabling automatic generation of the alternatives needed for scalar implicature computation. Was previously in Theories/Morphology/Core/ ScaleFromParadigm.lean; relocated 0.230.455 (sole consumer is this study file). @cite{horn-1972} @cite{kennedy-2007}

structure Core.Morphology.ScaleFromParadigm.MorphScale : Type

A morphologically-derived Horn scale.

• positive : String
• comparative : String
• superlative : String

def Core.Morphology.ScaleFromParadigm.instReprMorphScale.repr : MorphScale → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Morphology.ScaleFromParadigm.instReprMorphScale : Repr MorphScale

Equations

• Core.Morphology.ScaleFromParadigm.instReprMorphScale = { reprPrec := Core.Morphology.ScaleFromParadigm.instReprMorphScale.repr }

def Core.Morphology.ScaleFromParadigm.instBEqMorphScale.beq : MorphScale → MorphScale → Bool

Equations

• One or more equations did not get rendered due to their size.
• Core.Morphology.ScaleFromParadigm.instBEqMorphScale.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Core.Morphology.ScaleFromParadigm.instBEqMorphScale : BEq MorphScale

Equations

• Core.Morphology.ScaleFromParadigm.instBEqMorphScale = { beq := Core.Morphology.ScaleFromParadigm.instBEqMorphScale.beq }

def Core.Morphology.ScaleFromParadigm.MorphScale.toHornScale (ms : MorphScale) : Alternatives.HornScale String

Convert a MorphScale to a HornScale String, weakest-to-strongest.

Equations

• ms.toHornScale = { members := [ms.positive, ms.comparative, ms.superlative] }

def Core.Morphology.ScaleFromParadigm.adjectiveScale {σ : Type} (stem : Stem σ) : Option MorphScale

Extract a degree scale from a stem's paradigm.

Equations

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

def Core.Morphology.ScaleFromParadigm.morphologicalAlternatives {σ : Type} (stem : Stem σ) (form : String) : List String

Paradigm-mates as scalar alternatives, scale order preserved.

Equations

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

theorem Bobaljik2012.tall_aaa : Fragments.English.Modifiers.Adjectives.tall.suppletion = Core.Morphology.DegreeContainment.aaa

Regular adjectives have AAA suppletion patterns.

theorem Bobaljik2012.short_aaa : Fragments.English.Modifiers.Adjectives.short.suppletion = Core.Morphology.DegreeContainment.aaa

theorem Bobaljik2012.happy_aaa : Fragments.English.Modifiers.Adjectives.happy.suppletion = Core.Morphology.DegreeContainment.aaa

theorem Bobaljik2012.hot_aaa : Fragments.English.Modifiers.Adjectives.hot.suppletion = Core.Morphology.DegreeContainment.aaa

theorem Bobaljik2012.expensive_aaa : Fragments.English.Modifiers.Adjectives.expensive.suppletion = Core.Morphology.DegreeContainment.aaa

theorem Bobaljik2012.dry_aaa : Fragments.English.Modifiers.Adjectives.dry.suppletion = Core.Morphology.DegreeContainment.aaa

theorem Bobaljik2012.good_abb : Fragments.English.Modifiers.Adjectives.good.suppletion = Core.Morphology.DegreeContainment.abb

Suppletive adjectives have ABB suppletion patterns.

theorem Bobaljik2012.bad_abb : Fragments.English.Modifiers.Adjectives.bad.suppletion = Core.Morphology.DegreeContainment.abb

theorem Bobaljik2012.english_no_aba (e : Fragments.English.Modifiers.Adjectives.AdjModifierEntry) : e ∈ Fragments.English.Modifiers.Adjectives.allEntries → e.suppletion.IsContiguous

CSG: All English adjective entries satisfy contiguity (no *ABA violations).

theorem Bobaljik2012.good_csg : Fragments.English.Modifiers.Adjectives.good.suppletion.SprlSuppletive

CSG Part I applied to English data: "good" and "bad" have suppletive comparatives, so by csg_part1 their superlatives must be suppletive too — and they are.

theorem Bobaljik2012.bad_csg : Fragments.English.Modifiers.Adjectives.bad.suppletion.SprlSuppletive

theorem Bobaljik2012.good_csg_part2 : Fragments.English.Modifiers.Adjectives.good.suppletion.CmprSuppletive

CSG Part II via VI locality: if the superlative is suppletive, the comparative is too.

theorem Bobaljik2012.bad_csg_part2 : Fragments.English.Modifiers.Adjectives.bad.suppletion.CmprSuppletive

theorem Bobaljik2012.english_all_attested (e : Fragments.English.Modifiers.Adjectives.AdjModifierEntry) : e ∈ Fragments.English.Modifiers.Adjectives.allEntries → e.suppletion.IsContiguous ∧ e.suppletion.cmpr = e.suppletion.sprl

All English root suppletion patterns satisfy both contiguity (no *ABA — csg_part1) and VI locality (CMPR cell = SPRL cell — the DM-locality conjunction Degree.vi_cmpr_eq_sprl of Theories/Morphology/DM/ContainmentVI.lean). The conjunction restricts root patterns to AAA / ABB. Stated as the explicit conjunction so the underlying derivation is visible at use site, rather than packaged as a stipulated isAttested field.

theorem Bobaljik2012.english_ssg (e : Fragments.English.Modifiers.Adjectives.AdjModifierEntry) : e ∈ Fragments.English.Modifiers.Adjectives.allEntries → e.formSuper.isSome = true → e.formComp.isSome = true

SSG (@cite{bobaljik-2012}): If an entry has a synthetic superlative form, it also has a synthetic comparative form. No English adjective has -est without -er.

def Bobaljik2012.isSyntheticComp (e : Fragments.English.Modifiers.Adjectives.AdjModifierEntry) : Bool

Is the comparative form synthetic (a single morphological word, not periphrastic "more X")? Detected by the absence of a space in the comparative form string.

Equations

• Bobaljik2012.isSyntheticComp e = match e.formComp with | some f => !f.toList.any fun (x : Char) => x == ' ' | none => false

theorem Bobaljik2012.english_rsg (e : Fragments.English.Modifiers.Adjectives.AdjModifierEntry) : e ∈ Fragments.English.Modifiers.Adjectives.allEntries → e.suppletion.CmprSuppletive → isSyntheticComp e = true

RSG (@cite{bobaljik-2012}): Root suppletion is limited to synthetic comparatives. If an entry has a suppletive root (CMPR differs from POS), then its comparative form is synthetic (not periphrastic).

This rules out patterns like *good → more bett: a language cannot have a periphrastic comparative with a suppletive root.

Verified: "good" → "better" (synthetic), "bad" → "worse" (synthetic). Contrast: "expensive" → "more expensive" (periphrastic, but non-suppletive root — AAA, not ABB).

Lesslessness (@cite{bobaljik-2012}): No synthetic comparative of inferiority exists in any language. English expresses inferiority periphrastically ("less tall"), never synthetically.

The fragment-level verification (english_no_synthetic_inferior) was dropped during the Bool→Prop migration: kernel decide doesn't reduce String.startsWith over a fragment-list, and the structural proof (enumerate allEntries, dispatch each by rfl on the Bool value) requires fin_cases from mathlib which isn't pulled in here. The empirical claim is documented above; the cross-linguistic generalization sits in bobaljik-2012 directly. Re-encode if a future study file motivates a structural witness.

theorem Bobaljik2012.good_forms : Fragments.English.Modifiers.Adjectives.good.formComp = some "better" ∧ Fragments.English.Modifiers.Adjectives.good.formSuper = some "best"

The fragment records suppletive forms for "good" and "bad".

theorem Bobaljik2012.bad_forms : Fragments.English.Modifiers.Adjectives.bad.formComp = some "worse" ∧ Fragments.English.Modifiers.Adjectives.bad.formSuper = some "worst"

theorem Bobaljik2012.good_abb_from_forms : Fragments.English.Modifiers.Adjectives.good.suppletion = Core.Morphology.DegreeContainment.abb ∧ Fragments.English.Modifiers.Adjectives.good.formComp = some "better" ∧ Fragments.English.Modifiers.Adjectives.good.formSuper = some "best"

The suppletion field agrees with the surface forms: "good" → "better" → "best" is ABB (suppletive root shared across CMPR and SPRL).

def Bobaljik2012.attestedPatterns : List (String × Core.Morphology.DegreeContainment.DegreePattern)

The three attested degree-suppletive patterns.

Equations

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

theorem Bobaljik2012.attested_all_contiguous (pair : String × Core.Morphology.DegreeContainment.DegreePattern) : pair ∈ attestedPatterns → pair.2.IsContiguous

All attested patterns are contiguous.

theorem Bobaljik2012.aba_unattested : ¬Core.Morphology.DegreeContainment.aba.IsContiguous

The unattested *ABA pattern is not contiguous.

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

Latin CSG: All Latin adjective entries satisfy contiguity.

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

Latin bonus – melior – optimus derives ABC.

theorem Bobaljik2012.latin_all_three_patterns : (Fragments.Latin.Adjectives.allEntries.any fun (e : Fragments.Latin.Adjectives.LatinAdjEntry) => e.suppletion == Core.Morphology.DegreeContainment.aaa) = true ∧ (Fragments.Latin.Adjectives.allEntries.any fun (e : Fragments.Latin.Adjectives.LatinAdjEntry) => e.suppletion == Core.Morphology.DegreeContainment.abb) = true ∧ (Fragments.Latin.Adjectives.allEntries.any fun (e : Fragments.Latin.Adjectives.LatinAdjEntry) => e.suppletion == Core.Morphology.DegreeContainment.abc) = true

Latin exhibits all three attested patterns (AAA, ABB, ABC), confirming the cross-linguistic pattern inventory against a language with richer suppletion than English.

theorem Bobaljik2012.english_generic_contiguity (e : Fragments.English.Modifiers.Adjectives.AdjModifierEntry) : e ∈ Fragments.English.Modifiers.Adjectives.allEntries → Morphology.Containment.IsContiguous [e.suppletion.pos, e.suppletion.cmpr, e.suppletion.sprl]

The English CSG verification is an instance of the generic contiguity predicate from Containment.lean: each entry's suppletion pattern, when converted to a list, satisfies the domain-independent isContiguous.

Theories/Morphology/Core/ScaleFromParadigm.lean derives Horn scales from degree paradigms: a stem with comparative + superlative rules yields a 3-point scale [positive, comparative, superlative]. The tests below verify the extractor on the English adjective fragment.

theorem Bobaljik2012.tall_scale_exists : (Core.Morphology.ScaleFromParadigm.adjectiveScale Bobaljik2012.tallStem✝).isSome = true

Gradable adjectives produce a scale; non-gradables do not.

theorem Bobaljik2012.dead_no_scale : (Core.Morphology.ScaleFromParadigm.adjectiveScale Bobaljik2012.deadStem✝).isNone = true

theorem Bobaljik2012.pregnant_no_scale : (Core.Morphology.ScaleFromParadigm.adjectiveScale Bobaljik2012.pregnantStem✝).isNone = true

theorem Bobaljik2012.tall_scale_members : Option.map (fun (x : Core.Morphology.ScaleFromParadigm.MorphScale) => x.toHornScale.members) (Core.Morphology.ScaleFromParadigm.adjectiveScale Bobaljik2012.tallStem✝) = some ["tall", "taller", "tallest"]

Regular paradigm yields the expected 3-point scale.

theorem Bobaljik2012.good_scale_members : Option.map (fun (x : Core.Morphology.ScaleFromParadigm.MorphScale) => x.toHornScale.members) (Core.Morphology.ScaleFromParadigm.adjectiveScale Bobaljik2012.goodStem✝) = some ["good", "better", "best"]

Suppletive paradigm yields the irregular forms in scale position.

theorem Bobaljik2012.expensive_scale_members : Option.map (fun (x : Core.Morphology.ScaleFromParadigm.MorphScale) => x.toHornScale.members) (Core.Morphology.ScaleFromParadigm.adjectiveScale Bobaljik2012.expensiveStem✝) = some ["expensive", "more expensive", "most expensive"]

Periphrastic paradigm yields multi-word scale members.

morphologicalAlternatives stem form returns paradigm-mates of form preserving scale order — the input shape scalar-implicature reasoning expects. Tests confirm filter-by-equality semantics across the three scale positions, plus the empty-list result for non-gradable stems.

theorem Bobaljik2012.tall_alternatives : Core.Morphology.ScaleFromParadigm.morphologicalAlternatives Bobaljik2012.tallStem✝ "tall" = ["taller", "tallest"]

theorem Bobaljik2012.taller_alternatives : Core.Morphology.ScaleFromParadigm.morphologicalAlternatives Bobaljik2012.tallStem✝ "taller" = ["tall", "tallest"]

theorem Bobaljik2012.tallest_alternatives : Core.Morphology.ScaleFromParadigm.morphologicalAlternatives Bobaljik2012.tallStem✝ "tallest" = ["tall", "taller"]

theorem Bobaljik2012.dead_no_alternatives : Core.Morphology.ScaleFromParadigm.morphologicalAlternatives Bobaljik2012.deadStem✝ "dead" = []