Docs / Semantics / Degree / MeasurePhrase

Measure phrases and the changes of scale they survive

import Linglib.Semantics.Degree.MeasurePhrase · namespace Degree

Source

A differential comparative (3 inches taller) says that two measures differ by a given amount, and a factor equative (twice as tall) that one measure is a given multiple of another. A statement about measures is meaningful when every admissible change of scale preserves it: every strictly increasing map on an ordinal scale, every positive affine map on an interval scale, every positive scaling on a ratio scale. A differential needs differences but no zero, and an affine change of scale carries it to the differential whose amount is the image under the change's linear part. A factor equative needs a zero, so twice as hot is meaningless in degrees Celsius. On an ordinal scale only the zero differential and the factor $1$ survive.

Main definitions

Main statements

Implementation notes

A differential takes degrees in an additive torsor and amounts in its group, so dates or degrees Celsius need no origin; a factor multiplies degrees and so needs a ring. A change of scale carries one statement to another when it semiconjugates adding the first amount, or multiplying by the first factor, to the second.

Errata

  • Stevens 1946 gives the interval group as $x' = ax + b$ with no sign condition, but also says it lies in the isotonic group of increasing maps, which needs $a > 0$.

References

Differentials

The differential comparative a is d-much Adj-er than b holds when the measure of a exceeds that of b by d. It uses differences of degrees and no zero, so the degrees may form an affine space, as on an interval scale.

def DifferentialComparativeL70–74
{E : Type u_1} {V : Type u_2} {P : Type u_3} [VSub V P] (μ : E → P) (a b : E) (d : V) :
Prop

Used by lt_iff_exists_differentialComparative, differentialComparative_comp_of_semiconj, differentialComparative_comp_iff_semiconj, differentialComparative_comp_affineMap, differentialComparative_const_mul_add_const, differentialComparative_const_sub, differentialComparative_comp_strictMono_iff

Used in HayKennedyLevin1999, VanRooij2011, VonStechow1984

L77–80
L87–92
L94–103

An injective affine change of scale carries a differential to the differential whose amount is the image under its linear part, so the differences of an interval scale form a ratio scale.

theorem differentialComparative_comp_affineMapL107–113
{E : Type u_1} {k : Type u_2} {V₁ : Type u_3} {V₂ : Type u_4} {P₁ : Type u_5} {P₂ : Type u_6} [Ring k] [AddCommGroup V₁] [Module k V₁] [AddTorsor V₁ P₁] [AddCommGroup V₂] [Module k V₂] [AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) (hf : Function.Injective ⇑f) (μ : E → P₁) (a b : E) (d : V₁) :
DifferentialComparative (⇑f ∘ μ) a b (f.linear d) ↔ DifferentialComparative μ a b d

Built from

Every strictly increasing change of scale carries a differential to some differential exactly when its amount is zero, so a differential needs more than an ordinal scale.

theorem differentialComparative_comp_strictMono_iffL131–155
{E : Type u_1} {k : Type u_2} [CommRing k] [LinearOrder k] [IsStrictOrderedRing k] [Nontrivial E] {d : k} :
(∀ (g : k → k), StrictMono g → ∃ (d' : k), ∀ (μ : E → k) (a b : E), DifferentialComparative (g ∘ μ) a b d' ↔ DifferentialComparative μ a b d) ↔ d = 0

Built from

Factors

The factor equative a is n times as Adj as b holds when the measure of a is n times that of b. It multiplies degrees, so it needs a zero, as on a ratio scale.

def FactorEquativeL165–168
{E : Type u_1} {D : Type u_2} [Mul D] (μ : E → D) (a b : E) (n : D) :
Prop

Used by factorEquative_comp_of_semiconj, factorEquative_comp_iff_semiconj, factorEquative_const_mul, factorEquative_add_const_iff, factorEquative_comp_strictMono_iff

Used in VanRooij2011, VonStechow1984

L170–174
L176–183
L185–189

Translating a scale by c carries the factor equative of factor n to that of factor n' exactly when n' = n and n fixes c, so moving the zero of a scale destroys ratios.

theorem factorEquative_add_const_iffL191–201
{E : Type u_1} {D : Type u_2} [Ring D] [Nontrivial E] (c n n' : D) :
(∀ (μ : E → D) (a b : E), FactorEquative (fun (x : E) => μ x + c) a b n' ↔ FactorEquative μ a b n) ↔ n' = n ∧ n * c = c

Built from

Every strictly increasing change of scale carries a factor equative to some factor equative exactly when its factor is 1, so a factor equative needs more than an ordinal scale.

theorem factorEquative_comp_strictMono_iffL203–213
{E : Type u_1} {D : Type u_2} {n : D} [Ring D] [LinearOrder D] [IsStrictOrderedRing D] [Nontrivial E] :
(∀ (g : D → D), StrictMono g → ∃ (n' : D), ∀ (μ : E → D) (a b : E), FactorEquative (g ∘ μ) a b n' ↔ FactorEquative μ a b n) ↔ n = 1

Built from