@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 Phenomena.Comparison.Studies.Wellwood2015.LexCat : Type

Lexical categories relevant to the cross-categorial analysis.

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

instance Phenomena.Comparison.Studies.Wellwood2015.instDecidableEqLexCat : DecidableEq LexCat

Equations

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

instance Phenomena.Comparison.Studies.Wellwood2015.instBEqLexCat : BEq LexCat

Equations

• Phenomena.Comparison.Studies.Wellwood2015.instBEqLexCat = { beq := Phenomena.Comparison.Studies.Wellwood2015.instBEqLexCat.beq }

def Phenomena.Comparison.Studies.Wellwood2015.instBEqLexCat.beq : LexCat → LexCat → Bool

Equations

• Phenomena.Comparison.Studies.Wellwood2015.instBEqLexCat.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Comparison.Studies.Wellwood2015.instReprLexCat.repr : LexCat → ℕ → Std.Format

Equations

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

instance Phenomena.Comparison.Studies.Wellwood2015.instReprLexCat : Repr LexCat

Equations

• Phenomena.Comparison.Studies.Wellwood2015.instReprLexCat = { reprPrec := Phenomena.Comparison.Studies.Wellwood2015.instReprLexCat.repr }

structure Phenomena.Comparison.Studies.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 Phenomena.Comparison.Studies.Wellwood2015.instDecidableEqMuchFelicityDatum.decEq (x✝ x✝¹ : MuchFelicityDatum) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Comparison.Studies.Wellwood2015.instDecidableEqMuchFelicityDatum : DecidableEq MuchFelicityDatum

Equations

• Phenomena.Comparison.Studies.Wellwood2015.instDecidableEqMuchFelicityDatum = Phenomena.Comparison.Studies.Wellwood2015.instDecidableEqMuchFelicityDatum.decEq

instance Phenomena.Comparison.Studies.Wellwood2015.instBEqMuchFelicityDatum : BEq MuchFelicityDatum

Equations

• Phenomena.Comparison.Studies.Wellwood2015.instBEqMuchFelicityDatum = { beq := Phenomena.Comparison.Studies.Wellwood2015.instBEqMuchFelicityDatum.beq }

def Phenomena.Comparison.Studies.Wellwood2015.instBEqMuchFelicityDatum.beq : MuchFelicityDatum → MuchFelicityDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Comparison.Studies.Wellwood2015.instBEqMuchFelicityDatum.beq x✝¹ x✝ = false

instance Phenomena.Comparison.Studies.Wellwood2015.instReprMuchFelicityDatum : Repr MuchFelicityDatum

Equations

• Phenomena.Comparison.Studies.Wellwood2015.instReprMuchFelicityDatum = { reprPrec := Phenomena.Comparison.Studies.Wellwood2015.instReprMuchFelicityDatum.repr }

def Phenomena.Comparison.Studies.Wellwood2015.instReprMuchFelicityDatum.repr : MuchFelicityDatum → ℕ → Std.Format

Equations

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

def Phenomena.Comparison.Studies.Wellwood2015.massNounDatum : MuchFelicityDatum

Equations

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

def Phenomena.Comparison.Studies.Wellwood2015.countNounDatum : MuchFelicityDatum

Equations

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

def Phenomena.Comparison.Studies.Wellwood2015.atelicVPDatum : MuchFelicityDatum

Equations

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

def Phenomena.Comparison.Studies.Wellwood2015.telicVPDatum : MuchFelicityDatum

Equations

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

def Phenomena.Comparison.Studies.Wellwood2015.gradableAdjDatum : MuchFelicityDatum

Equations

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

def Phenomena.Comparison.Studies.Wellwood2015.nonGradableAdjDatum : MuchFelicityDatum

Equations

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

structure Phenomena.Comparison.Studies.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

instance Phenomena.Comparison.Studies.Wellwood2015.instReprGrammarShiftDatum : Repr GrammarShiftDatum

Equations

• Phenomena.Comparison.Studies.Wellwood2015.instReprGrammarShiftDatum = { reprPrec := Phenomena.Comparison.Studies.Wellwood2015.instReprGrammarShiftDatum.repr }

def Phenomena.Comparison.Studies.Wellwood2015.instReprGrammarShiftDatum.repr : GrammarShiftDatum → ℕ → Std.Format

Equations

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

