Bobaljik (2012): Universals in Comparative Morphology

[Bob12]

Overview

[Bob12] 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 Generalizations): two directions. CSG1: a suppletive comparative forces a suppletive superlative (*ABA excluded); CSG2: a suppletive superlative forces a suppletive comparative (*AAB excluded). Attested: AAA, ABB, ABC. Unattested: *ABA, *AAB. The derivations are asymmetric — CSG1 needs containment

   • Elsewhere + Antihomophony, CSG2 additionally portmanteau exponence, adjacency, and the markedness condition (202) — in the formalization adjacency's AAB-blocking role is absorbed into Grounded; see Morphology/Containment/Vocabulary.lean. Both are instantiated on the book's worked vocabularies below. Scope: relative superlatives only, not absolute superlatives / elatives (p. 2, p. 28). The CSG ranges over synthetic grades; among periphrastic superlatives it holds exactly of those embedding the comparative form (p. 30, p. 78).

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.

Scale-Generation Substrate

Connects morphological infrastructure (Morphology) to scalar- alternative infrastructure (Semantics/Alternatives/HornScale.lean), enabling automatic generation of the alternatives needed for scalar implicature computation. Lives in this study file because it is the sole consumer. [Hor72] [Ken07]

structure Bobaljik2012.ScaleFromParadigm.MorphScale : Type

A morphologically-derived Horn scale.

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

def Bobaljik2012.ScaleFromParadigm.instReprMorphScale.repr : MorphScale → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Bobaljik2012.ScaleFromParadigm.instReprMorphScale : Repr MorphScale

Equations

• Bobaljik2012.ScaleFromParadigm.instReprMorphScale = { reprPrec := Bobaljik2012.ScaleFromParadigm.instReprMorphScale.repr }

def Bobaljik2012.ScaleFromParadigm.instBEqMorphScale.beq : MorphScale → MorphScale → Bool

Equations

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

@[implicit_reducible]

instance Bobaljik2012.ScaleFromParadigm.instBEqMorphScale : BEq MorphScale

Equations

• Bobaljik2012.ScaleFromParadigm.instBEqMorphScale = { beq := Bobaljik2012.ScaleFromParadigm.instBEqMorphScale.beq }

def Bobaljik2012.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 Bobaljik2012.ScaleFromParadigm.adjectiveScale {σ : Type} (stem : Morphology.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 Bobaljik2012.ScaleFromParadigm.morphologicalAlternatives {σ : Type} (stem : Morphology.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.

Pattern Verification (English)

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

Regular adjectives have AAA suppletion patterns.

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

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

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

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

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

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

Suppletive adjectives have ABB suppletion patterns.

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

CSG Verification (English)

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

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

theorem Bobaljik2012.good_csg : 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 : English.Modifiers.Adjectives.bad.suppletion.SprlSuppletive

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

CSG Part II on the English data: if the superlative is suppletive, the comparative is too. Data-level check; the engine derivation (Morphology.Containment.csg2) is instantiated at welshAAB_blocked below.

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

Attestedness Verification (English)

theorem Bobaljik2012.english_all_attested (e : English.Modifiers.Adjectives.AdjModifierEntry) : e ∈ 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 the terminal-adjacent plateau (CMPR cell = SPRL cell — Morphology.Containment.realize_const_of_terminal_adjacent). 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.

SSG (Synthetic Superlative Generalization)

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

SSG ([Bob12]): If an entry has a synthetic superlative form, it also has a synthetic comparative form. No English adjective has -est without -er.

RSG (Root Suppletion Generalization)

def Bobaljik2012.IsSyntheticComp (e : English.Modifiers.Adjectives.AdjModifierEntry) : Prop

The comparative form is synthetic (a single morphological word, not periphrastic "more X"), detected as the absence of a space in the form string. Structural counterpart: Morphology.Containment.Synthesis (see the worked vocabularies below).

Equations

• Bobaljik2012.IsSyntheticComp e = ∃ f ∈ e.formComp, ' ' ∉ f.toList

@[implicit_reducible]

instance Bobaljik2012.instDecidableIsSyntheticComp (e : English.Modifiers.Adjectives.AdjModifierEntry) : Decidable (IsSyntheticComp e)

Equations

• Bobaljik2012.instDecidableIsSyntheticComp e = id inferInstance

theorem Bobaljik2012.english_rsg (e : English.Modifiers.Adjectives.AdjModifierEntry) : e ∈ English.Modifiers.Adjectives.allEntries → e.suppletion.CmprSuppletive → IsSyntheticComp e

RSG ([Bob12]): 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

Lesslessness ([Bob12] (5), ch. 7): no language has a synthetic comparative of inferiority — "less tall" is always periphrastic. The book's empirically strongest generalization but its least derived: the proposed account (CMPR plus a polarity-reversal head, with synthetic spellout blocked by the polar antonym's comparative) is a sketch the book itself flags as incomplete, so it is recorded as data-level prose, not as a theorem of the ch. 2–5 axioms.

Fragment Cross-Check

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

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

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

theorem Bobaljik2012.good_abb_from_forms : English.Modifiers.Adjectives.good.suppletion = Morphology.DegreeContainment.abb ∧ English.Modifiers.Adjectives.good.formComp = some "better" ∧ 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).

