Wellwood (2015): On the Semantics of Comparison Across Categories

Wellwood proposes that nominal, verbal and adjectival comparatives contain one degree-introducing morpheme, much, which denotes an assignment-supplied measure function, while -er and as compare the measure of what the base predicate applies to with the maximal degree of the than-clause, after von Stechow and Rullmann. The three domains share one truth condition, and the paper's derivations are one tree interpreted by Heim and Kratzer's engine at three lexical cells, measuring coffee, running events or heat states. What much measures must be non-trivially ordered by part-whole structure and measured monotonically, which a quantized domain cannot be. Which dimensions a comparative allows follows from what is measured rather than from the category of the measuring word, and the obligatory much of very with nouns and verbs is Bresnan's Much Deletion.

Main definitions

• comparativeTruth: the cross-categorial truth condition of the comparative.
• NontriviallyStructured: a domain with a satisfier properly part of another.
• MeasuredDomain.Model: the order model of what a comparative measures.

Main results

• matrix_derivation_denotes: the engine derives the matrix clause.
• nontriviallyStructured_of_cum: a cumulative domain with two satisfiers is non-trivially structured.
• model_restricted_iff: only states fix the comparative ordering for every admissible measure.
• very_much_deletion: Much Deletion.

Implementation notes

Degrees are rationals and eventualities an abstract event type; the engine's sorted domain is the sum of individuals and eventualities, and existential closure is a lexical item. The order models of the measured domains are the reals for states and the componentwise-ordered plane for entities and events. The bare-adjective, measure-phrase and scalar-change discussions of the paper's objections section are not formalized.

References

• [Wel15]
• [Bre73]
• [HK98]
• [Kra96]
• [Rul95]
• [Sch06b]
• [vS84]

The truth conditions

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 comparative, (42), (48), (65), holds when some eventuality bearing the role to a satisfies P and measures strictly above the maximal than-clause degree of b.

Equations

