Von Stechow 1984: Comparing Semantic Theories of Comparison

[vS84] evaluates eight semantic theories of the comparative — [Rus05], [Pos74], [Wil77], [Seu73], [Lew70], [Kle80], [Cre76b], [Hel81] — against nine phenomena (table (xvii)) and synthesizes them: Russellian definite descriptions of degrees plus an ACTUALLY operator. Russell's ambiguity ("I thought your yacht was larger than it is") is the presence or absence of ACTUALLY in the than-clause, not degree-operator scope. Example stimuli live in Data.Examples.VonStechow1984 (Examples.*).

Main definitions

• deReComparative, deDictoComparative: Russell's ambiguity as an ACTUALLY-anchored vs belief-world than-clause standard (§§II–V)
• moreSem, asSem: synthesis rules R4 (additive more) and R5 (multiplicative as) (§XIII)

Main results

• deDicto_absurd: the ACTUALLY-less reading is contradictory
• maxDeg_witness: modal comparatives as IsGreatest over accessible worlds (§VIII)
• klein_agrees_on_simple: the degree-free ordering matches degree comparison on simple comparatives, not on differentials (§XI)
• moreSem_exceeds_counterfactual_worlds: R13 — too as moreSem with a counterfactual threshold (§XIII.6)

Intensional degree semantics (§§II–V)

deReComparative vs deDictoComparative is von Stechow's analysis of Russell's ambiguity ((1), Examples.yacht): the than-clause standard is either ACTUALLY-anchored to the actual world or evaluated in the belief world — no degree-operator scope is involved. The ambiguous counterfactual ((26), Examples.ex26, §III) works the same way: its trivial reading's clauses are de dicto self-comparisons, contradictory by deDicto_absurd.

def VonStechow1984.intensionalComparative {W : Type u_1} {Entity : Type u_2} {D : Type u_3} [LinearOrder D] (μ : W → Entity → D) (w : W) (a b : Entity) : Prop

Comparative between world-indexed measures (R3): a exceeds b at w.

Equations

• VonStechow1984.intensionalComparative μ w a b = (μ w a > μ w b)

theorem VonStechow1984.intensionalComparative_rigid {W : Type u_1} {Entity : Type u_2} {D : Type u_3} [LinearOrder D] (μe : Entity → D) (w : W) (a b : Entity) : intensionalComparative (Intensional.Intension.rigid μe) w a b ↔ Degree.comparativeSem μe a b Core.Order.ScalePolarity.positive

A rigid measure reduces intensionalComparative to the extensional comparativeSem.

def VonStechow1984.deReComparative {W : Type u_1} {Entity : Type u_2} {D : Type u_3} [LinearOrder D] (μ : W → Entity → D) (w₀ wBel : W) (x : Entity) : Prop

De re reading of "I thought your yacht was larger than it is": the than-clause standard is ACTUALLY-anchored — evaluated at the actual world w₀ — while the matrix is evaluated at the belief world wBel.

Equations

• VonStechow1984.deReComparative μ w₀ wBel x = (μ wBel x > μ w₀ x)

def VonStechow1984.deDictoComparative {W : Type u_1} {Entity : Type u_2} {D : Type u_3} [LinearOrder D] (μ : W → Entity → D) (wBel : W) (x : Entity) : Prop

De dicto reading: no ACTUALLY, so standard and matrix are both evaluated at wBel.

Equations

• VonStechow1984.deDictoComparative μ wBel x = (μ wBel x > μ wBel x)

theorem VonStechow1984.deDicto_absurd {W : Type u_1} {Entity : Type u_2} {D : Type u_3} [LinearOrder D] (μ : W → Entity → D) (wBel : W) (x : Entity) : ¬deDictoComparative μ wBel x

The de dicto reading is contradictory.

theorem VonStechow1984.disjunction_to_conjunction_in_than {D : Type u_3} [LinearOrder D] (μa μb μc : D) (h : max μb μc < μa) : μb < μa ∧ μc < μa

(v) (Examples.exV; §§VI–VII): a disjunctive standard entails both disjuncts — the downward-entailingness of the than-clause that also licenses its NPIs (Degree.comparative_than_DE; Ladusaw1979.licensingStrength .clausalComparative = .antiAdditive).

theorem VonStechow1984.maxDeg_witness {W : Type u_1} {D : Type u_3} [LinearOrder D] {acc : Set W} {μA μB : W → D} {maxA maxB : D} (hmaxA : IsGreatest (μA '' acc) maxA) (hmaxB : IsGreatest (μB '' acc) maxB) (hgt : maxB < maxA) : ∃ w ∈ acc, ∀ v ∈ acc, μB v < μA w