Cross-Linguistic Pattern Inventory

def Bobaljik2012.attestedPatterns : List (String × 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 × Morphology.DegreeContainment.DegreePattern) : pair ∈ attestedPatterns → pair.2.IsContiguous

All attested patterns are contiguous.

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

The unattested *ABA pattern is not contiguous.

Cross-Linguistic Verification (Latin)

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

Latin CSG: All Latin adjective entries satisfy contiguity.

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

Latin bonus – melior – optimus derives ABC.

theorem Bobaljik2012.latin_all_three_patterns : (∃ e ∈ Latin.Adjectives.allEntries, e.suppletion = Morphology.DegreeContainment.aaa) ∧ (∃ e ∈ Latin.Adjectives.allEntries, e.suppletion = Morphology.DegreeContainment.abb) ∧ ∃ e ∈ Latin.Adjectives.allEntries, e.suppletion = Morphology.DegreeContainment.abc

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

The Realizational Derivation: the Book's Worked Vocabularies

The engine of Morphology/Containment/Vocabulary.lean run on the vocabularies [Bob12] actually writes down. ExponenceRules record exponent, exponed span, and conditioning context; realize runs Elsewhere insertion; degreeShape reads the root-suppletion class off the realized cells. The hypotheses of the engine's theorems (csg2, exists_portmanteau_of_ne) are decide-checked on each vocabulary, and the two unattested shapes are exhibited as violations of exactly one condition each: AAB violates Grounded ((202)), surface ABA violates Antihomophonous ((44)).

def Bobaljik2012.czechBad : List (Morphology.Containment.ExponenceRule 3 String)

Czech BAD ([Bob12] (39)): root allomorph hor- conditioned by CMPR, elsewhere špatn-.

Equations

• Bobaljik2012.czechBad = [{ exponent := "špatn", spans := 0, context := none }, { exponent := "hor", spans := 0, context := some 1 }]

theorem Bobaljik2012.czech_bad_realize : Morphology.Containment.realize czechBad = ![some "špatn", some "hor", some "hor"]

Elsewhere insertion realizes špatn-ý, hor-ší, nej-hor-ší: ABB.

theorem Bobaljik2012.czech_bad_abb : Morphology.DegreeContainment.degreeShape (Morphology.Containment.realize czechBad) = Morphology.DegreeContainment.abb

def Bobaljik2012.englishGood : List (Morphology.Containment.ExponenceRule 3 String)

English GOOD ([Bob12] (203)): bett- / __]CMPR], elsewhere good. Terminal and adjacent, so the plateau applies.

Equations

• Bobaljik2012.englishGood = [{ exponent := "good", spans := 0, context := none }, { exponent := "bett", spans := 0, context := some 1 }]

theorem Bobaljik2012.english_good_abb : Morphology.DegreeContainment.degreeShape (Morphology.Containment.realize englishGood) = Morphology.DegreeContainment.abb

def Bobaljik2012.englishBad : List (Morphology.Containment.ExponenceRule 3 String)

