Von Stechow 1984: Comparing Semantic Theories of Comparison

@cite{von-stechow-1984}

Arnim von Stechow. Comparing Semantic Theories of Comparison. Journal of Semantics 3(1-2): 1–77.

Core Contribution

A systematic evaluation of seven semantic theories of the comparative (Russell, Postal, Williams, Seuren, Lewis, Klein, Cresswell, Hellan) against nine empirical phenomena, culminating in a synthesis that combines Russellian definite descriptions with an ACTUALLY operator.

The key insight: Russell's ambiguity ("I thought your yacht was larger than it is") is explained by the presence or absence of ACTUALLY in the than-clause, NOT by scope differences of degree operators. This is simpler and better motivated than competing scope-based analyses.

Synthesis Rules (§XI)

• R1: Property abstraction — than/as-clauses determine properties of degrees
• R2: Nominalization — the Max operator makes a definite description
• R3: Adjectives as 2-place relations (individuals × degrees)
• R4: more / -er = addition: ⟦more⟧(d₁)(A⁰)(d₂)(x) iff A⁰(x, d₁ + d₂)
• R5: as = multiplication: ⟦as⟧(d₁)(A⁰)(d₂)(x) iff A⁰(x, d₁ · d₂)
• R6: pos with comparison class (average-based contextual standard)

Intensional degree semantics

Migrated from Theories/Semantics/Degree/Intensional.lean (single-paper substrate). World-indexed degree semantics for comparative constructions requiring intensional infrastructure: Russell's ambiguity, modal comparatives, ambiguous counterfactuals.

The central contribution: Russell's ambiguity ("I thought your yacht was larger than it is") is explained by presence or absence of an ACTUALLY operator that fixes evaluation to the actual world, NOT by scope differences of degree operators or definite descriptions.

def VonStechow1984.actuallyDeg {W : Type u_1} {D : Type u_2} (w₀ : W) (f : W → D) : D

Evaluate an intension at the actual world w₀. NOT @cite{kaplan-1989}'s tower-based indexical ACTUALLY (which manipulates context-index pairs for demonstratives) — von Stechow's operator is simpler: given a world-dependent value, extract its extension at w₀. Defined via Core.Intension.evalAt with arguments flipped (world first, for readability in comparative constructions where the actual world is syntactically prominent).

Equations

• VonStechow1984.actuallyDeg w₀ f = Core.Intension.evalAt f w₀

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 with world-indexed measure functions. Adjectives denote 2-place relations between individuals and degrees, evaluated at a world (R3).

Equations

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

theorem VonStechow1984.intensional_extensional_bridge {W : Type u_1} {Entity : Type u_2} {D : Type u_3} [LinearOrder D] (μe : Entity → D) (w : W) (a b : Entity) : intensionalComparative (fun (x : W) => μe) w a b ↔ Semantics.Degree.Comparative.comparativeSem μe a b Core.Scale.ScalePolarity.positive

When μ is rigid (world-invariant), intensionalComparative reduces 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: "I thought your yacht was larger than it ACTUALLY is." The than-clause contains ACTUALLY, so the standard is evaluated at the actual world w₀ while the matrix is evaluated in the belief world wBel. This reading is consistent — one can coherently believe an object exceeds its actual size.

Equations

