@cite{wellwood-2015}: On the Semantics of Comparison Across Categories

@cite{wellwood-2015}

Data, compositional derivation, and verification theorems from @cite{wellwood-2015}. All comparative sentences — nominal, verbal, and adjectival — share a uniform DegP pipeline in which much introduces a monotonic measure function μ. The cross-categorial parallel (mass/atelic/GA vs count/telic/non-GA) follows from mereological status, and dimensional restriction (§3.4) follows from whether the measured domain is linearly ordered.

Data Sources

• §2.1: Nominal comparatives (mass vs count nouns)
• §2.2: Verbal comparatives (atelic vs telic VPs)
• §3.1–3.2: Adjectival comparatives (gradable vs non-gradable adjectives)
• §3.3: Morphosyntactic evidence (more = much + -er, @cite{bresnan-1973})
• §3.4: Dimensional restriction patterns
• §5: Number morphology and measurement (grammar shifts measurement)
• §6.3: very distribution and covert much

Compositional Derivation (§2.3, §3.2)

The comparative is derived compositionally via the DegP:

1. ⟦much_μ⟧^A = A(μ) — introduces the measure function from the variable assignment (eq. 37)
2. ⟦-er⟧ — introduces strict comparison (>) against a standard
3. ⟦Deg'⟧ = ⟦much_μ + -er⟧ = λd.λα. μ(α) > d (eq. 37.i, 45.i)
4. ⟦ABS⟧ = λg.λd.λα. g(α) ≥ d — links degrees to predicates in the than-clause (eq. 38.ii)
5. ⟦than⟧ = λD. max(D) — selects maximal degree (eq. 38.i)
6. Predicate Modification conjoins DegP with the base predicate
7. Existential closure over the matrix eventuality

The result for all three domains (eqs. 42, 48, 65):

∃α. role(a, α) ∧ P(α) ∧ μ(extract(α)) >
    max{d | ∃α'. role(b, α') ∧ P(α') ∧ μ(extract(α')) ≥ d}

Under unique-event assumptions, this reduces to μ(extract(α_a)) > μ(extract(α_b)), bridging to comparativeSem (@cite{schwarzschild-2008}) and statesComparativeSem (@cite{cariani-santorio-wellwood-2024}).

inductive Wellwood2015.LexCat : Type

Lexical categories relevant to the cross-categorial analysis.

• massNoun : LexCat
• countNoun : LexCat
• atelicVP : LexCat
• telicVP : LexCat
• gradableAdj : LexCat
• nonGradableAdj : LexCat

@[implicit_reducible]

instance Wellwood2015.instDecidableEqLexCat : DecidableEq LexCat

Equations

• Wellwood2015.instDecidableEqLexCat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Wellwood2015.instReprLexCat.repr : LexCat → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Wellwood2015.instReprLexCat : Repr LexCat

Equations

• Wellwood2015.instReprLexCat = { reprPrec := Wellwood2015.instReprLexCat.repr }

structure Wellwood2015.MuchFelicityDatum : Type

Observed felicity of much/more with different lexical categories.

Mass nouns and atelic VPs are felicitous with much and allow multiple measurement dimensions. Count nouns and telic VPs are anomalous. GAs are felicitous but lexically fix a single dimension. Non-GAs are anomalous (not comparable).

Examples from the paper:

• "Al bought more coffee than Bill did." ✓ (VOLUME or WEIGHT)
• "? Al has more idea than Bill does." ✗
• "Al ran more than Bill did." ✓ (DURATION or DISTANCE)
• "? Al graduated high school more than Bill did." ✗
• "Al's coffee is hotter than Bill's." ✓ (TEMPERATURE)
• "? This table is more wooden than that one." ✗

• category : LexCat
• felicitousWithMuch : Bool
• multipleDimensions : Bool

def Wellwood2015.instDecidableEqMuchFelicityDatum.decEq (x✝ x✝¹ : MuchFelicityDatum) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Wellwood2015.instDecidableEqMuchFelicityDatum : DecidableEq MuchFelicityDatum

Equations

• Wellwood2015.instDecidableEqMuchFelicityDatum = Wellwood2015.instDecidableEqMuchFelicityDatum.decEq

def Wellwood2015.instReprMuchFelicityDatum.repr : MuchFelicityDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Wellwood2015.instReprMuchFelicityDatum : Repr MuchFelicityDatum

Equations

• Wellwood2015.instReprMuchFelicityDatum = { reprPrec := Wellwood2015.instReprMuchFelicityDatum.repr }

def Wellwood2015.massNounDatum : MuchFelicityDatum

Equations

• Wellwood2015.massNounDatum = { category := Wellwood2015.LexCat.massNoun, felicitousWithMuch := true, multipleDimensions := true }

def Wellwood2015.countNounDatum : MuchFelicityDatum

Equations

• Wellwood2015.countNounDatum = { category := Wellwood2015.LexCat.countNoun, felicitousWithMuch := false, multipleDimensions := false }

def Wellwood2015.atelicVPDatum : MuchFelicityDatum

Equations

• Wellwood2015.atelicVPDatum = { category := Wellwood2015.LexCat.atelicVP, felicitousWithMuch := true, multipleDimensions := true }

def Wellwood2015.telicVPDatum : MuchFelicityDatum

Equations

• Wellwood2015.telicVPDatum = { category := Wellwood2015.LexCat.telicVP, felicitousWithMuch := false, multipleDimensions := false }

def Wellwood2015.gradableAdjDatum : MuchFelicityDatum