def Phenomena.Comparison.Studies.Wellwood2015.rockShift : GrammarShiftDatum

Ex. 104: mass → count via plural morpheme.

Equations

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

def Phenomena.Comparison.Studies.Wellwood2015.runShift : GrammarShiftDatum

Ex. 105: atelic → telic via directional PP.

Equations

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

inductive Phenomena.Comparison.Studies.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

instance Phenomena.Comparison.Studies.Wellwood2015.instDecidableEqMeasuredDomain : DecidableEq MeasuredDomain

Equations

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

def Phenomena.Comparison.Studies.Wellwood2015.instBEqMeasuredDomain.beq : MeasuredDomain → MeasuredDomain → Bool

Equations

• Phenomena.Comparison.Studies.Wellwood2015.instBEqMeasuredDomain.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Comparison.Studies.Wellwood2015.instBEqMeasuredDomain : BEq MeasuredDomain

Equations

• Phenomena.Comparison.Studies.Wellwood2015.instBEqMeasuredDomain = { beq := Phenomena.Comparison.Studies.Wellwood2015.instBEqMeasuredDomain.beq }

def Phenomena.Comparison.Studies.Wellwood2015.instReprMeasuredDomain.repr : MeasuredDomain → ℕ → Std.Format

Equations

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

instance Phenomena.Comparison.Studies.Wellwood2015.instReprMeasuredDomain : Repr MeasuredDomain

Equations

• Phenomena.Comparison.Studies.Wellwood2015.instReprMeasuredDomain = { reprPrec := Phenomena.Comparison.Studies.Wellwood2015.instReprMeasuredDomain.repr }

structure Phenomena.Comparison.Studies.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

instance Phenomena.Comparison.Studies.Wellwood2015.instReprDimensionReversalDatum : Repr DimensionReversalDatum

Equations

• Phenomena.Comparison.Studies.Wellwood2015.instReprDimensionReversalDatum = { reprPrec := Phenomena.Comparison.Studies.Wellwood2015.instReprDimensionReversalDatum.repr }

def Phenomena.Comparison.Studies.Wellwood2015.instReprDimensionReversalDatum.repr : DimensionReversalDatum → ℕ → Std.Format

Equations

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

def Phenomena.Comparison.Studies.Wellwood2015.hotterDatum : DimensionReversalDatum

(82a): GA measuring states → intensive.

Equations

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

def Phenomena.Comparison.Studies.Wellwood2015.harderDatum : DimensionReversalDatum

(82b): GA measuring states → intensive.

Equations

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

def Phenomena.Comparison.Studies.Wellwood2015.moreCoffeeDatum : DimensionReversalDatum

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

Equations

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

def Phenomena.Comparison.Studies.Wellwood2015.morePlasticDatum : DimensionReversalDatum

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

Equations

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

def Phenomena.Comparison.Studies.Wellwood2015.fullerDatum : DimensionReversalDatum

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

Equations

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

def Phenomena.Comparison.Studies.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 Phenomena.Comparison.Studies.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 Phenomena.Comparison.Studies.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 Phenomena.Comparison.Studies.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 Phenomena.Comparison.Studies.Wellwood2015.droveMoreDatum : DimensionReversalDatum

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

Equations

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

def Phenomena.Comparison.Studies.Wellwood2015.dimensionReversalData : List DimensionReversalDatum

Equations

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

structure Phenomena.Comparison.Studies.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

instance Phenomena.Comparison.Studies.Wellwood2015.instReprStateModificationDatum : Repr StateModificationDatum

Equations

• Phenomena.Comparison.Studies.Wellwood2015.instReprStateModificationDatum = { reprPrec := Phenomena.Comparison.Studies.Wellwood2015.instReprStateModificationDatum.repr }

def Phenomena.Comparison.Studies.Wellwood2015.instReprStateModificationDatum.repr : StateModificationDatum → ℕ → Std.Format

Equations

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

def Phenomena.Comparison.Studies.Wellwood2015.happyMorningDatum : StateModificationDatum

Equations

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

def Phenomena.Comparison.Studies.Wellwood2015.patientPlaygroundDatum : StateModificationDatum

Equations

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

def Phenomena.Comparison.Studies.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

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

def Phenomena.Comparison.Studies.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

• Phenomena.Comparison.Studies.Wellwood2015.ABS μ d a = (μ a ≥ d)

def Phenomena.Comparison.Studies.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