• VonStechow1984.deReComparative μ w₀ wBel x = (μ wBel x > VonStechow1984.actuallyDeg w₀ fun (w : W) => μ 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: "I thought your yacht was larger than it is." No ACTUALLY — both matrix and standard evaluated in the belief world. Yields a contradictory thought: μ(wBel,x) > μ(wBel,x).

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: no entity can exceed its own degree in any world.

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

The de re reading reduces to comparing belief-world degree against the ACTUALLY-extracted actual-world degree.

def VonStechow1984.IsMaxDegOverWorlds {W : Type u_1} {D : Type u_3} [LinearOrder D] (acc : Set W) (μw : W → D) (d : D) : Prop

Maximal degree across a set of accessible worlds. "The biggest a polar bear could be" = max over ◇-accessible worlds of μ(polar bear). Used for modal comparatives. The acc parameter is a set of worlds (typically {w | R w₀ w = true} for some Core.Logic.Intensional.BAccessRel R and base world w₀).

Equations

• VonStechow1984.IsMaxDegOverWorlds acc μw d = ((∃ w ∈ acc, μw w = d) ∧ ∀ w ∈ acc, μw w ≤ d)

theorem VonStechow1984.isMaxDegOverWorlds_iff_isGreatest {W : Type u_1} {D : Type u_3} [LinearOrder D] (acc : Set W) (μw : W → D) (d : D) : IsMaxDegOverWorlds acc μw d ↔ IsGreatest (μw '' acc) d

IsMaxDegOverWorlds is IsGreatest on the degree image.

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 : IsMaxDegOverWorlds acc μA maxA) (hmaxB : IsMaxDegOverWorlds acc μB maxB) (hgt : maxA > maxB) : ∃ w ∈ acc, ∀ v ∈ acc, μA w > μB v

If the max possible A-degree exceeds the max possible B-degree, then the A-witness world beats every B-world.

Synthesis rules R4 (moreSem), R5 (asSem), R13 (tooSem)

def VonStechow1984.moreSem {Entity : Type u_1} (μ : Entity → ℚ) (x : Entity) (d₁ d₂ : ℚ) : Prop

R4: ⟦more⟧(d₁)(A⁰)(d₂)(x) iff A⁰(x, d₁ + d₂). more / -er is a 4-place relation. The differential d₁ specifies the gap; d₂ is the standard's maximal degree (from the than-clause via Max). Plain comparatives have d₁ > 0 supplied by context; measure-phrase differentials make d₁ explicit.

Equations

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

def VonStechow1984.asSem {Entity : Type u_1} (μ : Entity → ℚ) (x : Entity) (d₁ d₂ : ℚ) : Prop

R5: ⟦as⟧ uses multiplication instead of addition. "Ede is twice as fat as Angelika" = μ(Ede) ≥ 2 · μ(Angelika).

Equations

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

theorem VonStechow1984.moreSem_comparative_bridge {Entity : Type u_1} (μ : Entity → ℚ) (a b : Entity) (d₁ : ℚ) (hd₁ : d₁ > 0) : moreSem μ a d₁ (μ b) → Semantics.Degree.Comparative.comparativeSem μ a b Core.Scale.ScalePolarity.positive

R4 with d₁ > 0 and d₂ = μ(b) yields comparativeSem .positive.

theorem VonStechow1984.moreSem_differential_bridge {Entity : Type u_1} (μ : Entity → ℚ) (a b : Entity) (diff : ℚ) : Semantics.Degree.Differential.differentialComparative μ a b diff → moreSem μ a diff (μ b)

Exact differential entails R4's "at least" semantics.

theorem VonStechow1984.asSem_equative_bridge {Entity : Type u_1} (μ : Entity → ℚ) (a b : Entity) : asSem μ a 1 (μ b) ↔ Semantics.Degree.Comparative.equativeSem μ a b Core.Scale.ScalePolarity.positive

R5 with factor = 1 reduces to equative literal semantics.

theorem VonStechow1984.asSem_factor_bridge {Entity : Type u_1} (μ : Entity → ℚ) (a b : Entity) (factor : ℚ) : Semantics.Degree.Differential.factorEquative μ a b factor → asSem μ a factor (μ b)

R5 reduces to factorEquative when the inequality is tight.

def VonStechow1984.tooSem {Entity : Type u_1} (μ : Entity → ℚ) (x : Entity) (excess threshold : ℚ) : Prop

R13: too is a counterfactual comparative morpheme. Definitionally equal to moreSem — too and -er share the same additive structure, differing only in where the standard comes from (counterfactual vs. than-clause).

Equations

• VonStechow1984.tooSem μ x excess threshold = VonStechow1984.moreSem μ x excess threshold

theorem VonStechow1984.tooSem_eq_moreSem {Entity : Type u_1} (μ : Entity → ℚ) (x : Entity) (excess threshold : ℚ) : tooSem μ x excess threshold ↔ moreSem μ x excess threshold