• Wellwood2015.comparativeTruth role P extract μ a b = Degree.MaxComparative Degree.Comparison.gt (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, (27ii), is the comparative with a weak comparison.

Equations

• Wellwood2015.equativeTruth role P extract μ a b = Degree.MaxComparative Degree.Comparison.ge (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

The derivation

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

The degree phrase with -er, (37i), sets a strict threshold on the measure.

Equations

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

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

The degree phrase with abs, (38ii), sets a weak threshold.

Equations

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

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

The than-clause, (40), (41), denotes the degrees that some eventuality of b's reaches.

Equations

• Wellwood2015.thanClause role P μ b = {d : ℚ | ∃ (e : α), role b e ∧ P e ∧ 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, (37viii), existentially closes the role, the predicate and the degree phrase at the standard δ.

Equations

• Wellwood2015.matrixClause role P μ a δ = ∃ (e : α), role a e ∧ P e ∧ 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

Filling the standard with the maximal than-clause degree is the comparative.

The derivation, type-driven

@[reducible, inline]

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

The sorted domain consists of individuals and eventualities.

Equations

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

def Wellwood2015.lexicon {Ent α D : Type} [LinearOrder D] [Zero D] (role : Ent → α → Prop) (P : α → Prop) (μ0 : α → D) (subj : Ent) (δ : D) : HeimKratzer.Lexicon (Dom Ent α) Unit Id D

In the lexicon much is the measure (7), -er and abs the strict and weak degree heads ((27i), (38ii)), the role head composes by event identification ([Kra96]), and existential closure is an item.

Equations

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

def Wellwood2015.matrixTree : PhraseStructure.Tree Unit String

In the matrix tree, (36), (44), (60), the degree phrase modifies the base predicate, the role head adds the subject, and the event variable is closed.

Equations

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

def Wellwood2015.thanTree : PhraseStructure.Tree Unit String

The than-clause body, (39), (46), (62), is the matrix tree with abs 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 α)) : HeimKratzer.Tree.interp (lexicon role P μ0 a δ) g matrixTree = some ⟨Montague.Ty.t, pure (matrixClause role P μ0 a δ)⟩

The engine derives the matrix clause (37), (45), (61).

theorem Wellwood2015.than_derivation_denotes {Ent α : Type} (role : Ent → α → Prop) (P : α → Prop) (μ0 : α → ℚ) (b : Ent) (d : ℚ) (g : Assignment (Dom Ent α)) : HeimKratzer.Tree.interp (lexicon role P μ0 b d) g thanTree = some ⟨Montague.Ty.t, pure (d ∈ thanClause role P μ0 b)⟩

The engine derives the than-clause pointwise in the degree; abstraction over it (40), (47), (63) is the metalanguage's.

The three domains

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

The nominal comparative, (42), measures the theme of the agent's event.

Equations

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

def Wellwood2015.verbalComparative {Entity : Type u_1} {E : Type u_2} (frame : ArgumentStructure.ThematicFrame Entity E) (P : E → Prop) (μ : E → ℚ) (a b : Entity) : Prop

The verbal comparative, (48), measures the agent's event itself.

Equations

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

def Wellwood2015.adjectivalComparative {Entity : Type u_1} {E : Type u_2} (frame : ArgumentStructure.ThematicFrame Entity E) (P : E → Prop) (μ : E → ℚ) (a b : Entity) : Prop

The adjectival comparative, (65), measures the holder's state itself.

Equations

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

What much measures (26)

def Wellwood2015.NontriviallyStructured {α : Type u_1} [PartialOrder α] (P : α → Prop) : Prop

A domain is non-trivially structured when some satisfier is a proper part of another.

Equations

• Wellwood2015.NontriviallyStructured P = ∃ (x : α) (y : α), P x ∧ P y ∧ x < y

theorem Wellwood2015.not_nontriviallyStructured_of_qua {α : Type u_1} [PartialOrder α] {P : α → Prop} (hQ : Mereology.QUA P) : ¬NontriviallyStructured P

A quantized domain, that of a singular count noun, a telic verb phrase or a non-gradable adjective, is not non-trivially structured.

theorem Wellwood2015.nontriviallyStructured_of_cum {α : Type u_1} [SemilatticeSup α] {P : α → Prop} (hC : Mereology.CUM P) {x y : α} (hx : P x) (hy : P y) (hne : x ≠ y) : NontriviallyStructured P

A cumulative domain with two satisfiers is non-trivially structured, since their sum has one of them as a proper part.

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

On a quantized domain every measure is monotonic vacuously.

theorem Wellwood2015.exists_lt_of_strictMonoOn {α : Type u_1} [PartialOrder α] {P : α → Prop} (hP : NontriviallyStructured P) {μ : α → ℚ} (hμ : StrictMonoOn μ {x : α | P x}) : ∃ (x : α) (y : α), P x ∧ P y ∧ μ x < μ y

On a non-trivially structured domain a monotonic measure separates some pair, so the preservation of structure is non-trivial.

Dimension tracks the measured domain (§3.4)

inductive Wellwood2015.MeasuredDomain : Type

A MeasuredDomain is what a comparative measures, entities, events, or states.

• 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 ⋯

@[instance_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.

@[reducible, inline]

abbrev Wellwood2015.MeasuredDomain.Model : MeasuredDomain → Type

In the order model of a measured domain states are linearly ordered, while entities and events have incomparable parts, like coffee by weight and by volume.

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 := Real.instLE, toLT := Real.instLT, le_refl := ⋯, le_trans := ⋯, 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

Exactly the state domain fixes the comparative ordering for every admissible measure, so hotter and more heat measure intensively because they measure states, fuller and more coffee extensively because they measure entities (82)–(85).

Much Deletion (§3.3, §6.3)

def Wellwood2015.crossCategorialQP : Bresnan1973.QP

[Bre73]'s -er with much is the source of more in every domain.

Equations

• Wellwood2015.crossCategorialQP = { det := { clitic := some Bresnan1973.Clitic.er }, q := Bresnan1973.Q.much }

theorem Wellwood2015.crossCategorialQP_suppletion : crossCategorialQP.suppletion = some Bresnan1973.Form.more

theorem Wellwood2015.very_much_deletion : Bresnan1973.MuchDeletes { det := { }, q := Bresnan1973.Q.much } Bresnan1973.Position.adjective ∧ ¬Bresnan1973.MuchDeletes { det := { }, q := Bresnan1973.Q.much } Bresnan1973.Position.noun ∧ ¬Bresnan1973.MuchDeletes { det := { }, q := Bresnan1973.Q.much } Bresnan1973.Position.phrase

very needs much before a noun or a verb phrase and forbids it before an adjective (117), (118), since much deletes exactly before the adjective of its phrase (74).