[Wel15]: On the Semantics of Comparison Across Categories

Nominal ("more coffee"), verbal ("ran more"), and adjectival ("hotter") comparatives share one DegP pipeline: covert much denotes an assignment-supplied monotonic measure function (eqs. 7/28) and -er compares strictly against the maximal than-clause degree (eq. 38; [vS84], [Rul95]), yielding the same truth condition in all three domains (eqs. 42/48/65). Felicity with much tracks mereological status; dimension availability tracks the measured domain, not lexical category (§3.4).

Main declarations

• comparativeTruth / equativeTruth: the shared truth conditions for -er and as (eq. 27), instances of Degree.maxComparative / Degree.maxEquative.
• matrix_derivation_denotes / than_derivation_denotes: the derivations run type-driven through the [HK98] engine — one lexicon (-er, much, ABS, a role head) and one tree derive every domain's matrix and than-clause by FA/PM/EI/closure, and derivation_eq_comparativeTruth assembles them into eqs. 42/48/65.
• nominalComparative, verbalComparative, adjectivalComparative: the three domain instantiations (role × extraction).
• coffee_much_matches … wooden_much_matches: the §§2–3 felicity judgments predicted per-lexeme from fragment entries and substrate status maps; qua_measures_vacuously_admissible gives the mereological reason (antichains trivialize monotone measurement).
• model_restricted_iff / dimension_tracks_domain / dimension_not_category: §3.4 as order theory — exactly the state domain's model is DimensionallyRestricted, matching the intensive dimensions of exs. 82–89, while the category-based rival is refuted.
• very_tracks_much_deletion: the §6.3 very asymmetry derived from [Bre73] Much Deletion.

Implementation notes

Monotonicity of A(μ) is a felicity condition on the assignment, not part of the denotation. Example sentences and judgments are generated from Data/Examples/Wellwood2015.json; theorems consume them directly, with lexical categories derived from Fragments/English entries rather than annotated.

The measured domain (§3.4)

inductive Wellwood2015.MeasuredDomain : Type

What a comparative measures — the ontological domain whose mereological structure determines the 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_reducible]

instance Wellwood2015.instDecidableEqMeasuredDomain : DecidableEq MeasuredDomain

Equations

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

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

Equations

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

@[instance_reducible]

instance Wellwood2015.instReprMeasuredDomain : Repr MeasuredDomain

Equations

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

def Wellwood2015.measuredDomainOfFeature : String → Option MeasuredDomain

Parse a measuredDomain paper-feature of a generated example.

Equations

• Wellwood2015.measuredDomainOfFeature "entity" = some Wellwood2015.MeasuredDomain.entity
• Wellwood2015.measuredDomainOfFeature "event" = some Wellwood2015.MeasuredDomain.event
• Wellwood2015.measuredDomainOfFeature "state" = some Wellwood2015.MeasuredDomain.state
• Wellwood2015.measuredDomainOfFeature x✝ = none

The comparative truth condition (§§2.1–3.2)

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 truth condition shared by eqs. 42/48/65: some role-a eventuality satisfies P and measures strictly above the maximal than-clause degree. The domains differ only in role (Agent/Holder) and extraction (themeOf/id).

Equations

• Wellwood2015.comparativeTruth role P extract μ a b = Degree.maxComparative (fun (e : α) => role a e ∧ P e) (fun (e : α) => role b e ∧ P e) fun (e : α) => μ (extract e)

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