• Phenomena.Comparison.Studies.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 Phenomena.Comparison.Studies.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 than-clause degree set: the set of degrees d such that some b-eventuality satisfying P has a measured value at least d.

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

This is the ABS-mediated degree set from the than-clause (eq. 40 for nominal, eq. 47 for verbal, eq. 63 for adjectival).

Equations

• Phenomena.Comparison.Studies.Wellwood2015.thanDegrees role P extract μ b = {d : ℚ | ∃ (eb : α), role b eb ∧ P eb ∧ μ (extract eb) ≥ d}

def Phenomena.Comparison.Studies.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 paper's compositional comparative truth condition (eqs. 42, 48, 65).

"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)) > δ.

This is the result of composing: (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 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

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

def Phenomena.Comparison.Studies.Wellwood2015.nominalComparative {Entity : Type u_1} {Time : Type u_2} [LE Time] (frame : Semantics.Events.ThematicRoles.ThematicFrame Entity Time) (P : Semantics.Events.EvPred Time) (themeOf : Semantics.Events.Ev 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

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

def Phenomena.Comparison.Studies.Wellwood2015.verbalComparative {Entity : Type u_1} {Time : Type u_2} [LE Time] (frame : Semantics.Events.ThematicRoles.ThematicFrame Entity Time) (P : Semantics.Events.EvPred Time) (μ : Semantics.Events.Ev 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

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

def Phenomena.Comparison.Studies.Wellwood2015.adjectivalComparative {Entity : Type u_1} {Time : Type u_2} [LE Time] (frame : Semantics.Events.ThematicRoles.ThematicFrame Entity Time) (P : Semantics.Events.EvPred Time) (μ : Semantics.Events.Ev 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

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

theorem Phenomena.Comparison.Studies.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)

Under unique-event assumptions, the max of the than-clause degree set is μ(extract(eb)), and the comparative reduces to direct comparison.

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 Phenomena.Comparison.Studies.Wellwood2015.adjectival_max_reduces {Entity : Type u_1} {Time : Type u_2} [LE Time] {frame : Semantics.Events.ThematicRoles.ThematicFrame Entity Time} {P : Semantics.Events.EvPred Time} {μ : Semantics.Events.Ev Time → ℚ} {a b : Entity} {sa sb : Semantics.Events.Ev Time} (ha : frame.holder a sa ∧ P sa) (ha_unique : ∀ (s : Semantics.Events.Ev Time), frame.holder a s → P s → s = sa) (hb : frame.holder b sb ∧ P sb) (hb_unique : ∀ (s : Semantics.Events.Ev 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 Phenomena.Comparison.Studies.Wellwood2015.statesComparativeSem_is_lt {S : Type u_1} {D : Type u_2} [Preorder S] [Preorder D] (μ : S → D) (sa sb : S) : Semantics.Lexical.Adjective.StatesBased.statesComparativeSem μ sa sb ↔ μ sb < μ sa

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

theorem Phenomena.Comparison.Studies.Wellwood2015.max_eq_comparativeSem {Entity : Type u_1} {Time : Type u_2} {Measured : Type u_3} [LE Time] {role : Entity → Semantics.Events.Ev Time → Prop} {P : Semantics.Events.EvPred Time} {extract : Semantics.Events.Ev Time → Measured} {μ : Measured → ℚ} {a b : Entity} {ea eb : Semantics.Events.Ev Time} (ha : role a ea ∧ P ea) (ha_unique : ∀ (e : Semantics.Events.Ev Time), role a e → P e → e = ea) (hb : role b eb ∧ P eb) (hb_unique : ∀ (e : Semantics.Events.Ev 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 Phenomena.Comparison.Studies.Wellwood2015.state_domain_restricted {S : Type u_1} [LinearOrder S] : Semantics.Lexical.Measurement.DimensionallyRestricted S

State domains are dimensionally restricted when linearly ordered.

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

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

def Phenomena.Comparison.Studies.Wellwood2015.lexCatToStatus : LexCat → Semantics.Lexical.Measurement.MereologicalStatus

Map LexCat to MereologicalStatus using the theory's bridges.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Comparison.Studies.Wellwood2015.lexCatToStatus Phenomena.Comparison.Studies.Wellwood2015.LexCat.gradableAdj = Semantics.Lexical.Measurement.gradableToStatus
• Phenomena.Comparison.Studies.Wellwood2015.lexCatToStatus Phenomena.Comparison.Studies.Wellwood2015.LexCat.nonGradableAdj = Semantics.Lexical.Measurement.nonGradableToStatus

def Phenomena.Comparison.Studies.Wellwood2015.statusPredictsFelicitous : Semantics.Lexical.Measurement.MereologicalStatus → Bool

Equations

• Phenomena.Comparison.Studies.Wellwood2015.statusPredictsFelicitous Semantics.Lexical.Measurement.MereologicalStatus.cumulative = true
• Phenomena.Comparison.Studies.Wellwood2015.statusPredictsFelicitous Semantics.Lexical.Measurement.MereologicalStatus.quantized = false

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

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

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

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

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

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

theorem Phenomena.Comparison.Studies.Wellwood2015.massNoun_atelicVP_same_status : lexCatToStatus LexCat.massNoun = lexCatToStatus LexCat.atelicVP

theorem Phenomena.Comparison.Studies.Wellwood2015.countNoun_telicVP_same_status : lexCatToStatus LexCat.countNoun = lexCatToStatus LexCat.telicVP

theorem Phenomena.Comparison.Studies.Wellwood2015.gradableAdj_patterns_with_cum : lexCatToStatus LexCat.gradableAdj = lexCatToStatus LexCat.massNoun

theorem Phenomena.Comparison.Studies.Wellwood2015.nonGradableAdj_patterns_with_qua : lexCatToStatus LexCat.nonGradableAdj = lexCatToStatus LexCat.countNoun

theorem Phenomena.Comparison.Studies.Wellwood2015.run_shift_via_telicize : have p := Semantics.Tense.Aspect.LexicalAspect.activityProfile; Semantics.Lexical.Measurement.telicityToStatus p.telicity = Semantics.Lexical.Measurement.MereologicalStatus.cumulative ∧ Semantics.Lexical.Measurement.telicityToStatus p.telicize.telicity = Semantics.Lexical.Measurement.MereologicalStatus.quantized

theorem Phenomena.Comparison.Studies.Wellwood2015.build_shift_via_atelicize : have p := Semantics.Tense.Aspect.LexicalAspect.accomplishmentProfile; Semantics.Lexical.Measurement.telicityToStatus p.telicity = Semantics.Lexical.Measurement.MereologicalStatus.quantized ∧ Semantics.Lexical.Measurement.telicityToStatus p.atelicize.telicity = Semantics.Lexical.Measurement.MereologicalStatus.cumulative

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

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

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

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

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

def Phenomena.Comparison.Studies.Wellwood2015.measuredDomainRestricted : MeasuredDomain → Bool

Equations

• Phenomena.Comparison.Studies.Wellwood2015.measuredDomainRestricted Phenomena.Comparison.Studies.Wellwood2015.MeasuredDomain.state = true
• Phenomena.Comparison.Studies.Wellwood2015.measuredDomainRestricted Phenomena.Comparison.Studies.Wellwood2015.MeasuredDomain.entity = false
• Phenomena.Comparison.Studies.Wellwood2015.measuredDomainRestricted Phenomena.Comparison.Studies.Wellwood2015.MeasuredDomain.event = false

theorem Phenomena.Comparison.Studies.Wellwood2015.hotter_restricted : measuredDomainRestricted hotterDatum.measuredDomain = hotterDatum.intensive

theorem Phenomena.Comparison.Studies.Wellwood2015.harder_restricted : measuredDomainRestricted harderDatum.measuredDomain = harderDatum.intensive

theorem Phenomena.Comparison.Studies.Wellwood2015.moreCoffee_not_restricted : measuredDomainRestricted moreCoffeeDatum.measuredDomain = moreCoffeeDatum.intensive

theorem Phenomena.Comparison.Studies.Wellwood2015.morePlastic_not_restricted : measuredDomainRestricted morePlasticDatum.measuredDomain = morePlasticDatum.intensive

theorem Phenomena.Comparison.Studies.Wellwood2015.fuller_not_restricted : measuredDomainRestricted fullerDatum.measuredDomain = fullerDatum.intensive

theorem Phenomena.Comparison.Studies.Wellwood2015.heavier_not_restricted : measuredDomainRestricted heavierDatum.measuredDomain = heavierDatum.intensive

theorem Phenomena.Comparison.Studies.Wellwood2015.moreHeat_restricted : measuredDomainRestricted moreHeatDatum.measuredDomain = moreHeatDatum.intensive

theorem Phenomena.Comparison.Studies.Wellwood2015.moreFirmness_restricted : measuredDomainRestricted moreFirmnessDatum.measuredDomain = moreFirmnessDatum.intensive

theorem Phenomena.Comparison.Studies.Wellwood2015.spedUpMore_restricted : measuredDomainRestricted spedUpMoreDatum.measuredDomain = spedUpMoreDatum.intensive

theorem Phenomena.Comparison.Studies.Wellwood2015.droveMore_not_restricted : measuredDomainRestricted droveMoreDatum.measuredDomain = droveMoreDatum.intensive

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

structure Phenomena.Comparison.Studies.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 Phenomena.Comparison.Studies.Wellwood2015.instReprVeryDistributionDatum.repr : VeryDistributionDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Comparison.Studies.Wellwood2015.instReprVeryDistributionDatum : Repr VeryDistributionDatum

Equations

• Phenomena.Comparison.Studies.Wellwood2015.instReprVeryDistributionDatum = { reprPrec := Phenomena.Comparison.Studies.Wellwood2015.instReprVeryDistributionDatum.repr }

def Phenomena.Comparison.Studies.Wellwood2015.veryWithGA : VeryDistributionDatum

Equations

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

def Phenomena.Comparison.Studies.Wellwood2015.veryWithNoun : VeryDistributionDatum

Equations

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

def Phenomena.Comparison.Studies.Wellwood2015.veryWithVerb : VeryDistributionDatum

Equations

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

theorem Phenomena.Comparison.Studies.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 Phenomena.Comparison.Studies.Wellwood2015.very_ga_is_cum : lexCatToStatus veryWithGA.category = Semantics.Lexical.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 Phenomena.Comparison.Studies.Wellwood2015.cum_vp_measurable {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} {OBJ : α → Prop} (hCum : Semantics.Events.Krifka1998.CumTheta θ) (hObj : Mereology.CUM OBJ) : statusPredictsFelicitous (Semantics.Lexical.Measurement.telicityToStatus Semantics.Tense.Aspect.LexicalAspect.Telicity.atelic) = true ∧ Mereology.CUM (Semantics.Events.Krifka1998.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 Phenomena.Comparison.Studies.Wellwood2015.qua_vp_not_measurable {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} {OBJ : α → Prop} (hUP : Semantics.Events.Krifka1998.UP θ) (hSinc : Semantics.Events.Krifka1998.SINC θ) (hQua : Mereology.QUA OBJ) : statusPredictsFelicitous (Semantics.Lexical.Measurement.telicityToStatus Semantics.Tense.Aspect.LexicalAspect.Telicity.telic) = false ∧ Mereology.QUA (Semantics.Events.Krifka1998.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 Phenomena.Comparison.Studies.Wellwood2015.grammar_shifts_via_krifka {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} {OBJ_cum OBJ_qua : α → Prop} (hCumTheta : Semantics.Events.Krifka1998.CumTheta θ) (hCumObj : Mereology.CUM OBJ_cum) (hUP : Semantics.Events.Krifka1998.UP θ) (hSinc : Semantics.Events.Krifka1998.SINC θ) (hQuaObj : Mereology.QUA OBJ_qua) : Mereology.CUM (Semantics.Events.Krifka1998.VP θ OBJ_cum) ∧ Mereology.QUA (Semantics.Events.Krifka1998.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 Phenomena.Comparison.Studies.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

instance Phenomena.Comparison.Studies.Wellwood2015.instReprCrossCategorialDatum : Repr CrossCategorialDatum

Equations

• Phenomena.Comparison.Studies.Wellwood2015.instReprCrossCategorialDatum = { reprPrec := Phenomena.Comparison.Studies.Wellwood2015.instReprCrossCategorialDatum.repr }

def Phenomena.Comparison.Studies.Wellwood2015.instReprCrossCategorialDatum.repr : CrossCategorialDatum → ℕ → Std.Format

Equations

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

def Phenomena.Comparison.Studies.Wellwood2015.crossCategorialExamples : List CrossCategorialDatum

Equations

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

def Phenomena.Comparison.Studies.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

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

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

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

theorem Phenomena.Comparison.Studies.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 Phenomena.Comparison.Studies.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.