English BAD ([Bob12] (194)): worse as a √ROOT+CMPR portmanteau, elsewhere bad. ABB arises on the portmanteau route too — worse simply realizes the whole comparative node.

Equations

• Bobaljik2012.englishBad = [{ exponent := "bad", spans := 0, context := none }, { exponent := "worse", spans := 1, context := none }]

theorem Bobaljik2012.english_bad_abb : Morphology.DegreeContainment.degreeShape (Morphology.Containment.realize englishBad) = Morphology.DegreeContainment.abb

def Bobaljik2012.welshGood : List (Morphology.Containment.ExponenceRule 3 String)

Welsh GOOD ([Bob12] (198)): gor- / __]SPRL] and gwell, both √ROOT+CMPR portmanteaux, elsewhere da.

Equations

• Bobaljik2012.welshGood = [{ exponent := "da", spans := 0, context := none }, { exponent := "gwell", spans := 1, context := none }, { exponent := "gor", spans := 1, context := some 2 }]

theorem Bobaljik2012.welsh_good_abc : Morphology.DegreeContainment.degreeShape (Morphology.Containment.realize welshGood) = Morphology.DegreeContainment.abc

da, gwell, gor-au: ABC, generable because the C-exponent is a portmanteau.

def Bobaljik2012.latinBonus : List (Morphology.Containment.ExponenceRule 3 String)

Latin GOOD ([Bob12] (204)): opt- a √ROOT+CMPR portmanteau conditioned by SPRL, mel- a root allomorph conditioned by CMPR, elsewhere bon. The span structure also explains *opt-ior-imus: opt- swallows the CMPR cell, so regular -ior has nothing to realize.

Equations

• Bobaljik2012.latinBonus = [{ exponent := "bon", spans := 0, context := none }, { exponent := "mel", spans := 0, context := some 1 }, { exponent := "opt", spans := 1, context := some 2 }]

theorem Bobaljik2012.latin_bonus_realize : Morphology.Containment.realize latinBonus = ![some "bon", some "mel", some "opt"]

bon-us, mel-ior, opt-imus: the engine derives the book's star ABC paradigm.

theorem Bobaljik2012.latin_realize_abc : Morphology.DegreeContainment.degreeShape (Morphology.Containment.realize latinBonus) = Morphology.DegreeContainment.abc

theorem Bobaljik2012.latin_wellformed : Morphology.Containment.Adjacent latinBonus ∧ Morphology.Containment.Grounded latinBonus ∧ Morphology.Containment.Antihomophonous latinBonus

Latin satisfies every condition the CSG2 derivation needs.

theorem Bobaljik2012.latin_not_terminal : ¬Morphology.Containment.Terminal latinBonus

Latin is not terminal — and must not be: the terminal-adjacent plateau (realize_const_of_terminal_adjacent) would force CMPR = SPRL, wrongly excluding ABC. The portmanteau rule is what escapes it.

theorem Bobaljik2012.latin_superlative_portmanteau : Morphology.Containment.winner latinBonus 2 = some { exponent := "opt", spans := 1, context := some 2 }

Latin's superlative winner computed concretely: the portmanteau opt- — the ABC-requires-portmanteau consequence ([Bob12] §5.3.1, generalized there as (199)).

theorem Bobaljik2012.latin_sprl_needs_portmanteau : ∃ it ∈ latinBonus, Morphology.Containment.winner latinBonus 2 = some it ∧ 0 < ↑it.spans

The engine theorem applied: since Latin's comparative and superlative cells diverge, exists_portmanteau_of_ne forces a portmanteau winner at the superlative.

def Bobaljik2012.latinBonusNS : List (Morphology.Containment.ExponenceRule 3 String)

The nanosyntax lexicon for Latin GOOD, in the [Cah09] method (the degree application is later literature; see Morphology/Containment/Superset.lean): context-free entries storing successively larger constituents, competing under the Superset Principle.

Equations

• Bobaljik2012.latinBonusNS = [{ exponent := "bon", spans := 0, context := none }, { exponent := "mel", spans := 1, context := none }, { exponent := "opt", spans := 2, context := none }]

theorem Bobaljik2012.latin_ns_contextFree : Morphology.Containment.ContextFree latinBonusNS

