Documentation

Studies.VonStechow1984

von Stechow (1984): Comparing Semantic Theories of Comparison #

Von Stechow compares eight semantic theories of the comparative against his own synthesis, in which a than-clause denotes a Russellian definite description of a degree and may carry an ACTUALLY operator. Russell's yacht ambiguity is the presence or absence of ACTUALLY in the than-clause, a disjunctive than-clause entails both disjuncts, a modal comparative compares maxima over the accessible worlds, and Klein's degree-free ordering agrees with degree comparison on simple comparatives but not on differentials and factor phrases.

Main results #

Implementation notes #

Degrees form a linear order, with the additive or multiplicative structure the rule at hand needs; measures are world-indexed where ACTUALLY matters and extensional otherwise. The descriptive-adequacy table (xvii) over the eight theories is not transcribed, and the rules R6 to R12 for the positive, nominal, mass and adverbial comparatives are not formalized. The paper's examples are the rows of Data.Examples.VonStechow1984.

References #

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) :

The comparative between world-indexed measures, R3, holds when a exceeds b at w.

Equations
Instances For
    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 (fun (x : W) => μe) w a b ↔ μe b < μe a

    A rigid measure reduces intensionalComparative to the extensional comparison of the two measures.

    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) :

    On the 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
    Instances For
      def VonStechow1984.deDictoComparative {W : Type u_1} {Entity : Type u_2} {D : Type u_3} [LinearOrder D] (μ : W → Entity → D) (wBel : W) (x : Entity) :

      The de dicto reading has no ACTUALLY, so standard and matrix are both evaluated at wBel.

      Equations
      Instances For
        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

        In (v) (Examples.exV, §§VI–VII) a disjunctive standard entails both disjuncts, the downward-entailingness of the than-clause that also licenses its NPIs (Ladusaw1979.IsDownwardEntailing .clausalComparative).

        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

        In 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) :
        μ b < μ a ↔ (Degree.Delineation.ofMeasure μ).Outranks cc a b

        Klein's degree-free ordering ([Kle80]; §XI) matches degree comparison on simple comparatives via Delineation.ofMeasure; 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) :

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

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

          Synthesis rule R5 makes ⟦as⟧ multiply where R4 adds (twice as fat, (171b)).

          Equations
          Instances For
            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)) :
            μ b < μ a

            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) ↔ μ b ≤ μ a

            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

            Synthesis rule R13 (§XIII) is ⟦too⟧(d₁)(A⁰)(p)(x) = the max.d [x is d-A⁰] λd₂ [p □→ A⁰(x, d₂ − d₁)], so 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.