The equative truth condition (eq. 27.ii): as much compares weakly — some role-a eventuality satisfies P and measures at least the maximal as-clause degree. The same pipeline as comparativeTruth with ⪰ for ≻ ([Bre73]'s as filling the same Det slot).

Equations

• Wellwood2015.equativeTruth role P extract μ a b = Degree.maxEquative (fun (e : α) => role a e ∧ P e) (fun (e : α) => role b e ∧ P e) fun (e : α) => μ (extract e)

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

-er is strictly stronger than as (eq. 27.i ⇒ 27.ii).

The compositional derivation (§§2.1–3.2)

The paper's derivation steps as combinators, proven to compose to comparativeTruth.

def Wellwood2015.matrixDegP {α : Type u_2} (μ : α → ℚ) (δ : ℚ) (e : α) : Prop

⟦much_μ⟧^A = A(μ) composed with ⟦-er⟧: a strict degree threshold (37.i/45.i).

Equations

• Wellwood2015.matrixDegP μ δ e = (μ e > δ)

def Wellwood2015.absDegP {α : Type u_2} (μ : α → ℚ) (d : ℚ) (e : α) : Prop

ABS (38.ii): the weak degree threshold of the than-clause.

Equations

• Wellwood2015.absDegP μ d e = (μ e ≥ d)

def Wellwood2015.predMod {α : Type u_2} (P Q : α → Prop) (e : α) : Prop

Predicate Modification: intersective conjunction (37.iii/45.iii).

Equations

• Wellwood2015.predMod P Q e = (P e ∧ Q e)

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

The than-clause (39–41/47): degree abstraction over the ∃-closed ABS-composed clause.

Equations

• Wellwood2015.thanClause role P μ b = {d : ℚ | ∃ (e : α), role b e ∧ Wellwood2015.predMod P (Wellwood2015.absDegP μ d) e}

def Wellwood2015.matrixClause {Ent : Type u_1} {α : Type u_2} (role : Ent → α → Prop) (P : α → Prop) (μ : α → ℚ) (a : Ent) (δ : ℚ) : Prop

The matrix clause (37.viii/45.vi): ∃-closure over the PM of the base predicate with the DegP at standard δ.

Equations

• Wellwood2015.matrixClause role P μ a δ = ∃ (e : α), role a e ∧ Wellwood2015.predMod P (Wellwood2015.matrixDegP μ δ) e

theorem Wellwood2015.derivation_eq_comparativeTruth {Ent : Type u_1} {α : Type u_2} {Measured : Type u_3} (role : Ent → α → Prop) (P : α → Prop) (extract : α → Measured) (μ : Measured → ℚ) (a b : Ent) : (∃ (δ : ℚ), IsGreatest (thanClause role P (fun (e : α) => μ (extract e)) b) δ ∧ matrixClause role P (fun (e : α) => μ (extract e)) a δ) ↔ comparativeTruth role P extract μ a b

The derivation composes: max-selecting the than-clause standard for the matrix clause is comparativeTruth (eqs. 42/48/65).

The derivations, type-driven

The step-licensed derivations (37.i–viii, 45.i–vi, 61) run through the shared [HK98] engine (Semantics/Composition/Tree.lean): one lexicon — -er, much (eqs. 7/28), ABS (38.ii), the standard δ, a base predicate, and a [Kra96] role head — and one tree shape, composed by FA, PM, EI, FA, and existential closure. Degree abstraction for the than-clause (39–41) is the meta-language λ over the same tree with ABS in place of -er. The cross-categorial thesis is the parametricity: nominal, verbal, and adjectival matrices are the SAME tree at different (role, predicate, measure) cells.

@[reducible, inline]

abbrev Wellwood2015.Dom (Ent α : Type) : Type

The sorted composition domain: individuals ⊕ eventualities.

Equations

• Wellwood2015.Dom Ent α = (Ent ⊕ α)

def Wellwood2015.lexicon {Ent α : Type} (role : Ent → α → Prop) (P : α → Prop) (μ0 : α → ℚ) (subj : Ent) (δ : ℚ) : Semantics.Montague.Lexicon (Dom Ent α) Unit

Wellwood's lexicon over the engine: much is the assignment-supplied measure (eqs. 7/28), -er the strict and ABS (38.ii) the weak degree head, role a [Kra96] role head composing by EI.

Equations

• One or more equations did not get rendered due to their size.
• Wellwood2015.lexicon role P μ0 subj δ "δ" = some { ty := Intensional.Ty.d, denot := have this := δ; this }
• Wellwood2015.lexicon role P μ0 subj δ "subj" = some { ty := Intensional.Ty.e, denot := Sum.inl subj }
• Wellwood2015.lexicon role P μ0 subj δ w = none

def Wellwood2015.matrixTree : Syntax.Tree Unit String

The shared matrix tree (37.i–viii / 45.i–vi): [EC [subj [role [pred [[er much] δ]]]]] — Deg′ = FA(-er, much), DegP = FA(Deg′, δ), VP = PM, vP = EI, S = FA, then closure.

Equations

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

def Wellwood2015.thanTree : Syntax.Tree Unit String

The than-clause body (39–41/47): the same tree with ABS (38.ii) for -er.

Equations

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

theorem Wellwood2015.matrix_derivation_denotes {Ent α : Type} (role : Ent → α → Prop) (P : α → Prop) (μ0 : α → ℚ) (a : Ent) (δ : ℚ) (g : Assignment (Dom Ent α)) : Semantics.Composition.Tree.interp (Dom Ent α) Unit (lexicon role P μ0 a δ) g matrixTree = some { ty := Intensional.Ty.t, val := pure (matrixClause role P μ0 a δ) }

The engine derives the matrix clause: type-driven interpretation of matrixTree succeeds and denotes matrixClause (45.vi / 37.viii).

theorem Wellwood2015.than_derivation_denotes {Ent α : Type} (role : Ent → α → Prop) (P : α → Prop) (μ0 : α → ℚ) (b : Ent) (d : ℚ) (g : Assignment (Dom Ent α)) : Semantics.Composition.Tree.interp (Dom Ent α) Unit (lexicon role P μ0 b d) g thanTree = some { ty := Intensional.Ty.t, val := pure (d ∈ thanClause role P μ0 b) }

The engine derives the than-clause degree set pointwise: at each degree d, thanTree denotes membership of d in thanClause (39–41/47); degree abstraction is the meta-language λ over d.

Three domain instantiations

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

Nominal comparative (§2.1, eq. 42): Agent role, entities measured via themeOf.

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 : ArgumentStructure.ThematicFrame Entity Time) (P : Event Time → Prop) (μ : Event Time → ℚ) (a b : Entity) : Prop