"A polar bear could be bigger than a grizzly bear could be" ((x), Examples.exX; §VIII): if the greatest possible A-degree over the accessible worlds exceeds the greatest possible B-degree, some accessible A-world beats every B-world.

theorem VonStechow1984.klein_agrees_on_simple {Entity : Type u_2} {D : Type u_3} [LinearOrder D] (μ : Entity → D) (cc : Set Entity) (a b : Entity) (ha : a ∈ cc) (hb : b ∈ cc) : Degree.comparativeSem μ a b Core.Order.ScalePolarity.positive ↔ Degree.Delineation.ordering (Degree.Delineation.measureDelineation μ) cc a b

Klein's degree-free ordering ([Kle80]; §XI) matches degree comparison on simple comparatives via measureDelineation; the divergence is confined to differential and factor constructions ((171a)–(171c)).

Synthesis rules R4 (moreSem), R5 (asSem), R13 (too) (§XIII)

def VonStechow1984.moreSem {Entity : Type u_2} {D : Type u_3} [LinearOrder D] [Add D] (μ : Entity → D) (x : Entity) (d₁ d₂ : D) : Prop

R4: ⟦more⟧(d₁)(A⁰)(d₂)(x) iff A⁰(x, d₁ + d₂) with monotone A⁰ — the differential d₁ plus the than-clause maximum d₂.

Equations

• VonStechow1984.moreSem μ x d₁ d₂ = (d₁ + d₂ ≤ μ x)

def VonStechow1984.asSem {Entity : Type u_2} {D : Type u_3} [LinearOrder D] [Mul D] (μ : Entity → D) (x : Entity) (d₁ d₂ : D) : Prop

R5: ⟦as⟧ multiplies where R4 adds ("twice as fat", (171b)).

Equations

• VonStechow1984.asSem μ x d₁ d₂ = (d₁ * d₂ ≤ μ x)

theorem VonStechow1984.moreSem_comparative_bridge {Entity : Type u_2} {D : Type u_3} [LinearOrder D] [AddCommMonoid D] [IsOrderedCancelAddMonoid D] (μ : Entity → D) (a b : Entity) {d₁ : D} (hd₁ : 0 < d₁) (h : moreSem μ a d₁ (μ b)) : Degree.comparativeSem μ a b Core.Order.ScalePolarity.positive

R4 with a positive differential and d₂ = μ b yields the bare comparative.

theorem VonStechow1984.moreSem_differential_bridge {Entity : Type u_2} {D : Type u_3} [LinearOrder D] [AddCommGroup D] [IsOrderedAddMonoid D] (μ : Entity → D) (a b : Entity) (diff : D) (h : Degree.differentialComparative μ a b diff) : moreSem μ a diff (μ b)

An exact differential entails R4's at-least semantics.

theorem VonStechow1984.asSem_equative_bridge {Entity : Type u_2} {D : Type u_3} [LinearOrder D] [MulOneClass D] (μ : Entity → D) (a b : Entity) : asSem μ a 1 (μ b) ↔ Degree.equativeSem μ a b Core.Order.ScalePolarity.positive

R5 at factor 1 is the equative.

theorem VonStechow1984.asSem_factor_bridge {Entity : Type u_2} {D : Type u_3} [LinearOrder D] [Mul D] (μ : Entity → D) (a b : Entity) (factor : D) (h : Degree.factorEquative μ a b factor) : asSem μ a factor (μ b)

A tight factor phrase entails R5's at-least semantics.

theorem VonStechow1984.moreSem_exceeds_counterfactual_worlds {W : Type u_1} {Entity : Type u_2} {D : Type u_3} [LinearOrder D] [AddCommMonoid D] [IsOrderedCancelAddMonoid D] (μ : W → Entity → D) (w₀ : W) (acc : Set W) (x : Entity) {threshold excess : D} (hexcess : 0 < excess) (hmax : IsGreatest ((fun (w : W) => μ w x) '' acc) threshold) (htoo : moreSem (μ w₀) x excess threshold) (w : W) : w ∈ acc → μ w x < μ w₀ x

R13 (p. 69, §XIII.6): ⟦too⟧(d₁)(A⁰)(p)(x) = the max.d [x is d-A⁰] λd₂ [p □→ A⁰(x, d₂ − d₁)] — too is R4's moreSem with a counterfactually determined threshold (DegP head Degree.Head.excessive): when the threshold is greatest over the accessible worlds, being excess too A puts the actual degree above every accessible world's degree.