Equations

• Wellwood2015.gradableAdjDatum = { category := Wellwood2015.LexCat.gradableAdj, felicitousWithMuch := true, multipleDimensions := false }

def Wellwood2015.nonGradableAdjDatum : MuchFelicityDatum

Equations

• Wellwood2015.nonGradableAdjDatum = { category := Wellwood2015.LexCat.nonGradableAdj, felicitousWithMuch := false, multipleDimensions := false }

structure Wellwood2015.GrammarShiftDatum : Type

Number morphology and telicity shifts affect available dimensions (§5).

(104) a. "Al found more rock than Bill did." (WEIGHT, VOLUME, *NUMBER) b. "Al found more rocks than Bill did." (*WEIGHT, *VOLUME, NUMBER)

(105) a. "Al ran in the park more than Bill did." (DIST, DUR, NUMBER) b. "Al ran to the park more than Bill did." (*DIST, *DUR, NUMBER)

Shifting from mass → count (plural morpheme) or atelic → telic restricts measurement to NUMBER, blocking extensive dimensions.

• baseForm : String
• shiftedForm : String
• baseExtensive : Bool
• shiftedExtensive : Bool

@[implicit_reducible]

instance Wellwood2015.instReprGrammarShiftDatum : Repr GrammarShiftDatum

Equations

• Wellwood2015.instReprGrammarShiftDatum = { reprPrec := Wellwood2015.instReprGrammarShiftDatum.repr }

def Wellwood2015.instReprGrammarShiftDatum.repr : GrammarShiftDatum → ℕ → Std.Format

Equations

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

def Wellwood2015.rockShift : GrammarShiftDatum

Ex. 104: mass → count via plural morpheme.

Equations

• Wellwood2015.rockShift = { baseForm := "more rock", shiftedForm := "more rocks", baseExtensive := true, shiftedExtensive := false }

def Wellwood2015.runShift : GrammarShiftDatum

Ex. 105: atelic → telic via directional PP.

Equations

• Wellwood2015.runShift = { baseForm := "ran in the park more", shiftedForm := "ran to the park more", baseExtensive := true, shiftedExtensive := false }

inductive Wellwood2015.MeasuredDomain : Type

What is actually measured in a comparative — the ontological domain whose mereological structure determines available dimensions.

The key §3.4 insight: dimension type (intensive vs extensive) tracks the measured domain, not lexical category.

• entity : MeasuredDomain
• event : MeasuredDomain
• state : MeasuredDomain

@[implicit_reducible]

instance Wellwood2015.instDecidableEqMeasuredDomain : DecidableEq MeasuredDomain

Equations

• Wellwood2015.instDecidableEqMeasuredDomain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Wellwood2015.instReprMeasuredDomain : Repr MeasuredDomain

Equations

• Wellwood2015.instReprMeasuredDomain = { reprPrec := Wellwood2015.instReprMeasuredDomain.repr }

def Wellwood2015.instReprMeasuredDomain.repr : MeasuredDomain → ℕ → Std.Format

Equations

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

structure Wellwood2015.DimensionReversalDatum : Type

Dimension reversal: the same syntactic category can measure different ontological domains, and the available dimensions follow from the measured domain, not from the syntactic category.

• form : String
• category : LexCat
• dimensionName : String
• measuredDomain : MeasuredDomain
• intensive : Bool

@[implicit_reducible]

instance Wellwood2015.instReprDimensionReversalDatum : Repr DimensionReversalDatum

Equations

• Wellwood2015.instReprDimensionReversalDatum = { reprPrec := Wellwood2015.instReprDimensionReversalDatum.repr }

def Wellwood2015.instReprDimensionReversalDatum.repr : DimensionReversalDatum → ℕ → Std.Format

Equations

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

def Wellwood2015.hotterDatum : DimensionReversalDatum

(82a): GA measuring states → intensive.

Equations

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

def Wellwood2015.harderDatum : DimensionReversalDatum

(82b): GA measuring states → intensive.

Equations

• Wellwood2015.harderDatum = { form := "harder", category := Wellwood2015.LexCat.gradableAdj, dimensionName := "hardness", measuredDomain := Wellwood2015.MeasuredDomain.state, intensive := true }

def Wellwood2015.moreCoffeeDatum : DimensionReversalDatum

(83a): Mass noun measuring entities → extensive.

Equations

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

def Wellwood2015.morePlasticDatum : DimensionReversalDatum

(83b): Mass noun measuring entities → extensive.

Equations

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

def Wellwood2015.fullerDatum : DimensionReversalDatum

(84a): Reversal — GA but extensive, because measured domain is entity.

Equations

• Wellwood2015.fullerDatum = { form := "fuller", category := Wellwood2015.LexCat.gradableAdj, dimensionName := "volume", measuredDomain := Wellwood2015.MeasuredDomain.entity, intensive := false }

def Wellwood2015.heavierDatum : DimensionReversalDatum

(84b): Reversal — GA but extensive, because measured domain is entity.

Equations

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

def Wellwood2015.moreHeatDatum : DimensionReversalDatum

(85a): Reversal — noun but intensive, because measured domain is state.

Equations

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

def Wellwood2015.moreFirmnessDatum : DimensionReversalDatum

(85b): Reversal — noun but intensive, because measured domain is state.

Equations

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

def Wellwood2015.spedUpMoreDatum : DimensionReversalDatum

(89a): Reversal — verb but intensive, because measured domain is state.

Equations

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

def Wellwood2015.droveMoreDatum : DimensionReversalDatum