Verbal comparative (§2.2, eq. 48): Agent role, events measured directly.

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 : ArgumentStructure.ThematicFrame Entity Time) (P : Event Time → Prop) (μ : Event Time → ℚ) (a b : Entity) : Prop

Adjectival comparative (§3.2, eq. 65): Holder role, states measured directly.

Equations

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

Mereological status (§§2–3)

The paper's two-way cross-categorial classification and its bridges to the feature substrate. Interpretive notes: the paper does not label GA state domains "cumulative" in Krifka's technical sense — it argues they "form mereologies" (ordered domains with proper parts); we classify them .cumulative because the structural consequence (monotonic measurability) is the same.

inductive Wellwood2015.MereologicalStatus : Type

Cross-categorial mereological classification (§§2–3): cumulative domains have proper-part structure enabling monotonic measurement by much (mass nouns, atelic VPs, GA state domains); quantized domains lack it (count nouns, telic VPs, non-GA states).

• cumulative : MereologicalStatus
• quantized : MereologicalStatus

@[instance_reducible]

instance Wellwood2015.instDecidableEqMereologicalStatus : DecidableEq MereologicalStatus

Equations

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

@[instance_reducible]

instance Wellwood2015.instReprMereologicalStatus : Repr MereologicalStatus

Equations

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

def Wellwood2015.instReprMereologicalStatus.repr : MereologicalStatus → ℕ → Std.Format

Equations

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

def Wellwood2015.telicityToStatus : Features.Telicity → MereologicalStatus

Telicity determines status: atelic VPs are CUM, telic VPs QUA.

Equations

• Wellwood2015.telicityToStatus Features.Telicity.atelic = Wellwood2015.MereologicalStatus.cumulative
• Wellwood2015.telicityToStatus Features.Telicity.telic = Wellwood2015.MereologicalStatus.quantized

def Wellwood2015.numberToStatus : Semantics.Kinds.MeaningPreservation.NumberFeature → MereologicalStatus

Number determines status: mass CUM; count (sg/pl/neutral) QUA at the lexical level (plural CUM-at-plurality measures only NUMBER).