theorem Bobaljik2012.latin_ns_spellout : Morphology.Containment.spellout latinBonusNS = ![some "bon", some "mel", some "opt"]

Superset spellout derives the same ABC paradigm with no contextual apparatus — the entries are portmanteaus by constituent size alone, doing the work of DM's context-restricted ch. 5 machinery.

theorem Bobaljik2012.latin_ns_eq_dm : Morphology.Containment.spellout latinBonusNS = Morphology.Containment.realize latinBonus

Cross-framework agreement on the data: the nanosyntax lexicon and the DM vocabulary (204) realize the same paradigm cell for cell (the concrete face of Morphology.Containment.spelloutGenerable_iff_generable).

def Bobaljik2012.welshAAB : List (Morphology.Containment.ExponenceRule 3 String)

The hypothetical AAB vocabulary ([Bob12] (201)): gor- restricted to the superlative with no comparative-level counterpart. It generates the unattested AAB shape (*da – da-ch – gor-au)...

Equations

• Bobaljik2012.welshAAB = [{ exponent := "da", spans := 0, context := none }, { exponent := "gor", spans := 1, context := some 2 }]

theorem Bobaljik2012.welshAAB_realizes_aab : Morphology.DegreeContainment.degreeShape (Morphology.Containment.realize welshAAB) = Morphology.DegreeContainment.aab

theorem Bobaljik2012.welshAAB_not_grounded : ¬Morphology.Containment.Grounded welshAAB

...and is excluded by exactly one condition: its threshold set skips the comparative grade, violating Grounded ((202)).

theorem Bobaljik2012.welshAAB_blocked : ¬(Morphology.Containment.Antihomophonous welshAAB ∧ Morphology.Containment.Grounded welshAAB)

The engine theorem csg2 applied: no vocabulary realizing the AAB cells can satisfy both Antihomophony and Grounded — the AAB realization itself refutes the conjunction.

def Bobaljik2012.fakeAba : List (Morphology.Containment.ExponenceRule 3 String)

The homophonous-ABC loophole ([Bob12] (44) discussion): without Antihomophony, surface ABA is generable — a superlative root allomorph accidentally homophonous with the positive.

Equations

• Bobaljik2012.fakeAba = [{ exponent := "A", spans := 0, context := none }, { exponent := "B", spans := 0, context := some 1 }, { exponent := "A", spans := 0, context := some 2 }]

theorem Bobaljik2012.fakeAba_realizes_aba : Morphology.DegreeContainment.degreeShape (Morphology.Containment.realize fakeAba) = Morphology.DegreeContainment.aba

theorem Bobaljik2012.fakeAba_not_antihomophonous : ¬Morphology.Containment.Antihomophonous fakeAba

Synthesis: the Merger layer on the worked vocabularies

theorem Bobaljik2012.english_good_synthetic_comparative : { wordTop := 2 }.SyntheticAt 1

The structural synthetic/analytic notion (Morphology.Containment.Synthesis) on English good: the word merges through the superlative (wordTop = 2), and since the word-internal realization shows distinct root forms at the positive and comparative grades, rsg certifies the comparative as synthetic — the structural counterpart of english_rsg's string-level check.

Scale Generation from Degree Paradigms

ScaleFromParadigm (the Scale-Generation Substrate section above) 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 : (ScaleFromParadigm.adjectiveScale Bobaljik2012.tallStem✝).isSome = true

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

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

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

theorem Bobaljik2012.tall_scale_members : Option.map (fun (x : ScaleFromParadigm.MorphScale) => x.toHornScale.members) (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 : ScaleFromParadigm.MorphScale) => x.toHornScale.members) (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 : ScaleFromParadigm.MorphScale) => x.toHornScale.members) (ScaleFromParadigm.adjectiveScale Bobaljik2012.expensiveStem✝) = some ["expensive", "more expensive", "most expensive"]

Periphrastic paradigm yields multi-word scale members.

Morphological Alternatives

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 : ScaleFromParadigm.morphologicalAlternatives Bobaljik2012.tallStem✝ "tall" = ["taller", "tallest"]

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

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

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