(87a): Atelic VP measuring events → extensive.

Equations

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

def Wellwood2015.dimensionReversalData : List DimensionReversalDatum

Equations

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

structure Wellwood2015.StateModificationDatum : Type

States support predicate modification via conjunction (§3.5).

"happy in the morning" = ∃s. happy(s) ∧ Holder(x, s) ∧ in-the-morning(s)

• adjective : String
• modifier : String
• form : String

def Wellwood2015.instReprStateModificationDatum.repr : StateModificationDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Wellwood2015.instReprStateModificationDatum : Repr StateModificationDatum

Equations

• Wellwood2015.instReprStateModificationDatum = { reprPrec := Wellwood2015.instReprStateModificationDatum.repr }

def Wellwood2015.happyMorningDatum : StateModificationDatum

Equations

• Wellwood2015.happyMorningDatum = { adjective := "happy", modifier := "in the morning", form := "happy in the morning" }

def Wellwood2015.patientPlaygroundDatum : StateModificationDatum

Equations

• Wellwood2015.patientPlaygroundDatum = { adjective := "patient", modifier := "with Mary on the playground", form := "patient with Mary on the playground" }

def Wellwood2015.Deg' {α : Type u_1} (μ : α → ℚ) (d : ℚ) (a : α) : Prop

Deg' = much_μ + -er: the comparative degree head.

⟦Deg'⟧^A = λd.λα. A(μ)(α) > d

much_μ introduces the measure function A(μ) from the variable assignment (⟦much_μ⟧^A = A(μ), eq. 37); -er introduces the strict comparison (>). Their combination is the semantic core shared by all comparatives: a degree-parameterized predicate that holds of α iff its measure exceeds d.

Note: the denotation of much_μ is simply A(μ) — a variable assignment lookup — not a predicate. The monotonicity condition (that A(μ) be StrictMono on a part-whole ordering) is a felicity condition on the assignment, not part of the denotation.

(§2.1 eq. 37.i, §2.2 eq. 45.i)

Equations

• Wellwood2015.Deg' μ d a = (μ a > d)

def Wellwood2015.ABS {α : Type u_1} (μ : α → ℚ) (d : ℚ) (a : α) : Prop

ABS: type-shifter linking degrees to eventuality predicates.

⟦ABS⟧^A = λg.λd.λα. g(α) ≥ d

Used in the than-clause to create a set of degrees from a measure function. The weak inequality (≥) in ABS contrasts with the strict inequality (>) in Deg': the matrix uses >, the standard uses ≥, following @cite{von-stechow-1984}.

(§2.1 eq. 38.ii)

Equations

• Wellwood2015.ABS μ d a = (μ a ≥ d)

def Wellwood2015.IsMaxDeg (S : Set ℚ) (δ : ℚ) : Prop

⟦than⟧ = λD. max(D): a degree δ is the maximum of a degree set iff it belongs to the set and no element exceeds it.

(§2.1 eq. 38.i; @cite{von-stechow-1984}, @cite{heim-2001})

Equations

• Wellwood2015.IsMaxDeg S δ = (δ ∈ S ∧ ∀ d ∈ S, d ≤ δ)

Nominal comparative derivation (§2.1, eqs. 36–42)

"Al drank more coffee than Bill did"

Bottom-up composition (eq. 37):

1. ⟦Deg'⟧^A = λd.λα. A(μ)(α) > d                     (eq. 37.i: IE, FA)
2. ⟦DegP⟧^A = λα. A(μ)(α) > δ                         (eq. 37.ii: FA with δ)
3. ⟦NP⟧^A = λy. coffee(y) ∧ A(μ)(y) > δ               (eq. 37.iii: PM)
4. ⟦eP⟧^A = εy[coffee(y) ∧ A(μ)(y) > δ]               (eq. 37.iv: ε)
5. ⟦VP⟧^A = λe. drink(e)(εy[...])                      (eq. 37.v: FA)
6. ⟦vP⟧^A = λx.λe. Agent(e)(x) ∧ VP(e)                (eq. 37.vi: EI)
7. ⟦S⟧^A = λe. Agent(e)(a) ∧ VP(e)                     (eq. 37.vii: FA)
8. = ⊤ iff ∃e[Agent(e)(a) ∧ ...]                       (eq. 37.viii: ∃-closure)

Than-clause (eqs. 39–41):
δ = max(λd.∃e[Agent(e)(b) ∧ drink(e)(εy[coffee(y) ∧ A(μ)(y) ≥ d])])