Equations

• Wellwood2015.numberToStatus Semantics.Kinds.MeaningPreservation.NumberFeature.mass = Wellwood2015.MereologicalStatus.cumulative
• Wellwood2015.numberToStatus Semantics.Kinds.MeaningPreservation.NumberFeature.sg = Wellwood2015.MereologicalStatus.quantized
• Wellwood2015.numberToStatus Semantics.Kinds.MeaningPreservation.NumberFeature.pl = Wellwood2015.MereologicalStatus.quantized
• Wellwood2015.numberToStatus Semantics.Kinds.MeaningPreservation.NumberFeature.neutral = Wellwood2015.MereologicalStatus.quantized

def Wellwood2015.gradableToStatus : MereologicalStatus

GA state domains form mereologies (see the section note).

Equations

• Wellwood2015.gradableToStatus = Wellwood2015.MereologicalStatus.cumulative

def Wellwood2015.nonGradableToStatus : MereologicalStatus

Non-GA states are atomic and unordered — QUA as the closest label.

Equations

• Wellwood2015.nonGradableToStatus = Wellwood2015.MereologicalStatus.quantized

theorem Wellwood2015.telicize_shifts_status (p : Features.AspectualProfile) (h : p.telicity = Features.Telicity.atelic) : telicityToStatus p.telicity = MereologicalStatus.cumulative ∧ telicityToStatus p.telicize.telicity = MereologicalStatus.quantized

Telicization (§5) shifts status from cumulative to quantized.

Felicity from the lexicon (§§2–3)

Each felicity observation predicted from shared substrate: fragment entries where the lexicon has them (coffee, idea, run, hot), the paper's feature assignment otherwise.

def Wellwood2015.predictsFelicitous (s : MereologicalStatus) : Prop

much is predicted felicitous exactly with cumulative status.

Equations

• Wellwood2015.predictsFelicitous s = (s = Wellwood2015.MereologicalStatus.cumulative)

@[instance_reducible]

instance Wellwood2015.instDecidablePredMereologicalStatusPredictsFelicitous : DecidablePred predictsFelicitous

Equations

• Wellwood2015.instDecidablePredMereologicalStatusPredictsFelicitous s = Wellwood2015.instDecidablePredMereologicalStatusPredictsFelicitous._aux_1 s

def Wellwood2015.nounNumber (e : English.Nouns.NounEntry) : Semantics.Kinds.MeaningPreservation.NumberFeature

The lexical-level number feature of a fragment noun entry.

Equations

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

theorem Wellwood2015.coffee_much_matches : predictsFelicitous (numberToStatus (nounNumber English.Nouns.coffee)) ↔ Examples.felicity_mass.judgment = Features.Judgment.acceptable

"Al bought more coffee than Bill did" (§2.1): the fragment's mass entry gives cumulative status, predicting the recorded judgment.

theorem Wellwood2015.idea_much_matches : predictsFelicitous (numberToStatus (nounNumber English.Nouns.idea)) ↔ Examples.felicity_count.judgment = Features.Judgment.acceptable

"?Al has more idea than Bill does" (§2.1): count entry ⇒ quantized ⇒ anomalous.

theorem Wellwood2015.run_much_matches : English.Predicates.Verbal.run.vendlerClass = some Features.VendlerClass.activity ∧ (predictsFelicitous (telicityToStatus Features.Telicity.atelic) ↔ Examples.felicity_atelic.judgment = Features.Judgment.acceptable)

"Al ran more than Bill did" (§2.2): run is an activity in the fragment; atelic status predicts the recorded judgment.

theorem Wellwood2015.telic_much_matches : predictsFelicitous (telicityToStatus Features.Telicity.telic) ↔ Examples.felicity_telic.judgment = Features.Judgment.acceptable

"?Al graduated high school more than Bill did" (§2.2): telic ⇒ quantized ⇒ anomalous.

theorem Wellwood2015.hot_much_matches : predictsFelicitous gradableToStatus ↔ Examples.felicity_ga.judgment = Features.Judgment.acceptable