too and -er are the same additive operator (R4 = R13 structurally).

theorem VonStechow1984.tooSem_exceeds_counterfactual_worlds {W : Type u_1} {Entity : Type u_2} (μ : W → Entity → ℚ) (w₀ : W) (acc : Set W) (x : Entity) (threshold excess : ℚ) (hexcess : excess > 0) (hmax : IsMaxDegOverWorlds acc (fun (w : W) => μ w x) threshold) (htoo : tooSem (μ w₀) x excess threshold) (w : W) : w ∈ acc → μ w₀ x > μ w x

If x is (positively) too A for some counterfactual, then x's actual degree exceeds x's degree in every counterfactual world.

"50 kg too heavy to lift" means in every world where you can lift the pack, it weighs strictly less than it actually does. The excess d₁ > 0 creates the strict gap.

Kripke-modal bridge

def VonStechow1984.accessibleSet {W : Type u_1} (R : W → W → Bool) (w₀ : W) : Set W

Convert a binary accessibility relation to a set of worlds. Bridges abstract intensional degree infrastructure to Kripke frames.

Equations

• VonStechow1984.accessibleSet R w₀ = {w : W | R w₀ w = true}

theorem VonStechow1984.modalComparative_kripke {W : Type u_1} {D : Type u_2} [LinearOrder D] (R : W → W → Bool) (w₀ : W) (μA μB : W → D) (maxA maxB : D) (hmaxA : IsMaxDegOverWorlds (accessibleSet R w₀) μA maxA) (hmaxB : IsMaxDegOverWorlds (accessibleSet R w₀) μB maxB) (hgt : maxA > maxB) : ∃ (w : W), R w₀ w = true ∧ ∀ (v : W), R w₀ v = true → μA w > μB v

Modal comparatives grounded in Kripke accessibility. "A polar bear could be bigger than a grizzly bear could be" means: the max A-degree over ◇-accessible worlds exceeds the max B-degree.

LITTLE–□ non-commutativity (de Morgan)

@cite{buring-2007} §6: degree negation (LITTLE) does not commute with modal operators. Analysis 1 is LITTLE(□(P)) (exceeds the min); Analysis 2 is □(LITTLE(P)) (exceeds every complement). They differ by de Morgan's inequality for infinite meets.

def VonStechow1984.littleOverBox {W : Type u_1} {D : Type u_2} [LinearOrder D] (acc : Set W) (μw : W → D) (d : D) : Prop

Analysis 1: LITTLE scopes over □. "shorter than it has to be wide" = bridge-length < min-required-width.

Equations

• VonStechow1984.littleOverBox acc μw d = ∃ w ∈ acc, d > μw w

def VonStechow1984.boxOverLittle {W : Type u_1} {D : Type u_2} [LinearOrder D] (acc : Set W) (μw : W → D) (d : D) : Prop

Analysis 2: □ scopes over LITTLE. "shorter than it has to be narrow" = bridge-length < max-permitted-narrowness.

Equations

• VonStechow1984.boxOverLittle acc μw d = ∀ w ∈ acc, d > μw w

theorem VonStechow1984.boxOverLittle_implies_littleOverBox {W : Type u_1} {D : Type u_2} [LinearOrder D] (acc : Set W) (μw : W → D) (d : D) (hne : ∃ (w : W), w ∈ acc) : boxOverLittle acc μw d → littleOverBox acc μw d

Analysis 2 (□ over LITTLE) entails Analysis 1 (LITTLE over □), but not vice versa. The non-trivial direction of de Morgan: ⋀(¬Pᵢ) → ¬(⋀Pᵢ).

theorem VonStechow1984.littleOverBox_not_implies_boxOverLittle : ¬∀ (acc : Set Bool) (μw : Bool → ℚ) (d : ℚ), littleOverBox acc μw d → boxOverLittle acc μw d

The converse fails: Analysis 1 does NOT entail Analysis 2. Witness: acc = {w₁, w₂} with μ(w₁) = 5, μ(w₂) = 10, d = 7. Then d > min(5,10) = 5 (Analysis 1 holds) but d ≯ max(5,10) = 10 (Analysis 2 fails). Formal content of @cite{buring-2007} §6.