Full truth conditions (eq. 42):
∃e[Agent(e)(a) ∧ drink(e)(εx[coffee(x) ∧ A(μ)(x) >
  max(λd.∃e'[Agent(e')(b) ∧ drink(e')(εy[coffee(y) ∧ A(μ)(y) ≥ d])])])]

Abstracting away ε, with `themeOf` extracting the measured entity:
∃ea. Agent(a, ea) ∧ P(ea) ∧ μ(theme(ea)) >
  max{d | ∃eb. Agent(b, eb) ∧ P(eb) ∧ μ(theme(eb)) ≥ d}

Verbal comparative derivation (§2.2, eqs. 43–48)

"Al ran more than Bill did"

1. ⟦Deg'⟧^A = λd.λα. A(μ)(α) > d                     (eq. 45.i)
2. ⟦DegP⟧^A = λα. A(μ)(α) > δ                         (eq. 45.ii)
3. ⟦VP⟧^A = λe. run(e) ∧ A(μ)(e) > δ                  (eq. 45.iii: PM)
4. ⟦vP⟧^A = λx.λe. Agent(e)(x) ∧ run(e) ∧ A(μ)(e) > δ (eq. 45.iv: EI)
5. ⟦S⟧^A = λe. Agent(e)(a) ∧ run(e) ∧ A(μ)(e) > δ     (eq. 45.v: FA)
6. = ⊤ iff ∃e[Agent(e)(a) ∧ run(e) ∧ A(μ)(e) > δ]     (eq. 45.vi: ∃-closure)

Than-clause (eq. 47):
δ = max(λd.∃e[Agent(e)(b) ∧ run(e) ∧ A(μ)(e) ≥ d])

Full truth conditions (eq. 48):
∃e'[Agent(e')(a) ∧ run(e') ∧ A(μ)(e') >
  max(λd.∃e[Agent(e)(b) ∧ run(e) ∧ A(μ)(e) ≥ d])]

Adjectival comparative derivation (§3.2, eqs. 58–65)

"Al's coffee is hotter than Bill's"

1. ⟦hot⟧ = λs.hot(s)                                   (eq. 58)
2. ⟦much_μ hot⟧^A = λd.λs. hot(s) ∧ A(μ)(s) ≥ d       (eq. 60)
3. After -er: λd.λs. hot(s) ∧ A(μ)(s) > d              (eq. 61)
4. ⟦DegP⟧ = λs. hot(s) ∧ A(μ)(s) > δ                  (eq. 62)
5. ∃s[Holder(s)(a) ∧ hot(s) ∧ A(μ)(s) > δ]             (eq. 65)

Tree (97) — adjectival with modifiers via PM:
⟦more patient with Mary on the playground⟧ =
  λs. A(μ)(s) > δ ∧ patient(s) ∧ with(s)(m) ∧ on(s)(p)

def Wellwood2015.thanDegreesHetero {Ent : Type u_1} {α : Type u_2} {Measured : Type u_3} (role : Ent → α → Prop) (Pthan : α → Prop) (extract : α → Measured) (μ : Measured → ℚ) (b : Ent) : Set ℚ

Heterogeneous than-clause degree set, allowing distinct matrix and than-clause predicates: degrees d such that some b-eventuality satisfying Pthan has a measured value at least d.

Used by intensity comparatives (Phenomena/Attitudes/Studies/Pasternak2019.lean) where the matrix and than-clause have different themes, e.g., Ann hates Bill more than Matt hates Jeff — both sides use the hate predicate but conjoined with different theme-roles.

Equations

• Wellwood2015.thanDegreesHetero role Pthan extract μ b = {d : ℚ | ∃ (eb : α), role b eb ∧ Pthan eb ∧ μ (extract eb) ≥ d}

def Wellwood2015.comparativeTruthHetero {Ent : Type u_1} {α : Type u_2} {Measured : Type u_3} (role : Ent → α → Prop) (Pmatrix Pthan : α → Prop) (extract : α → Measured) (μ : Measured → ℚ) (a b : Ent) : Prop

The paper's compositional comparative truth condition, generalized to allow distinct matrix and than-clause predicates (Pmatrix, Pthan). The original homogeneous form (eqs. 42, 48, 65 of @cite{wellwood-2015} where matrix and than-clause use the same P) is the special case where Pmatrix = Pthan; see comparativeTruth below.

The heterogeneous form is needed for intensity comparatives (@cite{pasternak-2019} (53)) where matrix and than-clause have different themes, e.g., Ann hates Bill more than Matt hates Jeff.

Equations

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

def Wellwood2015.comparativeTruth {Ent : Type u_1} {α : Type u_2} {Measured : Type u_3} (role : Ent → α → Prop) (P : α → Prop) (extract : α → Measured) (μ : Measured → ℚ) (a b : Ent) : Prop

The original (homogeneous) comparative truth condition: matrix and than-clause use the same predicate. One-line specialization of the heterogeneous form. Existing consumers (nominalComparative, verbalComparative, adjectivalComparative) and downstream proof scripts unchanged.

"a V-s more P than b does" is true iff there exists an a-eventuality ea satisfying P, and a degree δ that is the max of the than-clause degree set, such that μ(extract(ea)) > δ.

Compositional derivation (eqs. 42, 48, 65 of @cite{wellwood-2015}): (1) much_μ introduces the measure function A(μ) (2) -er introduces strict comparison (>) against the standard δ (3) The than-clause provides δ = max{d | ∃eb. role(b,eb) ∧ P(eb) ∧ μ(extract(eb)) ≥ d} (4) Predicate Modification conjoins the degree condition with the base predicate (5) Existential closure over the matrix eventuality

The three Wellwood-2015 domains differ only in the thematic role, extraction function, and measured ontological sort:

Domain	role	extract	Measured	Example
Nominal	Agent	themeOf	Entity	"more coffee than"
Verbal	Agent	id	Event	"ran more than"
Adjectival	Holder	id	State	"hotter than"

Equations

• Wellwood2015.comparativeTruth role P extract μ a b = Wellwood2015.comparativeTruthHetero role P P extract μ a b

def Wellwood2015.thanDegrees {Ent : Type u_1} {α : Type u_2} {Measured : Type u_3} (role : Ent → α → Prop) (P : α → Prop) (extract : α → Measured) (μ : Measured → ℚ) (b : Ent) : Set ℚ

The original thanDegrees is the homogeneous specialization of thanDegreesHetero.

Equations

• Wellwood2015.thanDegrees role P extract μ b = Wellwood2015.thanDegreesHetero role P extract μ b

def Wellwood2015.nominalComparative {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (frame : Semantics.ArgumentStructure.ThematicFrame Entity Time) (P : Semantics.Events.EvPred Time) (themeOf : Semantics.Events.Event Time → Entity) (μ : Entity → ℚ) (a b : Entity) : Prop

Nominal comparative (§2.1, eq. 42): "Al bought more coffee than Bill did."

Measured domain: entities (via themeOf). Role: Agent. Extract: themeOf (the consumed/affected entity).

Equations

• Wellwood2015.nominalComparative frame P themeOf μ a b = Wellwood2015.comparativeTruth frame.agent P themeOf μ a b

def Wellwood2015.verbalComparative {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (frame : Semantics.ArgumentStructure.ThematicFrame Entity Time) (P : Semantics.Events.EvPred Time) (μ : Semantics.Events.Event Time → ℚ) (a b : Entity) : Prop

Verbal comparative (§2.2, eq. 48): "Al ran more than Bill did."

Measured domain: events directly (extract = id). Role: Agent.

Equations

• Wellwood2015.verbalComparative frame P μ a b = Wellwood2015.comparativeTruth frame.agent P id μ a b

def Wellwood2015.adjectivalComparative {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (frame : Semantics.ArgumentStructure.ThematicFrame Entity Time) (P : Semantics.Events.EvPred Time) (μ : Semantics.Events.Event Time → ℚ) (a b : Entity) : Prop

Adjectival comparative (§3.2, eq. 65): "This coffee is hotter than that coffee."

Measured domain: states directly (extract = id). Role: Holder.

Equations

• Wellwood2015.adjectivalComparative frame P μ a b = Wellwood2015.comparativeTruth frame.holder P id μ a b

theorem Wellwood2015.comparativeTruthHetero_max {Ent : Type u_1} {α : Type u_2} {Measured : Type u_3} {role : Ent → α → Prop} {Pmatrix Pthan : α → Prop} {extract : α → Measured} {μ : Measured → ℚ} {a b : Ent} {ea eb : α} (ha : role a ea ∧ Pmatrix ea) (ha_unique : ∀ (e : α), role a e → Pmatrix e → e = ea) (hb : role b eb ∧ Pthan eb) (hb_unique : ∀ (e : α), role b e → Pthan e → e = eb) : comparativeTruthHetero role Pmatrix Pthan extract μ a b ↔ μ (extract eb) < μ (extract ea)

Heterogeneous-predicate maximality reduction. Under unique-witness assumptions on both matrix (Pmatrix) and than-clause (Pthan), the comparative reduces to direct measure comparison. The original homogeneous comparativeTruth_max is the special case Pmatrix = Pthan.

theorem Wellwood2015.comparativeTruth_max {Ent : Type u_1} {α : Type u_2} {Measured : Type u_3} {role : Ent → α → Prop} {P : α → Prop} {extract : α → Measured} {μ : Measured → ℚ} {a b : Ent} {ea eb : α} (ha : role a ea ∧ P ea) (ha_unique : ∀ (e : α), role a e → P e → e = ea) (hb : role b eb ∧ P eb) (hb_unique : ∀ (e : α), role b e → P e → e = eb) : comparativeTruth role P extract μ a b ↔ μ (extract eb) < μ (extract ea)

Original maximality reduction (homogeneous case): one-line specialization of comparativeTruthHetero_max.

When b has a unique P-eventuality eb, the than-clause degree set {d | μ(extract(eb)) ≥ d} has max = μ(extract(eb)), so the comparative becomes μ(extract(ea)) > μ(extract(eb)).

theorem Wellwood2015.adjectival_max_reduces {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] {frame : Semantics.ArgumentStructure.ThematicFrame Entity Time} {P : Semantics.Events.EvPred Time} {μ : Semantics.Events.Event Time → ℚ} {a b : Entity} {sa sb : Semantics.Events.Event Time} (ha : frame.holder a sa ∧ P sa) (ha_unique : ∀ (s : Semantics.Events.Event Time), frame.holder a s → P s → s = sa) (hb : frame.holder b sb ∧ P sb) (hb_unique : ∀ (s : Semantics.Events.Event Time), frame.holder b s → P s → s = sb) : adjectivalComparative frame P μ a b ↔ μ sb < μ sa

Adjectival comparative under maximality reduces to μ(sb) < μ(sa).

theorem Wellwood2015.statesComparativeSem_is_lt {S : Type u_1} {D : Type u_2} [Preorder S] [Preorder D] (μ : S → D) (sa sb : S) : Semantics.Gradability.StatesBased.statesComparativeSem μ sa sb ↔ μ sb < μ sa

CSW's statesComparativeSem is definitionally μ sb < μ sa.

theorem Wellwood2015.max_eq_comparativeSem {Entity : Type u_1} {Time : Type u_2} {Measured : Type u_3} [LinearOrder Time] {role : Entity → Semantics.Events.Event Time → Prop} {P : Semantics.Events.EvPred Time} {extract : Semantics.Events.Event Time → Measured} {μ : Measured → ℚ} {a b : Entity} {ea eb : Semantics.Events.Event Time} (ha : role a ea ∧ P ea) (ha_unique : ∀ (e : Semantics.Events.Event Time), role a e → P e → e = ea) (hb : role b eb ∧ P eb) (hb_unique : ∀ (e : Semantics.Events.Event Time), role b e → P e → e = eb) : comparativeTruth role P extract μ a b ↔ Semantics.Degree.Comparative.comparativeSem (μ ∘ extract) ea eb Core.Scale.ScalePolarity.positive

All comparative domains under maximality = comparativeSem (Rett/Schwarzschild) on measured values.

theorem Wellwood2015.state_domain_restricted {S : Type u_1} [LinearOrder S] : Semantics.Measurement.DimensionallyRestricted S

State domains are dimensionally restricted when linearly ordered.

theorem Wellwood2015.not_restricted_of_disagreement {α : Type u_1} [Preorder α] {μ₁ μ₂ : α → ℚ} (hμ₁ : StrictMono μ₁) (hμ₂ : StrictMono μ₂) {a b : α} (h₁ : μ₁ a < μ₁ b) (h₂ : ¬μ₂ a < μ₂ b) : ¬Semantics.Measurement.DimensionallyRestricted α

If two admissible measures disagree on some pair, the domain is NOT dimensionally restricted.

def Wellwood2015.lexCatToStatus : LexCat → Semantics.Measurement.MereologicalStatus

Map LexCat to MereologicalStatus using the theory's bridges.

Equations

• Wellwood2015.lexCatToStatus Wellwood2015.LexCat.massNoun = Semantics.Measurement.numberToStatus Semantics.Kinds.MeaningPreservation.NumberFeature.mass
• Wellwood2015.lexCatToStatus Wellwood2015.LexCat.countNoun = Semantics.Measurement.numberToStatus Semantics.Kinds.MeaningPreservation.NumberFeature.sg
• Wellwood2015.lexCatToStatus Wellwood2015.LexCat.atelicVP = Semantics.Measurement.telicityToStatus Features.Telicity.atelic
• Wellwood2015.lexCatToStatus Wellwood2015.LexCat.telicVP = Semantics.Measurement.telicityToStatus Features.Telicity.telic
• Wellwood2015.lexCatToStatus Wellwood2015.LexCat.gradableAdj = Semantics.Measurement.gradableToStatus
• Wellwood2015.lexCatToStatus Wellwood2015.LexCat.nonGradableAdj = Semantics.Measurement.nonGradableToStatus

def Wellwood2015.statusPredictsFelicitous : Semantics.Measurement.MereologicalStatus → Bool

Equations

• Wellwood2015.statusPredictsFelicitous Semantics.Measurement.MereologicalStatus.cumulative = true
• Wellwood2015.statusPredictsFelicitous Semantics.Measurement.MereologicalStatus.quantized = false

theorem Wellwood2015.massNoun_felicity : statusPredictsFelicitous (lexCatToStatus LexCat.massNoun) = massNounDatum.felicitousWithMuch

theorem Wellwood2015.countNoun_felicity : statusPredictsFelicitous (lexCatToStatus LexCat.countNoun) = countNounDatum.felicitousWithMuch

theorem Wellwood2015.atelicVP_felicity : statusPredictsFelicitous (lexCatToStatus LexCat.atelicVP) = atelicVPDatum.felicitousWithMuch

theorem Wellwood2015.telicVP_felicity : statusPredictsFelicitous (lexCatToStatus LexCat.telicVP) = telicVPDatum.felicitousWithMuch

theorem Wellwood2015.gradableAdj_felicity : statusPredictsFelicitous (lexCatToStatus LexCat.gradableAdj) = gradableAdjDatum.felicitousWithMuch

theorem Wellwood2015.nonGradableAdj_felicity : statusPredictsFelicitous (lexCatToStatus LexCat.nonGradableAdj) = nonGradableAdjDatum.felicitousWithMuch

theorem Wellwood2015.massNoun_atelicVP_same_status : lexCatToStatus LexCat.massNoun = lexCatToStatus LexCat.atelicVP

theorem Wellwood2015.countNoun_telicVP_same_status : lexCatToStatus LexCat.countNoun = lexCatToStatus LexCat.telicVP

theorem Wellwood2015.gradableAdj_patterns_with_cum : lexCatToStatus LexCat.gradableAdj = lexCatToStatus LexCat.massNoun

theorem Wellwood2015.nonGradableAdj_patterns_with_qua : lexCatToStatus LexCat.nonGradableAdj = lexCatToStatus LexCat.countNoun

theorem Wellwood2015.run_shift_via_telicize : have p := Features.activityProfile; Semantics.Measurement.telicityToStatus p.telicity = Semantics.Measurement.MereologicalStatus.cumulative ∧ Semantics.Measurement.telicityToStatus p.telicize.telicity = Semantics.Measurement.MereologicalStatus.quantized

theorem Wellwood2015.build_shift_via_atelicize : have p := Features.accomplishmentProfile; Semantics.Measurement.telicityToStatus p.telicity = Semantics.Measurement.MereologicalStatus.quantized ∧ Semantics.Measurement.telicityToStatus p.atelicize.telicity = Semantics.Measurement.MereologicalStatus.cumulative

theorem Wellwood2015.rock_shift_status : lexCatToStatus LexCat.massNoun = Semantics.Measurement.MereologicalStatus.cumulative ∧ lexCatToStatus LexCat.countNoun = Semantics.Measurement.MereologicalStatus.quantized

theorem Wellwood2015.massNoun_open_scale : (lexCatToStatus LexCat.massNoun).toBoundedness = Core.Scale.Boundedness.open_

theorem Wellwood2015.countNoun_closed_scale : (lexCatToStatus LexCat.countNoun).toBoundedness = Core.Scale.Boundedness.closed

theorem Wellwood2015.atelicVP_open_scale : (lexCatToStatus LexCat.atelicVP).toBoundedness = Core.Scale.Boundedness.open_

theorem Wellwood2015.telicVP_closed_scale : (lexCatToStatus LexCat.telicVP).toBoundedness = Core.Scale.Boundedness.closed

def Wellwood2015.measuredDomainRestricted : MeasuredDomain → Bool

Equations

• Wellwood2015.measuredDomainRestricted Wellwood2015.MeasuredDomain.state = true
• Wellwood2015.measuredDomainRestricted Wellwood2015.MeasuredDomain.entity = false
• Wellwood2015.measuredDomainRestricted Wellwood2015.MeasuredDomain.event = false

theorem Wellwood2015.hotter_restricted : measuredDomainRestricted hotterDatum.measuredDomain = hotterDatum.intensive

theorem Wellwood2015.harder_restricted : measuredDomainRestricted harderDatum.measuredDomain = harderDatum.intensive

theorem Wellwood2015.moreCoffee_not_restricted : measuredDomainRestricted moreCoffeeDatum.measuredDomain = moreCoffeeDatum.intensive

theorem Wellwood2015.morePlastic_not_restricted : measuredDomainRestricted morePlasticDatum.measuredDomain = morePlasticDatum.intensive

theorem Wellwood2015.fuller_not_restricted : measuredDomainRestricted fullerDatum.measuredDomain = fullerDatum.intensive

theorem Wellwood2015.heavier_not_restricted : measuredDomainRestricted heavierDatum.measuredDomain = heavierDatum.intensive

theorem Wellwood2015.moreHeat_restricted : measuredDomainRestricted moreHeatDatum.measuredDomain = moreHeatDatum.intensive

theorem Wellwood2015.moreFirmness_restricted : measuredDomainRestricted moreFirmnessDatum.measuredDomain = moreFirmnessDatum.intensive

theorem Wellwood2015.spedUpMore_restricted : measuredDomainRestricted spedUpMoreDatum.measuredDomain = spedUpMoreDatum.intensive

theorem Wellwood2015.droveMore_not_restricted : measuredDomainRestricted droveMoreDatum.measuredDomain = droveMoreDatum.intensive

theorem Wellwood2015.state_mod_pm_bridge {Entity : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Semantics.Events.EvPred Time) (frame : Semantics.ArgumentStructure.ThematicFrame Entity Time) (x : Entity) (M : Semantics.ArgumentStructure.EventModifier Time) : Semantics.ArgumentStructure.modifiedStativeLogicalForm P frame x M ↔ Semantics.ArgumentStructure.stativeLogicalForm (Semantics.ArgumentStructure.modify P M) frame x

structure Wellwood2015.VeryDistributionDatum : Type

§6.3: very distribution tracks overt vs covert much.

• GAs: much is covert → very combines directly ("very hot", *"very much hot")
• N/V: much must be overt → very requires overt much ("very much coffee", *"very coffee")

• category : LexCat
• requiresOvertMuch : Bool
• felicitousExample : String
• infelicitousExample : String

def Wellwood2015.instReprVeryDistributionDatum.repr : VeryDistributionDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Wellwood2015.instReprVeryDistributionDatum : Repr VeryDistributionDatum

Equations

• Wellwood2015.instReprVeryDistributionDatum = { reprPrec := Wellwood2015.instReprVeryDistributionDatum.repr }

def Wellwood2015.veryWithGA : VeryDistributionDatum

Equations

• Wellwood2015.veryWithGA = { category := Wellwood2015.LexCat.gradableAdj, requiresOvertMuch := false, felicitousExample := "very hot", infelicitousExample := "*very much hot" }

def Wellwood2015.veryWithNoun : VeryDistributionDatum

Equations

• Wellwood2015.veryWithNoun = { category := Wellwood2015.LexCat.massNoun, requiresOvertMuch := true, felicitousExample := "very much coffee", infelicitousExample := "*very coffee" }

def Wellwood2015.veryWithVerb : VeryDistributionDatum

Equations

• Wellwood2015.veryWithVerb = { category := Wellwood2015.LexCat.atelicVP, requiresOvertMuch := true, felicitousExample := "very much ran", infelicitousExample := "*very ran" }

theorem Wellwood2015.very_requires_much_iff_not_ga : veryWithGA.requiresOvertMuch = false ∧ veryWithNoun.requiresOvertMuch = true ∧ veryWithVerb.requiresOvertMuch = true

The very distribution follows from whether much is overt or covert: GAs have covert much, so very combines directly (eq. 118). N/V require overt much, so very must co-occur with much (eq. 117).

theorem Wellwood2015.very_ga_is_cum : lexCatToStatus veryWithGA.category = Semantics.Measurement.MereologicalStatus.cumulative

very without overt much correlates with CUM (felicitous with much): GAs are CUM and don't require overt much; N/V are CUM but require it. The asymmetry: GAs have covert much, N/V need overt much.

Connection to @cite{krifka-1998}'s CUM/QUA propagation

@cite{wellwood-2015}'s cross-categorial parallel — mass nouns pattern with atelic VPs, count nouns with telic VPs — is explained by @cite{krifka-1998}'s telicity-through-quantization theory. Krifka shows that the VP inherits its mereological status from the NP via the incremental theme role:

• CUM propagation: CumTheta(θ) ∧ CUM(OBJ) → CUM(VP θ OBJ) "eat apples" is CUM because APPLES is CUM and EAT's theme is cumulative.

• QUA propagation: UP(θ) ∧ SINC(θ) ∧ QUA(OBJ) → QUA(VP θ OBJ) "eat two apples" is QUA because TWO-APPLES is QUA and EAT's theme is SINC.

Wellwood's claim that much-felicity tracks mereological status then follows compositionally: an atelic VP is felicitous with much because it inherits CUM from its mass-noun object; a telic VP is infelicitous because it inherits QUA from its quantized object.

The bridge theorems below connect Krifka's formal CUM/QUA predicates (on VP denotations) to Wellwood's MereologicalStatus classification and statusPredictsFelicitous.

theorem Wellwood2015.cum_vp_measurable {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) [Semantics.ArgumentStructure.IsCumThetaVerb θ] {OBJ : α → Prop} (hObj : Mereology.CUM OBJ) : statusPredictsFelicitous (Semantics.Measurement.telicityToStatus Features.Telicity.atelic) = true ∧ Mereology.CUM (Semantics.Aspect.Cumulativity.VP θ OBJ)

CUM(VP) → VP is measurable by much (cumulative status).

If @cite{krifka-1998}'s CUM propagation gives us CUM(VP θ OBJ), the VP's mereological status is .cumulative, predicting felicity with much and availability of multiple measurement dimensions (DURATION, DISTANCE, etc.).

theorem Wellwood2015.qua_vp_not_measurable {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) [Semantics.Aspect.Incremental.IsSincVerb θ] {OBJ : α → Prop} (hQua : Mereology.QUA OBJ) : statusPredictsFelicitous (Semantics.Measurement.telicityToStatus Features.Telicity.telic) = false ∧ Mereology.QUA (Semantics.Aspect.Cumulativity.VP θ OBJ)

QUA(VP) → VP is NOT measurable by much (quantized status).

If @cite{krifka-1998}'s QUA propagation gives us QUA(VP θ OBJ), the VP's mereological status is .quantized, predicting infelicity with much. Only NUMBER remains as a measurement dimension.

theorem Wellwood2015.grammar_shifts_via_krifka {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) [Semantics.Aspect.Incremental.IsSincVerb θ] {OBJ_cum OBJ_qua : α → Prop} (hCumObj : Mereology.CUM OBJ_cum) (hQuaObj : Mereology.QUA OBJ_qua) : Mereology.CUM (Semantics.Aspect.Cumulativity.VP θ OBJ_cum) ∧ Mereology.QUA (Semantics.Aspect.Cumulativity.VP θ OBJ_qua)

Grammar shifts measurement (§5): telicization of a CUM VP yields a QUA VP.

@cite{wellwood-2015} ex. 105: "ran in the park more" (atelic, CUM, extensive dimensions) vs "ran to the park more" (telic, QUA, NUMBER only).

@cite{krifka-1998}'s theory explains why: the directional PP introduces a quantized path argument, and QUA propagation through SINC transmits QUA to the VP, blocking extensive measurement.

This theorem connects the two accounts: given a CUM VP (from CUM propagation) and a QUA VP (from QUA propagation with a different object), the measurement status shifts from cumulative to quantized.

structure Wellwood2015.CrossCategorialDatum : Type

A cross-categorial comparison construction template: the same DegP shell applies across syntactic categories. @cite{wellwood-2015} §2, @cite{bresnan-1973}

• domain : String

  Syntactic domain (nominal, verbal, adjectival)

• comparativeExample : String

  Example comparative sentence

• equativeExample : String

  Example equative sentence

• degreeWord : String

  The degree word used

@[implicit_reducible]

instance Wellwood2015.instReprCrossCategorialDatum : Repr CrossCategorialDatum

Equations

• Wellwood2015.instReprCrossCategorialDatum = { reprPrec := Wellwood2015.instReprCrossCategorialDatum.repr }

def Wellwood2015.instReprCrossCategorialDatum.repr : CrossCategorialDatum → ℕ → Std.Format

Equations

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

def Wellwood2015.crossCategorialExamples : List CrossCategorialDatum

Equations

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

def Wellwood2015.crossCategorialQP : Bresnan1973.QP

@cite{bresnan-1973} decomposition: more = -er + much.

Wellwood's cross-categorial claim: the SAME QP underlies more across nominal ("more coffee"), verbal ("ran more"), and adverbial ("more quickly") domains. The adjectival domain ("taller") differs only by Much Deletion (Rule 10): much deletes before adjectives.

The formal QP structure and suppletion are in Bresnan1973.

Equations

• Wellwood2015.crossCategorialQP = { det := Bresnan1973.Det.er, q := Bresnan1973.Q.much }

theorem Wellwood2015.crossCategorial_more_from_suppletion : Bresnan1973.suppletion crossCategorialQP = some "more"

The surface form "more" derives from Bresnan's suppletion.

theorem Wellwood2015.covert_much_is_bresnan_deletion : Bresnan1973.muchDeletionApplies Bresnan1973.Q.much true = true

Wellwood §6.3: GAs have "covert much" — very combines directly with the adjective without overt much ("very hot", *"very much hot").

This is exactly Bresnan's Rule 10 (Much Deletion): much → ∅ before an adjective. The formal muchDeletionApplies predicate from Bresnan1973 captures when the deletion fires.

theorem Wellwood2015.overt_much_no_deletion : Bresnan1973.muchDeletionApplies Bresnan1973.Q.much false = false

N/V retain overt much because Much Deletion only applies before A. adjFollows = false → Much Deletion does not apply.