"Al's coffee is hotter than Bill's" (§3.1): GA state domains form mereologies (English.Predicates.Adjectival.hot carries a scalar dimension).

theorem Wellwood2015.wooden_much_matches : predictsFelicitous nonGradableToStatus ↔ Examples.felicity_nonga.judgment = Features.Judgment.acceptable

"?This piece of wood is more wooden than that one" (ex. 53a): non-GA states are atomic and unordered ⇒ anomalous.

theorem Wellwood2015.qua_measures_vacuously_admissible {α : Type u_1} [PartialOrder α] {P : α → Prop} (hQ : Mereology.QUA P) (μ : α → ℚ) : StrictMonoOn μ {x : α | P x}

Why quantized reference blocks much: a quantized extension is an antichain, so every measure is vacuously admissible on it — monotone measurement cannot discriminate, leaving only counting (many).

Dimensional restriction (§3.4)

@[reducible, inline]

abbrev Wellwood2015.MeasuredDomain.Model : MeasuredDomain → Type

Order model of a measured domain: states are linearly ordered; entity and event domains have incomparable parts (weight × volume, distance × duration).

Equations

• Wellwood2015.MeasuredDomain.state.Model = ℚ
• Wellwood2015.MeasuredDomain.entity.Model = (ℚ × ℚ)
• Wellwood2015.MeasuredDomain.event.Model = (ℚ × ℚ)

@[instance_reducible]

instance Wellwood2015.instPreorderModel (m : MeasuredDomain) : Preorder m.Model

Equations

• Wellwood2015.instPreorderModel Wellwood2015.MeasuredDomain.state = { toLE := Rat.instLE, toLT := Rat.instLT, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := Rat.lt_iff_le_not_ge }
• Wellwood2015.instPreorderModel Wellwood2015.MeasuredDomain.entity = { toLE := Prod.instLE_mathlib, toLT := Prod.instPreorder.toLT, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }
• Wellwood2015.instPreorderModel Wellwood2015.MeasuredDomain.event = { toLE := Prod.instLE_mathlib, toLT := Prod.instPreorder.toLT, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

theorem Wellwood2015.model_restricted_iff (m : MeasuredDomain) : Degree.DimensionallyRestricted m.Model ↔ m = MeasuredDomain.state

§3.4 as order theory: exactly the state domain is dimensionally restricted.

theorem Wellwood2015.dimension_tracks_domain (e : Data.Examples.LinguisticExample) : e ∈ Examples.all → ∀ (m : MeasuredDomain), (e.feature? "measuredDomain").bind measuredDomainOfFeature = some m → (Degree.DimensionallyRestricted m.Model ↔ e.feature? "intensive" = some "true")

§3.4 verified over the example annotations (exs. 82–89): the measured domain's order model is dimensionally restricted iff the observed dimension is intensive.

theorem Wellwood2015.dimension_not_category : ¬∀ e ∈ Examples.all, e.feature? "dataset" = some "dimension" → (e.feature? "category" = some "gradableAdj" ↔ e.feature? "intensive" = some "true")

The lexicalist rival §3.4 argues against — dimension fixed by category — fails on the reversal data (fuller, ex. 84a; more heat, ex. 85a).

Grammar shifts measurement (§5)

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

Ex. (105): telicization (the directional PP) shifts cumulative to quantized.

Bresnan's decomposition (§3.3)

def Wellwood2015.crossCategorialQP : Bresnan1973.QP

[Bre73]'s QP -er + much, underlying more in all domains; adjectives differ only by Much Deletion (Wellwood's (74)).

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.

very distribution (§6.3)

theorem Wellwood2015.very_tracks_much_deletion (e : Data.Examples.LinguisticExample) : e ∈ Examples.all → e.feature? "dataset" = some "very" → (e.feature? "requiresOvertMuch" = some "true" ↔ Bresnan1973.muchDeletionApplies Bresnan1973.Q.much (e.feature? "category" == some "gradableAdj") = false)

The §6.3 very asymmetry (exs. 117–118) follows from Much Deletion: much deletes exactly before adjectives, so only GAs host covert much, and very requires overt much everywhere else.