theorem VonStechow1984.littleBox_collapse_when_uniform {W : Type u_1} {D : Type u_2} [LinearOrder D] (acc : Set W) (μw : W → D) (d : D) (hne : ∃ (w : W), w ∈ acc) (hunif : ∀ w₁ ∈ acc, ∀ w₂ ∈ acc, μw w₁ = μw w₂) : littleOverBox acc μw d ↔ boxOverLittle acc μw d

When all accessible worlds agree on degree (trivial modal base), the two analyses collapse — scope is undetectable. @cite{heim-2001}'s monotone collapse at the modal level.

inductive VonStechow1984.TheoryFamily : Type

Theory families evaluated by von Stechow.

• russellPostalWilliams : TheoryFamily
• seurenLewisKlein : TheoryFamily
• cresswell : TheoryFamily
• hellan : TheoryFamily
• synthesis : TheoryFamily

@[implicit_reducible]

instance VonStechow1984.instDecidableEqTheoryFamily : DecidableEq TheoryFamily

Equations

• VonStechow1984.instDecidableEqTheoryFamily x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance VonStechow1984.instReprTheoryFamily : Repr TheoryFamily

Equations

• VonStechow1984.instReprTheoryFamily = { reprPrec := VonStechow1984.instReprTheoryFamily.repr }

def VonStechow1984.instReprTheoryFamily.repr : TheoryFamily → ℕ → Std.Format

Equations

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

inductive VonStechow1984.Phenomenon : Type

The nine phenomena used as evaluation criteria.

• russellAmbiguity : Phenomenon
• ambiguousCounterfactual : Phenomenon
• npiLicensing : Phenomenon
• quantConnectives : Phenomenon
• unwarrantedInference : Phenomenon
• negativeQuantifiers : Phenomenon
• modalComparative : Phenomenon
• differentialReadings : Phenomenon
• iteratedModality : Phenomenon

@[implicit_reducible]

instance VonStechow1984.instDecidableEqPhenomenon : DecidableEq Phenomenon

Equations

• VonStechow1984.instDecidableEqPhenomenon x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def VonStechow1984.instReprPhenomenon.repr : Phenomenon → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance VonStechow1984.instReprPhenomenon : Repr Phenomenon

Equations

• VonStechow1984.instReprPhenomenon = { reprPrec := VonStechow1984.instReprPhenomenon.repr }

inductive VonStechow1984.Score : Type

Adequacy scores from von Stechow's evaluation.

• plus : Score
• weakPlus : Score
• plusMinus : Score
• weakMinus : Score
• minus : Score
• minusStar : Score

@[implicit_reducible]

instance VonStechow1984.instDecidableEqScore : DecidableEq Score

Equations

• VonStechow1984.instDecidableEqScore x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def VonStechow1984.instReprScore.repr : Score → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• VonStechow1984.instReprScore.repr VonStechow1984.Score.plus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "VonStechow1984.Score.plus")).group prec✝

@[implicit_reducible]

instance VonStechow1984.instReprScore : Repr Score

Equations

• VonStechow1984.instReprScore = { reprPrec := VonStechow1984.instReprScore.repr }

structure VonStechow1984.ScorecardEntry : Type

• theory : TheoryFamily
• phenomenon : Phenomenon
• score : Score

@[implicit_reducible]

instance VonStechow1984.instReprScorecardEntry : Repr ScorecardEntry

Equations

• VonStechow1984.instReprScorecardEntry = { reprPrec := VonStechow1984.instReprScorecardEntry.repr }

def VonStechow1984.instReprScorecardEntry.repr : ScorecardEntry → ℕ → Std.Format

Equations

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

def VonStechow1984.scorecard : List ScorecardEntry

Von Stechow's descriptive adequacy scorecard (p. 4, Table xvii). Scores: Russell ((5)), Seuren/Lewis/Klein (3½), Cresswell (5), Hellan (3). The synthesis achieves 9/9.

Equations

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

structure VonStechow1984.AmbiguousCounterfactualDatum : Type

"If Mary had smoked less than she did, she would be healthier than she is" (p. 12, ex. 26). The nontrivial reading requires ACTUALLY in the than-clauses of both antecedent and consequent: the standards of comparison are actual-world values.

• sentence : String
• trivialReading : String
• informativeReading : String
• requiresActually : Bool

@[implicit_reducible]

instance VonStechow1984.instReprAmbiguousCounterfactualDatum : Repr AmbiguousCounterfactualDatum

Equations

• VonStechow1984.instReprAmbiguousCounterfactualDatum = { reprPrec := VonStechow1984.instReprAmbiguousCounterfactualDatum.repr }

def VonStechow1984.instReprAmbiguousCounterfactualDatum.repr : AmbiguousCounterfactualDatum → ℕ → Std.Format

Equations

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

def VonStechow1984.ambiguousCounterfactual : AmbiguousCounterfactualDatum

Equations

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

structure VonStechow1984.NPIDatum : Type

NPI data from §VI (pp. 26–27).

• sentence : String
• npiItem : String
• grammatical : Bool

@[implicit_reducible]

instance VonStechow1984.instReprNPIDatum : Repr NPIDatum

Equations

• VonStechow1984.instReprNPIDatum = { reprPrec := VonStechow1984.instReprNPIDatum.repr }

def VonStechow1984.instReprNPIDatum.repr : NPIDatum → ℕ → Std.Format

Equations

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

def VonStechow1984.npiData : List NPIDatum

Equations

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

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

"Konstanz is nicer than Düsseldorf or Stuttgart" entails "Konstanz is nicer than Düsseldorf and Stuttgart" (p. 2, ex. v). The than-clause maximum over a disjunctive standard is the max of the individual maxima: exceeding max(μb, μc) entails exceeding both individually.

structure VonStechow1984.InferenceDatum : Type

Blocking unwarranted inferences (p. 3, ex. vii): "Ede is fatter than Max" does NOT entail "Ede is fatter than everyone." Only Russell's theory correctly blocks this — the definite description ιd[everyone is d-fat] may not denote if people differ in fatness.

• premise : String
• conclusion : String
• valid : Bool
• explanation : String

def VonStechow1984.instReprInferenceDatum.repr : InferenceDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance VonStechow1984.instReprInferenceDatum : Repr InferenceDatum

Equations

• VonStechow1984.instReprInferenceDatum = { reprPrec := VonStechow1984.instReprInferenceDatum.repr }

def VonStechow1984.inferences : List InferenceDatum

Equations

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

def VonStechow1984.negativeQuantifierData : List InferenceDatum

Negative quantifiers (p. 3, ex. viii–ix): "*Ede is more intelligent than no one of us" — in Russell's theory, the definite description ιd[no one is d-intelligent] doesn't denote (there's no maximal degree of zero-person intelligence). In Cresswell's theory, (99) is a logical falsehood.

Equations

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

structure VonStechow1984.ModalComparativeDatum : Type

"A polar bear could be bigger than a grizzly bear could be" (p. 3). Only Seuren/Lewis can treat this natively. Russell's theory fails because the definite terms don't denote (indefinitely many possible sizes). Von Stechow's synthesis repairs Russell via the Max operator: compare max possible sizes across ◇-accessible worlds.

• sentence : String
• analysis : String
• theoriesThatHandle : List String

@[implicit_reducible]

instance VonStechow1984.instReprModalComparativeDatum : Repr ModalComparativeDatum

Equations

• VonStechow1984.instReprModalComparativeDatum = { reprPrec := VonStechow1984.instReprModalComparativeDatum.repr }

def VonStechow1984.instReprModalComparativeDatum.repr : ModalComparativeDatum → ℕ → Std.Format

Equations

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

def VonStechow1984.modalComparativeData : ModalComparativeDatum

Equations

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

theorem VonStechow1984.modalComparative_from_maxDeg {W : Type u_1} {D : Type u_2} [LinearOrder D] (acc : Set W) (μPolar μGrizzly : W → D) (maxP maxG : D) (hmaxP : IsMaxDegOverWorlds acc μPolar maxP) (hmaxG : IsMaxDegOverWorlds acc μGrizzly maxG) (hgt : maxP > maxG) : ∃ w ∈ acc, ∀ v ∈ acc, μPolar w > μGrizzly v

Modal comparative: if the max possible A-degree exceeds the max possible B-degree, there is a witness world where A beats every possible B (via maxDeg_witness from the theory layer).

structure VonStechow1984.KleinLimitation : Type

@cite{klein-1980}'s degree-free approach cannot handle:

1. Differential readings: "John is six inches taller than Mary"
2. Factor equatives: "Ede is twice as fat as Angelika"
3. Cross-dimensional: "Ede is more tall than broad"

Klein's framework has no degree ontology, so metric information (distances, ratios) cannot be expressed. The existing klein_measure_equivalence shows Klein agrees on simple comparatives (via measureDelineation), but this agreement breaks down for measure phrase constructions.

This limitation motivates von Stechow's R4/R5 (addition and multiplication on degrees) which Klein cannot express.

• sentence : String
• phenomenon : String
• explanation : String

def VonStechow1984.instReprKleinLimitation.repr : KleinLimitation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance VonStechow1984.instReprKleinLimitation : Repr KleinLimitation

Equations

• VonStechow1984.instReprKleinLimitation = { reprPrec := VonStechow1984.instReprKleinLimitation.repr }

def VonStechow1984.kleinLimitations : List KleinLimitation

Equations

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

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

Klein agrees with von Stechow's synthesis on simple comparatives: the degree comparison μ(a) > μ(b) induces a Klein ordering via measureDelineation (from Compare.klein_measure_equivalence). The divergence is only on differential and factor constructions.

structure VonStechow1984.CrossCategoryDatum : Type

Von Stechow's rules R7–R8 extend more uniformly across categories. Plural nouns: "more toads" = |X| > n (cardinality as degree). Mass nouns: "more gold" = amount(X) > d. Adverbs: "more loudly" = loudness(e) > d. The comparative morpheme is category-blind — only the measure function μ varies.

• sentence : String
• category : String
• measureFunction : String

@[implicit_reducible]

instance VonStechow1984.instReprCrossCategoryDatum : Repr CrossCategoryDatum

Equations

• VonStechow1984.instReprCrossCategoryDatum = { reprPrec := VonStechow1984.instReprCrossCategoryDatum.repr }

def VonStechow1984.instReprCrossCategoryDatum.repr : CrossCategoryDatum → ℕ → Std.Format

Equations

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

def VonStechow1984.crossCategoryData : List CrossCategoryDatum

Equations

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

structure VonStechow1984.TooCounterfactualDatum : Type

R13: too is a counterfactual comparative morpheme. "This pack is at least 50 kg too heavy to lift" means: if it were lighter by 50 kg, one could lift it.

R13 (p. 69): ⟦too⟧(d₁)(A⁰)(p)(x) = the max.d [x is d-A⁰] λd₂ [p □→ A⁰(x, d₂ − d₁)]. Here d₂ is the actual degree and d₁ is the excess; the counterfactual threshold is d₂ − d₁.

This is DegPType.excessive from Degree.Defs — the degree construction where the differential measures the excess over a counterfactual threshold. Von Stechow's analysis shows that too and -er share the same additive structure (R4), differing only in that too's standard comes from a counterfactual rather than a than-clause.

• sentence : String
• differential : String
• counterfactualBase : String
• degPType : Semantics.Degree.DegPType

@[implicit_reducible]

instance VonStechow1984.instReprTooCounterfactualDatum : Repr TooCounterfactualDatum

Equations

• VonStechow1984.instReprTooCounterfactualDatum = { reprPrec := VonStechow1984.instReprTooCounterfactualDatum.repr }

def VonStechow1984.instReprTooCounterfactualDatum.repr : TooCounterfactualDatum → ℕ → Std.Format

Equations

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

def VonStechow1984.tooData : List TooCounterfactualDatum

Equations

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